- the text model now supports invocations of the entity generator (to

[helm.git] / helm / software / lambda-delta / examples / exp_math / T0.hln

diff --git a/helm/software/lambda-delta/examples/exp_math/T0.hln b/helm/software/lambda-delta/examples/exp_math/T0.hln
index a1366dc7dca1a1cba0e9197611c656d271c644f8..aab161e0e1ffd7b42e478e713a9524efd5ec2cd5 100644 (file)
--- a/helm/software/lambda-delta/examples/exp_math/T0.hln
+++ b/helm/software/lambda-delta/examples/exp_math/T0.hln
@@ -19,7 +19,34 @@
 
 \close
 
-\open logical_abbreviations \* [1] 2.3. *\
+\open logical_abbreviations \* [1] 2.3. 2.5. *\
+
+   \def "logical comprehension restricted to classifications"
+      CAll = [q:*Obj->*Prop] [x:*Obj] Cl(x) -> q(x)      
+           : (*Obj -> *Prop) -> *Prop
+
+   \def "logical existence restricted to classifications"
+      CEx = [q:*Obj->*Prop] Ex([x:*Obj] And(Cl(x), q(x)))      
+          : (*Obj -> *Prop) -> *Prop
+
+   \def "logical comprehension restricted to a classification"
+      EAll = [a:*Obj, q:*Obj->*Prop] [x:*Obj] Eta(x, a) -> q(x)      
+           : *Obj => (*Obj -> *Prop) -> *Prop
+
+   \def "logical existence restricted to a classification"
+      EEx = [a:*Obj, q:*Obj->*Prop] Ex([x:*Obj] And(Eta(x, a), q(x)))      
+          : *Obj => (*Obj -> *Prop) -> *Prop
+
+\close
+
+\open non_logical_abbreviations \* [1] 2.4. *\
+
+   \def "convergence of a term to an object"
+      Conv = [t:*Term] EX([y:*Obj] E(t, y)) : *Term -> *Prop
+
+   \def "term-term equivalence"
+      Eq = [t1:*Term, t2:*Term] [y:*Obj] Iff(E(t1, y), E(t2, y))
+         : *Term => *Term -> *Prop
 
 \close