X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=matita%2Fmatita%2Fcontribs%2Flambdadelta%2Fbasic_1%2Fnext_plus%2Fprops.ma;h=2f42fc60e194d4ba9ce08945248e1ca78dd21f2a;hb=57ae1762497a5f3ea75740e2908e04adb8642cc2;hp=29d7c60d702e8f45b1ab553bebbfb51a15e95cff;hpb=6abec8ca6434937e46e098ed946bc6ed307f022b;p=helm.git

diff --git a/matita/matita/contribs/lambdadelta/basic_1/next_plus/props.ma b/matita/matita/contribs/lambdadelta/basic_1/next_plus/props.ma
index 29d7c60d7..2f42fc60e 100644
--- a/matita/matita/contribs/lambdadelta/basic_1/next_plus/props.ma
+++ b/matita/matita/contribs/lambdadelta/basic_1/next_plus/props.ma
@@ -16,74 +16,44 @@
 
 include "basic_1/next_plus/defs.ma".
 
-theorem next_plus_assoc:
+lemma next_plus_assoc:
  \forall (g: G).(\forall (n: nat).(\forall (h1: nat).(\forall (h2: nat).(eq 
 nat (next_plus g (next_plus g n h1) h2) (next_plus g n (plus h1 h2))))))
 \def
- \lambda (g: G).(\lambda (n: nat).(\lambda (h1: nat).(let TMP_5 \def (\lambda 
-(n0: nat).(\forall (h2: nat).(let TMP_1 \def (next_plus g n n0) in (let TMP_2 
-\def (next_plus g TMP_1 h2) in (let TMP_3 \def (plus n0 h2) in (let TMP_4 
-\def (next_plus g n TMP_3) in (eq nat TMP_2 TMP_4))))))) in (let TMP_7 \def 
-(\lambda (h2: nat).(let TMP_6 \def (next_plus g n h2) in (refl_equal nat 
-TMP_6))) in (let TMP_47 \def (\lambda (n0: nat).(\lambda (_: ((\forall (h2: 
-nat).(eq nat (next_plus g (next_plus g n n0) h2) (next_plus g n (plus n0 
-h2)))))).(\lambda (h2: nat).(let TMP_14 \def (\lambda (n1: nat).(let TMP_8 
-\def (next_plus g n n0) in (let TMP_9 \def (next g TMP_8) in (let TMP_10 \def 
-(next_plus g TMP_9 n1) in (let TMP_11 \def (plus n0 n1) in (let TMP_12 \def 
-(next_plus g n TMP_11) in (let TMP_13 \def (next g TMP_12) in (eq nat TMP_10 
-TMP_13)))))))) in (let TMP_19 \def (\lambda (n1: nat).(let TMP_15 \def 
-(next_plus g n n0) in (let TMP_16 \def (next g TMP_15) in (let TMP_17 \def 
-(next_plus g n n1) in (let TMP_18 \def (next g TMP_17) in (eq nat TMP_16 
-TMP_18)))))) in (let TMP_20 \def (next_plus g n n0) in (let TMP_21 \def (next 
-g TMP_20) in (let TMP_22 \def (refl_equal nat TMP_21) in (let TMP_23 \def 
-(plus n0 O) in (let TMP_24 \def (plus_n_O n0) in (let TMP_25 \def (eq_ind nat 
-n0 TMP_19 TMP_22 TMP_23 TMP_24) in (let TMP_46 \def (\lambda (n1: 
-nat).(\lambda (H0: (eq nat (next_plus g (next g (next_plus g n n0)) n1) (next 
-g (next_plus g n (plus n0 n1))))).(let TMP_26 \def (plus n0 n1) in (let 
-TMP_27 \def (S TMP_26) in (let TMP_34 \def (\lambda (n2: nat).(let TMP_28 
-\def (next_plus g n n0) in (let TMP_29 \def (next g TMP_28) in (let TMP_30 
-\def (next_plus g TMP_29 n1) in (let TMP_31 \def (next g TMP_30) in (let 
-TMP_32 \def (next_plus g n n2) in (let TMP_33 \def (next g TMP_32) in (eq nat 
-TMP_31 TMP_33)))))))) in (let TMP_35 \def (next g) in (let TMP_36 \def 
-(next_plus g n n0) in (let TMP_37 \def (next g TMP_36) in (let TMP_38 \def 
-(next_plus g TMP_37 n1) in (let TMP_39 \def (plus n0 n1) in (let TMP_40 \def 
-(next_plus g n TMP_39) in (let TMP_41 \def (next g TMP_40) in (let TMP_42 
-\def (f_equal nat nat TMP_35 TMP_38 TMP_41 H0) in (let TMP_43 \def (S n1) in 
-(let TMP_44 \def (plus n0 TMP_43) in (let TMP_45 \def (plus_n_Sm n0 n1) in 
-(eq_ind nat TMP_27 TMP_34 TMP_42 TMP_44 TMP_45))))))))))))))))) in (nat_ind 
-TMP_14 TMP_25 TMP_46 h2))))))))))))) in (nat_ind TMP_5 TMP_7 TMP_47 h1)))))).
+ \lambda (g: G).(\lambda (n: nat).(\lambda (h1: nat).(nat_ind (\lambda (n0: 
+nat).(\forall (h2: nat).(eq nat (next_plus g (next_plus g n n0) h2) 
+(next_plus g n (plus n0 h2))))) (\lambda (h2: nat).(refl_equal nat (next_plus 
+g n h2))) (\lambda (n0: nat).(\lambda (_: ((\forall (h2: nat).(eq nat 
+(next_plus g (next_plus g n n0) h2) (next_plus g n (plus n0 h2)))))).(\lambda 
+(h2: nat).(nat_ind (\lambda (n1: nat).(eq nat (next_plus g (next g (next_plus 
+g n n0)) n1) (next g (next_plus g n (plus n0 n1))))) (eq_ind nat n0 (\lambda 
+(n1: nat).(eq nat (next g (next_plus g n n0)) (next g (next_plus g n n1)))) 
+(refl_equal nat (next g (next_plus g n n0))) (plus n0 O) (plus_n_O n0)) 
+(\lambda (n1: nat).(\lambda (H0: (eq nat (next_plus g (next g (next_plus g n 
+n0)) n1) (next g (next_plus g n (plus n0 n1))))).(eq_ind nat (S (plus n0 n1)) 
+(\lambda (n2: nat).(eq nat (next g (next_plus g (next g (next_plus g n n0)) 
+n1)) (next g (next_plus g n n2)))) (f_equal nat nat (next g) (next_plus g 
+(next g (next_plus g n n0)) n1) (next g (next_plus g n (plus n0 n1))) H0) 
+(plus n0 (S n1)) (plus_n_Sm n0 n1)))) h2)))) h1))).
 
