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

diff --git a/helm/software/matita/contribs/LAMBDA-TYPES/Basic-1/lift/fwd.ma b/helm/software/matita/contribs/LAMBDA-TYPES/Basic-1/lift/fwd.ma
index 824deac30..324fed2fb 100644
--- a/helm/software/matita/contribs/LAMBDA-TYPES/Basic-1/lift/fwd.ma
+++ b/helm/software/matita/contribs/LAMBDA-TYPES/Basic-1/lift/fwd.ma
@@ -14,7 +14,7 @@
 
 (* This file was automatically generated: do not edit *********************)
 
-include "LambdaDelta-1/lift/defs.ma".
+include "Basic-1/lift/defs.ma".
 
 theorem lift_sort:
  \forall (n: nat).(\forall (h: nat).(\forall (d: nat).(eq T (lift h d (TSort 
@@ -22,6 +22,9 @@ n)) (TSort n))))
 \def
  \lambda (n: nat).(\lambda (_: nat).(\lambda (_: nat).(refl_equal T (TSort 
 n)))).
+(* COMMENTS
+Initial nodes: 13
+END *)
 
 theorem lift_lref_lt:
  \forall (n: nat).(\forall (h: nat).(\forall (d: nat).((lt n d) \to (eq T 
@@ -31,6 +34,9 @@ theorem lift_lref_lt:
 d)).(eq_ind bool true (\lambda (b: bool).(eq T (TLRef (match b with [true 
 \Rightarrow n | false \Rightarrow (plus n h)])) (TLRef n))) (refl_equal T 
 (TLRef n)) (blt n d) (sym_eq bool (blt n d) true (lt_blt d n H)))))).
+(* COMMENTS
+Initial nodes: 72
+END *)
 
 theorem lift_lref_ge:
  \forall (n: nat).(\forall (h: nat).(\forall (d: nat).((le d n) \to (eq T 
@@ -41,6 +47,9 @@ n)).(eq_ind bool false (\lambda (b: bool).(eq T (TLRef (match b with [true
 \Rightarrow n | false \Rightarrow (plus n h)])) (TLRef (plus n h)))) 
 (refl_equal T (TLRef (plus n h))) (blt n d) (sym_eq bool (blt n d) false 
 (le_bge d n H)))))).
+(* COMMENTS
+Initial nodes: 80
+END *)
 
 theorem lift_head:
  \forall (k: K).(\forall (u: T).(\forall (t: T).(\forall (h: nat).(\forall 
@@ -49,6 +58,9 @@ t)))))))
 \def
  \lambda (k: K).(\lambda (u: T).(\lambda (t: T).(\lambda (h: nat).(\lambda 
 (d: nat).(refl_equal T (THead k (lift h d u) (lift h (s k d) t))))))).
+(* COMMENTS
+Initial nodes: 37
+END *)
 
 theorem lift_bind:
  \forall (b: B).(\forall (u: T).(\forall (t: T).(\forall (h: nat).(\forall 
@@ -57,6 +69,9 @@ theorem lift_bind:
 \def
  \lambda (b: B).(\lambda (u: T).(\lambda (t: T).(\lambda (h: nat).(\lambda 
 (d: nat).(refl_equal T (THead (Bind b) (lift h d u) (lift h (S d) t))))))).
+(* COMMENTS
+Initial nodes: 37
+END *)
 
 theorem lift_flat:
  \forall (f: F).(\forall (u: T).(\forall (t: T).(\forall (h: nat).(\forall 
@@ -65,6 +80,9 @@ theorem lift_flat:
 \def
  \lambda (f: F).(\lambda (u: T).(\lambda (t: T).(\lambda (h: nat).(\lambda 
 (d: nat).(refl_equal T (THead (Flat f) (lift h d u) (lift h d t))))))).
+(* COMMENTS
+Initial nodes: 35
+END *)
 
 theorem lift_gen_sort:
  \forall (h: nat).(\forall (d: nat).(\forall (n: nat).(\forall (t: T).((eq T 
@@ -103,6 +121,9 @@ T).(match ee in T return (\lambda (_: T).Prop) with [(TSort _) \Rightarrow
 True | (TLRef _) \Rightarrow False | (THead _ _ _) \Rightarrow False])) I 
 (THead k (lift h d t0) (lift h (s k d) t1)) H2) in (False_ind (eq T (THead k 
 t0 t1) (TSort n)) H3))))))))) t)))).
