uri renaming and new nodes count

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

diff --git a/helm/software/matita/contribs/LAMBDA-TYPES/Basic-1/pr2/props.ma b/helm/software/matita/contribs/LAMBDA-TYPES/Basic-1/pr2/props.ma
index 74e2bf65ec1dd39edd9d6389aaa7a1e8d58064be..2faeb6ebdaf2903eb21df2f8459d39b6e5548a60 100644 (file)
--- a/helm/software/matita/contribs/LAMBDA-TYPES/Basic-1/pr2/props.ma
+++ b/helm/software/matita/contribs/LAMBDA-TYPES/Basic-1/pr2/props.ma
@@ -14,13 +14,13 @@
 
 (* This file was automatically generated: do not edit *********************)
 
-include "LambdaDelta-1/pr2/defs.ma".
+include "Basic-1/pr2/defs.ma".
 
-include "LambdaDelta-1/pr0/props.ma".
+include "Basic-1/pr0/props.ma".
 
-include "LambdaDelta-1/getl/drop.ma".
+include "Basic-1/getl/drop.ma".
 
-include "LambdaDelta-1/getl/clear.ma".
+include "Basic-1/getl/clear.ma".
 
 theorem pr2_thin_dx:
  \forall (c: C).(\forall (t1: T).(\forall (t2: T).((pr2 c t1 t2) \to (\forall 
@@ -39,6 +39,9 @@ t3)).(\lambda (t: T).(\lambda (H2: (subst0 i u0 t3 t)).(pr2_delta c0 d u0 i
 H0 (THead (Flat f) u t0) (THead (Flat f) u t3) (pr0_comp u u (pr0_refl u) t0 
 t3 H1 (Flat f)) (THead (Flat f) u t) (subst0_snd (Flat f) u0 t t3 i H2 
 u)))))))))))) c t1 t2 H)))))).
+(* COMMENTS
+Initial nodes: 239
+END *)
 
 theorem pr2_head_1:
  \forall (c: C).(\forall (u1: T).(\forall (u2: T).((pr2 c u1 u2) \to (\forall 
@@ -55,6 +58,9 @@ T).(\lambda (H1: (pr0 t1 t2)).(\lambda (t0: T).(\lambda (H2: (subst0 i u t2
 t0)).(pr2_delta c0 d u i H0 (THead k t1 t) (THead k t2 t) (pr0_comp t1 t2 H1 
 t t (pr0_refl t) k) (THead k t0 t) (subst0_fst u t0 t2 i H2 t k)))))))))))) c 
 u1 u2 H)))))).
+(* COMMENTS
+Initial nodes: 219
+END *)
 
 theorem pr2_head_2:
  \forall (c: C).(\forall (u: T).(\forall (t1: T).(\forall (t2: T).(\forall 
@@ -146,6 +152,9 @@ t0)))))))))) H1 (CHead c (Flat f) u) H5) in (pr2_delta c d u0 (r (Flat f) n)
 (THead (Flat f) u t4) (pr0_comp u u (pr0_refl u) t3 t4 H3 (Flat f)) (THead 
 (Flat f) u t) (subst0_snd (Flat f) u0 t t4 (r (Flat f) n) H4 u))))))))))))) 
 i)))))) k) y t1 t2 H0))) H)))))).
+(* COMMENTS
+Initial nodes: 1947
+END *)
 
 theorem clear_pr2_trans:
  \forall (c2: C).(\forall (t1: T).(\forall (t2: T).((pr2 c2 t1 t2) \to 
@@ -161,6 +170,9 @@ Abbr) u))).(\lambda (t3: T).(\lambda (t4: T).(\lambda (H1: (pr0 t3
 t4)).(\lambda (t: T).(\lambda (H2: (subst0 i u t4 t)).(\lambda (c1: 
 C).(\lambda (H3: (clear c1 c)).(pr2_delta c1 d u i (clear_getl_trans i c 
 (CHead d (Bind Abbr) u) H0 c1 H3) t3 t4 H1 t H2))))))))))))) c2 t1 t2 H)))).
+(* COMMENTS
+Initial nodes: 171
+END *)
 
 theorem pr2_cflat:
  \forall (c: C).(\forall (t1: T).(\forall (t2: T).((pr2 c t1 t2) \to (\forall 
@@ -176,6 +188,9 @@ u))).(\lambda (t3: T).(\lambda (t4: T).(\lambda (H1: (pr0 t3 t4)).(\lambda
 (t: T).(\lambda (H2: (subst0 i u t4 t)).(pr2_delta (CHead c0 (Flat f) v) d u 
 i (getl_flat c0 (CHead d (Bind Abbr) u) i H0 f v) t3 t4 H1 t H2))))))))))) c 
 t1 t2 H)))))).
+(* COMMENTS
+Initial nodes: 175
+END *)
 
 theorem pr2_ctail:
  \forall (c: C).(\forall (t1: T).(\forall (t2: T).((pr2 c t1 t2) \to (\forall 
@@ -190,6 +205,9 @@ nat).(\lambda (H0: (getl i c0 (CHead d (Bind Abbr) u0))).(\lambda (t3:
 T).(\lambda (t4: T).(\lambda (H1: (pr0 t3 t4)).(\lambda (t: T).(\lambda (H2: 
 (subst0 i u0 t4 t)).(pr2_delta (CTail k u c0) (CTail k u d) u0 i (getl_ctail 
 Abbr c0 d u0 i H0 k u) t3 t4 H1 t H2))))))))))) c t1 t2 H)))))).
+(* COMMENTS
+Initial nodes: 171
+END *)
 
 theorem pr2_change:
  \forall (b: B).((not (eq B b Abbr)) \to (\forall (c: C).(\forall (v1: 
@@ -240,6 +258,9 @@ u)) \to ((subst0 i0 u t4 t) \to (pr2 (CHead c (Bind b) v2) t3 t))))).(\lambda
 (getl_head (Bind b) i0 c (CHead d (Bind Abbr) u) (getl_gen_S (Bind b) c 
 (CHead d (Bind Abbr) u) v1 i0 H7) v2) t3 t4 H3 t H8))))) i H6 H4))))))))))))) 
 y t1 t2 H1))) H0)))))))).
+(* COMMENTS
+Initial nodes: 913
+END *)
 
 theorem pr2_lift:
  \forall (c: C).(\forall (e: C).(\forall (h: nat).(\forall (d: nat).((drop h 
@@ -280,4 +301,7 @@ h))))) H13)))))))) H8))) (\lambda (H7: (le d i)).(pr2_delta c d0 u (plus i h)
 (drop_getl_trans_ge i c e d h H (CHead d0 (Bind Abbr) u) H6 H7) (lift h d t3) 
 (lift h d t4) (pr0_lift t3 t4 H3 h d) (lift h d t) (subst0_lift_ge t4 t u i h 
 H4 d H7)))))))))))))))) y t1 t2 H1))) H0)))))))).
+(* COMMENTS
+Initial nodes: 849
+END *)