update in basic_2

[helm.git] / matita / matita / contribs / lambdadelta / basic_1 / pr2 / pr2.ma

diff --git a/matita/matita/contribs/lambdadelta/basic_1/pr2/pr2.ma b/matita/matita/contribs/lambdadelta/basic_1/pr2/pr2.ma
index f8df4e9e26c296e1fd104f7115fc12ddcbc1dd3a..3151fc53cc7dcb6c90e4e03a76c940d2c8335ef9 100644 (file)
--- a/matita/matita/contribs/lambdadelta/basic_1/pr2/pr2.ma
+++ b/matita/matita/contribs/lambdadelta/basic_1/pr2/pr2.ma
@@ -14,13 +14,13 @@
 
 (* This file was automatically generated: do not edit *********************)
 
-include "Basic-1/pr2/defs.ma".
+include "basic_1/pr2/defs.ma".
 
-include "Basic-1/pr0/pr0.ma".
+include "basic_1/pr0/pr0.ma".
 
-include "Basic-1/getl/props.ma".
+include "basic_1/getl/fwd.ma".
 
-theorem pr2_confluence__pr2_free_free:
+fact pr2_confluence__pr2_free_free:
  \forall (c: C).(\forall (t0: T).(\forall (t1: T).(\forall (t2: T).((pr0 t0 
 t1) \to ((pr0 t0 t2) \to (ex2 T (\lambda (t: T).(pr2 c t1 t)) (\lambda (t: 
 T).(pr2 c t2 t))))))))
@@ -32,11 +32,8 @@ t2 t)) (\lambda (t: T).(pr0 t1 t)) (ex2 T (\lambda (t: T).(pr2 c t1 t))
 x)).(\lambda (H2: (pr0 t1 x)).(ex_intro2 T (\lambda (t: T).(pr2 c t1 t)) 
 (\lambda (t: T).(pr2 c t2 t)) x (pr2_free c t1 x H2) (pr2_free c t2 x H1))))) 
 (pr0_confluence t0 t2 H0 t1 H))))))).
-(* COMMENTS
-Initial nodes: 135
-END *)
 
-theorem pr2_confluence__pr2_free_delta:
+fact pr2_confluence__pr2_free_delta:
  \forall (c: C).(\forall (d: C).(\forall (t0: T).(\forall (t1: T).(\forall 
 (t2: T).(\forall (t4: T).(\forall (u: T).(\forall (i: nat).((pr0 t0 t1) \to 
 ((getl i c (CHead d (Bind Abbr) u)) \to ((pr0 t0 t4) \to ((subst0 i u t4 t2) 
@@ -61,11 +58,8 @@ T).(pr2 c t2 t))) (\lambda (x0: T).(\lambda (H6: (pr0 t2 x0)).(\lambda (H7:
 T).(pr2 c t2 t)) x0 (pr2_delta c d u i H0 t1 x H4 x0 H7) (pr2_free c t2 x0 
 H6))))) H5)) (pr0_subst0 t4 x H3 u t2 i H2 u (pr0_refl u)))))) 
 (pr0_confluence t0 t4 H1 t1 H))))))))))))).
-(* COMMENTS
-Initial nodes: 403
-END *)
 
