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

diff --git a/helm/software/matita/contribs/LAMBDA-TYPES/Basic-1/lift/tlt.ma b/helm/software/matita/contribs/LAMBDA-TYPES/Basic-1/lift/tlt.ma
index 4e088a122..1d8edc7df 100644
--- a/helm/software/matita/contribs/LAMBDA-TYPES/Basic-1/lift/tlt.ma
+++ b/helm/software/matita/contribs/LAMBDA-TYPES/Basic-1/lift/tlt.ma
@@ -14,9 +14,9 @@
 
 (* This file was automatically generated: do not edit *********************)
 
-include "LambdaDelta-1/lift/fwd.ma".
+include "Basic-1/lift/fwd.ma".
 
-include "LambdaDelta-1/tlt/props.ma".
+include "Basic-1/tlt/props.ma".
 
 theorem lift_weight_map:
  \forall (t: T).(\forall (h: nat).(\forall (d: nat).(\forall (f: ((nat \to 
@@ -105,6 +105,9 @@ t0)) (weight_map f (lift h d t1))) (plus (weight_map f t0) (weight_map f t1))
 (weight_map f (lift h d t1)) (weight_map f t1) (H h d f H1) (H0 h d f H1))) 
 (lift h d (THead (Flat f0) t0 t1)) (lift_head (Flat f0) t0 t1 h d))) 
 k)))))))))) t).
+(* COMMENTS
+Initial nodes: 1969
+END *)
 
 theorem lift_weight:
  \forall (t: T).(\forall (h: nat).(\forall (d: nat).(eq nat (weight (lift h d 
@@ -113,6 +116,9 @@ t)) (weight t))))
  \lambda (t: T).(\lambda (h: nat).(\lambda (d: nat).(lift_weight_map t h d 
 (\lambda (_: nat).O) (\lambda (m: nat).(\lambda (_: (le d m)).(refl_equal nat 
 O)))))).
+(* COMMENTS
+Initial nodes: 31
+END *)
 
 theorem lift_weight_add:
  \forall (w: nat).(\forall (t: T).(\forall (h: nat).(\forall (d: 
@@ -261,6 +267,9 @@ t0)) (weight_map f (lift h d t1))) (plus (weight_map g (lift (S h) d t0))
 (lift (S h) d (THead (Flat f0) t0 t1)) (lift_head (Flat f0) t0 t1 (S h) d)) 
 (lift h d (THead (Flat f0) t0 t1)) (lift_head (Flat f0) t0 t1 h d))) 
 k))))))))))))) t)).
+(* COMMENTS
+Initial nodes: 3697
+END *)
 
 theorem lift_weight_add_O:
  \forall (w: nat).(\forall (t: T).(\forall (h: nat).(\forall (f: ((nat \to 
@@ -272,6 +281,9 @@ nat))).(lift_weight_add (plus (wadd f w O) O) t h O f (wadd f w) (\lambda (m:
 nat).(\lambda (H: (lt m O)).(lt_x_O m H (eq nat (wadd f w m) (f m))))) 
 (plus_n_O (wadd f w O)) (\lambda (m: nat).(\lambda (_: (le O m)).(refl_equal 
 nat (f m)))))))).
+(* COMMENTS
+Initial nodes: 93
+END *)
 
 theorem lift_tlt_dx:
  \forall (k: K).(\forall (u: T).(\forall (t: T).(\forall (h: nat).(\forall 
@@ -281,4 +293,7 @@ theorem lift_tlt_dx:
 (d: nat).(eq_ind nat (weight (lift h d t)) (\lambda (n: nat).(lt n (weight 
 (THead k u (lift h d t))))) (tlt_head_dx k u (lift h d t)) (weight t) 
 (lift_weight t h d)))))).
+(* COMMENTS
+Initial nodes: 71
+END *)