- poinwise extensions downgraded (current llor does not need the improved version)
- some refactoring in etc
--- /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 "hvbox( L1 ⊢ ⬌* break term 46 L2 )"
+ non associative with precedence 45
+ for @{ 'CPConvStar $L1 $L2 }.
+
+include "basic_2/grammar/lenv_px_sn.ma".
+include "basic_2/equivalence/cpcs.ma".
+
+(* CONTEXT-SENSITIVE PARALLEL EQUIVALENCE ON LOCAL ENVIRONMENTS *************)
+
+definition lcpcs: relation lenv ≝ lpx_sn … cpcs.
+
+interpretation "context-sensitive parallel equivalence (local environment)"
+ 'CPConvStar L1 L2 = (lcpcs L1 L2).
+
+(* Basic inversion lemmas ***************************************************)
+
+lemma lcpcs_inv_atom1: ∀L2. ⋆ ⊢ ⬌* L2 → L2 = ⋆.
+/2 width=2 by lpx_sn_inv_atom1/ qed-.
+
+lemma lcpcs_inv_pair1: ∀I,K1,V1,L2. K1. ⓑ{I} V1 ⊢ ⬌* L2 →
+ ∃∃K2,V2. K1 ⊢ ⬌* K2 & K1 ⊢ V1 ⬌* V2 & L2 = K2. ⓑ{I} V2.
+/2 width=1 by lpx_sn_inv_pair1/ qed-.
+
+lemma lcpcs_inv_atom2: ∀L1. L1 ⊢ ⬌* ⋆ → L1 = ⋆.
+/2 width=2 by lpx_sn_inv_atom2/ qed-.
+
+lemma lcpcs_inv_pair2: ∀I,L1,K2,V2. L1 ⊢ ⬌* K2. ⓑ{I} V2 →
+ ∃∃K1,V1. K1 ⊢ ⬌* K2 & K1 ⊢ V1 ⬌* V2 & L1 = K1. ⓑ{I} V1.
+/2 width=1 by lpx_sn_inv_pair2/ qed-.
+
+(* Basic forward lemmas *****************************************************)
+
+lemma lcpcs_fwd_length: ∀L1,L2. L1 ⊢ ⬌* L2 → |L1| = |L2|.
+/2 width=2 by lpx_sn_fwd_length/ 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/reducibility/ltpr.ma".
+include "basic_2/equivalence/lcpcs.ma".
+
+(* CONTEXT-SENSITIVE PARALLEL EQUIVALENCE ON LOCAL ENVIRONMENTS *************)
+
+(* Properties on context-free parallel reduction for local environments *****)
+
+lemma ltpr_lcpcs: ∀L1,L2. L1 ➡ L2 → L1 ⊢ ⬌* L2.
+#L1 #L2 #H elim H -L1 -L2 // /4 width=1/
+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 "hvbox( L1 ⊢ ⬌* break term 46 L2 )"
- non associative with precedence 45
- for @{ 'CPConvStar $L1 $L2 }.
-
-include "basic_2/grammar/lenv_px_sn.ma".
-include "basic_2/equivalence/cpcs.ma".
-
-(* CONTEXT-SENSITIVE PARALLEL EQUIVALENCE ON LOCAL ENVIRONMENTS *************)
-
-definition lcpcs: relation lenv ≝ lpx_sn … cpcs.
-
-interpretation "context-sensitive parallel equivalence (local environment)"
- 'CPConvStar L1 L2 = (lcpcs L1 L2).
-
-(* Basic inversion lemmas ***************************************************)
-
-lemma lcpcs_inv_atom1: ∀L2. ⋆ ⊢ ⬌* L2 → L2 = ⋆.
-/2 width=2 by lpx_sn_inv_atom1/ qed-.
-
-lemma lcpcs_inv_pair1: ∀I,K1,V1,L2. K1. ⓑ{I} V1 ⊢ ⬌* L2 →
- ∃∃K2,V2. K1 ⊢ ⬌* K2 & K1 ⊢ V1 ⬌* V2 & L2 = K2. ⓑ{I} V2.
-/2 width=1 by lpx_sn_inv_pair1/ qed-.
-
-lemma lcpcs_inv_atom2: ∀L1. L1 ⊢ ⬌* ⋆ → L1 = ⋆.
-/2 width=2 by lpx_sn_inv_atom2/ qed-.
-
-lemma lcpcs_inv_pair2: ∀I,L1,K2,V2. L1 ⊢ ⬌* K2. ⓑ{I} V2 →
- ∃∃K1,V1. K1 ⊢ ⬌* K2 & K1 ⊢ V1 ⬌* V2 & L1 = K1. ⓑ{I} V1.
-/2 width=1 by lpx_sn_inv_pair2/ qed-.
-
-(* Basic forward lemmas *****************************************************)
-
-lemma lcpcs_fwd_length: ∀L1,L2. L1 ⊢ ⬌* L2 → |L1| = |L2|.
-/2 width=2 by lpx_sn_fwd_length/ 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/reducibility/ltpr.ma".
-include "basic_2/equivalence/lcpcs.ma".
-
-(* CONTEXT-SENSITIVE PARALLEL EQUIVALENCE ON LOCAL ENVIRONMENTS *************)
-
-(* Properties on context-free parallel reduction for local environments *****)
-
-lemma ltpr_lcpcs: ∀L1,L2. L1 ➡ L2 → L1 ⊢ ⬌* L2.
-#L1 #L2 #H elim H -L1 -L2 // /4 width=1/
-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/grammar/lenv_length.ma".
-
-(* SN POINTWISE EXTENSION OF A CONTEXT-SENSITIVE REALTION FOR TERMS **********)
-
-inductive lpx_sn (R:lenv→relation term): relation lenv ≝
-| lpx_sn_stom: lpx_sn R (⋆) (⋆)
-| lpx_sn_pair: ∀I,K1,K2,V1,V2.
- lpx_sn R K1 K2 → R K1 V1 V2 → lpx_sn R (K1. ⓑ{I} V1) (K2. ⓑ{I} V2)
-.
-
-(* Basic inversion lemmas ***************************************************)
-
-fact lpx_sn_inv_atom1_aux: ∀R,L1,L2. lpx_sn R L1 L2 → L1 = ⋆ → L2 = ⋆.
-#R #L1 #L2 * -L1 -L2
-[ //
-| #I #K1 #K2 #V1 #V2 #_ #_ #H destruct
-]
-qed-.
-
-lemma lpx_sn_inv_atom1: ∀R,L2. lpx_sn R (⋆) L2 → L2 = ⋆.
-/2 width=4 by lpx_sn_inv_atom1_aux/ qed-.
-
-fact lpx_sn_inv_pair1_aux: ∀R,L1,L2. lpx_sn R L1 L2 → ∀I,K1,V1. L1 = K1. ⓑ{I} V1 →
- ∃∃K2,V2. lpx_sn R K1 K2 & R K1 V1 V2 & L2 = K2. ⓑ{I} V2.
-#R #L1 #L2 * -L1 -L2
-[ #J #K1 #V1 #H destruct
-| #I #K1 #K2 #V1 #V2 #HK12 #HV12 #J #L #W #H destruct /2 width=5/
-]
-qed-.
-
-lemma lpx_sn_inv_pair1: ∀R,I,K1,V1,L2. lpx_sn R (K1. ⓑ{I} V1) L2 →
- ∃∃K2,V2. lpx_sn R K1 K2 & R K1 V1 V2 & L2 = K2. ⓑ{I} V2.
-/2 width=3 by lpx_sn_inv_pair1_aux/ qed-.
-
-fact lpx_sn_inv_atom2_aux: ∀R,L1,L2. lpx_sn R L1 L2 → L2 = ⋆ → L1 = ⋆.
-#R #L1 #L2 * -L1 -L2
-[ //
-| #I #K1 #K2 #V1 #V2 #_ #_ #H destruct
-]
-qed-.
-
-lemma lpx_sn_inv_atom2: ∀R,L1. lpx_sn R L1 (⋆) → L1 = ⋆.
-/2 width=4 by lpx_sn_inv_atom2_aux/ qed-.
-
-fact lpx_sn_inv_pair2_aux: ∀R,L1,L2. lpx_sn R L1 L2 → ∀I,K2,V2. L2 = K2. ⓑ{I} V2 →
- ∃∃K1,V1. lpx_sn R K1 K2 & R K1 V1 V2 & L1 = K1. ⓑ{I} V1.
-#R #L1 #L2 * -L1 -L2
-[ #J #K2 #V2 #H destruct
-| #I #K1 #K2 #V1 #V2 #HK12 #HV12 #J #K #W #H destruct /2 width=5/
-]
-qed-.
-
-lemma lpx_sn_inv_pair2: ∀R,I,L1,K2,V2. lpx_sn R L1 (K2. ⓑ{I} V2) →
- ∃∃K1,V1. lpx_sn R K1 K2 & R K1 V1 V2 & L1 = K1. ⓑ{I} V1.
-/2 width=3 by lpx_sn_inv_pair2_aux/ qed-.
-
-(* Basic forward lemmas *****************************************************)
-
-lemma lpx_sn_fwd_length: ∀R,L1,L2. lpx_sn R L1 L2 → |L1| = |L2|.
-#R #L1 #L2 #H elim H -L1 -L2 normalize //
-qed-.
+++ /dev/null
-(**************************************************************************)
-(* ___ *)
-(* ||M|| *)
-(* ||A|| A project by Andrea Asperti *)
-(* ||T|| *)
-(* ||I|| Developers: *)
-(* ||T|| The HELM team. *)
-(* ||A|| http://helm.cs.unibo.it *)
-(* \ / *)
-(* \ / This file is distributed under the terms of the *)
-(* v GNU General Public License Version 2 *)
-(* *)
-(**************************************************************************)
-
-include "ground_2/xoa/xoa2.ma".
-include "basic_2/notation/relations/lazyor_4.ma".
-include "basic_2/relocation/lpx_sn_alt.ma".
-include "basic_2/substitution/cofrees.ma".
-
-(* POINTWISE UNION FOR LOCAL ENVIRONMENTS ***********************************)
-
-inductive clor (T) (L2) (I) (K1) (V1): predicate term ≝
-| clor_sn: |K1| < |L2| → |L2|-|K1|-1 ~ϵ 𝐅*⦃K1, T⦄ → clor T L2 I K1 V1 V1
-| clor_dx: ∀K2,V2. |K1| < |L2| → (|L2|-|K1|-1 ~ϵ 𝐅*⦃K1, T⦄ → ⊥) →
- ⇩[|L2|-|K1|-1] L2 ≡ K2.ⓑ{I}V2 → clor T L2 I K1 V1 V2
-.
-
-definition llor: relation4 term lenv lenv lenv ≝
- λT,L2. lpx_sn (clor T L2).
-
-interpretation
- "lazy union (local environment)"
- 'LazyOr L1 T L2 L = (llor T L2 L1 L).
-
-(* Basic properties *********************************************************)
-
-lemma llor_pair_sn: ∀I,L1,L2,L,V,T. L1 ⩖[T] L2 ≡ L →
- |L1| < |L2| → |L2|-|L1|-1 ~ϵ 𝐅*⦃L1, T⦄ →
- L1.ⓑ{I}V ⩖[T] L2 ≡ L.ⓑ{I}V.
-/3 width=2 by clor_sn, lpx_sn_pair/ qed.
-
-lemma llor_pair_dx: ∀I,L1,L2,L,K2,V1,V2,T. L1 ⩖[T] L2 ≡ L →
- |L1| < |L2| → (|L2|-|L1|-1 ~ϵ 𝐅*⦃L1, T⦄ → ⊥) →
- ⇩[|L2|-|L1|-1] L2 ≡ K2.ⓑ{I}V2 →
- L1.ⓑ{I}V1 ⩖[T] L2 ≡ L.ⓑ{I}V2.
-/4 width=3 by clor_dx, lpx_sn_pair/ qed.
-(*
-lemma llor_total: ∀T,L2,L1. |L1| ≤ |L2| → ∃L. L1 ⩖[T] L2 ≡ L.
-#T #L2 #L1 elim L1 -L1 /2 width=2 by ex_intro/
-#L1 #I1 #V1 #IHL1 normalize
-#H elim IHL1 -IHL1 /2 width=3 by transitive_le/
-#L #HT elim (cofrees_dec L1 T (|L2|-|L1|-1))
-[ /3 width=2 by llor_pair_sn, ex_intro/
-| elim (ldrop_O1_lt L2 (|L2|-|L1|-1))
- /5 width=4 by llor_pair_dx, monotonic_lt_minus_l, ex_intro/
-|
-]
-qed-.
-*)
-(* Alternative definition ***************************************************)
-
-(* Note: uses minus_minus_comm, minus_plus_m_m, commutative_plus, plus_minus *)
-lemma plus_minus_minus_be: ∀x,y,z:nat. y ≤ z → z ≤ x → (x - z) + (z - y) = x - y.
-#x #z #y #Hzy #Hyx >plus_minus // >commutative_plus >plus_minus //
-qed-.
-
-fact plus_minus_minus_be_aux: ∀i,x,y,z:nat. y ≤ z → z ≤ x → i = z - y → x - z + i = x - y.
-/2 width=1 by plus_minus_minus_be/ qed-.
-
-lemma llor_intro_alt: ∀T,L2,L1,L. |L1| ≤ |L2| → |L1| = |L| →
- (∀I1,I,K1,K,V1,V,i. ⇩[i] L1 ≡ K1.ⓑ{I1}V1 → ⇩[i] L ≡ K.ⓑ{I}V →
- (|L2|-|L1|+i ~ϵ 𝐅*⦃K1, T⦄ → I1 = I ∧ V1 = V) ∧
- (∀I2,K2,V2. (|L2|-|L1|+i ~ϵ 𝐅*⦃K1, T⦄ → ⊥) →
- ⇩[|L2|-|L1|+i] L2 ≡ K2.ⓑ{I2}V2 →
- ∧∧ I1 = I & I2 = I & V2 = V
- )
- ) → L1 ⩖[T] L2 ≡ L.
-#T #L2 #L1 #L #HL12 #HL1 #IH @lpx_sn_intro_alt // -HL1
-#I1 #I #K1 #K #V1 #V #i #HLK1 #HLK
-lapply (ldrop_fwd_length_minus4 … HLK1)
-lapply (ldrop_fwd_length_le4 … HLK1)
-normalize #HKL1 #H1i lapply (plus_minus_minus_be_aux … HL12 H1i) // #H2i
-lapply (transitive_le … HKL1 HL12) -HKL1 -HL12 #HKL1
-elim (IH … HLK1 HLK) -IH -HLK1 -HLK #IH1 #IH2
-elim (cofrees_dec K1 T (|L2|-|L1|+i))
-[ -IH2 #HT elim (IH1 … HT) -IH1
- /3 width=2 by clor_sn, conj/
-| -IH1 #H elim (ldrop_O1_lt L2 (|L2|-|L1|+i)) /2 width=1 by monotonic_lt_minus_l/
- #I2 #K2 #V2 #HLK2 elim (IH2 … HLK2) -IH2
- /5 width=3 by clor_dx, ex_intro, and3_intro/
-]
-qed.
-
-lemma llor_inv_alt: ∀T,L2,L1,L. L1 ⩖[T] L2 ≡ L → |L1| ≤ |L2| →
- |L1| = |L| ∧
- (∀I1,I,K1,K,V1,V,i.
- ⇩[i] L1 ≡ K1.ⓑ{I1}V1 → ⇩[i] L ≡ K.ⓑ{I}V →
- (∃∃U. ⇧[|L2|-|L1|+i, 1] U ≡ T &
- I1 = I & V1 = V & K1 ⩖[T] L2 ≡ K
- ) ∨
- (∃∃I2,K2,V2. (∀U. ⇧[|L2|-|L1|+i, 1] U ≡ T → ⊥) &
- ⇩[|L2|-|L1|+i] L2 ≡ K2.ⓑ{I2}V2 &
- I1 = I & V2 = V & K1 ⩖[T] L2 ≡ K
- )
- ).
-#T #L2 #L1 #L #H #HL12 elim (lpx_sn_inv_alt … H) -H
-#HL1 #IH @conj // -HL1
-#I1 #I #K1 #K #V1 #V #i #HLK1 #HLK
-lapply (ldrop_fwd_length_minus4 … HLK1)
-lapply (ldrop_fwd_length_le4 … HLK1)
-normalize #HKL1 #H1i lapply (plus_minus_minus_be_aux … HL12 H1i) //
-lapply (transitive_le … HKL1 HL12) -HKL1 -HL12
-elim (IH … HLK1 HLK) -IH #H *
-/4 width=5 by ex5_3_intro, ex4_intro, or_intror, or_introl/
-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/llor.ma".
+include "basic_2/substitution/lleq_alt.ma".
+
+(* LAZY EQUIVALENCE FOR LOCAL ENVIRONMENTS **********************************)
+
+(* Properties on poinwise union for local environments **********************)
+
+lemma llor_lleq_O: ∀T,L1,L2,L. L1 ⩖[T] L2 ≡ L → |L1| ≤ |L2| → |L2| = |L| → L2 ⋕[T, yinj 0] L.
+#T #L1 @(f2_ind … rfw … L1 T) -L1 -T
+#n #IH #L1 #T #Hn #L2 #L #H #HL12 #HL2 elim (llor_inv_alt … H) // destruct
+#HL1 #IHT @lleq_intro_alt //
+#I2 #I #K2 #K #V2 #V #i #_ #HnT #HLK2 #HLK lapply (ldrop_fwd_length_lt2 … HLK)
+#Hi elim (ldrop_O1_lt L1 i) //
+#I1 #K1 #V1 #HLK1 elim (IHT … HLK1 HLK) >HL1 >HL2 <minus_n_n -IHT -HLK1 -HLK
+[
+| * #I0 #K0 #V0 #_ #HLK0 lapply (ldrop_mono … HLK0 … HLK2) -HLK0 -HLK2
+ #H1 #H2 #H3 #_ destruct
+
+
+
+
--- /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/llor.ma".
+include "basic_2/computation/cpxs_lleq.ma".
+include "basic_2/computation/lpxs_ldrop.ma".
+include "basic_2/computation/lpxs_cpxs.ma".
+include "basic_2/computation/lpxs_lpxs.ma".
+
+(* SN EXTENDED PARALLEL REDUCTION FOR LOCAL ENVIRONMENTS ********************)
+
+axiom llor_fwd_sort: ∀L1,L2,L,d,k. L1 ⩖ [⋆k, d] L2 ≡ L → L = L2.
+
+axiom llor_fwd_lref: ∀L1,L2,L,d,i. L1 ⩖ [#i, d] L2 ≡ L →
+ ∨∨ (|L| ≤ i ∧ L = L2)
+ | (yinj i < d ∧ L = L2)
+ | ∃∃I1,I2,K1,K2,K,V1,V2. ⇩[i] L1 ≡ K1.ⓑ{I1}V1 &
+ ⇩[i] L2 ≡ K2.ⓑ{I2}V2 &
+ ⇩[i] L ≡ K.ⓑ{I2}V1 &
+ L2 ≃[yinj 0, yinj i] L &
+ K1 ⩖[V1, yinj 0] K2 ≡ K &
+ d ≤ yinj i.
+
+
+axiom llor_fwd_lref_lt: ∀L1,L2,L,d,i. L1 ⩖ [#i, d] L2 ≡ L → i < d → L = L2.
+
+axiom llor_inv_lref_be: ∀L1,L2,L,d,i. L1 ⩖ [#i, d] L2 ≡ L → d ≤ i →
+ ∀I1,I2,K1,K2,V1,V2. ⇩[i] L1 ≡ K1.ⓑ{I1}V1 → ⇩[i] L2 ≡ K2.ⓑ{I2}V2 →
+ ∃∃K. ⇩[i] L ≡ K.ⓑ{I2}V1 & L2 ≃[0, i] L &
+ K1 ⩖[V1, 0] K2 ≡ K.
+
+axiom llor_fwd_gref: ∀L1,L2,L,d,p. L1 ⩖ [§p, d] L2 ≡ L → L = L2.
+
+axiom llor_inv_bind: ∀a,I,L1,L2,L,V,T,d. L1 ⩖ [ⓑ{a,I}V.T, d] L2 ≡ L →
+ ∃∃L0. L1 ⩖ [V, d] L2 ≡ L0 & L1.ⓑ{I}V ⩖ [T, ⫯d] L0.ⓑ{I}V ≡ L.ⓑ{I}V.
+
+axiom llor_inv_flat: ∀I,L1,L2,L,V,T,d. L1 ⩖ [ⓕ{I}V.T, d] L2 ≡ L →
+ ∃∃L0. L1 ⩖ [V, d] L2 ≡ L0 & L1 ⩖ [T, d] L0 ≡ L.
+
+axiom llor_fwd_length_13: ∀L1,L2,L,T,d. L1 ⩖ [T, d] L2 ≡ L → |L1| = |L|.
+
+(* Properties obn lazy union for local environments *************************)
+
+lemma lpxs_llor_sn: ∀h,g,G,L1s,L0,L1d,T,d. L1s ⩖[T, d] L0 ≡ L1d →
+ ∀L2s,L2d. L2s ⩖[T, d] L0 ≡ L2d →
+ ⦃G, L1s⦄ ⊢ ➡*[h, g] L2s → ⦃G, L1d⦄ ⊢ ➡*[h, g] L2d.
+#h #g #G #L1s #L0 #L1d #T #d #H elim H -L1s -L0 -L1d -T -d
+[ #L1s #L0 #d #k #_ #L2s #L2d #H #_ >(llor_fwd_sort … H) //
+| #L1s #L0 #d #i #_ #Hid #L2s #L2d #H #_ >(llor_fwd_lref_lt … H) //
+| #I1s #I0 #L1s #L0 #L1d #K1s #K0 #K1d #V1s #V0 #d #i #Hdi #HLK1s #HLK0 #HLK1d #HL01d #HV1s #IHV1s #L2s #L2d #H #HL12s
+ elim (lpxs_ldrop_conf … HLK1s … HL12s) -L1s #Y #H #HLK2s
+ elim (lpxs_inv_pair1 … H) -H #K2s #V2s #HK12s #HV12s #H destruct
+ elim (llor_inv_lref_be … H … HLK2s HLK0) // -L2s -HLK0 -Hdi #K2d #HLK2d #HL02d #HV2s
+ lapply (leq_canc_sn … HL01d … HL02d) -L0 #HL12d
+ lapply (IHV1s … K2d … HK12s) -IHV1s -HK12s [2: #HK12d
+
+
+
+
+[ #I2d #I1s #L2d #L1s #L2s #K2d #K1s #K2s #V2d #V1s #d #i #Hdi #HLK2d #HLK1s #HLK2s #HL12s #_ #IHV2s #L1d #HL1sd #HL12d
+ elim (lpxs_ldrop_trans_O1 … HL12d … HLK2d) -L2d #Y #HLK1d #H
+ elim (lpxs_inv_pair2 … H) -H #K1d #V1d #HK12d #HV12d #H destruct
+ elim (lleq_inv_lref_ge … HL1sd … HLK1s HLK1d) // -d -I2d #H #HV1d destruct
+ lapply (lleq_cpxs_conf_dx … HV12d … HV1d) #HV2d
+ lapply (lleq_cpxs_trans … HV12d … HV1d) -HV12d -HV1d #HV12d
+ lapply (IHV2s … HV2d HK12d) -L1d -K1d -K2d #HK12s
+ elim (ldrop_lpxs_trans h g G … HLK1s (K2s.ⓑ{I1s}V2d)) /2 width=1 by lpxs_pair/ -V1d -K1s #Y #HL1sY #HYK2s #H
+ lapply (leq_canc_sn … HL12s … H) -HL12s -H #HL2sY
+ lapply (ldrop_O_inj … HLK2s HYK2s) -I1s -K2s -V2d #H
+ lapply (leq_join … HL2sY … H) -HL2sY -H #HL2sY
+ >(leq_inv_O_Y … HL2sY) -HL2sY //
+
+
+
+
+
+lemma lleq_lpxs_trans_llor: ∀h,g,G,L1s,L2s,L2d,T,d. L2d ⩖[T, d] L1s ≡ L2s →
+ ∀L1d. L1s ⋕[T, d] L1d → ⦃G, L1d⦄ ⊢ ➡*[h, g] L2d → ⦃G, L1s⦄ ⊢ ➡*[h, g] L2s.
+#h #g #G #L1s #L2s #L2d #T #d #H elim H -L1s -L2s -L2d -T -d //
+[ #I2d #I1s #L2d #L1s #L2s #K2d #K1s #K2s #V2d #V1s #d #i #Hdi #HLK2d #HLK1s #HLK2s #HL12s #_ #IHV2s #L1d #HL1sd #HL12d
+ elim (lpxs_ldrop_trans_O1 … HL12d … HLK2d) -L2d #Y #HLK1d #H
+ elim (lpxs_inv_pair2 … H) -H #K1d #V1d #HK12d #HV12d #H destruct
+ elim (lleq_inv_lref_ge … HL1sd … HLK1s HLK1d) // -d -I2d #H #HV1d destruct
+ lapply (lleq_cpxs_conf_dx … HV12d … HV1d) #HV2d
+ lapply (lleq_cpxs_trans … HV12d … HV1d) -HV12d -HV1d #HV12d
+ lapply (IHV2s … HV2d HK12d) -L1d -K1d -K2d #HK12s
+ elim (ldrop_lpxs_trans h g G … HLK1s (K2s.ⓑ{I1s}V2d)) /2 width=1 by lpxs_pair/ -V1d -K1s #Y #HL1sY #HYK2s #H
+ lapply (leq_canc_sn … HL12s … H) -HL12s -H #HL2sY
+ lapply (ldrop_O_inj … HLK2s HYK2s) -I1s -K2s -V2d #H
+ lapply (leq_join … HL2sY … H) -HL2sY -H #HL2sY
+ >(leq_inv_O_Y … HL2sY) -HL2sY //
+(*
+| #a #I #L2d #L1s #L0 #L2s #V #T #d #H0 #_ #IHV #IHT #L1d #H #HL12d
+ elim (lleq_inv_bind … H) -H #HV #HT
+*)
+| #I #L2d #L1s #LV #LT #L2s #V #T #d #H0 #_ #_ #IHV #IHT #IH #L1d #H #HL12d
+ elim (lleq_inv_flat … H) -H #HV #HT
+ lapply (IHV … HV HL12d) -HV #H1
+ lapply (IHT … HT HL12d) #H2
+
+
+
+ @(lpxs_trans … LV) /2 width=3 by/ -IHV
+ lapply (IHT … HL12d) // -IHT #H @(IH … H) -IH -H
+
+ @(IH … HL12d) -IHT -IHV
+
+ /4 width=5 by lpxs_trans/
+
+
+lemma lleq_lpx_conf_llor: ∀h,g,G,L1,L2,T,d. L1 ⋕[T, d] L2 → ∀K1. ⦃G, L1⦄ ⊢ ➡[h, g] K1 →
+ ∀K2. K1 ⩖[T, d] L2 ≡ K2 → ⦃G, L2⦄ ⊢ ➡[h, g] K2.
+#h #g #G #L1 #L2 #T #d #H @(lleq_ind_alt … H) -L1 -L2 -T -d
+[ #L1 #L2 #d #k #HL12 #K1 #HLK1 #K2 #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/substitution/llpx_sn_ldrop.ma".
+include "basic_2/reduction/cpr.ma".
+
+(* CONTEXT-SENSITIVE PARALLEL REDUCTION FOR TERMS ***************************)
+
+(* Properties on lazy sn pointwise extensions *******************************)
+
+lemma cpr_llpx_sn_conf: ∀R. (∀I,L.reflexive … (R I L)) →
+ (∀I.l_liftable (R I)) →
+ (∀I.l_deliftable_sn (R I)) →
+ ∀G. s_r_confluent1 … (cpr G) (llpx_sn R 0).
+#R #H1R #H2R #H3R #G #Ls #T1 #T2 #H elim H -G -Ls -T1 -T2
+[ //
+| #G #Ls #Ks #V1s #V2s #W2s #i #HLKs #_ #HVW2s #IHV12s #Ld #H elim (llpx_sn_inv_lref_ge_sn … H … HLKs) // -H
+ #Kd #V1d #HLKd #HV1s #HV1sd
+ lapply (ldrop_fwd_drop2 … HLKs) -HLKs #HLKs
+ lapply (ldrop_fwd_drop2 … HLKd) -HLKd #HLKd
+ @(llpx_sn_lift_le … HLKs HLKd … HVW2s) -HLKs -HLKd -HVW2s /2 width=1 by/ (**) (* full auto too slow *)
+| #a #I #G #Ls #V1 #V2 #T1 #T2 #_ #_ #IHV12 #IHT12 #Ld #H elim (llpx_sn_inv_bind_O … H) -H
+ /4 width=5 by llpx_sn_bind_repl_SO, llpx_sn_bind/
+| #I #G #Ls #V1 #V2 #T1 #T2 #_ #_ #IHV12 #IHT12 #Ld #H elim (llpx_sn_inv_flat … H) -H
+ /3 width=1 by llpx_sn_flat/
+| #G #Ls #V #T1 #T2 #T #_ #HT2 #IHT12 #Ld #H elim (llpx_sn_inv_bind_O … H) -H
+ /3 width=10 by llpx_sn_inv_lift_le, ldrop_drop/
+| #G #Ls #V #T1 #T2 #_ #IHT12 #Ld #H elim (llpx_sn_inv_flat … H) -H /2 width=1 by/
+| #a #G #Ls #V1 #V2 #W1 #W2 #T1 #T2 #_ #_ #_ #IHV12 #IHW12 #IHT12 #Ld #H elim (llpx_sn_inv_flat … H) -H
+ #HV1 #H elim (llpx_sn_inv_bind_O … H) -H
+ /4 width=5 by llpx_sn_bind_repl_SO, llpx_sn_flat, llpx_sn_bind/
+| #a #G #Ls #V1 #V2 #V #W1 #W2 #T1 #T2 #_ #HV2 #_ #_ #IHV12 #IHW12 #IHT12 #Ld #H elim (llpx_sn_inv_flat … H) -H
+ #HV1 #H elim (llpx_sn_inv_bind_O … H) -H //
+ #HW1 #HT1 @llpx_sn_bind_O /2 width=1 by/ @llpx_sn_flat (**) (* full auto too slow *)
+ [ /3 width=10 by llpx_sn_lift_le, ldrop_drop/
+ | /3 width=4 by llpx_sn_bind_repl_O/
+]
+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/llpx_sn_ldrop.ma".
+include "basic_2/reduction/cpx.ma".
+
+(* CONTEXT-SENSITIVE EXTENDED PARALLEL REDUCTION FOR TERMS ******************)
+
+(* Properties on lazy sn pointwise extensions *******************************)
+
+(* Note: lemma 1000 *)
+lemma cpx_llpx_sn_conf: ∀R. (∀I,L.reflexive … (R I L)) →
+ (∀I.l_liftable (R I)) →
+ (∀I.l_deliftable_sn (R I)) →
+ ∀h,g,G. s_r_confluent1 … (cpx h g G) (llpx_sn R 0).
+#R #H1R #H2R #H3R #h #g #G #Ls #T1 #T2 #H elim H -G -Ls -T1 -T2
+[ //
+| /3 width=4 by llpx_sn_fwd_length, llpx_sn_sort/
+| #I #G #Ls #Ks #V1s #V2s #W2s #i #HLKs #_ #HVW2s #IHV12s #Ld #H elim (llpx_sn_inv_lref_ge_sn … H … HLKs) // -H
+ #Kd #V1d #HLKd #HV1s #HV1sd
+ lapply (ldrop_fwd_drop2 … HLKs) -HLKs #HLKs
+ lapply (ldrop_fwd_drop2 … HLKd) -HLKd #HLKd
+ @(llpx_sn_lift_le … HLKs HLKd … HVW2s) -HLKs -HLKd -HVW2s /2 width=1 by/ (**) (* full auto too slow *)
+| #a #I #G #Ls #V1 #V2 #T1 #T2 #_ #_ #IHV12 #IHT12 #Ld #H elim (llpx_sn_inv_bind_O … H) -H
+ /4 width=5 by llpx_sn_bind_repl_SO, llpx_sn_bind/
+| #I #G #Ls #V1 #V2 #T1 #T2 #_ #_ #IHV12 #IHT12 #Ld #H elim (llpx_sn_inv_flat … H) -H
+ /3 width=1 by llpx_sn_flat/
+| #G #Ls #V #T1 #T2 #T #_ #HT2 #IHT12 #Ld #H elim (llpx_sn_inv_bind_O … H) -H
+ /3 width=10 by llpx_sn_inv_lift_le, ldrop_drop/
+| #G #Ls #V #T1 #T2 #_ #IHT12 #Ld #H elim (llpx_sn_inv_flat … H) -H /2 width=1 by/
+| #G #Ls #V1 #V2 #T #_ #IHV12 #Ld #H elim (llpx_sn_inv_flat … H) -H /2 width=1 by/
+| #a #G #Ls #V1 #V2 #W1 #W2 #T1 #T2 #_ #_ #_ #IHV12 #IHW12 #IHT12 #Ld #H elim (llpx_sn_inv_flat … H) -H
+ #HV1 #H elim (llpx_sn_inv_bind_O … H) -H
+ /4 width=5 by llpx_sn_bind_repl_SO, llpx_sn_flat, llpx_sn_bind/
+| #a #G #Ls #V1 #V2 #V #W1 #W2 #T1 #T2 #_ #HV2 #_ #_ #IHV12 #IHW12 #IHT12 #Ld #H elim (llpx_sn_inv_flat … H) -H
+ #HV1 #H elim (llpx_sn_inv_bind_O … H) -H //
+ #HW1 #HT1 @llpx_sn_bind_O /2 width=1 by/ @llpx_sn_flat (**) (* full auto too slow *)
+ [ /3 width=10 by llpx_sn_lift_le, ldrop_drop/
+ | /3 width=4 by llpx_sn_bind_repl_O/
+]
+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/lazyeq_4.ma".
+include "basic_2/substitution/llpx_sn.ma".
+
+(* LAZY EQUIVALENCE FOR LOCAL ENVIRONMENTS **********************************)
+
+definition ceq: relation4 bind2 lenv term term ≝ λI,L,T1,T2. T1 = T2.
+
+definition lleq: relation4 ynat term lenv lenv ≝ llpx_sn ceq.
+
+interpretation
+ "lazy equivalence (local environment)"
+ 'LazyEq T d L1 L2 = (lleq d T L1 L2).
+
+definition lleq_transitive: predicate (relation4 bind2 lenv term term) ≝
+ λR. ∀I,L2,T1,T2. R I L2 T1 T2 → ∀L1. L1 ≡[T1, 0] L2 → R I L1 T1 T2.
+
+(* Basic inversion lemmas ***************************************************)
+
+lemma lleq_ind: ∀R:relation4 ynat term lenv lenv. (
+ ∀L1,L2,d,k. |L1| = |L2| → R d (⋆k) L1 L2
+ ) → (
+ ∀L1,L2,d,i. |L1| = |L2| → yinj i < d → R d (#i) L1 L2
+ ) → (
+ ∀I,L1,L2,K1,K2,V,d,i. d ≤ yinj i →
+ ⇩[i] L1 ≡ K1.ⓑ{I}V → ⇩[i] L2 ≡ K2.ⓑ{I}V →
+ K1 ≡[V, yinj O] K2 → R (yinj O) V K1 K2 → R d (#i) L1 L2
+ ) → (
+ ∀L1,L2,d,i. |L1| = |L2| → |L1| ≤ i → |L2| ≤ i → R d (#i) L1 L2
+ ) → (
+ ∀L1,L2,d,p. |L1| = |L2| → R d (§p) L1 L2
+ ) → (
+ ∀a,I,L1,L2,V,T,d.
+ L1 ≡[V, d]L2 → L1.ⓑ{I}V ≡[T, ⫯d] L2.ⓑ{I}V →
+ R d V L1 L2 → R (⫯d) T (L1.ⓑ{I}V) (L2.ⓑ{I}V) → R d (ⓑ{a,I}V.T) L1 L2
+ ) → (
+ ∀I,L1,L2,V,T,d.
+ L1 ≡[V, d]L2 → L1 ≡[T, d] L2 →
+ R d V L1 L2 → R d T L1 L2 → R d (ⓕ{I}V.T) L1 L2
+ ) →
+ ∀d,T,L1,L2. L1 ≡[T, d] L2 → R d T L1 L2.
+#R #H1 #H2 #H3 #H4 #H5 #H6 #H7 #d #T #L1 #L2 #H elim H -L1 -L2 -T -d /2 width=8 by/
+qed-.
+
+lemma lleq_inv_bind: ∀a,I,L1,L2,V,T,d. L1 ≡[ⓑ{a,I}V.T, d] L2 →
+ L1 ≡[V, d] L2 ∧ L1.ⓑ{I}V ≡[T, ⫯d] L2.ⓑ{I}V.
+/2 width=2 by llpx_sn_inv_bind/ qed-.
+
+lemma lleq_inv_flat: ∀I,L1,L2,V,T,d. L1 ≡[ⓕ{I}V.T, d] L2 →
+ L1 ≡[V, d] L2 ∧ L1 ≡[T, d] L2.
+/2 width=2 by llpx_sn_inv_flat/ qed-.
+
+(* Basic forward lemmas *****************************************************)
+
+lemma lleq_fwd_length: ∀L1,L2,T,d. L1 ≡[T, d] L2 → |L1| = |L2|.
+/2 width=4 by llpx_sn_fwd_length/ qed-.
+
+lemma lleq_fwd_lref: ∀L1,L2,d,i. L1 ≡[#i, d] L2 →
+ ∨∨ |L1| ≤ i ∧ |L2| ≤ i
+ | yinj i < d
+ | ∃∃I,K1,K2,V. ⇩[i] L1 ≡ K1.ⓑ{I}V &
+ ⇩[i] L2 ≡ K2.ⓑ{I}V &
+ K1 ≡[V, yinj 0] K2 & d ≤ yinj i.
+#L1 #L2 #d #i #H elim (llpx_sn_fwd_lref … H) /2 width=1/
+* /3 width=7 by or3_intro2, ex4_4_intro/
+qed-.
+
+lemma lleq_fwd_ldrop_sn: ∀L1,L2,T,d. L1 ≡[d, T] L2 → ∀K1,i. ⇩[i] L1 ≡ K1 →
+ ∃K2. ⇩[i] L2 ≡ K2.
+/2 width=7 by llpx_sn_fwd_ldrop_sn/ qed-.
+
+lemma lleq_fwd_ldrop_dx: ∀L1,L2,T,d. L1 ≡[d, T] L2 → ∀K2,i. ⇩[i] L2 ≡ K2 →
+ ∃K1. ⇩[i] L1 ≡ K1.
+/2 width=7 by llpx_sn_fwd_ldrop_dx/ qed-.
+
+lemma lleq_fwd_bind_sn: ∀a,I,L1,L2,V,T,d.
+ L1 ≡[ⓑ{a,I}V.T, d] L2 → L1 ≡[V, d] L2.
+/2 width=4 by llpx_sn_fwd_bind_sn/ qed-.
+
+lemma lleq_fwd_bind_dx: ∀a,I,L1,L2,V,T,d.
+ L1 ≡[ⓑ{a,I}V.T, d] L2 → L1.ⓑ{I}V ≡[T, ⫯d] L2.ⓑ{I}V.
+/2 width=2 by llpx_sn_fwd_bind_dx/ qed-.
+
+lemma lleq_fwd_flat_sn: ∀I,L1,L2,V,T,d.
+ L1 ≡[ⓕ{I}V.T, d] L2 → L1 ≡[V, d] L2.
+/2 width=3 by llpx_sn_fwd_flat_sn/ qed-.
+
+lemma lleq_fwd_flat_dx: ∀I,L1,L2,V,T,d.
+ L1 ≡[ⓕ{I}V.T, d] L2 → L1 ≡[T, d] L2.
+/2 width=3 by llpx_sn_fwd_flat_dx/ qed-.
+
+(* Basic properties *********************************************************)
+
+lemma lleq_sort: ∀L1,L2,d,k. |L1| = |L2| → L1 ≡[⋆k, d] L2.
+/2 width=1 by llpx_sn_sort/ qed.
+
+lemma lleq_skip: ∀L1,L2,d,i. yinj i < d → |L1| = |L2| → L1 ≡[#i, d] L2.
+/2 width=1 by llpx_sn_skip/ qed.
+
+lemma lleq_lref: ∀I,L1,L2,K1,K2,V,d,i. d ≤ yinj i →
+ ⇩[i] L1 ≡ K1.ⓑ{I}V → ⇩[i] L2 ≡ K2.ⓑ{I}V →
+ K1 ≡[V, 0] K2 → L1 ≡[#i, d] L2.
+/2 width=9 by llpx_sn_lref/ qed.
+
+lemma lleq_free: ∀L1,L2,d,i. |L1| ≤ i → |L2| ≤ i → |L1| = |L2| → L1 ≡[#i, d] L2.
+/2 width=1 by llpx_sn_free/ qed.
+
+lemma lleq_gref: ∀L1,L2,d,p. |L1| = |L2| → L1 ≡[§p, d] L2.
+/2 width=1 by llpx_sn_gref/ qed.
+
+lemma lleq_bind: ∀a,I,L1,L2,V,T,d.
+ L1 ≡[V, d] L2 → L1.ⓑ{I}V ≡[T, ⫯d] L2.ⓑ{I}V →
+ L1 ≡[ⓑ{a,I}V.T, d] L2.
+/2 width=1 by llpx_sn_bind/ qed.
+
+lemma lleq_flat: ∀I,L1,L2,V,T,d.
+ L1 ≡[V, d] L2 → L1 ≡[T, d] L2 → L1 ≡[ⓕ{I}V.T, d] L2.
+/2 width=1 by llpx_sn_flat/ qed.
+
+lemma lleq_refl: ∀d,T. reflexive … (lleq d T).
+/2 width=1 by llpx_sn_refl/ qed.
+
+lemma lleq_Y: ∀L1,L2,T. |L1| = |L2| → L1 ≡[T, ∞] L2.
+/2 width=1 by llpx_sn_Y/ qed.
+
+lemma lleq_sym: ∀d,T. symmetric … (lleq d T).
+#d #T #L1 #L2 #H @(lleq_ind … H) -d -T -L1 -L2
+/2 width=7 by lleq_sort, lleq_skip, lleq_lref, lleq_free, lleq_gref, lleq_bind, lleq_flat/
+qed-.
+
+lemma lleq_ge_up: ∀L1,L2,U,dt. L1 ≡[U, dt] L2 →
+ ∀T,d,e. ⇧[d, e] T ≡ U →
+ dt ≤ d + e → L1 ≡[U, d] L2.
+/2 width=6 by llpx_sn_ge_up/ qed-.
+
+lemma lleq_ge: ∀L1,L2,T,d1. L1 ≡[T, d1] L2 → ∀d2. d1 ≤ d2 → L1 ≡[T, d2] L2.
+/2 width=3 by llpx_sn_ge/ qed-.
+
+lemma lleq_bind_O: ∀a,I,L1,L2,V,T. L1 ≡[V, 0] L2 → L1.ⓑ{I}V ≡[T, 0] L2.ⓑ{I}V →
+ L1 ≡[ⓑ{a,I}V.T, 0] L2.
+/2 width=1 by llpx_sn_bind_O/ qed-.
+
+(* Advancded properties on lazy pointwise exyensions ************************)
+
+lemma llpx_sn_lrefl: ∀R. (∀I,L. reflexive … (R I L)) →
+ ∀L1,L2,T,d. L1 ≡[T, d] L2 → llpx_sn R d T L1 L2.
+/2 width=3 by llpx_sn_co/ 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/llor.ma".
-include "basic_2/substitution/lleq_alt.ma".
-
-(* LAZY EQUIVALENCE FOR LOCAL ENVIRONMENTS **********************************)
-
-(* Properties on poinwise union for local environments **********************)
-
-lemma llor_lleq_O: ∀T,L1,L2,L. L1 ⩖[T] L2 ≡ L → |L1| ≤ |L2| → |L2| = |L| → L2 ⋕[T, yinj 0] L.
-#T #L1 @(f2_ind … rfw … L1 T) -L1 -T
-#n #IH #L1 #T #Hn #L2 #L #H #HL12 #HL2 elim (llor_inv_alt … H) // destruct
-#HL1 #IHT @lleq_intro_alt //
-#I2 #I #K2 #K #V2 #V #i #_ #HnT #HLK2 #HLK lapply (ldrop_fwd_length_lt2 … HLK)
-#Hi elim (ldrop_O1_lt L1 i) //
-#I1 #K1 #V1 #HLK1 elim (IHT … HLK1 HLK) >HL1 >HL2 <minus_n_n -IHT -HLK1 -HLK
-[
-| * #I0 #K0 #V0 #_ #HLK0 lapply (ldrop_mono … HLK0 … HLK2) -HLK0 -HLK2
- #H1 #H2 #H3 #_ destruct
-
-
-
-
--- /dev/null
+(**************************************************************************)
+(* ___ *)
+(* ||M|| *)
+(* ||A|| A project by Andrea Asperti *)
+(* ||T|| *)
+(* ||I|| Developers: *)
+(* ||T|| The HELM team. *)
+(* ||A|| http://helm.cs.unibo.it *)
+(* \ / *)
+(* \ / This file is distributed under the terms of the *)
+(* v GNU General Public License Version 2 *)
+(* *)
+(**************************************************************************)
+
+include "ground_2/ynat/ynat_plus.ma".
+include "basic_2/relocation/ldrop.ma".
+
+(* LAZY SN POINTWISE EXTENSION OF A CONTEXT-SENSITIVE REALTION FOR TERMS ****)
+
+inductive llpx_sn (R:relation4 bind2 lenv term term): relation4 ynat term lenv lenv ≝
+| llpx_sn_sort: ∀L1,L2,d,k. |L1| = |L2| → llpx_sn R d (⋆k) L1 L2
+| llpx_sn_skip: ∀L1,L2,d,i. |L1| = |L2| → yinj i < d → llpx_sn R d (#i) L1 L2
+| llpx_sn_lref: ∀I,L1,L2,K1,K2,V1,V2,d,i. d ≤ yinj i →
+ ⇩[i] L1 ≡ K1.ⓑ{I}V1 → ⇩[i] L2 ≡ K2.ⓑ{I}V2 →
+ llpx_sn R (yinj 0) V1 K1 K2 → R I K1 V1 V2 → llpx_sn R d (#i) L1 L2
+| llpx_sn_free: ∀L1,L2,d,i. |L1| ≤ i → |L2| ≤ i → |L1| = |L2| → llpx_sn R d (#i) L1 L2
+| llpx_sn_gref: ∀L1,L2,d,p. |L1| = |L2| → llpx_sn R d (§p) L1 L2
+| llpx_sn_bind: ∀a,I,L1,L2,V,T,d.
+ llpx_sn R d V L1 L2 → llpx_sn R (⫯d) T (L1.ⓑ{I}V) (L2.ⓑ{I}V) →
+ llpx_sn R d (ⓑ{a,I}V.T) L1 L2
+| llpx_sn_flat: ∀I,L1,L2,V,T,d.
+ llpx_sn R d V L1 L2 → llpx_sn R d T L1 L2 → llpx_sn R d (ⓕ{I}V.T) L1 L2
+.
+
+(* Basic inversion lemmas ***************************************************)
+
+fact llpx_sn_inv_bind_aux: ∀R,L1,L2,X,d. llpx_sn R d X L1 L2 →
+ ∀a,I,V,T. X = ⓑ{a,I}V.T →
+ llpx_sn R d V L1 L2 ∧ llpx_sn R (⫯d) T (L1.ⓑ{I}V) (L2.ⓑ{I}V).
+#R #L1 #L2 #X #d * -L1 -L2 -X -d
+[ #L1 #L2 #d #k #_ #b #J #W #U #H destruct
+| #L1 #L2 #d #i #_ #_ #b #J #W #U #H destruct
+| #I #L1 #L2 #K1 #K2 #V1 #V2 #d #i #_ #_ #_ #_ #_ #b #J #W #U #H destruct
+| #L1 #L2 #d #i #_ #_ #_ #b #J #W #U #H destruct
+| #L1 #L2 #d #p #_ #b #J #W #U #H destruct
+| #a #I #L1 #L2 #V #T #d #HV #HT #b #J #W #U #H destruct /2 width=1 by conj/
+| #I #L1 #L2 #V #T #d #_ #_ #b #J #W #U #H destruct
+]
+qed-.
+
+lemma llpx_sn_inv_bind: ∀R,a,I,L1,L2,V,T,d. llpx_sn R d (ⓑ{a,I}V.T) L1 L2 →
+ llpx_sn R d V L1 L2 ∧ llpx_sn R (⫯d) T (L1.ⓑ{I}V) (L2.ⓑ{I}V).
+/2 width=4 by llpx_sn_inv_bind_aux/ qed-.
+
+fact llpx_sn_inv_flat_aux: ∀R,L1,L2,X,d. llpx_sn R d X L1 L2 →
+ ∀I,V,T. X = ⓕ{I}V.T →
+ llpx_sn R d V L1 L2 ∧ llpx_sn R d T L1 L2.
+#R #L1 #L2 #X #d * -L1 -L2 -X -d
+[ #L1 #L2 #d #k #_ #J #W #U #H destruct
+| #L1 #L2 #d #i #_ #_ #J #W #U #H destruct
+| #I #L1 #L2 #K1 #K2 #V1 #V2 #d #i #_ #_ #_ #_ #_ #J #W #U #H destruct
+| #L1 #L2 #d #i #_ #_ #_ #J #W #U #H destruct
+| #L1 #L2 #d #p #_ #J #W #U #H destruct
+| #a #I #L1 #L2 #V #T #d #_ #_ #J #W #U #H destruct
+| #I #L1 #L2 #V #T #d #HV #HT #J #W #U #H destruct /2 width=1 by conj/
+]
+qed-.
+
+lemma llpx_sn_inv_flat: ∀R,I,L1,L2,V,T,d. llpx_sn R d (ⓕ{I}V.T) L1 L2 →
+ llpx_sn R d V L1 L2 ∧ llpx_sn R d T L1 L2.
+/2 width=4 by llpx_sn_inv_flat_aux/ qed-.
+
+(* Basic forward lemmas *****************************************************)
+
+lemma llpx_sn_fwd_length: ∀R,L1,L2,T,d. llpx_sn R d T L1 L2 → |L1| = |L2|.
+#R #L1 #L2 #T #d #H elim H -L1 -L2 -T -d //
+#I #L1 #L2 #K1 #K2 #V1 #V2 #d #i #_ #HLK1 #HLK2 #_ #_ #HK12
+lapply (ldrop_fwd_length … HLK1) -HLK1
+lapply (ldrop_fwd_length … HLK2) -HLK2
+normalize //
+qed-.
+
+lemma llpx_sn_fwd_ldrop_sn: ∀R,L1,L2,T,d. llpx_sn R d T L1 L2 →
+ ∀K1,i. ⇩[i] L1 ≡ K1 → ∃K2. ⇩[i] L2 ≡ K2.
+#R #L1 #L2 #T #d #H #K1 #i #HLK1 lapply (llpx_sn_fwd_length … H) -H
+#HL12 lapply (ldrop_fwd_length_le2 … HLK1) -HLK1 /2 width=1 by ldrop_O1_le/
+qed-.
+
+lemma llpx_sn_fwd_ldrop_dx: ∀R,L1,L2,T,d. llpx_sn R d T L1 L2 →
+ ∀K2,i. ⇩[i] L2 ≡ K2 → ∃K1. ⇩[i] L1 ≡ K1.
+#R #L1 #L2 #T #d #H #K2 #i #HLK2 lapply (llpx_sn_fwd_length … H) -H
+#HL12 lapply (ldrop_fwd_length_le2 … HLK2) -HLK2 /2 width=1 by ldrop_O1_le/
+qed-.
+
+fact llpx_sn_fwd_lref_aux: ∀R,L1,L2,X,d. llpx_sn R d X L1 L2 → ∀i. X = #i →
+ ∨∨ |L1| ≤ i ∧ |L2| ≤ i
+ | yinj i < d
+ | ∃∃I,K1,K2,V1,V2. ⇩[i] L1 ≡ K1.ⓑ{I}V1 &
+ ⇩[i] L2 ≡ K2.ⓑ{I}V2 &
+ llpx_sn R (yinj 0) V1 K1 K2 &
+ R I K1 V1 V2 & d ≤ yinj i.
+#R #L1 #L2 #X #d * -L1 -L2 -X -d
+[ #L1 #L2 #d #k #_ #j #H destruct
+| #L1 #L2 #d #i #_ #Hid #j #H destruct /2 width=1 by or3_intro1/
+| #I #L1 #L2 #K1 #K2 #V1 #V2 #d #i #Hdi #HLK1 #HLK2 #HK12 #HV12 #j #H destruct
+ /3 width=9 by or3_intro2, ex5_5_intro/
+| #L1 #L2 #d #i #HL1 #HL2 #_ #j #H destruct /3 width=1 by or3_intro0, conj/
+| #L1 #L2 #d #p #_ #j #H destruct
+| #a #I #L1 #L2 #V #T #d #_ #_ #j #H destruct
+| #I #L1 #L2 #V #T #d #_ #_ #j #H destruct
+]
+qed-.
+
+lemma llpx_sn_fwd_lref: ∀R,L1,L2,d,i. llpx_sn R d (#i) L1 L2 →
+ ∨∨ |L1| ≤ i ∧ |L2| ≤ i
+ | yinj i < d
+ | ∃∃I,K1,K2,V1,V2. ⇩[i] L1 ≡ K1.ⓑ{I}V1 &
+ ⇩[i] L2 ≡ K2.ⓑ{I}V2 &
+ llpx_sn R (yinj 0) V1 K1 K2 &
+ R I K1 V1 V2 & d ≤ yinj i.
+/2 width=3 by llpx_sn_fwd_lref_aux/ qed-.
+
+lemma llpx_sn_fwd_bind_sn: ∀R,a,I,L1,L2,V,T,d. llpx_sn R d (ⓑ{a,I}V.T) L1 L2 →
+ llpx_sn R d V L1 L2.
+#R #a #I #L1 #L2 #V #T #d #H elim (llpx_sn_inv_bind … H) -H //
+qed-.
+
+lemma llpx_sn_fwd_bind_dx: ∀R,a,I,L1,L2,V,T,d. llpx_sn R d (ⓑ{a,I}V.T) L1 L2 →
+ llpx_sn R (⫯d) T (L1.ⓑ{I}V) (L2.ⓑ{I}V).
+#R #a #I #L1 #L2 #V #T #d #H elim (llpx_sn_inv_bind … H) -H //
+qed-.
+
+lemma llpx_sn_fwd_flat_sn: ∀R,I,L1,L2,V,T,d. llpx_sn R d (ⓕ{I}V.T) L1 L2 →
+ llpx_sn R d V L1 L2.
+#R #I #L1 #L2 #V #T #d #H elim (llpx_sn_inv_flat … H) -H //
+qed-.
+
+lemma llpx_sn_fwd_flat_dx: ∀R,I,L1,L2,V,T,d. llpx_sn R d (ⓕ{I}V.T) L1 L2 →
+ llpx_sn R d T L1 L2.
+#R #I #L1 #L2 #V #T #d #H elim (llpx_sn_inv_flat … H) -H //
+qed-.
+
+lemma llpx_sn_fwd_pair_sn: ∀R,I,L1,L2,V,T,d. llpx_sn R d (②{I}V.T) L1 L2 →
+ llpx_sn R d V L1 L2.
+#R * /2 width=4 by llpx_sn_fwd_flat_sn, llpx_sn_fwd_bind_sn/
+qed-.
+
+(* Basic_properties *********************************************************)
+
+lemma llpx_sn_refl: ∀R. (∀I,L. reflexive … (R I L)) → ∀T,L,d. llpx_sn R d T L L.
+#R #HR #T #L @(f2_ind … rfw … L T) -L -T
+#n #IH #L * * /3 width=1 by llpx_sn_sort, llpx_sn_gref, llpx_sn_bind, llpx_sn_flat/
+#i #Hn elim (lt_or_ge i (|L|)) /2 width=1 by llpx_sn_free/
+#HiL #d elim (ylt_split i d) /2 width=1 by llpx_sn_skip/
+elim (ldrop_O1_lt … HiL) -HiL destruct /4 width=9 by llpx_sn_lref, ldrop_fwd_rfw/
+qed-.
+
+lemma llpx_sn_Y: ∀R,T,L1,L2. |L1| = |L2| → llpx_sn R (∞) T L1 L2.
+#R #T #L1 @(f2_ind … rfw … L1 T) -L1 -T
+#n #IH #L1 * * /3 width=1 by llpx_sn_sort, llpx_sn_skip, llpx_sn_gref, llpx_sn_flat/
+#a #I #V1 #T1 #Hn #L2 #HL12
+@llpx_sn_bind /2 width=1/ (**) (* explicit constructor *)
+@IH -IH // normalize /2 width=1 by eq_f2/
+qed-.
+
+lemma llpx_sn_ge_up: ∀R,L1,L2,U,dt. llpx_sn R dt U L1 L2 → ∀T,d,e. ⇧[d, e] T ≡ U →
+ dt ≤ d + e → llpx_sn R d U L1 L2.
+#R #L1 #L2 #U #dt #H elim H -L1 -L2 -U -dt
+[ #L1 #L2 #dt #k #HL12 #X #d #e #H #_ >(lift_inv_sort2 … H) -H /2 width=1 by llpx_sn_sort/
+| #L1 #L2 #dt #i #HL12 #Hidt #X #d #e #H #Hdtde
+ elim (lift_inv_lref2 … H) -H * #Hid #H destruct /3 width=1 by llpx_sn_skip, ylt_inj/ -HL12
+ elim (ylt_yle_false … Hidt) -Hidt
+ @(yle_trans … Hdtde) /2 width=1 by yle_inj/ (**) (* full auto too slow 11s *)
+| #I #L1 #L2 #K1 #K2 #W1 #W2 #dt #i #Hdti #HLK1 #HLK2 #HW1 #HW12 #_ #X #d #e #H #_
+ elim (lift_inv_lref2 … H) -H * #Hid #H destruct
+ [ lapply (llpx_sn_fwd_length … HW1) -HW1 #HK12
+ lapply (ldrop_fwd_length … HLK1) lapply (ldrop_fwd_length … HLK2)
+ normalize in ⊢ (%→%→?); -I -W1 -W2 -dt /3 width=1 by llpx_sn_skip, ylt_inj/
+ | /4 width=9 by llpx_sn_lref, yle_inj, le_plus_b/
+ ]
+| /2 width=1 by llpx_sn_free/
+| #L1 #L2 #dt #p #HL12 #X #d #e #H #_ >(lift_inv_gref2 … H) -H /2 width=1 by llpx_sn_gref/
+| #a #I #L1 #L2 #W #U #dt #_ #_ #IHV #IHT #X #d #e #H #Hdtde destruct
+ elim (lift_inv_bind2 … H) -H #V #T #HVW >commutative_plus #HTU #H destruct
+ @(llpx_sn_bind) /2 width=4 by/ (**) (* full auto fails *)
+ @(IHT … HTU) /2 width=1 by yle_succ/
+| #I #L1 #L2 #W #U #dt #_ #_ #IHV #IHT #X #d #e #H #Hdtde destruct
+ elim (lift_inv_flat2 … H) -H #HVW #HTU #H destruct
+ /3 width=4 by llpx_sn_flat/
+]
+qed-.
+
+(**) (* the minor premise comes first *)
+lemma llpx_sn_ge: ∀R,L1,L2,T,d1,d2. d1 ≤ d2 →
+ llpx_sn R d1 T L1 L2 → llpx_sn R d2 T L1 L2.
+#R #L1 #L2 #T #d1 #d2 * -d1 -d2 (**) (* destructed yle *)
+/3 width=6 by llpx_sn_ge_up, llpx_sn_Y, llpx_sn_fwd_length, yle_inj/
+qed-.
+
+lemma llpx_sn_bind_O: ∀R,a,I,L1,L2,V,T. llpx_sn R 0 V L1 L2 →
+ llpx_sn R 0 T (L1.ⓑ{I}V) (L2.ⓑ{I}V) →
+ llpx_sn R 0 (ⓑ{a,I}V.T) L1 L2.
+/3 width=3 by llpx_sn_ge, llpx_sn_bind/ qed-.
+
+lemma llpx_sn_co: ∀R1,R2. (∀I,L,T1,T2. R1 I L T1 T2 → R2 I L T1 T2) →
+ ∀L1,L2,T,d. llpx_sn R1 d T L1 L2 → llpx_sn R2 d T L1 L2.
+#R1 #R2 #HR12 #L1 #L2 #T #d #H elim H -L1 -L2 -T -d
+/3 width=9 by llpx_sn_sort, llpx_sn_skip, llpx_sn_lref, llpx_sn_free, llpx_sn_gref, llpx_sn_bind, llpx_sn_flat/
+qed-.
--- /dev/null
+(**************************************************************************)
+(* ___ *)
+(* ||M|| *)
+(* ||A|| A project by Andrea Asperti *)
+(* ||T|| *)
+(* ||I|| Developers: *)
+(* ||T|| The HELM team. *)
+(* ||A|| http://helm.cs.unibo.it *)
+(* \ / *)
+(* \ / This file is distributed under the terms of the *)
+(* v GNU General Public License Version 2 *)
+(* *)
+(**************************************************************************)
+
+include "basic_2/substitution/cofrees_alt.ma".
+include "basic_2/substitution/llpx_sn_alt_rec.ma".
+
+(* LAZY SN POINTWISE EXTENSION OF A CONTEXT-SENSITIVE REALTION FOR TERMS ****)
+
+(* alternative definition of llpx_sn (not recursive) *)
+definition llpx_sn_alt: relation4 bind2 lenv term term → relation4 ynat term lenv lenv ≝
+ λR,d,T,L1,L2. |L1| = |L2| ∧
+ (∀I1,I2,K1,K2,V1,V2,i. d ≤ yinj i → (L1 ⊢ i ~ϵ 𝐅*[d]⦃T⦄ → ⊥) →
+ ⇩[i] L1 ≡ K1.ⓑ{I1}V1 → ⇩[i] L2 ≡ K2.ⓑ{I2}V2 →
+ I1 = I2 ∧ R I1 K1 V1 V2
+ ).
+
+(* Main properties **********************************************************)
+
+theorem llpx_sn_llpx_sn_alt: ∀R,T,L1,L2,d. llpx_sn R d T L1 L2 → llpx_sn_alt R d T L1 L2.
+#R #U #L1 @(f2_ind … rfw … L1 U) -L1 -U
+#n #IHn #L1 #U #Hn #L2 #d #H elim (llpx_sn_inv_alt_r … H) -H
+#HL12 #IHU @conj //
+#I1 #I2 #K1 #K2 #V1 #V2 #i #Hdi #H #HLK1 #HLK2 elim (frees_inv_ge … H) -H //
+[ -n #HnU elim (IHU … HnU HLK1 HLK2) -IHU -HnU -HLK1 -HLK2 /2 width=1 by conj/
+| * #J1 #K10 #W10 #j #Hdj #Hji #HLK10 #HnW10 #HnU destruct
+ lapply (ldrop_fwd_drop2 … HLK10) #H
+ lapply (ldrop_conf_ge … H … HLK1 ?) -H /2 width=1 by lt_to_le/ <minus_plus #HK10
+ elim (ldrop_O1_lt (Ⓕ) L2 j) [2: <HL12 /2 width=5 by ldrop_fwd_length_lt2/ ] #J2 #K20 #W20 #HLK20
+ lapply (ldrop_fwd_drop2 … HLK20) #H
+ lapply (ldrop_conf_ge … H … HLK2 ?) -H /2 width=1 by lt_to_le/ <minus_plus #HK20
+ elim (IHn K10 W10 … K20 0) -IHn -HL12 /3 width=6 by ldrop_fwd_rfw/
+ elim (IHU … HnU HLK10 HLK20) -IHU -HnU -HLK10 -HLK20 //
+]
+qed.
+
+theorem llpx_sn_alt_inv_llpx_sn: ∀R,T,L1,L2,d. llpx_sn_alt R d T L1 L2 → llpx_sn R d T L1 L2.
+#R #U #L1 @(f2_ind … rfw … L1 U) -L1 -U
+#n #IHn #L1 #U #Hn #L2 #d * #HL12 #IHU @llpx_sn_intro_alt_r //
+#I1 #I2 #K1 #K2 #V1 #V2 #i #Hdi #HnU #HLK1 #HLK2 destruct
+elim (IHU … HLK1 HLK2) /3 width=6 by nlift_frees/
+#H #HV12 @and3_intro // @IHn -IHn /3 width=6 by ldrop_fwd_rfw/
+lapply (ldrop_fwd_drop2 … HLK1) #H1
+lapply (ldrop_fwd_drop2 … HLK2) -HLK2 #H2
+@conj [ @(ldrop_fwd_length_eq1 … H1 H2) // ] -HL12
+#Z1 #Z2 #Y1 #Y2 #X1 #X2 #j #_
+>(minus_plus_m_m j (i+1)) in ⊢ (%→?); >commutative_plus <minus_plus
+#HnV1 #HKY1 #HKY2 (**) (* full auto too slow *)
+lapply (ldrop_trans_ge … H1 … HKY1 ?) -H1 -HKY1 // #HLY1
+lapply (ldrop_trans_ge … H2 … HKY2 ?) -H2 -HKY2 // #HLY2
+/4 width=14 by frees_be, yle_plus_dx2_trans, yle_succ_dx/
+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/lift_neg.ma".
+include "basic_2/relocation/ldrop_ldrop.ma".
+include "basic_2/substitution/llpx_sn.ma".
+
+(* LAZY SN POINTWISE EXTENSION OF A CONTEXT-SENSITIVE REALTION FOR TERMS ****)
+
+(* alternative definition of llpx_sn (recursive) *)
+inductive llpx_sn_alt_r (R:relation4 bind2 lenv term term): relation4 ynat term lenv lenv ≝
+| llpx_sn_alt_r_intro: ∀L1,L2,T,d.
+ (∀I1,I2,K1,K2,V1,V2,i. d ≤ yinj i → (∀U. ⇧[i, 1] U ≡ T → ⊥) →
+ ⇩[i] L1 ≡ K1.ⓑ{I1}V1 → ⇩[i] L2 ≡ K2.ⓑ{I2}V2 → I1 = I2 ∧ R I1 K1 V1 V2
+ ) →
+ (∀I1,I2,K1,K2,V1,V2,i. d ≤ yinj i → (∀U. ⇧[i, 1] U ≡ T → ⊥) →
+ ⇩[i] L1 ≡ K1.ⓑ{I1}V1 → ⇩[i] L2 ≡ K2.ⓑ{I2}V2 → llpx_sn_alt_r R 0 V1 K1 K2
+ ) → |L1| = |L2| → llpx_sn_alt_r R d T L1 L2
+.
+
+(* Compact definition of llpx_sn_alt_r **************************************)
+
+lemma llpx_sn_alt_r_intro_alt: ∀R,L1,L2,T,d. |L1| = |L2| →
+ (∀I1,I2,K1,K2,V1,V2,i. d ≤ yinj i → (∀U. ⇧[i, 1] U ≡ T → ⊥) →
+ ⇩[i] L1 ≡ K1.ⓑ{I1}V1 → ⇩[i] L2 ≡ K2.ⓑ{I2}V2 →
+ ∧∧ I1 = I2 & R I1 K1 V1 V2 & llpx_sn_alt_r R 0 V1 K1 K2
+ ) → llpx_sn_alt_r R d T L1 L2.
+#R #L1 #L2 #T #d #HL12 #IH @llpx_sn_alt_r_intro // -HL12
+#I1 #I2 #K1 #K2 #V1 #V2 #i #Hid #HnT #HLK1 #HLK2
+elim (IH … HnT HLK1 HLK2) -IH -HnT -HLK1 -HLK2 /2 width=1 by conj/
+qed.
+
+lemma llpx_sn_alt_r_ind_alt: ∀R. ∀S:relation4 ynat term lenv lenv.
+ (∀L1,L2,T,d. |L1| = |L2| → (
+ ∀I1,I2,K1,K2,V1,V2,i. d ≤ yinj i → (∀U. ⇧[i, 1] U ≡ T → ⊥) →
+ ⇩[i] L1 ≡ K1.ⓑ{I1}V1 → ⇩[i] L2 ≡ K2.ⓑ{I2}V2 →
+ ∧∧ I1 = I2 & R I1 K1 V1 V2 & llpx_sn_alt_r R 0 V1 K1 K2 & S 0 V1 K1 K2
+ ) → S d T L1 L2) →
+ ∀L1,L2,T,d. llpx_sn_alt_r R d T L1 L2 → S d T L1 L2.
+#R #S #IH #L1 #L2 #T #d #H elim H -L1 -L2 -T -d
+#L1 #L2 #T #d #H1 #H2 #HL12 #IH2 @IH -IH // -HL12
+#I1 #I2 #K1 #K2 #V1 #V2 #i #Hid #HnT #HLK1 #HLK2
+elim (H1 … HnT HLK1 HLK2) -H1 /4 width=8 by and4_intro/
+qed-.
+
+lemma llpx_sn_alt_r_inv_alt: ∀R,L1,L2,T,d. llpx_sn_alt_r R d T L1 L2 →
+ |L1| = |L2| ∧
+ ∀I1,I2,K1,K2,V1,V2,i. d ≤ yinj i → (∀U. ⇧[i, 1] U ≡ T → ⊥) →
+ ⇩[i] L1 ≡ K1.ⓑ{I1}V1 → ⇩[i] L2 ≡ K2.ⓑ{I2}V2 →
+ ∧∧ I1 = I2 & R I1 K1 V1 V2 & llpx_sn_alt_r R 0 V1 K1 K2.
+#R #L1 #L2 #T #d #H @(llpx_sn_alt_r_ind_alt … H) -L1 -L2 -T -d
+#L1 #L2 #T #d #HL12 #IH @conj // -HL12
+#I1 #I2 #K1 #K2 #V1 #V2 #i #Hid #HnT #HLK1 #HLK2
+elim (IH … HnT HLK1 HLK2) -IH -HnT -HLK1 -HLK2 /2 width=1 by and3_intro/
+qed-.
+
+(* Basic inversion lemmas ***************************************************)
+
+lemma llpx_sn_alt_r_inv_flat: ∀R,I,L1,L2,V,T,d. llpx_sn_alt_r R d (ⓕ{I}V.T) L1 L2 →
+ llpx_sn_alt_r R d V L1 L2 ∧ llpx_sn_alt_r R d T L1 L2.
+#R #I #L1 #L2 #V #T #d #H elim (llpx_sn_alt_r_inv_alt … H) -H
+#HL12 #IH @conj @llpx_sn_alt_r_intro_alt // -HL12
+#I1 #I2 #K1 #K2 #V1 #V2 #i #Hdi #H #HLK1 #HLK2
+elim (IH … HLK1 HLK2) -IH -HLK1 -HLK2 //
+/3 width=8 by nlift_flat_sn, nlift_flat_dx, and3_intro/
+qed-.
+
+lemma llpx_sn_alt_r_inv_bind: ∀R,a,I,L1,L2,V,T,d. llpx_sn_alt_r R d (ⓑ{a,I}V.T) L1 L2 →
+ llpx_sn_alt_r R d V L1 L2 ∧ llpx_sn_alt_r R (⫯d) T (L1.ⓑ{I}V) (L2.ⓑ{I}V).
+#R #a #I #L1 #L2 #V #T #d #H elim (llpx_sn_alt_r_inv_alt … H) -H
+#HL12 #IH @conj @llpx_sn_alt_r_intro_alt [1,3: normalize // ] -HL12
+#I1 #I2 #K1 #K2 #V1 #V2 #i #Hdi #H #HLK1 #HLK2
+[ elim (IH … HLK1 HLK2) -IH -HLK1 -HLK2
+ /3 width=9 by nlift_bind_sn, and3_intro/
+| lapply (yle_inv_succ1 … Hdi) -Hdi * #Hdi #Hi
+ lapply (ldrop_inv_drop1_lt … HLK1 ?) -HLK1 /2 width=1 by ylt_O/ #HLK1
+ lapply (ldrop_inv_drop1_lt … HLK2 ?) -HLK2 /2 width=1 by ylt_O/ #HLK2
+ elim (IH … HLK1 HLK2) -IH -HLK1 -HLK2 /2 width=1 by and3_intro/
+ @nlift_bind_dx <plus_minus_m_m /2 width=2 by ylt_O/
+]
+qed-.
+
+(* Basic forward lemmas *****************************************************)
+
+lemma llpx_sn_alt_r_fwd_length: ∀R,L1,L2,T,d. llpx_sn_alt_r R d T L1 L2 → |L1| = |L2|.
+#R #L1 #L2 #T #d #H elim (llpx_sn_alt_r_inv_alt … H) -H //
+qed-.
+
+lemma llpx_sn_alt_r_fwd_lref: ∀R,L1,L2,d,i. llpx_sn_alt_r R d (#i) L1 L2 →
+ ∨∨ |L1| ≤ i ∧ |L2| ≤ i
+ | yinj i < d
+ | ∃∃I,K1,K2,V1,V2. ⇩[i] L1 ≡ K1.ⓑ{I}V1 &
+ ⇩[i] L2 ≡ K2.ⓑ{I}V2 &
+ llpx_sn_alt_r R (yinj 0) V1 K1 K2 &
+ R I K1 V1 V2 & d ≤ yinj i.
+#R #L1 #L2 #d #i #H elim (llpx_sn_alt_r_inv_alt … H) -H
+#HL12 #IH elim (lt_or_ge i (|L1|)) /3 width=1 by or3_intro0, conj/
+elim (ylt_split i d) /3 width=1 by or3_intro1/
+#Hdi #HL1 elim (ldrop_O1_lt (Ⓕ) … HL1)
+#I1 #K1 #V1 #HLK1 elim (ldrop_O1_lt (Ⓕ) L2 i) //
+#I2 #K2 #V2 #HLK2 elim (IH … HLK1 HLK2) -IH
+/3 width=9 by nlift_lref_be_SO, or3_intro2, ex5_5_intro/
+qed-.
+
+(* Basic properties *********************************************************)
+
+lemma llpx_sn_alt_r_sort: ∀R,L1,L2,d,k. |L1| = |L2| → llpx_sn_alt_r R d (⋆k) L1 L2.
+#R #L1 #L2 #d #k #HL12 @llpx_sn_alt_r_intro_alt // -HL12
+#I1 #I2 #K1 #K2 #V1 #V2 #i #_ #H elim (H (⋆k)) //
+qed.
+
+lemma llpx_sn_alt_r_gref: ∀R,L1,L2,d,p. |L1| = |L2| → llpx_sn_alt_r R d (§p) L1 L2.
+#R #L1 #L2 #d #p #HL12 @llpx_sn_alt_r_intro_alt // -HL12
+#I1 #I2 #K1 #K2 #V1 #V2 #i #_ #H elim (H (§p)) //
+qed.
+
+lemma llpx_sn_alt_r_skip: ∀R,L1,L2,d,i. |L1| = |L2| → yinj i < d → llpx_sn_alt_r R d (#i) L1 L2.
+#R #L1 #L2 #d #i #HL12 #Hid @llpx_sn_alt_r_intro_alt // -HL12
+#I1 #I2 #K1 #K2 #V1 #V2 #j #Hdj #H elim (H (#i)) -H
+/4 width=3 by lift_lref_lt, ylt_yle_trans, ylt_inv_inj/
+qed.
+
+lemma llpx_sn_alt_r_free: ∀R,L1,L2,d,i. |L1| ≤ i → |L2| ≤ i → |L1| = |L2| →
+ llpx_sn_alt_r R d (#i) L1 L2.
+#R #L1 #L2 #d #i #HL1 #_ #HL12 @llpx_sn_alt_r_intro_alt // -HL12
+#I1 #I2 #K1 #K2 #V1 #V2 #j #_ #H #HLK1 elim (H (#(i-1))) -H
+lapply (ldrop_fwd_length_lt2 … HLK1) -HLK1
+/3 width=3 by lift_lref_ge_minus, lt_to_le_to_lt/
+qed.
+
+lemma llpx_sn_alt_r_lref: ∀R,I,L1,L2,K1,K2,V1,V2,d,i. d ≤ yinj i →
+ ⇩[i] L1 ≡ K1.ⓑ{I}V1 → ⇩[i] L2 ≡ K2.ⓑ{I}V2 →
+ llpx_sn_alt_r R 0 V1 K1 K2 → R I K1 V1 V2 →
+ llpx_sn_alt_r R d (#i) L1 L2.
+#R #I #L1 #L2 #K1 #K2 #V1 #V2 #d #i #Hdi #HLK1 #HLK2 #HK12 #HV12 @llpx_sn_alt_r_intro_alt
+[ lapply (llpx_sn_alt_r_fwd_length … HK12) -HK12 #HK12
+ @(ldrop_fwd_length_eq2 … HLK1 HLK2) normalize //
+| #Z1 #Z2 #Y1 #Y2 #X1 #X2 #j #Hdj #H #HLY1 #HLY2
+ elim (lt_or_eq_or_gt i j) #Hij destruct
+ [ elim (H (#i)) -H /2 width=1 by lift_lref_lt/
+ | lapply (ldrop_mono … HLY1 … HLK1) -HLY1 -HLK1 #H destruct
+ lapply (ldrop_mono … HLY2 … HLK2) -HLY2 -HLK2 #H destruct /2 width=1 by and3_intro/
+ | elim (H (#(i-1))) -H /2 width=1 by lift_lref_ge_minus/
+ ]
+]
+qed.
+
+lemma llpx_sn_alt_r_flat: ∀R,I,L1,L2,V,T,d.
+ llpx_sn_alt_r R d V L1 L2 → llpx_sn_alt_r R d T L1 L2 →
+ llpx_sn_alt_r R d (ⓕ{I}V.T) L1 L2.
+#R #I #L1 #L2 #V #T #d #HV #HT
+elim (llpx_sn_alt_r_inv_alt … HV) -HV #HL12 #IHV
+elim (llpx_sn_alt_r_inv_alt … HT) -HT #_ #IHT
+@llpx_sn_alt_r_intro_alt // -HL12
+#I1 #I2 #K1 #K2 #V1 #V2 #i #Hdi #HnVT #HLK1 #HLK2
+elim (nlift_inv_flat … HnVT) -HnVT #H
+[ elim (IHV … HLK1 … HLK2) -IHV /2 width=2 by and3_intro/
+| elim (IHT … HLK1 … HLK2) -IHT /3 width=2 by and3_intro/
+]
+qed.
+
+lemma llpx_sn_alt_r_bind: ∀R,a,I,L1,L2,V,T,d.
+ llpx_sn_alt_r R d V L1 L2 →
+ llpx_sn_alt_r R (⫯d) T (L1.ⓑ{I}V) (L2.ⓑ{I}V) →
+ llpx_sn_alt_r R d (ⓑ{a,I}V.T) L1 L2.
+#R #a #I #L1 #L2 #V #T #d #HV #HT
+elim (llpx_sn_alt_r_inv_alt … HV) -HV #HL12 #IHV
+elim (llpx_sn_alt_r_inv_alt … HT) -HT #_ #IHT
+@llpx_sn_alt_r_intro_alt // -HL12
+#I1 #I2 #K1 #K2 #V1 #V2 #i #Hdi #HnVT #HLK1 #HLK2
+elim (nlift_inv_bind … HnVT) -HnVT #H
+[ elim (IHV … HLK1 … HLK2) -IHV /2 width=2 by and3_intro/
+| elim IHT -IHT /2 width=12 by ldrop_drop, yle_succ, and3_intro/
+]
+qed.
+
+(* Main properties **********************************************************)
+
+theorem llpx_sn_lpx_sn_alt_r: ∀R,L1,L2,T,d. llpx_sn R d T L1 L2 → llpx_sn_alt_r R d T L1 L2.
+#R #L1 #L2 #T #d #H elim H -L1 -L2 -T -d
+/2 width=9 by llpx_sn_alt_r_sort, llpx_sn_alt_r_gref, llpx_sn_alt_r_skip, llpx_sn_alt_r_free, llpx_sn_alt_r_lref, llpx_sn_alt_r_flat, llpx_sn_alt_r_bind/
+qed.
+
+(* Main inversion lemmas ****************************************************)
+
+theorem llpx_sn_alt_r_inv_lpx_sn: ∀R,T,L1,L2,d. llpx_sn_alt_r R d T L1 L2 → llpx_sn R d T L1 L2.
+#R #T #L1 @(f2_ind … rfw … L1 T) -L1 -T #n #IH #L1 * *
+[1,3: /3 width=4 by llpx_sn_alt_r_fwd_length, llpx_sn_gref, llpx_sn_sort/
+| #i #Hn #L2 #d #H lapply (llpx_sn_alt_r_fwd_length … H)
+ #HL12 elim (llpx_sn_alt_r_fwd_lref … H) -H
+ [ * /2 width=1 by llpx_sn_free/
+ | /2 width=1 by llpx_sn_skip/
+ | * /4 width=9 by llpx_sn_lref, ldrop_fwd_rfw/
+ ]
+| #a #I #V #T #Hn #L2 #d #H elim (llpx_sn_alt_r_inv_bind … H) -H
+ /3 width=1 by llpx_sn_bind/
+| #I #V #T #Hn #L2 #d #H elim (llpx_sn_alt_r_inv_flat … H) -H
+ /3 width=1 by llpx_sn_flat/
+]
+qed-.
+
+(* Alternative definition of llpx_sn (recursive) ****************************)
+
+lemma llpx_sn_intro_alt_r: ∀R,L1,L2,T,d. |L1| = |L2| →
+ (∀I1,I2,K1,K2,V1,V2,i. d ≤ yinj i → (∀U. ⇧[i, 1] U ≡ T → ⊥) →
+ ⇩[i] L1 ≡ K1.ⓑ{I1}V1 → ⇩[i] L2 ≡ K2.ⓑ{I2}V2 →
+ ∧∧ I1 = I2 & R I1 K1 V1 V2 & llpx_sn R 0 V1 K1 K2
+ ) → llpx_sn R d T L1 L2.
+#R #L1 #L2 #T #d #HL12 #IH @llpx_sn_alt_r_inv_lpx_sn
+@llpx_sn_alt_r_intro_alt // -HL12
+#I1 #I2 #K1 #K2 #V1 #V2 #i #Hid #HnT #HLK1 #HLK2
+elim (IH … HnT HLK1 HLK2) -IH -HnT -HLK1 -HLK2 /3 width=1 by llpx_sn_lpx_sn_alt_r, and3_intro/
+qed.
+
+lemma llpx_sn_ind_alt_r: ∀R. ∀S:relation4 ynat term lenv lenv.
+ (∀L1,L2,T,d. |L1| = |L2| → (
+ ∀I1,I2,K1,K2,V1,V2,i. d ≤ yinj i → (∀U. ⇧[i, 1] U ≡ T → ⊥) →
+ ⇩[i] L1 ≡ K1.ⓑ{I1}V1 → ⇩[i] L2 ≡ K2.ⓑ{I2}V2 →
+ ∧∧ I1 = I2 & R I1 K1 V1 V2 & llpx_sn R 0 V1 K1 K2 & S 0 V1 K1 K2
+ ) → S d T L1 L2) →
+ ∀L1,L2,T,d. llpx_sn R d T L1 L2 → S d T L1 L2.
+#R #S #IH1 #L1 #L2 #T #d #H lapply (llpx_sn_lpx_sn_alt_r … H) -H
+#H @(llpx_sn_alt_r_ind_alt … H) -L1 -L2 -T -d
+#L1 #L2 #T #d #HL12 #IH2 @IH1 -IH1 // -HL12
+#I1 #I2 #K1 #K2 #V1 #V2 #i #Hid #HnT #HLK1 #HLK2
+elim (IH2 … HnT HLK1 HLK2) -IH2 -HnT -HLK1 -HLK2 /3 width=1 by llpx_sn_alt_r_inv_lpx_sn, and4_intro/
+qed-.
+
+lemma llpx_sn_inv_alt_r: ∀R,L1,L2,T,d. llpx_sn R d T L1 L2 →
+ |L1| = |L2| ∧
+ ∀I1,I2,K1,K2,V1,V2,i. d ≤ yinj i → (∀U. ⇧[i, 1] U ≡ T → ⊥) →
+ ⇩[i] L1 ≡ K1.ⓑ{I1}V1 → ⇩[i] L2 ≡ K2.ⓑ{I2}V2 →
+ ∧∧ I1 = I2 & R I1 K1 V1 V2 & llpx_sn R 0 V1 K1 K2.
+#R #L1 #L2 #T #d #H lapply (llpx_sn_lpx_sn_alt_r … H) -H
+#H elim (llpx_sn_alt_r_inv_alt … H) -H
+#HL12 #IH @conj //
+#I1 #I2 #K1 #K2 #V1 #V2 #i #Hid #HnT #HLK1 #HLK2
+elim (IH … HnT HLK1 HLK2) -IH -HnT -HLK1 -HLK2 /3 width=1 by llpx_sn_alt_r_inv_lpx_sn, and3_intro/
+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/ldrop_ldrop.ma".
+include "basic_2/substitution/llpx_sn_leq.ma".
+
+(* LAZY SN POINTWISE EXTENSION OF A CONTEXT-SENSITIVE REALTION FOR TERMS ****)
+
+(* Advanced forward lemmas **************************************************)
+
+lemma llpx_sn_fwd_lref_dx: ∀R,L1,L2,d,i. llpx_sn R d (#i) L1 L2 →
+ ∀I,K2,V2. ⇩[i] L2 ≡ K2.ⓑ{I}V2 →
+ i < d ∨
+ ∃∃K1,V1. ⇩[i] L1 ≡ K1.ⓑ{I}V1 & llpx_sn R 0 V1 K1 K2 &
+ R I K1 V1 V2 & d ≤ i.
+#R #L1 #L2 #d #i #H #I #K2 #V2 #HLK2 elim (llpx_sn_fwd_lref … H) -H [ * || * ]
+[ #_ #H elim (lt_refl_false i)
+ lapply (ldrop_fwd_length_lt2 … HLK2) -HLK2
+ /2 width=3 by lt_to_le_to_lt/ (**) (* full auto too slow *)
+| /2 width=1 by or_introl/
+| #I #K11 #K22 #V11 #V22 #HLK11 #HLK22 #HK12 #HV12 #Hdi
+ lapply (ldrop_mono … HLK22 … HLK2) -L2 #H destruct
+ /3 width=5 by ex4_2_intro, or_intror/
+]
+qed-.
+
+lemma llpx_sn_fwd_lref_sn: ∀R,L1,L2,d,i. llpx_sn R d (#i) L1 L2 →
+ ∀I,K1,V1. ⇩[i] L1 ≡ K1.ⓑ{I}V1 →
+ i < d ∨
+ ∃∃K2,V2. ⇩[i] L2 ≡ K2.ⓑ{I}V2 & llpx_sn R 0 V1 K1 K2 &
+ R I K1 V1 V2 & d ≤ i.
+#R #L1 #L2 #d #i #H #I #K1 #V1 #HLK1 elim (llpx_sn_fwd_lref … H) -H [ * || * ]
+[ #H #_ elim (lt_refl_false i)
+ lapply (ldrop_fwd_length_lt2 … HLK1) -HLK1
+ /2 width=3 by lt_to_le_to_lt/ (**) (* full auto too slow *)
+| /2 width=1 by or_introl/
+| #I #K11 #K22 #V11 #V22 #HLK11 #HLK22 #HK12 #HV12 #Hdi
+ lapply (ldrop_mono … HLK11 … HLK1) -L1 #H destruct
+ /3 width=5 by ex4_2_intro, or_intror/
+]
+qed-.
+
+(* Advanced inversion lemmas ************************************************)
+
+lemma llpx_sn_inv_lref_ge_dx: ∀R,L1,L2,d,i. llpx_sn R d (#i) L1 L2 → d ≤ i →
+ ∀I,K2,V2. ⇩[i] L2 ≡ K2.ⓑ{I}V2 →
+ ∃∃K1,V1. ⇩[i] L1 ≡ K1.ⓑ{I}V1 &
+ llpx_sn R 0 V1 K1 K2 & R I K1 V1 V2.
+#R #L1 #L2 #d #i #H #Hdi #I #K2 #V2 #HLK2 elim (llpx_sn_fwd_lref_dx … H … HLK2) -L2
+[ #H elim (ylt_yle_false … H Hdi)
+| * /2 width=5 by ex3_2_intro/
+]
+qed-.
+
+lemma llpx_sn_inv_lref_ge_sn: ∀R,L1,L2,d,i. llpx_sn R d (#i) L1 L2 → d ≤ i →
+ ∀I,K1,V1. ⇩[i] L1 ≡ K1.ⓑ{I}V1 →
+ ∃∃K2,V2. ⇩[i] L2 ≡ K2.ⓑ{I}V2 &
+ llpx_sn R 0 V1 K1 K2 & R I K1 V1 V2.
+#R #L1 #L2 #d #i #H #Hdi #I #K1 #V1 #HLK1 elim (llpx_sn_fwd_lref_sn … H … HLK1) -L1
+[ #H elim (ylt_yle_false … H Hdi)
+| * /2 width=5 by ex3_2_intro/
+]
+qed-.
+
+lemma llpx_sn_inv_lref_ge_bi: ∀R,L1,L2,d,i. llpx_sn R d (#i) L1 L2 → d ≤ i →
+ ∀I1,I2,K1,K2,V1,V2.
+ ⇩[i] L1 ≡ K1.ⓑ{I1}V1 → ⇩[i] L2 ≡ K2.ⓑ{I2}V2 →
+ ∧∧ I1 = I2 & llpx_sn R 0 V1 K1 K2 & R I1 K1 V1 V2.
+#R #L1 #L2 #d #i #HL12 #Hdi #I1 #I2 #K1 #K2 #V1 #V2 #HLK1 #HLK2
+elim (llpx_sn_inv_lref_ge_sn … HL12 … HLK1) // -L1 -d
+#J #Y #HY lapply (ldrop_mono … HY … HLK2) -L2 -i #H destruct /2 width=1 by and3_intro/
+qed-.
+
+fact llpx_sn_inv_S_aux: ∀R,L1,L2,T,d0. llpx_sn R d0 T L1 L2 → ∀d. d0 = d + 1 →
+ ∀K1,K2,I,V1,V2. ⇩[d] L1 ≡ K1.ⓑ{I}V1 → ⇩[d] L2 ≡ K2.ⓑ{I}V2 →
+ llpx_sn R 0 V1 K1 K2 → R I K1 V1 V2 → llpx_sn R d T L1 L2.
+#R #L1 #L2 #T #d0 #H elim H -L1 -L2 -T -d0
+/2 width=1 by llpx_sn_gref, llpx_sn_free, llpx_sn_sort/
+[ #L1 #L2 #d0 #i #HL12 #Hid #d #H #K1 #K2 #I #V1 #V2 #HLK1 #HLK2 #HK12 #HV12 destruct
+ elim (yle_split_eq i d) /2 width=1 by llpx_sn_skip, ylt_fwd_succ2/ -HL12 -Hid
+ #H destruct /2 width=9 by llpx_sn_lref/
+| #I #L1 #L2 #K11 #K22 #V1 #V2 #d0 #i #Hd0i #HLK11 #HLK22 #HK12 #HV12 #_ #d #H #K1 #K2 #J #W1 #W2 #_ #_ #_ #_ destruct
+ /3 width=9 by llpx_sn_lref, yle_pred_sn/
+| #a #I #L1 #L2 #V #T #d0 #_ #_ #IHV #IHT #d #H #K1 #K2 #J #W1 #W2 #HLK1 #HLK2 #HK12 #HW12 destruct
+ /4 width=9 by llpx_sn_bind, ldrop_drop/
+| #I #L1 #L2 #V #T #d0 #_ #_ #IHV #IHT #d #H #K1 #K2 #J #W1 #W2 #HLK1 #HLK2 #HK12 #HW12 destruct
+ /3 width=9 by llpx_sn_flat/
+]
+qed-.
+
+lemma llpx_sn_inv_S: ∀R,L1,L2,T,d. llpx_sn R (d + 1) T L1 L2 →
+ ∀K1,K2,I,V1,V2. ⇩[d] L1 ≡ K1.ⓑ{I}V1 → ⇩[d] L2 ≡ K2.ⓑ{I}V2 →
+ llpx_sn R 0 V1 K1 K2 → R I K1 V1 V2 → llpx_sn R d T L1 L2.
+/2 width=9 by llpx_sn_inv_S_aux/ qed-.
+
+lemma llpx_sn_inv_bind_O: ∀R. (∀I,L. reflexive … (R I L)) →
+ ∀a,I,L1,L2,V,T. llpx_sn R 0 (ⓑ{a,I}V.T) L1 L2 →
+ llpx_sn R 0 V L1 L2 ∧ llpx_sn R 0 T (L1.ⓑ{I}V) (L2.ⓑ{I}V).
+#R #HR #a #I #L1 #L2 #V #T #H elim (llpx_sn_inv_bind … H) -H
+/3 width=9 by ldrop_pair, conj, llpx_sn_inv_S/
+qed-.
+
+(* More advanced forward lemmas *********************************************)
+
+lemma llpx_sn_fwd_bind_O_dx: ∀R. (∀I,L. reflexive … (R I L)) →
+ ∀a,I,L1,L2,V,T. llpx_sn R 0 (ⓑ{a,I}V.T) L1 L2 →
+ llpx_sn R 0 T (L1.ⓑ{I}V) (L2.ⓑ{I}V).
+#R #HR #a #I #L1 #L2 #V #T #H elim (llpx_sn_inv_bind_O … H) -H //
+qed-.
+
+(* Advanced properties ******************************************************)
+
+lemma llpx_sn_bind_repl_O: ∀R,I,L1,L2,V1,V2,T. llpx_sn R 0 T (L1.ⓑ{I}V1) (L2.ⓑ{I}V2) →
+ ∀J,W1,W2. llpx_sn R 0 W1 L1 L2 → R J L1 W1 W2 → llpx_sn R 0 T (L1.ⓑ{J}W1) (L2.ⓑ{J}W2).
+/3 width=9 by llpx_sn_bind_repl_SO, llpx_sn_inv_S/ qed-.
+
+lemma llpx_sn_dec: ∀R. (∀I,L,T1,T2. Decidable (R I L T1 T2)) →
+ ∀T,L1,L2,d. Decidable (llpx_sn R d T L1 L2).
+#R #HR #T #L1 @(f2_ind … rfw … L1 T) -L1 -T
+#n #IH #L1 * *
+[ #k #Hn #L2 elim (eq_nat_dec (|L1|) (|L2|)) /3 width=1 by or_introl, llpx_sn_sort/
+| #i #Hn #L2 elim (eq_nat_dec (|L1|) (|L2|))
+ [ #HL12 #d elim (ylt_split i d) /3 width=1 by llpx_sn_skip, or_introl/
+ #Hdi elim (lt_or_ge i (|L1|)) #HiL1
+ elim (lt_or_ge i (|L2|)) #HiL2 /3 width=1 by or_introl, llpx_sn_free/
+ elim (ldrop_O1_lt (Ⓕ) … HiL2) #I2 #K2 #V2 #HLK2
+ elim (ldrop_O1_lt (Ⓕ) … HiL1) #I1 #K1 #V1 #HLK1
+ elim (eq_bind2_dec I2 I1)
+ [ #H2 elim (HR I1 K1 V1 V2) -HR
+ [ #H3 elim (IH K1 V1 … K2 0) destruct
+ /3 width=9 by llpx_sn_lref, ldrop_fwd_rfw, or_introl/
+ ]
+ ]
+ -IH #H3 @or_intror
+ #H elim (llpx_sn_fwd_lref … H) -H [1,3,4,6,7,9: * ]
+ [1,3,5: /3 width=4 by lt_to_le_to_lt, lt_refl_false/
+ |7,8,9: /2 width=4 by ylt_yle_false/
+ ]
+ #Z #Y1 #Y2 #X1 #X2 #HLY1 #HLY2 #HY12 #HX12
+ lapply (ldrop_mono … HLY1 … HLK1) -HLY1 -HLK1
+ lapply (ldrop_mono … HLY2 … HLK2) -HLY2 -HLK2
+ #H #H0 destruct /2 width=1 by/
+ ]
+| #p #Hn #L2 elim (eq_nat_dec (|L1|) (|L2|)) /3 width=1 by or_introl, llpx_sn_gref/
+| #a #I #V #T #Hn #L2 #d destruct
+ elim (IH L1 V … L2 d) /2 width=1 by/
+ elim (IH (L1.ⓑ{I}V) T … (L2.ⓑ{I}V) (⫯d)) -IH /3 width=1 by or_introl, llpx_sn_bind/
+ #H1 #H2 @or_intror
+ #H elim (llpx_sn_inv_bind … H) -H /2 width=1 by/
+| #I #V #T #Hn #L2 #d destruct
+ elim (IH L1 V … L2 d) /2 width=1 by/
+ elim (IH L1 T … L2 d) -IH /3 width=1 by or_introl, llpx_sn_flat/
+ #H1 #H2 @or_intror
+ #H elim (llpx_sn_inv_flat … H) -H /2 width=1 by/
+]
+-n /4 width=4 by llpx_sn_fwd_length, or_intror/
+qed-.
+
+(* Properties on relocation *************************************************)
+
+lemma llpx_sn_lift_le: ∀R. (∀I. l_liftable (R I)) →
+ ∀K1,K2,T,d0. llpx_sn R d0 T K1 K2 →
+ ∀L1,L2,d,e. ⇩[Ⓕ, d, e] L1 ≡ K1 → ⇩[Ⓕ, d, e] L2 ≡ K2 →
+ ∀U. ⇧[d, e] T ≡ U → d0 ≤ d → llpx_sn R d0 U L1 L2.
+#R #HR #K1 #K2 #T #d0 #H elim H -K1 -K2 -T -d0
+[ #K1 #K2 #d0 #k #HK12 #L1 #L2 #d #e #HLK1 #HLK2 #X #H #_ >(lift_inv_sort1 … H) -X
+ lapply (ldrop_fwd_length_eq2 … HLK1 HLK2 HK12) -K1 -K2 -d
+ /2 width=1 by llpx_sn_sort/
+| #K1 #K2 #d0 #i #HK12 #Hid0 #L1 #L2 #d #e #HLK1 #HLK2 #X #H #Hd0 elim (lift_inv_lref1 … H) -H
+ * #Hdi #H destruct
+ [ lapply (ldrop_fwd_length_eq2 … HLK1 HLK2 HK12) -K1 -K2 -d
+ /2 width=1 by llpx_sn_skip/
+ | elim (ylt_yle_false … Hid0) -L1 -L2 -K1 -K2 -e -Hid0
+ /3 width=3 by yle_trans, yle_inj/
+ ]
+| #I #K1 #K2 #K11 #K22 #V1 #V2 #d0 #i #Hid0 #HK11 #HK22 #HK12 #HV12 #IHK12 #L1 #L2 #d #e #HLK1 #HLK2 #X #H #Hd0 elim (lift_inv_lref1 … H) -H
+ * #Hdi #H destruct [ -HK12 | -IHK12 ]
+ [ elim (ldrop_trans_lt … HLK1 … HK11) // -K1
+ elim (ldrop_trans_lt … HLK2 … HK22) // -Hdi -K2
+ /3 width=18 by llpx_sn_lref/
+ | lapply (ldrop_trans_ge_comm … HLK1 … HK11 ?) // -K1
+ lapply (ldrop_trans_ge_comm … HLK2 … HK22 ?) // -Hdi -Hd0 -K2
+ /3 width=9 by llpx_sn_lref, yle_plus_dx1_trans/
+ ]
+| #K1 #K2 #d0 #i #HK1 #HK2 #HK12 #L1 #L2 #d #e #HLK1 #HLK2 #X #H #Hd0 elim (lift_inv_lref1 … H) -H
+ * #Hid #H destruct
+ lapply (ldrop_fwd_length_eq2 … HLK1 HLK2 HK12) -HK12
+ [ /3 width=7 by llpx_sn_free, ldrop_fwd_be/
+ | lapply (ldrop_fwd_length … HLK1) -HLK1 #HLK1
+ lapply (ldrop_fwd_length … HLK2) -HLK2 #HLK2
+ @llpx_sn_free [ >HLK1 | >HLK2 ] -Hid -HLK1 -HLK2 /2 width=1 by monotonic_le_plus_r/ (**) (* explicit constructor *)
+ ]
+| #K1 #K2 #d0 #p #HK12 #L1 #L2 #d #e #HLK1 #HLK2 #X #H #_ >(lift_inv_gref1 … H) -X
+ lapply (ldrop_fwd_length_eq2 … HLK1 HLK2 HK12) -K1 -K2 -d -e
+ /2 width=1 by llpx_sn_gref/
+| #a #I #K1 #K2 #V #T #d0 #_ #_ #IHV #IHT #L1 #L2 #d #e #HLK1 #HLK2 #X #H #Hd0 elim (lift_inv_bind1 … H) -H
+ #W #U #HVW #HTU #H destruct /4 width=6 by llpx_sn_bind, ldrop_skip, yle_succ/
+| #I #K1 #K2 #V #T #d0 #_ #_ #IHV #IHT #L1 #L2 #d #e #HLK1 #HLK2 #X #H #Hd0 elim (lift_inv_flat1 … H) -H
+ #W #U #HVW #HTU #H destruct /3 width=6 by llpx_sn_flat/
+]
+qed-.
+
+lemma llpx_sn_lift_ge: ∀R,K1,K2,T,d0. llpx_sn R d0 T K1 K2 →
+ ∀L1,L2,d,e. ⇩[Ⓕ, d, e] L1 ≡ K1 → ⇩[Ⓕ, d, e] L2 ≡ K2 →
+ ∀U. ⇧[d, e] T ≡ U → d ≤ d0 → llpx_sn R (d0+e) U L1 L2.
+#R #K1 #K2 #T #d0 #H elim H -K1 -K2 -T -d0
+[ #K1 #K2 #d0 #k #HK12 #L1 #L2 #d #e #HLK1 #HLK2 #X #H #_ >(lift_inv_sort1 … H) -X
+ lapply (ldrop_fwd_length_eq2 … HLK1 HLK2 HK12) -K1 -K2 -d
+ /2 width=1 by llpx_sn_sort/
+| #K1 #K2 #d0 #i #HK12 #Hid0 #L1 #L2 #d #e #HLK1 #HLK2 #X #H #_ elim (lift_inv_lref1 … H) -H
+ * #_ #H destruct
+ lapply (ldrop_fwd_length_eq2 … HLK1 HLK2 HK12) -K1 -K2
+ [ /3 width=3 by llpx_sn_skip, ylt_plus_dx2_trans/
+ | /3 width=3 by llpx_sn_skip, monotonic_ylt_plus_dx/
+ ]
+| #I #K1 #K2 #K11 #K22 #V1 #V2 #d0 #i #Hid0 #HK11 #HK22 #HK12 #HV12 #_ #L1 #L2 #d #e #HLK1 #HLK2 #X #H #Hd0 elim (lift_inv_lref1 … H) -H
+ * #Hid #H destruct
+ [ elim (ylt_yle_false … Hid0) -I -L1 -L2 -K1 -K2 -K11 -K22 -V1 -V2 -e -Hid0
+ /3 width=3 by ylt_yle_trans, ylt_inj/
+ | lapply (ldrop_trans_ge_comm … HLK1 … HK11 ?) // -K1
+ lapply (ldrop_trans_ge_comm … HLK2 … HK22 ?) // -Hid -Hd0 -K2
+ /3 width=9 by llpx_sn_lref, monotonic_yle_plus_dx/
+ ]
+| #K1 #K2 #d0 #i #HK1 #HK2 #HK12 #L1 #L2 #d #e #HLK1 #HLK2 #X #H #Hd0 elim (lift_inv_lref1 … H) -H
+ * #Hid #H destruct
+ lapply (ldrop_fwd_length_eq2 … HLK1 HLK2 HK12) -HK12
+ [ /3 width=7 by llpx_sn_free, ldrop_fwd_be/
+ | lapply (ldrop_fwd_length … HLK1) -HLK1 #HLK1
+ lapply (ldrop_fwd_length … HLK2) -HLK2 #HLK2
+ @llpx_sn_free [ >HLK1 | >HLK2 ] -Hid -HLK1 -HLK2 /2 width=1 by monotonic_le_plus_r/ (**) (* explicit constructor *)
+ ]
+| #K1 #K2 #d0 #p #HK12 #L1 #L2 #d #e #HLK1 #HLK2 #X #H #_ >(lift_inv_gref1 … H) -X
+ lapply (ldrop_fwd_length_eq2 … HLK1 HLK2 HK12) -K1 -K2 -d
+ /2 width=1 by llpx_sn_gref/
+| #a #I #K1 #K2 #V #T #d0 #_ #_ #IHV #IHT #L1 #L2 #d #e #HLK1 #HLK2 #X #H #Hd0 elim (lift_inv_bind1 … H) -H
+ #W #U #HVW #HTU #H destruct /4 width=5 by llpx_sn_bind, ldrop_skip, yle_succ/
+| #I #K1 #K2 #V #T #d0 #_ #_ #IHV #IHT #L1 #L2 #d #e #HLK1 #HLK2 #X #H #Hd0 elim (lift_inv_flat1 … H) -H
+ #W #U #HVW #HTU #H destruct /3 width=5 by llpx_sn_flat/
+]
+qed-.
+
+(* Inversion lemmas on relocation *******************************************)
+
+lemma llpx_sn_inv_lift_le: ∀R. (∀I. l_deliftable_sn (R I)) →
+ ∀L1,L2,U,d0. llpx_sn R d0 U L1 L2 →
+ ∀K1,K2,d,e. ⇩[Ⓕ, d, e] L1 ≡ K1 → ⇩[Ⓕ, d, e] L2 ≡ K2 →
+ ∀T. ⇧[d, e] T ≡ U → d0 ≤ d → llpx_sn R d0 T K1 K2.
+#R #HR #L1 #L2 #U #d0 #H elim H -L1 -L2 -U -d0
+[ #L1 #L2 #d0 #k #HL12 #K1 #K2 #d #e #HLK1 #HLK2 #X #H #_ >(lift_inv_sort2 … H) -X
+ lapply (ldrop_fwd_length_eq1 … HLK1 HLK2 HL12) -L1 -L2 -d -e
+ /2 width=1 by llpx_sn_sort/
+| #L1 #L2 #d0 #i #HL12 #Hid0 #K1 #K2 #d #e #HLK1 #HLK2 #X #H #_ elim (lift_inv_lref2 … H) -H
+ * #_ #H destruct
+ lapply (ldrop_fwd_length_eq1 … HLK1 HLK2 HL12) -L1 -L2
+ [ /2 width=1 by llpx_sn_skip/
+ | /3 width=3 by llpx_sn_skip, yle_ylt_trans/
+ ]
+| #I #L1 #L2 #K11 #K22 #W1 #W2 #d0 #i #Hid0 #HLK11 #HLK22 #HK12 #HW12 #IHK12 #K1 #K2 #d #e #HLK1 #HLK2 #X #H #Hd0 elim (lift_inv_lref2 … H) -H
+ * #Hid #H destruct [ -HK12 | -IHK12 ]
+ [ elim (ldrop_conf_lt … HLK1 … HLK11) // -L1 #L1 #V1 #HKL1 #HKL11 #HVW1
+ elim (ldrop_conf_lt … HLK2 … HLK22) // -Hid -L2 #L2 #V2 #HKL2 #HKL22 #HVW2
+ elim (HR … HW12 … HKL11 … HVW1) -HR #V0 #HV0 #HV12
+ lapply (lift_inj … HV0 … HVW2) -HV0 -HVW2 #H destruct
+ /3 width=10 by llpx_sn_lref/
+ | lapply (ldrop_conf_ge … HLK1 … HLK11 ?) // -L1
+ lapply (ldrop_conf_ge … HLK2 … HLK22 ?) // -L2 -Hid0
+ elim (le_inv_plus_l … Hid) -Hid /4 width=9 by llpx_sn_lref, yle_trans, yle_inj/ (**) (* slow *)
+ ]
+| #L1 #L2 #d0 #i #HL1 #HL2 #HL12 #K1 #K2 #d #e #HLK1 #HLK2 #X #H #Hd0 elim (lift_inv_lref2 … H) -H
+ * #_ #H destruct
+ lapply (ldrop_fwd_length_eq1 … HLK1 HLK2 HL12)
+ [ lapply (ldrop_fwd_length_le4 … HLK1) -HLK1
+ lapply (ldrop_fwd_length_le4 … HLK2) -HLK2
+ #HKL2 #HKL1 #HK12 @llpx_sn_free // /2 width=3 by transitive_le/ (**) (* full auto too slow *)
+ | lapply (ldrop_fwd_length … HLK1) -HLK1 #H >H in HL1; -H
+ lapply (ldrop_fwd_length … HLK2) -HLK2 #H >H in HL2; -H
+ /3 width=1 by llpx_sn_free, le_plus_to_minus_r/
+ ]
+| #L1 #L2 #d0 #p #HL12 #K1 #K2 #d #e #HLK1 #HLK2 #X #H #_ >(lift_inv_gref2 … H) -X
+ lapply (ldrop_fwd_length_eq1 … HLK1 HLK2 HL12) -L1 -L2 -d -e
+ /2 width=1 by llpx_sn_gref/
+| #a #I #L1 #L2 #W #U #d0 #_ #_ #IHW #IHU #K1 #K2 #d #e #HLK1 #HLK2 #X #H #Hd0 elim (lift_inv_bind2 … H) -H
+ #V #T #HVW #HTU #H destruct /4 width=6 by llpx_sn_bind, ldrop_skip, yle_succ/
+| #I #L1 #L2 #W #U #d0 #_ #_ #IHW #IHU #K1 #K2 #d #e #HLK1 #HLK2 #X #H #Hd0 elim (lift_inv_flat2 … H) -H
+ #V #T #HVW #HTU #H destruct /3 width=6 by llpx_sn_flat/
+]
+qed-.
+
+lemma llpx_sn_inv_lift_be: ∀R,L1,L2,U,d0. llpx_sn R d0 U L1 L2 →
+ ∀K1,K2,d,e. ⇩[Ⓕ, d, e] L1 ≡ K1 → ⇩[Ⓕ, d, e] L2 ≡ K2 →
+ ∀T. ⇧[d, e] T ≡ U → d ≤ d0 → d0 ≤ yinj d + e → llpx_sn R d T K1 K2.
+#R #L1 #L2 #U #d0 #H elim H -L1 -L2 -U -d0
+[ #L1 #L2 #d0 #k #HL12 #K1 #K2 #d #e #HLK1 #HLK2 #X #H #_ #_ >(lift_inv_sort2 … H) -X
+ lapply (ldrop_fwd_length_eq1 … HLK1 HLK2 HL12) -L1 -L2 -d0 -e
+ /2 width=1 by llpx_sn_sort/
+| #L1 #L2 #d0 #i #HL12 #Hid0 #K1 #K2 #d #e #HLK1 #HLK2 #X #H #Hd0 #Hd0e elim (lift_inv_lref2 … H) -H
+ * #Hid #H destruct
+ [ lapply (ldrop_fwd_length_eq1 … HLK1 HLK2 HL12) -L1 -L2
+ -Hid0 /3 width=1 by llpx_sn_skip, ylt_inj/
+ | elim (ylt_yle_false … Hid0) -L1 -L2 -Hd0 -Hid0
+ /3 width=3 by yle_trans, yle_inj/ (**) (* slow *)
+ ]
+| #I #L1 #L2 #K11 #K22 #W1 #W2 #d0 #i #Hid0 #HLK11 #HLK22 #HK12 #HW12 #_ #K1 #K2 #d #e #HLK1 #HLK2 #X #H #Hd0 #Hd0e elim (lift_inv_lref2 … H) -H
+ * #Hid #H destruct
+ [ elim (ylt_yle_false … Hid0) -I -L1 -L2 -K11 -K22 -W1 -W2 -Hd0e -Hid0
+ /3 width=3 by ylt_yle_trans, ylt_inj/
+ | lapply (ldrop_conf_ge … HLK1 … HLK11 ?) // -L1
+ lapply (ldrop_conf_ge … HLK2 … HLK22 ?) // -L2 -Hid0 -Hd0 -Hd0e
+ elim (le_inv_plus_l … Hid) -Hid /3 width=9 by llpx_sn_lref, yle_inj/
+ ]
+| #L1 #L2 #d0 #i #HL1 #HL2 #HL12 #K1 #K2 #d #e #HLK1 #HLK2 #X #H #Hd0 #Hd0e elim (lift_inv_lref2 … H) -H
+ * #_ #H destruct
+ lapply (ldrop_fwd_length_eq1 … HLK1 HLK2 HL12)
+ [ lapply (ldrop_fwd_length_le4 … HLK1) -HLK1
+ lapply (ldrop_fwd_length_le4 … HLK2) -HLK2
+ #HKL2 #HKL1 #HK12 @llpx_sn_free // /2 width=3 by transitive_le/ (**) (* full auto too slow *)
+ | lapply (ldrop_fwd_length … HLK1) -HLK1 #H >H in HL1; -H
+ lapply (ldrop_fwd_length … HLK2) -HLK2 #H >H in HL2; -H
+ /3 width=1 by llpx_sn_free, le_plus_to_minus_r/
+ ]
+| #L1 #L2 #d0 #p #HL12 #K1 #K2 #d #e #HLK1 #HLK2 #X #H #_ #_ >(lift_inv_gref2 … H) -X
+ lapply (ldrop_fwd_length_eq1 … HLK1 HLK2 HL12) -L1 -L2 -d0 -e
+ /2 width=1 by llpx_sn_gref/
+| #a #I #L1 #L2 #W #U #d0 #_ #_ #IHW #IHU #K1 #K2 #d #e #HLK1 #HLK2 #X #H #Hd0 #Hd0e elim (lift_inv_bind2 … H) -H
+ >commutative_plus #V #T #HVW #HTU #H destruct
+ @llpx_sn_bind [ /2 width=5 by/ ] -IHW (**) (* explicit constructor *)
+ @(IHU … HTU) -IHU -HTU /2 width=1 by ldrop_skip, yle_succ/
+| #I #L1 #L2 #W #U #d0 #_ #_ #IHW #IHU #K1 #K2 #d #e #HLK1 #HLK2 #X #H #Hd0 #Hd0e elim (lift_inv_flat2 … H) -H
+ #V #T #HVW #HTU #H destruct /3 width=6 by llpx_sn_flat/
+]
+qed-.
+
+lemma llpx_sn_inv_lift_ge: ∀R,L1,L2,U,d0. llpx_sn R d0 U L1 L2 →
+ ∀K1,K2,d,e. ⇩[Ⓕ, d, e] L1 ≡ K1 → ⇩[Ⓕ, d, e] L2 ≡ K2 →
+ ∀T. ⇧[d, e] T ≡ U → yinj d + e ≤ d0 → llpx_sn R (d0-e) T K1 K2.
+#R #L1 #L2 #U #d0 #H elim H -L1 -L2 -U -d0
+[ #L1 #L2 #d0 #k #HL12 #K1 #K2 #d #e #HLK1 #HLK2 #X #H #_ >(lift_inv_sort2 … H) -X
+ lapply (ldrop_fwd_length_eq1 … HLK1 HLK2 HL12) -L1 -L2 -d
+ /2 width=1 by llpx_sn_sort/
+| #L1 #L2 #d0 #i #HL12 #Hid0 #K1 #K2 #d #e #HLK1 #HLK2 #X #H #Hded0 elim (lift_inv_lref2 … H) -H
+ * #Hid #H destruct [ -Hid0 | -Hded0 ]
+ lapply (ldrop_fwd_length_eq1 … HLK1 HLK2 HL12) -L1 -L2
+ [ /4 width=3 by llpx_sn_skip, yle_plus_to_minus_inj2, ylt_yle_trans, ylt_inj/
+ | elim (le_inv_plus_l … Hid) -Hid #_
+ /4 width=1 by llpx_sn_skip, monotonic_ylt_minus_dx, yle_inj/
+ ]
+| #I #L1 #L2 #K11 #K22 #W1 #W2 #d0 #i #Hid0 #HLK11 #HLK22 #HK12 #HW12 #_ #K1 #K2 #d #e #HLK1 #HLK2 #X #H #Hded0 elim (lift_inv_lref2 … H) -H
+ * #Hid #H destruct
+ [ elim (ylt_yle_false … Hid0) -I -L1 -L2 -K11 -K22 -W1 -W2 -Hid0
+ /3 width=3 by yle_fwd_plus_sn1, ylt_yle_trans, ylt_inj/
+ | lapply (ldrop_conf_ge … HLK1 … HLK11 ?) // -L1
+ lapply (ldrop_conf_ge … HLK2 … HLK22 ?) // -L2 -Hded0 -Hid
+ /3 width=9 by llpx_sn_lref, monotonic_yle_minus_dx/
+ ]
+| #L1 #L2 #d0 #i #HL1 #HL2 #HL12 #K1 #K2 #d #e #HLK1 #HLK2 #X #H #Hded0 elim (lift_inv_lref2 … H) -H
+ * #_ #H destruct
+ lapply (ldrop_fwd_length_eq1 … HLK1 HLK2 HL12)
+ [ lapply (ldrop_fwd_length_le4 … HLK1) -HLK1
+ lapply (ldrop_fwd_length_le4 … HLK2) -HLK2
+ #HKL2 #HKL1 #HK12 @llpx_sn_free // /2 width=3 by transitive_le/ (**) (* full auto too slow *)
+ | lapply (ldrop_fwd_length … HLK1) -HLK1 #H >H in HL1; -H
+ lapply (ldrop_fwd_length … HLK2) -HLK2 #H >H in HL2; -H
+ /3 width=1 by llpx_sn_free, le_plus_to_minus_r/
+ ]
+| #L1 #L2 #d0 #p #HL12 #K1 #K2 #d #e #HLK1 #HLK2 #X #H #_ >(lift_inv_gref2 … H) -X
+ lapply (ldrop_fwd_length_eq1 … HLK1 HLK2 HL12) -L1 -L2 -d
+ /2 width=1 by llpx_sn_gref/
+| #a #I #L1 #L2 #W #U #d0 #_ #_ #IHW #IHU #K1 #K2 #d #e #HLK1 #HLK2 #X #H #Hded0 elim (lift_inv_bind2 … H) -H
+ #V #T #HVW #HTU #H destruct
+ @llpx_sn_bind [ /2 width=5 by/ ] -IHW (**) (* explicit constructor *)
+ <yminus_succ1_inj /2 width=2 by yle_fwd_plus_sn2/
+ @(IHU … HTU) -IHU -HTU /2 width=1 by ldrop_skip, yle_succ/
+| #I #L1 #L2 #W #U #d0 #_ #_ #IHW #IHU #K1 #K2 #d #e #HLK1 #HLK2 #X #H #Hded0 elim (lift_inv_flat2 … H) -H
+ #V #T #HVW #HTU #H destruct /3 width=5 by llpx_sn_flat/
+]
+qed-.
+
+(* Advanced inversion lemmas on relocation **********************************)
+
+lemma llpx_sn_inv_lift_O: ∀R,L1,L2,U. llpx_sn R 0 U L1 L2 →
+ ∀K1,K2,e. ⇩[e] L1 ≡ K1 → ⇩[e] L2 ≡ K2 →
+ ∀T. ⇧[0, e] T ≡ U → llpx_sn R 0 T K1 K2.
+/2 width=11 by llpx_sn_inv_lift_be/ qed-.
+
+lemma llpx_sn_ldrop_conf_O: ∀R,L1,L2,U. llpx_sn R 0 U L1 L2 →
+ ∀K1,e. ⇩[e] L1 ≡ K1 → ∀T. ⇧[0, e] T ≡ U →
+ ∃∃K2. ⇩[e] L2 ≡ K2 & llpx_sn R 0 T K1 K2.
+#R #L1 #L2 #U #HU #K1 #e #HLK1 #T #HTU elim (llpx_sn_fwd_ldrop_sn … HU … HLK1)
+/3 width=10 by llpx_sn_inv_lift_O, ex2_intro/
+qed-.
+
+lemma llpx_sn_ldrop_trans_O: ∀R,L1,L2,U. llpx_sn R 0 U L1 L2 →
+ ∀K2,e. ⇩[e] L2 ≡ K2 → ∀T. ⇧[0, e] T ≡ U →
+ ∃∃K1. ⇩[e] L1 ≡ K1 & llpx_sn R 0 T K1 K2.
+#R #L1 #L2 #U #HU #K2 #e #HLK2 #T #HTU elim (llpx_sn_fwd_ldrop_dx … HU … HLK2)
+/3 width=10 by llpx_sn_inv_lift_O, ex2_intro/
+qed-.
+
+(* Inversion lemmas on negated lazy pointwise extension *********************)
+
+lemma nllpx_sn_inv_bind: ∀R. (∀I,L,T1,T2. Decidable (R I L T1 T2)) →
+ ∀a,I,L1,L2,V,T,d. (llpx_sn R d (ⓑ{a,I}V.T) L1 L2 → ⊥) →
+ (llpx_sn R d V L1 L2 → ⊥) ∨ (llpx_sn R (⫯d) T (L1.ⓑ{I}V) (L2.ⓑ{I}V) → ⊥).
+#R #HR #a #I #L1 #L2 #V #T #d #H elim (llpx_sn_dec … HR V L1 L2 d)
+/4 width=1 by llpx_sn_bind, or_intror, or_introl/
+qed-.
+
+lemma nllpx_sn_inv_flat: ∀R. (∀I,L,T1,T2. Decidable (R I L T1 T2)) →
+ ∀I,L1,L2,V,T,d. (llpx_sn R d (ⓕ{I}V.T) L1 L2 → ⊥) →
+ (llpx_sn R d V L1 L2 → ⊥) ∨ (llpx_sn R d T L1 L2 → ⊥).
+#R #HR #I #L1 #L2 #V #T #d #H elim (llpx_sn_dec … HR V L1 L2 d)
+/4 width=1 by llpx_sn_flat, or_intror, or_introl/
+qed-.
+
+lemma nllpx_sn_inv_bind_O: ∀R. (∀I,L,T1,T2. Decidable (R I L T1 T2)) →
+ ∀a,I,L1,L2,V,T. (llpx_sn R 0 (ⓑ{a,I}V.T) L1 L2 → ⊥) →
+ (llpx_sn R 0 V L1 L2 → ⊥) ∨ (llpx_sn R 0 T (L1.ⓑ{I}V) (L2.ⓑ{I}V) → ⊥).
+#R #HR #a #I #L1 #L2 #V #T #H elim (llpx_sn_dec … HR V L1 L2 0)
+/4 width=1 by llpx_sn_bind_O, or_intror, or_introl/
+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/lpx_sn_ldrop.ma".
+include "basic_2/substitution/llpx_sn.ma".
+
+(* LAZY SN POINTWISE EXTENSION OF A CONTEXT-SENSITIVE REALTION FOR TERMS ****)
+
+(* Properties on pointwise extensions ***************************************)
+
+lemma lpx_sn_llpx_sn: ∀R. (∀I,L. reflexive … (R I L)) →
+ ∀T,L1,L2,d. lpx_sn R L1 L2 → llpx_sn R d T L1 L2.
+#R #HR #T #L1 @(f2_ind … rfw … L1 T) -L1 -T
+#n #IH #L1 * *
+[ -HR -IH /4 width=2 by lpx_sn_fwd_length, llpx_sn_sort/
+| -HR #i elim (lt_or_ge i (|L1|))
+ [2: -IH /4 width=4 by lpx_sn_fwd_length, llpx_sn_free, le_repl_sn_conf_aux/ ]
+ #Hi #Hn #L2 #d elim (ylt_split i d)
+ [ -n /3 width=2 by llpx_sn_skip, lpx_sn_fwd_length/ ]
+ #Hdi #HL12 elim (ldrop_O1_lt (Ⓕ) L1 i) //
+ #I #K1 #V1 #HLK1 elim (lpx_sn_ldrop_conf … HL12 … HLK1) -HL12
+ /4 width=9 by llpx_sn_lref, ldrop_fwd_rfw/
+| -HR -IH /4 width=2 by lpx_sn_fwd_length, llpx_sn_gref/
+| /4 width=1 by llpx_sn_bind, lpx_sn_pair/
+| -HR /3 width=1 by llpx_sn_flat/
+]
+qed.
--- /dev/null
+(**************************************************************************)
+(* ___ *)
+(* ||M|| *)
+(* ||A|| A project by Andrea Asperti *)
+(* ||T|| *)
+(* ||I|| Developers: *)
+(* ||T|| The HELM team. *)
+(* ||A|| http://helm.cs.unibo.it *)
+(* \ / *)
+(* \ / This file is distributed under the terms of the *)
+(* v GNU General Public License Version 2 *)
+(* *)
+(**************************************************************************)
+
+include "basic_2/substitution/llpx_sn_ldrop.ma".
+
+(* LAZY SN POINTWISE EXTENSION OF A CONTEXT-SENSITIVE REALTION FOR TERMS ****)
+
+(* Properties about transitive closure **************************************)
+
+lemma llpx_sn_TC_pair_dx: ∀R. (∀I,L. reflexive … (R I L)) →
+ ∀I,L,V1,V2,T. LTC … (R I) L V1 V2 →
+ LTC … (llpx_sn R 0) T (L.ⓑ{I}V1) (L.ⓑ{I}V2).
+#R #HR #I #L #V1 #V2 #T #H @(TC_star_ind … V2 H) -V2
+/4 width=9 by llpx_sn_bind_repl_O, llpx_sn_refl, step, inj/
+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/predsn_3.ma".
+include "basic_2/relocation/lpx_sn.ma".
+include "basic_2/reduction/cpr.ma".
+
+(* SN PARALLEL REDUCTION FOR LOCAL ENVIRONMENTS *****************************)
+
+definition lpr: relation3 genv lenv lenv ≝ λG. lpx_sn (λ_.cpr G).
+
+interpretation "parallel reduction (local environment, sn variant)"
+ 'PRedSn G L1 L2 = (lpr G L1 L2).
+
+(* Basic inversion lemmas ***************************************************)
+
+(* Basic_1: includes: wcpr0_gen_sort *)
+lemma lpr_inv_atom1: ∀G,L2. ⦃G, ⋆⦄ ⊢ ➡ L2 → L2 = ⋆.
+/2 width=4 by lpx_sn_inv_atom1_aux/ qed-.
+
+(* Basic_1: includes: wcpr0_gen_head *)
+lemma lpr_inv_pair1: ∀I,G,K1,V1,L2. ⦃G, K1.ⓑ{I}V1⦄ ⊢ ➡ L2 →
+ ∃∃K2,V2. ⦃G, K1⦄ ⊢ ➡ K2 & ⦃G, K1⦄ ⊢ V1 ➡ V2 & L2 = K2.ⓑ{I}V2.
+/2 width=3 by lpx_sn_inv_pair1_aux/ qed-.
+
+lemma lpr_inv_atom2: ∀G,L1. ⦃G, L1⦄ ⊢ ➡ ⋆ → L1 = ⋆.
+/2 width=4 by lpx_sn_inv_atom2_aux/ qed-.
+
+lemma lpr_inv_pair2: ∀I,G,L1,K2,V2. ⦃G, L1⦄ ⊢ ➡ K2.ⓑ{I}V2 →
+ ∃∃K1,V1. ⦃G, K1⦄ ⊢ ➡ K2 & ⦃G, K1⦄ ⊢ V1 ➡ V2 & L1 = K1. ⓑ{I} V1.
+/2 width=3 by lpx_sn_inv_pair2_aux/ qed-.
+
+(* Basic properties *********************************************************)
+
+(* Note: lemma 250 *)
+lemma lpr_refl: ∀G,L. ⦃G, L⦄ ⊢ ➡ L.
+/2 width=1 by lpx_sn_refl/ qed.
+
+lemma lpr_pair: ∀I,G,K1,K2,V1,V2. ⦃G, K1⦄ ⊢ ➡ K2 → ⦃G, K1⦄ ⊢ V1 ➡ V2 →
+ ⦃G, K1.ⓑ{I}V1⦄ ⊢ ➡ K2.ⓑ{I}V2.
+/2 width=1 by lpx_sn_pair/ qed.
+
+(* Basic forward lemmas *****************************************************)
+
+lemma lpr_fwd_length: ∀G,L1,L2. ⦃G, L1⦄ ⊢ ➡ L2 → |L1| = |L2|.
+/2 width=2 by lpx_sn_fwd_length/ qed-.
+
+(* Basic_1: removed theorems 3: wcpr0_getl wcpr0_getl_back
+ pr0_subst1_back
+*)
--- /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/predsn_5.ma".
+include "basic_2/reduction/lpr.ma".
+include "basic_2/reduction/cpx.ma".
+
+(* SN EXTENDED PARALLEL REDUCTION FOR LOCAL ENVIRONMENTS ********************)
+
+definition lpx: ∀h. sd h → relation3 genv lenv lenv ≝
+ λh,g,G. lpx_sn (λ_.cpx h g G).
+
+interpretation "extended parallel reduction (local environment, sn variant)"
+ 'PRedSn h g G L1 L2 = (lpx h g G L1 L2).
+
+(* Basic inversion lemmas ***************************************************)
+
+lemma lpx_inv_atom1: ∀h,g,G,L2. ⦃G, ⋆⦄ ⊢ ➡[h, g] L2 → L2 = ⋆.
+/2 width=4 by lpx_sn_inv_atom1_aux/ qed-.
+
+lemma lpx_inv_pair1: ∀h,g,I,G,K1,V1,L2. ⦃G, K1.ⓑ{I}V1⦄ ⊢ ➡[h, g] L2 →
+ ∃∃K2,V2. ⦃G, K1⦄ ⊢ ➡[h, g] K2 & ⦃G, K1⦄ ⊢ V1 ➡[h, g] V2 &
+ L2 = K2. ⓑ{I} V2.
+/2 width=3 by lpx_sn_inv_pair1_aux/ qed-.
+
+lemma lpx_inv_atom2: ∀h,g,G,L1. ⦃G, L1⦄ ⊢ ➡[h, g] ⋆ → L1 = ⋆.
+/2 width=4 by lpx_sn_inv_atom2_aux/ qed-.
+
+lemma lpx_inv_pair2: ∀h,g,I,G,L1,K2,V2. ⦃G, L1⦄ ⊢ ➡[h, g] K2.ⓑ{I}V2 →
+ ∃∃K1,V1. ⦃G, K1⦄ ⊢ ➡[h, g] K2 & ⦃G, K1⦄ ⊢ V1 ➡[h, g] V2 &
+ L1 = K1. ⓑ{I} V1.
+/2 width=3 by lpx_sn_inv_pair2_aux/ qed-.
+
+lemma lpx_inv_pair: ∀h,g,I1,I2,G,L1,L2,V1,V2. ⦃G, L1.ⓑ{I1}V1⦄ ⊢ ➡[h, g] L2.ⓑ{I2}V2 →
+ ∧∧ ⦃G, L1⦄ ⊢ ➡[h, g] L2 & ⦃G, L1⦄ ⊢ V1 ➡[h, g] V2 & I1 = I2.
+/2 width=1 by lpx_sn_inv_pair/ qed-.
+
+(* Basic properties *********************************************************)
+
+lemma lpx_refl: ∀h,g,G,L. ⦃G, L⦄ ⊢ ➡[h, g] L.
+/2 width=1 by lpx_sn_refl/ qed.
+
+lemma lpx_pair: ∀h,g,I,G,K1,K2,V1,V2. ⦃G, K1⦄ ⊢ ➡[h, g] K2 → ⦃G, K1⦄ ⊢ V1 ➡[h, g] V2 →
+ ⦃G, K1.ⓑ{I}V1⦄ ⊢ ➡[h, g] K2.ⓑ{I}V2.
+/2 width=1 by lpx_sn_pair/ qed.
+
+lemma lpr_lpx: ∀h,g,G,L1,L2. ⦃G, L1⦄ ⊢ ➡ L2 → ⦃G, L1⦄ ⊢ ➡[h, g] L2.
+#h #g #G #L1 #L2 #H elim H -L1 -L2 /3 width=1 by lpx_pair, cpr_cpx/
+qed.
+
+(* Basic forward lemmas *****************************************************)
+
+lemma lpx_fwd_length: ∀h,g,G,L1,L2. ⦃G, L1⦄ ⊢ ➡[h, g] L2 → |L1| = |L2|.
+/2 width=2 by lpx_sn_fwd_length/ 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/grammar/lenv_length.ma".
+
+(* SN POINTWISE EXTENSION OF A CONTEXT-SENSITIVE REALTION FOR TERMS *********)
+
+inductive lpx_sn (R:relation4 bind2 lenv term term): relation lenv ≝
+| lpx_sn_atom: lpx_sn R (⋆) (⋆)
+| lpx_sn_pair: ∀I,K1,K2,V1,V2.
+ lpx_sn R K1 K2 → R I K1 V1 V2 →
+ lpx_sn R (K1.ⓑ{I}V1) (K2.ⓑ{I}V2)
+.
+
+(* Basic properties *********************************************************)
+
+lemma lpx_sn_refl: ∀R. (∀I,L. reflexive ? (R I L)) → reflexive … (lpx_sn R).
+#R #HR #L elim L -L /2 width=1 by lpx_sn_atom, lpx_sn_pair/
+qed-.
+
+(* Basic inversion lemmas ***************************************************)
+
+fact lpx_sn_inv_atom1_aux: ∀R,L1,L2. lpx_sn R L1 L2 → L1 = ⋆ → L2 = ⋆.
+#R #L1 #L2 * -L1 -L2
+[ //
+| #I #K1 #K2 #V1 #V2 #_ #_ #H destruct
+]
+qed-.
+
+lemma lpx_sn_inv_atom1: ∀R,L2. lpx_sn R (⋆) L2 → L2 = ⋆.
+/2 width=4 by lpx_sn_inv_atom1_aux/ qed-.
+
+fact lpx_sn_inv_pair1_aux: ∀R,L1,L2. lpx_sn R L1 L2 → ∀I,K1,V1. L1 = K1.ⓑ{I}V1 →
+ ∃∃K2,V2. lpx_sn R K1 K2 & R I K1 V1 V2 & L2 = K2.ⓑ{I}V2.
+#R #L1 #L2 * -L1 -L2
+[ #J #K1 #V1 #H destruct
+| #I #K1 #K2 #V1 #V2 #HK12 #HV12 #J #L #W #H destruct /2 width=5 by ex3_2_intro/
+]
+qed-.
+
+lemma lpx_sn_inv_pair1: ∀R,I,K1,V1,L2. lpx_sn R (K1.ⓑ{I}V1) L2 →
+ ∃∃K2,V2. lpx_sn R K1 K2 & R I K1 V1 V2 & L2 = K2.ⓑ{I}V2.
+/2 width=3 by lpx_sn_inv_pair1_aux/ qed-.
+
+fact lpx_sn_inv_atom2_aux: ∀R,L1,L2. lpx_sn R L1 L2 → L2 = ⋆ → L1 = ⋆.
+#R #L1 #L2 * -L1 -L2
+[ //
+| #I #K1 #K2 #V1 #V2 #_ #_ #H destruct
+]
+qed-.
+
+lemma lpx_sn_inv_atom2: ∀R,L1. lpx_sn R L1 (⋆) → L1 = ⋆.
+/2 width=4 by lpx_sn_inv_atom2_aux/ qed-.
+
+fact lpx_sn_inv_pair2_aux: ∀R,L1,L2. lpx_sn R L1 L2 → ∀I,K2,V2. L2 = K2.ⓑ{I}V2 →
+ ∃∃K1,V1. lpx_sn R K1 K2 & R I K1 V1 V2 & L1 = K1.ⓑ{I}V1.
+#R #L1 #L2 * -L1 -L2
+[ #J #K2 #V2 #H destruct
+| #I #K1 #K2 #V1 #V2 #HK12 #HV12 #J #K #W #H destruct /2 width=5 by ex3_2_intro/
+]
+qed-.
+
+lemma lpx_sn_inv_pair2: ∀R,I,L1,K2,V2. lpx_sn R L1 (K2.ⓑ{I}V2) →
+ ∃∃K1,V1. lpx_sn R K1 K2 & R I K1 V1 V2 & L1 = K1.ⓑ{I}V1.
+/2 width=3 by lpx_sn_inv_pair2_aux/ qed-.
+
+lemma lpx_sn_inv_pair: ∀R,I1,I2,L1,L2,V1,V2.
+ lpx_sn R (L1.ⓑ{I1}V1) (L2.ⓑ{I2}V2) →
+ ∧∧ lpx_sn R L1 L2 & R I1 L1 V1 V2 & I1 = I2.
+#R #I1 #I2 #L1 #L2 #V1 #V2 #H elim (lpx_sn_inv_pair1 … H) -H
+#L0 #V0 #HL10 #HV10 #H destruct /2 width=1 by and3_intro/
+qed-.
+
+(* Basic forward lemmas *****************************************************)
+
+lemma lpx_sn_fwd_length: ∀R,L1,L2. lpx_sn R L1 L2 → |L1| = |L2|.
+#R #L1 #L2 #H elim H -L1 -L2 normalize //
+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/ldrop.ma".
+include "basic_2/relocation/lpx_sn.ma".
+
+(* SN POINTWISE EXTENSION OF A CONTEXT-SENSITIVE REALTION FOR TERMS *********)
+
+(* alternative definition of lpx_sn *)
+definition lpx_sn_alt: relation4 bind2 lenv term term → relation lenv ≝
+ λR,L1,L2. |L1| = |L2| ∧
+ (∀I1,I2,K1,K2,V1,V2,i.
+ ⇩[i] L1 ≡ K1.ⓑ{I1}V1 → ⇩[i] L2 ≡ K2.ⓑ{I2}V2 →
+ I1 = I2 ∧ R I1 K1 V1 V2
+ ).
+
+(* Basic forward lemmas ******************************************************)
+
+lemma lpx_sn_alt_fwd_length: ∀R,L1,L2. lpx_sn_alt R L1 L2 → |L1| = |L2|.
+#R #L1 #L2 #H elim H //
+qed-.
+
+(* Basic inversion lemmas ***************************************************)
+
+lemma lpx_sn_alt_inv_atom1: ∀R,L2. lpx_sn_alt R (⋆) L2 → L2 = ⋆.
+#R #L2 #H lapply (lpx_sn_alt_fwd_length … H) -H
+normalize /2 width=1 by length_inv_zero_sn/
+qed-.
+
+lemma lpx_sn_alt_inv_pair1: ∀R,I,L2,K1,V1. lpx_sn_alt R (K1.ⓑ{I}V1) L2 →
+ ∃∃K2,V2. lpx_sn_alt R K1 K2 & R I K1 V1 V2 & L2 = K2.ⓑ{I}V2.
+#R #I1 #L2 #K1 #V1 #H elim H -H
+#H #IH elim (length_inv_pos_sn … H) -H
+#I2 #K2 #V2 #HK12 #H destruct
+elim (IH I1 I2 K1 K2 V1 V2 0) //
+#H #HV12 destruct @(ex3_2_intro … K2 V2) // -HV12
+@conj // -HK12
+#J1 #J2 #L1 #L2 #W1 #W2 #i #HKL1 #HKL2 elim (IH J1 J2 L1 L2 W1 W2 (i+1)) -IH
+/2 width=1 by ldrop_drop, conj/
+qed-.
+
+lemma lpx_sn_alt_inv_atom2: ∀R,L1. lpx_sn_alt R L1 (⋆) → L1 = ⋆.
+#R #L1 #H lapply (lpx_sn_alt_fwd_length … H) -H
+normalize /2 width=1 by length_inv_zero_dx/
+qed-.
+
+lemma lpx_sn_alt_inv_pair2: ∀R,I,L1,K2,V2. lpx_sn_alt R L1 (K2.ⓑ{I}V2) →
+ ∃∃K1,V1. lpx_sn_alt R K1 K2 & R I K1 V1 V2 & L1 = K1.ⓑ{I}V1.
+#R #I2 #L1 #K2 #V2 #H elim H -H
+#H #IH elim (length_inv_pos_dx … H) -H
+#I1 #K1 #V1 #HK12 #H destruct
+elim (IH I1 I2 K1 K2 V1 V2 0) //
+#H #HV12 destruct @(ex3_2_intro … K1 V1) // -HV12
+@conj // -HK12
+#J1 #J2 #L1 #L2 #W1 #W2 #i #HKL1 #HKL2 elim (IH J1 J2 L1 L2 W1 W2 (i+1)) -IH
+/2 width=1 by ldrop_drop, conj/
+qed-.
+
+(* Basic properties *********************************************************)
+
+lemma lpx_sn_alt_atom: ∀R. lpx_sn_alt R (⋆) (⋆).
+#R @conj //
+#I1 #I2 #K1 #K2 #V1 #V2 #i #HLK1 elim (ldrop_inv_atom1 … HLK1) -HLK1
+#H destruct
+qed.
+
+lemma lpx_sn_alt_pair: ∀R,I,L1,L2,V1,V2.
+ lpx_sn_alt R L1 L2 → R I L1 V1 V2 →
+ lpx_sn_alt R (L1.ⓑ{I}V1) (L2.ⓑ{I}V2).
+#R #I #L1 #L2 #V1 #V2 #H #HV12 elim H -H
+#HL12 #IH @conj normalize //
+#I1 #I2 #K1 #K2 #W1 #W2 #i @(nat_ind_plus … i) -i
+[ #HLK1 #HLK2
+ lapply (ldrop_inv_O2 … HLK1) -HLK1 #H destruct
+ lapply (ldrop_inv_O2 … HLK2) -HLK2 #H destruct
+ /2 width=1 by conj/
+| -HL12 -HV12 /3 width=6 by ldrop_inv_drop1/
+]
+qed.
+
+(* Main properties **********************************************************)
+
+theorem lpx_sn_lpx_sn_alt: ∀R,L1,L2. lpx_sn R L1 L2 → lpx_sn_alt R L1 L2.
+#R #L1 #L2 #H elim H -L1 -L2
+/2 width=1 by lpx_sn_alt_atom, lpx_sn_alt_pair/
+qed.
+
+(* Main inversion lemmas ****************************************************)
+
+theorem lpx_sn_alt_inv_lpx_sn: ∀R,L1,L2. lpx_sn_alt R L1 L2 → lpx_sn R L1 L2.
+#R #L1 elim L1 -L1
+[ #L2 #H lapply (lpx_sn_alt_inv_atom1 … H) -H //
+| #L1 #I #V1 #IH #X #H elim (lpx_sn_alt_inv_pair1 … H) -H
+ #L2 #V2 #HL12 #HV12 #H destruct /3 width=1 by lpx_sn_pair/
+]
+qed-.
+
+(* alternative definition of lpx_sn *****************************************)
+
+lemma lpx_sn_intro_alt: ∀R,L1,L2. |L1| = |L2| →
+ (∀I1,I2,K1,K2,V1,V2,i.
+ ⇩[i] L1 ≡ K1.ⓑ{I1}V1 → ⇩[i] L2 ≡ K2.ⓑ{I2}V2 →
+ I1 = I2 ∧ R I1 K1 V1 V2
+ ) → lpx_sn R L1 L2.
+/4 width=4 by lpx_sn_alt_inv_lpx_sn, conj/ qed.
+
+lemma lpx_sn_inv_alt: ∀R,L1,L2. lpx_sn R L1 L2 →
+ |L1| = |L2| ∧
+ ∀I1,I2,K1,K2,V1,V2,i.
+ ⇩[i] L1 ≡ K1.ⓑ{I1}V1 → ⇩[i] L2 ≡ K2.ⓑ{I2}V2 →
+ I1 = I2 ∧ R I1 K1 V1 V2.
+#R #L1 #L2 #H lapply (lpx_sn_lpx_sn_alt … H) -H
+#H elim H -H /3 width=4 by conj/
+qed-.
--- /dev/null
+(**************************************************************************)
+(* ___ *)
+(* ||M|| *)
+(* ||A|| A project by Andrea Asperti *)
+(* ||T|| *)
+(* ||I|| Developers: *)
+(* ||T|| The HELM team. *)
+(* ||A|| http://helm.cs.unibo.it *)
+(* \ / *)
+(* \ / This file is distributed under the terms of the *)
+(* v GNU General Public License Version 2 *)
+(* *)
+(**************************************************************************)
+
+include "basic_2/relocation/ldrop_leq.ma".
+include "basic_2/relocation/lpx_sn.ma".
+
+(* SN POINTWISE EXTENSION OF A CONTEXT-SENSITIVE REALTION FOR TERMS *********)
+
+(* Properies on dropping ****************************************************)
+
+lemma lpx_sn_ldrop_conf: ∀R,L1,L2. lpx_sn R L1 L2 →
+ ∀I,K1,V1,i. ⇩[i] L1 ≡ K1.ⓑ{I}V1 →
+ ∃∃K2,V2. ⇩[i] L2 ≡ K2.ⓑ{I}V2 & lpx_sn R K1 K2 & R I K1 V1 V2.
+#R #L1 #L2 #H elim H -L1 -L2
+[ #I0 #K0 #V0 #i #H elim (ldrop_inv_atom1 … H) -H #H destruct
+| #I #K1 #K2 #V1 #V2 #HK12 #HV12 #IHK12 #I0 #K0 #V0 #i #H elim (ldrop_inv_O1_pair1 … H) * -H
+ [ -IHK12 #H1 #H2 destruct /3 width=5 by ldrop_pair, ex3_2_intro/
+ | -HK12 -HV12 #Hi #HK10 elim (IHK12 … HK10) -IHK12 -HK10
+ /3 width=5 by ldrop_drop_lt, ex3_2_intro/
+ ]
+]
+qed-.
+
+lemma lpx_sn_ldrop_trans: ∀R,L1,L2. lpx_sn R L1 L2 →
+ ∀I,K2,V2,i. ⇩[i] L2 ≡ K2.ⓑ{I}V2 →
+ ∃∃K1,V1. ⇩[i] L1 ≡ K1.ⓑ{I}V1 & lpx_sn R K1 K2 & R I K1 V1 V2.
+#R #L1 #L2 #H elim H -L1 -L2
+[ #I0 #K0 #V0 #i #H elim (ldrop_inv_atom1 … H) -H #H destruct
+| #I #K1 #K2 #V1 #V2 #HK12 #HV12 #IHK12 #I0 #K0 #V0 #i #H elim (ldrop_inv_O1_pair1 … H) * -H
+ [ -IHK12 #H1 #H2 destruct /3 width=5 by ldrop_pair, ex3_2_intro/
+ | -HK12 -HV12 #Hi #HK10 elim (IHK12 … HK10) -IHK12 -HK10
+ /3 width=5 by ldrop_drop_lt, ex3_2_intro/
+ ]
+]
+qed-.
+
+lemma lpx_sn_deliftable_dropable: ∀R. (∀I. l_deliftable_sn (R I)) → dropable_sn (lpx_sn R).
+#R #HR #L1 #K1 #s #d #e #H elim H -L1 -K1 -d -e
+[ #d #e #He #X #H >(lpx_sn_inv_atom1 … H) -H
+ /4 width=3 by ldrop_atom, lpx_sn_atom, ex2_intro/
+| #I #K1 #V1 #X #H elim (lpx_sn_inv_pair1 … H) -H
+ #L2 #V2 #HL12 #HV12 #H destruct
+ /3 width=5 by ldrop_pair, lpx_sn_pair, ex2_intro/
+| #I #L1 #K1 #V1 #e #_ #IHLK1 #X #H elim (lpx_sn_inv_pair1 … H) -H
+ #L2 #V2 #HL12 #HV12 #H destruct
+ elim (IHLK1 … HL12) -L1 /3 width=3 by ldrop_drop, ex2_intro/
+| #I #L1 #K1 #V1 #W1 #d #e #HLK1 #HWV1 #IHLK1 #X #H
+ elim (lpx_sn_inv_pair1 … H) -H #L2 #V2 #HL12 #HV12 #H destruct
+ elim (HR … HV12 … HLK1 … HWV1) -V1
+ elim (IHLK1 … HL12) -L1 /3 width=5 by ldrop_skip, lpx_sn_pair, ex2_intro/
+]
+qed-.
+
+lemma lpx_sn_liftable_dedropable: ∀R. (∀I,L. reflexive ? (R I L)) →
+ (∀I. l_liftable (R I)) → dedropable_sn (lpx_sn R).
+#R #H1R #H2R #L1 #K1 #s #d #e #H elim H -L1 -K1 -d -e
+[ #d #e #He #X #H >(lpx_sn_inv_atom1 … H) -H
+ /4 width=4 by ldrop_atom, lpx_sn_atom, ex3_intro/
+| #I #K1 #V1 #X #H elim (lpx_sn_inv_pair1 … H) -H
+ #K2 #V2 #HK12 #HV12 #H destruct
+ lapply (lpx_sn_fwd_length … HK12)
+ #H @(ex3_intro … (K2.ⓑ{I}V2)) (**) (* explicit constructor *)
+ /3 width=1 by lpx_sn_pair, monotonic_le_plus_l/
+ @leq_O2 normalize //
+| #I #L1 #K1 #V1 #e #_ #IHLK1 #K2 #HK12 elim (IHLK1 … HK12) -K1
+ /3 width=5 by ldrop_drop, leq_pair, lpx_sn_pair, ex3_intro/
+| #I #L1 #K1 #V1 #W1 #d #e #HLK1 #HWV1 #IHLK1 #X #H
+ elim (lpx_sn_inv_pair1 … H) -H #K2 #W2 #HK12 #HW12 #H destruct
+ elim (lift_total W2 d e) #V2 #HWV2
+ lapply (H2R … HW12 … HLK1 … HWV1 … HWV2) -W1
+ elim (IHLK1 … HK12) -K1
+ /3 width=6 by ldrop_skip, leq_succ, lpx_sn_pair, ex3_intro/
+]
+qed-.
+
+fact lpx_sn_dropable_aux: ∀R,L2,K2,s,d,e. ⇩[s, d, e] L2 ≡ K2 → ∀L1. lpx_sn R L1 L2 →
+ d = 0 → ∃∃K1. ⇩[s, 0, e] L1 ≡ K1 & lpx_sn R K1 K2.
+#R #L2 #K2 #s #d #e #H elim H -L2 -K2 -d -e
+[ #d #e #He #X #H >(lpx_sn_inv_atom2 … H) -H
+ /4 width=3 by ldrop_atom, lpx_sn_atom, ex2_intro/
+| #I #K2 #V2 #X #H elim (lpx_sn_inv_pair2 … H) -H
+ #K1 #V1 #HK12 #HV12 #H destruct
+ /3 width=5 by ldrop_pair, lpx_sn_pair, ex2_intro/
+| #I #L2 #K2 #V2 #e #_ #IHLK2 #X #H #_ elim (lpx_sn_inv_pair2 … H) -H
+ #L1 #V1 #HL12 #HV12 #H destruct
+ elim (IHLK2 … HL12) -L2 /3 width=3 by ldrop_drop, ex2_intro/
+| #I #L2 #K2 #V2 #W2 #d #e #_ #_ #_ #L1 #_
+ <plus_n_Sm #H destruct
+]
+qed-.
+
+lemma lpx_sn_dropable: ∀R. dropable_dx (lpx_sn R).
+/2 width=5 by lpx_sn_dropable_aux/ 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/lpx_sn.ma".
+
+(* SN POINTWISE EXTENSION OF A CONTEXT-SENSITIVE REALTION FOR TERMS *********)
+
+definition lpx_sn_confluent: relation (relation3 lenv term term) ≝ λR1,R2.
+ ∀L0,T0,T1. R1 L0 T0 T1 → ∀T2. R2 L0 T0 T2 →
+ ∀L1. lpx_sn (λ_.R1) L0 L1 → ∀L2. lpx_sn (λ_.R2) L0 L2 →
+ ∃∃T. R2 L1 T1 T & R1 L2 T2 T.
+
+definition lpx_sn_transitive: relation (relation3 lenv term term) ≝ λR1,R2.
+ ∀L1,T1,T. R1 L1 T1 T → ∀L2. lpx_sn (λ_.R1) L1 L2 →
+ ∀T2. R2 L2 T T2 → R1 L1 T1 T2.
+
+(* Main properties **********************************************************)
+
+theorem lpx_sn_trans: ∀R. lpx_sn_transitive R R → Transitive … (lpx_sn (λ_.R)).
+#R #HR #L1 #L #H elim H -L1 -L //
+#I #L1 #L #V1 #V #HL1 #HV1 #IHL1 #X #H
+elim (lpx_sn_inv_pair1 … H) -H #L2 #V2 #HL2 #HV2 #H destruct /3 width=5 by lpx_sn_pair/
+qed-.
+
+theorem lpx_sn_conf: ∀R1,R2. lpx_sn_confluent R1 R2 →
+ confluent2 … (lpx_sn (λ_.R1)) (lpx_sn (λ_.R2)).
+#R1 #R2 #HR12 #L0 @(f_ind … length … L0) -L0 #n #IH *
+[ #_ #X1 #H1 #X2 #H2 -n
+ >(lpx_sn_inv_atom1 … H1) -X1
+ >(lpx_sn_inv_atom1 … H2) -X2 /2 width=3 by lpx_sn_atom, ex2_intro/
+| #L0 #I #V0 #Hn #X1 #H1 #X2 #H2 destruct
+ elim (lpx_sn_inv_pair1 … H1) -H1 #L1 #V1 #HL01 #HV01 #H destruct
+ elim (lpx_sn_inv_pair1 … H2) -H2 #L2 #V2 #HL02 #HV02 #H destruct
+ elim (IH … HL01 … HL02) -IH normalize // #L #HL1 #HL2
+ elim (HR12 … HV01 … HV02 … HL01 … HL02) -L0 -V0 /3 width=5 by lpx_sn_pair, ex2_intro/
+]
+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/lpx_sn.ma".
+
+(* SN POINTWISE EXTENSION OF A CONTEXT-SENSITIVE REALTION FOR TERMS *********)
+
+(* Properties on transitive_closure *****************************************)
+
+lemma TC_lpx_sn_pair_refl: ∀R. (∀I,L. reflexive … (R I L)) →
+ ∀L1,L2. TC … (lpx_sn R) L1 L2 →
+ ∀I,V. TC … (lpx_sn R) (L1.ⓑ{I}V) (L2. ⓑ{I}V).
+#R #HR #L1 #L2 #H @(TC_star_ind … L2 H) -L2
+[ /2 width=1 by lpx_sn_refl/
+| /3 width=1 by TC_reflexive, lpx_sn_refl/
+| /3 width=5 by lpx_sn_pair, step/
+]
+qed-.
+
+lemma TC_lpx_sn_pair: ∀R. (∀I,L. reflexive … (R I L)) →
+ ∀I,L1,L2. TC … (lpx_sn R) L1 L2 →
+ ∀V1,V2. LTC … (R I) L1 V1 V2 →
+ TC … (lpx_sn R) (L1.ⓑ{I}V1) (L2. ⓑ{I}V2).
+#R #HR #I #L1 #L2 #HL12 #V1 #V2 #H @(TC_star_ind_dx … V1 H) -V1 //
+[ /2 width=1 by TC_lpx_sn_pair_refl/
+| /4 width=3 by TC_strap, lpx_sn_pair, lpx_sn_refl/
+]
+qed-.
+
+lemma lpx_sn_LTC_TC_lpx_sn: ∀R. (∀I,L. reflexive … (R I L)) →
+ ∀L1,L2. lpx_sn (λI.LTC … (R I)) L1 L2 →
+ TC … (lpx_sn R) L1 L2.
+#R #HR #L1 #L2 #H elim H -L1 -L2
+/2 width=1 by TC_lpx_sn_pair, lpx_sn_atom, inj/
+qed-.
+
+(* Inversion lemmas on transitive closure ***********************************)
+
+lemma TC_lpx_sn_inv_atom2: ∀R,L1. TC … (lpx_sn R) L1 (⋆) → L1 = ⋆.
+#R #L1 #H @(TC_ind_dx … L1 H) -L1
+[ /2 width=2 by lpx_sn_inv_atom2/
+| #L1 #L #HL1 #_ #IHL2 destruct /2 width=2 by lpx_sn_inv_atom2/
+]
+qed-.
+
+lemma TC_lpx_sn_inv_pair2: ∀R. (∀I.s_rs_transitive … (R I) (λ_.lpx_sn R)) →
+ ∀I,L1,K2,V2. TC … (lpx_sn R) L1 (K2.ⓑ{I}V2) →
+ ∃∃K1,V1. TC … (lpx_sn R) K1 K2 & LTC … (R I) K1 V1 V2 & L1 = K1.ⓑ{I}V1.
+#R #HR #I #L1 #K2 #V2 #H @(TC_ind_dx … L1 H) -L1
+[ #L1 #H elim (lpx_sn_inv_pair2 … H) -H /3 width=5 by inj, ex3_2_intro/
+| #L1 #L #HL1 #_ * #K #V #HK2 #HV2 #H destruct
+ elim (lpx_sn_inv_pair2 … HL1) -HL1 #K1 #V1 #HK1 #HV1 #H destruct
+ lapply (HR … HV2 … HK1) -HR -HV2 /3 width=5 by TC_strap, ex3_2_intro/
+]
+qed-.
+
+lemma TC_lpx_sn_ind: ∀R. (∀I.s_rs_transitive … (R I) (λ_.lpx_sn R)) →
+ ∀S:relation lenv.
+ S (⋆) (⋆) → (
+ ∀I,K1,K2,V1,V2.
+ TC … (lpx_sn R) K1 K2 → LTC … (R I) K1 V1 V2 →
+ S K1 K2 → S (K1.ⓑ{I}V1) (K2.ⓑ{I}V2)
+ ) →
+ ∀L2,L1. TC … (lpx_sn R) L1 L2 → S L1 L2.
+#R #HR #S #IH1 #IH2 #L2 elim L2 -L2
+[ #X #H >(TC_lpx_sn_inv_atom2 … H) -X //
+| #L2 #I #V2 #IHL2 #X #H
+ elim (TC_lpx_sn_inv_pair2 … H) // -H -HR
+ #L1 #V1 #HL12 #HV12 #H destruct /3 width=1 by/
+]
+qed-.
+
+lemma TC_lpx_sn_inv_atom1: ∀R,L2. TC … (lpx_sn R) (⋆) L2 → L2 = ⋆.
+#R #L2 #H elim H -L2
+[ /2 width=2 by lpx_sn_inv_atom1/
+| #L #L2 #_ #HL2 #IHL1 destruct /2 width=2 by lpx_sn_inv_atom1/
+]
+qed-.
+
+fact TC_lpx_sn_inv_pair1_aux: ∀R. (∀I.s_rs_transitive … (R I) (λ_.lpx_sn R)) →
+ ∀L1,L2. TC … (lpx_sn R) L1 L2 →
+ ∀I,K1,V1. L1 = K1.ⓑ{I}V1 →
+ ∃∃K2,V2. TC … (lpx_sn R) K1 K2 & LTC … (R I) K1 V1 V2 & L2 = K2. ⓑ{I} V2.
+#R #HR #L1 #L2 #H @(TC_lpx_sn_ind … H) // -HR -L1 -L2
+[ #J #K #W #H destruct
+| #I #L1 #L2 #V1 #V2 #HL12 #HV12 #_ #J #K #W #H destruct /2 width=5 by ex3_2_intro/
+]
+qed-.
+
+lemma TC_lpx_sn_inv_pair1: ∀R. (∀I.s_rs_transitive … (R I) (λ_.lpx_sn R)) →
+ ∀I,K1,L2,V1. TC … (lpx_sn R) (K1.ⓑ{I}V1) L2 →
+ ∃∃K2,V2. TC … (lpx_sn R) K1 K2 & LTC … (R I) K1 V1 V2 & L2 = K2. ⓑ{I} V2.
+/2 width=3 by TC_lpx_sn_inv_pair1_aux/ qed-.
+
+lemma TC_lpx_sn_inv_lpx_sn_LTC: ∀R. (∀I.s_rs_transitive … (R I) (λ_.lpx_sn R)) →
+ ∀L1,L2. TC … (lpx_sn R) L1 L2 →
+ lpx_sn (λI.LTC … (R I)) L1 L2.
+/3 width=4 by TC_lpx_sn_ind, lpx_sn_pair/ qed-.
+
+(* Forward lemmas on transitive closure *************************************)
+
+lemma TC_lpx_sn_fwd_length: ∀R,L1,L2. TC … (lpx_sn R) L1 L2 → |L1| = |L2|.
+#R #L1 #L2 #H elim H -L2
+[ #L2 #HL12 >(lpx_sn_fwd_length … HL12) -HL12 //
+| #L #L2 #_ #HL2 #IHL1
+ >IHL1 -L1 >(lpx_sn_fwd_length … HL2) -HL2 //
+]
+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/llor.ma".
-include "basic_2/computation/cpxs_lleq.ma".
-include "basic_2/computation/lpxs_ldrop.ma".
-include "basic_2/computation/lpxs_cpxs.ma".
-include "basic_2/computation/lpxs_lpxs.ma".
-
-(* SN EXTENDED PARALLEL REDUCTION FOR LOCAL ENVIRONMENTS ********************)
-
-axiom llor_fwd_sort: ∀L1,L2,L,d,k. L1 ⩖ [⋆k, d] L2 ≡ L → L = L2.
-
-axiom llor_fwd_lref: ∀L1,L2,L,d,i. L1 ⩖ [#i, d] L2 ≡ L →
- ∨∨ (|L| ≤ i ∧ L = L2)
- | (yinj i < d ∧ L = L2)
- | ∃∃I1,I2,K1,K2,K,V1,V2. ⇩[i] L1 ≡ K1.ⓑ{I1}V1 &
- ⇩[i] L2 ≡ K2.ⓑ{I2}V2 &
- ⇩[i] L ≡ K.ⓑ{I2}V1 &
- L2 ≃[yinj 0, yinj i] L &
- K1 ⩖[V1, yinj 0] K2 ≡ K &
- d ≤ yinj i.
-
-
-axiom llor_fwd_lref_lt: ∀L1,L2,L,d,i. L1 ⩖ [#i, d] L2 ≡ L → i < d → L = L2.
-
-axiom llor_inv_lref_be: ∀L1,L2,L,d,i. L1 ⩖ [#i, d] L2 ≡ L → d ≤ i →
- ∀I1,I2,K1,K2,V1,V2. ⇩[i] L1 ≡ K1.ⓑ{I1}V1 → ⇩[i] L2 ≡ K2.ⓑ{I2}V2 →
- ∃∃K. ⇩[i] L ≡ K.ⓑ{I2}V1 & L2 ≃[0, i] L &
- K1 ⩖[V1, 0] K2 ≡ K.
-
-axiom llor_fwd_gref: ∀L1,L2,L,d,p. L1 ⩖ [§p, d] L2 ≡ L → L = L2.
-
-axiom llor_inv_bind: ∀a,I,L1,L2,L,V,T,d. L1 ⩖ [ⓑ{a,I}V.T, d] L2 ≡ L →
- ∃∃L0. L1 ⩖ [V, d] L2 ≡ L0 & L1.ⓑ{I}V ⩖ [T, ⫯d] L0.ⓑ{I}V ≡ L.ⓑ{I}V.
-
-axiom llor_inv_flat: ∀I,L1,L2,L,V,T,d. L1 ⩖ [ⓕ{I}V.T, d] L2 ≡ L →
- ∃∃L0. L1 ⩖ [V, d] L2 ≡ L0 & L1 ⩖ [T, d] L0 ≡ L.
-
-axiom llor_fwd_length_13: ∀L1,L2,L,T,d. L1 ⩖ [T, d] L2 ≡ L → |L1| = |L|.
-
-(* Properties obn lazy union for local environments *************************)
-
-lemma lpxs_llor_sn: ∀h,g,G,L1s,L0,L1d,T,d. L1s ⩖[T, d] L0 ≡ L1d →
- ∀L2s,L2d. L2s ⩖[T, d] L0 ≡ L2d →
- ⦃G, L1s⦄ ⊢ ➡*[h, g] L2s → ⦃G, L1d⦄ ⊢ ➡*[h, g] L2d.
-#h #g #G #L1s #L0 #L1d #T #d #H elim H -L1s -L0 -L1d -T -d
-[ #L1s #L0 #d #k #_ #L2s #L2d #H #_ >(llor_fwd_sort … H) //
-| #L1s #L0 #d #i #_ #Hid #L2s #L2d #H #_ >(llor_fwd_lref_lt … H) //
-| #I1s #I0 #L1s #L0 #L1d #K1s #K0 #K1d #V1s #V0 #d #i #Hdi #HLK1s #HLK0 #HLK1d #HL01d #HV1s #IHV1s #L2s #L2d #H #HL12s
- elim (lpxs_ldrop_conf … HLK1s … HL12s) -L1s #Y #H #HLK2s
- elim (lpxs_inv_pair1 … H) -H #K2s #V2s #HK12s #HV12s #H destruct
- elim (llor_inv_lref_be … H … HLK2s HLK0) // -L2s -HLK0 -Hdi #K2d #HLK2d #HL02d #HV2s
- lapply (leq_canc_sn … HL01d … HL02d) -L0 #HL12d
- lapply (IHV1s … K2d … HK12s) -IHV1s -HK12s [2: #HK12d
-
-
-
-
-[ #I2d #I1s #L2d #L1s #L2s #K2d #K1s #K2s #V2d #V1s #d #i #Hdi #HLK2d #HLK1s #HLK2s #HL12s #_ #IHV2s #L1d #HL1sd #HL12d
- elim (lpxs_ldrop_trans_O1 … HL12d … HLK2d) -L2d #Y #HLK1d #H
- elim (lpxs_inv_pair2 … H) -H #K1d #V1d #HK12d #HV12d #H destruct
- elim (lleq_inv_lref_ge … HL1sd … HLK1s HLK1d) // -d -I2d #H #HV1d destruct
- lapply (lleq_cpxs_conf_dx … HV12d … HV1d) #HV2d
- lapply (lleq_cpxs_trans … HV12d … HV1d) -HV12d -HV1d #HV12d
- lapply (IHV2s … HV2d HK12d) -L1d -K1d -K2d #HK12s
- elim (ldrop_lpxs_trans h g G … HLK1s (K2s.ⓑ{I1s}V2d)) /2 width=1 by lpxs_pair/ -V1d -K1s #Y #HL1sY #HYK2s #H
- lapply (leq_canc_sn … HL12s … H) -HL12s -H #HL2sY
- lapply (ldrop_O_inj … HLK2s HYK2s) -I1s -K2s -V2d #H
- lapply (leq_join … HL2sY … H) -HL2sY -H #HL2sY
- >(leq_inv_O_Y … HL2sY) -HL2sY //
-
-
-
-
-
-lemma lleq_lpxs_trans_llor: ∀h,g,G,L1s,L2s,L2d,T,d. L2d ⩖[T, d] L1s ≡ L2s →
- ∀L1d. L1s ⋕[T, d] L1d → ⦃G, L1d⦄ ⊢ ➡*[h, g] L2d → ⦃G, L1s⦄ ⊢ ➡*[h, g] L2s.
-#h #g #G #L1s #L2s #L2d #T #d #H elim H -L1s -L2s -L2d -T -d //
-[ #I2d #I1s #L2d #L1s #L2s #K2d #K1s #K2s #V2d #V1s #d #i #Hdi #HLK2d #HLK1s #HLK2s #HL12s #_ #IHV2s #L1d #HL1sd #HL12d
- elim (lpxs_ldrop_trans_O1 … HL12d … HLK2d) -L2d #Y #HLK1d #H
- elim (lpxs_inv_pair2 … H) -H #K1d #V1d #HK12d #HV12d #H destruct
- elim (lleq_inv_lref_ge … HL1sd … HLK1s HLK1d) // -d -I2d #H #HV1d destruct
- lapply (lleq_cpxs_conf_dx … HV12d … HV1d) #HV2d
- lapply (lleq_cpxs_trans … HV12d … HV1d) -HV12d -HV1d #HV12d
- lapply (IHV2s … HV2d HK12d) -L1d -K1d -K2d #HK12s
- elim (ldrop_lpxs_trans h g G … HLK1s (K2s.ⓑ{I1s}V2d)) /2 width=1 by lpxs_pair/ -V1d -K1s #Y #HL1sY #HYK2s #H
- lapply (leq_canc_sn … HL12s … H) -HL12s -H #HL2sY
- lapply (ldrop_O_inj … HLK2s HYK2s) -I1s -K2s -V2d #H
- lapply (leq_join … HL2sY … H) -HL2sY -H #HL2sY
- >(leq_inv_O_Y … HL2sY) -HL2sY //
-(*
-| #a #I #L2d #L1s #L0 #L2s #V #T #d #H0 #_ #IHV #IHT #L1d #H #HL12d
- elim (lleq_inv_bind … H) -H #HV #HT
-*)
-| #I #L2d #L1s #LV #LT #L2s #V #T #d #H0 #_ #_ #IHV #IHT #IH #L1d #H #HL12d
- elim (lleq_inv_flat … H) -H #HV #HT
- lapply (IHV … HV HL12d) -HV #H1
- lapply (IHT … HT HL12d) #H2
-
-
-
- @(lpxs_trans … LV) /2 width=3 by/ -IHV
- lapply (IHT … HL12d) // -IHT #H @(IH … H) -IH -H
-
- @(IH … HL12d) -IHT -IHV
-
- /4 width=5 by lpxs_trans/
-
-
-lemma lleq_lpx_conf_llor: ∀h,g,G,L1,L2,T,d. L1 ⋕[T, d] L2 → ∀K1. ⦃G, L1⦄ ⊢ ➡[h, g] K1 →
- ∀K2. K1 ⩖[T, d] L2 ≡ K2 → ⦃G, L2⦄ ⊢ ➡[h, g] K2.
-#h #g #G #L1 #L2 #T #d #H @(lleq_ind_alt … H) -L1 -L2 -T -d
-[ #L1 #L2 #d #k #HL12 #K1 #HLK1 #K2 #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/substitution/llpx_sn_ldrop.ma".
+include "basic_2/static/ssta.ma".
+
+(* STRATIFIED STATIC TYPE ASSIGNMENT FOR TERMS ******************************)
+
+(* Properties on lazy sn pointwise extensions *******************************)
+
+lemma ssta_llpx_sn_conf: ∀R. (∀I,L.reflexive … (R I L)) →
+ (∀I.l_liftable (R I)) →
+ ∀h,g,G. s_r_confluent1 … (ssta h g G) (llpx_sn R 0).
+#R #H1R #H2R #h #g #G #Ls #T1 #T2 #H elim H -G -Ls -T1 -T2
+[ /3 width=4 by llpx_sn_fwd_length, llpx_sn_sort/
+| #G #Ls #Ks #V1s #W2s #V2s #i #HLKs #_ #HVW2s #IHV12s #Ld #H elim (llpx_sn_inv_lref_ge_sn … H … HLKs) // -H
+ #Kd #V1d #HLKd #HV1s #HV1sd
+ lapply (ldrop_fwd_drop2 … HLKs) -HLKs #HLKs
+ lapply (ldrop_fwd_drop2 … HLKd) -HLKd #HLKd
+ @(llpx_sn_lift_le … HLKs HLKd … HVW2s) -HLKs -HLKd -HVW2s /2 width=1 by/ (**) (* full auto too slow *)
+| #G #Ls #Ks #V1s #W1s #l #i #HLKs #Hl #HVW1s #Ld #H elim (llpx_sn_inv_lref_ge_sn … H … HLKs) // -H
+ #Kd #V1d #HLKd #HV1s #HV1sd
+ lapply (ldrop_fwd_drop2 … HLKs) -HLKs #HLKs
+ lapply (ldrop_fwd_drop2 … HLKd) -HLKd #HLKd
+ @(llpx_sn_lift_le … HLKs HLKd … HVW1s) -HLKs -HLKd -HVW1s /2 width=1 by/ (**) (* full auto too slow *)
+| #a #I #G #Ls #V #T1 #T2 #_ #IHT12 #Ld #H elim (llpx_sn_inv_bind_O … H) -H
+ /4 width=5 by llpx_sn_bind_repl_SO, llpx_sn_bind/
+| #G #Ls #V #T1 #T2 #_ #IHT12 #Ld #H elim (llpx_sn_inv_flat … H) -H
+ /3 width=1 by llpx_sn_flat/
+| #G #Ls #V #T1 #T2 #_ #IHT12 #Ld #H elim (llpx_sn_inv_flat … H) -H
+ /3 width=1 by llpx_sn_flat/
+]
+qed-.
(* Properties on lazy sn pointwise extensions *******************************)
-lemma cpr_llpx_sn_conf: ∀R. (∀I,L.reflexive … (R I L)) →
- (∀I.l_liftable (R I)) →
- (∀I.l_deliftable_sn (R I)) →
+lemma cpr_llpx_sn_conf: ∀R. (∀L. reflexive … (R L)) → l_liftable R → l_deliftable_sn R →
∀G. s_r_confluent1 … (cpr G) (llpx_sn R 0).
#R #H1R #H2R #H3R #G #Ls #T1 #T2 #H elim H -G -Ls -T1 -T2
[ //
(* Properties on lazy sn pointwise extensions *******************************)
(* Note: lemma 1000 *)
-lemma cpx_llpx_sn_conf: ∀R. (∀I,L.reflexive … (R I L)) →
- (∀I.l_liftable (R I)) →
- (∀I.l_deliftable_sn (R I)) →
+lemma cpx_llpx_sn_conf: ∀R. (∀L. reflexive … (R L)) → l_liftable R → l_deliftable_sn R →
∀h,g,G. s_r_confluent1 … (cpx h g G) (llpx_sn R 0).
#R #H1R #H2R #H3R #h #g #G #Ls #T1 #T2 #H elim H -G -Ls -T1 -T2
[ //
(* SN PARALLEL REDUCTION FOR LOCAL ENVIRONMENTS *****************************)
-definition lpr: relation3 genv lenv lenv ≝ λG. lpx_sn (λ_.cpr G).
+definition lpr: relation3 genv lenv lenv ≝ λG. lpx_sn (cpr G).
interpretation "parallel reduction (local environment, sn variant)"
'PRedSn G L1 L2 = (lpr G L1 L2).
(* SN EXTENDED PARALLEL REDUCTION FOR LOCAL ENVIRONMENTS ********************)
definition lpx: ∀h. sd h → relation3 genv lenv lenv ≝
- λh,g,G. lpx_sn (λ_.cpx h g G).
+ λh,g,G. lpx_sn (cpx h g G).
interpretation "extended parallel reduction (local environment, sn variant)"
'PRedSn h g G L1 L2 = (lpx h g G L1 L2).
(* SN POINTWISE EXTENSION OF A CONTEXT-SENSITIVE REALTION FOR TERMS *********)
-inductive lpx_sn (R:relation4 bind2 lenv term term): relation lenv ≝
+inductive lpx_sn (R:relation3 lenv term term): relation lenv ≝
| lpx_sn_atom: lpx_sn R (⋆) (⋆)
| lpx_sn_pair: ∀I,K1,K2,V1,V2.
- lpx_sn R K1 K2 → R I K1 V1 V2 →
- lpx_sn R (K1.ⓑ{I}V1) (K2.ⓑ{I}V2)
+ lpx_sn R K1 K2 → R K1 V1 V2 →
+ lpx_sn R (K1. ⓑ{I} V1) (K2. ⓑ{I} V2)
.
(* Basic properties *********************************************************)
-lemma lpx_sn_refl: ∀R. (∀I,L. reflexive ? (R I L)) → reflexive … (lpx_sn R).
+lemma lpx_sn_refl: ∀R. (∀L. reflexive ? (R L)) → reflexive … (lpx_sn R).
#R #HR #L elim L -L /2 width=1 by lpx_sn_atom, lpx_sn_pair/
qed-.
lemma lpx_sn_inv_atom1: ∀R,L2. lpx_sn R (⋆) L2 → L2 = ⋆.
/2 width=4 by lpx_sn_inv_atom1_aux/ qed-.
-fact lpx_sn_inv_pair1_aux: ∀R,L1,L2. lpx_sn R L1 L2 → ∀I,K1,V1. L1 = K1.ⓑ{I}V1 →
- ∃∃K2,V2. lpx_sn R K1 K2 & R I K1 V1 V2 & L2 = K2.ⓑ{I}V2.
+fact lpx_sn_inv_pair1_aux: ∀R,L1,L2. lpx_sn R L1 L2 → ∀I,K1,V1. L1 = K1. ⓑ{I} V1 →
+ ∃∃K2,V2. lpx_sn R K1 K2 & R K1 V1 V2 & L2 = K2. ⓑ{I} V2.
#R #L1 #L2 * -L1 -L2
[ #J #K1 #V1 #H destruct
| #I #K1 #K2 #V1 #V2 #HK12 #HV12 #J #L #W #H destruct /2 width=5 by ex3_2_intro/
]
qed-.
-lemma lpx_sn_inv_pair1: ∀R,I,K1,V1,L2. lpx_sn R (K1.ⓑ{I}V1) L2 →
- ∃∃K2,V2. lpx_sn R K1 K2 & R I K1 V1 V2 & L2 = K2.ⓑ{I}V2.
+lemma lpx_sn_inv_pair1: ∀R,I,K1,V1,L2. lpx_sn R (K1. ⓑ{I} V1) L2 →
+ ∃∃K2,V2. lpx_sn R K1 K2 & R K1 V1 V2 & L2 = K2. ⓑ{I} V2.
/2 width=3 by lpx_sn_inv_pair1_aux/ qed-.
fact lpx_sn_inv_atom2_aux: ∀R,L1,L2. lpx_sn R L1 L2 → L2 = ⋆ → L1 = ⋆.
lemma lpx_sn_inv_atom2: ∀R,L1. lpx_sn R L1 (⋆) → L1 = ⋆.
/2 width=4 by lpx_sn_inv_atom2_aux/ qed-.
-fact lpx_sn_inv_pair2_aux: ∀R,L1,L2. lpx_sn R L1 L2 → ∀I,K2,V2. L2 = K2.ⓑ{I}V2 →
- ∃∃K1,V1. lpx_sn R K1 K2 & R I K1 V1 V2 & L1 = K1.ⓑ{I}V1.
+fact lpx_sn_inv_pair2_aux: ∀R,L1,L2. lpx_sn R L1 L2 → ∀I,K2,V2. L2 = K2. ⓑ{I} V2 →
+ ∃∃K1,V1. lpx_sn R K1 K2 & R K1 V1 V2 & L1 = K1. ⓑ{I} V1.
#R #L1 #L2 * -L1 -L2
[ #J #K2 #V2 #H destruct
| #I #K1 #K2 #V1 #V2 #HK12 #HV12 #J #K #W #H destruct /2 width=5 by ex3_2_intro/
]
qed-.
-lemma lpx_sn_inv_pair2: ∀R,I,L1,K2,V2. lpx_sn R L1 (K2.ⓑ{I}V2) →
- ∃∃K1,V1. lpx_sn R K1 K2 & R I K1 V1 V2 & L1 = K1.ⓑ{I}V1.
+lemma lpx_sn_inv_pair2: ∀R,I,L1,K2,V2. lpx_sn R L1 (K2. ⓑ{I} V2) →
+ ∃∃K1,V1. lpx_sn R K1 K2 & R K1 V1 V2 & L1 = K1. ⓑ{I} V1.
/2 width=3 by lpx_sn_inv_pair2_aux/ qed-.
lemma lpx_sn_inv_pair: ∀R,I1,I2,L1,L2,V1,V2.
lpx_sn R (L1.ⓑ{I1}V1) (L2.ⓑ{I2}V2) →
- ∧∧ lpx_sn R L1 L2 & R I1 L1 V1 V2 & I1 = I2.
+ ∧∧ lpx_sn R L1 L2 & R L1 V1 V2 & I1 = I2.
#R #I1 #I2 #L1 #L2 #V1 #V2 #H elim (lpx_sn_inv_pair1 … H) -H
#L0 #V0 #HL10 #HV10 #H destruct /2 width=1 by and3_intro/
qed-.
(* SN POINTWISE EXTENSION OF A CONTEXT-SENSITIVE REALTION FOR TERMS *********)
(* alternative definition of lpx_sn *)
-definition lpx_sn_alt: relation4 bind2 lenv term term → relation lenv ≝
+definition lpx_sn_alt: relation3 lenv term term → relation lenv ≝
λR,L1,L2. |L1| = |L2| ∧
(∀I1,I2,K1,K2,V1,V2,i.
⇩[i] L1 ≡ K1.ⓑ{I1}V1 → ⇩[i] L2 ≡ K2.ⓑ{I2}V2 →
- I1 = I2 ∧ R I1 K1 V1 V2
+ I1 = I2 ∧ R K1 V1 V2
).
(* Basic forward lemmas ******************************************************)
qed-.
lemma lpx_sn_alt_inv_pair1: ∀R,I,L2,K1,V1. lpx_sn_alt R (K1.ⓑ{I}V1) L2 →
- ∃∃K2,V2. lpx_sn_alt R K1 K2 & R I K1 V1 V2 & L2 = K2.ⓑ{I}V2.
+ ∃∃K2,V2. lpx_sn_alt R K1 K2 & R K1 V1 V2 & L2 = K2.ⓑ{I}V2.
#R #I1 #L2 #K1 #V1 #H elim H -H
#H #IH elim (length_inv_pos_sn … H) -H
#I2 #K2 #V2 #HK12 #H destruct
qed-.
lemma lpx_sn_alt_inv_pair2: ∀R,I,L1,K2,V2. lpx_sn_alt R L1 (K2.ⓑ{I}V2) →
- ∃∃K1,V1. lpx_sn_alt R K1 K2 & R I K1 V1 V2 & L1 = K1.ⓑ{I}V1.
+ ∃∃K1,V1. lpx_sn_alt R K1 K2 & R K1 V1 V2 & L1 = K1.ⓑ{I}V1.
#R #I2 #L1 #K2 #V2 #H elim H -H
#H #IH elim (length_inv_pos_dx … H) -H
#I1 #K1 #V1 #HK12 #H destruct
qed.
lemma lpx_sn_alt_pair: ∀R,I,L1,L2,V1,V2.
- lpx_sn_alt R L1 L2 → R I L1 V1 V2 →
+ lpx_sn_alt R L1 L2 → R L1 V1 V2 →
lpx_sn_alt R (L1.ⓑ{I}V1) (L2.ⓑ{I}V2).
#R #I #L1 #L2 #V1 #V2 #H #HV12 elim H -H
#HL12 #IH @conj normalize //
lemma lpx_sn_intro_alt: ∀R,L1,L2. |L1| = |L2| →
(∀I1,I2,K1,K2,V1,V2,i.
⇩[i] L1 ≡ K1.ⓑ{I1}V1 → ⇩[i] L2 ≡ K2.ⓑ{I2}V2 →
- I1 = I2 ∧ R I1 K1 V1 V2
+ I1 = I2 ∧ R K1 V1 V2
) → lpx_sn R L1 L2.
/4 width=4 by lpx_sn_alt_inv_lpx_sn, conj/ qed.
|L1| = |L2| ∧
∀I1,I2,K1,K2,V1,V2,i.
⇩[i] L1 ≡ K1.ⓑ{I1}V1 → ⇩[i] L2 ≡ K2.ⓑ{I2}V2 →
- I1 = I2 ∧ R I1 K1 V1 V2.
+ I1 = I2 ∧ R K1 V1 V2.
#R #L1 #L2 #H lapply (lpx_sn_lpx_sn_alt … H) -H
#H elim H -H /3 width=4 by conj/
qed-.
lemma lpx_sn_ldrop_conf: ∀R,L1,L2. lpx_sn R L1 L2 →
∀I,K1,V1,i. ⇩[i] L1 ≡ K1.ⓑ{I}V1 →
- ∃∃K2,V2. ⇩[i] L2 ≡ K2.ⓑ{I}V2 & lpx_sn R K1 K2 & R I K1 V1 V2.
+ ∃∃K2,V2. ⇩[i] L2 ≡ K2.ⓑ{I}V2 & lpx_sn R K1 K2 & R K1 V1 V2.
#R #L1 #L2 #H elim H -L1 -L2
[ #I0 #K0 #V0 #i #H elim (ldrop_inv_atom1 … H) -H #H destruct
| #I #K1 #K2 #V1 #V2 #HK12 #HV12 #IHK12 #I0 #K0 #V0 #i #H elim (ldrop_inv_O1_pair1 … H) * -H
lemma lpx_sn_ldrop_trans: ∀R,L1,L2. lpx_sn R L1 L2 →
∀I,K2,V2,i. ⇩[i] L2 ≡ K2.ⓑ{I}V2 →
- ∃∃K1,V1. ⇩[i] L1 ≡ K1.ⓑ{I}V1 & lpx_sn R K1 K2 & R I K1 V1 V2.
+ ∃∃K1,V1. ⇩[i] L1 ≡ K1.ⓑ{I}V1 & lpx_sn R K1 K2 & R K1 V1 V2.
#R #L1 #L2 #H elim H -L1 -L2
[ #I0 #K0 #V0 #i #H elim (ldrop_inv_atom1 … H) -H #H destruct
| #I #K1 #K2 #V1 #V2 #HK12 #HV12 #IHK12 #I0 #K0 #V0 #i #H elim (ldrop_inv_O1_pair1 … H) * -H
]
qed-.
-lemma lpx_sn_deliftable_dropable: ∀R. (∀I. l_deliftable_sn (R I)) → dropable_sn (lpx_sn R).
+lemma lpx_sn_deliftable_dropable: ∀R. l_deliftable_sn R → dropable_sn (lpx_sn R).
#R #HR #L1 #K1 #s #d #e #H elim H -L1 -K1 -d -e
[ #d #e #He #X #H >(lpx_sn_inv_atom1 … H) -H
/4 width=3 by ldrop_atom, lpx_sn_atom, ex2_intro/
]
qed-.
-lemma lpx_sn_liftable_dedropable: ∀R. (∀I,L. reflexive ? (R I L)) →
- (∀I. l_liftable (R I)) → dedropable_sn (lpx_sn R).
+lemma lpx_sn_liftable_dedropable: ∀R. (∀L. reflexive ? (R L)) →
+ l_liftable R → dedropable_sn (lpx_sn R).
#R #H1R #H2R #L1 #K1 #s #d #e #H elim H -L1 -K1 -d -e
[ #d #e #He #X #H >(lpx_sn_inv_atom1 … H) -H
/4 width=4 by ldrop_atom, lpx_sn_atom, ex3_intro/
definition lpx_sn_confluent: relation (relation3 lenv term term) ≝ λR1,R2.
∀L0,T0,T1. R1 L0 T0 T1 → ∀T2. R2 L0 T0 T2 →
- ∀L1. lpx_sn (λ_.R1) L0 L1 → ∀L2. lpx_sn (λ_.R2) L0 L2 →
+ ∀L1. lpx_sn R1 L0 L1 → ∀L2. lpx_sn R2 L0 L2 →
∃∃T. R2 L1 T1 T & R1 L2 T2 T.
definition lpx_sn_transitive: relation (relation3 lenv term term) ≝ λR1,R2.
- ∀L1,T1,T. R1 L1 T1 T → ∀L2. lpx_sn (λ_.R1) L1 L2 →
+ ∀L1,T1,T. R1 L1 T1 T → ∀L2. lpx_sn R1 L1 L2 →
∀T2. R2 L2 T T2 → R1 L1 T1 T2.
(* Main properties **********************************************************)
-theorem lpx_sn_trans: ∀R. lpx_sn_transitive R R → Transitive … (lpx_sn (λ_.R)).
+theorem lpx_sn_trans: ∀R. lpx_sn_transitive R R → Transitive … (lpx_sn R).
#R #HR #L1 #L #H elim H -L1 -L //
#I #L1 #L #V1 #V #HL1 #HV1 #IHL1 #X #H
elim (lpx_sn_inv_pair1 … H) -H #L2 #V2 #HL2 #HV2 #H destruct /3 width=5 by lpx_sn_pair/
qed-.
theorem lpx_sn_conf: ∀R1,R2. lpx_sn_confluent R1 R2 →
- confluent2 … (lpx_sn (λ_.R1)) (lpx_sn (λ_.R2)).
+ confluent2 … (lpx_sn R1) (lpx_sn R2).
#R1 #R2 #HR12 #L0 @(f_ind … length … L0) -L0 #n #IH *
[ #_ #X1 #H1 #X2 #H2 -n
>(lpx_sn_inv_atom1 … H1) -X1
(* Properties on transitive_closure *****************************************)
-lemma TC_lpx_sn_pair_refl: ∀R. (∀I,L. reflexive … (R I L)) →
+lemma TC_lpx_sn_pair_refl: ∀R. (∀L. reflexive … (R L)) →
∀L1,L2. TC … (lpx_sn R) L1 L2 →
- ∀I,V. TC … (lpx_sn R) (L1.ⓑ{I}V) (L2. ⓑ{I}V).
+ ∀I,V. TC … (lpx_sn R) (L1. ⓑ{I} V) (L2. ⓑ{I} V).
#R #HR #L1 #L2 #H @(TC_star_ind … L2 H) -L2
[ /2 width=1 by lpx_sn_refl/
| /3 width=1 by TC_reflexive, lpx_sn_refl/
]
qed-.
-lemma TC_lpx_sn_pair: ∀R. (∀I,L. reflexive … (R I L)) →
+lemma TC_lpx_sn_pair: ∀R. (∀L. reflexive … (R L)) →
∀I,L1,L2. TC … (lpx_sn R) L1 L2 →
- ∀V1,V2. LTC … (R I) L1 V1 V2 →
- TC … (lpx_sn R) (L1.ⓑ{I}V1) (L2. ⓑ{I}V2).
+ ∀V1,V2. LTC … R L1 V1 V2 →
+ TC … (lpx_sn R) (L1. ⓑ{I} V1) (L2. ⓑ{I} V2).
#R #HR #I #L1 #L2 #HL12 #V1 #V2 #H @(TC_star_ind_dx … V1 H) -V1 //
[ /2 width=1 by TC_lpx_sn_pair_refl/
| /4 width=3 by TC_strap, lpx_sn_pair, lpx_sn_refl/
]
qed-.
-lemma lpx_sn_LTC_TC_lpx_sn: ∀R. (∀I,L. reflexive … (R I L)) →
- ∀L1,L2. lpx_sn (λI.LTC … (R I)) L1 L2 →
+lemma lpx_sn_LTC_TC_lpx_sn: ∀R. (∀L. reflexive … (R L)) →
+ ∀L1,L2. lpx_sn (LTC … R) L1 L2 →
TC … (lpx_sn R) L1 L2.
#R #HR #L1 #L2 #H elim H -L1 -L2
/2 width=1 by TC_lpx_sn_pair, lpx_sn_atom, inj/
]
qed-.
-lemma TC_lpx_sn_inv_pair2: ∀R. (∀I.s_rs_transitive … (R I) (λ_.lpx_sn R)) →
+lemma TC_lpx_sn_inv_pair2: ∀R. s_rs_transitive … R (λ_. lpx_sn R) →
∀I,L1,K2,V2. TC … (lpx_sn R) L1 (K2.ⓑ{I}V2) →
- ∃∃K1,V1. TC … (lpx_sn R) K1 K2 & LTC … (R I) K1 V1 V2 & L1 = K1.ⓑ{I}V1.
+ ∃∃K1,V1. TC … (lpx_sn R) K1 K2 & LTC … R K1 V1 V2 & L1 = K1. ⓑ{I} V1.
#R #HR #I #L1 #K2 #V2 #H @(TC_ind_dx … L1 H) -L1
[ #L1 #H elim (lpx_sn_inv_pair2 … H) -H /3 width=5 by inj, ex3_2_intro/
| #L1 #L #HL1 #_ * #K #V #HK2 #HV2 #H destruct
]
qed-.
-lemma TC_lpx_sn_ind: ∀R. (∀I.s_rs_transitive … (R I) (λ_.lpx_sn R)) →
+lemma TC_lpx_sn_ind: ∀R. s_rs_transitive … R (λ_. lpx_sn R) →
∀S:relation lenv.
S (⋆) (⋆) → (
∀I,K1,K2,V1,V2.
- TC … (lpx_sn R) K1 K2 → LTC … (R I) K1 V1 V2 →
+ TC … (lpx_sn R) K1 K2 → LTC … R K1 V1 V2 →
S K1 K2 → S (K1.ⓑ{I}V1) (K2.ⓑ{I}V2)
) →
∀L2,L1. TC … (lpx_sn R) L1 L2 → S L1 L2.
]
qed-.
-fact TC_lpx_sn_inv_pair1_aux: ∀R. (∀I.s_rs_transitive … (R I) (λ_.lpx_sn R)) →
+fact TC_lpx_sn_inv_pair1_aux: ∀R. s_rs_transitive … R (λ_. lpx_sn R) →
∀L1,L2. TC … (lpx_sn R) L1 L2 →
∀I,K1,V1. L1 = K1.ⓑ{I}V1 →
- ∃∃K2,V2. TC … (lpx_sn R) K1 K2 & LTC … (R I) K1 V1 V2 & L2 = K2. ⓑ{I} V2.
+ ∃∃K2,V2. TC … (lpx_sn R) K1 K2 & LTC … R K1 V1 V2 & L2 = K2. ⓑ{I} V2.
#R #HR #L1 #L2 #H @(TC_lpx_sn_ind … H) // -HR -L1 -L2
[ #J #K #W #H destruct
| #I #L1 #L2 #V1 #V2 #HL12 #HV12 #_ #J #K #W #H destruct /2 width=5 by ex3_2_intro/
]
qed-.
-lemma TC_lpx_sn_inv_pair1: ∀R. (∀I.s_rs_transitive … (R I) (λ_.lpx_sn R)) →
+lemma TC_lpx_sn_inv_pair1: ∀R. s_rs_transitive … R (λ_. lpx_sn R) →
∀I,K1,L2,V1. TC … (lpx_sn R) (K1.ⓑ{I}V1) L2 →
- ∃∃K2,V2. TC … (lpx_sn R) K1 K2 & LTC … (R I) K1 V1 V2 & L2 = K2. ⓑ{I} V2.
+ ∃∃K2,V2. TC … (lpx_sn R) K1 K2 & LTC … R K1 V1 V2 & L2 = K2. ⓑ{I} V2.
/2 width=3 by TC_lpx_sn_inv_pair1_aux/ qed-.
-lemma TC_lpx_sn_inv_lpx_sn_LTC: ∀R. (∀I.s_rs_transitive … (R I) (λ_.lpx_sn R)) →
+lemma TC_lpx_sn_inv_lpx_sn_LTC: ∀R. s_rs_transitive … R (λ_. lpx_sn R) →
∀L1,L2. TC … (lpx_sn R) L1 L2 →
- lpx_sn (λI.LTC … (R I)) L1 L2.
+ lpx_sn (LTC … R) L1 L2.
/3 width=4 by TC_lpx_sn_ind, lpx_sn_pair/ qed-.
(* Forward lemmas on transitive closure *************************************)
(* Properties on lazy sn pointwise extensions *******************************)
-lemma ssta_llpx_sn_conf: ∀R. (∀I,L.reflexive … (R I L)) →
- (∀I.l_liftable (R I)) →
+lemma ssta_llpx_sn_conf: ∀R. (∀L. reflexive … (R L)) → l_liftable R →
∀h,g,G. s_r_confluent1 … (ssta h g G) (llpx_sn R 0).
#R #H1R #H2R #h #g #G #Ls #T1 #T2 #H elim H -G -Ls -T1 -T2
[ /3 width=4 by llpx_sn_fwd_length, llpx_sn_sort/
(* LAZY EQUIVALENCE FOR LOCAL ENVIRONMENTS **********************************)
-definition ceq: relation4 bind2 lenv term term ≝ λI,L,T1,T2. T1 = T2.
+definition ceq: relation3 lenv term term ≝ λL,T1,T2. T1 = T2.
definition lleq: relation4 ynat term lenv lenv ≝ llpx_sn ceq.
"lazy equivalence (local environment)"
'LazyEq T d L1 L2 = (lleq d T L1 L2).
-definition lleq_transitive: predicate (relation4 bind2 lenv term term) ≝
- λR. ∀I,L2,T1,T2. R I L2 T1 T2 → ∀L1. L1 ≡[T1, 0] L2 → R I L1 T1 T2.
+definition lleq_transitive: predicate (relation3 lenv term term) ≝
+ λR. ∀L2,T1,T2. R L2 T1 T2 → ∀L1. L1 ≡[T1, 0] L2 → R L1 T1 T2.
(* Basic inversion lemmas ***************************************************)
(* Advancded properties on lazy pointwise exyensions ************************)
-lemma llpx_sn_lrefl: ∀R. (∀I,L. reflexive … (R I L)) →
+lemma llpx_sn_lrefl: ∀R. (∀L. reflexive … (R L)) →
∀L1,L2,T,d. L1 ≡[T, d] L2 → llpx_sn R d T L1 L2.
/2 width=3 by llpx_sn_co/ 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/lazyor_4.ma".
+include "basic_2/relocation/lpx_sn.ma".
+include "basic_2/substitution/cofrees.ma".
+
+(* POINTWISE UNION FOR LOCAL ENVIRONMENTS ***********************************)
+
+inductive clor (T) (L2) (K1) (V1): predicate term ≝
+| clor_sn: |K1| < |L2| → K1 ⊢ |L2|-|K1|-1 ~ϵ 𝐅*[yinj 0]⦃T⦄ → clor T L2 K1 V1 V1
+| clor_dx: ∀I,K2,V2. |K1| < |L2| → (K1 ⊢ |L2|-|K1|-1 ~ϵ 𝐅*[yinj 0]⦃T⦄ → ⊥) →
+ ⇩[|L2|-|K1|-1] L2 ≡ K2.ⓑ{I}V2 → clor T L2 K1 V1 V2
+.
+
+definition llor: relation4 term lenv lenv lenv ≝
+ λT,L2. lpx_sn (clor T L2).
+
+interpretation
+ "lazy union (local environment)"
+ 'LazyOr L1 T L2 L = (llor T L2 L1 L).
+
+(* Basic properties *********************************************************)
+
+lemma llor_pair_sn: ∀I,L1,L2,L,V,T. L1 ⩖[T] L2 ≡ L →
+ |L1| < |L2| → L1 ⊢ |L2|-|L1|-1 ~ϵ 𝐅*[yinj 0]⦃T⦄ →
+ L1.ⓑ{I}V ⩖[T] L2 ≡ L.ⓑ{I}V.
+/3 width=2 by clor_sn, lpx_sn_pair/ qed.
+
+lemma llor_pair_dx: ∀I,J,L1,L2,L,K2,V1,V2,T. L1 ⩖[T] L2 ≡ L →
+ |L1| < |L2| → (L1 ⊢ |L2|-|L1|-1 ~ϵ 𝐅*[yinj 0]⦃T⦄ → ⊥) →
+ ⇩[|L2|-|L1|-1] L2 ≡ K2.ⓑ{J}V2 →
+ L1.ⓑ{I}V1 ⩖[T] L2 ≡ L.ⓑ{I}V2.
+/4 width=3 by clor_dx, lpx_sn_pair/ qed.
+
+lemma llor_total: ∀T,L2,L1. |L1| ≤ |L2| → ∃L. L1 ⩖[T] L2 ≡ L.
+#T #L2 #L1 elim L1 -L1 /2 width=2 by ex_intro/
+#L1 #I1 #V1 #IHL1 normalize
+#H elim IHL1 -IHL1 /2 width=3 by transitive_le/
+#L #HT elim (cofrees_dec L1 T 0 (|L2|-|L1|-1))
+[ /3 width=2 by llor_pair_sn, ex_intro/
+| elim (ldrop_O1_lt (Ⓕ) L2 (|L2|-|L1|-1))
+ /5 width=4 by llor_pair_dx, monotonic_lt_minus_l, ex_intro/
+]
+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/lpx_sn_alt.ma".
+include "basic_2/substitution/llor.ma".
+
+(* POINTWISE UNION FOR LOCAL ENVIRONMENTS ***********************************)
+
+(* Alternative definition ***************************************************)
+
+theorem llor_intro_alt: ∀T,L2,L1,L. |L1| ≤ |L2| → |L1| = |L| →
+ (∀I1,I,K1,K,V1,V,i. ⇩[i] L1 ≡ K1.ⓑ{I1}V1 → ⇩[i] L ≡ K.ⓑ{I}V →
+ (K1 ⊢ |L2|-|L1|+i ~ϵ 𝐅*[yinj 0]⦃T⦄ → I1 = I ∧ V1 = V) ∧
+ (∀I2,K2,V2. (K1 ⊢ |L2|-|L1|+i ~ϵ 𝐅*[yinj 0]⦃T⦄ → ⊥) →
+ ⇩[|L2|-|L1|+i] L2 ≡ K2.ⓑ{I2}V2 → I1 = I ∧ V2 = V
+ )
+ ) → L1 ⩖[T] L2 ≡ L.
+#T #L2 #L1 #L #HL12 #HL1 #IH @lpx_sn_intro_alt // -HL1
+#I1 #I #K1 #K #V1 #V #i #HLK1 #HLK
+lapply (ldrop_fwd_length_minus4 … HLK1)
+lapply (ldrop_fwd_length_le4 … HLK1)
+normalize in ⊢ (%→%→?); #HKL1 #Hi
+lapply (plus_minus_minus_be_aux … HL12 Hi) // -Hi <minus_plus #Hi
+lapply (transitive_le … HKL1 HL12) -HKL1 -HL12 #HKL1
+elim (IH … HLK1 HLK) -IH -HLK1 -HLK #IH1 #IH2
+elim (cofrees_dec K1 T 0 (|L2|-|L1|+i))
+[ -IH2 #HT elim (IH1 … HT) -IH1
+ #HI1 #HV1 @conj // <HV1 -V @clor_sn // <Hi -Hi //
+| -IH1 #HnT elim (ldrop_O1_lt (Ⓕ) L2 (|L2|-|L1|+i)) /2 width=1 by monotonic_lt_minus_l/
+ #I2 #K2 #V2 #HLK2 elim (IH2 … HLK2) -IH2 /2 width=1 by/
+ #HI1 #HV2 @conj // <HV2 -V @(clor_dx … I2 K2) // <Hi -Hi /2 width=1 by/
+]
+qed.
+
+theorem llor_inv_alt: ∀T,L2,L1,L. L1 ⩖[T] L2 ≡ L → |L1| ≤ |L2| →
+ |L1| = |L| ∧
+ (∀I1,I,K1,K,V1,V,i.
+ ⇩[i] L1 ≡ K1.ⓑ{I1}V1 → ⇩[i] L ≡ K.ⓑ{I}V →
+ (∧∧ K1 ⊢ |L2|-|L1|+i ~ϵ 𝐅*[yinj 0]⦃T⦄ & I1 = I & V1 = V) ∨
+ (∃∃I2,K2,V2. (K1 ⊢ |L2|-|L1|+i ~ϵ 𝐅*[yinj 0]⦃T⦄ → ⊥) &
+ ⇩[|L2|-|L1|+i] L2 ≡ K2.ⓑ{I2}V2 &
+ I1 = I & V2 = V
+ )
+ ).
+#T #L2 #L1 #L #H #HL12 elim (lpx_sn_inv_alt … H) -H
+#HL1 #IH @conj // -HL1
+#I1 #I #K1 #K #V1 #V #i #HLK1 #HLK
+lapply (ldrop_fwd_length_minus4 … HLK1)
+lapply (ldrop_fwd_length_le4 … HLK1)
+normalize in ⊢ (%→%→?); #HKL1 #Hi
+lapply (plus_minus_minus_be_aux … HL12 Hi) // -HL12 -Hi -HKL1
+<minus_plus #Hi >Hi -Hi
+elim (IH … HLK1 HLK) -IH #HI1 *
+/4 width=5 by or_introl, or_intror, and3_intro, ex4_3_intro/
+qed-.
(* LAZY SN POINTWISE EXTENSION OF A CONTEXT-SENSITIVE REALTION FOR TERMS ****)
-inductive llpx_sn (R:relation4 bind2 lenv term term): relation4 ynat term lenv lenv ≝
+inductive llpx_sn (R:relation3 lenv term term): relation4 ynat term lenv lenv ≝
| llpx_sn_sort: ∀L1,L2,d,k. |L1| = |L2| → llpx_sn R d (⋆k) L1 L2
| llpx_sn_skip: ∀L1,L2,d,i. |L1| = |L2| → yinj i < d → llpx_sn R d (#i) L1 L2
| llpx_sn_lref: ∀I,L1,L2,K1,K2,V1,V2,d,i. d ≤ yinj i →
⇩[i] L1 ≡ K1.ⓑ{I}V1 → ⇩[i] L2 ≡ K2.ⓑ{I}V2 →
- llpx_sn R (yinj 0) V1 K1 K2 → R I K1 V1 V2 → llpx_sn R d (#i) L1 L2
+ llpx_sn R (yinj 0) V1 K1 K2 → R K1 V1 V2 → llpx_sn R d (#i) L1 L2
| llpx_sn_free: ∀L1,L2,d,i. |L1| ≤ i → |L2| ≤ i → |L1| = |L2| → llpx_sn R d (#i) L1 L2
| llpx_sn_gref: ∀L1,L2,d,p. |L1| = |L2| → llpx_sn R d (§p) L1 L2
| llpx_sn_bind: ∀a,I,L1,L2,V,T,d.
| ∃∃I,K1,K2,V1,V2. ⇩[i] L1 ≡ K1.ⓑ{I}V1 &
⇩[i] L2 ≡ K2.ⓑ{I}V2 &
llpx_sn R (yinj 0) V1 K1 K2 &
- R I K1 V1 V2 & d ≤ yinj i.
+ R K1 V1 V2 & d ≤ yinj i.
#R #L1 #L2 #X #d * -L1 -L2 -X -d
[ #L1 #L2 #d #k #_ #j #H destruct
| #L1 #L2 #d #i #_ #Hid #j #H destruct /2 width=1 by or3_intro1/
| ∃∃I,K1,K2,V1,V2. ⇩[i] L1 ≡ K1.ⓑ{I}V1 &
⇩[i] L2 ≡ K2.ⓑ{I}V2 &
llpx_sn R (yinj 0) V1 K1 K2 &
- R I K1 V1 V2 & d ≤ yinj i.
+ R K1 V1 V2 & d ≤ yinj i.
/2 width=3 by llpx_sn_fwd_lref_aux/ qed-.
lemma llpx_sn_fwd_bind_sn: ∀R,a,I,L1,L2,V,T,d. llpx_sn R d (ⓑ{a,I}V.T) L1 L2 →
(* Basic_properties *********************************************************)
-lemma llpx_sn_refl: ∀R. (∀I,L. reflexive … (R I L)) → ∀T,L,d. llpx_sn R d T L L.
+lemma llpx_sn_refl: ∀R. (∀L. reflexive … (R L)) → ∀T,L,d. llpx_sn R d T L L.
#R #HR #T #L @(f2_ind … rfw … L T) -L -T
#n #IH #L * * /3 width=1 by llpx_sn_sort, llpx_sn_gref, llpx_sn_bind, llpx_sn_flat/
#i #Hn elim (lt_or_ge i (|L|)) /2 width=1 by llpx_sn_free/
llpx_sn R 0 (ⓑ{a,I}V.T) L1 L2.
/3 width=3 by llpx_sn_ge, llpx_sn_bind/ qed-.
-lemma llpx_sn_co: ∀R1,R2. (∀I,L,T1,T2. R1 I L T1 T2 → R2 I L T1 T2) →
+lemma llpx_sn_co: ∀R1,R2. (∀L,T1,T2. R1 L T1 T2 → R2 L T1 T2) →
∀L1,L2,T,d. llpx_sn R1 d T L1 L2 → llpx_sn R2 d T L1 L2.
#R1 #R2 #HR12 #L1 #L2 #T #d #H elim H -L1 -L2 -T -d
/3 width=9 by llpx_sn_sort, llpx_sn_skip, llpx_sn_lref, llpx_sn_free, llpx_sn_gref, llpx_sn_bind, llpx_sn_flat/
(* LAZY SN POINTWISE EXTENSION OF A CONTEXT-SENSITIVE REALTION FOR TERMS ****)
(* alternative definition of llpx_sn (not recursive) *)
-definition llpx_sn_alt: relation4 bind2 lenv term term → relation4 ynat term lenv lenv ≝
+definition llpx_sn_alt: relation3 lenv term term → relation4 ynat term lenv lenv ≝
λR,d,T,L1,L2. |L1| = |L2| ∧
(∀I1,I2,K1,K2,V1,V2,i. d ≤ yinj i → (L1 ⊢ i ~ϵ 𝐅*[d]⦃T⦄ → ⊥) →
⇩[i] L1 ≡ K1.ⓑ{I1}V1 → ⇩[i] L2 ≡ K2.ⓑ{I2}V2 →
- I1 = I2 ∧ R I1 K1 V1 V2
+ I1 = I2 ∧ R K1 V1 V2
).
(* Main properties **********************************************************)
(* LAZY SN POINTWISE EXTENSION OF A CONTEXT-SENSITIVE REALTION FOR TERMS ****)
(* alternative definition of llpx_sn (recursive) *)
-inductive llpx_sn_alt_r (R:relation4 bind2 lenv term term): relation4 ynat term lenv lenv ≝
+inductive llpx_sn_alt_r (R:relation3 lenv term term): relation4 ynat term lenv lenv ≝
| llpx_sn_alt_r_intro: ∀L1,L2,T,d.
(∀I1,I2,K1,K2,V1,V2,i. d ≤ yinj i → (∀U. ⇧[i, 1] U ≡ T → ⊥) →
- ⇩[i] L1 ≡ K1.ⓑ{I1}V1 → ⇩[i] L2 ≡ K2.ⓑ{I2}V2 → I1 = I2 ∧ R I1 K1 V1 V2
+ ⇩[i] L1 ≡ K1.ⓑ{I1}V1 → ⇩[i] L2 ≡ K2.ⓑ{I2}V2 → I1 = I2 ∧ R K1 V1 V2
) →
(∀I1,I2,K1,K2,V1,V2,i. d ≤ yinj i → (∀U. ⇧[i, 1] U ≡ T → ⊥) →
⇩[i] L1 ≡ K1.ⓑ{I1}V1 → ⇩[i] L2 ≡ K2.ⓑ{I2}V2 → llpx_sn_alt_r R 0 V1 K1 K2
lemma llpx_sn_alt_r_intro_alt: ∀R,L1,L2,T,d. |L1| = |L2| →
(∀I1,I2,K1,K2,V1,V2,i. d ≤ yinj i → (∀U. ⇧[i, 1] U ≡ T → ⊥) →
- ⇩[i] L1 ≡ K1.ⓑ{I1}V1 → ⇩[i] L2 ≡ K2.ⓑ{I2}V2 →
- ∧∧ I1 = I2 & R I1 K1 V1 V2 & llpx_sn_alt_r R 0 V1 K1 K2
+ ⇩[i] L1 ≡ K1.ⓑ{I1}V1 → ⇩[i] L2 ≡ K2.ⓑ{I2}V2 →
+ ∧∧ I1 = I2 & R K1 V1 V2 & llpx_sn_alt_r R 0 V1 K1 K2
) → llpx_sn_alt_r R d T L1 L2.
#R #L1 #L2 #T #d #HL12 #IH @llpx_sn_alt_r_intro // -HL12
#I1 #I2 #K1 #K2 #V1 #V2 #i #Hid #HnT #HLK1 #HLK2
(∀L1,L2,T,d. |L1| = |L2| → (
∀I1,I2,K1,K2,V1,V2,i. d ≤ yinj i → (∀U. ⇧[i, 1] U ≡ T → ⊥) →
⇩[i] L1 ≡ K1.ⓑ{I1}V1 → ⇩[i] L2 ≡ K2.ⓑ{I2}V2 →
- ∧∧ I1 = I2 & R I1 K1 V1 V2 & llpx_sn_alt_r R 0 V1 K1 K2 & S 0 V1 K1 K2
+ ∧∧ I1 = I2 & R K1 V1 V2 & llpx_sn_alt_r R 0 V1 K1 K2 & S 0 V1 K1 K2
) → S d T L1 L2) →
∀L1,L2,T,d. llpx_sn_alt_r R d T L1 L2 → S d T L1 L2.
#R #S #IH #L1 #L2 #T #d #H elim H -L1 -L2 -T -d
lemma llpx_sn_alt_r_inv_alt: ∀R,L1,L2,T,d. llpx_sn_alt_r R d T L1 L2 →
|L1| = |L2| ∧
∀I1,I2,K1,K2,V1,V2,i. d ≤ yinj i → (∀U. ⇧[i, 1] U ≡ T → ⊥) →
- ⇩[i] L1 ≡ K1.ⓑ{I1}V1 → ⇩[i] L2 ≡ K2.ⓑ{I2}V2 →
- ∧∧ I1 = I2 & R I1 K1 V1 V2 & llpx_sn_alt_r R 0 V1 K1 K2.
+ ⇩[i] L1 ≡ K1.ⓑ{I1}V1 → ⇩[i] L2 ≡ K2.ⓑ{I2}V2 →
+ ∧∧ I1 = I2 & R K1 V1 V2 & llpx_sn_alt_r R 0 V1 K1 K2.
#R #L1 #L2 #T #d #H @(llpx_sn_alt_r_ind_alt … H) -L1 -L2 -T -d
#L1 #L2 #T #d #HL12 #IH @conj // -HL12
#I1 #I2 #K1 #K2 #V1 #V2 #i #Hid #HnT #HLK1 #HLK2
| ∃∃I,K1,K2,V1,V2. ⇩[i] L1 ≡ K1.ⓑ{I}V1 &
⇩[i] L2 ≡ K2.ⓑ{I}V2 &
llpx_sn_alt_r R (yinj 0) V1 K1 K2 &
- R I K1 V1 V2 & d ≤ yinj i.
+ R K1 V1 V2 & d ≤ yinj i.
#R #L1 #L2 #d #i #H elim (llpx_sn_alt_r_inv_alt … H) -H
#HL12 #IH elim (lt_or_ge i (|L1|)) /3 width=1 by or3_intro0, conj/
elim (ylt_split i d) /3 width=1 by or3_intro1/
lemma llpx_sn_alt_r_lref: ∀R,I,L1,L2,K1,K2,V1,V2,d,i. d ≤ yinj i →
⇩[i] L1 ≡ K1.ⓑ{I}V1 → ⇩[i] L2 ≡ K2.ⓑ{I}V2 →
- llpx_sn_alt_r R 0 V1 K1 K2 → R I K1 V1 V2 →
+ llpx_sn_alt_r R 0 V1 K1 K2 → R K1 V1 V2 →
llpx_sn_alt_r R d (#i) L1 L2.
#R #I #L1 #L2 #K1 #K2 #V1 #V2 #d #i #Hdi #HLK1 #HLK2 #HK12 #HV12 @llpx_sn_alt_r_intro_alt
[ lapply (llpx_sn_alt_r_fwd_length … HK12) -HK12 #HK12
lemma llpx_sn_intro_alt_r: ∀R,L1,L2,T,d. |L1| = |L2| →
(∀I1,I2,K1,K2,V1,V2,i. d ≤ yinj i → (∀U. ⇧[i, 1] U ≡ T → ⊥) →
⇩[i] L1 ≡ K1.ⓑ{I1}V1 → ⇩[i] L2 ≡ K2.ⓑ{I2}V2 →
- ∧∧ I1 = I2 & R I1 K1 V1 V2 & llpx_sn R 0 V1 K1 K2
+ ∧∧ I1 = I2 & R K1 V1 V2 & llpx_sn R 0 V1 K1 K2
) → llpx_sn R d T L1 L2.
#R #L1 #L2 #T #d #HL12 #IH @llpx_sn_alt_r_inv_lpx_sn
@llpx_sn_alt_r_intro_alt // -HL12
(∀L1,L2,T,d. |L1| = |L2| → (
∀I1,I2,K1,K2,V1,V2,i. d ≤ yinj i → (∀U. ⇧[i, 1] U ≡ T → ⊥) →
⇩[i] L1 ≡ K1.ⓑ{I1}V1 → ⇩[i] L2 ≡ K2.ⓑ{I2}V2 →
- ∧∧ I1 = I2 & R I1 K1 V1 V2 & llpx_sn R 0 V1 K1 K2 & S 0 V1 K1 K2
+ ∧∧ I1 = I2 & R K1 V1 V2 & llpx_sn R 0 V1 K1 K2 & S 0 V1 K1 K2
) → S d T L1 L2) →
∀L1,L2,T,d. llpx_sn R d T L1 L2 → S d T L1 L2.
#R #S #IH1 #L1 #L2 #T #d #H lapply (llpx_sn_lpx_sn_alt_r … H) -H
|L1| = |L2| ∧
∀I1,I2,K1,K2,V1,V2,i. d ≤ yinj i → (∀U. ⇧[i, 1] U ≡ T → ⊥) →
⇩[i] L1 ≡ K1.ⓑ{I1}V1 → ⇩[i] L2 ≡ K2.ⓑ{I2}V2 →
- ∧∧ I1 = I2 & R I1 K1 V1 V2 & llpx_sn R 0 V1 K1 K2.
+ ∧∧ I1 = I2 & R K1 V1 V2 & llpx_sn R 0 V1 K1 K2.
#R #L1 #L2 #T #d #H lapply (llpx_sn_lpx_sn_alt_r … H) -H
#H elim (llpx_sn_alt_r_inv_alt … H) -H
#HL12 #IH @conj //
∀I,K2,V2. ⇩[i] L2 ≡ K2.ⓑ{I}V2 →
i < d ∨
∃∃K1,V1. ⇩[i] L1 ≡ K1.ⓑ{I}V1 & llpx_sn R 0 V1 K1 K2 &
- R I K1 V1 V2 & d ≤ i.
+ R K1 V1 V2 & d ≤ i.
#R #L1 #L2 #d #i #H #I #K2 #V2 #HLK2 elim (llpx_sn_fwd_lref … H) -H [ * || * ]
[ #_ #H elim (lt_refl_false i)
lapply (ldrop_fwd_length_lt2 … HLK2) -HLK2
∀I,K1,V1. ⇩[i] L1 ≡ K1.ⓑ{I}V1 →
i < d ∨
∃∃K2,V2. ⇩[i] L2 ≡ K2.ⓑ{I}V2 & llpx_sn R 0 V1 K1 K2 &
- R I K1 V1 V2 & d ≤ i.
+ R K1 V1 V2 & d ≤ i.
#R #L1 #L2 #d #i #H #I #K1 #V1 #HLK1 elim (llpx_sn_fwd_lref … H) -H [ * || * ]
[ #H #_ elim (lt_refl_false i)
lapply (ldrop_fwd_length_lt2 … HLK1) -HLK1
lemma llpx_sn_inv_lref_ge_dx: ∀R,L1,L2,d,i. llpx_sn R d (#i) L1 L2 → d ≤ i →
∀I,K2,V2. ⇩[i] L2 ≡ K2.ⓑ{I}V2 →
∃∃K1,V1. ⇩[i] L1 ≡ K1.ⓑ{I}V1 &
- llpx_sn R 0 V1 K1 K2 & R I K1 V1 V2.
+ llpx_sn R 0 V1 K1 K2 & R K1 V1 V2.
#R #L1 #L2 #d #i #H #Hdi #I #K2 #V2 #HLK2 elim (llpx_sn_fwd_lref_dx … H … HLK2) -L2
[ #H elim (ylt_yle_false … H Hdi)
| * /2 width=5 by ex3_2_intro/
lemma llpx_sn_inv_lref_ge_sn: ∀R,L1,L2,d,i. llpx_sn R d (#i) L1 L2 → d ≤ i →
∀I,K1,V1. ⇩[i] L1 ≡ K1.ⓑ{I}V1 →
∃∃K2,V2. ⇩[i] L2 ≡ K2.ⓑ{I}V2 &
- llpx_sn R 0 V1 K1 K2 & R I K1 V1 V2.
+ llpx_sn R 0 V1 K1 K2 & R K1 V1 V2.
#R #L1 #L2 #d #i #H #Hdi #I #K1 #V1 #HLK1 elim (llpx_sn_fwd_lref_sn … H … HLK1) -L1
[ #H elim (ylt_yle_false … H Hdi)
| * /2 width=5 by ex3_2_intro/
lemma llpx_sn_inv_lref_ge_bi: ∀R,L1,L2,d,i. llpx_sn R d (#i) L1 L2 → d ≤ i →
∀I1,I2,K1,K2,V1,V2.
⇩[i] L1 ≡ K1.ⓑ{I1}V1 → ⇩[i] L2 ≡ K2.ⓑ{I2}V2 →
- ∧∧ I1 = I2 & llpx_sn R 0 V1 K1 K2 & R I1 K1 V1 V2.
+ ∧∧ I1 = I2 & llpx_sn R 0 V1 K1 K2 & R K1 V1 V2.
#R #L1 #L2 #d #i #HL12 #Hdi #I1 #I2 #K1 #K2 #V1 #V2 #HLK1 #HLK2
elim (llpx_sn_inv_lref_ge_sn … HL12 … HLK1) // -L1 -d
#J #Y #HY lapply (ldrop_mono … HY … HLK2) -L2 -i #H destruct /2 width=1 by and3_intro/
fact llpx_sn_inv_S_aux: ∀R,L1,L2,T,d0. llpx_sn R d0 T L1 L2 → ∀d. d0 = d + 1 →
∀K1,K2,I,V1,V2. ⇩[d] L1 ≡ K1.ⓑ{I}V1 → ⇩[d] L2 ≡ K2.ⓑ{I}V2 →
- llpx_sn R 0 V1 K1 K2 → R I K1 V1 V2 → llpx_sn R d T L1 L2.
+ llpx_sn R 0 V1 K1 K2 → R K1 V1 V2 → llpx_sn R d T L1 L2.
#R #L1 #L2 #T #d0 #H elim H -L1 -L2 -T -d0
/2 width=1 by llpx_sn_gref, llpx_sn_free, llpx_sn_sort/
[ #L1 #L2 #d0 #i #HL12 #Hid #d #H #K1 #K2 #I #V1 #V2 #HLK1 #HLK2 #HK12 #HV12 destruct
lemma llpx_sn_inv_S: ∀R,L1,L2,T,d. llpx_sn R (d + 1) T L1 L2 →
∀K1,K2,I,V1,V2. ⇩[d] L1 ≡ K1.ⓑ{I}V1 → ⇩[d] L2 ≡ K2.ⓑ{I}V2 →
- llpx_sn R 0 V1 K1 K2 → R I K1 V1 V2 → llpx_sn R d T L1 L2.
+ llpx_sn R 0 V1 K1 K2 → R K1 V1 V2 → llpx_sn R d T L1 L2.
/2 width=9 by llpx_sn_inv_S_aux/ qed-.
-lemma llpx_sn_inv_bind_O: ∀R. (∀I,L. reflexive … (R I L)) →
+lemma llpx_sn_inv_bind_O: ∀R. (∀L. reflexive … (R L)) →
∀a,I,L1,L2,V,T. llpx_sn R 0 (ⓑ{a,I}V.T) L1 L2 →
llpx_sn R 0 V L1 L2 ∧ llpx_sn R 0 T (L1.ⓑ{I}V) (L2.ⓑ{I}V).
#R #HR #a #I #L1 #L2 #V #T #H elim (llpx_sn_inv_bind … H) -H
(* More advanced forward lemmas *********************************************)
-lemma llpx_sn_fwd_bind_O_dx: ∀R. (∀I,L. reflexive … (R I L)) →
+lemma llpx_sn_fwd_bind_O_dx: ∀R. (∀L. reflexive … (R L)) →
∀a,I,L1,L2,V,T. llpx_sn R 0 (ⓑ{a,I}V.T) L1 L2 →
llpx_sn R 0 T (L1.ⓑ{I}V) (L2.ⓑ{I}V).
#R #HR #a #I #L1 #L2 #V #T #H elim (llpx_sn_inv_bind_O … H) -H //
(* Advanced properties ******************************************************)
lemma llpx_sn_bind_repl_O: ∀R,I,L1,L2,V1,V2,T. llpx_sn R 0 T (L1.ⓑ{I}V1) (L2.ⓑ{I}V2) →
- ∀J,W1,W2. llpx_sn R 0 W1 L1 L2 → R J L1 W1 W2 → llpx_sn R 0 T (L1.ⓑ{J}W1) (L2.ⓑ{J}W2).
+ ∀J,W1,W2. llpx_sn R 0 W1 L1 L2 → R L1 W1 W2 → llpx_sn R 0 T (L1.ⓑ{J}W1) (L2.ⓑ{J}W2).
/3 width=9 by llpx_sn_bind_repl_SO, llpx_sn_inv_S/ qed-.
-lemma llpx_sn_dec: ∀R. (∀I,L,T1,T2. Decidable (R I L T1 T2)) →
+lemma llpx_sn_dec: ∀R. (∀L,T1,T2. Decidable (R L T1 T2)) →
∀T,L1,L2,d. Decidable (llpx_sn R d T L1 L2).
#R #HR #T #L1 @(f2_ind … rfw … L1 T) -L1 -T
#n #IH #L1 * *
elim (ldrop_O1_lt (Ⓕ) … HiL2) #I2 #K2 #V2 #HLK2
elim (ldrop_O1_lt (Ⓕ) … HiL1) #I1 #K1 #V1 #HLK1
elim (eq_bind2_dec I2 I1)
- [ #H2 elim (HR I1 K1 V1 V2) -HR
+ [ #H2 elim (HR K1 V1 V2) -HR
[ #H3 elim (IH K1 V1 … K2 0) destruct
/3 width=9 by llpx_sn_lref, ldrop_fwd_rfw, or_introl/
]
(* Properties on relocation *************************************************)
-lemma llpx_sn_lift_le: ∀R. (∀I. l_liftable (R I)) →
+lemma llpx_sn_lift_le: ∀R. l_liftable R →
∀K1,K2,T,d0. llpx_sn R d0 T K1 K2 →
∀L1,L2,d,e. ⇩[Ⓕ, d, e] L1 ≡ K1 → ⇩[Ⓕ, d, e] L2 ≡ K2 →
∀U. ⇧[d, e] T ≡ U → d0 ≤ d → llpx_sn R d0 U L1 L2.
(* Inversion lemmas on relocation *******************************************)
-lemma llpx_sn_inv_lift_le: ∀R. (∀I. l_deliftable_sn (R I)) →
+lemma llpx_sn_inv_lift_le: ∀R. l_deliftable_sn R →
∀L1,L2,U,d0. llpx_sn R d0 U L1 L2 →
∀K1,K2,d,e. ⇩[Ⓕ, d, e] L1 ≡ K1 → ⇩[Ⓕ, d, e] L2 ≡ K2 →
∀T. ⇧[d, e] T ≡ U → d0 ≤ d → llpx_sn R d0 T K1 K2.
(* Inversion lemmas on negated lazy pointwise extension *********************)
-lemma nllpx_sn_inv_bind: ∀R. (∀I,L,T1,T2. Decidable (R I L T1 T2)) →
+lemma nllpx_sn_inv_bind: ∀R. (∀L,T1,T2. Decidable (R L T1 T2)) →
∀a,I,L1,L2,V,T,d. (llpx_sn R d (ⓑ{a,I}V.T) L1 L2 → ⊥) →
(llpx_sn R d V L1 L2 → ⊥) ∨ (llpx_sn R (⫯d) T (L1.ⓑ{I}V) (L2.ⓑ{I}V) → ⊥).
#R #HR #a #I #L1 #L2 #V #T #d #H elim (llpx_sn_dec … HR V L1 L2 d)
/4 width=1 by llpx_sn_bind, or_intror, or_introl/
qed-.
-lemma nllpx_sn_inv_flat: ∀R. (∀I,L,T1,T2. Decidable (R I L T1 T2)) →
+lemma nllpx_sn_inv_flat: ∀R. (∀L,T1,T2. Decidable (R L T1 T2)) →
∀I,L1,L2,V,T,d. (llpx_sn R d (ⓕ{I}V.T) L1 L2 → ⊥) →
(llpx_sn R d V L1 L2 → ⊥) ∨ (llpx_sn R d T L1 L2 → ⊥).
#R #HR #I #L1 #L2 #V #T #d #H elim (llpx_sn_dec … HR V L1 L2 d)
/4 width=1 by llpx_sn_flat, or_intror, or_introl/
qed-.
-lemma nllpx_sn_inv_bind_O: ∀R. (∀I,L,T1,T2. Decidable (R I L T1 T2)) →
+lemma nllpx_sn_inv_bind_O: ∀R. (∀L,T1,T2. Decidable (R L T1 T2)) →
∀a,I,L1,L2,V,T. (llpx_sn R 0 (ⓑ{a,I}V.T) L1 L2 → ⊥) →
(llpx_sn R 0 V L1 L2 → ⊥) ∨ (llpx_sn R 0 T (L1.ⓑ{I}V) (L2.ⓑ{I}V) → ⊥).
#R #HR #a #I #L1 #L2 #V #T #H elim (llpx_sn_dec … HR V L1 L2 0)
(* Properties on pointwise extensions ***************************************)
-lemma lpx_sn_llpx_sn: ∀R. (∀I,L. reflexive … (R I L)) →
+lemma lpx_sn_llpx_sn: ∀R. (∀L. reflexive … (R L)) →
∀T,L1,L2,d. lpx_sn R L1 L2 → llpx_sn R d T L1 L2.
#R #HR #T #L1 @(f2_ind … rfw … L1 T) -L1 -T
#n #IH #L1 * *
(* Properties about transitive closure **************************************)
-lemma llpx_sn_TC_pair_dx: ∀R. (∀I,L. reflexive … (R I L)) →
- ∀I,L,V1,V2,T. LTC … (R I) L V1 V2 →
+lemma llpx_sn_TC_pair_dx: ∀R. (∀L. reflexive … (R L)) →
+ ∀I,L,V1,V2,T. LTC … R L V1 V2 →
LTC … (llpx_sn R 0) T (L.ⓑ{I}V1) (L.ⓑ{I}V2).
#R #HR #I #L #V1 #V2 #T #H @(TC_star_ind … V2 H) -V2
/4 width=9 by llpx_sn_bind_repl_O, llpx_sn_refl, step, inj/
}
]
[ { "pointwise union for local environments" * } {
- [ "llor ( ? ⩖[?] ? ≡ ? )" * ]
+ [ "llor ( ? ⩖[?] ? ≡ ? )" "llor_alt" * ]
}
]
[ { "context-sensitive exclusion from free variables" * } {
(* Equations ****************************************************************)
+(* Note: uses minus_minus_comm, minus_plus_m_m, commutative_plus, plus_minus *)
+lemma plus_minus_minus_be: ∀x,y,z. y ≤ z → z ≤ x → (x - z) + (z - y) = x - y.
+#x #z #y #Hzy #Hyx >plus_minus // >commutative_plus >plus_minus //
+qed-.
+
+fact plus_minus_minus_be_aux: ∀i,x,y,z. y ≤ z → z ≤ x → i = z - y → x - z + i = x - y.
+/2 width=1 by plus_minus_minus_be/ qed-.
+
lemma plus_n_2: ∀n. n + 2 = n + 1 + 1.
// qed.
projects / helm.git / commitdiff