X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=matita%2Fmatita%2Fcontribs%2Flambdadelta%2Fbasic_1%2Ftlt%2Fprops.ma;h=6df71b39e7fc4926af6a854a83a7cae08c96dd95;hb=57ae1762497a5f3ea75740e2908e04adb8642cc2;hp=0b4f16d4181fe4d47b744395a33e8e2af01f9eb4;hpb=88a68a9c334646bc17314d5327cd3b790202acd6;p=helm.git

diff --git a/matita/matita/contribs/lambdadelta/basic_1/tlt/props.ma b/matita/matita/contribs/lambdadelta/basic_1/tlt/props.ma
index 0b4f16d41..6df71b39e 100644
--- a/matita/matita/contribs/lambdadelta/basic_1/tlt/props.ma
+++ b/matita/matita/contribs/lambdadelta/basic_1/tlt/props.ma
@@ -14,9 +14,11 @@
 
 (* This file was automatically generated: do not edit *********************)
 
-include "Basic-1/tlt/defs.ma".
+include "basic_1/T/fwd.ma".
 
-theorem wadd_le:
+include "basic_1/tlt/defs.ma".
+
+lemma wadd_le:
  \forall (f: ((nat \to nat))).(\forall (g: ((nat \to nat))).(((\forall (n: 
 nat).(le (f n) (g n)))) \to (\forall (v: nat).(\forall (w: nat).((le v w) \to 
 (\forall (n: nat).(le (wadd f v n) (wadd g w n))))))))
@@ -26,11 +28,8 @@ nat).(le (f n) (g n)))) \to (\forall (v: nat).(\forall (w: nat).((le v w) \to
 nat).(\lambda (H0: (le v w)).(\lambda (n: nat).(nat_ind (\lambda (n0: 
 nat).(le (wadd f v n0) (wadd g w n0))) H0 (\lambda (n0: nat).(\lambda (_: (le 
 (wadd f v n0) (wadd g w n0))).(H n0))) n))))))).
-(* COMMENTS
-Initial nodes: 81
-END *)
 
-theorem wadd_lt:
+lemma wadd_lt:
  \forall (f: ((nat \to nat))).(\forall (g: ((nat \to nat))).(((\forall (n: 
 nat).(le (f n) (g n)))) \to (\forall (v: nat).(\forall (w: nat).((lt v w) \to 
 (\forall (n: nat).(le (wadd f v n) (wadd g w n))))))))
@@ -38,24 +37,18 @@ nat).(le (f n) (g n)))) \to (\forall (v: nat).(\forall (w: nat).((lt v w) \to
  \lambda (f: ((nat \to nat))).(\lambda (g: ((nat \to nat))).(\lambda (H: 
 ((\forall (n: nat).(le (f n) (g n))))).(\lambda (v: nat).(\lambda (w: 
 nat).(\lambda (H0: (lt v w)).(\lambda (n: nat).(nat_ind (\lambda (n0: 
-nat).(le (wadd f v n0) (wadd g w n0))) (le_S_n v w (le_S (S v) w H0)) 
-(\lambda (n0: nat).(\lambda (_: (le (wadd f v n0) (wadd g w n0))).(H n0))) 
-n))))))).
-(* COMMENTS
-Initial nodes: 95
-END *)
+nat).(le (wadd f v n0) (wadd g w n0))) (le_S_n v w (le_S_n (S v) (S w) (le_S 
+(S (S v)) (S w) (le_n_S (S v) w H0)))) (\lambda (n0: nat).(\lambda (_: (le 
+(wadd f v n0) (wadd g w n0))).(H n0))) n))))))).
 
-theorem wadd_O:
+lemma wadd_O:
  \forall (n: nat).(eq nat (wadd (\lambda (_: nat).O) O n) O)
 \def
  \lambda (n: nat).(nat_ind (\lambda (n0: nat).(eq nat (wadd (\lambda (_: 
 nat).O) O n0) O)) (refl_equal nat O) (\lambda (n0: nat).(\lambda (_: (eq nat 
 (wadd (\lambda (_: nat).O) O n0) O)).(refl_equal nat O))) n).
-(* COMMENTS
-Initial nodes: 53
-END *)
 
