X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=helm%2Fsoftware%2Fmatita%2Fcontribs%2FLAMBDA-TYPES%2FBasic-1%2Flift1%2Ffwd.ma;h=e9ae2d11c2585ae7911db5c947f4a7b31a69100a;hb=de77f79d60ee3c1d30fe03469172950b557441f3;hp=8a164af044947544e94c185b3d5900272dccd3a3;hpb=3531d88e2a19cba027b4b882f8dd74bf37283b9c;p=helm.git

diff --git a/helm/software/matita/contribs/LAMBDA-TYPES/Basic-1/lift1/fwd.ma b/helm/software/matita/contribs/LAMBDA-TYPES/Basic-1/lift1/fwd.ma
index 8a164af04..e9ae2d11c 100644
--- a/helm/software/matita/contribs/LAMBDA-TYPES/Basic-1/lift1/fwd.ma
+++ b/helm/software/matita/contribs/LAMBDA-TYPES/Basic-1/lift1/fwd.ma
@@ -14,9 +14,9 @@
 
 (* This file was automatically generated: do not edit *********************)
 
-include "LambdaDelta-1/lift1/defs.ma".
+include "Basic-1/lift1/defs.ma".
 
-include "LambdaDelta-1/lift/fwd.ma".
+include "Basic-1/lift/fwd.ma".
 
 theorem lift1_sort:
  \forall (n: nat).(\forall (is: PList).(eq T (lift1 is (TSort n)) (TSort n)))
@@ -26,6 +26,9 @@ theorem lift1_sort:
 nat).(\lambda (n1: nat).(\lambda (p: PList).(\lambda (H: (eq T (lift1 p 
 (TSort n)) (TSort n))).(eq_ind_r T (TSort n) (\lambda (t: T).(eq T (lift n0 
 n1 t) (TSort n))) (refl_equal T (TSort n)) (lift1 p (TSort n)) H))))) is)).
+(* COMMENTS
+Initial nodes: 99
+END *)
 
 theorem lift1_lref:
  \forall (hds: PList).(\forall (i: nat).(eq T (lift1 hds (TLRef i)) (TLRef 
@@ -40,6 +43,9 @@ T (lift n n0 t) (TLRef (match (blt (trans p i) n0) with [true \Rightarrow
 (trans p i) | false \Rightarrow (plus (trans p i) n)])))) (refl_equal T 
 (TLRef (match (blt (trans p i) n0) with [true \Rightarrow (trans p i) | false 
 \Rightarrow (plus (trans p i) n)]))) (lift1 p (TLRef i)) (H i))))))) hds).
+(* COMMENTS
+Initial nodes: 165
+END *)
 
 theorem lift1_bind:
  \forall (b: B).(\forall (hds: PList).(\forall (u: T).(\forall (t: T).(eq T 
@@ -61,6 +67,9 @@ n0 (lift1 p u)) (lift n (S n0) (lift1 (Ss p) t))) (\lambda (t0: T).(eq T t0
 (Ss p) t)))) (lift n n0 (THead (Bind b) (lift1 p u) (lift1 (Ss p) t))) 
 (lift_bind b (lift1 p u) (lift1 (Ss p) t) n n0)) (lift1 p (THead (Bind b) u 
 t)) (H u t)))))))) hds)).
+(* COMMENTS
+Initial nodes: 379
+END *)
 
 theorem lift1_flat:
  \forall (f: F).(\forall (hds: PList).(\forall (u: T).(\forall (t: T).(eq T 
@@ -81,6 +90,9 @@ n n0 (lift1 p u)) (lift n n0 (lift1 p t))))) (refl_equal T (THead (Flat f)
 (lift n n0 (lift1 p u)) (lift n n0 (lift1 p t)))) (lift n n0 (THead (Flat f) 
 (lift1 p u) (lift1 p t))) (lift_flat f (lift1 p u) (lift1 p t) n n0)) (lift1 
 p (THead (Flat f) u t)) (H u t)))))))) hds)).
+(* COMMENTS
+Initial nodes: 353
+END *)
 
 theorem lift1_cons_tail:
  \forall (t: T).(\forall (h: nat).(\forall (d: nat).(\forall (hds: PList).(eq 
@@ -94,6 +106,9 @@ nat).(\lambda (n0: nat).(\lambda (p: PList).(\lambda (H: (eq T (lift1
 t)) (\lambda (t0: T).(eq T (lift n n0 t0) (lift n n0 (lift1 p (lift h d 
 t))))) (refl_equal T (lift n n0 (lift1 p (lift h d t)))) (lift1 (PConsTail p 
 h d) t) H))))) hds)))).
+(* COMMENTS
+Initial nodes: 171
+END *)
 
 theorem lifts1_flat:
  \forall (f: F).(\forall (hds: PList).(\forall (t: T).(\forall (ts: 
@@ -114,6 +129,9 @@ hds t0) t2) (THead (Flat f) (lift1 hds t0) (THeads (Flat f) (lifts1 hds t1)
 f) (lifts1 hds t1) (lift1 hds t)))) (lift1 hds (THeads (Flat f) t1 t)) H) 
 (lift1 hds (THead (Flat f) t0 (THeads (Flat f) t1 t))) (lift1_flat f hds t0 
 (THeads (Flat f) t1 t)))))) ts)))).
+(* COMMENTS
+Initial nodes: 329
+END *)
 
 theorem lifts1_nil:
  \forall (ts: TList).(eq TList (lifts1 PNil ts) ts)
@@ -123,6 +141,9 @@ t)) (refl_equal TList TNil) (\lambda (t: T).(\lambda (t0: TList).(\lambda (H:
 (eq TList (lifts1 PNil t0) t0)).(eq_ind_r TList t0 (\lambda (t1: TList).(eq 
 TList (TCons t t1) (TCons t t0))) (refl_equal TList (TCons t t0)) (lifts1 
 PNil t0) H)))) ts).
+(* COMMENTS
+Initial nodes: 83
+END *)
 
 theorem lifts1_cons:
  \forall (h: nat).(\forall (d: nat).(\forall (hds: PList).(\forall (ts: 
@@ -137,4 +158,7 @@ TList).(eq TList (TCons (lift h d (lift1 hds t)) t1) (TCons (lift h d (lift1
 hds t)) (lifts h d (lifts1 hds t0))))) (refl_equal TList (TCons (lift h d 
 (lift1 hds t)) (lifts h d (lifts1 hds t0)))) (lifts1 (PCons h d hds) t0) 
 H)))) ts)))).
+(* COMMENTS
+Initial nodes: 187
+END *)