- main proposition on lsx finally proved!

[helm.git] / matita / matita / contribs / lambdadelta / basic_2 / computation / lsx_ldrop.ma

diff --git a/matita/matita/contribs/lambdadelta/basic_2/computation/lsx_ldrop.ma b/matita/matita/contribs/lambdadelta/basic_2/computation/lsx_ldrop.ma
index 261168b92375f5ae1a41e3a6e2478ef93995be18..cdb3f2fbc4bbd7ffce648484f0179dee0f8cb93c 100644 (file)
--- a/matita/matita/contribs/lambdadelta/basic_2/computation/lsx_ldrop.ma
+++ b/matita/matita/contribs/lambdadelta/basic_2/computation/lsx_ldrop.ma
@@ -13,6 +13,7 @@
 (**************************************************************************)
 
 include "basic_2/substitution/lleq_ldrop.ma".
+include "basic_2/computation/lpxs_ldrop.ma".
 include "basic_2/computation/lsx.ma".
 
 (* SN EXTENDED STRONGLY NORMALIZING LOCAL ENVIRONMENTS **********************)
@@ -30,3 +31,52 @@ lemma lsx_lref_skip: ∀h,g,G,L,d,i. yinj i < d → G ⊢ ⋕⬊*[h, g, #i, d] L
 #L2 #HL12 #H elim H -H
 /3 width=4 by lpxs_fwd_length, lleq_skip/
 qed.
+
+(* Properties on relocation *************************************************)
+
+lemma lsx_lift_le: ∀h,g,G,K,T,U,dt,d,e. dt ≤ yinj d →
+                   ⇧[d, e] T ≡ U → G ⊢ ⋕⬊*[h, g, T, dt] K →
+                   ∀L. ⇩[Ⓕ, d, e] L ≡ K → G ⊢ ⋕⬊*[h, g, U, dt] L.
+#h #g #G #K #T #U #dt #d #e #Hdtd #HTU #H @(lsx_ind … H) -K
+#K1 #_ #IHK1 #L1 #HLK1 @lsx_intro
+#L2 #HL12 #HnU elim (lpxs_ldrop_conf … HLK1 … HL12) -HL12
+/4 width=10 by lleq_lift_le/
+qed-.
+
+lemma lsx_lift_ge: ∀h,g,G,K,T,U,dt,d,e. yinj d ≤ dt →
+                   ⇧[d, e] T ≡ U → G ⊢ ⋕⬊*[h, g, T, dt] K →
+                   ∀L. ⇩[Ⓕ, d, e] L ≡ K → G ⊢ ⋕⬊*[h, g, U, dt + e] L.
+#h #g #G #K #T #U #dt #d #e #Hddt #HTU #H @(lsx_ind … H) -K
+#K1 #_ #IHK1 #L1 #HLK1 @lsx_intro
+#L2 #HL12 #HnU elim (lpxs_ldrop_conf … HLK1 … HL12) -HL12
+/4 width=9 by lleq_lift_ge/
+qed-.
+
+(* Inversion lemmas on relocation *******************************************)
+
+lemma lsx_inv_lift_le: ∀h,g,G,L,T,U,dt,d,e. dt ≤ yinj d →
+                       ⇧[d, e] T ≡ U → G ⊢ ⋕⬊*[h, g, U, dt] L →
+                       ∀K. ⇩[Ⓕ, d, e] L ≡ K → G ⊢ ⋕⬊*[h, g, T, dt] K.
+#h #g #G #L #T #U #dt #d #e #Hdtd #HTU #H @(lsx_ind … H) -L
+#L1 #_ #IHL1 #K1 #HLK1 @lsx_intro
+#K2 #HK12 #HnT elim (ldrop_lpxs_trans … HLK1 … HK12) -HK12
+/4 width=10 by lleq_inv_lift_le/
+qed-.
+
+lemma lsx_inv_lift_be: ∀h,g,G,L,T,U,dt,d,e. yinj d ≤ dt → dt ≤ d + e →
+                       ⇧[d, e] T ≡ U → G ⊢ ⋕⬊*[h, g, U, dt] L →
+                       ∀K. ⇩[Ⓕ, d, e] L ≡ K → G ⊢ ⋕⬊*[h, g, T, d] K.
+#h #g #G #L #T #U #dt #d #e #Hddt #Hdtde #HTU #H @(lsx_ind … H) -L
+#L1 #_ #IHL1 #K1 #HLK1 @lsx_intro
+#K2 #HK12 #HnT elim (ldrop_lpxs_trans … HLK1 … HK12) -HK12
+/4 width=11 by lleq_inv_lift_be/
+qed-.
+
+lemma lsx_inv_lift_ge: ∀h,g,G,L,T,U,dt,d,e. yinj d + yinj e ≤ dt →
+                       ⇧[d, e] T ≡ U → G ⊢ ⋕⬊*[h, g, U, dt] L →
+                       ∀K. ⇩[Ⓕ, d, e] L ≡ K → G ⊢ ⋕⬊*[h, g, T, dt-e] K.
+#h #g #G #L #T #U #dt #d #e #Hdedt #HTU #H @(lsx_ind … H) -L
+#L1 #_ #IHL1 #K1 #HLK1 @lsx_intro
+#K2 #HK12 #HnT elim (ldrop_lpxs_trans … HLK1 … HK12) -HK12
+/4 width=9 by lleq_inv_lift_ge/
+qed-.