X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=matita%2Fmatita%2Fcontribs%2Flambda_delta%2Fbasic_2%2Fsubstitution%2Flsubs.ma;h=f27883b028036991a6bff9a38df2adef4075bd13;hb=fec1a061eeca5e7e05b4f0c3e299983b163569c3;hp=fb6468c909ff6eb4c2381100216a8e7bf9009bc3;hpb=78d4844bcccb3deb58a3179151c3045298782b18;p=helm.git

diff --git a/matita/matita/contribs/lambda_delta/basic_2/substitution/lsubs.ma b/matita/matita/contribs/lambda_delta/basic_2/substitution/lsubs.ma
index fb6468c90..f27883b02 100644
--- a/matita/matita/contribs/lambda_delta/basic_2/substitution/lsubs.ma
+++ b/matita/matita/contribs/lambda_delta/basic_2/substitution/lsubs.ma
@@ -22,7 +22,7 @@ inductive lsubs: nat → nat → relation lenv ≝
 | lsubs_abbr: ∀L1,L2,V,e. lsubs 0 e L1 L2 →
               lsubs 0 (e + 1) (L1. ⓓV) (L2.ⓓV)
 | lsubs_abst: ∀L1,L2,I,V1,V2,e. lsubs 0 e L1 L2 →
-              lsubs 0 (e + 1) (L1. ⓛV1) (L2.ⓑ{I} V2)
+              lsubs 0 (e + 1) (L1. ⓑ{I}V1) (L2. ⓛV2)
 | lsubs_skip: ∀L1,L2,I1,I2,V1,V2,d,e.
               lsubs d e L1 L2 → lsubs (d + 1) e (L1. ⓑ{I1} V1) (L2. ⓑ{I2} V2)
 .
@@ -31,9 +31,9 @@ interpretation
   "local environment refinement (substitution)"
   'SubEq L1 d e L2 = (lsubs d e L1 L2).
 
-definition lsubs_conf: ∀S. (lenv → relation S) → Prop ≝ λS,R.
-                       ∀L1,s1,s2. R L1 s1 s2 →
-                       ∀L2,d,e. L1 ≼ [d, e] L2 → R L2 s1 s2.
+definition lsubs_trans: ∀S. (lenv → relation S) → Prop ≝ λS,R.
+                        ∀L2,s1,s2. R L2 s1 s2 →
+                        ∀L1,d,e. L1 ≼ [d, e] L2 → R L1 s1 s2.
 
 (* Basic properties *********************************************************)
 
@@ -48,7 +48,7 @@ lemma lsubs_abbr_lt: ∀L1,L2,V,e. L1 ≼ [0, e - 1] L2 → 0 < e →
 qed.
 
 lemma lsubs_abst_lt: ∀L1,L2,I,V1,V2,e. L1 ≼ [0, e - 1] L2 → 0 < e →
-                     L1. ⓛV1 ≼ [0, e] L2.ⓑ{I} V2.
+                     L1. ⓑ{I}V1 ≼ [0, e] L2. ⓛV2.
 #L1 #L2 #I #V1 #V2 #e #HL12 #He >(plus_minus_m_m e 1) // /2 width=1/
 qed.
 
@@ -58,7 +58,7 @@ lemma lsubs_skip_lt: ∀L1,L2,d,e. L1 ≼ [d - 1, e] L2 → 0 < d →
 qed.
 
 lemma lsubs_bind_lt: ∀I,L1,L2,V,e. L1 ≼ [0, e - 1] L2 → 0 < e → 
-                     L1. ⓑ{I}V ≼ [0, e] L2.ⓓV.
+                     L1. ⓓV ≼ [0, e] L2. ⓑ{I}V.
 * /2 width=1/ qed.
 
 lemma lsubs_refl: ∀d,e,L. L ≼ [d, e] L.
@@ -68,7 +68,7 @@ lemma lsubs_refl: ∀d,e,L. L ≼ [d, e] L.
 ]
 qed.
 
