interval characterization proofs and worked examples

1 files changed, 27 insertions, 0 deletions

diff --git a/examples/constraints.sol b/examples/constraints.sol
new file mode 100644
index 0000000..676f4c1
--- /dev/null
+++ b/examples/constraints.sol
@@ -0,0 +1,27 @@
+% Membership is not generation. Open membership constrains; the
+% engine residuates, propagates, and enumerates only finite ranges.
+
+% An open constraint comes back as the answer's condition.
+Query expression: [Integer value: X]
+
+% A later equality grounds it and the residue discharges.
+Query expression: [Natural value: X] :and [Equal left: X right: 5]
+
+% Bounds that pin an integer into a finite range enumerate, the
+% same admissible enumeration Between performs explicitly.
+Query expression: [Natural value: X] :and [LessThan left: X right: 4]
+
+% Strict rational bounds tighten to integers: 1/2 < X <= 5/2.
+Query expression:
+  [Integer value: X] :and
+  [GreaterThan left: X right: 1/2] :and
+  [LessThanEqual left: X right: 5/2]
+
+% An empty interval is no, not a conditioned maybe.
+Query expression: [GreaterThan left: X right: 5] :and [LessThan left: X right: 3]
+
+% Explicit bounded generation.
+Query expression: [Between value: X lower: 1 upper: 4] :and [GreaterThan left: X right: 2]
+
+% Disjunction branches finitely.
+Query expression: [Equal left: X right: 1] :or [Equal left: X right: 2]