(* 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))))))
(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
(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
(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 *)