X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=helm%2Fsoftware%2Fmatita%2Fcontribs%2FLAMBDA-TYPES%2FBasic-1%2Ftlt%2Fprops.ma;h=0b4f16d4181fe4d47b744395a33e8e2af01f9eb4;hb=d3548c16f481b14ce94e64c790bc767c59590050;hp=72b13d733f8628b6a33c31dac064244daa8f3a60;hpb=3531d88e2a19cba027b4b882f8dd74bf37283b9c;p=helm.git

diff --git a/helm/software/matita/contribs/LAMBDA-TYPES/Basic-1/tlt/props.ma b/helm/software/matita/contribs/LAMBDA-TYPES/Basic-1/tlt/props.ma
index 72b13d733..0b4f16d41 100644
--- a/helm/software/matita/contribs/LAMBDA-TYPES/Basic-1/tlt/props.ma
+++ b/helm/software/matita/contribs/LAMBDA-TYPES/Basic-1/tlt/props.ma
@@ -14,7 +14,7 @@
 
 (* This file was automatically generated: do not edit *********************)
 
-include "LambdaDelta-1/tlt/defs.ma".
+include "Basic-1/tlt/defs.ma".
 
 theorem wadd_le:
  \forall (f: ((nat \to nat))).(\forall (g: ((nat \to nat))).(((\forall (n: 
@@ -26,6 +26,9 @@ 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:
  \forall (f: ((nat \to nat))).(\forall (g: ((nat \to nat))).(((\forall (n: 
@@ -38,6 +41,9 @@ 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 *)
 
 theorem wadd_O:
  \forall (n: nat).(eq nat (wadd (\lambda (_: nat).O) O n) O)
@@ -45,6 +51,9 @@ theorem wadd_O:
  \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:
  \forall (t: T).(\forall (f: ((nat \to nat))).(\forall (g: ((nat \to 
@@ -124,6 +133,9 @@ 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:
  \forall (t: T).(\forall (f: ((nat \to nat))).(\forall (g: ((nat \to 
@@ -136,6 +148,9 @@ 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:
  \forall (t: T).(eq nat (weight_map (wadd (\lambda (_: nat).O) O) t) 
@@ -143,6 +158,9 @@ theorem weight_add_O:
 \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:
  \forall (t: T).(\forall (m: nat).(le (weight_map (wadd (\lambda (_: nat).O) 
@@ -152,6 +170,9 @@ O) t) (weight_map (wadd (\lambda (_: nat).O) (S m)) t)))
 (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 *)
 
 theorem tlt_trans:
  \forall (v: T).(\forall (u: T).(\forall (t: T).((tlt u v) \to ((tlt v t) \to 
@@ -160,6 +181,9 @@ 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:
  \forall (k: K).(\forall (u: T).(\forall (t: T).(tlt u (THead k u t))))
@@ -188,6 +212,9 @@ 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:
  \forall (k: K).(\forall (u: T).(\forall (t: T).(tlt t (THead k u t))))
@@ -233,6 +260,9 @@ 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 
@@ -244,6 +274,9 @@ 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) 
@@ -261,4 +294,7 @@ T).(P t0))) (\lambda (n0: nat).(\lambda (H0: ((\forall (m: nat).((lt m n0)
 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 *)