X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;ds=sidebyside;f=matita%2Fmatita%2Fcontribs%2Flambdadelta%2Fbasic_1%2Fflt%2Fprops.ma;h=61344ece03b5981257939e4a3039d19e4e8a116a;hb=639e798161afea770f41d78673c0fe3be4125beb;hp=8c69278e3f650be261b5d1714d1238f15304f56d;hpb=15455aa487e001c643b4f46daf82612b8409f1ae;p=helm.git

diff --git a/matita/matita/contribs/lambdadelta/basic_1/flt/props.ma b/matita/matita/contribs/lambdadelta/basic_1/flt/props.ma
index 8c69278e3..61344ece0 100644
--- a/matita/matita/contribs/lambdadelta/basic_1/flt/props.ma
+++ b/matita/matita/contribs/lambdadelta/basic_1/flt/props.ma
@@ -22,68 +22,38 @@ theorem flt_thead_sx:
  \forall (k: K).(\forall (c: C).(\forall (u: T).(\forall (t: T).(flt c u c 
 (THead k u t)))))
 \def
- \lambda (_: K).(\lambda (c: C).(\lambda (u: T).(\lambda (t: T).(let TMP_1 
-\def (tweight u) in (let TMP_2 \def (tweight u) in (let TMP_3 \def (tweight 
-t) in (let TMP_4 \def (plus TMP_2 TMP_3) in (let TMP_5 \def (S TMP_4) in (let 
-TMP_6 \def (cweight c) in (let TMP_7 \def (tweight u) in (let TMP_8 \def 
-(tweight u) in (let TMP_9 \def (tweight t) in (let TMP_10 \def (plus TMP_8 
-TMP_9) in (let TMP_11 \def (tweight u) in (let TMP_12 \def (tweight t) in 
-(let TMP_13 \def (le_plus_l TMP_11 TMP_12) in (let TMP_14 \def (le_n_S TMP_7 
-TMP_10 TMP_13) in (lt_reg_l TMP_1 TMP_5 TMP_6 TMP_14)))))))))))))))))).
+ \lambda (_: K).(\lambda (c: C).(\lambda (u: T).(\lambda (t: T).(lt_reg_l 
+(tweight u) (S (plus (tweight u) (tweight t))) (cweight c) (le_n_S (tweight 
+u) (plus (tweight u) (tweight t)) (le_plus_l (tweight u) (tweight t))))))).
 
 theorem flt_thead_dx:
  \forall (k: K).(\forall (c: C).(\forall (u: T).(\forall (t: T).(flt c t c 
 (THead k u t)))))
 \def
- \lambda (_: K).(\lambda (c: C).(\lambda (u: T).(\lambda (t: T).(let TMP_1 
-\def (tweight t) in (let TMP_2 \def (tweight u) in (let TMP_3 \def (tweight 
-t) in (let TMP_4 \def (plus TMP_2 TMP_3) in (let TMP_5 \def (S TMP_4) in (let 
-TMP_6 \def (cweight c) in (let TMP_7 \def (tweight t) in (let TMP_8 \def 
-(tweight u) in (let TMP_9 \def (tweight t) in (let TMP_10 \def (plus TMP_8 
-TMP_9) in (let TMP_11 \def (tweight u) in (let TMP_12 \def (tweight t) in 
-(let TMP_13 \def (le_plus_r TMP_11 TMP_12) in (let TMP_14 \def (le_n_S TMP_7 
-TMP_10 TMP_13) in (lt_reg_l TMP_1 TMP_5 TMP_6 TMP_14)))))))))))))))))).
+ \lambda (_: K).(\lambda (c: C).(\lambda (u: T).(\lambda (t: T).(lt_reg_l 
+(tweight t) (S (plus (tweight u) (tweight t))) (cweight c) (le_n_S (tweight 
+t) (plus (tweight u) (tweight t)) (le_plus_r (tweight u) (tweight t))))))).
 
 theorem flt_shift:
  \forall (k: K).(\forall (c: C).(\forall (u: T).(\forall (t: T).(flt (CHead c 
 k u) t c (THead k u t)))))
 \def
