X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=matita%2Fmatita%2Fcontribs%2Flambdadelta%2Fbasic_1%2Fex0%2Fprops.ma;h=c115f9d6b0ab040e511245b51affd7016a3333a2;hb=a4ba77d9df157e443e6fb39dc7376996faea9973;hp=96dd77da32096e890b34708d6eafeed56ea78c3b;hpb=88a68a9c334646bc17314d5327cd3b790202acd6;p=helm.git

diff --git a/matita/matita/contribs/lambdadelta/basic_1/ex0/props.ma b/matita/matita/contribs/lambdadelta/basic_1/ex0/props.ma
index 96dd77da3..c115f9d6b 100644
--- a/matita/matita/contribs/lambdadelta/basic_1/ex0/props.ma
+++ b/matita/matita/contribs/lambdadelta/basic_1/ex0/props.ma
@@ -14,13 +14,13 @@
 
 (* This file was automatically generated: do not edit *********************)
 
-include "Basic-1/ex0/defs.ma".
+include "basic_1/ex0/fwd.ma".
 
-include "Basic-1/leq/defs.ma".
+include "basic_1/leq/fwd.ma".
 
-include "Basic-1/aplus/props.ma".
+include "basic_1/aplus/props.ma".
 
-theorem aplus_gz_le:
+lemma aplus_gz_le:
  \forall (k: nat).(\forall (h: nat).(\forall (n: nat).((le h k) \to (eq A 
 (aplus gz (ASort h n) k) (ASort O (plus (minus k h) n))))))
 \def
@@ -52,11 +52,8 @@ k0)) a)) (eq_ind A (aplus gz (asucc gz (ASort (S n) n0)) k0) (\lambda (a:
 A).(eq A a (aplus gz (ASort n n0) k0))) (refl_equal A (aplus gz (ASort n n0) 
 k0)) (asucc gz (aplus gz (ASort (S n) n0) k0)) (aplus_asucc gz k0 (ASort (S 
 n) n0))) (ASort O (plus (minus k0 n) n0)) (IH n n0 H_y))))))) h)))) k).
-(* COMMENTS
-Initial nodes: 683
-END *)
 
-theorem aplus_gz_ge:
+lemma aplus_gz_ge:
  \forall (n: nat).(\forall (k: nat).(\forall (h: nat).((le k h) \to (eq A 
 (aplus gz (ASort h n) k) (ASort (minus h k) n)))))
 \def
@@ -71,33 +68,27 @@ h) \to (eq A (aplus gz (ASort h n) k0) (ASort (minus h k0) n)))))).(\lambda
 (S k0) O)).(ex2_ind nat (\lambda (n0: nat).(eq nat O (S n0))) (\lambda (n0: 
 nat).(le k0 n0)) (eq A (asucc gz (aplus gz (ASort O n) k0)) (ASort O n)) 
 (\lambda (x: nat).(\lambda (H0: (eq nat O (S x))).(\lambda (_: (le k0 
-x)).(let H2 \def (eq_ind nat O (\lambda (ee: nat).(match ee in nat return 
-(\lambda (_: nat).Prop) with [O \Rightarrow True | (S _) \Rightarrow False])) 
-I (S x) H0) in (False_ind (eq A (asucc gz (aplus gz (ASort O n) k0)) (ASort O 
-n)) H2))))) (le_gen_S k0 O H))) (\lambda (n0: nat).(\lambda (_: (((le (S k0) 
-n0) \to (eq A (asucc gz (aplus gz (ASort n0 n) k0)) (ASort (minus n0 (S k0)) 
-n))))).(\lambda (H0: (le (S k0) (S n0))).(let H_y \def (le_S_n k0 n0 H0) in 
-(eq_ind A (aplus gz (ASort n0 n) k0) (\lambda (a: A).(eq A (asucc gz (aplus 
-gz (ASort (S n0) n) k0)) a)) (eq_ind A (aplus gz (asucc gz (ASort (S n0) n)) 
-k0) (\lambda (a: A).(eq A a (aplus gz (ASort n0 n) k0))) (refl_equal A (aplus 
-gz (ASort n0 n) k0)) (asucc gz (aplus gz (ASort (S n0) n) k0)) (aplus_asucc 
-gz k0 (ASort (S n0) n))) (ASort (minus n0 k0) n) (IH n0 H_y)))))) h)))) k)).
-(* COMMENTS
-Initial nodes: 524
-END *)
+x)).(let H2 \def (eq_ind nat O (\lambda (ee: nat).(match ee with [O 
+\Rightarrow True | (S _) \Rightarrow False])) I (S x) H0) in (False_ind (eq A 
+(asucc gz (aplus gz (ASort O n) k0)) (ASort O n)) H2))))) (le_gen_S k0 O H))) 
+(\lambda (n0: nat).(\lambda (_: (((le (S k0) n0) \to (eq A (asucc gz (aplus 
+gz (ASort n0 n) k0)) (ASort (minus n0 (S k0)) n))))).(\lambda (H0: (le (S k0) 
+(S n0))).(let H_y \def (le_S_n k0 n0 H0) in (eq_ind A (aplus gz (ASort n0 n) 
+k0) (\lambda (a: A).(eq A (asucc gz (aplus gz (ASort (S n0) n) k0)) a)) 
+(eq_ind A (aplus gz (asucc gz (ASort (S n0) n)) k0) (\lambda (a: A).(eq A a 
+(aplus gz (ASort n0 n) k0))) (refl_equal A (aplus gz (ASort n0 n) k0)) (asucc 
+gz (aplus gz (ASort (S n0) n) k0)) (aplus_asucc gz k0 (ASort (S n0) n))) 
+(ASort (minus n0 k0) n) (IH n0 H_y)))))) h)))) k)).
 
