X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=matita%2Fmatita%2Fcontribs%2Flambdadelta%2Fbasic_1%2Flift%2Ftlt.ma;h=5adcfd6d895e5ff749ce4d90135516520c47a884;hb=57ae1762497a5f3ea75740e2908e04adb8642cc2;hp=1d8edc7df1ade777f0dce10e9bc7b0b1e35bc855;hpb=88a68a9c334646bc17314d5327cd3b790202acd6;p=helm.git

diff --git a/matita/matita/contribs/lambdadelta/basic_1/lift/tlt.ma b/matita/matita/contribs/lambdadelta/basic_1/lift/tlt.ma
index 1d8edc7df..5adcfd6d8 100644
--- a/matita/matita/contribs/lambdadelta/basic_1/lift/tlt.ma
+++ b/matita/matita/contribs/lambdadelta/basic_1/lift/tlt.ma
@@ -14,11 +14,11 @@
 
 (* This file was automatically generated: do not edit *********************)
 
-include "Basic-1/lift/fwd.ma".
+include "basic_1/lift/props.ma".
 
-include "Basic-1/tlt/props.ma".
+include "basic_1/tlt/props.ma".
 
-theorem lift_weight_map:
+lemma lift_weight_map:
  \forall (t: T).(\forall (h: nat).(\forall (d: nat).(\forall (f: ((nat \to 
 nat))).(((\forall (m: nat).((le d m) \to (eq nat (f m) O)))) \to (eq nat 
 (weight_map f (lift h d t)) (weight_map f t))))))
@@ -105,22 +105,16 @@ 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:
+lemma lift_weight:
  \forall (t: T).(\forall (h: nat).(\forall (d: nat).(eq nat (weight (lift h d 
 t)) (weight t))))
 \def
  \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:
+lemma lift_weight_add:
  \forall (w: nat).(\forall (t: T).(\forall (h: nat).(\forall (d: 
 nat).(\forall (f: ((nat \to nat))).(\forall (g: ((nat \to nat))).(((\forall 
 (m: nat).((lt m d) \to (eq nat (g m) (f m))))) \to ((eq nat (g d) w) \to 
@@ -267,25 +261,19 @@ 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:
+lemma lift_weight_add_O:
  \forall (w: nat).(\forall (t: T).(\forall (h: nat).(\forall (f: ((nat \to 
 nat))).(eq nat (weight_map f (lift h O t)) (weight_map (wadd f w) (lift (S h) 
 O t))))))
 \def
  \lambda (w: nat).(\lambda (t: T).(\lambda (h: nat).(\lambda (f: ((nat \to 
-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))).(lift_weight_add (minus (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))))) 
+(minus_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:
+lemma lift_tlt_dx:
  \forall (k: K).(\forall (u: T).(\forall (t: T).(\forall (h: nat).(\forall 
 (d: nat).(tlt t (THead k u (lift h d t)))))))
 \def
@@ -293,7 +281,4 @@ 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 *)