--- /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/reduction/cpx_cpys.ma".
+include "basic_2/computation/cpxs.ma".
+
+(* CONTEXT-SENSITIVE EXTENDED PARALLEL COMPUTATION ON TERMS *****************)
+
+(* Properties on local environment refinement for extended substitution *****)
+
+lemma lsuby_cpxs_trans: ∀h,g,G. lsub_trans … (cpxs h g G) (lsuby 0 (∞)).
+/3 width=5 by lsuby_cpx_trans, LTC_lsub_trans/
+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/cpye_lift.ma".
-include "basic_2/reduction/lpx_cpye.ma".
-include "basic_2/computation/cpxs_cpxs.ma".
-include "basic_2/computation/lpxs.ma".
-
-(* SN EXTENDED PARALLEL COMPUTATION ON LOCAL ENVIRONMENTS *******************)
-
-(* Forward lemmas on evaluation for extended substitution *******************)
-
-lemma cpx_cpye_fwd_lpxs: ∀h,g,G,L1,L2. ⦃G, L1⦄ ⊢ ➡*[h, g] L2 →
- ∀T1,T2. ⦃G, L1⦄ ⊢ T1 ➡[h, g] T2 →
- ∀U1,d,e. ⦃G, L1⦄ ⊢ T1 ▶*[d, e] 𝐍⦃U1⦄ →
- ∀U2. ⦃G, L2⦄ ⊢ T2 ▶*[d, e] 𝐍⦃U2⦄ →
- ⦃G, L1⦄ ⊢ U1 ➡*[h, g] U2.
-#h #g #G #L1 #L2 #H @(lpxs_ind_dx … H) -L1
-[ /3 width=9 by cpx_cpxs, cpx_cpye_fwd_lpx/
-| #L1 #L #HL1 #_ #IHL2 #T1 #T2 #HT12 #U1 #d #e #HTU1 #U2 #HTU2
- elim (cpye_total G L T2 d e) #X2 #HTX2
- lapply (cpx_cpye_fwd_lpx … HT12 … HL1 … HTU1 … HTX2) -T1
- /4 width=9 by lpx_cpxs_trans, cpxs_strap2/ (**) (* full auto too long: 41s *)
-]
-qed-.
(* *)
(**************************************************************************)
-include "basic_2/substitution/lleq_ext.ma".
+include "basic_2/reduction/lpx_lleq.ma".
+include "basic_2/computation/cpxs_cpys.ma".
include "basic_2/computation/lpxs_ldrop.ma".
include "basic_2/computation/lpxs_cpxs.ma".
(* SN EXTENDED PARALLEL COMPUTATION FOR LOCAL ENVIRONMENTS ******************)
-(* Advanced properties ******************************************************)
+(* Properties on lazy equivalence for local environments ********************)
-axiom lleq_lpxs_trans: ∀h,g,G,L1,L2,T,d. L1 ⋕[T, d] L2 → ∀K2. ⦃G, L2⦄ ⊢ ➡*[h, g] K2 →
+lemma lleq_lpxs_trans: ∀h,g,G,L2,K2. ⦃G, L2⦄ ⊢ ➡*[h, g] K2 →
+ ∀L1,T,d. L1 ⋕[T, d] L2 →
∃∃K1. ⦃G, L1⦄ ⊢ ➡*[h, g] K1 & K1 ⋕[T, d] K2.
-(*
-#h #g #G #L1 #L2 #T #d #H @(lleq_ind_alt … H) -L1 -L2 -T -d
-[
-|
-|
-|
-|
-| #a #I #L1 #L2 #V #T #d #_ #_ #IHV #IHT #K2 #HLK2
- elim (IHV … HLK2) -IHV #KV #HLKV #HV
- elim (IHT (K2.ⓑ{I}V)) -IHT /2 width=1 by lpxs_pair_refl/ -HLK2 #Y #H #HT
- elim (lpxs_inv_pair1 … H) -H #KT #VT #HLKT #_ #H destruct
-
-#h #g #G #L1 #L2 #T #d * #HL12 #IH #K2 #HLK2
-*)
-
-(* Properties on lazy equivalence for local environments ********************)
+#h #g #G #L2 #K2 #H @(lpxs_ind … H) -K2 /2 width=3 by ex2_intro/
+#K #K2 #_ #HK2 #IH #L1 #T #d #HT elim (IH … HT) -L2
+#L #HL1 #HT elim (lleq_lpx_trans … HK2 … HT) -K
+/3 width=3 by lpxs_strap1, ex2_intro/
+qed-.
lemma lpxs_lleq_fqu_trans: ∀h,g,G1,G2,L1,L2,T1,T2. ⦃G1, L1, T1⦄ ⊃ ⦃G2, L2, T2⦄ →
∀K1. ⦃G1, K1⦄ ⊢ ➡*[h, g] L1 → K1 ⋕[T1, 0] L1 →
| * #HG #HL #HT destruct /2 width=4 by ex3_intro/
]
qed-.
+
+fact lsuby_lpxs_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. |L1| = |L0| → |L| = |L2| → L0 ⋕[T, d] L2 ↔ L1 ⋕[T, d] L).
+#h #g #G #L1 #L0 #d #e #H elim H -L1 -L0 -d -e
+[ #L1 #d #e #_ #L2 #H >(lpxs_inv_atom1 … H) -H
+ /3 width=5 by ex3_intro, conj/
+| #I1 #I0 #L1 #L0 #V1 #V0 #_ #_ #He destruct
+| #I1 #I0 #L1 #L0 #V1 #e #HL10 #IHL10 #He #Y #H
+ elim (lpxs_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.ⓑ{I1}V2)) /3 width=3 by lpxs_pair, lsuby_cpxs_trans, lsuby_pair/
+ #T #H1 #H2 lapply (injective_plus_l … H1) lapply (injective_plus_l … H2) -H1 -H2
+ #H1 #H2 elim (IH T) // #HL0dx #HL0sn
+ @conj #H @(lleq_lsuby_repl … H) -H normalize
+ /3 width=1 by lsuby_sym, lsuby_pair_O_Y/
+| #I1 #I0 #L1 #L0 #V1 #V0 #d #e #HL10 #IHL10 #He #Y #H
+ elim (lpxs_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 lpxs_pair, lsuby_succ/
+ #T #H1 #H2 lapply (injective_plus_l … H1) lapply (injective_plus_l … H2) -H1 -H2
+ #H1 #H2 elim (IH T) // #HL0dx #HL0sn
+ @conj #H @(lleq_lsuby_repl … H) -H
+ /3 width=1 by lsuby_sym, lsuby_succ/ normalize //
+]
+qed-.
+
+lemma lsuby_lpxs_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. |L1| = |L0| → |L| = |L2| → L0 ⋕[T, d] L2 ↔ L1 ⋕[T, d] L).
+/2 width=1 by lsuby_lpxs_trans_lleq_aux/ qed-.
(* *)
(**************************************************************************)
-include "basic_2/notation/relations/lazysn_5.ma".
+include "basic_2/notation/relations/lazysn_6.ma".
include "basic_2/substitution/lleq.ma".
include "basic_2/computation/lpxs.ma".
(* SN EXTENDED STRONGLY NORMALIZING LOCAL ENVIRONMENTS **********************)
-definition lsx: ∀h. sd h → relation3 term genv lenv ≝
- λh,g,T,G. SN … (lpxs h g G) (lleq 0 T).
+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 T G L = (lsx h g T G L).
+ 'LazySN h g d T G L = (lsx h g T d G L).
(* Basic eliminators ********************************************************)
-lemma lsx_ind: ∀h,g,T,G. ∀R:predicate lenv.
- (∀L1. G ⊢ ⋕⬊*[h, g, T] L1 →
- (∀L2. ⦃G, L1⦄ ⊢ ➡*[h, g] L2 → (L1 ⋕[T, 0] L2 → ⊥) → R L2) →
+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] L → R L.
-#h #g #T #G #R #H0 #L1 #H elim H -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,T,G,L1.
- (∀L2. ⦃G, L1⦄ ⊢ ➡*[h, g] L2 → (L1 ⋕[T, 0] L2 → ⊥) → G ⊢ ⋕⬊*[h, g, T] L2) →
- G ⊢ ⋕⬊*[h, g, T] L1.
+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,T,G. G ⊢ ⋕⬊*[h, g, T] ⋆.
-#h #g #T #G @lsx_intro
+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,k. G ⊢ ⋕⬊*[h, g, ⋆k] L.
-#h #g #G #L1 #k @lsx_intro
+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,p. G ⊢ ⋕⬊*[h, g, §p] L.
-#h #g #G #L1 #p @lsx_intro
+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.
(* Basic forward lemmas *****************************************************)
-lemma lsx_fwd_bind_sn: ∀h,g,a,I,G,L,V,T. G ⊢ ⋕⬊*[h, g, ⓑ{a,I}V.T] L →
- G ⊢ ⋕⬊*[h, g, V] L.
-#h #g #a #I #G #L #V #T #H @(lsx_ind … H) -L
+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. G ⊢ ⋕⬊*[h, g, ⓕ{I}V.T] L →
- G ⊢ ⋕⬊*[h, g, V] L.
-#h #g #I #G #L #V #T #H @(lsx_ind … H) -L
+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. G ⊢ ⋕⬊*[h, g, ⓕ{I}V.T] L →
- G ⊢ ⋕⬊*[h, g, T] L.
-#h #g #I #G #L #V #T #H @(lsx_ind … H) -L
+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. G ⊢ ⋕⬊*[h, g, ②{I}V.T] L →
- G ⊢ ⋕⬊*[h, g, V] L.
+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. G ⊢ ⋕⬊*[h, g, ⓕ{I}V.T] L →
- G ⊢ ⋕⬊*[h, g, V] L ∧ G ⊢ ⋕⬊*[h, g, T] L.
+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-.
(* *)
(**************************************************************************)
+include "basic_2/reduction/cpx_cpys.ma".
+include "basic_2/computation/lpxs_llneq.ma".
+include "basic_2/computation/csx_alt.ma".
+include "basic_2/computation/lsx_lpxs.ma".
+
+(* SN EXTENDED STRONGLY NORMALIZING LOCAL ENVIRONMENTS **********************)
+
+(* Advanced properties ******************************************************)
+
+lemma lpxs_cpys_csx_lsx: ∀h,g,G,L1,U. ⦃G, L1⦄ ⊢ ⬊*[h, g] U →
+ ∀T. ⦃G, L1⦄ ⊢ T ▶*[0, ∞] U →
+ G ⊢ ⋕⬊*[h, g, T] L1.
+#h #g #G #L1 #U #H @(csx_ind_alt … H) -U
+#U #_ #IHU #T #HTU @lsx_intro
+#L2 #HL02 #HnT elim (lpxs_nlleq_fwd_cpxs … HL02 HnT) -HnT
+#U0 #U2 #H0 #H2 #HU02 #HnU02 elim (cpys_conf_eq … HTU … H0)
+#X #HUX #H0X elim (eq_term_dec U X) #HnUX destruct
+[ -HUX
+| -HnU02 @(lsx_lpxs_trans … HL02) @(IHU … HnUX)
+ [ /3 width=3 by cpys_cpx, cpx_cpxs/
+ | /2 width=3 by cpys_trans_eq/
+ ]
+]
+
+lemma lpxs_cpys_csx_lsx: ∀h,g,G,L1,U. ⦃G, L1⦄ ⊢ ⬊*[h, g] U →
+ ∀L2. ⦃G, L1⦄ ⊢ ➡*[h, g] L2 → ∀T. ⦃G, L2⦄ ⊢ T ▶*[0, ∞] U →
+ G ⊢ ⋕⬊*[h, g, T] L2.
+#h #g #G #L1 #U #H @(csx_ind_alt … H) -U
+#U #_ #IHU #L0 #HL10 #T #HTU @lsx_intro
+#L2 #HL02 #HnT elim (lpxs_nlleq_fwd_cpxs … HL02 HnT) -HnT
+#U0 #U2 #H0 #H2 #HU02 #HnU02 elim (cpys_conf_eq … HTU … H0)
+#X #HUX #H0X elim (eq_term_dec U X) #HnUX destruct
+[ -HUX
+| -HnU02 @(IHU … HnUX)
+
+
+-HnT /4 width=9 by lpxs_trans, lpxs_cpxs_trans, cpx_cpye_fwd_lpxs/
+]
+
+
+
+
+
+
+
include "basic_2/reduction/cpx_cpys.ma".
include "basic_2/computation/lpxs_cpye.ma".
include "basic_2/computation/csx_alt.ma".
(* Advanced properties ******************************************************)
-lemma lsx_lleq_trans: ∀h,g,T,G,L1. G ⊢ ⋕⬊*[h, g, T] L1 →
- ∀L2. L1 ⋕[T, 0] L2 → G ⊢ ⋕⬊*[h, g, T] L2.
-#h #g #T #G #L1 #H @(lsx_ind … H) -L1
+lemma lsx_leqy_conf: ∀h,g,G,L1,T,d. G ⊢ ⋕⬊*[h, g, T, d] L1 →
+ ∀L2. L1 ⊑×[d, ∞] L2 → |L1| = |L2| → G ⊢ ⋕⬊*[h, g, T, d] L2.
+#h #g #G #L1 #T #d #H @(lsx_ind … H) -L1
+#L1 #_ #IHL1 #L2 #H1L12 #H2L12 @lsx_intro
+#L3 #H1L23 #HnL23 lapply (lpxs_fwd_length … H1L23)
+#H2L23 elim (lsuby_lpxs_trans_lleq … H1L12 … H1L23) -H1L12 -H1L23
+#L0 #H1L03 #H1L10 #H lapply (lpxs_fwd_length … H1L10)
+#H2L10 elim (H T) -H //
+#_ #H @(IHL1 … H1L10) -IHL1 -H1L10 /3 width=1 by/
+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 … HL12 … HLK2) -HLK2
+#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. G ⊢ ⋕⬊*[h, g, T] L1 →
- ∀L2. ⦃G, L1⦄ ⊢ ➡*[h, g] L2 → G ⊢ ⋕⬊*[h, g, T] L2.
-#h #g #T #G #L1 #H @(lsx_ind … H) -L1 #L1 #HL1 #IHL1 #L2 #HL12
-elim (lleq_dec T L1 L2 0) /3 width=4 by lsx_lleq_trans/
+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_flat_lpxs: ∀h,g,I,G,L1,V. G ⊢ ⋕⬊*[h, g, V] L1 →
- ∀L2,T. G ⊢ ⋕⬊*[h, g, T] L2 → ⦃G, L1⦄ ⊢ ➡*[h, g] L2 →
- G ⊢ ⋕⬊*[h, g, ⓕ{I}T.V] L2.
-#h #g #I #G #L1 #V #H @(lsx_ind … H) -L1
+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 [ -HL2 -IHL1 | -HL1 -IHL2 ]
-[ /3 width=1 by/
-| #HnV elim (lleq_dec V L1 L2 0)
+#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. G ⊢ ⋕⬊*[h, g, V] L →
- ∀T. G ⊢ ⋕⬊*[h, g, T] L → G ⊢ ⋕⬊*[h, g, ⓕ{I}T.V] L.
+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_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_leqy_conf … (L2.ⓑ{I}V1)) /2 width=1 by lsuby_succ/
+@IHL1 // #H @HT -IHL1 -HL12 -HT
+@(lleq_lsuby_trans … (L2.ⓑ{I}V1))
+/2 width=2 by lleq_fwd_bind_dx, lsuby_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/notation/relations/psubstnormal_5.ma".
+include "basic_2/relocation/cpy.ma".
+
+(* NORMAL TERMS FOR CONTEXT-SENSITIVE EXTENDED SUBSTITUTION *****************)
+
+definition cny: ∀d,e. relation3 genv lenv term ≝
+ λd,e,G,L. NF … (cpy d e G L) (eq …).
+
+interpretation
+ "normality for context-sensitive extended substitution (term)"
+ 'PSubstNormal G L T d e = (cny d e G L T).
+
+(* Basic inversion lemmas ***************************************************)
+
+lemma cny_inv_lref: ∀G,L,d,e,i. ⦃G, L⦄ ⊢ ▶[d, e] 𝐍⦃#i⦄ →
+ ∨∨ yinj i < d | d + e ≤ yinj i | |L| ≤ i.
+#G #L #d #e #i #H elim (ylt_split i d) /2 width=1 by or3_intro0/
+#Hdi elim (ylt_split i (d+e)) /2 width=1 by or3_intro1/
+#Hide elim (lt_or_ge i (|L|)) /2 width=1 by or3_intro2/
+#Hi elim (ldrop_O1_lt L i) //
+#I #K #V #HLK elim (lift_total V 0 (i+1))
+#W #HVW lapply (H W ?) -H /2 width=5 by cpy_subst/ -HLK
+#H destruct elim (lift_inv_lref2_be … HVW) -L -d -e //
+qed-.
+
+lemma cny_inv_bind: ∀a,I,G,L,V,T,d,e. ⦃G, L⦄ ⊢ ▶[d, e] 𝐍⦃ⓑ{a,I}V.T⦄ →
+ ⦃G, L⦄ ⊢ ▶[d, e] 𝐍⦃V⦄ ∧ ⦃G, L.ⓑ{I}V⦄ ⊢ ▶[⫯d, e] 𝐍⦃T⦄.
+#a #I #G #L #V1 #T1 #d #e #HVT1 @conj
+[ #V2 #HV2 lapply (HVT1 (ⓑ{a,I}V2.T1) ?) -HVT1
+| #T2 #HT2 lapply (HVT1 (ⓑ{a,I}V1.T2) ?) -HVT1
+]
+/2 width=1 by cpy_bind/ #H destruct //
+qed-.
+
+lemma cny_inv_flat: ∀I,G,L,V,T,d,e. ⦃G, L⦄ ⊢ ▶[d, e] 𝐍⦃ⓕ{I}V.T⦄ →
+ ⦃G, L⦄ ⊢ ▶[d, e] 𝐍⦃V⦄ ∧ ⦃G, L⦄ ⊢ ▶[d, e] 𝐍⦃T⦄.
+#I #G #L #V1 #T1 #d #e #HVT1 @conj
+[ #V2 #HV2 lapply (HVT1 (ⓕ{I}V2.T1) ?) -HVT1
+| #T2 #HT2 lapply (HVT1 (ⓕ{I}V1.T2) ?) -HVT1
+]
+/2 width=1 by cpy_flat/ #H destruct //
+qed-.
+
+(* Basic properties *********************************************************)
+
+lemma lsuby_cny_conf: ∀G,d,e.
+ ∀L1,T. ⦃G, L1⦄ ⊢ ▶[d, e] 𝐍⦃T⦄ →
+ ∀L2. L1 ⊑×[d, e] L2 → ⦃G, L2⦄ ⊢ ▶[d, e] 𝐍⦃T⦄.
+#G #d #e #L1 #T1 #HT1 #L2 #HL12 #T2 #HT12
+@HT1 /3 width=3 by lsuby_cpy_trans/
+qed-.
+
+lemma cny_sort: ∀G,L,d,e,k. ⦃G, L⦄ ⊢ ▶[d, e] 𝐍⦃⋆k⦄.
+#G #L #d #e #k #X #H elim (cpy_inv_sort1 … H) -H //
+qed.
+
+lemma cny_lref_free: ∀G,L,d,e,i. |L| ≤ i → ⦃G, L⦄ ⊢ ▶[d, e] 𝐍⦃#i⦄.
+#G #L #d #e #i #Hi #X #H elim (cpy_inv_lref1 … H) -H // *
+#I #K #V #_ #_ #HLK #_ lapply (ldrop_fwd_length_lt2 … HLK) -HLK
+#H elim (lt_refl_false i) /2 width=3 by lt_to_le_to_lt/
+qed.
+
+lemma cny_lref_atom: ∀G,L,d,e,i. ⇩[i] L ≡ ⋆ → ⦃G, L⦄ ⊢ ▶[d, e] 𝐍⦃#i⦄.
+#G #L #d #e #i #HL @cny_lref_free >(ldrop_fwd_length … HL) -HL //
+qed.
+
+lemma cny_lref_top: ∀G,L,d,e,i. d+e ≤ yinj i → ⦃G, L⦄ ⊢ ▶[d, e] 𝐍⦃#i⦄.
+#G #L #d #e #i #Hdei #X #H elim (cpy_inv_lref1 … H) -H // *
+#I #K #V #_ #H elim (ylt_yle_false … H) //
+qed.
+
+lemma cny_lref_skip: ∀G,L,d,e,i. yinj i < d → ⦃G, L⦄ ⊢ ▶[d, e] 𝐍⦃#i⦄.
+#G #L #d #e #i #Hid #X #H elim (cpy_inv_lref1 … H) -H // *
+#I #K #V #H elim (ylt_yle_false … H) //
+qed.
+
+lemma cny_gref: ∀G,L,d,e,p. ⦃G, L⦄ ⊢ ▶[d, e] 𝐍⦃§p⦄.
+#G #L #d #e #p #X #H elim (cpy_inv_gref1 … H) -H //
+qed.
+
+lemma cny_bind: ∀G,L,V,d,e. ⦃G, L⦄ ⊢ ▶[d, e] 𝐍⦃V⦄ →
+ ∀I,T. ⦃G, L.ⓑ{I}V⦄ ⊢ ▶[⫯d, e] 𝐍⦃T⦄ →
+ ∀a. ⦃G, L⦄ ⊢ ▶[d, e] 𝐍⦃ⓑ{a,I}V.T⦄.
+#G #L #V1 #d #e #HV1 #I #T1 #HT1 #a #X #H
+elim (cpy_inv_bind1 … H) -H #V2 #T2 #HV12 #HT12 #H destruct
+>(HV1 … HV12) -V2 >(HT1 … HT12) -T2 //
+qed.
+
+lemma cny_flat: ∀G,L,V,d,e. ⦃G, L⦄ ⊢ ▶[d, e] 𝐍⦃V⦄ →
+ ∀T. ⦃G, L⦄ ⊢ ▶[d, e] 𝐍⦃T⦄ →
+ ∀I. ⦃G, L⦄ ⊢ ▶[d, e] 𝐍⦃ⓕ{I}V.T⦄.
+#G #L #V1 #d #e #HV1 #T1 #HT1 #I #X #H
+elim (cpy_inv_flat1 … H) -H #V2 #T2 #HV12 #HT12 #H destruct
+>(HV1 … HV12) -V2 >(HT1 … HT12) -T2 //
+qed.
+
+lemma cny_narrow: ∀G,L,T,d1,e1. ⦃G, L⦄ ⊢ ▶[d1, e1] 𝐍⦃T⦄ →
+ ∀d2,e2. d1 ≤ d2 → d2 + e2 ≤ d1 + e1 → ⦃G, L⦄ ⊢ ▶[d2, e2] 𝐍⦃T⦄.
+#G #L #T1 #d1 #e1 #HT1 #d2 #e2 #Hd12 #Hde21 #T2 #HT12
+@HT1 /2 width=5 by cpy_weak/ 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/cpy_lift.ma".
+include "basic_2/relocation/cny.ma".
+
+(* NORMAL TERMS FOR CONTEXT-SENSITIVE EXTENDED SUBSTITUTION *****************)
+
+(* Properties on relocation *************************************************)
+
+lemma cny_lift_le: ∀G,L,K,T,U,s,d,dt,e,et. ⦃G, K⦄ ⊢ ▶[dt, et] 𝐍⦃T⦄ → ⇩[s, d, e] L ≡ K →
+ ⇧[d, e] T ≡ U → dt + et ≤ d → ⦃G, L⦄ ⊢ ▶[dt, et] 𝐍⦃U⦄.
+#G #L #K #T1 #U1 #s #d #dt #e #et #HT1 #HLK #HTU1 #Hdetd #U2 #HU12
+elim (cpy_inv_lift1_le … HU12 … HLK … HTU1) // -L -Hdetd #T2 #HT12
+>(HT1 … HT12) -K /2 width=5 by lift_mono/
+qed-.
+
+lemma cny_lift_be: ∀G,L,K,T,U,s,d,dt,e,et. ⦃G, K⦄ ⊢ ▶[dt, et] 𝐍⦃T⦄ → ⇩[s, d, e] L ≡ K →
+ ⇧[d, e] T ≡ U → dt ≤ d → yinj d ≤ dt + et → ⦃G, L⦄ ⊢ ▶[dt, et+e] 𝐍⦃U⦄.
+#G #L #K #T1 #U1 #s #d #dt #e #et #HT1 #HLK #HTU1 #Hdtd #Hddet #U2 #HU12
+elim (cpy_inv_lift1_be … HU12 … HLK … HTU1) /2 width=1 by monotonic_yle_plus_dx/ -L -Hdtd -Hddet #T2
+>yplus_minus_inj #HT12 >(HT1 … HT12) -K /2 width=5 by lift_mono/
+qed-.
+
+lemma cny_lift_ge: ∀G,L,K,T,U,s,d,dt,e,et. ⦃G, K⦄ ⊢ ▶[dt, et] 𝐍⦃T⦄ → ⇩[s, d, e] L ≡ K →
+ ⇧[d, e] T ≡ U → d ≤ dt → ⦃G, L⦄ ⊢ ▶[dt+e, et] 𝐍⦃U⦄.
+#G #L #K #T1 #U1 #s #d #dt #e #et #HT1 #HLK #HTU1 #Hddt #U2 #HU12
+elim (cpy_inv_lift1_ge … HU12 … HLK … HTU1) /2 width=1 by monotonic_yle_plus_dx/ -L -Hddt #T2
+>yplus_minus_inj #HT12 >(HT1 … HT12) -K /2 width=5 by lift_mono/
+qed-.
+
+(* Inversion lemmas on relocation *******************************************)
+
+lemma cny_inv_lift_le: ∀G,L,K,T,U,s,d,dt,e,et. ⦃G, L⦄ ⊢ ▶[dt, et] 𝐍⦃U⦄ → ⇩[s, d, e] L ≡ K →
+ ⇧[d, e] T ≡ U → dt + et ≤ d → ⦃G, K⦄ ⊢ ▶[dt, et] 𝐍⦃T⦄.
+#G #L #K #T1 #U1 #s #d #dt #e #et #HU1 #HLK #HTU1 #Hdetd #T2 #HT12
+elim (lift_total T2 d e) #U2 #HTU2
+lapply (cpy_lift_le … HT12 … HLK … HTU1 … HTU2 ?) // -K -Hdetd #HU12
+lapply (HU1 … HU12) -L /2 width=5 by lift_inj/
+qed-.
+
+lemma cny_inv_lift_be: ∀G,L,K,T,U,s,d,dt,e,et. ⦃G, L⦄ ⊢ ▶[dt, et] 𝐍⦃U⦄ → ⇩[s, d, e] L ≡ K →
+ ⇧[d, e] T ≡ U → dt ≤ d → yinj d + e ≤ dt + et → ⦃G, K⦄ ⊢ ▶[dt, et-e] 𝐍⦃T⦄.
+#G #L #K #T1 #U1 #s #d #dt #e #et #HU1 #HLK #HTU1 #Hdtd #Hdedet #T2 #HT12
+lapply (yle_fwd_plus_ge_inj … Hdedet) // #Heet
+elim (yle_inv_plus_inj2 … Hdedet) -Hdedet #Hddete #Hedet
+elim (lift_total T2 d e) #U2 #HTU2
+lapply (cpy_lift_be … HT12 … HLK … HTU1 … HTU2 ? ?) // [ >yplus_minus_assoc_inj // ] -K -Hdtd -Hddete
+>ymax_pre_sn // -Heet #HU12
+lapply (HU1 … HU12) -L /2 width=5 by lift_inj/
+qed-.
+
+lemma cny_inv_lift_ge: ∀G,L,K,T,U,s,d,dt,e,et. ⦃G, L⦄ ⊢ ▶[dt, et] 𝐍⦃U⦄ → ⇩[s, d, e] L ≡ K →
+ ⇧[d, e] T ≡ U → yinj d + e ≤ dt → ⦃G, K⦄ ⊢ ▶[dt-e, et] 𝐍⦃T⦄.
+#G #L #K #T1 #U1 #s #d #dt #e #et #HU1 #HLK #HTU1 #Hdedt #T2 #HT12
+elim (yle_inv_plus_inj2 … Hdedt) -Hdedt #Hddte #Hedt
+elim (lift_total T2 d e) #U2 #HTU2
+lapply (cpy_lift_ge … HT12 … HLK … HTU1 … HTU2 ?) // -K -Hddte
+>ymax_pre_sn // -Hedt #HU12
+lapply (HU1 … HU12) -L /2 width=5 by lift_inj/
+qed-.
+
+(* Advanced inversion lemmas on relocation **********************************)
+
+lemma cny_inv_lift_ge_up: ∀G,L,K,T,U,s,d,dt,e,et. ⦃G, L⦄ ⊢ ▶[dt, et] 𝐍⦃U⦄ → ⇩[s, d, e] L ≡ K →
+ ⇧[d, e] T ≡ U → d ≤ dt → dt ≤ yinj d + e → yinj d + e ≤ dt + et →
+ ⦃G, K⦄ ⊢ ▶[d, dt + et - (yinj d + e)] 𝐍⦃T⦄.
+#G #L #K #T1 #U1 #s #d #dt #e #et #HU1 #HLK #HTU1 #Hddt #Hdtde #Hdedet
+lapply (cny_narrow … HU1 (d+e) (dt+et-(d+e)) ? ?) -HU1 [ >ymax_pre_sn_comm ] // #HU1
+lapply (cny_inv_lift_ge … HU1 … HLK … HTU1 ?) // -L -U1
+>yplus_minus_inj //
+qed-.
+
+lemma cny_inv_lift_subst: ∀G,L,K,V,W,i,d,e. d ≤ yinj i → i < d + e →
+ ⇩[i+1] L ≡ K → ⦃G, L⦄ ⊢ ▶[d, e] 𝐍⦃W⦄ →
+ ⇧[O, i+1] V ≡ W → ⦃G, K⦄ ⊢ ▶[O, ⫰(d+e-i)] 𝐍⦃V⦄.
+#G #L #K #V #W #i #d #e #Hdi #Hide #HLK #HW #HVW
+lapply (cny_inv_lift_ge_up … HW … HLK … HVW ? ? ?) //
+>yplus_O1 <yplus_inj >yplus_SO2
+[ /2 width=1 by ylt_fwd_le_succ1/
+| /2 width=3 by yle_trans/
+| >yminus_succ2 //
+]
+qed-.
+
+(* Advanced properties ******************************************************)
+
+(* Note: this should be applicable in a forward manner *)
+lemma cny_lift_ge_up: ∀G,L,K,T,U,s,d,dt,e,et. ⦃G, K⦄ ⊢ ▶[yinj d, dt + et - (yinj d + yinj e)] 𝐍⦃T⦄ →
+ ⇩[s, d, e] L ≡ K → ⇧[d, e] T ≡ U →
+ yinj d ≤ dt → dt ≤ yinj d + yinj e → yinj d + yinj e ≤ dt + et →
+ ⦃G, L⦄ ⊢ ▶[dt, et] 𝐍⦃U⦄.
+#G #L #K #T1 #U1 #s #d #dt #e #et #HT1 #HLK #HTU1 #Hddt #Hdtde #Hdedet
+lapply (cny_lift_be … HT1 … HLK … HTU1 ? ?) // -K -T1
+#HU1 @(cny_narrow … HU1) -HU1 // (**) (* auto fails *)
+qed-.
+
+lemma cny_lift_subst: ∀G,L,K,V,W,i,d,e. d ≤ yinj i → i < d + e →
+ ⇩[i+1] L ≡ K → ⦃G, K⦄ ⊢ ▶[O, ⫰(d+e-i)] 𝐍⦃V⦄ →
+ ⇧[O, i+1] V ≡ W → ⦃G, L⦄ ⊢ ▶[d, e] 𝐍⦃W⦄.
+#G #L #K #V #W #i #d #e #Hdi #Hide #HLK #HV #HVW
+@(cny_lift_ge_up … HLK … HVW) // >yplus_O1 <yplus_inj >yplus_SO2
+[ >yminus_succ2 //
+| /2 width=3 by yle_trans/
+| /2 width=1 by ylt_fwd_le_succ1/
+]
+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/delta_equivalence/cpzs.ma".
+include "basic_2/reduction/cpx.ma".
+
+fact destruct_tsort_tsort: ∀k1,k2. ⋆k1 = ⋆k2 → k1 = k2.
+#k1 #k2 #H destruct //
+qed-.
+
+axiom cpzs_inv_subst: ∀I,G,L,K,V1,V2,W2,i.
+ ⇩[i] L ≡ K.ⓑ{I}V1 → ⇧[O, i+1] V2 ≡ W2 →
+ ⦃G, L⦄ ⊢ #i ◆*[O, ∞] W2 → ⦃G, K⦄⊢ V1 ◆*[O, ∞] V2.
+
+axiom cpzs_subst: ∀I,G,L,K,V1,V2,W2,i.
+ ⇩[i] L ≡ K.ⓑ{I}V1 → ⇧[O, i+1] V2 ≡ W2 →
+ ⦃G, K⦄⊢ V1 ◆*[O, ∞] V2 → ⦃G, L⦄ ⊢ #i ◆*[O, ∞] W2.
+
+(* CONTEXT-SENSITIVE EXTENDED PARALLEL REDUCTION FOR TERMS ******************)
+
+(* Forward lemmas on delta-equivalence for terms ****************************)
+
+lemma cpx_fwd_cpys_cpzs: ∀h,g,G,L,T1,T2. ⦃G, L⦄ ⊢ T1 ➡[h, g] T2 →
+ ∀d,e. ⦃G, L⦄ ⊢ T1 ◆*[d, e] T2 ↔ ⦃G, L⦄ ⊢ T1 ▶*[d, e] T2.
+#h #g #G #L #T1 #T2 #H elim H -G -L -T1 -T2
+[ /2 width=1 by conj/
+| #G #L #k #l #_ #d #e @conj #H lapply (next_lt h k)
+ [ <(cpzs_inv_sort … H)
+ | lapply (cpys_inv_sort1 … H) -H #H >(destruct_tsort_tsort … H)
+ ] -H #H elim (lt_refl_false … H)
+| #I #G #L #K #V1 #V2 #W2 #i #HLK #_ #HVW2 #IHV12 #d #e @conj #H
+(*
+ [ @(cpys_subst … HLK … HVW2) // >yminus_Y_inj /3 width=7 by cpzs_inv_subst/
+ | elim (cpys_inv_lref1_ldrop … H … HLK … HVW2) -H /3 width=7 by cpzs_subst/
+ ]
+*)
+| #a #I #G #L #V1 #V2 #T1 #T2 #_ #_ #IHV12 #IHT12 #d #e
+ elim (IHV12 d e) -IHV12 elim (IHT12 (⫯d) e) -IHT12
+ #IHTdx #IHTsn #IHVdx #IHVsn @conj #H
+ [ elim (cpzs_inv_bind … H) -H /3 width=1 by cpys_bind/
+ | elim (cpys_inv_bind1 … H) -H #X1 #X2 #H1 #H2 #H destruct /3 width=1 by cpzs_bind/
+ ]
+| #I #G #L #V1 #V2 #T1 #T2 #_ #_ #IHV12 #IHT12 #d #e
+ elim (IHV12 d e) -IHV12 elim (IHT12 (d) e) -IHT12
+ #IHTdx #IHTsn #IHVdx #IHVsn @conj #H
+ [ elim (cpzs_inv_flat … H) -H /3 width=1 by cpys_flat/
+ | elim (cpys_inv_flat1 … H) -H #X1 #X2 #H1 #H2 #H destruct /3 width=1 by cpzs_flat/
+ ]
+| #G #L #V #U1 #U2 #T2 #_ #HTU2 #_ #d #e @conj #H
+| #G #L #V1 #T1 #T2 #_ #_ #d #e @conj #H
+| #G #L #V1 #V2 #T1 #HV12 #_ #d #e @conj #H
+| #a #G #L #V1 #V2 #W1 #W2 #T1 #T2 #_ #_ #_ #_ #_ #_ #d #e @conj #H
+ [ elim (cpzs_inv_flat_bind … H)
+ | elim (cpys_inv_flat1 … H) -H #X1 #X2 #H1 #H2 #H destruct
+ ]
+| #a #G #L #V1 #V #V2 #W1 #W2 #T1 #T2 #_ #_ #_ #_ #_ #_ #_ #d #e @conj #H
+ [ elim (cpzs_inv_flat_bind … H)
+ | elim (cpys_inv_flat1 … H) -H #X1 #X2 #H1 #H2 #H destruct
+ ]
+]
+
+
\ No newline at end of file
--- /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/psubsteval_6.ma".
+include "basic_2/relocation/cny.ma".
+include "basic_2/substitution/cpys.ma".
+
+(* EVALUATION FOR CONTEXT-SENSITIVE EXTENDED SUBSTITUTION ON TERMS **********)
+
+definition cpye: ynat → ynat → relation4 genv lenv term term ≝
+ λd,e,G,L,T1,T2. ⦃G, L⦄ ⊢ T1 ▶*[d, e] T2 ∧ ⦃G, L⦄ ⊢ ▶[d, e] 𝐍⦃T2⦄.
+
+interpretation "evaluation for context-sensitive extended substitution (term)"
+ 'PSubstEval G L T1 T2 d e = (cpye d e G L T1 T2).
+
+(* Basic_properties *********************************************************)
+
+(* Note: this should go in subconversion *)
+lemma leqy_cpye_trans: ∀G,L2,T1,T2,d,e. ⦃G, L2⦄ ⊢ T1 ▶*[d, e] 𝐍⦃T2⦄ →
+ ∀L1. L1 ⊑×[d, e] L2 → L2 ⊑×[d, e] L1 → ⦃G, L1⦄ ⊢ T1 ▶*[d, e] 𝐍⦃T2⦄.
+#G #L2 #T1 #T2 #d #e *
+/4 width=8 by lsuby_cpys_trans, lsuby_cny_conf, conj/
+qed-.
+
+lemma cpye_sort: ∀G,L,d,e,k. ⦃G, L⦄ ⊢ ⋆k ▶*[d, e] 𝐍⦃⋆k⦄.
+/3 width=5 by cny_sort, conj/ qed.
+
+lemma cpye_free: ∀G,L,d,e,i. |L| ≤ i → ⦃G, L⦄ ⊢ #i ▶*[d, e] 𝐍⦃#i⦄.
+/3 width=6 by cny_lref_free, conj/ qed.
+
+lemma cpye_top: ∀G,L,d,e,i. d + e ≤ yinj i → ⦃G, L⦄ ⊢ #i ▶*[d, e] 𝐍⦃#i⦄.
+/3 width=6 by cny_lref_top, conj/ qed.
+
+lemma cpye_skip: ∀G,L,d,e,i. yinj i < d → ⦃G, L⦄ ⊢ #i ▶*[d, e] 𝐍⦃#i⦄.
+/3 width=6 by cny_lref_skip, conj/ qed.
+
+lemma cpye_gref: ∀G,L,d,e,p. ⦃G, L⦄ ⊢ §p ▶*[d, e] 𝐍⦃§p⦄.
+/3 width=5 by cny_gref, conj/ qed.
+
+lemma cpye_bind: ∀G,L,V1,V2,d,e. ⦃G, L⦄ ⊢ V1 ▶*[d, e] 𝐍⦃V2⦄ →
+ ∀I,T1,T2. ⦃G, L.ⓑ{I}V1⦄ ⊢ T1 ▶*[⫯d, e] 𝐍⦃T2⦄ →
+ ∀a. ⦃G, L⦄ ⊢ ⓑ{a,I}V1.T1 ▶*[d, e] 𝐍⦃ⓑ{a,I}V2.T2⦄.
+#G #L #V1 #V2 #d #e * #HV12 #HV2 #I #T1 #T2 *
+/5 width=8 by cpys_bind, cny_bind, lsuby_cny_conf, lsuby_succ, conj/
+qed.
+
+lemma cpye_flat: ∀G,L,V1,V2,d,e. ⦃G, L⦄ ⊢ V1 ▶*[d, e] 𝐍⦃V2⦄ →
+ ∀T1,T2. ⦃G, L⦄ ⊢ T1 ▶*[d, e] 𝐍⦃T2⦄ →
+ ∀I. ⦃G, L⦄ ⊢ ⓕ{I}V1.T1 ▶*[d, e] 𝐍⦃ⓕ{I}V2.T2⦄.
+#G #L #V1 #V2 #d #e * #HV12 #HV2 #T1 #T2 *
+/3 width=7 by cpys_flat, cny_flat, conj/
+qed.
+
+(* Basic inversion lemmas ***************************************************)
+
+lemma cpye_inv_sort1: ∀G,L,X,d,e,k. ⦃G, L⦄ ⊢ ⋆k ▶*[d, e] 𝐍⦃X⦄ → X = ⋆k.
+#G #L #X #d #e #k * /2 width=5 by cpys_inv_sort1/
+qed-.
+
+lemma cpye_inv_gref1: ∀G,L,X,d,e,p. ⦃G, L⦄ ⊢ §p ▶*[d, e] 𝐍⦃X⦄ → X = §p.
+#G #L #X #d #e #p * /2 width=5 by cpys_inv_gref1/
+qed-.
+
+lemma cpye_inv_bind1: ∀a,I,G,L,V1,T1,X,d,e. ⦃G, L⦄ ⊢ ⓑ{a,I}V1.T1 ▶*[d, e] 𝐍⦃X⦄ →
+ ∃∃V2,T2. ⦃G, L⦄ ⊢ V1 ▶*[d, e] 𝐍⦃V2⦄ & ⦃G, L.ⓑ{I}V1⦄ ⊢ T1 ▶*[⫯d, e] 𝐍⦃T2⦄ &
+ X = ⓑ{a,I}V2.T2.
+#a #I #G #L #V1 #T1 #X #d #e * #H1 #H2 elim (cpys_inv_bind1 … H1) -H1
+#V2 #T2 #HV12 #HT12 #H destruct elim (cny_inv_bind … H2) -H2
+/5 width=8 by lsuby_cny_conf, lsuby_succ, ex3_2_intro, conj/
+qed-.
+
+lemma cpye_inv_flat1: ∀I,G,L,V1,T1,X,d,e. ⦃G, L⦄ ⊢ ⓕ{I}V1.T1 ▶*[d, e] 𝐍⦃X⦄ →
+ ∃∃V2,T2. ⦃G, L⦄ ⊢ V1 ▶*[d, e] 𝐍⦃V2⦄ & ⦃G, L⦄ ⊢ T1 ▶*[d, e] 𝐍⦃T2⦄ &
+ X = ⓕ{I}V2.T2.
+#I #G #L #V1 #T1 #X #d #e * #H1 #H2 elim (cpys_inv_flat1 … H1) -H1
+#V2 #T2 #HV12 #HT12 #H destruct elim (cny_inv_flat … H2) -H2
+/3 width=5 by ex3_2_intro, 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/psubstevalalt_6.ma".
+include "basic_2/substitution/cpye_lift.ma".
+
+(* EVALUATION FOR CONTEXT-SENSITIVE EXTENDED SUBSTITUTION ON TERMS **********)
+
+(* Note: alternative definition of cpye *)
+inductive cpyea: ynat → ynat → relation4 genv lenv term term ≝
+| cpyea_sort : ∀G,L,d,e,k. cpyea d e G L (⋆k) (⋆k)
+| cpyea_free : ∀G,L,d,e,i. |L| ≤ i → cpyea d e G L (#i) (#i)
+| cpyea_top : ∀G,L,d,e,i. d + e ≤ yinj i → cpyea d e G L (#i) (#i)
+| cpyea_skip : ∀G,L,d,e,i. yinj i < d → cpyea d e G L (#i) (#i)
+| cpyea_subst: ∀I,G,L,K,V1,V2,W2,i,d,e. d ≤ yinj i → yinj i < d+e →
+ ⇩[i] L ≡ K.ⓑ{I}V1 → cpyea (yinj 0) (⫰(d+e-yinj i)) G K V1 V2 →
+ ⇧[0, i+1] V2 ≡ W2 → cpyea d e G L (#i) W2
+| cpyea_gref : ∀G,L,d,e,p. cpyea d e G L (§p) (§p)
+| cpyea_bind : ∀a,I,G,L,V1,V2,T1,T2,d,e.
+ cpyea d e G L V1 V2 → cpyea (⫯d) e G (L.ⓑ{I}V1) T1 T2 →
+ cpyea d e G L (ⓑ{a,I}V1.T1) (ⓑ{a,I}V2.T2)
+| cpyea_flat : ∀I,G,L,V1,V2,T1,T2,d,e.
+ cpyea d e G L V1 V2 → cpyea d e G L T1 T2 →
+ cpyea d e G L (ⓕ{I}V1.T1) (ⓕ{I}V2.T2)
+.
+
+interpretation
+ "evaluation for context-sensitive extended substitution (term) alternative"
+ 'PSubstEvalAlt G L T1 T2 d e = (cpyea d e G L T1 T2).
+
+(* Main properties **********************************************************)
+
+theorem cpye_cpyea: ∀G,L,T1,T2,d,e. ⦃G, L⦄ ⊢ T1 ▶*[d, e] 𝐍⦃T2⦄ → ⦃G, L⦄ ⊢ T1 ▶▶*[d, e] 𝐍⦃T2⦄.
+#G #L #T1 @(fqup_wf_ind_eq … G L T1) -G -L -T1
+#Z #Y #X #IH #G #L * *
+[ #k #_ #_ #_ #T2 #d #e #H -X -Y -Z >(cpye_inv_sort1 … H) -H //
+| #i #HG #HL #HT #T2 #d #e #H destruct
+ elim (cpye_inv_lref1 … H) -H *
+ /4 width=7 by cpyea_subst, cpyea_free, cpyea_top, cpyea_skip, fqup_lref/
+| #p #_ #_ #_ #T2 #d #e #H -X -Y -Z >(cpye_inv_gref1 … H) -H //
+| #a #I #V1 #T1 #HG #HL #HT #T #d #e #H destruct
+ elim (cpye_inv_bind1 … H) -H /3 width=1 by cpyea_bind/
+| #I #V1 #T1 #HG #HL #HT #T #d #e #H destruct
+ elim (cpye_inv_flat1 … H) -H /3 width=1 by cpyea_flat/
+]
+qed.
+
+(* Main inversion properties ************************************************)
+
+theorem cpyea_inv_cpye: ∀G,L,T1,T2,d,e. ⦃G, L⦄ ⊢ T1 ▶▶*[d, e] 𝐍⦃T2⦄ → ⦃G, L⦄ ⊢ T1 ▶*[d, e] 𝐍⦃T2⦄.
+#G #L #T1 #T2 #d #e #H elim H -G -L -T1 -T2 -d -e
+/2 width=7 by cpye_subst, cpye_flat, cpye_bind, cpye_skip, cpye_top, cpye_free/
+qed-.
+
+(* Advanced eliminators *****************************************************)
+
+lemma cpye_ind_alt: ∀R:ynat→ynat→relation4 genv lenv term term.
+ (∀G,L,d,e,k. R d e G L (⋆k) (⋆k)) →
+ (∀G,L,d,e,i. |L| ≤ i → R d e G L (#i) (#i)) →
+ (∀G,L,d,e,i. d + e ≤ yinj i → R d e G L (#i) (#i)) →
+ (∀G,L,d,e,i. yinj i < d → R d e G L (#i) (#i)) →
+ (∀I,G,L,K,V1,V2,W2,i,d,e. d ≤ yinj i → yinj i < d + e →
+ ⇩[i] L ≡ K.ⓑ{I}V1 → ⦃G, K⦄ ⊢ V1 ▶*[yinj O, ⫰(d+e-yinj i)] 𝐍⦃V2⦄ →
+ ⇧[O, i+1] V2 ≡ W2 → R (yinj O) (⫰(d+e-yinj i)) G K V1 V2 → R d e G L (#i) W2
+ ) →
+ (∀G,L,d,e,p. R d e G L (§p) (§p)) →
+ (∀a,I,G,L,V1,V2,T1,T2,d,e. ⦃G, L⦄ ⊢ V1 ▶*[d, e] 𝐍⦃V2⦄ →
+ ⦃G, L.ⓑ{I}V1⦄ ⊢ T1 ▶*[⫯d, e] 𝐍⦃T2⦄ → R d e G L V1 V2 →
+ R (⫯d) e G (L.ⓑ{I}V1) T1 T2 → R d e G L (ⓑ{a,I}V1.T1) (ⓑ{a,I}V2.T2)
+ ) →
+ (∀I,G,L,V1,V2,T1,T2,d,e. ⦃G, L⦄ ⊢ V1 ▶*[d, e] 𝐍⦃V2⦄ →
+ ⦃G, L⦄ ⊢ T1 ▶*[d, e] 𝐍⦃T2⦄ → R d e G L V1 V2 →
+ R d e G L T1 T2 → R d e G L (ⓕ{I}V1.T1) (ⓕ{I}V2.T2)
+ ) →
+ ∀d,e,G,L,T1,T2. ⦃G, L⦄ ⊢ T1 ▶*[d, e] 𝐍⦃T2⦄ → R d e G L T1 T2.
+#R #H1 #H2 #H3 #H4 #H5 #H6 #H7 #H8 #d #e #G #L #T1 #T2 #H elim (cpye_cpyea … H) -G -L -T1 -T2 -d -e
+/3 width=8 by cpyea_inv_cpye/
+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/cpys_cny.ma".
+include "basic_2/substitution/cpys_cpys.ma".
+include "basic_2/substitution/cpye.ma".
+
+(* EVALUATION FOR CONTEXT-SENSITIVE EXTENDED SUBSTITUTION ON TERMS **********)
+
+(* Advanced properties ******************************************************)
+
+lemma cpye_cpys_conf: ∀G,L,T,T2,d,e. ⦃G, L⦄ ⊢ T ▶*[d, e] 𝐍⦃T2⦄ →
+ ∀T1. ⦃G, L⦄ ⊢ T ▶*[d, e] T1 → ⦃G, L⦄ ⊢ T1 ▶*[d, e] T2.
+#G #L #T #T2 #d #e * #H2 #HT2 #T1 #H1 elim (cpys_conf_eq … H1 … H2) -T
+#T0 #HT10 #HT20 >(cpys_inv_cny1 … HT2 … HT20) -T2 //
+qed-.
+
\ No newline at end of file
--- /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/cny_lift.ma".
+include "basic_2/substitution/fqup.ma".
+include "basic_2/substitution/cpys_lift.ma".
+include "basic_2/substitution/cpye.ma".
+
+(* EVALUATION FOR CONTEXT-SENSITIVE EXTENDED SUBSTITUTION ON TERMS **********)
+
+(* Advanced properties ******************************************************)
+
+lemma cpye_subst: ∀I,G,L,K,V1,V2,W2,i,d,e. d ≤ yinj i → i < d + e →
+ ⇩[i] L ≡ K.ⓑ{I}V1 → ⦃G, K⦄ ⊢ V1 ▶*[O, ⫰(d+e-i)] 𝐍⦃V2⦄ →
+ ⇧[O, i+1] V2 ≡ W2 → ⦃G, L⦄ ⊢ #i ▶*[d, e] 𝐍⦃W2⦄.
+#I #G #L #K #V1 #V2 #W2 #i #d #e #Hdi #Hide #HLK *
+/4 width=13 by cpys_subst, cny_lift_subst, ldrop_fwd_drop2, conj/
+qed.
+
+lemma cpye_total: ∀G,L,T1,d,e. ∃T2. ⦃G, L⦄ ⊢ T1 ▶*[d, e] 𝐍⦃T2⦄.
+#G #L #T1 @(fqup_wf_ind_eq … G L T1) -G -L -T1
+#Z #Y #X #IH #G #L * *
+[ #k #HG #HL #HT #d #e destruct -IH /2 width=2 by ex_intro/
+| #i #HG #HL #HT #d #e destruct
+ elim (ylt_split i d) /3 width=2 by cpye_skip, ex_intro/
+ elim (ylt_split i (d+e)) /3 width=2 by cpye_top, ex_intro/
+ elim (lt_or_ge i (|L|)) /3 width=2 by cpye_free, ex_intro/
+ #Hi #Hide #Hdi elim (ldrop_O1_lt L i) // -Hi
+ #I #K #V1 #HLK elim (IH G K V1 … 0 (⫰(d+e-i))) -IH /2 width=2 by fqup_lref/
+ #V2 elim (lift_total V2 0 (i+1)) /3 width=8 by ex_intro, cpye_subst/
+| #p #HG #HL #HT #d #e destruct -IH /2 width=2 by ex_intro/
+| #a #I #V1 #T1 #HG #HL #HT #d #e destruct
+ elim (IH G L V1 … d e) // elim (IH G (L.ⓑ{I}V1) T1 … (⫯d) e) //
+ /3 width=2 by cpye_bind, ex_intro/
+| #I #V1 #T1 #HG #HL #HT #d #e destruct
+ elim (IH G L V1 … d e) // elim (IH G L T1 … d e) //
+ /3 width=2 by cpye_flat, ex_intro/
+]
+qed-.
+
+(* Advanced inversion lemmas ************************************************)
+
+lemma cpye_inv_lref1: ∀G,L,T2,d,e,i. ⦃G, L⦄ ⊢ #i ▶*[d, e] 𝐍⦃T2⦄ →
+ ∨∨ |L| ≤ i ∧ T2 = #i
+ | d + e ≤ yinj i ∧ T2 = #i
+ | yinj i < d ∧ T2 = #i
+ | ∃∃I,K,V1,V2. d ≤ yinj i & yinj i < d + e &
+ ⇩[i] L ≡ K.ⓑ{I}V1 &
+ ⦃G, K⦄ ⊢ V1 ▶*[yinj 0, ⫰(d+e-yinj i)] 𝐍⦃V2⦄ &
+ ⇧[O, i+1] V2 ≡ T2.
+#G #L #T2 #i #d #e * #H1 #H2 elim (cpys_inv_lref1 … H1) -H1
+[ #H destruct elim (cny_inv_lref … H2) -H2
+ /3 width=1 by or4_intro0, or4_intro1, or4_intro2, conj/
+| * #I #K #V1 #V2 #Hdi #Hide #HLK #HV12 #HVT2
+ @or4_intro3 @(ex5_4_intro … HLK … HVT2) (**) (* explicit constructor *)
+ /4 width=13 by cny_inv_lift_subst, ldrop_fwd_drop2, conj/
+]
+qed-.
+
+lemma cpye_inv_lref1_free: ∀G,L,T2,d,e,i. ⦃G, L⦄ ⊢ #i ▶*[d, e] 𝐍⦃T2⦄ →
+ (∨∨ |L| ≤ i | d + e ≤ yinj i | yinj i < d) → T2 = #i.
+#G #L #T2 #d #e #i #H * elim (cpye_inv_lref1 … H) -H * //
+#I #K #V1 #V2 #Hdi #Hide #HLK #_ #_ #H
+[ elim (lt_refl_false i) -d
+ @(lt_to_le_to_lt … H) -H /2 width=5 by ldrop_fwd_length_lt2/ (**) (* full auto slow: 19s *)
+]
+elim (ylt_yle_false … H) //
+qed-.
+
+lemma cpye_inv_lref1_lget: ∀G,L,T2,d,e,i. ⦃G, L⦄ ⊢ #i ▶*[d, e] 𝐍⦃T2⦄ →
+ ∀I,K,V1. ⇩[i] L ≡ K.ⓑ{I}V1 →
+ ∨∨ d + e ≤ yinj i ∧ T2 = #i
+ | yinj i < d ∧ T2 = #i
+ | ∃∃V2. d ≤ yinj i & yinj i < d + e &
+ ⦃G, K⦄ ⊢ V1 ▶*[yinj 0, ⫰(d+e-yinj i)] 𝐍⦃V2⦄ &
+ ⇧[O, i+1] V2 ≡ T2.
+#G #L #T2 #d #e #i #H #I #K #V1 #HLK elim (cpye_inv_lref1 … H) -H *
+[ #H elim (lt_refl_false i) -T2 -d
+ @(lt_to_le_to_lt … H) -H /2 width=5 by ldrop_fwd_length_lt2/
+| /3 width=1 by or3_intro0, conj/
+| /3 width=1 by or3_intro1, conj/
+| #Z #Y #X1 #X2 #Hdi #Hide #HLY #HX12 #HXT2
+ lapply (ldrop_mono … HLY … HLK) -HLY -HLK #H destruct
+ /3 width=3 by or3_intro2, ex4_intro/
+]
+qed-.
+
+lemma cpye_inv_lref1_subst_ex: ∀G,L,T2,d,e,i. ⦃G, L⦄ ⊢ #i ▶*[d, e] 𝐍⦃T2⦄ →
+ ∀I,K,V1. d ≤ yinj i → yinj i < d + e →
+ ⇩[i] L ≡ K.ⓑ{I}V1 →
+ ∃∃V2. ⦃G, K⦄ ⊢ V1 ▶*[yinj 0, ⫰(d+e-yinj i)] 𝐍⦃V2⦄ &
+ ⇧[O, i+1] V2 ≡ T2.
+#G #L #T2 #d #e #i #H #I #K #V1 #Hdi #Hide #HLK
+elim (cpye_inv_lref1_lget … H … HLK) -H * /2 width=3 by ex2_intro/
+#H elim (ylt_yle_false … H) //
+qed-.
+
+lemma cpye_inv_lref1_subst: ∀G,L,T2,d,e,i. ⦃G, L⦄ ⊢ #i ▶*[d, e] 𝐍⦃T2⦄ →
+ ∀I,K,V1,V2. d ≤ yinj i → yinj i < d + e →
+ ⇩[i] L ≡ K.ⓑ{I}V1 → ⇧[O, i+1] V2 ≡ T2 →
+ ⦃G, K⦄ ⊢ V1 ▶*[yinj 0, ⫰(d+e-yinj i)] 𝐍⦃V2⦄.
+#G #L #T2 #d #e #i #H #I #K #V1 #V2 #Hdi #Hide #HLK #HVT2
+elim (cpye_inv_lref1_subst_ex … H … HLK) -H -HLK //
+#X2 #H0 #HXT2 lapply (lift_inj … HXT2 … HVT2) -HXT2 -HVT2 #H destruct //
+qed-.
+
+(* Inversion lemmas on relocation *******************************************)
+
+lemma cpye_inv_lift1_le: ∀G,L,U1,U2,dt,et. ⦃G, L⦄ ⊢ U1 ▶*[dt, et] 𝐍⦃U2⦄ →
+ ∀K,s,d,e. ⇩[s, d, e] L ≡ K → ∀T1. ⇧[d, e] T1 ≡ U1 →
+ dt + et ≤ d →
+ ∃∃T2. ⦃G, K⦄ ⊢ T1 ▶*[dt, et] 𝐍⦃T2⦄ & ⇧[d, e] T2 ≡ U2.
+#G #L #U1 #U2 #dt #et * #HU12 #HU2 #K #s #d #e #HLK #T1 #HTU1 #Hdetd
+elim (cpys_inv_lift1_le … HU12 … HLK … HTU1) -U1 // #T2 #HT12 #HTU2
+lapply (cny_inv_lift_le … HU2 … HLK … HTU2 ?) -L
+/3 width=3 by ex2_intro, conj/
+qed-.
+
+lemma cpye_inv_lift1_be: ∀G,L,U1,U2,dt,et. ⦃G, L⦄ ⊢ U1 ▶*[dt, et] 𝐍⦃U2⦄ →
+ ∀K,s,d,e. ⇩[s, d, e] L ≡ K → ∀T1. ⇧[d, e] T1 ≡ U1 →
+ dt ≤ d → yinj d + e ≤ dt + et →
+ ∃∃T2. ⦃G, K⦄ ⊢ T1 ▶*[dt, et - e] 𝐍⦃T2⦄ & ⇧[d, e] T2 ≡ U2.
+#G #L #U1 #U2 #dt #et * #HU12 #HU2 #K #s #d #e #HLK #T1 #HTU1 #Hdtd #Hdedet
+elim (cpys_inv_lift1_be … HU12 … HLK … HTU1) -U1 // #T2 #HT12 #HTU2
+lapply (cny_inv_lift_be … HU2 … HLK … HTU2 ? ?) -L
+/3 width=3 by ex2_intro, conj/
+qed-.
+
+lemma cpye_inv_lift1_ge: ∀G,L,U1,U2,dt,et. ⦃G, L⦄ ⊢ U1 ▶*[dt, et] 𝐍⦃U2⦄ →
+ ∀K,s,d,e. ⇩[s, d, e] L ≡ K → ∀T1. ⇧[d, e] T1 ≡ U1 →
+ yinj d + e ≤ dt →
+ ∃∃T2. ⦃G, K⦄ ⊢ T1 ▶*[dt - e, et] 𝐍⦃T2⦄ & ⇧[d, e] T2 ≡ U2.
+#G #L #U1 #U2 #dt #et * #HU12 #HU2 #K #s #d #e #HLK #T1 #HTU1 #Hdedt
+elim (cpys_inv_lift1_ge … HU12 … HLK … HTU1) -U1 // #T2 #HT12 #HTU2
+lapply (cny_inv_lift_ge … HU2 … HLK … HTU2 ?) -L
+/3 width=3 by ex2_intro, conj/
+qed-.
+
+lemma cpye_inv_lift1_ge_up: ∀G,L,U1,U2,dt,et. ⦃G, L⦄ ⊢ U1 ▶*[dt, et] 𝐍⦃U2⦄ →
+ ∀K,s,d,e. ⇩[s, d, e] L ≡ K → ∀T1. ⇧[d, e] T1 ≡ U1 →
+ d ≤ dt → dt ≤ yinj d + e → yinj d + e ≤ dt + et →
+ ∃∃T2. ⦃G, K⦄ ⊢ T1 ▶*[d, dt + et - (yinj d + e)] 𝐍⦃T2⦄ &
+ ⇧[d, e] T2 ≡ U2.
+#G #L #U1 #U2 #dt #et * #HU12 #HU2 #K #s #d #e #HLK #T1 #HTU1 #Hddt #Hdtde #Hdedet
+elim (cpys_inv_lift1_ge_up … HU12 … HLK … HTU1) -U1 // #T2 #HT12 #HTU2
+lapply (cny_inv_lift_ge_up … HU2 … HLK … HTU2 ? ? ?) -L
+/3 width=3 by ex2_intro, conj/
+qed-.
+
+lemma cpye_inv_lift1_subst: ∀G,L,W1,W2,d,e. ⦃G, L⦄ ⊢ W1 ▶*[d, e] 𝐍⦃W2⦄ →
+ ∀K,V1,i. ⇩[i+1] L ≡ K → ⇧[O, i+1] V1 ≡ W1 →
+ d ≤ yinj i → i < d + e →
+ ∃∃V2. ⦃G, K⦄ ⊢ V1 ▶*[O, ⫰(d+e-i)] 𝐍⦃V2⦄ & ⇧[O, i+1] V2 ≡ W2.
+#G #L #W1 #W2 #d #e * #HW12 #HW2 #K #V1 #i #HLK #HVW1 #Hdi #Hide
+elim (cpys_inv_lift1_subst … HW12 … HLK … HVW1) -W1 // #V2 #HV12 #HVW2
+lapply (cny_inv_lift_subst … HLK HW2 HVW2) -L
+/3 width=3 by ex2_intro, 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/relocation/cny.ma".
+include "basic_2/substitution/cpys.ma".
+
+(* CONTEXT-SENSITIVE EXTENDED MULTIPLE SUBSTITUTION FOR TERMS ***************)
+
+(* Inversion lemmas on normality for extended substitution ******************)
+
+lemma cpys_inv_cny1: ∀G,L,T1,d,e. ⦃G, L⦄ ⊢ ▶[d, e] 𝐍⦃T1⦄ →
+ ∀T2. ⦃G, L⦄ ⊢ T1 ▶*[d, e] T2 → T1 = T2.
+#G #L #T1 #d #e #HT1 #T2 #H @(cpys_ind … H) -T2 //
+#T #T2 #_ #HT2 #IHT1 destruct <(HT1 … HT2) -T //
+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/pdeltaconvstar_6.ma".
+include "basic_2/substitution/cpye_lift.ma".
+
+(* CONTEXT-SENSITIVE EXTENDED DELTA-EQUIVALENCE FOR TERMS *******************)
+
+definition cpzs: ynat → ynat → relation4 genv lenv term term ≝
+ λd,e,G,L,T1,T2.
+ ∃∃T. ⦃G, L⦄ ⊢ T1 ▶*[d, e] 𝐍⦃T⦄ & ⦃G, L⦄ ⊢ T2 ▶*[d, e] 𝐍⦃T⦄.
+
+interpretation "context-sensitive extended delta-equivalence (term)"
+ 'PDeltaConvStar G L T1 d e T2 = (cpzs d e G L T1 T2).
+
+(* Basic properties **********************************************************)
+
+lemma cpye_div: ∀G,L,T1,T,d,e. ⦃G, L⦄ ⊢ T1 ▶*[d, e] 𝐍⦃T⦄ →
+ ∀T2. ⦃G, L⦄ ⊢ T2 ▶*[d, e] 𝐍⦃T⦄ → ⦃G, L⦄ ⊢ T1 ◆*[d, e] T2.
+/2 width=3 by ex2_intro/ qed.
+
+lemma cpzs_refl: ∀G,L,d,e. reflexive … (cpzs d e G L).
+#G #L #d #e #T elim (cpye_total G L T d e) /2 width=3 by cpye_div/
+qed.
+
+lemma cpzs_bind: ∀G,L,V1,V2,d,e. ⦃G, L⦄ ⊢ V1 ◆*[d, e] V2 →
+ ∀I,T1,T2. ⦃G, L.ⓑ{I}V1⦄ ⊢ T1 ◆*[⫯d, e] T2 →
+ ∀a. ⦃G, L⦄ ⊢ ⓑ{a,I}V1.T1 ◆*[d, e] ⓑ{a,I}V2.T2.
+#G #L #V1 #V2 #d #e * #V #HV1 #HV2 #I #T1 #T2 *
+/5 width=10 by cpye_div, cpye_bind, leqy_cpye_trans, cny_bind, lsuby_succ/
+qed.
+
+lemma cpzs_flat: ∀G,L,V1,V2,d,e. ⦃G, L⦄ ⊢ V1 ◆*[d, e] V2 →
+ ∀T1,T2. ⦃G, L⦄ ⊢ T1 ◆*[d, e] T2 →
+ ∀I. ⦃G, L⦄ ⊢ ⓕ{I}V1.T1 ◆*[d, e] ⓕ{I}V2.T2.
+#G #L #V1 #V2 #d #e * #V #HV1 #HV2 #T1 #T2 *
+/3 width=5 by cpye_div, cpye_flat, cny_flat/
+qed.
+
+(* Basic inversion lemmas ***************************************************)
+
+lemma cpzs_inv_sort: ∀G,L,d,e,k1,k2. ⦃G, L⦄ ⊢ ⋆k1 ◆*[d, e] ⋆k2 → k1 = k2.
+#G #L #d #e #k1 #k2 * #X #H1 #H2
+lapply (cpye_inv_sort1 … H1) -H1 #H1
+lapply (cpye_inv_sort1 … H2) -H2 #H2
+destruct //
+qed-.
+
+lemma cpzs_inv_bind: ∀a1,a2,I1,I2,G,L,V1,V2,T1,T2,d,e. ⦃G, L⦄ ⊢ ⓑ{a1,I1}V1.T1 ◆*[d, e] ⓑ{a2,I2}V2.T2 →
+ ∧∧ a1 = a2 & I1 = I2
+ & ⦃G, L⦄ ⊢ V1 ◆*[d, e] V2 & ⦃G, L.ⓑ{I1}V1⦄ ⊢ T1 ◆*[⫯d, e] T2.
+#a1 #a2 #I1 #I2 #G #L #V1 #V2 #T1 #T2 #d #e * #X #H1 #H2
+elim (cpye_inv_bind1 … H1) -H1 #V2 #T2 #HV12 #HT12 #H1
+elim (cpye_inv_bind1 … H2) -H2 #W2 #U2 #HW12 #HU12 #H2
+destruct /5 width=8 by cpye_div, leqy_cpye_trans, lsuby_succ, and4_intro/
+qed-.
+
+lemma cpzs_inv_flat: ∀I1,I2,G,L,V1,V2,T1,T2,d,e. ⦃G, L⦄ ⊢ ⓕ{I1}V1.T1 ◆*[d, e] ⓕ{I2}V2.T2 →
+ ∧∧ I1 = I2
+ & ⦃G, L⦄ ⊢ V1 ◆*[d, e] V2 & ⦃G, L⦄ ⊢ T1 ◆*[d, e] T2.
+#I1 #I2 #G #L #V1 #V2 #T1 #T2 #d #e * #X #H1 #H2
+elim (cpye_inv_flat1 … H1) -H1 #V2 #T2 #HV12 #HT12 #H1
+elim (cpye_inv_flat1 … H2) -H2 #W2 #U2 #HW12 #HU12 #H2
+destruct /3 width=3 by cpye_div, and3_intro/
+qed-.
+
+lemma cpzs_inv_flat_bind: ∀a2,I1,I2,G,L,V1,V2,T1,T2,d,e. ⦃G, L⦄ ⊢ ⓕ{I1}V1.T1 ◆*[d, e] ⓑ{a2,I2}V2.T2 → ⊥.
+#a2 #I1 #I2 #G #L #V1 #V2 #T1 #T2 #d #e * #X #H1 #H2
+elim (cpye_inv_flat1 … H1) -H1 #V2 #T2 #HV12 #HT12 #H1
+elim (cpye_inv_bind1 … H2) -H2 #W2 #U2 #HW12 #HU12 #H2
+destruct
+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/cpye_lift.ma".
+include "basic_2/substitution/lleq_alt.ma".
+
+(* LAZY EQUIVALENCE FOR LOCAL ENVIRONMENTS **********************************)
+
+(* Forward lemmas on evaluation for extended substitution *******************)
+
+lemma lleq_fwd_cpye: ∀L1,L2,T,d. L1 ⋕[T, d] L2 → ∀G,T1. ⦃G, L1⦄ ⊢ T ▶*[d, ∞] 𝐍⦃T1⦄ →
+ ∀T2. ⦃G, L2⦄ ⊢ T ▶*[d, ∞] 𝐍⦃T2⦄ → T1 = T2.
+#L1 #L2 #T #d #H @(lleq_ind_alt … H) -L1 -L2 -T -d
+[ #L1 #L2 #d #k #_ #G #T1 #H1 #T2 #H2
+ >(cpye_inv_sort1 … H1) -H1 >(cpye_inv_sort1 … H2) -H2 //
+| #L1 #L2 #d #i #_ #Hid #G #T1 #H1 #T2 #H2
+ >(cpye_inv_lref1_free … H1) -H1 [ >(cpye_inv_lref1_free … H2) -H2 ]
+ /2 width=1 by or3_intro2/
+| #I1 #I2 #L1 #L2 #K1 #K2 #V #d #i #Hdi #HLK1 #HLK2 #_ #IHV #G #T1 #H1 #T2 #H2
+ elim (cpye_inv_lref1_subst_ex … H1 … HLK1) -H1 -HLK1 //
+ elim (cpye_inv_lref1_subst_ex … H2 … HLK2) -H2 -HLK2 //
+ >yminus_Y_inj #V2 #HV2 #HVT2 #V1 #HV1 #HVT1
+ lapply (IHV … HV1 … HV2) -IHV -HV1 -HV2 #H destruct /2 width=5 by lift_mono/
+| #L1 #L2 #d #i #_ #HL1 #HL2 #G #T1 #H1 #T2 #H2
+ >(cpye_inv_lref1_free … H1) -H1 [ >(cpye_inv_lref1_free … H2) -H2 ]
+ /2 width=1 by or3_intro0/
+| #L1 #L2 #d #p #_ #G #T1 #H1 #T2 #H2
+ >(cpye_inv_gref1 … H1) -H1 >(cpye_inv_gref1 … H2) -H2 //
+| #a #I #L1 #L2 #V #T #d #_ #_ #IHV #IHT #G #X1 #H1 #X2 #H2
+ elim (cpye_inv_bind1 … H1) -H1 #V1 #T1 #HV1 #HT1 #H destruct
+ elim (cpye_inv_bind1 … H2) -H2 #V2 #T2 #HV2 #HT2 #H destruct
+ /3 width=3 by eq_f2/
+| #I #L1 #L2 #V #T #d #_ #_ #IHV #IHT #G #X1 #H1 #X2 #H2
+ elim (cpye_inv_flat1 … H1) -H1 #V1 #T1 #HV1 #HT1 #H destruct
+ elim (cpye_inv_flat1 … H2) -H2 #V2 #T2 #HV2 #HT2 #H destruct
+ /3 width=3 by eq_f2/
+]
+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/cpye_cpye.ma".
+include "basic_2/reduction/lpx_cpys.ma".
+
+axiom cpx_cpys_conf_lpx: ∀h,g,G,d,e.
+ ∀L0,T0,T1. ⦃G, L0⦄ ⊢ T0 ➡[h, g] T1 → ∀L1. ⦃G, L0⦄ ⊢ ➡[h, g] L1 →
+ ∀T2. ⦃G, L0⦄ ⊢ T0 ▶*[d, e] T2 →
+ ∃∃T. ⦃G, L1⦄ ⊢ T1 ▶*[d, e] T & ⦃G, L0⦄ ⊢ T2 ➡[h, g] T.
+
+(* SN EXTENDED PARALLEL REDUCTION ON LOCAL ENVIRONMENTS *********************)
+
+(* Forward lemmas on evaluation for extended substitution *******************)
+
+lemma cpx_cpys_cpye_fwd_lpx: ∀h,g,G,L1,T1,T2. ⦃G, L1⦄ ⊢ T1 ➡[h, g] T2 →
+ ∀L2. ⦃G, L1⦄ ⊢ ➡[h, g] L2 →
+ ∀U1,d,e. ⦃G, L1⦄ ⊢ T1 ▶*[d, e] U1 →
+ ∀U2. ⦃G, L2⦄ ⊢ T2 ▶*[d, e] 𝐍⦃U2⦄ →
+ ⦃G, L1⦄ ⊢ U1 ➡[h, g] U2.
+#h #g #G #L1 #T1 #T2 #HT12 #L2 #HL12 #U1 #d #e #HTU1
+elim (cpx_cpys_conf_lpx … HT12 … HL12 … HTU1) -T1
+/3 width=9 by cpx_cpys_trans_lpx, cpye_cpys_conf/
+qed-.
+
+lemma cpx_cpye_fwd_lpx: ∀h,g,G,L1,T1,T2. ⦃G, L1⦄ ⊢ T1 ➡[h, g] T2 →
+ ∀L2. ⦃G, L1⦄ ⊢ ➡[h, g] L2 →
+ ∀U1,d,e. ⦃G, L1⦄ ⊢ T1 ▶*[d, e] 𝐍⦃U1⦄ →
+ ∀U2. ⦃G, L2⦄ ⊢ T2 ▶*[d, e] 𝐍⦃U2⦄ →
+ ⦃G, L1⦄ ⊢ U1 ➡[h, g] U2.
+#h #g #G #L1 #T1 #T2 #HT12 #L2 #HL12 #U1 #d #e *
+/2 width=9 by cpx_cpys_cpye_fwd_lpx/
+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/cpye_lift.ma".
+include "basic_2/reduction/lpx_cpye.ma".
+include "basic_2/computation/cpxs_cpxs.ma".
+include "basic_2/computation/lpxs.ma".
+
+(* SN EXTENDED PARALLEL COMPUTATION ON LOCAL ENVIRONMENTS *******************)
+
+(* Forward lemmas on evaluation for extended substitution *******************)
+
+lemma cpx_cpye_fwd_lpxs: ∀h,g,G,L1,L2. ⦃G, L1⦄ ⊢ ➡*[h, g] L2 →
+ ∀T1,T2. ⦃G, L1⦄ ⊢ T1 ➡[h, g] T2 →
+ ∀U1,d,e. ⦃G, L1⦄ ⊢ T1 ▶*[d, e] 𝐍⦃U1⦄ →
+ ∀U2. ⦃G, L2⦄ ⊢ T2 ▶*[d, e] 𝐍⦃U2⦄ →
+ ⦃G, L1⦄ ⊢ U1 ➡*[h, g] U2.
+#h #g #G #L1 #L2 #H @(lpxs_ind_dx … H) -L1
+[ /3 width=9 by cpx_cpxs, cpx_cpye_fwd_lpx/
+| #L1 #L #HL1 #_ #IHL2 #T1 #T2 #HT12 #U1 #d #e #HTU1 #U2 #HTU2
+ elim (cpye_total G L T2 d e) #X2 #HTX2
+ lapply (cpx_cpye_fwd_lpx … HT12 … HL1 … HTU1 … HTX2) -T1
+ /4 width=9 by lpx_cpxs_trans, cpxs_strap2/ (**) (* full auto too long: 41s *)
+]
+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 *)
+(* *)
+(**************************************************************************)
+
+(* NOTATION FOR THE FORMAL SYSTEM λδ ****************************************)
+
+notation "hvbox( ⦃ term 46 G , break term 46 L ⦄ ⊢ break term 46 T1 break ◆ * [ term 46 d , break term 46 e ] break term 46 T2 )"
+ non associative with precedence 45
+ for @{ 'PDeltaConvStar $G $L $T1 $d $e $T2 }.
--- /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( ⦃ term 46 G, break term 46 L ⦄ ⊢ break term 46 T1 ▶ * break [ term 46 d , break term 46 e ] break 𝐍 ⦃ term 46 T2 ⦄ )"
+ non associative with precedence 45
+ for @{ 'PSubstEval $G $L $T1 $T2 $d $e }.
--- /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( ⦃ term 46 G, break term 46 L ⦄ ⊢ break term 46 T1 ▶ ▶ * break [ term 46 d , break term 46 e ] break 𝐍 ⦃ term 46 T2 ⦄ )"
+ non associative with precedence 45
+ for @{ 'PSubstEvalAlt $G $L $T1 $T2 $d $e }.
--- /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( ⦃ term 46 G, break term 46 L ⦄ ⊢ ▶ break [ term 46 d , break term 46 e ] 𝐍 break ⦃ term 46 T ⦄ )"
+ non associative with precedence 45
+ for @{ 'PSubstNormal $G $L $T $d $e }.
--- /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( L1 ⧣ break [ term 46 T , break term 46 d ] break term 46 L2 )"
+ non associative with precedence 45
+ for @{ 'LazyNegatedEq $T $d $L1 $L2 }.
--- /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( L1 ⧣ ⧣ break [ term 46 T , break term 46 d ] break term 46 L2 )"
+ non associative with precedence 45
+ for @{ 'LazyNegatedEqAlt $T $d $L1 $L2 }.
--- /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/lazynegatedeq_4.ma".
+include "basic_2/substitution/lleq.ma".
+
+(* NEGATED LAZY EQUIVALENCE FOR LOCAL ENVIRONMENTS **************************)
+
+definition llneq: relation4 ynat term lenv lenv ≝
+ λd,T,L1,L2. |L1| = |L2| ∧ (L1 ⋕[T, d] L2 → ⊥).
+
+interpretation
+ "negated lazy equivalence (local environment)"
+ 'LazyNegatedEq T d L1 L2 = (llneq d T L1 L2).
--- /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/lazynegatedeqalt_4.ma".
+include "basic_2/substitution/lleq_lleq.ma".
+include "basic_2/substitution/llneq.ma".
+
+(* NEGATED LAZY EQUIVALENCE FOR LOCAL ENVIRONMENTS **************************)
+
+(* alternative definition of llneq *)
+inductive llneqa: relation4 ynat term lenv lenv ≝
+| llneqa_neq: ∀I1,I2,L1,L2,K1,K2,V1,V2,d,i. d ≤ yinj i →
+ ⇩[i]L1 ≡ K1.ⓑ{I1}V1 → ⇩[i]L2 ≡ K2.ⓑ{I2}V2 →
+ |K1| = |K2| → (V1 = V2 → ⊥) → llneqa d (#i) L1 L2
+| llneqa_eq : ∀I1,I2,L1,L2,K1,K2,V,d,i. d ≤ yinj i →
+ ⇩[i]L1 ≡ K1.ⓑ{I1}V → ⇩[i]L2 ≡ K2.ⓑ{I2}V →
+ llneqa 0 (V) K1 K2 → llneqa d (#i) L1 L2
+| llneqa_bind_sn: ∀a,I,L1,L2,V,T,d.
+ llneqa d V L1 L2 → llneqa d (ⓑ{a,I}V.T) L1 L2
+| llneqa_bind_dx: ∀a,I,L1,L2,V,T,d.
+ llneqa (⫯d) T (L1.ⓑ{I}V) (L2.ⓑ{I}V) → llneqa d (ⓑ{a,I}V.T) L1 L2
+| llneqa_flat_sn: ∀I,L1,L2,V,T,d.
+ llneqa d V L1 L2 → llneqa d (ⓕ{I}V.T) L1 L2
+| llneqa_flat_dx: ∀I,L1,L2,V,T,d.
+ llneqa d T L1 L2 → llneqa d (ⓕ{I}V.T) L1 L2
+.
+
+interpretation
+ "negated lazy equivalence (local environment) alternative"
+ 'LazyNegatedEqAlt T d L1 L2 = (llneqa d T L1 L2).
+
+(* Main properties **********************************************************)
+
+theorem llneq_llneqa: ∀T,L1,L2,d. L1 ⧣[T, d] L2 → L1 ⧣⧣[T, d] L2.
+#T #L1 @(f2_ind … rfw … L1 T) -L1 -T
+#n #IH #L1 * *
+[ #k #Hn #L2 #d * #HL12 #H elim H /2 width=1 by lleq_sort/
+| #i #Hn #L2 #d * #HL12 #H elim (ylt_split i d) #Hdi
+ [ elim H /2 width=1 by lleq_skip/ ]
+ elim (lt_or_ge i (|L1|)) #HiL1
+ [2: elim H /3 width=3 by lleq_free, le_repl_sn_aux/ ]
+ elim (ldrop_O1_lt … HiL1) #I1 #K1 #V1 #HLK1
+ elim (ldrop_O1_lt L2 i) /2 width=1 by/ #I2 #K2 #V2 #HLK2
+ lapply (ldrop_fwd_length_eq1 … HLK1 HLK2 HL12) normalize
+ elim (eq_term_dec V1 V2) #HnV12 destruct
+ [2: #H @(llneqa_neq … HLK1 … HLK2) /2 width=1 by/ ] (**) (* explicit constructor *)
+ elim (lleq_dec V2 K1 K2 0) #HnV2 [ elim H /2 width=8 by lleq_lref/ ]
+ #H @(llneqa_eq … HLK1 … HLK2) /4 width=2 by ldrop_fwd_rfw, conj/ (**) (* explicit constructor *)
+| #p #Hn #L2 #d * #HL12 #H elim H /2 width=1 by lleq_gref/
+| #a #I #V #T #Hn #L2 #d * #HL12 #H destruct elim (nlleq_inv_bind … H) -H
+ [ /5 width=1 by llneqa_bind_sn, conj/
+ | #H @llneqa_bind_dx @IH // @conj normalize /2 width=1 by/
+ ]
+| #I #V #T #Hn #L2 #d * #HL12 #H destruct elim (nlleq_inv_flat … H) -H
+ /5 width=1 by llneqa_flat_dx, llneqa_flat_sn, 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/substitution/llneq_alt.ma".
+
+(* NEGATED LAZY EQUIVALENCE FOR LOCAL ENVIRONMENTS **************************)
+
+(* Advanced inversion lemmas ************************************************)
+
+lemma llneq_inv_atom1: ∀L1,L2,T,d. L1 ⧣⧣[T, d] L2 → |L1| ≤ d → ⊥.
+#L1 #L2 #T #d #H elim H -L1 -L2 -T -d /2 width=1 by/
+[ #I1 #I2 #L1 #L2 #K1 #K2 #V1 #V2 #d #i #Hdi #HLK1 #_ #_ #_
+ >(ldrop_fwd_length … HLK1) -HLK1 normalize
+ #H lapply (yle_trans … H … Hdi) -d
+ /3 width=4 by yle_inv_inj, le_plus_xySz_x_false/
+| #I1 #I2 #L1 #L2 #K1 #K2 #V #d #i #Hdi #HLK1 #_ #_ #_
+ >(ldrop_fwd_length … HLK1) -HLK1 normalize
+ #H lapply (yle_trans … H … Hdi) -d
+ /3 width=4 by yle_inv_inj, le_plus_xySz_x_false/
+| #a #I #L1 <yplus_inj /4 width=1 by yle_succ/
+]
+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/llneq_alt.ma".
+include "basic_2/computation/lpxs_ldrop.ma".
+include "basic_2/computation/lpxs_cpxs.ma".
+
+(* SN EXTENDED PARALLEL COMPUTATION FOR LOCAL ENVIRONMENTS ******************)
+
+(* Forward lemmas on negated lazy equivalence for local environments ********)
+
+lemma lpxs_llneq_fwd_cpxs: ∀h,g,G,L1,L2,T,d. L1 ⧣⧣[T, d] L2 → ⦃G, L1⦄ ⊢ ➡*[h, g] L2 →
+ ∃∃T1,T2. ⦃G, L1⦄ ⊢ T ▶*[d, ∞] T1 & ⦃G, L2⦄ ⊢ T ▶*[d, ∞] T2 &
+ ⦃G, L1⦄ ⊢ T1 ➡*[h, g] T2 & (T1 = T2 → ⊥).
+#h #g #G #L1 #L2 #T #d #H elim H -L1 -L2 -T -d
+[ #I1 #I2 #L1 #L2 #K1 #K2 #V1 #V2 #d #i #Hdi #HLK1 #HLK2 #_ #HnV12 #HL12
+ elim (lpxs_ldrop_conf … HLK1 … HL12) -HL12 #Y #H #HY
+ elim (lpxs_inv_pair1 … H) -H #Z #X #_ #HV12 #H destruct
+ lapply (ldrop_mono … HY … HLK2) -HY #H destruct
+ lapply (ldrop_fwd_drop2 … HLK1) #H2LK1
+ elim (lift_total V1 0 (i+1)) #T1 #HVT1
+ elim (lift_total V2 0 (i+1)) #T2 #HVT2
+ @(ex4_2_intro … T1 T2) /3 width=10 by cpxs_lift, cpys_subst, lift_inj/ (**) (* explicit constructor *)
+| #I1 #I2 #L1 #L2 #K1 #K2 #V #d #i #Hdi #HLK1 #HLK2 #_ #IHK12 #HL12
+ elim (lpxs_ldrop_conf … HLK1 … HL12) -HL12 #Y #H #HY
+ elim (lpxs_inv_pair1 … H) -H #Z #X #HK12 #_ #H destruct
+ lapply (ldrop_mono … HY … HLK2) -HY #H destruct
+ elim (IHK12 HK12) -IHK12 -HK12 #V1 #V2 #HV1 #HV2 #HV12 #HnV12
+ lapply (ldrop_fwd_drop2 … HLK1) #H2LK1
+ elim (lift_total V1 0 (i+1)) #T1 #HVT1
+ elim (lift_total V2 0 (i+1)) #T2 #HVT2
+ @(ex4_2_intro … T1 T2) /3 width=10 by cpxs_lift, cpys_subst_Y2, lift_inj/ (**) (* explicit constructor *)
+| #a #I #L1 #L2 #V #T #d #_ #IHV #HL12 elim (IHV HL12) -IHV -HL12
+ #V1 #V2 #HV1 #HV2 #HV12 #HnV12
+ @(ex4_2_intro … (ⓑ{a,I}V1.T) (ⓑ{a,I}V2.T)) /2 width=1 by cpys_bind, cpxs_pair_sn/
+ #H destruct /2 width=1 by/
+| #a #I #L1 #L2 #V #T #d #_ #IHT #HL12 elim (IHT ?) /2 width=1 by lpxs_pair_refl/ -IHT -HL12
+ #T1 #T2 #HT1 #HT2 #HT12 #HnT12
+ @(ex4_2_intro … (ⓑ{a,I}V.T1) (ⓑ{a,I}V.T2)) /2 width=1 by cpys_bind, cpxs_bind_dx/
+ #H destruct /2 width=1 by/
+| #I #L1 #L2 #V #T #d #_ #IHV #HL12 elim (IHV HL12) -IHV -HL12
+ #V1 #V2 #HV1 #HV2 #HV12 #HnV12
+ @(ex4_2_intro … (ⓕ{I}V1.T) (ⓕ{I}V2.T)) /2 width=1 by cpys_flat, cpxs_pair_sn/
+ #H destruct /2 width=1 by/
+| #I #L1 #L2 #V #T #d #_ #IHT #HL12 elim (IHT HL12) -IHT -HL12
+ #T1 #T2 #HT1 #HT2 #HT12 #HnT12
+ @(ex4_2_intro … (ⓕ{I}V.T1) (ⓕ{I}V.T2)) /2 width=1 by cpys_flat, cpxs_flat_dx/
+ #H destruct /2 width=1 by/
+]
+qed-.
+
+lemma lpxs_nlleq_fwd_cpxs: ∀h,g,G,L1,L2,T,d. ⦃G, L1⦄ ⊢ ➡*[h, g] L2 →
+ (L1 ⋕[T, d] L2 → ⊥) →
+ ∃∃T1,T2. ⦃G, L1⦄ ⊢ T ▶*[d, ∞] T1 & ⦃G, L2⦄ ⊢ T ▶*[d, ∞] T2 &
+ ⦃G, L1⦄ ⊢ T1 ➡*[h, g] T2 & (T1 = T2 → ⊥).
+/5 width=4 by lpxs_llneq_fwd_cpxs, lpxs_fwd_length, llneq_llneqa, 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 *)
-(* *)
-(**************************************************************************)
-
-(* NOTATION FOR THE FORMAL SYSTEM λδ ****************************************)
-
-notation "hvbox( G ⊢ ⋕ ⬊ * break [ term 46 h , break term 46 g , break term 46 T ] break term 46 L )"
- non associative with precedence 45
- for @{ 'LazySN $h $g $T $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 @{ 'LazySN $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( ⦃ term 46 G, break term 46 L ⦄ ⊢ break term 46 T1 ▶ * break [ term 46 d , break term 46 e ] break 𝐍 ⦃ term 46 T2 ⦄ )"
- non associative with precedence 45
- for @{ 'PSubstEval $G $L $T1 $T2 $d $e }.
+++ /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( ⦃ term 46 G, break term 46 L ⦄ ⊢ break term 46 T1 ▶ ▶ * break [ term 46 d , break term 46 e ] break 𝐍 ⦃ term 46 T2 ⦄ )"
- non associative with precedence 45
- for @{ 'PSubstEvalAlt $G $L $T1 $T2 $d $e }.
+++ /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( ⦃ term 46 G, break term 46 L ⦄ ⊢ ▶ break [ term 46 d , break term 46 e ] 𝐍 break ⦃ term 46 T ⦄ )"
- non associative with precedence 45
- for @{ 'PSubstNormal $G $L $T $d $e }.
(* CONTEXT-SENSITIVE EXTENDED PARALLEL REDUCTION FOR TERMS ******************)
+(* Properties on local environment refinement for extended substitution *****)
+
+lemma lsuby_cpx_trans: ∀h,g,G. lsub_trans … (cpx h g G) (lsuby 0 (∞)).
+#h #g #G #L1 #T1 #T2 #H elim H -G -L1 -T1 -T2
+[ //
+| /2 width=2 by cpx_sort/
+| #I #G #L1 #K1 #V1 #V2 #W2 #i #HLK1 #_ #HVW2 #IHV12 #L2 #HL12
+ elim (lsuby_fwd_ldrop2_be … HL12 … HLK1) // -HL12 -HLK1 /3 width=7 by cpx_delta/
+|4,9: /4 width=1 by cpx_bind, cpx_beta, lsuby_pair_O_Y/
+|5,7,8: /3 width=1 by cpx_flat, cpx_tau, cpx_ti/
+|6,10: /4 width=3 by cpx_zeta, cpx_theta, lsuby_pair_O_Y/
+]
+qed-.
+
(* Properties on context-sensitive extended multiple substitution for terms *)
lemma cpys_cpx: ∀h,g,G,L,T1,T2,d,e. ⦃G, L⦄ ⊢ T1 ▶*[d, e] T2 → ⦃G, L⦄ ⊢ T1 ➡[h, g] T2.
+++ /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/cpye_cpye.ma".
-include "basic_2/reduction/lpx_cpys.ma".
-
-axiom cpx_cpys_conf_lpx: ∀h,g,G,d,e.
- ∀L0,T0,T1. ⦃G, L0⦄ ⊢ T0 ➡[h, g] T1 → ∀L1. ⦃G, L0⦄ ⊢ ➡[h, g] L1 →
- ∀T2. ⦃G, L0⦄ ⊢ T0 ▶*[d, e] T2 →
- ∃∃T. ⦃G, L1⦄ ⊢ T1 ▶*[d, e] T & ⦃G, L0⦄ ⊢ T2 ➡[h, g] T.
-
-(* SN EXTENDED PARALLEL REDUCTION ON LOCAL ENVIRONMENTS *********************)
-
-(* Forward lemmas on evaluation for extended substitution *******************)
-
-lemma cpx_cpys_cpye_fwd_lpx: ∀h,g,G,L1,T1,T2. ⦃G, L1⦄ ⊢ T1 ➡[h, g] T2 →
- ∀L2. ⦃G, L1⦄ ⊢ ➡[h, g] L2 →
- ∀U1,d,e. ⦃G, L1⦄ ⊢ T1 ▶*[d, e] U1 →
- ∀U2. ⦃G, L2⦄ ⊢ T2 ▶*[d, e] 𝐍⦃U2⦄ →
- ⦃G, L1⦄ ⊢ U1 ➡[h, g] U2.
-#h #g #G #L1 #T1 #T2 #HT12 #L2 #HL12 #U1 #d #e #HTU1
-elim (cpx_cpys_conf_lpx … HT12 … HL12 … HTU1) -T1
-/3 width=9 by cpx_cpys_trans_lpx, cpye_cpys_conf/
-qed-.
-
-lemma cpx_cpye_fwd_lpx: ∀h,g,G,L1,T1,T2. ⦃G, L1⦄ ⊢ T1 ➡[h, g] T2 →
- ∀L2. ⦃G, L1⦄ ⊢ ➡[h, g] L2 →
- ∀U1,d,e. ⦃G, L1⦄ ⊢ T1 ▶*[d, e] 𝐍⦃U1⦄ →
- ∀U2. ⦃G, L2⦄ ⊢ T2 ▶*[d, e] 𝐍⦃U2⦄ →
- ⦃G, L1⦄ ⊢ U1 ➡[h, g] U2.
-#h #g #G #L1 #T1 #T2 #HT12 #L2 #HL12 #U1 #d #e *
-/2 width=9 by cpx_cpys_cpye_fwd_lpx/
-qed-.
(* SN EXTENDED PARALLEL REDUCTION FOR LOCAL ENVIRONMENTS ********************)
(* Properties on lazy equivalence for local environments ********************)
+(*
+lamma pippo: ∀h,g,G,L2,K2. ⦃G, L2⦄ ⊢ ➡[h, g] K2 → ∀L1. |L1| = |L2| →
+ ∃∃K1. ⦃G, L1⦄ ⊢ ➡[h, g] K1 & |K1| = |K2| &
+ (∀T,d. L1 ⋕[T, d] L2 ↔ K1 ⋕[T, d] K2).
+#h #g #G #L2 #K2 #H elim H -L2 -K2
+[ #L1 #H >(length_inv_zero_dx … H) -L1 /3 width=5 by ex3_intro, conj/
+| #I2 #L2 #K2 #V2 #W2 #_ #HVW2 #IHLK2 #Y #H
+ elim (length_inv_pos_dx … H) -H #I #L1 #V1 #HL12 #H destruct
+ elim (IHLK2 … HL12) -IHLK2 #K1 #HLK1 #HK12 #IH
+ elim (eq_term_dec V1 V2) #H destruct
+ [ @(ex3_intro … (K1.ⓑ{I}W2)) normalize /2 width=1 by /
+*)
+axiom lleq_lpx_trans: ∀h,g,G,L2,K2. ⦃G, L2⦄ ⊢ ➡[h, g] K2 →
+ ∀L1,T,d. L1 ⋕[T, d] L2 →
+ ∃∃K1. ⦃G, L1⦄ ⊢ ➡[h, g] K1 & K1 ⋕[T, d] K2.
+(*
+#h #g #G #L2 #K2 #H elim H -L2 -K2
+[ #L1 #T #d #H lapply (lleq_fwd_length … H) -H
+ #H >(length_inv_zero_dx … H) -L1 /2 width=3 by ex2_intro/
+| #I2 #L2 #K2 #V2 #W2 #HLK2 #HVW2 #IHLK2 #Y #T #d #HT
+ lapply (lleq_fwd_length … HT) #H
+ elim (length_inv_pos_dx … H) -H #I1 #L1 #V1 #HL12 #H destruct
+ elim (eq_term_dec V1 V2) #H destruct
+ [ @ex2_intro …
+*)
lemma lpx_lleq_fqu_trans: ∀h,g,G1,G2,L1,L2,T1,T2. ⦃G1, L1, T1⦄ ⊃ ⦃G2, L2, T2⦄ →
∀K1. ⦃G1, K1⦄ ⊢ ➡[h, g] L1 → K1 ⋕[T1, 0] L1 →
+++ /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/psubstnormal_5.ma".
-include "basic_2/relocation/cpy.ma".
-
-(* NORMAL TERMS FOR CONTEXT-SENSITIVE EXTENDED SUBSTITUTION *****************)
-
-definition cny: ∀d,e. relation3 genv lenv term ≝
- λd,e,G,L. NF … (cpy d e G L) (eq …).
-
-interpretation
- "normality for context-sensitive extended substitution (term)"
- 'PSubstNormal G L T d e = (cny d e G L T).
-
-(* Basic inversion lemmas ***************************************************)
-
-lemma cny_inv_lref: ∀G,L,d,e,i. ⦃G, L⦄ ⊢ ▶[d, e] 𝐍⦃#i⦄ →
- ∨∨ yinj i < d | d + e ≤ yinj i | |L| ≤ i.
-#G #L #d #e #i #H elim (ylt_split i d) /2 width=1 by or3_intro0/
-#Hdi elim (ylt_split i (d+e)) /2 width=1 by or3_intro1/
-#Hide elim (lt_or_ge i (|L|)) /2 width=1 by or3_intro2/
-#Hi elim (ldrop_O1_lt L i) //
-#I #K #V #HLK elim (lift_total V 0 (i+1))
-#W #HVW lapply (H W ?) -H /2 width=5 by cpy_subst/ -HLK
-#H destruct elim (lift_inv_lref2_be … HVW) -L -d -e //
-qed-.
-
-lemma cny_inv_bind: ∀a,I,G,L,V,T,d,e. ⦃G, L⦄ ⊢ ▶[d, e] 𝐍⦃ⓑ{a,I}V.T⦄ →
- ⦃G, L⦄ ⊢ ▶[d, e] 𝐍⦃V⦄ ∧ ⦃G, L.ⓑ{I}V⦄ ⊢ ▶[⫯d, e] 𝐍⦃T⦄.
-#a #I #G #L #V1 #T1 #d #e #HVT1 @conj
-[ #V2 #HV2 lapply (HVT1 (ⓑ{a,I}V2.T1) ?) -HVT1
-| #T2 #HT2 lapply (HVT1 (ⓑ{a,I}V1.T2) ?) -HVT1
-]
-/2 width=1 by cpy_bind/ #H destruct //
-qed-.
-
-lemma cny_inv_flat: ∀I,G,L,V,T,d,e. ⦃G, L⦄ ⊢ ▶[d, e] 𝐍⦃ⓕ{I}V.T⦄ →
- ⦃G, L⦄ ⊢ ▶[d, e] 𝐍⦃V⦄ ∧ ⦃G, L⦄ ⊢ ▶[d, e] 𝐍⦃T⦄.
-#I #G #L #V1 #T1 #d #e #HVT1 @conj
-[ #V2 #HV2 lapply (HVT1 (ⓕ{I}V2.T1) ?) -HVT1
-| #T2 #HT2 lapply (HVT1 (ⓕ{I}V1.T2) ?) -HVT1
-]
-/2 width=1 by cpy_flat/ #H destruct //
-qed-.
-
-(* Basic properties *********************************************************)
-
-lemma lsuby_cny_conf: ∀G,d,e.
- ∀L1,T. ⦃G, L1⦄ ⊢ ▶[d, e] 𝐍⦃T⦄ →
- ∀L2. L1 ⊑×[d, e] L2 → ⦃G, L2⦄ ⊢ ▶[d, e] 𝐍⦃T⦄.
-#G #d #e #L1 #T1 #HT1 #L2 #HL12 #T2 #HT12
-@HT1 /3 width=3 by lsuby_cpy_trans/
-qed-.
-
-lemma cny_sort: ∀G,L,d,e,k. ⦃G, L⦄ ⊢ ▶[d, e] 𝐍⦃⋆k⦄.
-#G #L #d #e #k #X #H elim (cpy_inv_sort1 … H) -H //
-qed.
-
-lemma cny_lref_free: ∀G,L,d,e,i. |L| ≤ i → ⦃G, L⦄ ⊢ ▶[d, e] 𝐍⦃#i⦄.
-#G #L #d #e #i #Hi #X #H elim (cpy_inv_lref1 … H) -H // *
-#I #K #V #_ #_ #HLK #_ lapply (ldrop_fwd_length_lt2 … HLK) -HLK
-#H elim (lt_refl_false i) /2 width=3 by lt_to_le_to_lt/
-qed.
-
-lemma cny_lref_atom: ∀G,L,d,e,i. ⇩[i] L ≡ ⋆ → ⦃G, L⦄ ⊢ ▶[d, e] 𝐍⦃#i⦄.
-#G #L #d #e #i #HL @cny_lref_free >(ldrop_fwd_length … HL) -HL //
-qed.
-
-lemma cny_lref_top: ∀G,L,d,e,i. d+e ≤ yinj i → ⦃G, L⦄ ⊢ ▶[d, e] 𝐍⦃#i⦄.
-#G #L #d #e #i #Hdei #X #H elim (cpy_inv_lref1 … H) -H // *
-#I #K #V #_ #H elim (ylt_yle_false … H) //
-qed.
-
-lemma cny_lref_skip: ∀G,L,d,e,i. yinj i < d → ⦃G, L⦄ ⊢ ▶[d, e] 𝐍⦃#i⦄.
-#G #L #d #e #i #Hid #X #H elim (cpy_inv_lref1 … H) -H // *
-#I #K #V #H elim (ylt_yle_false … H) //
-qed.
-
-lemma cny_gref: ∀G,L,d,e,p. ⦃G, L⦄ ⊢ ▶[d, e] 𝐍⦃§p⦄.
-#G #L #d #e #p #X #H elim (cpy_inv_gref1 … H) -H //
-qed.
-
-lemma cny_bind: ∀G,L,V,d,e. ⦃G, L⦄ ⊢ ▶[d, e] 𝐍⦃V⦄ →
- ∀I,T. ⦃G, L.ⓑ{I}V⦄ ⊢ ▶[⫯d, e] 𝐍⦃T⦄ →
- ∀a. ⦃G, L⦄ ⊢ ▶[d, e] 𝐍⦃ⓑ{a,I}V.T⦄.
-#G #L #V1 #d #e #HV1 #I #T1 #HT1 #a #X #H
-elim (cpy_inv_bind1 … H) -H #V2 #T2 #HV12 #HT12 #H destruct
->(HV1 … HV12) -V2 >(HT1 … HT12) -T2 //
-qed.
-
-lemma cny_flat: ∀G,L,V,d,e. ⦃G, L⦄ ⊢ ▶[d, e] 𝐍⦃V⦄ →
- ∀T. ⦃G, L⦄ ⊢ ▶[d, e] 𝐍⦃T⦄ →
- ∀I. ⦃G, L⦄ ⊢ ▶[d, e] 𝐍⦃ⓕ{I}V.T⦄.
-#G #L #V1 #d #e #HV1 #T1 #HT1 #I #X #H
-elim (cpy_inv_flat1 … H) -H #V2 #T2 #HV12 #HT12 #H destruct
->(HV1 … HV12) -V2 >(HT1 … HT12) -T2 //
-qed.
-
-lemma cny_narrow: ∀G,L,T,d1,e1. ⦃G, L⦄ ⊢ ▶[d1, e1] 𝐍⦃T⦄ →
- ∀d2,e2. d1 ≤ d2 → d2 + e2 ≤ d1 + e1 → ⦃G, L⦄ ⊢ ▶[d2, e2] 𝐍⦃T⦄.
-#G #L #T1 #d1 #e1 #HT1 #d2 #e2 #Hd12 #Hde21 #T2 #HT12
-@HT1 /2 width=5 by cpy_weak/ 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/cpy_lift.ma".
-include "basic_2/relocation/cny.ma".
-
-(* NORMAL TERMS FOR CONTEXT-SENSITIVE EXTENDED SUBSTITUTION *****************)
-
-(* Properties on relocation *************************************************)
-
-lemma cny_lift_le: ∀G,L,K,T,U,s,d,dt,e,et. ⦃G, K⦄ ⊢ ▶[dt, et] 𝐍⦃T⦄ → ⇩[s, d, e] L ≡ K →
- ⇧[d, e] T ≡ U → dt + et ≤ d → ⦃G, L⦄ ⊢ ▶[dt, et] 𝐍⦃U⦄.
-#G #L #K #T1 #U1 #s #d #dt #e #et #HT1 #HLK #HTU1 #Hdetd #U2 #HU12
-elim (cpy_inv_lift1_le … HU12 … HLK … HTU1) // -L -Hdetd #T2 #HT12
->(HT1 … HT12) -K /2 width=5 by lift_mono/
-qed-.
-
-lemma cny_lift_be: ∀G,L,K,T,U,s,d,dt,e,et. ⦃G, K⦄ ⊢ ▶[dt, et] 𝐍⦃T⦄ → ⇩[s, d, e] L ≡ K →
- ⇧[d, e] T ≡ U → dt ≤ d → yinj d ≤ dt + et → ⦃G, L⦄ ⊢ ▶[dt, et+e] 𝐍⦃U⦄.
-#G #L #K #T1 #U1 #s #d #dt #e #et #HT1 #HLK #HTU1 #Hdtd #Hddet #U2 #HU12
-elim (cpy_inv_lift1_be … HU12 … HLK … HTU1) /2 width=1 by monotonic_yle_plus_dx/ -L -Hdtd -Hddet #T2
->yplus_minus_inj #HT12 >(HT1 … HT12) -K /2 width=5 by lift_mono/
-qed-.
-
-lemma cny_lift_ge: ∀G,L,K,T,U,s,d,dt,e,et. ⦃G, K⦄ ⊢ ▶[dt, et] 𝐍⦃T⦄ → ⇩[s, d, e] L ≡ K →
- ⇧[d, e] T ≡ U → d ≤ dt → ⦃G, L⦄ ⊢ ▶[dt+e, et] 𝐍⦃U⦄.
-#G #L #K #T1 #U1 #s #d #dt #e #et #HT1 #HLK #HTU1 #Hddt #U2 #HU12
-elim (cpy_inv_lift1_ge … HU12 … HLK … HTU1) /2 width=1 by monotonic_yle_plus_dx/ -L -Hddt #T2
->yplus_minus_inj #HT12 >(HT1 … HT12) -K /2 width=5 by lift_mono/
-qed-.
-
-(* Inversion lemmas on relocation *******************************************)
-
-lemma cny_inv_lift_le: ∀G,L,K,T,U,s,d,dt,e,et. ⦃G, L⦄ ⊢ ▶[dt, et] 𝐍⦃U⦄ → ⇩[s, d, e] L ≡ K →
- ⇧[d, e] T ≡ U → dt + et ≤ d → ⦃G, K⦄ ⊢ ▶[dt, et] 𝐍⦃T⦄.
-#G #L #K #T1 #U1 #s #d #dt #e #et #HU1 #HLK #HTU1 #Hdetd #T2 #HT12
-elim (lift_total T2 d e) #U2 #HTU2
-lapply (cpy_lift_le … HT12 … HLK … HTU1 … HTU2 ?) // -K -Hdetd #HU12
-lapply (HU1 … HU12) -L /2 width=5 by lift_inj/
-qed-.
-
-lemma cny_inv_lift_be: ∀G,L,K,T,U,s,d,dt,e,et. ⦃G, L⦄ ⊢ ▶[dt, et] 𝐍⦃U⦄ → ⇩[s, d, e] L ≡ K →
- ⇧[d, e] T ≡ U → dt ≤ d → yinj d + e ≤ dt + et → ⦃G, K⦄ ⊢ ▶[dt, et-e] 𝐍⦃T⦄.
-#G #L #K #T1 #U1 #s #d #dt #e #et #HU1 #HLK #HTU1 #Hdtd #Hdedet #T2 #HT12
-lapply (yle_fwd_plus_ge_inj … Hdedet) // #Heet
-elim (yle_inv_plus_inj2 … Hdedet) -Hdedet #Hddete #Hedet
-elim (lift_total T2 d e) #U2 #HTU2
-lapply (cpy_lift_be … HT12 … HLK … HTU1 … HTU2 ? ?) // [ >yplus_minus_assoc_inj // ] -K -Hdtd -Hddete
->ymax_pre_sn // -Heet #HU12
-lapply (HU1 … HU12) -L /2 width=5 by lift_inj/
-qed-.
-
-lemma cny_inv_lift_ge: ∀G,L,K,T,U,s,d,dt,e,et. ⦃G, L⦄ ⊢ ▶[dt, et] 𝐍⦃U⦄ → ⇩[s, d, e] L ≡ K →
- ⇧[d, e] T ≡ U → yinj d + e ≤ dt → ⦃G, K⦄ ⊢ ▶[dt-e, et] 𝐍⦃T⦄.
-#G #L #K #T1 #U1 #s #d #dt #e #et #HU1 #HLK #HTU1 #Hdedt #T2 #HT12
-elim (yle_inv_plus_inj2 … Hdedt) -Hdedt #Hddte #Hedt
-elim (lift_total T2 d e) #U2 #HTU2
-lapply (cpy_lift_ge … HT12 … HLK … HTU1 … HTU2 ?) // -K -Hddte
->ymax_pre_sn // -Hedt #HU12
-lapply (HU1 … HU12) -L /2 width=5 by lift_inj/
-qed-.
-
-(* Advanced inversion lemmas on relocation **********************************)
-
-lemma cny_inv_lift_ge_up: ∀G,L,K,T,U,s,d,dt,e,et. ⦃G, L⦄ ⊢ ▶[dt, et] 𝐍⦃U⦄ → ⇩[s, d, e] L ≡ K →
- ⇧[d, e] T ≡ U → d ≤ dt → dt ≤ yinj d + e → yinj d + e ≤ dt + et →
- ⦃G, K⦄ ⊢ ▶[d, dt + et - (yinj d + e)] 𝐍⦃T⦄.
-#G #L #K #T1 #U1 #s #d #dt #e #et #HU1 #HLK #HTU1 #Hddt #Hdtde #Hdedet
-lapply (cny_narrow … HU1 (d+e) (dt+et-(d+e)) ? ?) -HU1 [ >ymax_pre_sn_comm ] // #HU1
-lapply (cny_inv_lift_ge … HU1 … HLK … HTU1 ?) // -L -U1
->yplus_minus_inj //
-qed-.
-
-lemma cny_inv_lift_subst: ∀G,L,K,V,W,i,d,e. d ≤ yinj i → i < d + e →
- ⇩[i+1] L ≡ K → ⦃G, L⦄ ⊢ ▶[d, e] 𝐍⦃W⦄ →
- ⇧[O, i+1] V ≡ W → ⦃G, K⦄ ⊢ ▶[O, ⫰(d+e-i)] 𝐍⦃V⦄.
-#G #L #K #V #W #i #d #e #Hdi #Hide #HLK #HW #HVW
-lapply (cny_inv_lift_ge_up … HW … HLK … HVW ? ? ?) //
->yplus_O1 <yplus_inj >yplus_SO2
-[ /2 width=1 by ylt_fwd_le_succ1/
-| /2 width=3 by yle_trans/
-| >yminus_succ2 //
-]
-qed-.
-
-(* Advanced properties ******************************************************)
-
-(* Note: this should be applicable in a forward manner *)
-lemma cny_lift_ge_up: ∀G,L,K,T,U,s,d,dt,e,et. ⦃G, K⦄ ⊢ ▶[yinj d, dt + et - (yinj d + yinj e)] 𝐍⦃T⦄ →
- ⇩[s, d, e] L ≡ K → ⇧[d, e] T ≡ U →
- yinj d ≤ dt → dt ≤ yinj d + yinj e → yinj d + yinj e ≤ dt + et →
- ⦃G, L⦄ ⊢ ▶[dt, et] 𝐍⦃U⦄.
-#G #L #K #T1 #U1 #s #d #dt #e #et #HT1 #HLK #HTU1 #Hddt #Hdtde #Hdedet
-lapply (cny_lift_be … HT1 … HLK … HTU1 ? ?) // -K -T1
-#HU1 @(cny_narrow … HU1) -HU1 // (**) (* auto fails *)
-qed-.
-
-lemma cny_lift_subst: ∀G,L,K,V,W,i,d,e. d ≤ yinj i → i < d + e →
- ⇩[i+1] L ≡ K → ⦃G, K⦄ ⊢ ▶[O, ⫰(d+e-i)] 𝐍⦃V⦄ →
- ⇧[O, i+1] V ≡ W → ⦃G, L⦄ ⊢ ▶[d, e] 𝐍⦃W⦄.
-#G #L #K #V #W #i #d #e #Hdi #Hide #HLK #HV #HVW
-@(cny_lift_ge_up … HLK … HVW) // >yplus_O1 <yplus_inj >yplus_SO2
-[ >yminus_succ2 //
-| /2 width=3 by yle_trans/
-| /2 width=1 by ylt_fwd_le_succ1/
-]
-qed-.
#I1 #I2 #L1 #L2 #V1 #V2 #d #e #HL12 #Hd <(ylt_inv_O1 … Hd) /2 width=1 by lsuby_succ/
qed.
+lemma lsuby_pair_O_Y: ∀L1,L2. L1 ⊑×[0, ∞] L2 →
+ ∀I1,I2,V. L1.ⓑ{I1}V ⊑×[0,∞] L2.ⓑ{I2}V.
+#L1 #L2 #HL12 #I1 #I2 #V lapply (lsuby_pair I1 I2 … V … HL12) -HL12 //
+qed.
+
lemma lsuby_refl: ∀L,d,e. L ⊑×[d, e] L.
#L elim L -L //
#L #I #V #IHL #d elim (ynat_cases … d) [| * #x ]
#He destruct /2 width=1 by lsuby_zero, lsuby_pair/
qed.
-lemma lsuby_length: ∀L1,L2. |L2| ≤ |L1| → L1 ⊑×[yinj 0, yinj 0] L2.
-#L1 elim L1 -L1
-[ #X #H lapply (le_n_O_to_eq … H) -H
- #H lapply (length_inv_zero_sn … H) #H destruct /2 width=1 by lsuby_atom/
-| #L1 #I1 #V1 #IHL1 * normalize
- /4 width=2 by lsuby_zero, le_S_S_to_le/
+lemma lsuby_O1: ∀L2,L1,d. |L2| ≤ |L1| → L1 ⊑×[d, yinj 0] L2.
+#L2 elim L2 -L2 // #L2 #I2 #V2 #IHL2 * normalize
+[ #d #H lapply (le_n_O_to_eq … H) -H <plus_n_Sm #H destruct
+| #L1 #I1 #V1 #d #H lapply (le_plus_to_le_r … H) -H #HL12
+ elim (ynat_cases d) /3 width=1 by lsuby_zero/
+ * /3 width=1 by lsuby_succ/
]
qed.
lemma lsuby_sym: ∀d,e,L1,L2. L1 ⊑×[d, e] L2 → |L1| = |L2| → L2 ⊑×[d, e] L1.
#d #e #L1 #L2 #H elim H -d -e -L1 -L2
[ #L1 #d #e #H >(length_inv_zero_dx … H) -L1 //
-| /2 width=1 by lsuby_length/
+| /2 width=1 by lsuby_O1/
| #I1 #I2 #L1 #L2 #V #e #_ #IHL12 #H lapply (injective_plus_l … H)
/3 width=1 by lsuby_pair/
| #I1 #I2 #L1 #L2 #V1 #V2 #d #e #_ #IHL12 #H lapply (injective_plus_l … H)
+++ /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/psubsteval_6.ma".
-include "basic_2/relocation/cny.ma".
-include "basic_2/substitution/cpys.ma".
-
-(* EVALUATION FOR CONTEXT-SENSITIVE EXTENDED SUBSTITUTION ON TERMS **********)
-
-definition cpye: ynat → ynat → relation4 genv lenv term term ≝
- λd,e,G,L,T1,T2. ⦃G, L⦄ ⊢ T1 ▶*[d, e] T2 ∧ ⦃G, L⦄ ⊢ ▶[d, e] 𝐍⦃T2⦄.
-
-interpretation "evaluation for context-sensitive extended substitution (term)"
- 'PSubstEval G L T1 T2 d e = (cpye d e G L T1 T2).
-
-(* Basic_properties *********************************************************)
-
-lemma cpye_sort: ∀G,L,d,e,k. ⦃G, L⦄ ⊢ ⋆k ▶*[d, e] 𝐍⦃⋆k⦄.
-/3 width=5 by cny_sort, conj/ qed.
-
-lemma cpye_free: ∀G,L,d,e,i. |L| ≤ i → ⦃G, L⦄ ⊢ #i ▶*[d, e] 𝐍⦃#i⦄.
-/3 width=6 by cny_lref_free, conj/ qed.
-
-lemma cpye_top: ∀G,L,d,e,i. d + e ≤ yinj i → ⦃G, L⦄ ⊢ #i ▶*[d, e] 𝐍⦃#i⦄.
-/3 width=6 by cny_lref_top, conj/ qed.
-
-lemma cpye_skip: ∀G,L,d,e,i. yinj i < d → ⦃G, L⦄ ⊢ #i ▶*[d, e] 𝐍⦃#i⦄.
-/3 width=6 by cny_lref_skip, conj/ qed.
-
-lemma cpye_gref: ∀G,L,d,e,p. ⦃G, L⦄ ⊢ §p ▶*[d, e] 𝐍⦃§p⦄.
-/3 width=5 by cny_gref, conj/ qed.
-
-lemma cpye_bind: ∀G,L,V1,V2,d,e. ⦃G, L⦄ ⊢ V1 ▶*[d, e] 𝐍⦃V2⦄ →
- ∀I,T1,T2. ⦃G, L.ⓑ{I}V1⦄ ⊢ T1 ▶*[⫯d, e] 𝐍⦃T2⦄ →
- ∀a. ⦃G, L⦄ ⊢ ⓑ{a,I}V1.T1 ▶*[d, e] 𝐍⦃ⓑ{a,I}V2.T2⦄.
-#G #L #V1 #V2 #d #e * #HV12 #HV2 #I #T1 #T2 *
-/5 width=8 by cpys_bind, cny_bind, lsuby_cny_conf, lsuby_succ, conj/
-qed.
-
-lemma cpye_flat: ∀G,L,V1,V2,d,e. ⦃G, L⦄ ⊢ V1 ▶*[d, e] 𝐍⦃V2⦄ →
- ∀T1,T2. ⦃G, L⦄ ⊢ T1 ▶*[d, e] 𝐍⦃T2⦄ →
- ∀I. ⦃G, L⦄ ⊢ ⓕ{I}V1.T1 ▶*[d, e] 𝐍⦃ⓕ{I}V2.T2⦄.
-#G #L #V1 #V2 #d #e * #HV12 #HV2 #T1 #T2 *
-/3 width=7 by cpys_flat, cny_flat, conj/
-qed.
-
-(* Basic inversion lemmas ***************************************************)
-
-lemma cpye_inv_sort1: ∀G,L,X,d,e,k. ⦃G, L⦄ ⊢ ⋆k ▶*[d, e] 𝐍⦃X⦄ → X = ⋆k.
-#G #L #X #d #e #k * /2 width=5 by cpys_inv_sort1/
-qed-.
-
-lemma cpye_inv_gref1: ∀G,L,X,d,e,p. ⦃G, L⦄ ⊢ §p ▶*[d, e] 𝐍⦃X⦄ → X = §p.
-#G #L #X #d #e #p * /2 width=5 by cpys_inv_gref1/
-qed-.
-
-lemma cpye_inv_bind1: ∀a,I,G,L,V1,T1,X,d,e. ⦃G, L⦄ ⊢ ⓑ{a,I}V1.T1 ▶*[d, e] 𝐍⦃X⦄ →
- ∃∃V2,T2. ⦃G, L⦄ ⊢ V1 ▶*[d, e] 𝐍⦃V2⦄ & ⦃G, L.ⓑ{I}V1⦄ ⊢ T1 ▶*[⫯d, e] 𝐍⦃T2⦄ &
- X = ⓑ{a,I}V2.T2.
-#a #I #G #L #V1 #T1 #X #d #e * #H1 #H2 elim (cpys_inv_bind1 … H1) -H1
-#V2 #T2 #HV12 #HT12 #H destruct elim (cny_inv_bind … H2) -H2
-/5 width=8 by lsuby_cny_conf, lsuby_succ, ex3_2_intro, conj/
-qed-.
-
-lemma cpye_inv_flat1: ∀I,G,L,V1,T1,X,d,e. ⦃G, L⦄ ⊢ ⓕ{I}V1.T1 ▶*[d, e] 𝐍⦃X⦄ →
- ∃∃V2,T2. ⦃G, L⦄ ⊢ V1 ▶*[d, e] 𝐍⦃V2⦄ & ⦃G, L⦄ ⊢ T1 ▶*[d, e] 𝐍⦃T2⦄ &
- X = ⓕ{I}V2.T2.
-#I #G #L #V1 #T1 #X #d #e * #H1 #H2 elim (cpys_inv_flat1 … H1) -H1
-#V2 #T2 #HV12 #HT12 #H destruct elim (cny_inv_flat … H2) -H2
-/3 width=5 by ex3_2_intro, 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/psubstevalalt_6.ma".
-include "basic_2/substitution/cpye_lift.ma".
-
-(* EVALUATION FOR CONTEXT-SENSITIVE EXTENDED SUBSTITUTION ON TERMS **********)
-
-(* Note: alternative definition of cpye *)
-inductive cpyea: ynat → ynat → relation4 genv lenv term term ≝
-| cpyea_sort : ∀G,L,d,e,k. cpyea d e G L (⋆k) (⋆k)
-| cpyea_free : ∀G,L,d,e,i. |L| ≤ i → cpyea d e G L (#i) (#i)
-| cpyea_top : ∀G,L,d,e,i. d + e ≤ yinj i → cpyea d e G L (#i) (#i)
-| cpyea_skip : ∀G,L,d,e,i. yinj i < d → cpyea d e G L (#i) (#i)
-| cpyea_subst: ∀I,G,L,K,V1,V2,W2,i,d,e. d ≤ yinj i → yinj i < d+e →
- ⇩[i] L ≡ K.ⓑ{I}V1 → cpyea (yinj 0) (⫰(d+e-yinj i)) G K V1 V2 →
- ⇧[0, i+1] V2 ≡ W2 → cpyea d e G L (#i) W2
-| cpyea_gref : ∀G,L,d,e,p. cpyea d e G L (§p) (§p)
-| cpyea_bind : ∀a,I,G,L,V1,V2,T1,T2,d,e.
- cpyea d e G L V1 V2 → cpyea (⫯d) e G (L.ⓑ{I}V1) T1 T2 →
- cpyea d e G L (ⓑ{a,I}V1.T1) (ⓑ{a,I}V2.T2)
-| cpyea_flat : ∀I,G,L,V1,V2,T1,T2,d,e.
- cpyea d e G L V1 V2 → cpyea d e G L T1 T2 →
- cpyea d e G L (ⓕ{I}V1.T1) (ⓕ{I}V2.T2)
-.
-
-interpretation
- "evaluation for context-sensitive extended substitution (term) alternative"
- 'PSubstEvalAlt G L T1 T2 d e = (cpyea d e G L T1 T2).
-
-(* Main properties **********************************************************)
-
-theorem cpye_cpyea: ∀G,L,T1,T2,d,e. ⦃G, L⦄ ⊢ T1 ▶*[d, e] 𝐍⦃T2⦄ → ⦃G, L⦄ ⊢ T1 ▶▶*[d, e] 𝐍⦃T2⦄.
-#G #L #T1 @(fqup_wf_ind_eq … G L T1) -G -L -T1
-#Z #Y #X #IH #G #L * *
-[ #k #_ #_ #_ #T2 #d #e #H -X -Y -Z >(cpye_inv_sort1 … H) -H //
-| #i #HG #HL #HT #T2 #d #e #H destruct
- elim (cpye_inv_lref1 … H) -H *
- /4 width=7 by cpyea_subst, cpyea_free, cpyea_top, cpyea_skip, fqup_lref/
-| #p #_ #_ #_ #T2 #d #e #H -X -Y -Z >(cpye_inv_gref1 … H) -H //
-| #a #I #V1 #T1 #HG #HL #HT #T #d #e #H destruct
- elim (cpye_inv_bind1 … H) -H /3 width=1 by cpyea_bind/
-| #I #V1 #T1 #HG #HL #HT #T #d #e #H destruct
- elim (cpye_inv_flat1 … H) -H /3 width=1 by cpyea_flat/
-]
-qed.
-
-(* Main inversion properties ************************************************)
-
-theorem cpyea_inv_cpye: ∀G,L,T1,T2,d,e. ⦃G, L⦄ ⊢ T1 ▶▶*[d, e] 𝐍⦃T2⦄ → ⦃G, L⦄ ⊢ T1 ▶*[d, e] 𝐍⦃T2⦄.
-#G #L #T1 #T2 #d #e #H elim H -G -L -T1 -T2 -d -e
-/2 width=7 by cpye_subst, cpye_flat, cpye_bind, cpye_skip, cpye_top, cpye_free/
-qed-.
-
-(* Advanced eliminators *****************************************************)
-
-lemma cpye_ind_alt: ∀R:ynat→ynat→relation4 genv lenv term term.
- (∀G,L,d,e,k. R d e G L (⋆k) (⋆k)) →
- (∀G,L,d,e,i. |L| ≤ i → R d e G L (#i) (#i)) →
- (∀G,L,d,e,i. d + e ≤ yinj i → R d e G L (#i) (#i)) →
- (∀G,L,d,e,i. yinj i < d → R d e G L (#i) (#i)) →
- (∀I,G,L,K,V1,V2,W2,i,d,e. d ≤ yinj i → yinj i < d + e →
- ⇩[i] L ≡ K.ⓑ{I}V1 → ⦃G, K⦄ ⊢ V1 ▶*[yinj O, ⫰(d+e-yinj i)] 𝐍⦃V2⦄ →
- ⇧[O, i+1] V2 ≡ W2 → R (yinj O) (⫰(d+e-yinj i)) G K V1 V2 → R d e G L (#i) W2
- ) →
- (∀G,L,d,e,p. R d e G L (§p) (§p)) →
- (∀a,I,G,L,V1,V2,T1,T2,d,e. ⦃G, L⦄ ⊢ V1 ▶*[d, e] 𝐍⦃V2⦄ →
- ⦃G, L.ⓑ{I}V1⦄ ⊢ T1 ▶*[⫯d, e] 𝐍⦃T2⦄ → R d e G L V1 V2 →
- R (⫯d) e G (L.ⓑ{I}V1) T1 T2 → R d e G L (ⓑ{a,I}V1.T1) (ⓑ{a,I}V2.T2)
- ) →
- (∀I,G,L,V1,V2,T1,T2,d,e. ⦃G, L⦄ ⊢ V1 ▶*[d, e] 𝐍⦃V2⦄ →
- ⦃G, L⦄ ⊢ T1 ▶*[d, e] 𝐍⦃T2⦄ → R d e G L V1 V2 →
- R d e G L T1 T2 → R d e G L (ⓕ{I}V1.T1) (ⓕ{I}V2.T2)
- ) →
- ∀d,e,G,L,T1,T2. ⦃G, L⦄ ⊢ T1 ▶*[d, e] 𝐍⦃T2⦄ → R d e G L T1 T2.
-#R #H1 #H2 #H3 #H4 #H5 #H6 #H7 #H8 #d #e #G #L #T1 #T2 #H elim (cpye_cpyea … H) -G -L -T1 -T2 -d -e
-/3 width=8 by cpyea_inv_cpye/
-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/cpys_cny.ma".
-include "basic_2/substitution/cpys_cpys.ma".
-include "basic_2/substitution/cpye.ma".
-
-(* EVALUATION FOR CONTEXT-SENSITIVE EXTENDED SUBSTITUTION ON TERMS **********)
-
-(* Advanced properties ******************************************************)
-
-lemma cpye_cpys_conf: ∀G,L,T,T2,d,e. ⦃G, L⦄ ⊢ T ▶*[d, e] 𝐍⦃T2⦄ →
- ∀T1. ⦃G, L⦄ ⊢ T ▶*[d, e] T1 → ⦃G, L⦄ ⊢ T1 ▶*[d, e] T2.
-#G #L #T #T2 #d #e * #H2 #HT2 #T1 #H1 elim (cpys_conf_eq … H1 … H2) -T
-#T0 #HT10 #HT20 >(cpys_inv_cny1 … HT2 … HT20) -T2 //
-qed-.
-
\ No newline at end of file
+++ /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/cny_lift.ma".
-include "basic_2/substitution/fqup.ma".
-include "basic_2/substitution/cpys_lift.ma".
-include "basic_2/substitution/cpye.ma".
-
-(* EVALUATION FOR CONTEXT-SENSITIVE EXTENDED SUBSTITUTION ON TERMS **********)
-
-(* Advanced properties ******************************************************)
-
-lemma cpye_subst: ∀I,G,L,K,V1,V2,W2,i,d,e. d ≤ yinj i → i < d + e →
- ⇩[i] L ≡ K.ⓑ{I}V1 → ⦃G, K⦄ ⊢ V1 ▶*[O, ⫰(d+e-i)] 𝐍⦃V2⦄ →
- ⇧[O, i+1] V2 ≡ W2 → ⦃G, L⦄ ⊢ #i ▶*[d, e] 𝐍⦃W2⦄.
-#I #G #L #K #V1 #V2 #W2 #i #d #e #Hdi #Hide #HLK *
-/4 width=13 by cpys_subst, cny_lift_subst, ldrop_fwd_drop2, conj/
-qed.
-
-lemma cpye_total: ∀G,L,T1,d,e. ∃T2. ⦃G, L⦄ ⊢ T1 ▶*[d, e] 𝐍⦃T2⦄.
-#G #L #T1 @(fqup_wf_ind_eq … G L T1) -G -L -T1
-#Z #Y #X #IH #G #L * *
-[ #k #HG #HL #HT #d #e destruct -IH /2 width=2 by ex_intro/
-| #i #HG #HL #HT #d #e destruct
- elim (ylt_split i d) /3 width=2 by cpye_skip, ex_intro/
- elim (ylt_split i (d+e)) /3 width=2 by cpye_top, ex_intro/
- elim (lt_or_ge i (|L|)) /3 width=2 by cpye_free, ex_intro/
- #Hi #Hide #Hdi elim (ldrop_O1_lt L i) // -Hi
- #I #K #V1 #HLK elim (IH G K V1 … 0 (⫰(d+e-i))) -IH /2 width=2 by fqup_lref/
- #V2 elim (lift_total V2 0 (i+1)) /3 width=8 by ex_intro, cpye_subst/
-| #p #HG #HL #HT #d #e destruct -IH /2 width=2 by ex_intro/
-| #a #I #V1 #T1 #HG #HL #HT #d #e destruct
- elim (IH G L V1 … d e) // elim (IH G (L.ⓑ{I}V1) T1 … (⫯d) e) //
- /3 width=2 by cpye_bind, ex_intro/
-| #I #V1 #T1 #HG #HL #HT #d #e destruct
- elim (IH G L V1 … d e) // elim (IH G L T1 … d e) //
- /3 width=2 by cpye_flat, ex_intro/
-]
-qed-.
-
-(* Advanced inversion lemmas ************************************************)
-
-lemma cpye_inv_lref1: ∀G,L,T2,d,e,i. ⦃G, L⦄ ⊢ #i ▶*[d, e] 𝐍⦃T2⦄ →
- ∨∨ |L| ≤ i ∧ T2 = #i
- | d + e ≤ yinj i ∧ T2 = #i
- | yinj i < d ∧ T2 = #i
- | ∃∃I,K,V1,V2. d ≤ yinj i & yinj i < d + e &
- ⇩[i] L ≡ K.ⓑ{I}V1 &
- ⦃G, K⦄ ⊢ V1 ▶*[yinj 0, ⫰(d+e-yinj i)] 𝐍⦃V2⦄ &
- ⇧[O, i+1] V2 ≡ T2.
-#G #L #T2 #i #d #e * #H1 #H2 elim (cpys_inv_lref1 … H1) -H1
-[ #H destruct elim (cny_inv_lref … H2) -H2
- /3 width=1 by or4_intro0, or4_intro1, or4_intro2, conj/
-| * #I #K #V1 #V2 #Hdi #Hide #HLK #HV12 #HVT2
- @or4_intro3 @(ex5_4_intro … HLK … HVT2) (**) (* explicit constructor *)
- /4 width=13 by cny_inv_lift_subst, ldrop_fwd_drop2, conj/
-]
-qed-.
-
-lemma cpye_inv_lref1_free: ∀G,L,T2,d,e,i. ⦃G, L⦄ ⊢ #i ▶*[d, e] 𝐍⦃T2⦄ →
- (∨∨ |L| ≤ i | d + e ≤ yinj i | yinj i < d) → T2 = #i.
-#G #L #T2 #d #e #i #H * elim (cpye_inv_lref1 … H) -H * //
-#I #K #V1 #V2 #Hdi #Hide #HLK #_ #_ #H
-[ elim (lt_refl_false i) -d
- @(lt_to_le_to_lt … H) -H /2 width=5 by ldrop_fwd_length_lt2/ (**) (* full auto slow: 19s *)
-]
-elim (ylt_yle_false … H) //
-qed-.
-
-lemma cpye_inv_lref1_lget: ∀G,L,T2,d,e,i. ⦃G, L⦄ ⊢ #i ▶*[d, e] 𝐍⦃T2⦄ →
- ∀I,K,V1. ⇩[i] L ≡ K.ⓑ{I}V1 →
- ∨∨ d + e ≤ yinj i ∧ T2 = #i
- | yinj i < d ∧ T2 = #i
- | ∃∃V2. d ≤ yinj i & yinj i < d + e &
- ⦃G, K⦄ ⊢ V1 ▶*[yinj 0, ⫰(d+e-yinj i)] 𝐍⦃V2⦄ &
- ⇧[O, i+1] V2 ≡ T2.
-#G #L #T2 #d #e #i #H #I #K #V1 #HLK elim (cpye_inv_lref1 … H) -H *
-[ #H elim (lt_refl_false i) -T2 -d
- @(lt_to_le_to_lt … H) -H /2 width=5 by ldrop_fwd_length_lt2/
-| /3 width=1 by or3_intro0, conj/
-| /3 width=1 by or3_intro1, conj/
-| #Z #Y #X1 #X2 #Hdi #Hide #HLY #HX12 #HXT2
- lapply (ldrop_mono … HLY … HLK) -HLY -HLK #H destruct
- /3 width=3 by or3_intro2, ex4_intro/
-]
-qed-.
-
-lemma cpye_inv_lref1_subst_ex: ∀G,L,T2,d,e,i. ⦃G, L⦄ ⊢ #i ▶*[d, e] 𝐍⦃T2⦄ →
- ∀I,K,V1. d ≤ yinj i → yinj i < d + e →
- ⇩[i] L ≡ K.ⓑ{I}V1 →
- ∃∃V2. ⦃G, K⦄ ⊢ V1 ▶*[yinj 0, ⫰(d+e-yinj i)] 𝐍⦃V2⦄ &
- ⇧[O, i+1] V2 ≡ T2.
-#G #L #T2 #d #e #i #H #I #K #V1 #Hdi #Hide #HLK
-elim (cpye_inv_lref1_lget … H … HLK) -H * /2 width=3 by ex2_intro/
-#H elim (ylt_yle_false … H) //
-qed-.
-
-lemma cpye_inv_lref1_subst: ∀G,L,T2,d,e,i. ⦃G, L⦄ ⊢ #i ▶*[d, e] 𝐍⦃T2⦄ →
- ∀I,K,V1,V2. d ≤ yinj i → yinj i < d + e →
- ⇩[i] L ≡ K.ⓑ{I}V1 → ⇧[O, i+1] V2 ≡ T2 →
- ⦃G, K⦄ ⊢ V1 ▶*[yinj 0, ⫰(d+e-yinj i)] 𝐍⦃V2⦄.
-#G #L #T2 #d #e #i #H #I #K #V1 #V2 #Hdi #Hide #HLK #HVT2
-elim (cpye_inv_lref1_subst_ex … H … HLK) -H -HLK //
-#X2 #H0 #HXT2 lapply (lift_inj … HXT2 … HVT2) -HXT2 -HVT2 #H destruct //
-qed-.
-
-(* Inversion lemmas on relocation *******************************************)
-
-lemma cpye_inv_lift1_le: ∀G,L,U1,U2,dt,et. ⦃G, L⦄ ⊢ U1 ▶*[dt, et] 𝐍⦃U2⦄ →
- ∀K,s,d,e. ⇩[s, d, e] L ≡ K → ∀T1. ⇧[d, e] T1 ≡ U1 →
- dt + et ≤ d →
- ∃∃T2. ⦃G, K⦄ ⊢ T1 ▶*[dt, et] 𝐍⦃T2⦄ & ⇧[d, e] T2 ≡ U2.
-#G #L #U1 #U2 #dt #et * #HU12 #HU2 #K #s #d #e #HLK #T1 #HTU1 #Hdetd
-elim (cpys_inv_lift1_le … HU12 … HLK … HTU1) -U1 // #T2 #HT12 #HTU2
-lapply (cny_inv_lift_le … HU2 … HLK … HTU2 ?) -L
-/3 width=3 by ex2_intro, conj/
-qed-.
-
-lemma cpye_inv_lift1_be: ∀G,L,U1,U2,dt,et. ⦃G, L⦄ ⊢ U1 ▶*[dt, et] 𝐍⦃U2⦄ →
- ∀K,s,d,e. ⇩[s, d, e] L ≡ K → ∀T1. ⇧[d, e] T1 ≡ U1 →
- dt ≤ d → yinj d + e ≤ dt + et →
- ∃∃T2. ⦃G, K⦄ ⊢ T1 ▶*[dt, et - e] 𝐍⦃T2⦄ & ⇧[d, e] T2 ≡ U2.
-#G #L #U1 #U2 #dt #et * #HU12 #HU2 #K #s #d #e #HLK #T1 #HTU1 #Hdtd #Hdedet
-elim (cpys_inv_lift1_be … HU12 … HLK … HTU1) -U1 // #T2 #HT12 #HTU2
-lapply (cny_inv_lift_be … HU2 … HLK … HTU2 ? ?) -L
-/3 width=3 by ex2_intro, conj/
-qed-.
-
-lemma cpye_inv_lift1_ge: ∀G,L,U1,U2,dt,et. ⦃G, L⦄ ⊢ U1 ▶*[dt, et] 𝐍⦃U2⦄ →
- ∀K,s,d,e. ⇩[s, d, e] L ≡ K → ∀T1. ⇧[d, e] T1 ≡ U1 →
- yinj d + e ≤ dt →
- ∃∃T2. ⦃G, K⦄ ⊢ T1 ▶*[dt - e, et] 𝐍⦃T2⦄ & ⇧[d, e] T2 ≡ U2.
-#G #L #U1 #U2 #dt #et * #HU12 #HU2 #K #s #d #e #HLK #T1 #HTU1 #Hdedt
-elim (cpys_inv_lift1_ge … HU12 … HLK … HTU1) -U1 // #T2 #HT12 #HTU2
-lapply (cny_inv_lift_ge … HU2 … HLK … HTU2 ?) -L
-/3 width=3 by ex2_intro, conj/
-qed-.
-
-lemma cpye_inv_lift1_ge_up: ∀G,L,U1,U2,dt,et. ⦃G, L⦄ ⊢ U1 ▶*[dt, et] 𝐍⦃U2⦄ →
- ∀K,s,d,e. ⇩[s, d, e] L ≡ K → ∀T1. ⇧[d, e] T1 ≡ U1 →
- d ≤ dt → dt ≤ yinj d + e → yinj d + e ≤ dt + et →
- ∃∃T2. ⦃G, K⦄ ⊢ T1 ▶*[d, dt + et - (yinj d + e)] 𝐍⦃T2⦄ &
- ⇧[d, e] T2 ≡ U2.
-#G #L #U1 #U2 #dt #et * #HU12 #HU2 #K #s #d #e #HLK #T1 #HTU1 #Hddt #Hdtde #Hdedet
-elim (cpys_inv_lift1_ge_up … HU12 … HLK … HTU1) -U1 // #T2 #HT12 #HTU2
-lapply (cny_inv_lift_ge_up … HU2 … HLK … HTU2 ? ? ?) -L
-/3 width=3 by ex2_intro, conj/
-qed-.
-
-lemma cpye_inv_lift1_subst: ∀G,L,W1,W2,d,e. ⦃G, L⦄ ⊢ W1 ▶*[d, e] 𝐍⦃W2⦄ →
- ∀K,V1,i. ⇩[i+1] L ≡ K → ⇧[O, i+1] V1 ≡ W1 →
- d ≤ yinj i → i < d + e →
- ∃∃V2. ⦃G, K⦄ ⊢ V1 ▶*[O, ⫰(d+e-i)] 𝐍⦃V2⦄ & ⇧[O, i+1] V2 ≡ W2.
-#G #L #W1 #W2 #d #e * #HW12 #HW2 #K #V1 #i #HLK #HVW1 #Hdi #Hide
-elim (cpys_inv_lift1_subst … HW12 … HLK … HVW1) -W1 // #V2 #HV12 #HVW2
-lapply (cny_inv_lift_subst … HLK HW2 HVW2) -L
-/3 width=3 by ex2_intro, 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/relocation/cny.ma".
-include "basic_2/substitution/cpys.ma".
-
-(* CONTEXT-SENSITIVE EXTENDED MULTIPLE SUBSTITUTION FOR TERMS ***************)
-
-(* Inversion lemmas on normality for extended substitution ******************)
-
-lemma cpys_inv_cny1: ∀G,L,T1,d,e. ⦃G, L⦄ ⊢ ▶[d, e] 𝐍⦃T1⦄ →
- ∀T2. ⦃G, L⦄ ⊢ T1 ▶*[d, e] T2 → T1 = T2.
-#G #L #T1 #d #e #HT1 #T2 #H @(cpys_ind … H) -T2 //
-#T #T2 #_ #HT2 #IHT1 destruct <(HT1 … HT2) -T //
-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/cpye_lift.ma".
-include "basic_2/substitution/lleq_alt.ma".
-
-(* LAZY EQUIVALENCE FOR LOCAL ENVIRONMENTS **********************************)
-
-(* Forward lemmas on evaluation for extended substitution *******************)
-
-lemma lleq_fwd_cpye: ∀L1,L2,T,d. L1 ⋕[T, d] L2 → ∀G,T1. ⦃G, L1⦄ ⊢ T ▶*[d, ∞] 𝐍⦃T1⦄ →
- ∀T2. ⦃G, L2⦄ ⊢ T ▶*[d, ∞] 𝐍⦃T2⦄ → T1 = T2.
-#L1 #L2 #T #d #H @(lleq_ind_alt … H) -L1 -L2 -T -d
-[ #L1 #L2 #d #k #_ #G #T1 #H1 #T2 #H2
- >(cpye_inv_sort1 … H1) -H1 >(cpye_inv_sort1 … H2) -H2 //
-| #L1 #L2 #d #i #_ #Hid #G #T1 #H1 #T2 #H2
- >(cpye_inv_lref1_free … H1) -H1 [ >(cpye_inv_lref1_free … H2) -H2 ]
- /2 width=1 by or3_intro2/
-| #I1 #I2 #L1 #L2 #K1 #K2 #V #d #i #Hdi #HLK1 #HLK2 #_ #IHV #G #T1 #H1 #T2 #H2
- elim (cpye_inv_lref1_subst_ex … H1 … HLK1) -H1 -HLK1 //
- elim (cpye_inv_lref1_subst_ex … H2 … HLK2) -H2 -HLK2 //
- >yminus_Y_inj #V2 #HV2 #HVT2 #V1 #HV1 #HVT1
- lapply (IHV … HV1 … HV2) -IHV -HV1 -HV2 #H destruct /2 width=5 by lift_mono/
-| #L1 #L2 #d #i #_ #HL1 #HL2 #G #T1 #H1 #T2 #H2
- >(cpye_inv_lref1_free … H1) -H1 [ >(cpye_inv_lref1_free … H2) -H2 ]
- /2 width=1 by or3_intro0/
-| #L1 #L2 #d #p #_ #G #T1 #H1 #T2 #H2
- >(cpye_inv_gref1 … H1) -H1 >(cpye_inv_gref1 … H2) -H2 //
-| #a #I #L1 #L2 #V #T #d #_ #_ #IHV #IHT #G #X1 #H1 #X2 #H2
- elim (cpye_inv_bind1 … H1) -H1 #V1 #T1 #HV1 #HT1 #H destruct
- elim (cpye_inv_bind1 … H2) -H2 #V2 #T2 #HV2 #HT2 #H destruct
- /3 width=3 by eq_f2/
-| #I #L1 #L2 #V #T #d #_ #_ #IHV #IHT #G #X1 #H1 #X2 #H2
- elim (cpye_inv_flat1 … H1) -H1 #V1 #T1 #HV1 #HT1 #H destruct
- elim (cpye_inv_flat1 … H2) -H2 #V2 #T2 #HV2 #HT2 #H destruct
- /3 width=3 by eq_f2/
-]
-qed-.
}
]
[ { "strongly normalizing extended computation" * } {
- [ "lsx ( ? ⊢ ⬊*[?,?,?] ? )" "lsx_cpxs" + "lsx_csx" * ]
+ [ "lsx ( ? ⊢ ⬊*[?,?,?,?] ? )" "lsx_cpxs" + "lsx_csx" * ]
[ "csx_vector ( ⦃?,?⦄ ⊢ ⬊*[?,?] ? )" "csx_tstc_vector" + "csx_aaa" * ]
[ "csx ( ⦃?,?⦄ ⊢ ⬊*[?,?] ? )" "csx_alt ( ⦃?,?⦄ ⊢ ⬊⬊*[?,?] ? )" "csx_lift" + "csx_lpx" + "csx_fpbs" * ]
}
}
]
[ { "context-sensitive extended computation" * } {
- [ "lpxs ( ⦃?,?⦄ ⊢ ➡*[?,?] ? )" "lpxs_alt ( ⦃?,?⦄ ⊢ ➡➡*[?,?] ? )" "lpxs_ldrop" + "lpxs_cpye" + "lpxs_lleq" + "lpxs_aaa" + "lpxs_cpxs" + "lpxs_lpxs" * ]
- [ "cpxs ( ⦃?,?⦄ ⊢ ? ➡*[?,?] ? )" "cpxs_tstc" + "cpxs_tstc_vector" + "cpxs_lift" + "cpxs_lleq" + "cpxs_aaa" + "cpxs_cpxs" * ]
+ [ "lpxs ( ⦃?,?⦄ ⊢ ➡*[?,?] ? )" "lpxs_alt ( ⦃?,?⦄ ⊢ ➡➡*[?,?] ? )" "lpxs_ldrop" + "lpxs_lleq" + "lpxs_aaa" + "lpxs_cpxs" + "lpxs_lpxs" * ]
+ [ "cpxs ( ⦃?,?⦄ ⊢ ? ➡*[?,?] ? )" "cpxs_tstc" + "cpxs_tstc_vector" + "cpxs_lift" + "cpxs_cpys" + "cpxs_lleq" + "cpxs_aaa" + "cpxs_cpxs" * ]
}
]
[ { "context-sensitive computation" * } {
}
]
[ { "context-sensitive extended reduction" * } {
- [ "lpx ( ⦃?,?⦄ ⊢ ➡[?,?] ? )" "lpx_ldrop" + "lpx_cpys" + "lpx_cpye" + "lpx_lleq" + "lpx_aaa" * ]
+ [ "lpx ( ⦃?,?⦄ ⊢ ➡[?,?] ? )" "lpx_ldrop" + "lpx_cpys" + "lpx_lleq" + "lpx_aaa" * ]
[ "cpx ( ⦃?,?⦄ ⊢ ? ➡[?,?] ? )" "cpx_lift" + "cpx_cpys" + "cpx_lleq" + "cpx_cix" * ]
}
]
class "yellow"
[ { "substitution" * } {
[ { "lazy equivalence for local environments" * } {
- [ "lleq ( ? ⋕[?,?] ? )" "lleq_alt ( ? ⋕⋕[?,?] ? )" "lleq_ldrop" + "lleq_fqus" + "lleq_cpye" + "lleq_lleq" + "lleq_ext" * ]
+ [ "lleq ( ? ⋕[?,?] ? )" "lleq_alt ( ? ⋕⋕[?,?] ? )" "lleq_ldrop" + "lleq_fqus" + "lleq_lleq" + "lleq_ext" * ]
}
]
- [ { "evaluation for contxt-sensitive extended substitution" * } {
- [ "cpye ( ⦃?,?⦄ ⊢ ? ▶*[?,?] 𝐍⦃?⦄ )" "cpye_alt ( ⦃?,?⦄ ⊢ ? ▶▶*[?,?] 𝐍⦃?⦄ )" "cpye_lift" + "cpye_cpye" * ]
- }
- ]
[ { "contxt-sensitive extended multiple substitution" * } {
- [ "cpys ( ⦃?,?⦄ ⊢ ? ▶*[?,?] ? )" "cpys_alt ( ⦃?,?⦄ ⊢ ? ▶▶*[?,?] ? )" "cpys_lift" + "cpys_cny" + "cpys_cpys" * ]
+ [ "cpys ( ⦃?,?⦄ ⊢ ? ▶*[?,?] ? )" "cpys_alt ( ⦃?,?⦄ ⊢ ? ▶▶*[?,?] ? )" "cpys_lift" + "cpys_cpys" * ]
}
]
[ { "iterated structural successor for closures" * } {
]
class "orange"
[ { "relocation" * } {
- [ { "normal forms for context-sensitive extended substitution" * } {
- [ "cny ( ⦃?,?⦄ ⊢ ▶[?,?] 𝐍⦃?⦄ )" "cny_lift" * ]
- }
- ]
[ { "contxt-sensitive extended ordinary substitution" * } {
[ "cpy ( ⦃?,?⦄ ⊢ ? ▶[?,?] ? )" "cpy_lift" + "cpy_cpy" * ]
}
projects / helm.git / commitdiff