uri renaming and new nodes count

[helm.git] / helm / software / matita / contribs / LAMBDA-TYPES / Basic-1 / pr3 / props.ma

diff --git a/helm/software/matita/contribs/LAMBDA-TYPES/Basic-1/pr3/props.ma b/helm/software/matita/contribs/LAMBDA-TYPES/Basic-1/pr3/props.ma
index 3569888ebaf64d11180dc02f6cb64e6472448e5c..777f5d85d886636069e512ed5bd96c6b36196f26 100644 (file)
--- a/helm/software/matita/contribs/LAMBDA-TYPES/Basic-1/pr3/props.ma
+++ b/helm/software/matita/contribs/LAMBDA-TYPES/Basic-1/pr3/props.ma
@@ -14,11 +14,11 @@
 
 (* This file was automatically generated: do not edit *********************)
 
-include "LambdaDelta-1/pr3/pr1.ma".
+include "Basic-1/pr3/pr1.ma".
 
-include "LambdaDelta-1/pr2/props.ma".
+include "Basic-1/pr2/props.ma".
 
-include "LambdaDelta-1/pr1/props.ma".
+include "Basic-1/pr1/props.ma".
 
 theorem clear_pr3_trans:
  \forall (c2: C).(\forall (t1: T).(\forall (t2: T).((pr3 c2 t1 t2) \to 
@@ -30,6 +30,9 @@ T).(\lambda (t0: T).(pr3 c1 t t0))) (\lambda (t: T).(pr3_refl c1 t)) (\lambda
 (t3: T).(\lambda (t4: T).(\lambda (H1: (pr2 c2 t4 t3)).(\lambda (t5: 
 T).(\lambda (_: (pr3 c2 t3 t5)).(\lambda (H3: (pr3 c1 t3 t5)).(pr3_sing c1 t3 
 t4 (clear_pr2_trans c2 t4 t3 H1 c1 H0) t5 H3))))))) t1 t2 H)))))).
+(* COMMENTS
+Initial nodes: 107
+END *)
 
 theorem pr3_pr2:
  \forall (c: C).(\forall (t1: T).(\forall (t2: T).((pr2 c t1 t2) \to (pr3 c 
@@ -37,6 +40,9 @@ t1 t2))))
 \def
  \lambda (c: C).(\lambda (t1: T).(\lambda (t2: T).(\lambda (H: (pr2 c t1 
 t2)).(pr3_sing c t2 t1 H t2 (pr3_refl c t2))))).
+(* COMMENTS
+Initial nodes: 31
+END *)
 
 theorem pr3_t:
  \forall (t2: T).(\forall (t1: T).(\forall (c: C).((pr3 c t1 t2) \to (\forall 
@@ -49,6 +55,9 @@ c t t3)).H0))) (\lambda (t0: T).(\lambda (t3: T).(\lambda (H0: (pr2 c t3
 t0)).(\lambda (t4: T).(\lambda (_: (pr3 c t0 t4)).(\lambda (H2: ((\forall 
 (t5: T).((pr3 c t4 t5) \to (pr3 c t0 t5))))).(\lambda (t5: T).(\lambda (H3: 
 (pr3 c t4 t5)).(pr3_sing c t0 t3 H0 t5 (H2 t5 H3)))))))))) t1 t2 H)))).
+(* COMMENTS
+Initial nodes: 127
+END *)
 
 theorem pr3_thin_dx:
  \forall (c: C).(\forall (t1: T).(\forall (t2: T).((pr3 c t1 t2) \to (\forall 
@@ -63,6 +72,9 @@ T).(\lambda (H0: (pr2 c t3 t0)).(\lambda (t4: T).(\lambda (_: (pr3 c t0
 t4)).(\lambda (H2: (pr3 c (THead (Flat f) u t0) (THead (Flat f) u 
 t4))).(pr3_sing c (THead (Flat f) u t0) (THead (Flat f) u t3) (pr2_thin_dx c 
 t3 t0 H0 u f) (THead (Flat f) u t4) H2))))))) t1 t2 H)))))).
