--- /dev/null
+(**************************************************************************)
+(* ___ *)
+(* ||M|| *)
+(* ||A|| A project by Andrea Asperti *)
+(* ||T|| *)
+(* ||I|| Developers: *)
+(* ||T|| The HELM team. *)
+(* ||A|| http://helm.cs.unibo.it *)
+(* \ / *)
+(* \ / This file is distributed under the terms of the *)
+(* v GNU General Public License Version 2 *)
+(* *)
+(**************************************************************************)
+
+include "basic_2/notation/relations/cosn_5.ma".
+include "basic_2/computation/lsx.ma".
+
+(* SN EXTENDED STRONGLY CONORMALIZING LOCAL ENVIRONMENTS ********************)
+
+inductive lcosx (h) (g) (G): relation2 ynat lenv ≝
+| lcosx_sort: ∀d. lcosx h g G d (⋆)
+| lcosx_skip: ∀I,L,T. lcosx h g G 0 L → lcosx h g G 0 (L.ⓑ{I}T)
+| lcosx_pair: ∀I,L,T,d. G ⊢ ⬊*[h, g, T, d] L →
+ lcosx h g G d L → lcosx h g G (⫯d) (L.ⓑ{I}T)
+.
+
+interpretation
+ "sn extended strong conormalization (local environment)"
+ 'CoSN h g d G L = (lcosx h g G d L).
+
+(* Basic properties *********************************************************)
+
+lemma lcosx_O: ∀h,g,G,L. G ⊢ ~⬊*[h, g, 0] L.
+#h #g #G #L elim L /2 width=1 by lcosx_skip/
+qed.
+
+lemma lcosx_ldrop_trans_lt: ∀h,g,G,L,d. G ⊢ ~⬊*[h, g, d] L →
+ ∀I,K,V,i. ⇩[i] L ≡ K.ⓑ{I}V → i < d →
+ G ⊢ ~⬊*[h, g, ⫰(d-i)] K ∧ G ⊢ ⬊*[h, g, V, ⫰(d-i)] K.
+#h #g #G #L #d #H elim H -L -d
+[ #d #J #K #V #i #H elim (ldrop_inv_atom1 … H) -H #H destruct
+| #I #L #T #_ #_ #J #K #V #i #_ #H elim (ylt_yle_false … H) -H //
+| #I #L #T #d #HT #HL #IHL #J #K #V #i #H #Hid
+ elim (ldrop_inv_O1_pair1 … H) -H * #Hi #HLK destruct
+ [ >ypred_succ /2 width=1 by conj/
+ | lapply (ylt_pred … Hid ?) -Hid /2 width=1 by ylt_inj/ >ypred_succ #Hid
+ elim (IHL … HLK ?) -IHL -HLK <yminus_inj >yminus_SO2 //
+ <(ypred_succ d) in ⊢ (%→%→?); >yminus_pred /2 width=1 by ylt_inj, conj/
+ ]
+]
+qed-.
+
+(* Basic inversion lemmas ***************************************************)
+
+fact lcosx_inv_succ_aux: ∀h,g,G,L,x. G ⊢ ~⬊*[h, g, x] L → ∀d. x = ⫯d →
+ L = ⋆ ∨
+ ∃∃I,K,V. L = K.ⓑ{I}V & G ⊢ ~⬊*[h, g, d] K &
+ G ⊢ ⬊*[h, g, V, d] K.
+#h #g #G #L #d * -L -d /2 width=1 by or_introl/
+[ #I #L #T #_ #x #H elim (ysucc_inv_O_sn … H)
+| #I #L #T #d #HT #HL #x #H <(ysucc_inj … H) -x
+ /3 width=6 by ex3_3_intro, or_intror/
+]
+qed-.
+
+lemma lcosx_inv_succ: ∀h,g,G,L,d. G ⊢ ~⬊*[h, g, ⫯d] L → L = ⋆ ∨
+ ∃∃I,K,V. L = K.ⓑ{I}V & G ⊢ ~⬊*[h, g, d] K &
+ G ⊢ ⬊*[h, g, V, d] K.
+/2 width=3 by lcosx_inv_succ_aux/ qed-.
+
+lemma lcosx_inv_pair: ∀h,g,I,G,L,T,d. G ⊢ ~⬊*[h, g, ⫯d] L.ⓑ{I}T →
+ G ⊢ ~⬊*[h, g, d] L ∧ G ⊢ ⬊*[h, g, T, d] L.
+#h #g #I #G #L #T #d #H elim (lcosx_inv_succ … H) -H
+[ #H destruct
+| * #Z #Y #X #H destruct /2 width=1 by conj/
+]
+qed-.
--- /dev/null
+(**************************************************************************)
+(* ___ *)
+(* ||M|| *)
+(* ||A|| A project by Andrea Asperti *)
+(* ||T|| *)
+(* ||I|| Developers: *)
+(* ||T|| The HELM team. *)
+(* ||A|| http://helm.cs.unibo.it *)
+(* \ / *)
+(* \ / This file is distributed under the terms of the *)
+(* v GNU General Public License Version 2 *)
+(* *)
+(**************************************************************************)
+
+include "ground_2/ynat/ynat_max.ma".
+include "basic_2/computation/lsx_ldrop.ma".
+include "basic_2/computation/lsx_lpx.ma".
+include "basic_2/computation/lsx_lpxs.ma".
+include "basic_2/computation/lcosx.ma".
+
+(* SN EXTENDED STRONGLY CONORMALIZING LOCAL ENVIRONMENTS ********************)
+
+(* Properties on extended context-sensitive parallel reduction for term *****)
+
+lemma lsx_cpx_trans_lcosx: ∀h,g,G,L,T1,T2. ⦃G, L⦄ ⊢ T1 ➡[h, g] T2 →
+ ∀d. G ⊢ ~⬊*[h, g, d] L →
+ G ⊢ ⬊*[h, g, T1, d] L → G ⊢ ⬊*[h, g, T2, d] L.
+#h #g #G #L #T1 #T2 #H elim H -G -L -T1 -T2 //
+[ #I #G #L #K #V1 #V2 #W2 #i #HLK #_ #HVW2 #IHV12 #d #HL #H
+ elim (ylt_split i d) #Hdi [ -H | -HL ]
+ [ <(ymax_pre_sn d (⫯i)) /2 width=1 by ylt_fwd_le_succ/
+ elim (lcosx_ldrop_trans_lt … HL … HLK) // -HL -Hdi
+ lapply (ldrop_fwd_drop2 … HLK) -HLK /3 width=7 by lsx_lift_ge/
+ | lapply (lsx_fwd_lref_be … H … HLK) // -H -Hdi
+ lapply (ldrop_fwd_drop2 … HLK) -HLK
+ /4 width=10 by lsx_ge, lsx_lift_le/
+ ]
+| #a #I #G #L #V1 #V2 #T1 #T2 #_ #_ #IHV12 #IHT12 #d #HL #H
+ elim (lsx_inv_bind … H) -H #HV1 #HT1
+ @lsx_bind /2 width=2 by/ (**) (* explicit constructor *)
+ @(lsx_leq_conf … (L.ⓑ{I}V1)) /3 width=1 by lcosx_pair, leq_succ/
+| #I #G #L #V1 #V2 #T1 #T2 #_ #_ #IHV12 #IHT12 #d #HL #H
+ elim (lsx_inv_flat … H) -H /3 width=1 by lsx_flat/
+| #G #L #V #U1 #U2 #T2 #_ #HTU2 #IHU12 #d #HL #H
+ elim (lsx_inv_bind … H) -H
+ /4 width=9 by lcosx_pair, lsx_inv_lift_ge, ldrop_drop/
+| #G #L #V #T1 #T2 #_ #IHT12 #d #HL #H
+ elim (lsx_inv_flat … H) -H /2 width=1 by/
+| #G #L #V1 #V2 #T #_ #IHV12 #d #HL #H
+ elim (lsx_inv_flat … H) -H /2 width=1 by/
+| #a #G #L #V1 #V2 #W1 #W2 #T1 #T2 #_ #_ #_ #IHV12 #IHW12 #IHT12 #d #HL #H
+ elim (lsx_inv_flat … H) -H #HV1 #H
+ elim (lsx_inv_bind … H) -H #HW1 #HT1
+ @lsx_bind /3 width=1 by lsx_flat/ (**) (* explicit constructor *)
+ @(lsx_leq_conf … (L.ⓛW1)) /3 width=1 by lcosx_pair, leq_succ/
+| #a #G #L #V1 #V2 #U2 #W1 #W2 #T1 #T2 #_ #HVU2 #_ #_ #IHV12 #IHW12 #IHT12 #d #HL #H
+ elim (lsx_inv_flat … H) -H #HV1 #H
+ elim (lsx_inv_bind … H) -H #HW1 #HT1
+ @lsx_bind /2 width=1 by/ (**) (* explicit constructor *)
+ @lsx_flat [ /3 width=7 by lsx_lift_ge, ldrop_drop/ ]
+ @(lsx_leq_conf … (L.ⓓW1)) /3 width=1 by lcosx_pair, leq_succ/
+]
+qed-.
+
+lemma lsx_cpx_trans_O: ∀h,g,G,L,T1,T2. ⦃G, L⦄ ⊢ T1 ➡[h, g] T2 →
+ G ⊢ ⬊*[h, g, T1, 0] L → G ⊢ ⬊*[h, g, T2, 0] L.
+/2 width=3 by lsx_cpx_trans_lcosx/ qed-.
--- /dev/null
+(**************************************************************************)
+(* ___ *)
+(* ||M|| *)
+(* ||A|| A project by Andrea Asperti *)
+(* ||T|| *)
+(* ||I|| Developers: *)
+(* ||T|| The HELM team. *)
+(* ||A|| http://helm.cs.unibo.it *)
+(* \ / *)
+(* \ / This file is distributed under the terms of the *)
+(* v GNU General Public License Version 2 *)
+(* *)
+(**************************************************************************)
+
+include "basic_2/notation/relations/sn_6.ma".
+include "basic_2/substitution/lleq.ma".
+include "basic_2/reduction/lpx.ma".
+
+(* SN EXTENDED STRONGLY NORMALIZING LOCAL ENVIRONMENTS **********************)
+
+definition lsx: ∀h. sd h → relation4 ynat term genv lenv ≝
+ λh,g,d,T,G. SN … (lpx h g G) (lleq d T).
+
+interpretation
+ "extended strong normalization (local environment)"
+ 'SN h g d T G L = (lsx h g T d G L).
+
+(* Basic eliminators ********************************************************)
+
+lemma lsx_ind: ∀h,g,G,T,d. ∀R:predicate lenv.
+ (∀L1. G ⊢ ⬊*[h, g, T, d] L1 →
+ (∀L2. ⦃G, L1⦄ ⊢ ➡[h, g] L2 → (L1 ⋕[T, d] L2 → ⊥) → R L2) →
+ R L1
+ ) →
+ ∀L. G ⊢ ⬊*[h, g, T, d] L → R L.
+#h #g #G #T #d #R #H0 #L1 #H elim H -L1
+/5 width=1 by lleq_sym, SN_intro/
+qed-.
+
+(* Basic properties *********************************************************)
+
+lemma lsx_intro: ∀h,g,G,L1,T,d.
+ (∀L2. ⦃G, L1⦄ ⊢ ➡[h, g] L2 → (L1 ⋕[T, d] L2 → ⊥) → G ⊢ ⬊*[h, g, T, d] L2) →
+ G ⊢ ⬊*[h, g, T, d] L1.
+/5 width=1 by lleq_sym, SN_intro/ qed.
+
+lemma lsx_atom: ∀h,g,G,T,d. G ⊢ ⬊*[h, g, T, d] ⋆.
+#h #g #G #T #d @lsx_intro
+#X #H #HT lapply (lpx_inv_atom1 … H) -H
+#H destruct elim HT -HT //
+qed.
+
+lemma lsx_sort: ∀h,g,G,L,d,k. G ⊢ ⬊*[h, g, ⋆k, d] L.
+#h #g #G #L1 #d #k @lsx_intro
+#L2 #HL12 #H elim H -H
+/3 width=4 by lpx_fwd_length, lleq_sort/
+qed.
+
+lemma lsx_gref: ∀h,g,G,L,d,p. G ⊢ ⬊*[h, g, §p, d] L.
+#h #g #G #L1 #d #p @lsx_intro
+#L2 #HL12 #H elim H -H
+/3 width=4 by lpx_fwd_length, lleq_gref/
+qed.
+
+lemma lsx_ge_up: ∀h,g,G,L,T,U,dt,d,e. dt ≤ yinj d + yinj e →
+ ⇧[d, e] T ≡ U → G ⊢ ⬊*[h, g, U, dt] L → G ⊢ ⬊*[h, g, U, d] L.
+#h #g #G #L #T #U #dt #d #e #Hdtde #HTU #H @(lsx_ind … H) -L
+/5 width=7 by lsx_intro, lleq_ge_up/
+qed-.
+
+lemma lsx_ge: ∀h,g,G,L,T,d1,d2. d1 ≤ d2 →
+ G ⊢ ⬊*[h, g, T, d1] L → G ⊢ ⬊*[h, g, T, d2] L.
+#h #g #G #L #T #d1 #d2 #Hd12 #H @(lsx_ind … H) -L
+/5 width=7 by lsx_intro, lleq_ge/
+qed-.
+
+(* Basic forward lemmas *****************************************************)
+
+lemma lsx_fwd_bind_sn: ∀h,g,a,I,G,L,V,T,d. G ⊢ ⬊*[h, g, ⓑ{a,I}V.T, d] L →
+ G ⊢ ⬊*[h, g, V, d] L.
+#h #g #a #I #G #L #V #T #d #H @(lsx_ind … H) -L
+#L1 #_ #IHL1 @lsx_intro
+#L2 #HL12 #HV @IHL1 /3 width=4 by lleq_fwd_bind_sn/
+qed-.
+
+lemma lsx_fwd_flat_sn: ∀h,g,I,G,L,V,T,d. G ⊢ ⬊*[h, g, ⓕ{I}V.T, d] L →
+ G ⊢ ⬊*[h, g, V, d] L.
+#h #g #I #G #L #V #T #d #H @(lsx_ind … H) -L
+#L1 #_ #IHL1 @lsx_intro
+#L2 #HL12 #HV @IHL1 /3 width=3 by lleq_fwd_flat_sn/
+qed-.
+
+lemma lsx_fwd_flat_dx: ∀h,g,I,G,L,V,T,d. G ⊢ ⬊*[h, g, ⓕ{I}V.T, d] L →
+ G ⊢ ⬊*[h, g, T, d] L.
+#h #g #I #G #L #V #T #d #H @(lsx_ind … H) -L
+#L1 #_ #IHL1 @lsx_intro
+#L2 #HL12 #HV @IHL1 /3 width=3 by lleq_fwd_flat_dx/
+qed-.
+
+lemma lsx_fwd_pair_sn: ∀h,g,I,G,L,V,T,d. G ⊢ ⬊*[h, g, ②{I}V.T, d] L →
+ G ⊢ ⬊*[h, g, V, d] L.
+#h #g * /2 width=4 by lsx_fwd_bind_sn, lsx_fwd_flat_sn/
+qed-.
+
+(* Basic inversion lemmas ***************************************************)
+
+lemma lsx_inv_flat: ∀h,g,I,G,L,V,T,d. G ⊢ ⬊*[h, g, ⓕ{I}V.T, d] L →
+ G ⊢ ⬊*[h, g, V, d] L ∧ G ⊢ ⬊*[h, g, T, d] L.
+/3 width=3 by lsx_fwd_flat_sn, lsx_fwd_flat_dx, conj/ qed-.
--- /dev/null
+(**************************************************************************)
+(* ___ *)
+(* ||M|| *)
+(* ||A|| A project by Andrea Asperti *)
+(* ||T|| *)
+(* ||I|| Developers: *)
+(* ||T|| The HELM team. *)
+(* ||A|| http://helm.cs.unibo.it *)
+(* \ / *)
+(* \ / This file is distributed under the terms of the *)
+(* v GNU General Public License Version 2 *)
+(* *)
+(**************************************************************************)
+
+include "basic_2/notation/relations/snalt_6.ma".
+include "basic_2/substitution/lleq_lleq.ma".
+include "basic_2/computation/lpxs_lleq.ma".
+include "basic_2/computation/lsx.ma".
+
+(* SN EXTENDED STRONGLY NORMALIZING LOCAL ENVIRONMENTS **********************)
+
+(* alternative definition of lsx *)
+definition lsxa: ∀h. sd h → relation4 ynat term genv lenv ≝
+ λh,g,d,T,G. SN … (lpxs h g G) (lleq d T).
+
+interpretation
+ "extended strong normalization (local environment) alternative"
+ 'SNAlt h g d T G L = (lsxa h g T d G L).
+
+(* Basic eliminators ********************************************************)
+
+lemma lsxa_ind: ∀h,g,G,T,d. ∀R:predicate lenv.
+ (∀L1. G ⊢ ⬊⬊*[h, g, T, d] L1 →
+ (∀L2. ⦃G, L1⦄ ⊢ ➡*[h, g] L2 → (L1 ⋕[T, d] L2 → ⊥) → R L2) →
+ R L1
+ ) →
+ ∀L. G ⊢ ⬊⬊*[h, g, T, d] L → R L.
+#h #g #G #T #d #R #H0 #L1 #H elim H -L1
+/5 width=1 by lleq_sym, SN_intro/
+qed-.
+
+(* Basic properties *********************************************************)
+
+lemma lsxa_intro: ∀h,g,G,L1,T,d.
+ (∀L2. ⦃G, L1⦄ ⊢ ➡*[h, g] L2 → (L1 ⋕[T, d] L2 → ⊥) → G ⊢ ⬊⬊*[h, g, T, d] L2) →
+ G ⊢ ⬊⬊*[h, g, T, d] L1.
+/5 width=1 by lleq_sym, SN_intro/ qed.
+
+fact lsxa_intro_aux: ∀h,g,G,L1,T,d.
+ (∀L,L2. ⦃G, L⦄ ⊢ ➡*[h, g] L2 → L1 ⋕[T, d] L → (L1 ⋕[T, d] L2 → ⊥) → G ⊢ ⬊⬊*[h, g, T, d] L2) →
+ G ⊢ ⬊⬊*[h, g, T, d] L1.
+/4 width=3 by lsxa_intro/ qed-.
+
+lemma lsxa_lleq_trans: ∀h,g,T,G,L1,d. G ⊢ ⬊⬊*[h, g, T, d] L1 →
+ ∀L2. L1 ⋕[T, d] L2 → G ⊢ ⬊⬊*[h, g, T, d] L2.
+#h #g #T #G #L1 #d #H @(lsxa_ind … H) -L1
+#L1 #_ #IHL1 #L2 #HL12 @lsxa_intro
+#K2 #HLK2 #HnLK2 elim (lleq_lpxs_trans … HLK2 … HL12) -HLK2
+/5 width=4 by lleq_canc_sn, lleq_trans/
+qed-.
+
+lemma lsxa_lpxs_trans: ∀h,g,T,G,L1,d. G ⊢ ⬊⬊*[h, g, T, d] L1 →
+ ∀L2. ⦃G, L1⦄ ⊢ ➡*[h, g] L2 → G ⊢ ⬊⬊*[h, g, T, d] L2.
+#h #g #T #G #L1 #d #H @(lsxa_ind … H) -L1 #L1 #HL1 #IHL1 #L2 #HL12
+elim (lleq_dec T L1 L2 d) /3 width=4 by lsxa_lleq_trans/
+qed-.
+
+lemma lsxa_intro_lpx: ∀h,g,G,L1,T,d.
+ (∀L2. ⦃G, L1⦄ ⊢ ➡[h, g] L2 → (L1 ⋕[T, d] L2 → ⊥) → G ⊢ ⬊⬊*[h, g, T, d] L2) →
+ G ⊢ ⬊⬊*[h, g, T, d] L1.
+#h #g #G #L1 #T #d #IH @lsxa_intro_aux
+#L #L2 #H @(lpxs_ind_dx … H) -L
+[ #H destruct #H elim H //
+| #L0 #L elim (lleq_dec T L1 L d) /3 width=1 by/
+ #HnT #HL0 #HL2 #_ #HT #_ elim (lleq_lpx_trans … HL0 … HT) -L0
+ #L0 #HL10 #HL0 @(lsxa_lpxs_trans … HL2) -HL2
+ /5 width=3 by lsxa_lleq_trans, lleq_trans/
+]
+qed-.
+
+(* Main properties **********************************************************)
+
+theorem lsx_lsxa: ∀h,g,G,L,T,d. G ⊢ ⬊*[h, g, T, d] L → G ⊢ ⬊⬊*[h, g, T, d] L.
+#h #g #G #L #T #d #H @(lsx_ind … H) -L
+/4 width=1 by lsxa_intro_lpx/
+qed.
+
+(* Main inversion lemmas ****************************************************)
+
+theorem lsxa_inv_lsx: ∀h,g,G,L,T,d. G ⊢ ⬊⬊*[h, g, T, d] L → G ⊢ ⬊*[h, g, T, d] L.
+#h #g #G #L #T #d #H @(lsxa_ind … H) -L
+/4 width=1 by lsx_intro, lpx_lpxs/
+qed-.
+
+(* Advanced properties ******************************************************)
+
+lemma lsx_intro_alt: ∀h,g,G,L1,T,d.
+ (∀L2. ⦃G, L1⦄ ⊢ ➡*[h, g] L2 → (L1 ⋕[T, d] L2 → ⊥) → G ⊢ ⬊*[h, g, T, d] L2) →
+ G ⊢ ⬊*[h, g, T, d] L1.
+/6 width=1 by lsxa_inv_lsx, lsx_lsxa, lsxa_intro/ qed.
+
+lemma lsx_lpxs_trans: ∀h,g,G,L1,T,d. G ⊢ ⬊*[h, g, T, d] L1 →
+ ∀L2. ⦃G, L1⦄ ⊢ ➡*[h, g] L2 → G ⊢ ⬊*[h, g, T, d] L2.
+/4 width=3 by lsxa_inv_lsx, lsx_lsxa, lsxa_lpxs_trans/ qed-.
+
+(* Advanced eliminators *****************************************************)
+
+lemma lsx_ind_alt: ∀h,g,G,T,d. ∀R:predicate lenv.
+ (∀L1. G ⊢ ⬊*[h, g, T, d] L1 →
+ (∀L2. ⦃G, L1⦄ ⊢ ➡*[h, g] L2 → (L1 ⋕[T, d] L2 → ⊥) → R L2) →
+ R L1
+ ) →
+ ∀L. G ⊢ ⬊*[h, g, T, d] L → R L.
+#h #g #G #T #d #R #IH #L #H @(lsxa_ind h g G T d … L)
+/4 width=1 by lsxa_inv_lsx, lsx_lsxa/
+qed-.
--- /dev/null
+(**************************************************************************)
+(* ___ *)
+(* ||M|| *)
+(* ||A|| A project by Andrea Asperti *)
+(* ||T|| *)
+(* ||I|| Developers: *)
+(* ||T|| The HELM team. *)
+(* ||A|| http://helm.cs.unibo.it *)
+(* \ / *)
+(* \ / This file is distributed under the terms of the *)
+(* v GNU General Public License Version 2 *)
+(* *)
+(**************************************************************************)
+
+include "basic_2/computation/csx_lpxs.ma".
+include "basic_2/computation/lcosx_cpx.ma".
+
+(* SN EXTENDED STRONGLY NORMALIZING LOCAL ENVIRONMENTS **********************)
+
+(* Advanced properties ******************************************************)
+
+lemma lsx_lref_be_lpxs: ∀h,g,I,G,K1,V,i,d. d ≤ yinj i → ⦃G, K1⦄ ⊢ ⬊*[h, g] V →
+ ∀K2. G ⊢ ⬊*[h, g, V, 0] K2 → ⦃G, K1⦄ ⊢ ➡*[h, g] K2 →
+ ∀L2. ⇩[i] L2 ≡ K2.ⓑ{I}V → G ⊢ ⬊*[h, g, #i, d] L2.
+#h #g #I #G #K1 #V #i #d #Hdi #H @(csx_ind_alt … H) -V
+#V0 #_ #IHV0 #K2 #H @(lsx_ind … H) -K2
+#K0 #HK0 #IHK0 #HK10 #L0 #HLK0 @lsx_intro
+#L2 #HL02 #HnL02 elim (lpx_ldrop_conf … HLK0 … HL02) -HL02
+#Y #H #HLK2 elim (lpx_inv_pair1 … H) -H
+#K2 #V2 #HK02 #HV02 #H destruct
+elim (eq_term_dec V0 V2) #HnV02 destruct [ -IHV0 -HV02 -HK0 | -IHK0 -HnL02 -HLK0 ]
+[ /4 width=8 by lpxs_strap1, lleq_lref/
+| @(IHV0 … HnV02 … HLK2) -IHV0 -HnV02 -HLK2
+ /3 width=4 by lsx_cpx_trans_O, lsx_lpx_trans, lpxs_cpx_trans, lpxs_strap1/ (**) (* full auto too slow *)
+]
+qed.
+
+lemma lsx_lref_be: ∀h,g,I,G,K,V,i,d. d ≤ yinj i → ⦃G, K⦄ ⊢ ⬊*[h, g] V →
+ G ⊢ ⬊*[h, g, V, 0] K →
+ ∀L. ⇩[i] L ≡ K.ⓑ{I}V → G ⊢ ⬊*[h, g, #i, d] L.
+/2 width=8 by lsx_lref_be_lpxs/ qed.
+
+(* Main properties **********************************************************)
+
+theorem csx_lsx: ∀h,g,G,L,T. ⦃G, L⦄ ⊢ ⬊*[h, g] T → ∀d. G ⊢ ⬊*[h, g, T, d] L.
+#h #g #G #L #T @(fqup_wf_ind_eq … G L T) -G -L -T
+#Z #Y #X #IH #G #L * * //
+[ #i #HG #HL #HT #H #d destruct
+ elim (lt_or_ge i (|L|)) /2 width=1 by lsx_lref_free/
+ elim (ylt_split i d) /2 width=1 by lsx_lref_skip/
+ #Hdi #Hi elim (ldrop_O1_lt … Hi) -Hi
+ #I #K #V #HLK lapply (csx_inv_lref_bind … HLK … H) -H
+ /4 width=6 by lsx_lref_be, fqup_lref/
+| #a #I #V #T #HG #HL #HT #H #d destruct
+ elim (csx_fwd_bind … H) -H /3 width=1 by lsx_bind/
+| #I #V #T #HG #HL #HT #H #d destruct
+ elim (csx_fwd_flat … H) -H /3 width=1 by lsx_flat/
+]
+qed.
--- /dev/null
+(**************************************************************************)
+(* ___ *)
+(* ||M|| *)
+(* ||A|| A project by Andrea Asperti *)
+(* ||T|| *)
+(* ||I|| Developers: *)
+(* ||T|| The HELM team. *)
+(* ||A|| http://helm.cs.unibo.it *)
+(* \ / *)
+(* \ / This file is distributed under the terms of the *)
+(* v GNU General Public License Version 2 *)
+(* *)
+(**************************************************************************)
+
+include "basic_2/substitution/lleq_ldrop.ma".
+include "basic_2/reduction/lpx_ldrop.ma".
+include "basic_2/computation/lsx.ma".
+
+(* SN EXTENDED STRONGLY NORMALIZING LOCAL ENVIRONMENTS **********************)
+
+(* Advanced properties ******************************************************)
+
+lemma lsx_lref_free: ∀h,g,G,L,d,i. |L| ≤ i → G ⊢ ⬊*[h, g, #i, d] L.
+#h #g #G #L1 #d #i #HL1 @lsx_intro
+#L2 #HL12 #H elim H -H
+/4 width=6 by lpx_fwd_length, lleq_free, le_repl_sn_conf_aux/
+qed.
+
+lemma lsx_lref_skip: ∀h,g,G,L,d,i. yinj i < d → G ⊢ ⬊*[h, g, #i, d] L.
+#h #g #G #L1 #d #i #HL1 @lsx_intro
+#L2 #HL12 #H elim H -H
+/3 width=4 by lpx_fwd_length, lleq_skip/
+qed.
+
+(* Advanced forward lemmas **************************************************)
+
+lemma lsx_fwd_lref_be: ∀h,g,I,G,L,d,i. d ≤ yinj i → G ⊢ ⬊*[h, g, #i, d] L →
+ ∀K,V. ⇩[i] L ≡ K.ⓑ{I}V → G ⊢ ⬊*[h, g, V, 0] K.
+#h #g #I #G #L #d #i #Hdi #H @(lsx_ind … H) -L
+#L1 #_ #IHL1 #K1 #V #HLK1 @lsx_intro
+#K2 #HK12 #HnK12 lapply (ldrop_fwd_drop2 … HLK1)
+#H2LK1 elim (ldrop_lpx_trans … H2LK1 … HK12) -H2LK1 -HK12
+#L2 #HL12 #H2LK2 #H elim (leq_ldrop_conf_be … H … HLK1) -H /2 width=1 by ylt_inj/
+#Y #_ #HLK2 lapply (ldrop_fwd_drop2 … HLK2)
+#HY lapply (ldrop_mono … HY … H2LK2) -HY -H2LK2 #H destruct
+/4 width=10 by lleq_inv_lref_ge/
+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 (lpx_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 (lpx_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_lpx_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_lpx_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_lpx_trans … HLK1 … HK12) -HK12
+/4 width=9 by lleq_inv_lift_ge/
+qed-.
--- /dev/null
+(**************************************************************************)
+(* ___ *)
+(* ||M|| *)
+(* ||A|| A project by Andrea Asperti *)
+(* ||T|| *)
+(* ||I|| Developers: *)
+(* ||T|| The HELM team. *)
+(* ||A|| http://helm.cs.unibo.it *)
+(* \ / *)
+(* \ / This file is distributed under the terms of the *)
+(* v GNU General Public License Version 2 *)
+(* *)
+(**************************************************************************)
+
+include "basic_2/substitution/lleq_lleq.ma".
+include "basic_2/reduction/lpx_lleq.ma".
+include "basic_2/computation/lsx.ma".
+
+(* SN EXTENDED STRONGLY NORMALIZING LOCAL ENVIRONMENTS **********************)
+
+(* Advanced properties ******************************************************)
+
+lemma lsx_lleq_trans: ∀h,g,T,G,L1,d. G ⊢ ⬊*[h, g, T, d] L1 →
+ ∀L2. L1 ⋕[T, d] L2 → G ⊢ ⬊*[h, g, T, d] L2.
+#h #g #T #G #L1 #d #H @(lsx_ind … H) -L1
+#L1 #_ #IHL1 #L2 #HL12 @lsx_intro
+#K2 #HLK2 #HnLK2 elim (lleq_lpx_trans … HLK2 … HL12) -HLK2
+/5 width=4 by lleq_canc_sn, lleq_trans/
+qed-.
+
+lemma lsx_lpx_trans: ∀h,g,T,G,L1,d. G ⊢ ⬊*[h, g, T, d] L1 →
+ ∀L2. ⦃G, L1⦄ ⊢ ➡[h, g] L2 → G ⊢ ⬊*[h, g, T, d] L2.
+#h #g #T #G #L1 #d #H @(lsx_ind … H) -L1 #L1 #HL1 #IHL1 #L2 #HL12
+elim (lleq_dec T L1 L2 d) /3 width=4 by lsx_lleq_trans/
+qed-.
+
+lemma lsx_leq_conf: ∀h,g,G,L1,T,d. G ⊢ ⬊*[h, g, T, d] L1 →
+ ∀L2. L1 ≃[d, ∞] L2 → G ⊢ ⬊*[h, g, T, d] L2.
+#h #g #G #L1 #T #d #H @(lsx_ind … H) -L1
+#L1 #_ #IHL1 #L2 #HL12 @lsx_intro
+#L3 #HL23 #HnL23 elim (leq_lpx_trans_lleq … HL12 … HL23) -HL12 -HL23
+#L0 #HL03 #HL10 #H elim (H T) -H /4 width=4 by/
+qed-.
+
+(* Advanced forward lemmas **************************************************)
+
+lemma lsx_fwd_bind_dx: ∀h,g,a,I,G,L,V,T,d. G ⊢ ⬊*[h, g, ⓑ{a,I}V.T, d] L →
+ G ⊢ ⬊*[h, g, T, ⫯d] L.ⓑ{I}V.
+#h #g #a #I #G #L #V1 #T #d #H @(lsx_ind … H) -L
+#L1 #_ #IHL1 @lsx_intro
+#Y #H #HT elim (lpx_inv_pair1 … H) -H
+#L2 #V2 #HL12 #_ #H destruct
+@(lsx_leq_conf … (L2.ⓑ{I}V1)) /2 width=1 by leq_succ/
+@IHL1 // #H @HT -IHL1 -HL12 -HT
+@(lleq_leq_trans … (L2.ⓑ{I}V1))
+/2 width=2 by lleq_fwd_bind_dx, leq_succ/
+qed-.
+
+(* Advanced inversion lemmas ************************************************)
+
+lemma lsx_inv_bind: ∀h,g,a,I,G,L,V,T,d. G ⊢ ⬊*[h, g, ⓑ{a, I}V.T, d] L →
+ G ⊢ ⬊*[h, g, V, d] L ∧ G ⊢ ⬊*[h, g, T, ⫯d] L.ⓑ{I}V.
+/3 width=4 by lsx_fwd_bind_sn, lsx_fwd_bind_dx, conj/ qed-.
--- /dev/null
+(**************************************************************************)
+(* ___ *)
+(* ||M|| *)
+(* ||A|| A project by Andrea Asperti *)
+(* ||T|| *)
+(* ||I|| Developers: *)
+(* ||T|| The HELM team. *)
+(* ||A|| http://helm.cs.unibo.it *)
+(* \ / *)
+(* \ / This file is distributed under the terms of the *)
+(* v GNU General Public License Version 2 *)
+(* *)
+(**************************************************************************)
+
+include "basic_2/computation/lpxs_lpxs.ma".
+include "basic_2/computation/lsx_alt.ma".
+
+(* SN EXTENDED STRONGLY NORMALIZING LOCAL ENVIRONMENTS **********************)
+
+(* Advanced properties ******************************************************)
+
+fact lsx_bind_lpxs_aux: ∀h,g,a,I,G,L1,V,d. G ⊢ ⬊*[h, g, V, d] L1 →
+ ∀Y,T. G ⊢ ⬊*[h, g, T, ⫯d] Y →
+ ∀L2. Y = L2.ⓑ{I}V → ⦃G, L1⦄ ⊢ ➡*[h, g] L2 →
+ G ⊢ ⬊*[h, g, ⓑ{a,I}V.T, d] L2.
+#h #g #a #I #G #L1 #V #d #H @(lsx_ind_alt … H) -L1
+#L1 #HL1 #IHL1 #Y #T #H @(lsx_ind_alt … H) -Y
+#Y #HY #IHY #L2 #H #HL12 destruct @lsx_intro_alt
+#L0 #HL20 lapply (lpxs_trans … HL12 … HL20)
+#HL10 #H elim (nlleq_inv_bind … H) -H [ -HL1 -IHY | -HY -IHL1 ]
+[ #HnV elim (lleq_dec V L1 L2 d)
+ [ #HV @(IHL1 … L0) /3 width=5 by lsx_lpxs_trans, lpxs_pair, lleq_canc_sn/ (**) (* full auto too slow *)
+ | -HnV -HL10 /4 width=5 by lsx_lpxs_trans, lpxs_pair/
+ ]
+| /3 width=4 by lpxs_pair/
+]
+qed-.
+
+lemma lsx_bind: ∀h,g,a,I,G,L,V,d. G ⊢ ⬊*[h, g, V, d] L →
+ ∀T. G ⊢ ⬊*[h, g, T, ⫯d] L.ⓑ{I}V →
+ G ⊢ ⬊*[h, g, ⓑ{a,I}V.T, d] L.
+/2 width=3 by lsx_bind_lpxs_aux/ qed.
+
+lemma lsx_flat_lpxs: ∀h,g,I,G,L1,V,d. G ⊢ ⬊*[h, g, V, d] L1 →
+ ∀L2,T. G ⊢ ⬊*[h, g, T, d] L2 → ⦃G, L1⦄ ⊢ ➡*[h, g] L2 →
+ G ⊢ ⬊*[h, g, ⓕ{I}V.T, d] L2.
+#h #g #I #G #L1 #V #d #H @(lsx_ind_alt … H) -L1
+#L1 #HL1 #IHL1 #L2 #T #H @(lsx_ind_alt … H) -L2
+#L2 #HL2 #IHL2 #HL12 @lsx_intro_alt
+#L0 #HL20 lapply (lpxs_trans … HL12 … HL20)
+#HL10 #H elim (nlleq_inv_flat … H) -H [ -HL1 -IHL2 | -HL2 -IHL1 ]
+[ #HnV elim (lleq_dec V L1 L2 d)
+ [ #HV @(IHL1 … L0) /3 width=3 by lsx_lpxs_trans, lleq_canc_sn/ (**) (* full auto too slow: 47s *)
+ | -HnV -HL10 /3 width=4 by lsx_lpxs_trans/
+ ]
+| /3 width=1 by/
+]
+qed-.
+
+lemma lsx_flat: ∀h,g,I,G,L,V,d. G ⊢ ⬊*[h, g, V, d] L →
+ ∀T. G ⊢ ⬊*[h, g, T, d] L → G ⊢ ⬊*[h, g, ⓕ{I}V.T, d] L.
+/2 width=3 by lsx_flat_lpxs/ qed.
+++ /dev/null
-(**************************************************************************)
-(* ___ *)
-(* ||M|| *)
-(* ||A|| A project by Andrea Asperti *)
-(* ||T|| *)
-(* ||I|| Developers: *)
-(* ||T|| The HELM team. *)
-(* ||A|| http://helm.cs.unibo.it *)
-(* \ / *)
-(* \ / This file is distributed under the terms of the *)
-(* v GNU General Public License Version 2 *)
-(* *)
-(**************************************************************************)
-
-include "basic_2/notation/relations/lazycosn_5.ma".
-include "basic_2/computation/lsx.ma".
-
-(* SN EXTENDED STRONGLY CONORMALIZING LOCAL ENVIRONMENTS ********************)
-
-inductive lcosx (h) (g) (G): relation2 ynat lenv ≝
-| lcosx_sort: ∀d. lcosx h g G d (⋆)
-| lcosx_skip: ∀I,L,T. lcosx h g G 0 L → lcosx h g G 0 (L.ⓑ{I}T)
-| lcosx_pair: ∀I,L,T,d. G ⊢ ⋕⬊*[h, g, T, d] L →
- lcosx h g G d L → lcosx h g G (⫯d) (L.ⓑ{I}T)
-.
-
-interpretation
- "sn extended strong conormalization (local environment)"
- 'LazyCoSN h g d G L = (lcosx h g G d L).
-
-(* Basic properties *********************************************************)
-
-lemma lcosx_O: ∀h,g,G,L. G ⊢ ⧤⬊*[h, g, 0] L.
-#h #g #G #L elim L /2 width=1 by lcosx_skip/
-qed.
-
-lemma lcosx_ldrop_trans_lt: ∀h,g,G,L,d. G ⊢ ⧤⬊*[h, g, d] L →
- ∀I,K,V,i. ⇩[i] L ≡ K.ⓑ{I}V → i < d →
- G ⊢ ⧤⬊*[h, g, ⫰(d-i)] K ∧ G ⊢ ⋕⬊*[h, g, V, ⫰(d-i)] K.
-#h #g #G #L #d #H elim H -L -d
-[ #d #J #K #V #i #H elim (ldrop_inv_atom1 … H) -H #H destruct
-| #I #L #T #_ #_ #J #K #V #i #_ #H elim (ylt_yle_false … H) -H //
-| #I #L #T #d #HT #HL #IHL #J #K #V #i #H #Hid
- elim (ldrop_inv_O1_pair1 … H) -H * #Hi #HLK destruct
- [ >ypred_succ /2 width=1 by conj/
- | lapply (ylt_pred … Hid ?) -Hid /2 width=1 by ylt_inj/ >ypred_succ #Hid
- elim (IHL … HLK ?) -IHL -HLK <yminus_inj >yminus_SO2 //
- <(ypred_succ d) in ⊢ (%→%→?); >yminus_pred /2 width=1 by ylt_inj, conj/
- ]
-]
-qed-.
-
-(* Basic inversion lemmas ***************************************************)
-
-fact lcosx_inv_succ_aux: ∀h,g,G,L,x. G ⊢ ⧤⬊*[h, g, x] L → ∀d. x = ⫯d →
- L = ⋆ ∨
- ∃∃I,K,V. L = K.ⓑ{I}V & G ⊢ ⧤⬊*[h, g, d] K &
- G ⊢ ⋕⬊*[h, g, V, d] K.
-#h #g #G #L #d * -L -d /2 width=1 by or_introl/
-[ #I #L #T #_ #x #H elim (ysucc_inv_O_sn … H)
-| #I #L #T #d #HT #HL #x #H <(ysucc_inj … H) -x
- /3 width=6 by ex3_3_intro, or_intror/
-]
-qed-.
-
-lemma lcosx_inv_succ: ∀h,g,G,L,d. G ⊢ ⧤⬊*[h, g, ⫯d] L → L = ⋆ ∨
- ∃∃I,K,V. L = K.ⓑ{I}V & G ⊢ ⧤⬊*[h, g, d] K &
- G ⊢ ⋕⬊*[h, g, V, d] K.
-/2 width=3 by lcosx_inv_succ_aux/ qed-.
-
-lemma lcosx_inv_pair: ∀h,g,I,G,L,T,d. G ⊢ ⧤⬊*[h, g, ⫯d] L.ⓑ{I}T →
- G ⊢ ⧤⬊*[h, g, d] L ∧ G ⊢ ⋕⬊*[h, g, T, d] L.
-#h #g #I #G #L #T #d #H elim (lcosx_inv_succ … H) -H
-[ #H destruct
-| * #Z #Y #X #H destruct /2 width=1 by conj/
-]
-qed-.
+++ /dev/null
-(**************************************************************************)
-(* ___ *)
-(* ||M|| *)
-(* ||A|| A project by Andrea Asperti *)
-(* ||T|| *)
-(* ||I|| Developers: *)
-(* ||T|| The HELM team. *)
-(* ||A|| http://helm.cs.unibo.it *)
-(* \ / *)
-(* \ / This file is distributed under the terms of the *)
-(* v GNU General Public License Version 2 *)
-(* *)
-(**************************************************************************)
-
-include "ground_2/ynat/ynat_max.ma".
-include "basic_2/computation/lsx_ldrop.ma".
-include "basic_2/computation/lsx_lpxs.ma".
-include "basic_2/computation/lcosx.ma".
-
-(* SN EXTENDED STRONGLY CONORMALIZING LOCAL ENVIRONMENTS ********************)
-
-(* Properties on extended context-sensitive parallel computation for term ***)
-
-lemma lsx_cpx_trans_lcosx: ∀h,g,G,L,T1,T2. ⦃G, L⦄ ⊢ T1 ➡[h, g] T2 →
- ∀d. G ⊢ ⧤⬊*[h, g, d] L →
- G ⊢ ⋕⬊*[h, g, T1, d] L → G ⊢ ⋕⬊*[h, g, T2, d] L.
-#h #g #G #L #T1 #T2 #H elim H -G -L -T1 -T2 //
-[ #I #G #L #K #V1 #V2 #W2 #i #HLK #_ #HVW2 #IHV12 #d #HL #H
- elim (ylt_split i d) #Hdi [ -H | -HL ]
- [ <(ymax_pre_sn d (⫯i)) /2 width=1 by ylt_fwd_le_succ/
- elim (lcosx_ldrop_trans_lt … HL … HLK) // -HL -Hdi
- lapply (ldrop_fwd_drop2 … HLK) -HLK /3 width=7 by lsx_lift_ge/
- | lapply (lsx_fwd_lref_be … H … HLK) // -H -Hdi
- lapply (ldrop_fwd_drop2 … HLK) -HLK
- /4 width=10 by lsx_ge, lsx_lift_le/
- ]
-| #a #I #G #L #V1 #V2 #T1 #T2 #_ #_ #IHV12 #IHT12 #d #HL #H
- elim (lsx_inv_bind … H) -H #HV1 #HT1
- @lsx_bind /2 width=2 by/ (**) (* explicit constructor *)
- @(lsx_leq_conf … (L.ⓑ{I}V1)) /3 width=1 by lcosx_pair, leq_succ/
-| #I #G #L #V1 #V2 #T1 #T2 #_ #_ #IHV12 #IHT12 #d #HL #H
- elim (lsx_inv_flat … H) -H /3 width=1 by lsx_flat/
-| #G #L #V #U1 #U2 #T2 #_ #HTU2 #IHU12 #d #HL #H
- elim (lsx_inv_bind … H) -H
- /4 width=9 by lcosx_pair, lsx_inv_lift_ge, ldrop_drop/
-| #G #L #V #T1 #T2 #_ #IHT12 #d #HL #H
- elim (lsx_inv_flat … H) -H /2 width=1 by/
-| #G #L #V1 #V2 #T #_ #IHV12 #d #HL #H
- elim (lsx_inv_flat … H) -H /2 width=1 by/
-| #a #G #L #V1 #V2 #W1 #W2 #T1 #T2 #_ #_ #_ #IHV12 #IHW12 #IHT12 #d #HL #H
- elim (lsx_inv_flat … H) -H #HV1 #H
- elim (lsx_inv_bind … H) -H #HW1 #HT1
- @lsx_bind /3 width=1 by lsx_flat/ (**) (* explicit constructor *)
- @(lsx_leq_conf … (L.ⓛW1)) /3 width=1 by lcosx_pair, leq_succ/
-| #a #G #L #V1 #V2 #U2 #W1 #W2 #T1 #T2 #_ #HVU2 #_ #_ #IHV12 #IHW12 #IHT12 #d #HL #H
- elim (lsx_inv_flat … H) -H #HV1 #H
- elim (lsx_inv_bind … H) -H #HW1 #HT1
- @lsx_bind /2 width=1 by/ (**) (* explicit constructor *)
- @lsx_flat [ /3 width=7 by lsx_lift_ge, ldrop_drop/ ]
- @(lsx_leq_conf … (L.ⓓW1)) /3 width=1 by lcosx_pair, leq_succ/
-]
-qed-.
-
-lemma lsx_cpx_trans_O: ∀h,g,G,L,T1,T2. ⦃G, L⦄ ⊢ T1 ➡[h, g] T2 →
- G ⊢ ⋕⬊*[h, g, T1, 0] L → G ⊢ ⋕⬊*[h, g, T2, 0] L.
-/2 width=3 by lsx_cpx_trans_lcosx/ qed-.
-
-lemma lsx_cpxs_trans_O: ∀h,g,G,L,T1,T2. ⦃G, L⦄ ⊢ T1 ➡*[h, g] T2 →
- G ⊢ ⋕⬊*[h, g, T1, 0] L → G ⊢ ⋕⬊*[h, g, T2, 0] L.
-#h #g #G #L #T1 #T2 #H @(cpxs_ind … H) -T2
-/3 width=3 by lsx_cpx_trans_O, cpxs_strap1/
-qed-.
+++ /dev/null
-(**************************************************************************)
-(* ___ *)
-(* ||M|| *)
-(* ||A|| A project by Andrea Asperti *)
-(* ||T|| *)
-(* ||I|| Developers: *)
-(* ||T|| The HELM team. *)
-(* ||A|| http://helm.cs.unibo.it *)
-(* \ / *)
-(* \ / This file is distributed under the terms of the *)
-(* v GNU General Public License Version 2 *)
-(* *)
-(**************************************************************************)
-
-include "basic_2/notation/relations/lazysn_6.ma".
-include "basic_2/relocation/lleq.ma".
-include "basic_2/computation/lpxs.ma".
-
-(* SN EXTENDED STRONGLY NORMALIZING LOCAL ENVIRONMENTS **********************)
-
-definition lsx: ∀h. sd h → relation4 ynat term genv lenv ≝
- λh,g,d,T,G. SN … (lpxs h g G) (lleq d T).
-
-interpretation
- "extended strong normalization (local environment)"
- 'LazySN h g d T G L = (lsx h g T d G L).
-
-(* Basic eliminators ********************************************************)
-
-lemma lsx_ind: ∀h,g,G,T,d. ∀R:predicate lenv.
- (∀L1. G ⊢ ⋕⬊*[h, g, T, d] L1 →
- (∀L2. ⦃G, L1⦄ ⊢ ➡*[h, g] L2 → (L1 ⋕[T, d] L2 → ⊥) → R L2) →
- R L1
- ) →
- ∀L. G ⊢ ⋕⬊*[h, g, T, d] L → R L.
-#h #g #G #T #d #R #H0 #L1 #H elim H -L1
-/5 width=1 by lleq_sym, SN_intro/
-qed-.
-
-(* Basic properties *********************************************************)
-
-lemma lsx_intro: ∀h,g,G,L1,T,d.
- (∀L2. ⦃G, L1⦄ ⊢ ➡*[h, g] L2 → (L1 ⋕[T, d] L2 → ⊥) → G ⊢ ⋕⬊*[h, g, T, d] L2) →
- G ⊢ ⋕⬊*[h, g, T, d] L1.
-/5 width=1 by lleq_sym, SN_intro/ qed.
-
-lemma lsx_atom: ∀h,g,G,T,d. G ⊢ ⋕⬊*[h, g, T, d] ⋆.
-#h #g #G #T #d @lsx_intro
-#X #H #HT lapply (lpxs_inv_atom1 … H) -H
-#H destruct elim HT -HT //
-qed.
-
-lemma lsx_sort: ∀h,g,G,L,d,k. G ⊢ ⋕⬊*[h, g, ⋆k, d] L.
-#h #g #G #L1 #d #k @lsx_intro
-#L2 #HL12 #H elim H -H
-/3 width=4 by lpxs_fwd_length, lleq_sort/
-qed.
-
-lemma lsx_gref: ∀h,g,G,L,d,p. G ⊢ ⋕⬊*[h, g, §p, d] L.
-#h #g #G #L1 #d #p @lsx_intro
-#L2 #HL12 #H elim H -H
-/3 width=4 by lpxs_fwd_length, lleq_gref/
-qed.
-
-lemma lsx_ge_up: ∀h,g,G,L,T,U,dt,d,e. dt ≤ yinj d + yinj e →
- ⇧[d, e] T ≡ U → G ⊢ ⋕⬊*[h, g, U, dt] L → G ⊢ ⋕⬊*[h, g, U, d] L.
-#h #g #G #L #T #U #dt #d #e #Hdtde #HTU #H @(lsx_ind … H) -L
-/5 width=7 by lsx_intro, lleq_ge_up/
-qed-.
-
-(* Basic forward lemmas *****************************************************)
-
-lemma lsx_fwd_bind_sn: ∀h,g,a,I,G,L,V,T,d. G ⊢ ⋕⬊*[h, g, ⓑ{a,I}V.T, d] L →
- G ⊢ ⋕⬊*[h, g, V, d] L.
-#h #g #a #I #G #L #V #T #d #H @(lsx_ind … H) -L
-#L1 #_ #IHL1 @lsx_intro
-#L2 #HL12 #HV @IHL1 /3 width=4 by lleq_fwd_bind_sn/
-qed-.
-
-lemma lsx_fwd_flat_sn: ∀h,g,I,G,L,V,T,d. G ⊢ ⋕⬊*[h, g, ⓕ{I}V.T, d] L →
- G ⊢ ⋕⬊*[h, g, V, d] L.
-#h #g #I #G #L #V #T #d #H @(lsx_ind … H) -L
-#L1 #_ #IHL1 @lsx_intro
-#L2 #HL12 #HV @IHL1 /3 width=3 by lleq_fwd_flat_sn/
-qed-.
-
-lemma lsx_fwd_flat_dx: ∀h,g,I,G,L,V,T,d. G ⊢ ⋕⬊*[h, g, ⓕ{I}V.T, d] L →
- G ⊢ ⋕⬊*[h, g, T, d] L.
-#h #g #I #G #L #V #T #d #H @(lsx_ind … H) -L
-#L1 #_ #IHL1 @lsx_intro
-#L2 #HL12 #HV @IHL1 /3 width=3 by lleq_fwd_flat_dx/
-qed-.
-
-lemma lsx_fwd_pair_sn: ∀h,g,I,G,L,V,T,d. G ⊢ ⋕⬊*[h, g, ②{I}V.T, d] L →
- G ⊢ ⋕⬊*[h, g, V, d] L.
-#h #g * /2 width=4 by lsx_fwd_bind_sn, lsx_fwd_flat_sn/
-qed-.
-
-(* Basic inversion lemmas ***************************************************)
-
-lemma lsx_inv_flat: ∀h,g,I,G,L,V,T,d. G ⊢ ⋕⬊*[h, g, ⓕ{I}V.T, d] L →
- G ⊢ ⋕⬊*[h, g, V, d] L ∧ G ⊢ ⋕⬊*[h, g, T, d] L.
-/3 width=3 by lsx_fwd_flat_sn, lsx_fwd_flat_dx, conj/ qed-.
+++ /dev/null
-(**************************************************************************)
-(* ___ *)
-(* ||M|| *)
-(* ||A|| A project by Andrea Asperti *)
-(* ||T|| *)
-(* ||I|| Developers: *)
-(* ||T|| The HELM team. *)
-(* ||A|| http://helm.cs.unibo.it *)
-(* \ / *)
-(* \ / This file is distributed under the terms of the *)
-(* v GNU General Public License Version 2 *)
-(* *)
-(**************************************************************************)
-
-include "basic_2/computation/csx_lpxs.ma".
-include "basic_2/computation/lcosx_cpxs.ma".
-
-(* SN EXTENDED STRONGLY NORMALIZING LOCAL ENVIRONMENTS **********************)
-
-(* Advanced properties ******************************************************)
-
-lemma lsx_lref_be_lpxs: ∀h,g,I,G,K1,V,i,d. d ≤ yinj i → ⦃G, K1⦄ ⊢ ⬊*[h, g] V →
- ∀K2. G ⊢ ⋕⬊*[h, g, V, 0] K2 → ⦃G, K1⦄ ⊢ ➡*[h, g] K2 →
- ∀L2. ⇩[i] L2 ≡ K2.ⓑ{I}V → G ⊢ ⋕⬊*[h, g, #i, d] L2.
-#h #g #I #G #K1 #V #i #d #Hdi #H @(csx_ind_alt … H) -V
-#V0 #_ #IHV0 #K2 #H @(lsx_ind … H) -K2
-#K0 #HK0 #IHK0 #HK10 #L0 #HLK0 @lsx_intro
-#L2 #HL02 #HnL02 elim (lpxs_ldrop_conf … HLK0 … HL02) -HL02
-#Y #H #HLK2 elim (lpxs_inv_pair1 … H) -H
-#K2 #V2 #HK02 #HV02 #H destruct
-lapply (lpxs_trans … HK10 … HK02) #HK12
-elim (eq_term_dec V0 V2) #HnV02 destruct [ -IHV0 -HV02 -HK0 -HK10 | -IHK0 -HnL02 -HLK0 ]
-[ /4 width=8 by lleq_lref/
-| @(IHV0 … HnV02 … HK12 … HLK2) -IHV0 -HnV02 -HK12 -HLK2
- /3 width=4 by lsx_cpxs_trans_O, lsx_lpxs_trans, lpxs_cpxs_trans/ (**) (* full auto too slow *)
-]
-qed.
-
-lemma lsx_lref_be: ∀h,g,I,G,K,V,i,d. d ≤ yinj i → ⦃G, K⦄ ⊢ ⬊*[h, g] V →
- G ⊢ ⋕⬊*[h, g, V, 0] K →
- ∀L. ⇩[i] L ≡ K.ⓑ{I}V → G ⊢ ⋕⬊*[h, g, #i, d] L.
-/2 width=8 by lsx_lref_be_lpxs/ qed.
-
-(* Main properties **********************************************************)
-
-theorem csx_lsx: ∀h,g,G,L,T. ⦃G, L⦄ ⊢ ⬊*[h, g] T → ∀d. G ⊢ ⋕⬊*[h, g, T, d] L.
-#h #g #G #L #T @(fqup_wf_ind_eq … G L T) -G -L -T
-#Z #Y #X #IH #G #L * * //
-[ #i #HG #HL #HT #H #d destruct
- elim (lt_or_ge i (|L|)) /2 width=1 by lsx_lref_free/
- elim (ylt_split i d) /2 width=1 by lsx_lref_skip/
- #Hdi #Hi elim (ldrop_O1_lt … Hi) -Hi
- #I #K #V #HLK lapply (csx_inv_lref_bind … HLK … H) -H
- /4 width=6 by lsx_lref_be, fqup_lref/
-| #a #I #V #T #HG #HL #HT #H #d destruct
- elim (csx_fwd_bind … H) -H /3 width=1 by lsx_bind/
-| #I #V #T #HG #HL #HT #H #d destruct
- elim (csx_fwd_flat … H) -H /3 width=1 by lsx_flat/
-]
-qed.
+++ /dev/null
-(**************************************************************************)
-(* ___ *)
-(* ||M|| *)
-(* ||A|| A project by Andrea Asperti *)
-(* ||T|| *)
-(* ||I|| Developers: *)
-(* ||T|| The HELM team. *)
-(* ||A|| http://helm.cs.unibo.it *)
-(* \ / *)
-(* \ / This file is distributed under the terms of the *)
-(* v GNU General Public License Version 2 *)
-(* *)
-(**************************************************************************)
-
-include "basic_2/relocation/lleq_ldrop.ma".
-include "basic_2/computation/lpxs_ldrop.ma".
-include "basic_2/computation/lsx.ma".
-
-(* SN EXTENDED STRONGLY NORMALIZING LOCAL ENVIRONMENTS **********************)
-
-(* Advanced properties ******************************************************)
-
-lemma lsx_lref_free: ∀h,g,G,L,d,i. |L| ≤ i → G ⊢ ⋕⬊*[h, g, #i, d] L.
-#h #g #G #L1 #d #i #HL1 @lsx_intro
-#L2 #HL12 #H elim H -H
-/4 width=6 by lpxs_fwd_length, lleq_free, le_repl_sn_conf_aux/
-qed.
-
-lemma lsx_lref_skip: ∀h,g,G,L,d,i. yinj i < d → G ⊢ ⋕⬊*[h, g, #i, d] L.
-#h #g #G #L1 #d #i #HL1 @lsx_intro
-#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-.
+++ /dev/null
-(**************************************************************************)
-(* ___ *)
-(* ||M|| *)
-(* ||A|| A project by Andrea Asperti *)
-(* ||T|| *)
-(* ||I|| Developers: *)
-(* ||T|| The HELM team. *)
-(* ||A|| http://helm.cs.unibo.it *)
-(* \ / *)
-(* \ / This file is distributed under the terms of the *)
-(* v GNU General Public License Version 2 *)
-(* *)
-(**************************************************************************)
-
-include "basic_2/relocation/lleq_lleq.ma".
-include "basic_2/computation/lpxs_lleq.ma".
-include "basic_2/computation/lpxs_lpxs.ma".
-include "basic_2/computation/lsx.ma".
-
-(* SN EXTENDED STRONGLY NORMALIZING LOCAL ENVIRONMENTS **********************)
-
-(* Advanced properties ******************************************************)
-
-lemma lsx_leq_conf: ∀h,g,G,L1,T,d. G ⊢ ⋕⬊*[h, g, T, d] L1 →
- ∀L2. L1 ≃[d, ∞] L2 → G ⊢ ⋕⬊*[h, g, T, d] L2.
-#h #g #G #L1 #T #d #H @(lsx_ind … H) -L1
-#L1 #_ #IHL1 #L2 #HL12 @lsx_intro
-#L3 #HL23 #HnL23 elim (leq_lpxs_trans_lleq … HL12 … HL23) -HL12 -HL23
-#L0 #HL03 #HL10 #H elim (H T) -H /4 width=4 by/
-qed-.
-
-lemma lsx_ge: ∀h,g,G,L,T,d1,d2. d1 ≤ d2 →
- G ⊢ ⋕⬊*[h, g, T, d1] L → G ⊢ ⋕⬊*[h, g, T, d2] L.
-#h #g #G #L #T #d1 #d2 #Hd12 #H @(lsx_ind … H) -L
-/5 width=7 by lsx_intro, lleq_ge/
-qed-.
-
-lemma lsx_lleq_trans: ∀h,g,T,G,L1,d. G ⊢ ⋕⬊*[h, g, T, d] L1 →
- ∀L2. L1 ⋕[T, d] L2 → G ⊢ ⋕⬊*[h, g, T, d] L2.
-#h #g #T #G #L1 #d #H @(lsx_ind … H) -L1
-#L1 #_ #IHL1 #L2 #HL12 @lsx_intro
-#K2 #HLK2 #HnLK2 elim (lleq_lpxs_trans … HLK2 … HL12) -HLK2
-/5 width=4 by lleq_canc_sn, lleq_trans/
-qed-.
-
-lemma lsx_lpxs_trans: ∀h,g,T,G,L1,d. G ⊢ ⋕⬊*[h, g, T, d] L1 →
- ∀L2. ⦃G, L1⦄ ⊢ ➡*[h, g] L2 → G ⊢ ⋕⬊*[h, g, T, d] L2.
-#h #g #T #G #L1 #d #H @(lsx_ind … H) -L1 #L1 #HL1 #IHL1 #L2 #HL12
-elim (lleq_dec T L1 L2 d) /3 width=4 by lsx_lleq_trans/
-qed-.
-
-fact lsx_bind_lpxs_aux: ∀h,g,a,I,G,L1,V,d. G ⊢ ⋕⬊*[h, g, V, d] L1 →
- ∀Y,T. G ⊢ ⋕⬊*[h, g, T, ⫯d] Y →
- ∀L2. Y = L2.ⓑ{I}V → ⦃G, L1⦄ ⊢ ➡*[h, g] L2 →
- G ⊢ ⋕⬊*[h, g, ⓑ{a,I}V.T, d] L2.
-#h #g #a #I #G #L1 #V #d #H @(lsx_ind … H) -L1
-#L1 #HL1 #IHL1 #Y #T #H @(lsx_ind … H) -Y
-#Y #HY #IHY #L2 #H #HL12 destruct @lsx_intro
-#L0 #HL20 lapply (lpxs_trans … HL12 … HL20)
-#HL10 #H elim (nlleq_inv_bind … H) -H [ -HL1 -IHY | -HY -IHL1 ]
-[ #HnV elim (lleq_dec V L1 L2 d)
- [ #HV @(IHL1 … L0) /3 width=5 by lsx_lpxs_trans, lpxs_pair, lleq_canc_sn/ (**) (* full auto too slow *)
- | -HnV -HL10 /4 width=5 by lsx_lpxs_trans, lpxs_pair/
- ]
-| /3 width=4 by lpxs_pair/
-]
-qed-.
-
-lemma lsx_bind: ∀h,g,a,I,G,L,V,d. G ⊢ ⋕⬊*[h, g, V, d] L →
- ∀T. G ⊢ ⋕⬊*[h, g, T, ⫯d] L.ⓑ{I}V →
- G ⊢ ⋕⬊*[h, g, ⓑ{a,I}V.T, d] L.
-/2 width=3 by lsx_bind_lpxs_aux/ qed.
-
-lemma lsx_flat_lpxs: ∀h,g,I,G,L1,V,d. G ⊢ ⋕⬊*[h, g, V, d] L1 →
- ∀L2,T. G ⊢ ⋕⬊*[h, g, T, d] L2 → ⦃G, L1⦄ ⊢ ➡*[h, g] L2 →
- G ⊢ ⋕⬊*[h, g, ⓕ{I}V.T, d] L2.
-#h #g #I #G #L1 #V #d #H @(lsx_ind … H) -L1
-#L1 #HL1 #IHL1 #L2 #T #H @(lsx_ind … H) -L2
-#L2 #HL2 #IHL2 #HL12 @lsx_intro
-#L0 #HL20 lapply (lpxs_trans … HL12 … HL20)
-#HL10 #H elim (nlleq_inv_flat … H) -H [ -HL1 -IHL2 | -HL2 -IHL1 ]
-[ #HnV elim (lleq_dec V L1 L2 d)
- [ #HV @(IHL1 … L0) /3 width=3 by lsx_lpxs_trans, lleq_canc_sn/ (**) (* full auto too slow: 47s *)
- | -HnV -HL10 /3 width=4 by lsx_lpxs_trans/
- ]
-| /3 width=1 by/
-]
-qed-.
-
-lemma lsx_flat: ∀h,g,I,G,L,V,d. G ⊢ ⋕⬊*[h, g, V, d] L →
- ∀T. G ⊢ ⋕⬊*[h, g, T, d] L → G ⊢ ⋕⬊*[h, g, ⓕ{I}V.T, d] L.
-/2 width=3 by lsx_flat_lpxs/ qed.
-
-(* Advanced forward lemmas **************************************************)
-
-lemma lsx_fwd_lref_be: ∀h,g,I,G,L,d,i. d ≤ yinj i → G ⊢ ⋕⬊*[h, g, #i, d] L →
- ∀K,V. ⇩[i] L ≡ K.ⓑ{I}V → G ⊢ ⋕⬊*[h, g, V, 0] K.
-#h #g #I #G #L #d #i #Hdi #H @(lsx_ind … H) -L
-#L1 #_ #IHL1 #K1 #V #HLK1 @lsx_intro
-#K2 #HK12 #HnK12 lapply (ldrop_fwd_drop2 … HLK1)
-#H2LK1 elim (ldrop_lpxs_trans … H2LK1 … HK12) -H2LK1 -HK12
-#L2 #HL12 #H2LK2 #H elim (leq_ldrop_conf_be … H … HLK1) -H /2 width=1 by ylt_inj/
-#Y #_ #HLK2 lapply (ldrop_fwd_drop2 … HLK2)
-#HY lapply (ldrop_mono … HY … H2LK2) -HY -H2LK2 #H destruct
-/4 width=10 by lleq_inv_lref_ge/
-qed-.
-
-lemma lsx_fwd_bind_dx: ∀h,g,a,I,G,L,V,T,d. G ⊢ ⋕⬊*[h, g, ⓑ{a,I}V.T, d] L →
- G ⊢ ⋕⬊*[h, g, T, ⫯d] L.ⓑ{I}V.
-#h #g #a #I #G #L #V1 #T #d #H @(lsx_ind … H) -L
-#L1 #_ #IHL1 @lsx_intro
-#Y #H #HT elim (lpxs_inv_pair1 … H) -H
-#L2 #V2 #HL12 #_ #H destruct
-@(lsx_leq_conf … (L2.ⓑ{I}V1)) /2 width=1 by leq_succ/
-@IHL1 // #H @HT -IHL1 -HL12 -HT
-@(lleq_leq_trans … (L2.ⓑ{I}V1))
-/2 width=2 by lleq_fwd_bind_dx, leq_succ/
-qed-.
-
-(* Advanced inversion lemmas ************************************************)
-
-lemma lsx_inv_bind: ∀h,g,a,I,G,L,V,T,d. G ⊢ ⋕⬊*[h, g, ⓑ{a, I}V.T, d] L →
- G ⊢ ⋕⬊*[h, g, V, d] L ∧ G ⊢ ⋕⬊*[h, g, T, ⫯d] L.ⓑ{I}V.
-/3 width=4 by lsx_fwd_bind_sn, lsx_fwd_bind_dx, conj/ qed-.
r: reduction
s: substitution
u: supclosure
+w: reserved for generic pointwise extension
x: extended reduction
y: extended substitution
r: proper multiple step (restricted) (restricted)
s: reflexive transitive closure (star)
u: proper single step (restricted) (unit)
+x: reserved for generic pointwise extension
--- /dev/null
+(**************************************************************************)
+(* ___ *)
+(* ||M|| *)
+(* ||A|| A project by Andrea Asperti *)
+(* ||T|| *)
+(* ||I|| Developers: *)
+(* ||T|| The HELM team. *)
+(* ||A|| http://helm.cs.unibo.it *)
+(* \ / *)
+(* \ / This file is distributed under the terms of the *)
+(* v GNU General Public License Version 2 *)
+(* *)
+(**************************************************************************)
+
+(* NOTATION FOR THE FORMAL SYSTEM λδ ****************************************)
+
+notation "hvbox( G ⊢ ~ ⬊ * break [ term 46 h , break term 46 g , break term 46 d ] break term 46 L )"
+ non associative with precedence 45
+ for @{ 'CoSN $h $g $d $G $L }.
+++ /dev/null
-(**************************************************************************)
-(* ___ *)
-(* ||M|| *)
-(* ||A|| A project by Andrea Asperti *)
-(* ||T|| *)
-(* ||I|| Developers: *)
-(* ||T|| The HELM team. *)
-(* ||A|| http://helm.cs.unibo.it *)
-(* \ / *)
-(* \ / This file is distributed under the terms of the *)
-(* v GNU General Public License Version 2 *)
-(* *)
-(**************************************************************************)
-
-(* NOTATION FOR THE FORMAL SYSTEM λδ ****************************************)
-
-notation "hvbox( G ⊢ ⧤ ⬊ * break [ term 46 h , break term 46 g , break term 46 d ] break term 46 L )"
- non associative with precedence 45
- for @{ 'LazyCoSN $h $g $d $G $L }.
--- /dev/null
+(**************************************************************************)
+(* ___ *)
+(* ||M|| *)
+(* ||A|| A project by Andrea Asperti *)
+(* ||T|| *)
+(* ||I|| Developers: *)
+(* ||T|| The HELM team. *)
+(* ||A|| http://helm.cs.unibo.it *)
+(* \ / *)
+(* \ / This file is distributed under the terms of the *)
+(* v GNU General Public License Version 2 *)
+(* *)
+(**************************************************************************)
+
+(* NOTATION FOR THE FORMAL SYSTEM λδ ****************************************)
+
+notation "hvbox( G ⊢ ⬊ * break [ term 46 h , break term 46 g , break term 46 T , break term 46 d ] break term 46 L )"
+ non associative with precedence 45
+ for @{ 'SN $h $g $T $d $G $L }.
--- /dev/null
+(**************************************************************************)
+(* ___ *)
+(* ||M|| *)
+(* ||A|| A project by Andrea Asperti *)
+(* ||T|| *)
+(* ||I|| Developers: *)
+(* ||T|| The HELM team. *)
+(* ||A|| http://helm.cs.unibo.it *)
+(* \ / *)
+(* \ / This file is distributed under the terms of the *)
+(* v GNU General Public License Version 2 *)
+(* *)
+(**************************************************************************)
+
+(* NOTATION FOR THE FORMAL SYSTEM λδ ****************************************)
+
+notation "hvbox( G ⊢ ⬊ ⬊ * break [ term 46 h , break term 46 g , break term 46 T , break term 46 d ] break term 46 L )"
+ non associative with precedence 45
+ for @{ 'SNAlt $h $g $T $d $G $L }.
(* *)
(**************************************************************************)
+include "basic_2/substitution/lleq_leq.ma".
include "basic_2/substitution/lleq_ldrop.ma".
+include "basic_2/reduction/cpx_leq.ma".
include "basic_2/reduction/lpx_ldrop.ma".
(* SN EXTENDED PARALLEL REDUCTION FOR LOCAL ENVIRONMENTS ********************)
| * #HG #HL #HT destruct /2 width=4 by ex3_intro/
]
qed-.
+
+fact leq_lpx_trans_lleq_aux: ∀h,g,G,L1,L0,d,e. L1 ≃[d, e] L0 → e = ∞ →
+ ∀L2. ⦃G, L0⦄ ⊢ ➡[h, g] L2 →
+ ∃∃L. L ≃[d, e] L2 & ⦃G, L1⦄ ⊢ ➡[h, g] L &
+ (∀T. L0 ⋕[T, d] L2 ↔ L1 ⋕[T, d] L).
+#h #g #G #L1 #L0 #d #e #H elim H -L1 -L0 -d -e
+[ #d #e #_ #L2 #H >(lpx_inv_atom1 … H) -H
+ /3 width=5 by ex3_intro, conj/
+| #I1 #I0 #L1 #L0 #V1 #V0 #_ #_ #He destruct
+| #I #L1 #L0 #V1 #e #HL10 #IHL10 #He #Y #H
+ elim (lpx_inv_pair1 … H) -H #L2 #V2 #HL02 #HV02 #H destruct
+ lapply (ysucc_inv_Y_dx … He) -He #He
+ elim (IHL10 … HL02) // -IHL10 -HL02 #L #HL2 #HL1 #IH
+ @(ex3_intro … (L.ⓑ{I}V2)) /3 width=3 by lpx_pair, leq_cpx_trans, leq_pair/
+ #T elim (IH T) #HL0dx #HL0sn
+ @conj #H @(lleq_leq_repl … H) -H /3 width=1 by leq_sym, leq_pair_O_Y/
+| #I1 #I0 #L1 #L0 #V1 #V0 #d #e #HL10 #IHL10 #He #Y #H
+ elim (lpx_inv_pair1 … H) -H #L2 #V2 #HL02 #HV02 #H destruct
+ elim (IHL10 … HL02) // -IHL10 -HL02 #L #HL2 #HL1 #IH
+ @(ex3_intro … (L.ⓑ{I1}V1)) /3 width=1 by lpx_pair, leq_succ/
+ #T elim (IH T) #HL0dx #HL0sn
+ @conj #H @(lleq_leq_repl … H) -H /3 width=1 by leq_sym, leq_succ/
+]
+qed-.
+
+lemma leq_lpx_trans_lleq: ∀h,g,G,L1,L0,d. L1 ≃[d, ∞] L0 →
+ ∀L2. ⦃G, L0⦄ ⊢ ➡[h, g] L2 →
+ ∃∃L. L ≃[d, ∞] L2 & ⦃G, L1⦄ ⊢ ➡[h, g] L &
+ (∀T. L0 ⋕[T, d] L2 ↔ L1 ⋕[T, d] L).
+/2 width=1 by leq_lpx_trans_lleq_aux/ qed-.
}
]
[ { "strongly normalizing extended computation" * } {
-(* [ "lcosx ( ? ⊢ ⧤⬊*[?,?,?] ? )" "lcosx_cpxs" * ] *)
+ [ "lcosx ( ? ⊢ ~⬊*[?,?,?] ? )" "lcosx_cpx" * ]
[ "llsx ( ? ⊢ ⋕⬊*[?,?,?,?] ? )" "llsx_alt ( ? ⊢ ⋕⬊⬊*[?,?,?,?] ? )" "llsx_ldrop" + "llsx_llpx" + "llsx_llpxs" + "llsx_csx" * ]
+ [ "lsx ( ? ⊢ ⬊*[?,?,?,?] ? )" "lsx_alt ( ? ⊢ ⬊⬊*[?,?,?,?] ? )" "lsx_ldrop" + "lsx_lpx" + "lsx_lpxs" + "llsx_csx" * ]
[ "csx_vector ( ⦃?,?⦄ ⊢ ⬊*[?,?] ? )" "csx_tstc_vector" + "csx_aaa" * ]
[ "csx ( ⦃?,?⦄ ⊢ ⬊*[?,?] ? )" "csx_alt ( ⦃?,?⦄ ⊢ ⬊⬊*[?,?] ? )" "csx_lift" + "csx_lpx" + "csx_llpx" + "csx_lpxs" + "csx_llpxs" + "csx_fpbs" * ]
}
projects / helm.git / commitdiff