X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=helm%2Fsoftware%2Flambda-delta%2Fexamples%2Fexp_math%2FT0.hln;h=aab161e0e1ffd7b42e478e713a9524efd5ec2cd5;hb=55d6dde568f1daf1fa6902428bda7caec147375a;hp=a1366dc7dca1a1cba0e9197611c656d271c644f8;hpb=4c157ac5c58f34fffc98289c2d2e71032d584a83;p=helm.git

diff --git a/helm/software/lambda-delta/examples/exp_math/T0.hln b/helm/software/lambda-delta/examples/exp_math/T0.hln
index a1366dc7d..aab161e0e 100644
--- 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