-lemma TC_lsubs_conf: ∀S,R. lsubs_conf S R → lsubs_conf S (λL. (TC … (R L))).
+lemma TC_lsubs_trans: ∀S,R. lsubs_trans S R → lsubs_trans S (λL. (TC … (R L))).
 #S #R #HR #L1 #s1 #s2 #H elim H -s2
 [ /3 width=5/
 | #s #s2 #_ #Hs2 #IHs1 #L2 #d #e #HL12
@@ -93,9 +93,43 @@ lemma lsubs_inv_atom1: ∀L2,d,e. ⋆ ≼ [d, e] L2 →
                        L2 = ⋆ ∨ (d = 0 ∧ e = 0).
 /2 width=3/ qed-.
 
-fact lsubs_inv_abbr1_aux: ∀L1,L2,d,e. L1 ≼ [d, e] L2 →
-                          ∀K1,V. L1 = K1.ⓓV → d = 0 → 0 < e →
-                          ∃∃K2. K1 ≼ [0, e - 1] K2 & L2 = K2.ⓓV.
+fact lsubs_inv_skip1_aux: ∀L1,L2,d,e. L1 ≼ [d, e] L2 →
+                          ∀I1,K1,V1. L1 = K1.ⓑ{I1}V1 → 0 < d →
+                          ∃∃I2,K2,V2. K1 ≼ [d - 1, e] K2 & L2 = K2.ⓑ{I2}V2.
+#L1 #L2 #d #e * -L1 -L2 -d -e
+[ #d #e #I1 #K1 #V1 #H destruct
+| #L1 #L2 #I1 #K1 #V1 #_ #H
+  elim (lt_zero_false … H)
+| #L1 #L2 #W #e #_ #I1 #K1 #V1 #_ #H
+  elim (lt_zero_false … H)
+| #L1 #L2 #I #W1 #W2 #e #_ #I1 #K1 #V1 #_ #H
+  elim (lt_zero_false … H)
+| #L1 #L2 #J1 #J2 #W1 #W2 #d #e #HL12 #I1 #K1 #V1 #H #_ destruct /2 width=5/
+]
+qed.
+
+lemma lsubs_inv_skip1: ∀I1,K1,L2,V1,d,e. K1.ⓑ{I1}V1 ≼ [d, e] L2 → 0 < d →
+                       ∃∃I2,K2,V2. K1 ≼ [d - 1, e] K2 & L2 = K2.ⓑ{I2}V2.
+/2 width=5/ qed-.
+
+fact lsubs_inv_atom2_aux: ∀L1,L2,d,e. L1 ≼ [d, e] L2 → L2 = ⋆ →
+                          L1 = ⋆ ∨ (d = 0 ∧ e = 0).
+#L1 #L2 #d #e * -L1 -L2 -d -e
+[ /2 width=1/
+| /3 width=1/
+| #L1 #L2 #W #e #_ #H destruct
+| #L1 #L2 #I #W1 #W2 #e #_ #H destruct
+| #L1 #L2 #I1 #I2 #W1 #W2 #d #e #_ #H destruct
+]
+qed.
+
+lemma lsubs_inv_atom2: ∀L1,d,e. L1 ≼ [d, e] ⋆ →
+                       L1 = ⋆ ∨ (d = 0 ∧ e = 0).
+/2 width=3/ qed-.
+
+fact lsubs_inv_abbr2_aux: ∀L1,L2,d,e. L1 ≼ [d, e] L2 →
+                          ∀K2,V. L2 = K2.ⓓV → d = 0 → 0 < e →
+                          ∃∃K1. K1 ≼ [0, e - 1] K2 & L1 = K1.ⓓV.
 #L1 #L2 #d #e * -L1 -L2 -d -e
 [ #d #e #K1 #V #H destruct
 | #L1 #L2 #K1 #V #_ #_ #H
@@ -106,13 +140,13 @@ fact lsubs_inv_abbr1_aux: ∀L1,L2,d,e. L1 ≼ [d, e] L2 →
 ]
 qed.
 
-lemma lsubs_inv_abbr1: ∀K1,L2,V,e. K1.ⓓV ≼ [0, e] L2 → 0 < e →
-                       ∃∃K2. K1 ≼ [0, e - 1] K2 & L2 = K2.ⓓV.
+lemma lsubs_inv_abbr2: ∀L1,K2,V,e. L1 ≼ [0, e] K2.ⓓV → 0 < e →
+                       ∃∃K1. K1 ≼ [0, e - 1] K2 & L1 = K1.ⓓV.
 /2 width=5/ qed-.
 
-fact lsubs_inv_skip1_aux: ∀L1,L2,d,e. L1 ≼ [d, e] L2 →
-                          ∀I1,K1,V1. L1 = K1.ⓑ{I1}V1 → 0 < d →
-                          ∃∃I2,K2,V2. K1 ≼ [d - 1, e] K2 & L2 = K2.ⓑ{I2}V2.
+fact lsubs_inv_skip2_aux: ∀L1,L2,d,e. L1 ≼ [d, e] L2 →
+                          ∀I2,K2,V2. L2 = K2.ⓑ{I2}V2 → 0 < d →
+                          ∃∃I1,K1,V1. K1 ≼ [d - 1, e] K2 & L1 = K1.ⓑ{I1}V1.
 #L1 #L2 #d #e * -L1 -L2 -d -e
 [ #d #e #I1 #K1 #V1 #H destruct
 | #L1 #L2 #I1 #K1 #V1 #_ #H
@@ -125,8 +159,8 @@ fact lsubs_inv_skip1_aux: ∀L1,L2,d,e. L1 ≼ [d, e] L2 →
 ]
 qed.
 
-lemma lsubs_inv_skip1: ∀I1,K1,L2,V1,d,e. K1.ⓑ{I1}V1 ≼ [d, e] L2 → 0 < d →
-                       ∃∃I2,K2,V2. K1 ≼ [d - 1, e] K2 & L2 = K2.ⓑ{I2}V2.
+lemma lsubs_inv_skip2: ∀I2,L1,K2,V2,d,e. L1 ≼ [d, e] K2.ⓑ{I2}V2 → 0 < d →
+                       ∃∃I1,K1,V1. K1 ≼ [d - 1, e] K2 & L1 = K1.ⓑ{I1}V1.
 /2 width=5/ qed-.
 
 (* Basic forward lemmas *****************************************************)