WIP

README2.md

@@ -210,27 +210,38 @@ cargo run -- --help
 // Define a preorder theory
 theory Preorder {
   X : Sort;
-  leq : [a: X, b: X] -> Prop;
 
-  // Reflexivity
-  forall x : X. |- [a: x, b: x] leq;
+  // The ordering relation: x <= y
+  leq : [x: X, y: X] -> Prop;
 
-  // Transitivity
-  forall x : X, y : X, z : X.
-    [a: x, b: y] leq, [a: y, b: z] leq |- [a: x, b: z] leq;
+  // Reflexivity: x <= x
+  ax/refl : forall x : X.
+    |- [x: x, y: x] leq;
+
+  // Transitivity: x <= y and y <= z implies x <= z
+  ax/trans : forall x : X, y : X, z : X.
+    [x: x, y: y] leq, [x: y, y: z] leq |- [x: x, y: z] leq;
 }
 
-// Define an instance
-instance Chain3 : Preorder = {
+// Define an instance with automatic chase
+// The 'chase' keyword applies axioms to compute the closure
+instance Chain3 : Preorder = chase {
   bot : X;
   mid : X;
   top : X;
-  [a: bot, b: mid] leq;
-  [a: mid, b: top] leq;
+
+  // Assert the basic ordering; chase derives reflexive pairs
+  // and transitive closure (bot <= top)
+  [x: bot, y: mid] leq;
+  [x: mid, y: top] leq;
 }
 ```
 
-Then run `:chase Chain3` to compute the transitive closure.
+After loading this file, the chase algorithm automatically computes:
+- Reflexive pairs: `bot <= bot`, `mid <= mid`, `top <= top`
+- Transitive closure: `bot <= top`
+
+You can also define an instance without `chase` and run `:chase Chain3` manually.
 
 ## Development