From b7ab0a9d1f0275db32a526faf7cffe9d520b15c8 Mon Sep 17 00:00:00 2001 From: Marcos Magueta Date: Sun, 12 Jul 2026 10:20:13 -0300 Subject: interval characterization proofs and worked examples --- examples/arithmetic.sol | 17 +++++++++++++++++ 1 file changed, 17 insertions(+) create mode 100644 examples/arithmetic.sol (limited to 'examples/arithmetic.sol') 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] -- cgit v1.2.3