-theorem next_plus_gz:
+lemma next_plus_gz:
  \forall (n: nat).(\forall (h: nat).(eq nat (next_plus gz n h) (plus h n)))
 \def
  \lambda (n: nat).(\lambda (h: nat).(nat_ind (\lambda (n0: nat).(eq nat 
 (next_plus gz n n0) (plus n0 n))) (refl_equal nat n) (\lambda (n0: 
 nat).(\lambda (H: (eq nat (next_plus gz n n0) (plus n0 n))).(f_equal nat nat 
 S (next_plus gz n n0) (plus n0 n) H))) h)).
-(* COMMENTS
-Initial nodes: 77
-END *)
 
-theorem leqz_leq:
+lemma leqz_leq:
  \forall (a1: A).(\forall (a2: A).((leq gz a1 a2) \to (leqz a1 a2)))
 \def
  \lambda (a1: A).(\lambda (a2: A).(\lambda (H: (leq gz a1 a2)).(leq_ind gz 
@@ -108,68 +99,61 @@ h1 (leqz (ASort h1 n1) (ASort h2 n2)) (\lambda (H1: (lt k h1)).(lt_le_e k h2
 (leqz (ASort h1 n1) (ASort h2 n2)) (\lambda (H2: (lt k h2)).(let H3 \def 
 (eq_ind A (aplus gz (ASort h1 n1) k) (\lambda (a: A).(eq A a (aplus gz (ASort 
 h2 n2) k))) H0 (ASort (minus h1 k) n1) (aplus_gz_ge n1 k h1 (le_S_n k h1 
-(le_S (S k) h1 H1)))) in (let H4 \def (eq_ind A (aplus gz (ASort h2 n2) k) 
-(\lambda (a: A).(eq A (ASort (minus h1 k) n1) a)) H3 (ASort (minus h2 k) n2) 
-(aplus_gz_ge n2 k h2 (le_S_n k h2 (le_S (S k) h2 H2)))) in (let H5 \def 
-(f_equal A nat (\lambda (e: A).(match e in A return (\lambda (_: A).nat) with 
-[(ASort n _) \Rightarrow n | (AHead _ _) \Rightarrow ((let rec minus (n: nat) 
-on n: (nat \to nat) \def (\lambda (m: nat).(match n with [O \Rightarrow O | 
-(S k0) \Rightarrow (match m with [O \Rightarrow (S k0) | (S l) \Rightarrow 
-(minus k0 l)])])) in minus) h1 k)])) (ASort (minus h1 k) n1) (ASort (minus h2 
-k) n2) H4) in ((let H6 \def (f_equal A nat (\lambda (e: A).(match e in A 
-return (\lambda (_: A).nat) with [(ASort _ n) \Rightarrow n | (AHead _ _) 
-\Rightarrow n1])) (ASort (minus h1 k) n1) (ASort (minus h2 k) n2) H4) in 
-(\lambda (H7: (eq nat (minus h1 k) (minus h2 k))).(eq_ind nat n1 (\lambda (n: 
-nat).(leqz (ASort h1 n1) (ASort h2 n))) (eq_ind nat h1 (\lambda (n: 
-nat).(leqz (ASort h1 n1) (ASort n n1))) (leqz_sort h1 h1 n1 n1 (refl_equal 
-nat (plus h1 n1))) h2 (minus_minus k h1 h2 (le_S_n k h1 (le_S (S k) h1 H1)) 
-(le_S_n k h2 (le_S (S k) h2 H2)) H7)) n2 H6))) H5))))) (\lambda (H2: (le h2 
+(le_S_n (S k) (S h1) (le_S (S (S k)) (S h1) (le_n_S (S k) h1 H1)))))) in (let 
+H4 \def (eq_ind A (aplus gz (ASort h2 n2) k) (\lambda (a: A).(eq A (ASort 
+(minus h1 k) n1) a)) H3 (ASort (minus h2 k) n2) (aplus_gz_ge n2 k h2 (le_S_n 
+k h2 (le_S_n (S k) (S h2) (le_S (S (S k)) (S h2) (le_n_S (S k) h2 H2)))))) in 
+(let H5 \def (f_equal A nat (\lambda (e: A).(match e with [(ASort n _) 
+\Rightarrow n | (AHead _ _) \Rightarrow (minus h1 k)])) (ASort (minus h1 k) 
+n1) (ASort (minus h2 k) n2) H4) in ((let H6 \def (f_equal A nat (\lambda (e: 
+A).(match e with [(ASort _ n) \Rightarrow n | (AHead _ _) \Rightarrow n1])) 
+(ASort (minus h1 k) n1) (ASort (minus h2 k) n2) H4) in (\lambda (H7: (eq nat 
+(minus h1 k) (minus h2 k))).(eq_ind nat n1 (\lambda (n: nat).(leqz (ASort h1 
+n1) (ASort h2 n))) (eq_ind nat h1 (\lambda (n: nat).(leqz (ASort h1 n1) 
+(ASort n n1))) (leqz_sort h1 h1 n1 n1 (refl_equal nat (plus h1 n1))) h2 
+(minus_minus k h1 h2 (le_S_n k h1 (le_S_n (S k) (S h1) (le_S (S (S k)) (S h1) 
+(le_n_S (S k) h1 H1)))) (le_S_n k h2 (le_S_n (S k) (S h2) (le_S (S (S k)) (S 
+h2) (le_n_S (S k) h2 H2)))) H7)) n2 H6))) H5))))) (\lambda (H2: (le h2 
 k)).(let H3 \def (eq_ind A (aplus gz (ASort h1 n1) k) (\lambda (a: A).(eq A a 
 (aplus gz (ASort h2 n2) k))) H0 (ASort (minus h1 k) n1) (aplus_gz_ge n1 k h1 
-(le_S_n k h1 (le_S (S k) h1 H1)))) in (let H4 \def (eq_ind A (aplus gz (ASort 
-h2 n2) k) (\lambda (a: A).(eq A (ASort (minus h1 k) n1) a)) H3 (ASort O (plus 
-(minus k h2) n2)) (aplus_gz_le k h2 n2 H2)) in (let H5 \def (eq_ind nat 
-(minus h1 k) (\lambda (n: nat).(eq A (ASort n n1) (ASort O (plus (minus k h2) 
-n2)))) H4 (S (minus h1 (S k))) (minus_x_Sy h1 k H1)) in (let H6 \def (eq_ind 
-A (ASort (S (minus h1 (S k))) n1) (\lambda (ee: A).(match ee in A return 
-(\lambda (_: A).Prop) with [(ASort n _) \Rightarrow (match n in nat return 
-(\lambda (_: nat).Prop) with [O \Rightarrow False | (S _) \Rightarrow True]) 
-| (AHead _ _) \Rightarrow False])) I (ASort O (plus (minus k h2) n2)) H5) in 
-(False_ind (leqz (ASort h1 n1) (ASort h2 n2)) H6)))))))) (\lambda (H1: (le h1 
+(le_S_n k h1 (le_S_n (S k) (S h1) (le_S (S (S k)) (S h1) (le_n_S (S k) h1 
+H1)))))) in (let H4 \def (eq_ind A (aplus gz (ASort h2 n2) k) (\lambda (a: 
+A).(eq A (ASort (minus h1 k) n1) a)) H3 (ASort O (plus (minus k h2) n2)) 
+(aplus_gz_le k h2 n2 H2)) in (let H5 \def (eq_ind nat (minus h1 k) (\lambda 
+(n: nat).(eq A (ASort n n1) (ASort O (plus (minus k h2) n2)))) H4 (S (minus 
+h1 (S k))) (minus_x_Sy h1 k H1)) in (let H6 \def (eq_ind A (ASort (S (minus 
+h1 (S k))) n1) (\lambda (ee: A).(match ee with [(ASort n _) \Rightarrow 
+(match n with [O \Rightarrow False | (S _) \Rightarrow True]) | (AHead _ _) 
+\Rightarrow False])) I (ASort O (plus (minus k h2) n2)) H5) in (False_ind 
+(leqz (ASort h1 n1) (ASort h2 n2)) H6)))))))) (\lambda (H1: (le h1 
 k)).(lt_le_e k h2 (leqz (ASort h1 n1) (ASort h2 n2)) (\lambda (H2: (lt k 
 h2)).(let H3 \def (eq_ind A (aplus gz (ASort h1 n1) k) (\lambda (a: A).(eq A 
 a (aplus gz (ASort h2 n2) k))) H0 (ASort O (plus (minus k h1) n1)) 
 (aplus_gz_le k h1 n1 H1)) in (let H4 \def (eq_ind A (aplus gz (ASort h2 n2) 
 k) (\lambda (a: A).(eq A (ASort O (plus (minus k h1) n1)) a)) H3 (ASort 
-(minus h2 k) n2) (aplus_gz_ge n2 k h2 (le_S_n k h2 (le_S (S k) h2 H2)))) in 
-(let H5 \def (sym_eq A (ASort O (plus (minus k h1) n1)) (ASort (minus h2 k) 
-n2) H4) in (let H6 \def (eq_ind nat (minus h2 k) (\lambda (n: nat).(eq A 
-(ASort n n2) (ASort O (plus (minus k h1) n1)))) H5 (S (minus h2 (S k))) 
-(minus_x_Sy h2 k H2)) in (let H7 \def (eq_ind A (ASort (S (minus h2 (S k))) 
-n2) (\lambda (ee: A).(match ee in A return (\lambda (_: A).Prop) with [(ASort 
-n _) \Rightarrow (match n in nat return (\lambda (_: nat).Prop) with [O 
-\Rightarrow False | (S _) \Rightarrow True]) | (AHead _ _) \Rightarrow 
-False])) I (ASort O (plus (minus k h1) n1)) H6) in (False_ind (leqz (ASort h1 
-n1) (ASort h2 n2)) H7))))))) (\lambda (H2: (le h2 k)).(let H3 \def (eq_ind A 
-(aplus gz (ASort h1 n1) k) (\lambda (a: A).(eq A a (aplus gz (ASort h2 n2) 
-k))) H0 (ASort O (plus (minus k h1) n1)) (aplus_gz_le k h1 n1 H1)) in (let H4 
-\def (eq_ind A (aplus gz (ASort h2 n2) k) (\lambda (a: A).(eq A (ASort O 
-(plus (minus k h1) n1)) a)) H3 (ASort O (plus (minus k h2) n2)) (aplus_gz_le 
-k h2 n2 H2)) in (let H5 \def (f_equal A nat (\lambda (e: A).(match e in A 
-return (\lambda (_: A).nat) with [(ASort _ n) \Rightarrow n | (AHead _ _) 
-\Rightarrow ((let rec plus (n: nat) on n: (nat \to nat) \def (\lambda (m: 
-nat).(match n with [O \Rightarrow m | (S p) \Rightarrow (S (plus p m))])) in 
-plus) (minus k h1) n1)])) (ASort O (plus (minus k h1) n1)) (ASort O (plus 
-(minus k h2) n2)) H4) in (let H_y \def (plus_plus k h1 h2 n1 n2 H1 H2 H5) in 
-(leqz_sort h1 h2 n1 n2 H_y))))))))))))))) (\lambda (a0: A).(\lambda (a3: 
-A).(\lambda (_: (leq gz a0 a3)).(\lambda (H1: (leqz a0 a3)).(\lambda (a4: 
-A).(\lambda (a5: A).(\lambda (_: (leq gz a4 a5)).(\lambda (H3: (leqz a4 
-a5)).(leqz_head a0 a3 H1 a4 a5 H3))))))))) a1 a2 H))).
-(* COMMENTS
-Initial nodes: 1375
-END *)
+(minus h2 k) n2) (aplus_gz_ge n2 k h2 (le_S_n k h2 (le_S_n (S k) (S h2) (le_S 
+(S (S k)) (S h2) (le_n_S (S k) h2 H2)))))) in (let H5 \def (sym_eq A (ASort O 
+(plus (minus k h1) n1)) (ASort (minus h2 k) n2) H4) in (let H6 \def (eq_ind 
+nat (minus h2 k) (\lambda (n: nat).(eq A (ASort n n2) (ASort O (plus (minus k 
+h1) n1)))) H5 (S (minus h2 (S k))) (minus_x_Sy h2 k H2)) in (let H7 \def 
+(eq_ind A (ASort (S (minus h2 (S k))) n2) (\lambda (ee: A).(match ee with 
+[(ASort n _) \Rightarrow (match n with [O \Rightarrow False | (S _) 
+\Rightarrow True]) | (AHead _ _) \Rightarrow False])) I (ASort O (plus (minus 
+k h1) n1)) H6) in (False_ind (leqz (ASort h1 n1) (ASort h2 n2)) H7))))))) 
+(\lambda (H2: (le h2 k)).(let H3 \def (eq_ind A (aplus gz (ASort h1 n1) k) 
+(\lambda (a: A).(eq A a (aplus gz (ASort h2 n2) k))) H0 (ASort O (plus (minus 
+k h1) n1)) (aplus_gz_le k h1 n1 H1)) in (let H4 \def (eq_ind A (aplus gz 
+(ASort h2 n2) k) (\lambda (a: A).(eq A (ASort O (plus (minus k h1) n1)) a)) 
+H3 (ASort O (plus (minus k h2) n2)) (aplus_gz_le k h2 n2 H2)) in (let H5 \def 
+(f_equal A nat (\lambda (e: A).(match e with [(ASort _ n) \Rightarrow n | 
+(AHead _ _) \Rightarrow (plus (minus k h1) n1)])) (ASort O (plus (minus k h1) 
+n1)) (ASort O (plus (minus k h2) n2)) H4) in (let H_y \def (plus_plus k h1 h2 
+n1 n2 H1 H2 H5) in (leqz_sort h1 h2 n1 n2 H_y))))))))))))))) (\lambda (a0: 
+A).(\lambda (a3: A).(\lambda (_: (leq gz a0 a3)).(\lambda (H1: (leqz a0 
+a3)).(\lambda (a4: A).(\lambda (a5: A).(\lambda (_: (leq gz a4 a5)).(\lambda 
+(H3: (leqz a4 a5)).(leqz_head a0 a3 H1 a4 a5 H3))))))))) a1 a2 H))).
 
-theorem leq_leqz:
+lemma leq_leqz:
  \forall (a1: A).(\forall (a2: A).((leqz a1 a2) \to (leq gz a1 a2)))
 \def
  \lambda (a1: A).(\lambda (a2: A).(\lambda (H: (leqz a1 a2)).(leqz_ind 
@@ -201,7 +185,4 @@ h2)) (aplus_asort_simpl gz (plus h1 h2) h1 n1)))))))) (\lambda (a0:
 A).(\lambda (a3: A).(\lambda (_: (leqz a0 a3)).(\lambda (H1: (leq gz a0 
 a3)).(\lambda (a4: A).(\lambda (a5: A).(\lambda (_: (leqz a4 a5)).(\lambda 
 (H3: (leq gz a4 a5)).(leq_head gz a0 a3 H1 a4 a5 H3))))))))) a1 a2 H))).
-(* COMMENTS
-Initial nodes: 717
-END *)