-theorem next_plus_next:
+lemma next_plus_next:
  \forall (g: G).(\forall (n: nat).(\forall (h: nat).(eq nat (next_plus g 
 (next g n) h) (next g (next_plus g n h)))))
 \def
- \lambda (g: G).(\lambda (n: nat).(\lambda (h: nat).(let TMP_1 \def (S O) in 
-(let TMP_2 \def (plus TMP_1 h) in (let TMP_3 \def (next_plus g n TMP_2) in 
-(let TMP_6 \def (\lambda (n0: nat).(let TMP_4 \def (next_plus g n h) in (let 
-TMP_5 \def (next g TMP_4) in (eq nat n0 TMP_5)))) in (let TMP_7 \def 
-(next_plus g n h) in (let TMP_8 \def (next g TMP_7) in (let TMP_9 \def 
-(refl_equal nat TMP_8) in (let TMP_10 \def (S O) in (let TMP_11 \def 
-(next_plus g n TMP_10) in (let TMP_12 \def (next_plus g TMP_11 h) in (let 
-TMP_13 \def (S O) in (let TMP_14 \def (next_plus_assoc g n TMP_13 h) in 
-(eq_ind_r nat TMP_3 TMP_6 TMP_9 TMP_12 TMP_14))))))))))))))).
+ \lambda (g: G).(\lambda (n: nat).(\lambda (h: nat).(eq_ind_r nat (next_plus 
+g n (plus (S O) h)) (\lambda (n0: nat).(eq nat n0 (next g (next_plus g n 
+h)))) (refl_equal nat (next g (next_plus g n h))) (next_plus g (next_plus g n 
+(S O)) h) (next_plus_assoc g n (S O) h)))).
 
-theorem next_plus_lt:
+lemma next_plus_lt:
  \forall (g: G).(\forall (h: nat).(\forall (n: nat).(lt n (next_plus g (next 
 g n) h))))
 \def
- \lambda (g: G).(\lambda (h: nat).(let TMP_3 \def (\lambda (n: nat).(\forall 
-(n0: nat).(let TMP_1 \def (next g n0) in (let TMP_2 \def (next_plus g TMP_1 
-n) in (lt n0 TMP_2))))) in (let TMP_4 \def (\lambda (n: nat).(next_lt g n)) 
-in (let TMP_22 \def (\lambda (n: nat).(\lambda (H: ((\forall (n0: nat).(lt n0 
-(next_plus g (next g n0) n))))).(\lambda (n0: nat).(let TMP_5 \def (next g 
-n0) in (let TMP_6 \def (next g TMP_5) in (let TMP_7 \def (next_plus g TMP_6 
-n) in (let TMP_8 \def (\lambda (n1: nat).(lt n0 n1)) in (let TMP_9 \def (next 
-g n0) in (let TMP_10 \def (next g n0) in (let TMP_11 \def (next g TMP_10) in 
-(let TMP_12 \def (next_plus g TMP_11 n) in (let TMP_13 \def (next_lt g n0) in 
-(let TMP_14 \def (next g n0) in (let TMP_15 \def (H TMP_14) in (let TMP_16 
-\def (lt_trans n0 TMP_9 TMP_12 TMP_13 TMP_15) in (let TMP_17 \def (next g n0) 
-in (let TMP_18 \def (next_plus g TMP_17 n) in (let TMP_19 \def (next g 
-TMP_18) in (let TMP_20 \def (next g n0) in (let TMP_21 \def (next_plus_next g 
-TMP_20 n) in (eq_ind nat TMP_7 TMP_8 TMP_16 TMP_19 
-TMP_21))))))))))))))))))))) in (nat_ind TMP_3 TMP_4 TMP_22 h))))).
+ \lambda (g: G).(\lambda (h: nat).(nat_ind (\lambda (n: nat).(\forall (n0: 
+nat).(lt n0 (next_plus g (next g n0) n)))) (\lambda (n: nat).(next_lt g n)) 
+(\lambda (n: nat).(\lambda (H: ((\forall (n0: nat).(lt n0 (next_plus g (next 
+g n0) n))))).(\lambda (n0: nat).(eq_ind nat (next_plus g (next g (next g n0)) 
+n) (\lambda (n1: nat).(lt n0 n1)) (lt_trans n0 (next g n0) (next_plus g (next 
+g (next g n0)) n) (next_lt g n0) (H (next g n0))) (next g (next_plus g (next 
+g n0) n)) (next_plus_next g (next g n0) n))))) h)).