1 (**************************************************************************)
4 (* ||A|| A project by Andrea Asperti *)
6 (* ||I|| Developers: *)
7 (* ||T|| The HELM team. *)
8 (* ||A|| http://helm.cs.unibo.it *)
10 (* \ / This file is distributed under the terms of the *)
11 (* v GNU General Public License Version 2 *)
13 (**************************************************************************)
15 include "basic_2/substitution/lleq_ldrop.ma".
16 include "basic_2/computation/lpxs_ldrop.ma".
17 include "basic_2/computation/lsx.ma".
19 (* SN EXTENDED STRONGLY NORMALIZING LOCAL ENVIRONMENTS **********************)
21 (* Advanced properties ******************************************************)
23 lemma lsx_lref_free: ∀h,g,G,L,d,i. |L| ≤ i → G ⊢ ⋕⬊*[h, g, #i, d] L.
24 #h #g #G #L1 #d #i #HL1 @lsx_intro
25 #L2 #HL12 #H elim H -H
26 /4 width=6 by lpxs_fwd_length, lleq_free, le_repl_sn_conf_aux/
29 lemma lsx_lref_skip: ∀h,g,G,L,d,i. yinj i < d → G ⊢ ⋕⬊*[h, g, #i, d] L.
30 #h #g #G #L1 #d #i #HL1 @lsx_intro
31 #L2 #HL12 #H elim H -H
32 /3 width=4 by lpxs_fwd_length, lleq_skip/
35 (* Properties on relocation *************************************************)
37 lemma lsx_lift_le: ∀h,g,G,K,T,U,dt,d,e. dt ≤ yinj d →
38 ⇧[d, e] T ≡ U → G ⊢ ⋕⬊*[h, g, T, dt] K →
39 ∀L. ⇩[Ⓕ, d, e] L ≡ K → G ⊢ ⋕⬊*[h, g, U, dt] L.
40 #h #g #G #K #T #U #dt #d #e #Hdtd #HTU #H @(lsx_ind … H) -K
41 #K1 #_ #IHK1 #L1 #HLK1 @lsx_intro
42 #L2 #HL12 #HnU elim (lpxs_ldrop_conf … HLK1 … HL12) -HL12
43 /4 width=10 by lleq_lift_le/
46 lemma lsx_lift_ge: ∀h,g,G,K,T,U,dt,d,e. yinj d ≤ dt →
47 ⇧[d, e] T ≡ U → G ⊢ ⋕⬊*[h, g, T, dt] K →
48 ∀L. ⇩[Ⓕ, d, e] L ≡ K → G ⊢ ⋕⬊*[h, g, U, dt + e] L.
49 #h #g #G #K #T #U #dt #d #e #Hddt #HTU #H @(lsx_ind … H) -K
50 #K1 #_ #IHK1 #L1 #HLK1 @lsx_intro
51 #L2 #HL12 #HnU elim (lpxs_ldrop_conf … HLK1 … HL12) -HL12
52 /4 width=9 by lleq_lift_ge/
55 (* Inversion lemmas on relocation *******************************************)
57 lemma lsx_inv_lift_le: ∀h,g,G,L,T,U,dt,d,e. dt ≤ yinj d →
58 ⇧[d, e] T ≡ U → G ⊢ ⋕⬊*[h, g, U, dt] L →
59 ∀K. ⇩[Ⓕ, d, e] L ≡ K → G ⊢ ⋕⬊*[h, g, T, dt] K.
60 #h #g #G #L #T #U #dt #d #e #Hdtd #HTU #H @(lsx_ind … H) -L
61 #L1 #_ #IHL1 #K1 #HLK1 @lsx_intro
62 #K2 #HK12 #HnT elim (ldrop_lpxs_trans … HLK1 … HK12) -HK12
63 /4 width=10 by lleq_inv_lift_le/
66 lemma lsx_inv_lift_be: ∀h,g,G,L,T,U,dt,d,e. yinj d ≤ dt → dt ≤ d + e →
67 ⇧[d, e] T ≡ U → G ⊢ ⋕⬊*[h, g, U, dt] L →
68 ∀K. ⇩[Ⓕ, d, e] L ≡ K → G ⊢ ⋕⬊*[h, g, T, d] K.
69 #h #g #G #L #T #U #dt #d #e #Hddt #Hdtde #HTU #H @(lsx_ind … H) -L
70 #L1 #_ #IHL1 #K1 #HLK1 @lsx_intro
71 #K2 #HK12 #HnT elim (ldrop_lpxs_trans … HLK1 … HK12) -HK12
72 /4 width=11 by lleq_inv_lift_be/
75 lemma lsx_inv_lift_ge: ∀h,g,G,L,T,U,dt,d,e. yinj d + yinj e ≤ dt →
76 ⇧[d, e] T ≡ U → G ⊢ ⋕⬊*[h, g, U, dt] L →
77 ∀K. ⇩[Ⓕ, d, e] L ≡ K → G ⊢ ⋕⬊*[h, g, T, dt-e] K.
78 #h #g #G #L #T #U #dt #d #e #Hdedt #HTU #H @(lsx_ind … H) -L
79 #L1 #_ #IHL1 #K1 #HLK1 @lsx_intro
80 #K2 #HK12 #HnT elim (ldrop_lpxs_trans … HLK1 … HK12) -HK12
81 /4 width=9 by lleq_inv_lift_ge/