-theorem pr2_confluence__pr2_delta_delta:
+fact pr2_confluence__pr2_delta_delta:
  \forall (c: C).(\forall (d: C).(\forall (d0: C).(\forall (t0: T).(\forall 
 (t1: T).(\forall (t2: T).(\forall (t3: T).(\forall (t4: T).(\forall (u: 
 T).(\forall (u0: T).(\forall (i: nat).(\forall (i0: nat).((getl i c (CHead d 
@@ -122,41 +116,37 @@ u i H t2 x1 H11 x2 H14))))) (subst0_confluence_neq x x1 u0 i0 H12 x0 u i H9
 H2 i H13) in (let H16 \def (eq_ind C (CHead d (Bind Abbr) u) (\lambda (c0: 
 C).(getl i c c0)) H (CHead d0 (Bind Abbr) u0) (getl_mono c (CHead d (Bind 
 Abbr) u) i H (CHead d0 (Bind Abbr) u0) H15)) in (let H17 \def (f_equal C C 
-(\lambda (e: C).(match e in C return (\lambda (_: C).C) with [(CSort _) 
-\Rightarrow d | (CHead c0 _ _) \Rightarrow c0])) (CHead d (Bind Abbr) u) 
-(CHead d0 (Bind Abbr) u0) (getl_mono c (CHead d (Bind Abbr) u) i H (CHead d0 
-(Bind Abbr) u0) H15)) in ((let H18 \def (f_equal C T (\lambda (e: C).(match e 
-in C return (\lambda (_: C).T) with [(CSort _) \Rightarrow u | (CHead _ _ t) 
-\Rightarrow t])) (CHead d (Bind Abbr) u) (CHead d0 (Bind Abbr) u0) (getl_mono 
-c (CHead d (Bind Abbr) u) i H (CHead d0 (Bind Abbr) u0) H15)) in (\lambda 
-(H19: (eq C d d0)).(let H20 \def (eq_ind_r T u0 (\lambda (t: T).(subst0 i t x 
-x1)) H14 u H18) in (let H21 \def (eq_ind_r T u0 (\lambda (t: T).(getl i c 
-(CHead d0 (Bind Abbr) t))) H16 u H18) in (let H22 \def (eq_ind_r C d0 
-(\lambda (c0: C).(getl i c (CHead c0 (Bind Abbr) u))) H21 d H19) in (or4_ind 
-(eq T x1 x0) (ex2 T (\lambda (t: T).(subst0 i u x1 t)) (\lambda (t: 
-T).(subst0 i u x0 t))) (subst0 i u x1 x0) (subst0 i u x0 x1) (ex2 T (\lambda 
-(t: T).(pr2 c t1 t)) (\lambda (t: T).(pr2 c t2 t))) (\lambda (H23: (eq T x1 
-x0)).(let H24 \def (eq_ind T x1 (\lambda (t: T).(pr0 t2 t)) H11 x0 H23) in 
-(ex_intro2 T (\lambda (t: T).(pr2 c t1 t)) (\lambda (t: T).(pr2 c t2 t)) x0 
-(pr2_free c t1 x0 H8) (pr2_free c t2 x0 H24)))) (\lambda (H23: (ex2 T 
-(\lambda (t: T).(subst0 i u x1 t)) (\lambda (t: T).(subst0 i u x0 
-t)))).(ex2_ind T (\lambda (t: T).(subst0 i u x1 t)) (\lambda (t: T).(subst0 i 
-u x0 t)) (ex2 T (\lambda (t: T).(pr2 c t1 t)) (\lambda (t: T).(pr2 c t2 t))) 
-(\lambda (x2: T).(\lambda (H24: (subst0 i u x1 x2)).(\lambda (H25: (subst0 i 
-u x0 x2)).(ex_intro2 T (\lambda (t: T).(pr2 c t1 t)) (\lambda (t: T).(pr2 c 
-t2 t)) x2 (pr2_delta c d u i H22 t1 x0 H8 x2 H25) (pr2_delta c d u i H22 t2 
-x1 H11 x2 H24))))) H23)) (\lambda (H23: (subst0 i u x1 x0)).(ex_intro2 T 
-(\lambda (t: T).(pr2 c t1 t)) (\lambda (t: T).(pr2 c t2 t)) x0 (pr2_free c t1 
-x0 H8) (pr2_delta c d u i H22 t2 x1 H11 x0 H23))) (\lambda (H23: (subst0 i u 
-x0 x1)).(ex_intro2 T (\lambda (t: T).(pr2 c t1 t)) (\lambda (t: T).(pr2 c t2 
-t)) x1 (pr2_delta c d u i H22 t1 x0 H8 x1 H23) (pr2_free c t2 x1 H11))) 
-(subst0_confluence_eq x x1 u i H20 x0 H9))))))) H17)))))))))) H10)) 
-(pr0_subst0 t4 x H5 u0 t2 i0 H4 u0 (pr0_refl u0)))))) H7)) (pr0_subst0 t3 x 
-H6 u t1 i H1 u (pr0_refl u)))))) (pr0_confluence t0 t4 H3 t3 
-H0))))))))))))))))))).
-(* COMMENTS
-Initial nodes: 1901
-END *)
+(\lambda (e: C).(match e with [(CSort _) \Rightarrow d | (CHead c0 _ _) 
+\Rightarrow c0])) (CHead d (Bind Abbr) u) (CHead d0 (Bind Abbr) u0) 
+(getl_mono c (CHead d (Bind Abbr) u) i H (CHead d0 (Bind Abbr) u0) H15)) in 
+((let H18 \def (f_equal C T (\lambda (e: C).(match e with [(CSort _) 
+\Rightarrow u | (CHead _ _ t) \Rightarrow t])) (CHead d (Bind Abbr) u) (CHead 
+d0 (Bind Abbr) u0) (getl_mono c (CHead d (Bind Abbr) u) i H (CHead d0 (Bind 
+Abbr) u0) H15)) in (\lambda (H19: (eq C d d0)).(let H20 \def (eq_ind_r T u0 
+(\lambda (t: T).(subst0 i t x x1)) H14 u H18) in (let H21 \def (eq_ind_r T u0 
+(\lambda (t: T).(getl i c (CHead d0 (Bind Abbr) t))) H16 u H18) in (let H22 
+\def (eq_ind_r C d0 (\lambda (c0: C).(getl i c (CHead c0 (Bind Abbr) u))) H21 
+d H19) in (or4_ind (eq T x1 x0) (ex2 T (\lambda (t: T).(subst0 i u x1 t)) 
+(\lambda (t: T).(subst0 i u x0 t))) (subst0 i u x1 x0) (subst0 i u x0 x1) 
+(ex2 T (\lambda (t: T).(pr2 c t1 t)) (\lambda (t: T).(pr2 c t2 t))) (\lambda 
+(H23: (eq T x1 x0)).(let H24 \def (eq_ind T x1 (\lambda (t: T).(pr0 t2 t)) 
+H11 x0 H23) in (ex_intro2 T (\lambda (t: T).(pr2 c t1 t)) (\lambda (t: 
+T).(pr2 c t2 t)) x0 (pr2_free c t1 x0 H8) (pr2_free c t2 x0 H24)))) (\lambda 
+(H23: (ex2 T (\lambda (t: T).(subst0 i u x1 t)) (\lambda (t: T).(subst0 i u 
+x0 t)))).(ex2_ind T (\lambda (t: T).(subst0 i u x1 t)) (\lambda (t: 
+T).(subst0 i u x0 t)) (ex2 T (\lambda (t: T).(pr2 c t1 t)) (\lambda (t: 
+T).(pr2 c t2 t))) (\lambda (x2: T).(\lambda (H24: (subst0 i u x1 
+x2)).(\lambda (H25: (subst0 i u x0 x2)).(ex_intro2 T (\lambda (t: T).(pr2 c 
+t1 t)) (\lambda (t: T).(pr2 c t2 t)) x2 (pr2_delta c d u i H22 t1 x0 H8 x2 
+H25) (pr2_delta c d u i H22 t2 x1 H11 x2 H24))))) H23)) (\lambda (H23: 
+(subst0 i u x1 x0)).(ex_intro2 T (\lambda (t: T).(pr2 c t1 t)) (\lambda (t: 
+T).(pr2 c t2 t)) x0 (pr2_free c t1 x0 H8) (pr2_delta c d u i H22 t2 x1 H11 x0 
+H23))) (\lambda (H23: (subst0 i u x0 x1)).(ex_intro2 T (\lambda (t: T).(pr2 c 
+t1 t)) (\lambda (t: T).(pr2 c t2 t)) x1 (pr2_delta c d u i H22 t1 x0 H8 x1 
+H23) (pr2_free c t2 x1 H11))) (subst0_confluence_eq x x1 u i H20 x0 H9))))))) 
+H17)))))))))) H10)) (pr0_subst0 t4 x H5 u0 t2 i0 H4 u0 (pr0_refl u0)))))) 
+H7)) (pr0_subst0 t3 x H6 u t1 i H1 u (pr0_refl u)))))) (pr0_confluence t0 t4 
+H3 t3 H0))))))))))))))))))).
 
 theorem pr2_confluence:
  \forall (c: C).(\forall (t0: T).(\forall (t1: T).((pr2 c t0 t1) \to (\forall 
@@ -164,10 +154,7 @@ theorem pr2_confluence:
 T).(pr2 c t2 t))))))))
 \def
  \lambda (c: C).(\lambda (t0: T).(\lambda (t1: T).(\lambda (H: (pr2 c t0 
-t1)).(\lambda (t2: T).(\lambda (H0: (pr2 c t0 t2)).(let H1 \def (match H in 
-pr2 return (\lambda (c0: C).(\lambda (t: T).(\lambda (t3: T).(\lambda (_: 
-(pr2 c0 t t3)).((eq C c0 c) \to ((eq T t t0) \to ((eq T t3 t1) \to (ex2 T 
-(\lambda (t4: T).(pr2 c t1 t4)) (\lambda (t4: T).(pr2 c t2 t4)))))))))) with 
+t1)).(\lambda (t2: T).(\lambda (H0: (pr2 c t0 t2)).(let H1 \def (match H with 
 [(pr2_free c0 t3 t4 H1) \Rightarrow (\lambda (H2: (eq C c0 c)).(\lambda (H3: 
 (eq T t3 t0)).(\lambda (H4: (eq T t4 t1)).(eq_ind C c (\lambda (_: C).((eq T 
 t3 t0) \to ((eq T t4 t1) \to ((pr0 t3 t4) \to (ex2 T (\lambda (t: T).(pr2 c 
@@ -176,10 +163,7 @@ T t0 (\lambda (t: T).((eq T t4 t1) \to ((pr0 t t4) \to (ex2 T (\lambda (t5:
 T).(pr2 c t1 t5)) (\lambda (t5: T).(pr2 c t2 t5)))))) (\lambda (H6: (eq T t4 
 t1)).(eq_ind T t1 (\lambda (t: T).((pr0 t0 t) \to (ex2 T (\lambda (t5: 
 T).(pr2 c t1 t5)) (\lambda (t5: T).(pr2 c t2 t5))))) (\lambda (H7: (pr0 t0 
-t1)).(let H8 \def (match H0 in pr2 return (\lambda (c1: C).(\lambda (t: 
-T).(\lambda (t5: T).(\lambda (_: (pr2 c1 t t5)).((eq C c1 c) \to ((eq T t t0) 
-\to ((eq T t5 t2) \to (ex2 T (\lambda (t6: T).(pr2 c t1 t6)) (\lambda (t6: 
-T).(pr2 c t2 t6)))))))))) with [(pr2_free c1 t5 t6 H8) \Rightarrow (\lambda 
+t1)).(let H8 \def (match H0 with [(pr2_free c1 t5 t6 H8) \Rightarrow (\lambda 
 (H9: (eq C c1 c)).(\lambda (H10: (eq T t5 t0)).(\lambda (H11: (eq T t6 
 t2)).(eq_ind C c (\lambda (_: C).((eq T t5 t0) \to ((eq T t6 t2) \to ((pr0 t5 
 t6) \to (ex2 T (\lambda (t: T).(pr2 c t1 t)) (\lambda (t: T).(pr2 c t2 
@@ -219,10 +203,7 @@ T t1 (\lambda (t5: T).((getl i c (CHead d (Bind Abbr) u)) \to ((pr0 t0 t4)
 \to ((subst0 i u t4 t5) \to (ex2 T (\lambda (t6: T).(pr2 c t1 t6)) (\lambda 
 (t6: T).(pr2 c t2 t6))))))) (\lambda (H9: (getl i c (CHead d (Bind Abbr) 
 u))).(\lambda (H10: (pr0 t0 t4)).(\lambda (H11: (subst0 i u t4 t1)).(let H12 
-\def (match H0 in pr2 return (\lambda (c1: C).(\lambda (t5: T).(\lambda (t6: 
-T).(\lambda (_: (pr2 c1 t5 t6)).((eq C c1 c) \to ((eq T t5 t0) \to ((eq T t6 
-t2) \to (ex2 T (\lambda (t7: T).(pr2 c t1 t7)) (\lambda (t7: T).(pr2 c t2 
-t7)))))))))) with [(pr2_free c1 t5 t6 H12) \Rightarrow (\lambda (H13: (eq C 
+\def (match H0 with [(pr2_free c1 t5 t6 H12) \Rightarrow (\lambda (H13: (eq C 
 c1 c)).(\lambda (H14: (eq T t5 t0)).(\lambda (H15: (eq T t6 t2)).(eq_ind C c 
 (\lambda (_: C).((eq T t5 t0) \to ((eq T t6 t2) \to ((pr0 t5 t6) \to (ex2 T 
 (\lambda (t7: T).(pr2 c t1 t7)) (\lambda (t7: T).(pr2 c t2 t7))))))) (\lambda 
@@ -252,7 +233,4 @@ H11 H20 H21 H22)))) t7 (sym_eq T t7 t2 H19))) t5 (sym_eq T t5 t0 H18))) c1
 (refl_equal T t0) (refl_equal T t2)))))) t (sym_eq T t t1 H8))) t3 (sym_eq T 
 t3 t0 H7))) c0 (sym_eq C c0 c H4) H5 H6 H1 H2 H3))))]) in (H1 (refl_equal C 
 c) (refl_equal T t0) (refl_equal T t1)))))))).
-(* COMMENTS
-Initial nodes: 2087
-END *)