+(* COMMENTS
+Initial nodes: 167
+END *)
 
 theorem pr3_head_1:
  \forall (c: C).(\forall (u1: T).(\forall (u2: T).((pr3 c u1 u2) \to (\forall 
@@ -77,6 +89,9 @@ T).(\lambda (t1: T).(\lambda (H0: (pr2 c t1 t2)).(\lambda (t3: T).(\lambda
 (THead k t2 t) (THead k t3 t)))))).(\lambda (k: K).(\lambda (t: T).(pr3_sing 
 c (THead k t2 t) (THead k t1 t) (pr2_head_1 c t1 t2 H0 k t) (THead k t3 t) 
 (H2 k t)))))))))) u1 u2 H)))).
+(* COMMENTS
+Initial nodes: 167
+END *)
 
 theorem pr3_head_2:
  \forall (c: C).(\forall (u: T).(\forall (t1: T).(\forall (t2: T).(\forall 
@@ -91,6 +106,9 @@ T).(\lambda (H0: (pr2 (CHead c k u) t3 t0)).(\lambda (t4: T).(\lambda (_:
 (pr3 (CHead c k u) t0 t4)).(\lambda (H2: (pr3 c (THead k u t0) (THead k u 
 t4))).(pr3_sing c (THead k u t0) (THead k u t3) (pr2_head_2 c u t3 t0 k H0) 
 (THead k u t4) H2))))))) t1 t2 H)))))).
+(* COMMENTS
+Initial nodes: 175
+END *)
 
 theorem pr3_head_21:
  \forall (c: C).(\forall (u1: T).(\forall (u2: T).((pr3 c u1 u2) \to (\forall 
@@ -101,6 +119,9 @@ c (THead k u1 t1) (THead k u2 t2)))))))))
 u2)).(\lambda (k: K).(\lambda (t1: T).(\lambda (t2: T).(\lambda (H0: (pr3 
 (CHead c k u1) t1 t2)).(pr3_t (THead k u1 t2) (THead k u1 t1) c (pr3_head_2 c 
 u1 t1 t2 k H0) (THead k u2 t2) (pr3_head_1 c u1 u2 H k t2))))))))).
+(* COMMENTS
+Initial nodes: 89
+END *)
 
 theorem pr3_head_12:
  \forall (c: C).(\forall (u1: T).(\forall (u2: T).((pr3 c u1 u2) \to (\forall 
@@ -111,6 +132,9 @@ c (THead k u1 t1) (THead k u2 t2)))))))))
 u2)).(\lambda (k: K).(\lambda (t1: T).(\lambda (t2: T).(\lambda (H0: (pr3 
 (CHead c k u2) t1 t2)).(pr3_t (THead k u2 t1) (THead k u1 t1) c (pr3_head_1 c 
 u1 u2 H k t1) (THead k u2 t2) (pr3_head_2 c u2 t1 t2 k H0))))))))).
+(* COMMENTS
+Initial nodes: 89
+END *)
 
 theorem pr3_cflat:
  \forall (c: C).(\forall (t1: T).(\forall (t2: T).((pr3 c t1 t2) \to (\forall 
@@ -124,6 +148,9 @@ T).(\lambda (t4: T).(\lambda (H0: (pr2 c t4 t3)).(\lambda (t5: T).(\lambda
 (_: (pr3 c t3 t5)).(\lambda (H2: ((\forall (f: F).(\forall (v: T).(pr3 (CHead 
 c (Flat f) v) t3 t5))))).(\lambda (f: F).(\lambda (v: T).(pr3_sing (CHead c 
 (Flat f) v) t3 t4 (pr2_cflat c t4 t3 H0 f v) t5 (H2 f v)))))))))) t1 t2 H)))).
+(* COMMENTS
+Initial nodes: 151
+END *)
 
 theorem pr3_flat:
  \forall (c: C).(\forall (u1: T).(\forall (u2: T).((pr3 c u1 u2) \to (\forall 
@@ -134,6 +161,9 @@ theorem pr3_flat:
 u2)).(\lambda (t1: T).(\lambda (t2: T).(\lambda (H0: (pr3 c t1 t2)).(\lambda 
 (f: F).(pr3_head_12 c u1 u2 H (Flat f) t1 t2 (pr3_cflat c t1 t2 H0 f 
 u2))))))))).