-theorem weight_le:
+lemma weight_le:
  \forall (t: T).(\forall (f: ((nat \to nat))).(\forall (g: ((nat \to 
 nat))).(((\forall (n: nat).(le (f n) (g n)))) \to (le (weight_map f t) 
 (weight_map g t)))))
@@ -64,12 +57,12 @@ nat))).(((\forall (n: nat).(le (f n) (g n)))) \to (le (weight_map f t)
 nat))).(\forall (g: ((nat \to nat))).(((\forall (n: nat).(le (f n) (g n)))) 
 \to (le (weight_map f t0) (weight_map g t0)))))) (\lambda (n: nat).(\lambda 
 (f: ((nat \to nat))).(\lambda (g: ((nat \to nat))).(\lambda (_: ((\forall 
-(n0: nat).(le (f n0) (g n0))))).(le_n (weight_map g (TSort n))))))) (\lambda 
-(n: nat).(\lambda (f: ((nat \to nat))).(\lambda (g: ((nat \to nat))).(\lambda 
-(H: ((\forall (n0: nat).(le (f n0) (g n0))))).(H n))))) (\lambda (k: 
-K).(K_ind (\lambda (k0: K).(\forall (t0: T).(((\forall (f: ((nat \to 
-nat))).(\forall (g: ((nat \to nat))).(((\forall (n: nat).(le (f n) (g n)))) 
-\to (le (weight_map f t0) (weight_map g t0)))))) \to (\forall (t1: 
+(n0: nat).(le (f n0) (g n0))))).(le_O_n (weight_map g (TSort n))))))) 
+(\lambda (n: nat).(\lambda (f: ((nat \to nat))).(\lambda (g: ((nat \to 
+nat))).(\lambda (H: ((\forall (n0: nat).(le (f n0) (g n0))))).(H n))))) 
+(\lambda (k: K).(K_ind (\lambda (k0: K).(\forall (t0: T).(((\forall (f: ((nat 
+\to nat))).(\forall (g: ((nat \to nat))).(((\forall (n: nat).(le (f n) (g 
+n)))) \to (le (weight_map f t0) (weight_map g t0)))))) \to (\forall (t1: 
 T).(((\forall (f: ((nat \to nat))).(\forall (g: ((nat \to nat))).(((\forall 
 (n: nat).(le (f n) (g n)))) \to (le (weight_map f t1) (weight_map g t1)))))) 
 \to (\forall (f: ((nat \to nat))).(\forall (g: ((nat \to nat))).(((\forall 
@@ -112,17 +105,17 @@ t0) (weight_map g t0))))))).(\lambda (t1: T).(\lambda (H0: ((\forall (f:
 (plus (weight_map g t0) (weight_map (wadd g O) t1)) (le_plus_plus (weight_map 
 f t0) (weight_map g t0) (weight_map (wadd f O) t1) (weight_map (wadd g O) t1) 
 (H f g H1) (H0 (wadd f O) (wadd g O) (\lambda (n: nat).(wadd_le f g H1 O O 
-(le_n O) n)))))))))))) (\lambda (t0: T).(\lambda (H: ((\forall (f: ((nat \to 
-nat))).(\forall (g: ((nat \to nat))).(((\forall (n: nat).(le (f n) (g n)))) 
-\to (le (weight_map f t0) (weight_map g t0))))))).(\lambda (t1: T).(\lambda 
-(H0: ((\forall (f: ((nat \to nat))).(\forall (g: ((nat \to nat))).(((\forall 
-(n: nat).(le (f n) (g n)))) \to (le (weight_map f t1) (weight_map g 
-t1))))))).(\lambda (f: ((nat \to nat))).(\lambda (g: ((nat \to 
+(le_O_n O) n)))))))))))) (\lambda (t0: T).(\lambda (H: ((\forall (f: ((nat 
+\to nat))).(\forall (g: ((nat \to nat))).(((\forall (n: nat).(le (f n) (g 
+n)))) \to (le (weight_map f t0) (weight_map g t0))))))).(\lambda (t1: 
+T).(\lambda (H0: ((\forall (f: ((nat \to nat))).(\forall (g: ((nat \to 
+nat))).(((\forall (n: nat).(le (f n) (g n)))) \to (le (weight_map f t1) 
+(weight_map g t1))))))).(\lambda (f: ((nat \to nat))).(\lambda (g: ((nat \to 
 nat))).(\lambda (H1: ((\forall (n: nat).(le (f n) (g n))))).(le_n_S (plus 
 (weight_map f t0) (weight_map (wadd f O) t1)) (plus (weight_map g t0) 
 (weight_map (wadd g O) t1)) (le_plus_plus (weight_map f t0) (weight_map g t0) 
 (weight_map (wadd f O) t1) (weight_map (wadd g O) t1) (H f g H1) (H0 (wadd f 
-O) (wadd g O) (\lambda (n: nat).(wadd_le f g H1 O O (le_n O) n)))))))))))) 
+O) (wadd g O) (\lambda (n: nat).(wadd_le f g H1 O O (le_O_n O) n)))))))))))) 
 b)) (\lambda (_: F).(\lambda (t0: T).(\lambda (H: ((\forall (f0: ((nat \to 
 nat))).(\forall (g: ((nat \to nat))).(((\forall (n: nat).(le (f0 n) (g n)))) 
 \to (le (weight_map f0 t0) (weight_map g t0))))))).(\lambda (t1: T).(\lambda 
@@ -133,11 +126,8 @@ nat))).(\lambda (H1: ((\forall (n: nat).(le (f0 n) (g n))))).(le_n_S (plus
 (weight_map f0 t0) (weight_map f0 t1)) (plus (weight_map g t0) (weight_map g 
 t1)) (le_plus_plus (weight_map f0 t0) (weight_map g t0) (weight_map f0 t1) 
 (weight_map g t1) (H f0 g H1) (H0 f0 g H1))))))))))) k)) t).