- \lambda (_: K).(\lambda (c: C).(\lambda (u: T).(\lambda (t: T).(let TMP_1 
-\def (cweight c) in (let TMP_2 \def (tweight u) in (let TMP_3 \def (tweight 
-t) in (let TMP_4 \def (plus TMP_2 TMP_3) in (let TMP_5 \def (plus TMP_1 
-TMP_4) in (let TMP_6 \def (S TMP_5) in (let TMP_12 \def (\lambda (n: 
-nat).(let TMP_7 \def (cweight c) in (let TMP_8 \def (tweight u) in (let TMP_9 
-\def (plus TMP_7 TMP_8) in (let TMP_10 \def (tweight t) in (let TMP_11 \def 
-(plus TMP_9 TMP_10) in (lt TMP_11 n))))))) in (let TMP_13 \def (cweight c) in 
-(let TMP_14 \def (tweight u) in (let TMP_15 \def (plus TMP_13 TMP_14) in (let 
-TMP_16 \def (tweight t) in (let TMP_17 \def (plus TMP_15 TMP_16) in (let 
-TMP_24 \def (\lambda (n: nat).(let TMP_18 \def (cweight c) in (let TMP_19 
-\def (tweight u) in (let TMP_20 \def (plus TMP_18 TMP_19) in (let TMP_21 \def 
-(tweight t) in (let TMP_22 \def (plus TMP_20 TMP_21) in (let TMP_23 \def (S 
-n) in (lt TMP_22 TMP_23)))))))) in (let TMP_25 \def (cweight c) in (let 
-TMP_26 \def (tweight u) in (let TMP_27 \def (plus TMP_25 TMP_26) in (let 
-TMP_28 \def (tweight t) in (let TMP_29 \def (plus TMP_27 TMP_28) in (let 
-TMP_30 \def (S TMP_29) in (let TMP_31 \def (le_n TMP_30) in (let TMP_32 \def 
-(cweight c) in (let TMP_33 \def (tweight u) in (let TMP_34 \def (tweight t) 
-in (let TMP_35 \def (plus TMP_33 TMP_34) in (let TMP_36 \def (plus TMP_32 
-TMP_35) in (let TMP_37 \def (cweight c) in (let TMP_38 \def (tweight u) in 
-(let TMP_39 \def (tweight t) in (let TMP_40 \def (plus_assoc_l TMP_37 TMP_38 
-TMP_39) in (let TMP_41 \def (eq_ind_r nat TMP_17 TMP_24 TMP_31 TMP_36 TMP_40) 
-in (let TMP_42 \def (cweight c) in (let TMP_43 \def (tweight u) in (let 
-TMP_44 \def (tweight t) in (let TMP_45 \def (plus TMP_43 TMP_44) in (let 
-TMP_46 \def (S TMP_45) in (let TMP_47 \def (plus TMP_42 TMP_46) in (let 
-TMP_48 \def (cweight c) in (let TMP_49 \def (tweight u) in (let TMP_50 \def 
-(tweight t) in (let TMP_51 \def (plus TMP_49 TMP_50) in (let TMP_52 \def 
-(plus_n_Sm TMP_48 TMP_51) in (eq_ind nat TMP_6 TMP_12 TMP_41 TMP_47 
-TMP_52))))))))))))))))))))))))))))))))))))))))))))).
+ \lambda (_: K).(\lambda (c: C).(\lambda (u: T).(\lambda (t: T).(eq_ind nat 
+(S (plus (cweight c) (plus (tweight u) (tweight t)))) (\lambda (n: nat).(lt 
+(plus (plus (cweight c) (tweight u)) (tweight t)) n)) (eq_ind_r nat (plus 
+(plus (cweight c) (tweight u)) (tweight t)) (\lambda (n: nat).(lt (plus (plus 
+(cweight c) (tweight u)) (tweight t)) (S n))) (le_n (S (plus (plus (cweight 
+c) (tweight u)) (tweight t)))) (plus (cweight c) (plus (tweight u) (tweight 
+t))) (plus_assoc_l (cweight c) (tweight u) (tweight t))) (plus (cweight c) (S 
+(plus (tweight u) (tweight t)))) (plus_n_Sm (cweight c) (plus (tweight u) 
+(tweight t))))))).
 
 theorem flt_arith0:
  \forall (k: K).(\forall (c: C).(\forall (t: T).(\forall (i: nat).(flt c t 
 (CHead c k t) (TLRef i)))))
 \def
