X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=helm%2Fsoftware%2Fmatita%2Fcontribs%2FLAMBDA-TYPES%2FBasic-1%2Fex0%2Fprops.ma;h=96dd77da32096e890b34708d6eafeed56ea78c3b;hb=a4cd6a8a1d6a008518c12daca794b9e811c1dee5;hp=148879216ca30fefbabaee3675b8da399f34e3ee;hpb=3531d88e2a19cba027b4b882f8dd74bf37283b9c;p=helm.git

diff --git a/helm/software/matita/contribs/LAMBDA-TYPES/Basic-1/ex0/props.ma b/helm/software/matita/contribs/LAMBDA-TYPES/Basic-1/ex0/props.ma
index 148879216..96dd77da3 100644
--- a/helm/software/matita/contribs/LAMBDA-TYPES/Basic-1/ex0/props.ma
+++ b/helm/software/matita/contribs/LAMBDA-TYPES/Basic-1/ex0/props.ma
@@ -14,11 +14,11 @@
 
 (* This file was automatically generated: do not edit *********************)
 
-include "LambdaDelta-1/ex0/defs.ma".
+include "Basic-1/ex0/defs.ma".
 
-include "LambdaDelta-1/leq/defs.ma".
+include "Basic-1/leq/defs.ma".
 
-include "LambdaDelta-1/aplus/props.ma".
+include "Basic-1/aplus/props.ma".
 
 theorem aplus_gz_le:
  \forall (k: nat).(\forall (h: nat).(\forall (n: nat).((le h k) \to (eq A 
@@ -52,6 +52,9 @@ k0)) a)) (eq_ind A (aplus gz (asucc gz (ASort (S n) n0)) k0) (\lambda (a:
 A).(eq A a (aplus gz (ASort n n0) k0))) (refl_equal A (aplus gz (ASort n n0) 
 k0)) (asucc gz (aplus gz (ASort (S n) n0) k0)) (aplus_asucc gz k0 (ASort (S 
 n) n0))) (ASort O (plus (minus k0 n) n0)) (IH n n0 H_y))))))) h)))) k).
+(* COMMENTS
+Initial nodes: 683
+END *)
 
 theorem aplus_gz_ge:
  \forall (n: nat).(\forall (k: nat).(\forall (h: nat).((le k h) \to (eq A 
@@ -79,6 +82,9 @@ gz (ASort (S n0) n) k0)) a)) (eq_ind A (aplus gz (asucc gz (ASort (S n0) n))
 k0) (\lambda (a: A).(eq A a (aplus gz (ASort n0 n) k0))) (refl_equal A (aplus 
 gz (ASort n0 n) k0)) (asucc gz (aplus gz (ASort (S n0) n) k0)) (aplus_asucc 
 gz k0 (ASort (S n0) n))) (ASort (minus n0 k0) n) (IH n0 H_y)))))) h)))) k)).
+(* COMMENTS
+Initial nodes: 524
+END *)
 
 theorem next_plus_gz:
  \forall (n: nat).(\forall (h: nat).(eq nat (next_plus gz n h) (plus h n)))
@@ -87,6 +93,9 @@ theorem next_plus_gz:
 (next_plus gz n n0) (plus n0 n))) (refl_equal nat n) (\lambda (n0: 
 nat).(\lambda (H: (eq nat (next_plus gz n n0) (plus n0 n))).(f_equal nat nat 
 S (next_plus gz n n0) (plus n0 n) H))) h)).
+(* COMMENTS
+Initial nodes: 77
+END *)
 
 theorem leqz_leq:
  \forall (a1: A).(\forall (a2: A).((leq gz a1 a2) \to (leqz a1 a2)))
@@ -156,6 +165,9 @@ plus) (minus k h1) n1)])) (ASort O (plus (minus k h1) n1)) (ASort O (plus
 A).(\lambda (_: (leq gz a0 a3)).(\lambda (H1: (leqz a0 a3)).(\lambda (a4: 
 A).(\lambda (a5: A).(\lambda (_: (leq gz a4 a5)).(\lambda (H3: (leqz a4 
 a5)).(leqz_head a0 a3 H1 a4 a5 H3))))))))) a1 a2 H))).
+(* COMMENTS
+Initial nodes: 1375
+END *)
 
 theorem leq_leqz:
  \forall (a1: A).(\forall (a2: A).((leqz a1 a2) \to (leq gz a1 a2)))
@@ -189,4 +201,7 @@ h2)) (aplus_asort_simpl gz (plus h1 h2) h1 n1)))))))) (\lambda (a0:
 A).(\lambda (a3: A).(\lambda (_: (leqz a0 a3)).(\lambda (H1: (leq gz a0 
 a3)).(\lambda (a4: A).(\lambda (a5: A).(\lambda (_: (leqz a4 a5)).(\lambda 
 (H3: (leq gz a4 a5)).(leq_head gz a0 a3 H1 a4 a5 H3))))))))) a1 a2 H))).
+(* COMMENTS
+Initial nodes: 717
+END *)