-(* COMMENTS
-Initial nodes: 1309
-END *)
 
-theorem weight_eq:
+lemma weight_eq:
  \forall (t: T).(\forall (f: ((nat \to nat))).(\forall (g: ((nat \to 
 nat))).(((\forall (n: nat).(eq nat (f n) (g n)))) \to (eq nat (weight_map f 
 t) (weight_map g t)))))
@@ -148,31 +138,22 @@ nat))).(\lambda (H: ((\forall (n: nat).(eq nat (f n) (g n))))).(le_antisym
 nat).(eq_ind_r nat (g n) (\lambda (n0: nat).(le n0 (g n))) (le_n (g n)) (f n) 
 (H n)))) (weight_le t g f (\lambda (n: nat).(eq_ind_r nat (g n) (\lambda (n0: 
 nat).(le (g n) n0)) (le_n (g n)) (f n) (H n)))))))).
-(* COMMENTS
-Initial nodes: 121
-END *)
 
-theorem weight_add_O:
+lemma weight_add_O:
  \forall (t: T).(eq nat (weight_map (wadd (\lambda (_: nat).O) O) t) 
 (weight_map (\lambda (_: nat).O) t))
 \def
  \lambda (t: T).(weight_eq t (wadd (\lambda (_: nat).O) O) (\lambda (_: 
 nat).O) (\lambda (n: nat).(wadd_O n))).
-(* COMMENTS
-Initial nodes: 23
-END *)
 