- \lambda (_: K).(\lambda (c: C).(\lambda (t: T).(\lambda (_: nat).(let TMP_1 
-\def (cweight c) in (let TMP_2 \def (tweight t) in (let TMP_3 \def (plus 
-TMP_1 TMP_2) in (lt_x_plus_x_Sy TMP_3 O))))))).
+ \lambda (_: K).(\lambda (c: C).(\lambda (t: T).(\lambda (_: 
+nat).(lt_x_plus_x_Sy (plus (cweight c) (tweight t)) O)))).
 
 theorem flt_arith1:
  \forall (k1: K).(\forall (c1: C).(\forall (c2: C).(\forall (t1: T).((cle 
@@ -92,25 +62,13 @@ nat).(flt c1 t1 (CHead c2 k2 t2) (TLRef i)))))))))
 \def
  \lambda (_: K).(\lambda (c1: C).(\lambda (c2: C).(\lambda (t1: T).(\lambda 
 (H: (le (plus (cweight c1) (tweight t1)) (cweight c2))).(\lambda (_: 
-K).(\lambda (t2: T).(\lambda (_: nat).(let TMP_1 \def (cweight c1) in (let 
-TMP_2 \def (tweight t1) in (let TMP_3 \def (plus TMP_1 TMP_2) in (let TMP_4 
-\def (cweight c2) in (let TMP_5 \def (cweight c2) in (let TMP_6 \def (tweight 
-t2) in (let TMP_7 \def (plus TMP_5 TMP_6) in (let TMP_8 \def (S O) in (let 
-TMP_9 \def (plus TMP_7 TMP_8) in (let TMP_10 \def (S O) in (let TMP_11 \def 
-(cweight c2) in (let TMP_12 \def (tweight t2) in (let TMP_13 \def (plus 
-TMP_11 TMP_12) in (let TMP_14 \def (plus TMP_10 TMP_13) in (let TMP_16 \def 
-(\lambda (n: nat).(let TMP_15 \def (cweight c2) in (lt TMP_15 n))) in (let 
-TMP_17 \def (cweight c2) in (let TMP_18 \def (cweight c2) in (let TMP_19 \def 
-(tweight t2) in (let TMP_20 \def (plus TMP_18 TMP_19) in (let TMP_21 \def 
-(cweight c2) in (let TMP_22 \def (tweight t2) in (let TMP_23 \def (le_plus_l 
-TMP_21 TMP_22) in (let TMP_24 \def (le_lt_n_Sm TMP_17 TMP_20 TMP_23) in (let 
-TMP_25 \def (cweight c2) in (let TMP_26 \def (tweight t2) in (let TMP_27 \def 
-(plus TMP_25 TMP_26) in (let TMP_28 \def (S O) in (let TMP_29 \def (plus 
-TMP_27 TMP_28) in (let TMP_30 \def (cweight c2) in (let TMP_31 \def (tweight 
-t2) in (let TMP_32 \def (plus TMP_30 TMP_31) in (let TMP_33 \def (S O) in 
-(let TMP_34 \def (plus_sym TMP_32 TMP_33) in (let TMP_35 \def (eq_ind_r nat 
-TMP_14 TMP_16 TMP_24 TMP_29 TMP_34) in (le_lt_trans TMP_3 TMP_4 TMP_9 H 
-TMP_35)))))))))))))))))))))))))))))))))))))))))).
+K).(\lambda (t2: T).(\lambda (_: nat).(le_lt_trans (plus (cweight c1) 
+(tweight t1)) (cweight c2) (plus (plus (cweight c2) (tweight t2)) (S O)) H 
+(eq_ind_r nat (plus (S O) (plus (cweight c2) (tweight t2))) (\lambda (n: 
+nat).(lt (cweight c2) n)) (le_lt_n_Sm (cweight c2) (plus (cweight c2) 
+(tweight t2)) (le_plus_l (cweight c2) (tweight t2))) (plus (plus (cweight c2) 
+(tweight t2)) (S O)) (plus_sym (plus (cweight c2) (tweight t2)) (S 
+O))))))))))).
 
 theorem flt_arith2:
  \forall (c1: C).(\forall (c2: C).(\forall (t1: T).(\forall (i: nat).((flt c1 
@@ -119,19 +77,10 @@ c1 t1 (CHead c2 k2 t2) (TLRef j)))))))))
 \def
  \lambda (c1: C).(\lambda (c2: C).(\lambda (t1: T).(\lambda (_: nat).(\lambda 
 (H: (lt (plus (cweight c1) (tweight t1)) (plus (cweight c2) (S O)))).(\lambda 
-(_: K).(\lambda (t2: T).(\lambda (_: nat).(let TMP_1 \def (cweight c1) in 
-(let TMP_2 \def (tweight t1) in (let TMP_3 \def (plus TMP_1 TMP_2) in (let 
-TMP_4 \def (cweight c2) in (let TMP_5 \def (S O) in (let TMP_6 \def (plus 
-TMP_4 TMP_5) in (let TMP_7 \def (cweight c2) in (let TMP_8 \def (tweight t2) 
-in (let TMP_9 \def (plus TMP_7 TMP_8) in (let TMP_10 \def (S O) in (let 
-TMP_11 \def (plus TMP_9 TMP_10) in (let TMP_12 \def (cweight c2) in (let 
-TMP_13 \def (cweight c2) in (let TMP_14 \def (tweight t2) in (let TMP_15 \def 
-(plus TMP_13 TMP_14) in (let TMP_16 \def (S O) in (let TMP_17 \def (S O) in 
-(let TMP_18 \def (cweight c2) in (let TMP_19 \def (tweight t2) in (let TMP_20 
-\def (le_plus_l TMP_18 TMP_19) in (let TMP_21 \def (S O) in (let TMP_22 \def 
-(le_n TMP_21) in (let TMP_23 \def (le_plus_plus TMP_12 TMP_15 TMP_16 TMP_17 
-TMP_20 TMP_22) in (lt_le_trans TMP_3 TMP_6 TMP_11 H 
-TMP_23))))))))))))))))))))))))))))))).
+(_: K).(\lambda (t2: T).(\lambda (_: nat).(lt_le_trans (plus (cweight c1) 
+(tweight t1)) (plus (cweight c2) (S O)) (plus (plus (cweight c2) (tweight 
+t2)) (S O)) H (le_plus_plus (cweight c2) (plus (cweight c2) (tweight t2)) (S 
+O) (S O) (le_plus_l (cweight c2) (tweight t2)) (le_n (S O))))))))))).
 
 theorem cle_flt_trans:
  \forall (c1: C).(\forall (c2: C).((cle c1 c2) \to (\forall (c3: C).(\forall 
@@ -139,16 +88,10 @@ theorem cle_flt_trans:
 \def
  \lambda (c1: C).(\lambda (c2: C).(\lambda (H: (le (cweight c1) (cweight 
 c2))).(\lambda (c3: C).(\lambda (u2: T).(\lambda (u3: T).(\lambda (H0: (lt 
-(plus (cweight c2) (tweight u2)) (plus (cweight c3) (tweight u3)))).(let 
-TMP_1 \def (cweight c1) in (let TMP_2 \def (tweight u2) in (let TMP_3 \def 
-(plus TMP_1 TMP_2) in (let TMP_4 \def (cweight c2) in (let TMP_5 \def 
-(tweight u2) in (let TMP_6 \def (plus TMP_4 TMP_5) in (let TMP_7 \def 
-(cweight c3) in (let TMP_8 \def (tweight u3) in (let TMP_9 \def (plus TMP_7 
-TMP_8) in (let TMP_10 \def (cweight c1) in (let TMP_11 \def (cweight c2) in 
-(let TMP_12 \def (tweight u2) in (let TMP_13 \def (tweight u2) in (let TMP_14 
-\def (tweight u2) in (let TMP_15 \def (le_n TMP_14) in (let TMP_16 \def 
-(le_plus_plus TMP_10 TMP_11 TMP_12 TMP_13 H TMP_15) in (le_lt_trans TMP_3 
-TMP_6 TMP_9 TMP_16 H0))))))))))))))))))))))).
+(plus (cweight c2) (tweight u2)) (plus (cweight c3) (tweight 
+u3)))).(le_lt_trans (plus (cweight c1) (tweight u2)) (plus (cweight c2) 
+(tweight u2)) (plus (cweight c3) (tweight u3)) (le_plus_plus (cweight c1) 
+(cweight c2) (tweight u2) (tweight u2) H (le_n (tweight u2))) H0))))))).
 
 theorem flt_trans:
  \forall (c1: C).(\forall (c2: C).(\forall (t1: T).(\forall (t2: T).((flt c1 
@@ -157,7 +100,6 @@ c1 t1 c3 t3))))))))
 \def
  \lambda (c1: C).(\lambda (c2: C).(\lambda (t1: T).(\lambda (t2: T).(\lambda 
 (H: (lt (fweight c1 t1) (fweight c2 t2))).(\lambda (c3: C).(\lambda (t3: 
-T).(\lambda (H0: (lt (fweight c2 t2) (fweight c3 t3))).(let TMP_1 \def 
-(fweight c1 t1) in (let TMP_2 \def (fweight c2 t2) in (let TMP_3 \def 
-(fweight c3 t3) in (lt_trans TMP_1 TMP_2 TMP_3 H H0))))))))))).
+T).(\lambda (H0: (lt (fweight c2 t2) (fweight c3 t3))).(lt_trans (fweight c1 
+t1) (fweight c2 t2) (fweight c3 t3) H H0)))))))).