+(* COMMENTS
+Initial nodes: 59
+END *)
 
 theorem pr3_pr0_pr2_t:
  \forall (u1: T).(\forall (u2: T).((pr0 u1 u2) \to (\forall (c: C).(\forall 
@@ -205,6 +235,9 @@ u))).(\lambda (_: (((getl i0 (CHead c (Flat f) u2) (CHead d (Bind Abbr) u))
 (CHead c (Flat f) u1) t3 t (pr2_cflat c t3 t (pr2_delta c d u (r (Flat f) i0) 
 (getl_gen_S (Flat f) c (CHead d (Bind Abbr) u) u2 i0 H9) t3 t4 H3 t H8) f 
 u1))))) k H7 IHi))))) i H6 H4))))))))))))) y t1 t2 H1))) H0)))))))).
+(* COMMENTS
+Initial nodes: 1557
+END *)
 
 theorem pr3_pr2_pr2_t:
  \forall (c: C).(\forall (u1: T).(\forall (u2: T).((pr2 c u1 u2) \to (\forall 
@@ -286,6 +319,9 @@ f) t) (CHead d0 (Bind Abbr) u0))).(pr3_pr2 (CHead c0 (Flat f) t1) t4 t6
 (pr2_cflat c0 t4 t6 (pr2_delta c0 d0 u0 (r (Flat f) i1) (getl_gen_S (Flat f) 
 c0 (CHead d0 (Bind Abbr) u0) t i1 H12) t4 t5 H6 t6 H11) f t1)))) k H10))))) 
 i0 H9 H7))))))))))))) y t0 t3 H4))) H3))))))))))))))) c u1 u2 H)))).
+(* COMMENTS
+Initial nodes: 1697
+END *)
 
 theorem pr3_pr2_pr3_t:
  \forall (c: C).(\forall (u2: T).(\forall (t1: T).(\forall (t2: T).(\forall 
@@ -302,6 +338,9 @@ T).(\lambda (H0: (pr2 (CHead c k u2) t3 t0)).(\lambda (t4: T).(\lambda (_:
 \to (pr3 (CHead c k u1) t0 t4))))).(\lambda (u1: T).(\lambda (H3: (pr2 c u1 
 u2)).(pr3_t t0 t3 (CHead c k u1) (pr3_pr2_pr2_t c u1 u2 H3 t3 t0 k H0) t4 (H2 
 u1 H3)))))))))) t1 t2 H)))))).
+(* COMMENTS
+Initial nodes: 199
+END *)
 
 theorem pr3_pr3_pr3_t:
  \forall (c: C).(\forall (u1: T).(\forall (u2: T).((pr3 c u1 u2) \to (\forall 
@@ -318,6 +357,9 @@ t3)).(\lambda (H2: ((\forall (t4: T).(\forall (t5: T).(\forall (k: K).((pr3
 (CHead c k t3) t4 t5) \to (pr3 (CHead c k t2) t4 t5))))))).(\lambda (t0: 
 T).(\lambda (t4: T).(\lambda (k: K).(\lambda (H3: (pr3 (CHead c k t3) t0 
 t4)).(pr3_pr2_pr3_t c t2 t0 t4 k (H2 t0 t4 k H3) t1 H0))))))))))) u1 u2 H)))).
+(* COMMENTS
+Initial nodes: 187
+END *)
 
 theorem pr3_lift:
  \forall (c: C).(\forall (e: C).(\forall (h: nat).(\forall (d: nat).((drop h 
@@ -332,6 +374,9 @@ d t0)))) (\lambda (t: T).(pr3_refl c (lift h d t))) (\lambda (t0: T).(\lambda
 t4)).(\lambda (H3: (pr3 c (lift h d t0) (lift h d t4))).(pr3_sing c (lift h d 
 t0) (lift h d t3) (pr2_lift c e h d H t3 t0 H1) (lift h d t4) H3))))))) t1 t2 
 H0)))))))).
+(* COMMENTS
+Initial nodes: 167
+END *)
 
 theorem pr3_eta:
  \forall (c: C).(\forall (w: T).(\forall (u: T).(let t \def (THead (Bind 
@@ -356,4 +401,7 @@ O) (S O) u) (lift (S O) (S O) u) (pr0_refl (lift (S O) (S O) u))) u (pr1_sing
 Abbr) (TLRef O) (lift (S O) O u)) u (pr0_zeta Abbr not_abbr_abst u u 
 (pr0_refl u) (TLRef O))))) (CHead c (Bind Abst) w))) (lift (S O) O (THead 
 (Bind Abst) w u)) (lift_bind Abst w u (S O) O))))))).
+(* COMMENTS
+Initial nodes: 523
+END *)