-theorem weight_add_S:
+lemma weight_add_S:
  \forall (t: T).(\forall (m: nat).(le (weight_map (wadd (\lambda (_: nat).O) 
 O) t) (weight_map (wadd (\lambda (_: nat).O) (S m)) t)))
 \def
  \lambda (t: T).(\lambda (m: nat).(weight_le t (wadd (\lambda (_: nat).O) O) 
 (wadd (\lambda (_: nat).O) (S m)) (\lambda (n: nat).(wadd_le (\lambda (_: 
-nat).O) (\lambda (_: nat).O) (\lambda (_: nat).(le_n O)) O (S m) (le_S O m 
-(le_O_n m)) n)))).
-(* COMMENTS
-Initial nodes: 61
-END *)
+nat).O) (\lambda (_: nat).O) (\lambda (_: nat).(le_O_n O)) O (S m) (le_O_n (S 
+m)) n)))).
 
 theorem tlt_trans:
  \forall (v: T).(\forall (u: T).(\forall (t: T).((tlt u v) \to ((tlt v t) \to 
@@ -181,11 +162,8 @@ theorem tlt_trans:
  \lambda (v: T).(\lambda (u: T).(\lambda (t: T).(\lambda (H: (lt (weight u) 
 (weight v))).(\lambda (H0: (lt (weight v) (weight t))).(lt_trans (weight u) 
 (weight v) (weight t) H H0))))).
-(* COMMENTS
-Initial nodes: 43
-END *)
 
-theorem tlt_head_sx:
+lemma tlt_head_sx:
  \forall (k: K).(\forall (u: T).(\forall (t: T).(tlt u (THead k u t))))
 \def
  \lambda (k: K).(K_ind (\lambda (k0: K).(\forall (u: T).(\forall (t: T).(lt 
@@ -212,11 +190,8 @@ t))))) b)) (\lambda (_: F).(\lambda (u: T).(\lambda (t: T).(le_n_S
 (weight_map (\lambda (_: nat).O) u) (plus (weight_map (\lambda (_: nat).O) u) 
 (weight_map (\lambda (_: nat).O) t)) (le_plus_l (weight_map (\lambda (_: 
 nat).O) u) (weight_map (\lambda (_: nat).O) t)))))) k).
-(* COMMENTS
-Initial nodes: 379
-END *)
 
-theorem tlt_head_dx:
+lemma tlt_head_dx:
  \forall (k: K).(\forall (u: T).(\forall (t: T).(tlt t (THead k u t))))
 \def
  \lambda (k: K).(K_ind (\lambda (k0: K).(\forall (u: T).(\forall (t: T).(lt 
@@ -260,41 +235,4 @@ T).(\lambda (t: T).(le_n_S (weight_map (\lambda (_: nat).O) t) (plus
 (weight_map (\lambda (_: nat).O) u) (weight_map (\lambda (_: nat).O) t)) 
 (le_plus_r (weight_map (\lambda (_: nat).O) u) (weight_map (\lambda (_: 
 nat).O) t)))))) k).
-(* COMMENTS
-Initial nodes: 659
-END *)
-
-theorem tlt_wf__q_ind:
- \forall (P: ((T \to Prop))).(((\forall (n: nat).((\lambda (P0: ((T \to 
-Prop))).(\lambda (n0: nat).(\forall (t: T).((eq nat (weight t) n0) \to (P0 
-t))))) P n))) \to (\forall (t: T).(P t)))
-\def
- let Q \def (\lambda (P: ((T \to Prop))).(\lambda (n: nat).(\forall (t: 
-T).((eq nat (weight t) n) \to (P t))))) in (\lambda (P: ((T \to 
-Prop))).(\lambda (H: ((\forall (n: nat).(\forall (t: T).((eq nat (weight t) 
-n) \to (P t)))))).(\lambda (t: T).(H (weight t) t (refl_equal nat (weight 
-t)))))).
-(* COMMENTS
-Initial nodes: 61
-END *)
-
-theorem tlt_wf_ind:
- \forall (P: ((T \to Prop))).(((\forall (t: T).(((\forall (v: T).((tlt v t) 
-\to (P v)))) \to (P t)))) \to (\forall (t: T).(P t)))
-\def
- let Q \def (\lambda (P: ((T \to Prop))).(\lambda (n: nat).(\forall (t: 
-T).((eq nat (weight t) n) \to (P t))))) in (\lambda (P: ((T \to 
-Prop))).(\lambda (H: ((\forall (t: T).(((\forall (v: T).((lt (weight v) 
-(weight t)) \to (P v)))) \to (P t))))).(\lambda (t: T).(tlt_wf__q_ind 
-(\lambda (t0: T).(P t0)) (\lambda (n: nat).(lt_wf_ind n (Q (\lambda (t0: 
-T).(P t0))) (\lambda (n0: nat).(\lambda (H0: ((\forall (m: nat).((lt m n0) 
-\to (Q (\lambda (t0: T).(P t0)) m))))).(\lambda (t0: T).(\lambda (H1: (eq nat 
-(weight t0) n0)).(let H2 \def (eq_ind_r nat n0 (\lambda (n1: nat).(\forall 
-(m: nat).((lt m n1) \to (\forall (t1: T).((eq nat (weight t1) m) \to (P 
-t1)))))) H0 (weight t0) H1) in (H t0 (\lambda (v: T).(\lambda (H3: (lt 
-(weight v) (weight t0))).(H2 (weight v) H3 v (refl_equal nat (weight 
-v))))))))))))) t)))).
-(* COMMENTS
-Initial nodes: 179
-END *)