interval characterization proofs and worked examples

1 files changed, 17 insertions, 0 deletions

diff --git a/examples/arithmetic.sol b/examples/arithmetic.sol
new file mode 100644
index 0000000..a56d82e
--- /dev/null
+++ b/examples/arithmetic.sol
@@ -0,0 +1,17 @@
+% Arithmetic solves backward, and the numeric tower keeps its
+% minimal shape: an integer-valued rational IS the integer.
+
+% Forward: 3 + 4.
+Query expression: [Plus left: 3 right: 4 result: R]
+
+% Backward: what plus 5 gives 12?
+Query expression: [Plus left: X right: 5 result: 12]
+
+% Through the rationals: 3 * X = 2.
+Query expression: [Times left: 3 right: X result: 2]
+
+% Minimal shape: 1/2 + 1/2 is the integer 1, not the rational 2/2.
+Query expression: [Plus left: 1/2 right: 1/2 result: R]
+
+% Rationals reduce on sight: 2/4 equals 1/2.
+Query expression: [Equal left: 2/4 right: 1/2]