uri renaming and new nodes count

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

diff --git a/helm/software/matita/contribs/LAMBDA-TYPES/Basic-1/pr3/iso.ma b/helm/software/matita/contribs/LAMBDA-TYPES/Basic-1/pr3/iso.ma
index 51e8083d9e21adb395e1948f5dee4d6b60dd0fcb..c7b2fb7aa60fb4575c2daf66be96966fcb621c54 100644 (file)
--- a/helm/software/matita/contribs/LAMBDA-TYPES/Basic-1/pr3/iso.ma
+++ b/helm/software/matita/contribs/LAMBDA-TYPES/Basic-1/pr3/iso.ma
@@ -14,11 +14,11 @@
 
 (* This file was automatically generated: do not edit *********************)
 
-include "LambdaDelta-1/pr3/fwd.ma".
+include "Basic-1/pr3/fwd.ma".
 
-include "LambdaDelta-1/iso/props.ma".
+include "Basic-1/iso/props.ma".
 
-include "LambdaDelta-1/tlist/props.ma".
+include "Basic-1/tlist/props.ma".
 
 theorem pr3_iso_appls_abbr:
  \forall (c: C).(\forall (d: C).(\forall (w: T).(\forall (i: nat).((getl i c 
@@ -199,6 +199,9 @@ u2 (pr3_t (THead (Bind x0) x5 (THead (Flat Appl) (lift (S O) O x4) x3))
 c x1 x5 H9 (Bind x0) (THead (Flat Appl) (lift (S O) O x4) x2) (THead (Flat 
 Appl) (lift (S O) O x4) x3) (pr3_thin_dx (CHead c (Bind x0) x5) x2 x3 H10 
 (lift (S O) O x4) Appl)) u2 H7)))))))))))))) H4)) H3)))))))) vs)))))).
+(* COMMENTS
+Initial nodes: 3759
+END *)
 
 theorem pr3_iso_appls_cast:
  \forall (c: C).(\forall (v: T).(\forall (t: T).(\forall (vs: TList).(let u1 
@@ -359,6 +362,9 @@ O) O x4) x3)) (THead (Bind x0) x1 (THead (Flat Appl) (lift (S O) O x4) x2)) c
 (pr3_head_12 c x1 x5 H8 (Bind x0) (THead (Flat Appl) (lift (S O) O x4) x2) 
 (THead (Flat Appl) (lift (S O) O x4) x3) (pr3_thin_dx (CHead c (Bind x0) x5) 
 x2 x3 H9 (lift (S O) O x4) Appl)) u2 H6)))))))))))))) H3)) H2)))))))) vs)))).
+(* COMMENTS
+Initial nodes: 3297
+END *)
 
 theorem pr3_iso_appl_bind:
  \forall (b: B).((not (eq B b Abst)) \to (\forall (v1: T).(\forall (v2: 
@@ -581,6 +587,9 @@ H8 (Bind x0) (THead (Flat Appl) (lift (S O) O x4) x2) (THead (Flat Appl)
 O) O x4) Appl))) (THead (Flat Appl) (lift (S O) O x4) (lift (S O) O (THead 
 (Bind x0) x1 x2))) (lift_flat Appl x4 (THead (Bind x0) x1 x2) (S O) O)))) 
 H10))) u2 H6))))))))))))) H3)) H2)))))))))).
+(* COMMENTS
+Initial nodes: 4805
+END *)
 
 theorem pr3_iso_appls_appl_bind:
  \forall (b: B).((not (eq B b Abst)) \to (\forall (v: T).(\forall (u: 
@@ -749,6 +758,9 @@ Appl) (lift (S O) O x4) x2)) c (pr3_head_12 c x1 x5 H9 (Bind x0) (THead (Flat
 Appl) (lift (S O) O x4) x2) (THead (Flat Appl) (lift (S O) O x4) x3) 
 (pr3_thin_dx (CHead c (Bind x0) x5) x2 x3 H10 (lift (S O) O x4) Appl)) u2 
 H7)))))))))))))) H4)) H3))))))))) vs)))))).
+(* COMMENTS
+Initial nodes: 3571
+END *)
 
 theorem pr3_iso_appls_bind:
  \forall (b: B).((not (eq B b Abst)) \to (\forall (vs: TList).(\forall (u: 
@@ -829,6 +841,9 @@ t) t0))) (iso_head t1 t1 (THeads (Flat Appl) ts0 (THead (Flat Appl) t (THead
 (Flat Appl) (TApp (lifts (S O) O ts) (lift (S O) O t)) t0) (theads_tapp (Flat 
 Appl) (lift (S O) O t) t0 (lifts (S O) O ts))) (lifts (S O) O (TApp ts t)) 
 (lifts_tapp (S O) O t ts))))))))))) vs))).
+(* COMMENTS
+Initial nodes: 1681
+END *)
 
 theorem pr3_iso_beta:
  \forall (v: T).(\forall (w: T).(\forall (t: T).(let u1 \def (THead (Flat 
@@ -970,6 +985,9 @@ H5 Abst H17) in (let H22 \def (eq_ind B x0 (\lambda (b: B).(not (eq B b
 Abst))) H3 Abst H17) in (let H23 \def (match (H22 (refl_equal B Abst)) in 
 False return (\lambda (_: False).(pr3 c (THead (Bind Abbr) v t) u2)) with []) 
 in H23))))))))) H14)) H13))))))) H9)))))))))))))) H2)) H1)))))))).
+(* COMMENTS
+Initial nodes: 2459
+END *)
 
 theorem pr3_iso_appls_beta:
  \forall (us: TList).(\forall (v: T).(\forall (w: T).(\forall (t: T).(let u1 
@@ -1131,4 +1149,7 @@ O) O x4) x3)) (THead (Bind x0) x1 (THead (Flat Appl) (lift (S O) O x4) x2)) c
 (pr3_head_12 c x1 x5 H8 (Bind x0) (THead (Flat Appl) (lift (S O) O x4) x2) 
 (THead (Flat Appl) (lift (S O) O x4) x3) (pr3_thin_dx (CHead c (Bind x0) x5) 
 x2 x3 H9 (lift (S O) O x4) Appl)) u2 H6)))))))))))))) H3)) H2)))))))))))) us).
+(* COMMENTS
+Initial nodes: 3345
+END *)