From fcb6bd3e1e317af7cd91d6fced454c7344443e52 Mon Sep 17 00:00:00 2001
From: Hassan Abedi <cogitator.tech@gmail.com>
Date: Fri, 20 Mar 2026 11:05:58 +0100
Subject: [PATCH] WIP

---
 README2.md | 33 ++++++++++++++++++++++-----------
 1 file changed, 22 insertions(+), 11 deletions(-)

diff --git a/README2.md b/README2.md
index 2712125..f3a0fb0 100644
--- a/README2.md
+++ b/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