+(* COMMENTS
+Initial nodes: 613
+END *)
 
 theorem lift_gen_lref:
  \forall (t: T).(\forall (d: nat).(\forall (h: nat).(\forall (i: nat).((eq T 
@@ -162,6 +183,9 @@ H3 \def (eq_ind T (TLRef i) (\lambda (ee: T).(match ee in T return (\lambda
 t1)) H2) in (False_ind (or (land (lt i d) (eq T (THead k t0 t1) (TLRef i))) 
 (land (le (plus d h) i) (eq T (THead k t0 t1) (TLRef (minus i h))))) 
 H3)))))))))))) t).
+(* COMMENTS
+Initial nodes: 1221
+END *)
 
 theorem lift_gen_lref_lt:
  \forall (h: nat).(\forall (d: nat).(\forall (n: nat).((lt n d) \to (\forall 
@@ -181,6 +205,9 @@ d h) n)).(\lambda (H4: (eq T t (TLRef (minus n h)))).(eq_ind_r T (TLRef
 (minus n h)) (\lambda (t0: T).(eq T t0 (TLRef n))) (le_false (plus d h) n (eq 
 T (TLRef (minus n h)) (TLRef n)) H3 (lt_le_S n (plus d h) (le_plus_trans (S 
 n) d h H))) t H4))) H2)) H1)))))))).
+(* COMMENTS
+Initial nodes: 363
+END *)
 
 theorem lift_gen_lref_false:
  \forall (h: nat).(\forall (d: nat).(\forall (n: nat).((le d n) \to ((lt n 
@@ -198,6 +225,9 @@ H4))) H3)) (\lambda (H3: (land (le (plus d h) n) (eq T t (TLRef (minus n
 h))))).(land_ind (le (plus d h) n) (eq T t (TLRef (minus n h))) P (\lambda 
 (H4: (le (plus d h) n)).(\lambda (_: (eq T t (TLRef (minus n h)))).(le_false 
 (plus d h) n P H4 H0))) H3)) H2)))))))))).
+(* COMMENTS
+Initial nodes: 269
+END *)
 
 theorem lift_gen_lref_ge:
  \forall (h: nat).(\forall (d: nat).(\forall (n: nat).((le d n) \to (\forall 
@@ -220,6 +250,9 @@ h) h))) (eq T t (TLRef n)) (\lambda (_: (le (plus d h) (plus n h))).(\lambda
 (H4: (eq T t (TLRef (minus (plus n h) h)))).(eq_ind_r T (TLRef (minus (plus n 
 h) h)) (\lambda (t0: T).(eq T t0 (TLRef n))) (f_equal nat T TLRef (minus 
 (plus n h) h) n (minus_plus_r n h)) t H4))) H2)) H1)))))))).
+(* COMMENTS
+Initial nodes: 473
+END *)
 
 theorem lift_gen_head:
  \forall (k: K).(\forall (u: T).(\forall (t: T).(\forall (x: T).(\forall (h: 
@@ -321,6 +354,9 @@ k y z)))) (\lambda (y: T).(\lambda (_: T).(eq T (lift h d t0) (lift h d y))))
 z)))) t0 t1 (refl_equal T (THead k t0 t1)) (refl_equal T (lift h d t0)) 
 (refl_equal T (lift h (s k d) t1))) u H6))) t H8))) k0 H7))))) H4)) 
 H3))))))))))) x)))).
+(* COMMENTS
+Initial nodes: 2083
+END *)
 
 theorem lift_gen_bind:
  \forall (b: B).(\forall (u: T).(\forall (t: T).(\forall (x: T).(\forall (h: 
@@ -355,6 +391,9 @@ b) y z)))) (\lambda (y: T).(\lambda (_: T).(eq T (lift h d x0) (lift h d
 y)))) (\lambda (_: T).(\lambda (z: T).(eq T (lift h (S d) x1) (lift h (S d) 
 z)))) x0 x1 (refl_equal T (THead (Bind b) x0 x1)) (refl_equal T (lift h d 
 x0)) (refl_equal T (lift h (S d) x1))) u H2) t H3) x H1)))))) H0))))))))).
+(* COMMENTS
+Initial nodes: 637
+END *)
 
 theorem lift_gen_flat:
  \forall (f: F).(\forall (u: T).(\forall (t: T).(\forall (x: T).(\forall (h: 
@@ -389,4 +428,7 @@ T).(eq T (lift h d x0) (lift h d y)))) (\lambda (_: T).(\lambda (z: T).(eq T
 (lift h d x1) (lift h d z)))) x0 x1 (refl_equal T (THead (Flat f) x0 x1)) 
 (refl_equal T (lift h d x0)) (refl_equal T (lift h d x1))) u H2) t H3) x 
 H1)))))) H0))))))))).
+(* COMMENTS
+Initial nodes: 615
+END *)