--- /dev/null
+include "basic_2/grammar/cl_shift.ma".
+include "basic_2/relocation/ldrop_append.ma".
+
+lemma cpy_append: ∀G,d,e. l_appendable_sn … (cpy d e G).
+#G #d #e #K #T1 #T2 #H elim H -G -K -T1 -T2 -d -e
+/2 width=1 by cpy_atom, cpy_bind, cpy_flat/
+#I #G #K #K0 #V #W #i #d #e #Hdi #Hide #HK0 #HVW #L
+lapply (ldrop_fwd_length_lt2 … HK0) #H
+@(cpy_subst I … (L@@K0) … HVW) // (**) (* /4/ does not work *)
+@(ldrop_O1_append_sn_le … HK0) /2 width=2 by lt_to_le/
+qed-.
+
+lemma cpy_fwd_shift1: ∀G,L1,L,T1,T,d,e. ⦃G, L⦄ ⊢ L1 @@ T1 ▶[d, e] T →
+ ∃∃L2,T2. |L1| = |L2| & T = L2 @@ T2.
+#G #L1 @(lenv_ind_dx … L1) -L1 normalize
+[ #L #T1 #T #d #e #HT1
+ @(ex2_2_intro … (⋆)) // (**) (* explicit constructor *)
+| #I #L1 #V1 #IH #L #T1 #X #d #e
+ >shift_append_assoc normalize #H
+ elim (cpy_inv_bind1 … H) -H
+ #V0 #T0 #_ #HT10 #H destruct
+ elim (IH … HT10) -IH -HT10 #L2 #T2 #HL12 #H destruct
+ >append_length >HL12 -HL12
+ @(ex2_2_intro … (⋆.ⓑ{I}V0@@L2) T2) [ >append_length ] (**) (* explicit constructor *)
+ /2 width=3 by trans_eq/
+]
+qed-.
--- /dev/null
+include "basic_2/grammar/cl_shift.ma".
+include "basic_2/relocation/ldrop_append.ma".
+
+lemma cpys_append: ∀G. l_appendable_sn … (cpys G).
+#G #K #T1 #T2 #H elim H -G -K -T1 -T2
+/2 width=3 by cpys_bind, cpys_flat/
+#I #G #K #K0 #V1 #V2 #W2 #i #HK0 #_ #HVW2 #IHV12 #L
+lapply (ldrop_fwd_length_lt2 … HK0) #H
+@(cpys_delta … I … (L@@K0) V1 … HVW2) //
+@(ldrop_O1_append_sn_le … HK0) /2 width=2 by lt_to_le/ (**) (* /3/ does not work *)
+qed.
+
+lemma cpys_fwd_shift1: ∀G,L1,L,T1,T. ⦃G, L⦄ ⊢ L1 @@ T1 ▶*× T →
+ ∃∃L2,T2. |L1| = |L2| & T = L2 @@ T2.
+#G #L1 @(lenv_ind_dx … L1) -L1 normalize
+[ #L #T1 #T #HT1 @(ex2_2_intro … (⋆)) // (**) (* explicit constructor *)
+| #I #L1 #V1 #IH #L #T1 #X >shift_append_assoc normalize
+ #H elim (cpys_inv_bind1 … H) -H
+ #V0 #T0 #_ #HT10 #H destruct
+ elim (IH … HT10) -IH -HT10 #L2 #T2 #HL12 #H destruct
+ >append_length >HL12 -HL12
+ @(ex2_2_intro … (⋆.ⓑ{I}V0@@L2) T2) [ >append_length ] /2 width=3 by trans_eq/ (**) (* explicit constructor *)
+]
+qed-.
--- /dev/null
+lemma cpys_append: ∀G,d,e. l_appendable_sn … (cpys d e G).
+#G #d #e #K #T1 #T2 #H @(cpys_ind … H) -T2
+/3 width=3 by cpys_strap1, cpy_append/
+qed-.
+
+lemma cpys_fwd_shift1: ∀G,L,L1,T1,T,d,e. ⦃G, L⦄ ⊢ L1 @@ T1 ▶*[d, e] T →
+ ∃∃L2,T2. |L1| = |L2| & T = L2 @@ T2.
+#G #L #L1 #T1 #T #d #e #H @(cpys_ind … H) -T
+[ /2 width=4 by ex2_2_intro/
+| #T #X #_ #HX * #L0 #T0 #HL10 #H destruct
+ elim (cpy_fwd_shift1 … HX) -HX #L2 #T2 #HL02 #H destruct
+ /2 width=4 by ex2_2_intro/
+]
+qed-.
--- /dev/null
+lemma lpys_append: ∀G,K1,K2. ⦃G, K1⦄ ⊢ ▶*× K2 → ∀L1,L2. ⦃G, L1⦄ ⊢ ▶*× L2 →
+ ⦃G, L1 @@ K1⦄ ⊢ ▶*× L2 @@ K2.
+/3 width=1 by lpx_sn_append, cpys_append/ qed.
+
+(* Advanced forward lemmas **************************************************)
+
+lemma lpys_fwd_append1: ∀G,K1,L1,L. ⦃G, K1 @@ L1⦄ ⊢ ▶*× L →
+ ∃∃K2,L2. ⦃G, K1⦄ ⊢ ▶*× K2 & L = K2 @@ L2.
+/2 width=2 by lpx_sn_fwd_append1/ qed-.
+
+lemma lpys_fwd_append2: ∀G,L,K2,L2. ⦃G, L⦄ ⊢ ▶*× K2 @@ L2 →
+ ∃∃K1,L1. ⦃G, K1⦄ ⊢ ▶*× K2 & L = K1 @@ L1.
+/2 width=2 by lpx_sn_fwd_append2/ qed-.
+
+(* Advanced forward lemmas **************************************************)
+
+lemma cpys_fwd_shift1_ext: ∀G,L1,L,T1,T. ⦃G, L⦄ ⊢ L1 @@ T1 ▶*× T →
+ ∃∃L2,T2. ⦃G, L @@ L1⦄ ⊢ ▶*× L @@ L2 & ⦃G, L @@ L1⦄ ⊢ T1 ▶*× T2 &
+ T = L2 @@ T2.
+#G #L1 @(lenv_ind_dx … L1) -L1
+[ #L #T1 #T #HT1 @ex3_2_intro
+ [3: // |4,5: // |1,2: skip ] (**) (* auto does not work *)
+| #I #L1 #V1 #IH #L #T1 #T >shift_append_assoc #H <append_assoc
+ elim (cpys_inv_bind1 … H) -H #V2 #T2 #HV12 #HT12 #H destruct
+ elim (IH … HT12) -IH -HT12 #L2 #T #HL12 #HT1 #H destruct
+ lapply (lpys_trans … HL12 (L.ⓑ{I}V2@@L2) ?) -HL12 /3 width=1 by lpys_append, lpys_pair/ #HL12
+ @(ex3_2_intro … (⋆.ⓑ{I}V2@@L2)) [4: /2 width=3 by trans_eq/ | skip ] <append_assoc // (**) (* explicit constructor *)
+]
+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/cofreestar_3.ma".
+include "basic_2/relocation/lift_neg.ma".
+include "basic_2/substitution/cpys.ma".
+
+(* CONTEXT-SENSITIVE EXCLUSION FROM FREE VARIABLES **************************)
+
+definition cofrees: relation3 lenv nat term ≝
+ λL,i,U1. ∀U2. ⦃⋆, L⦄ ⊢ U1 ▶* U2 → ∃T2. ⇧[i, 1] T2 ≡ U2.
+
+interpretation
+ "context-sensitive exclusion from free variables (term)"
+ 'CoFreeStar L i U = (cofrees L i U).
+
+(* Basic forward lemmas *****************************************************)
+
+lemma cofrees_fwd_lift: ∀L,U,i. L ⊢ i ~ϵ 𝐅*⦃U⦄ → ∃T. ⇧[i, 1] T ≡ U.
+/2 width=1 by/ qed-.
+
+lemma cofrees_fwd_bind_sn: ∀a,I,L,W,U,i. L ⊢ i ~ϵ 𝐅*⦃ⓑ{a,I}W.U⦄ →
+ L ⊢ i ~ϵ 𝐅*⦃W⦄.
+#a #I #L #W1 #U #i #H #W2 #HW12 elim (H (ⓑ{a,I}W2.U)) /2 width=1 by cpys_bind/ -W1
+#X #H elim (lift_inv_bind2 … H) -H /2 width=2 by ex_intro/
+qed-.
+
+lemma cofrees_fwd_bind_dx: ∀a,I,L,W,U,i. L ⊢ i ~ϵ 𝐅*⦃ⓑ{a,I}W.U⦄ →
+ L.ⓑ{I}W ⊢ i+1 ~ϵ 𝐅*⦃U⦄.
+#a #I #L #W #U1 #i #H #U2 #HU12 elim (H (ⓑ{a,I}W.U2)) /2 width=1 by cpys_bind/ -U1
+#X #H elim (lift_inv_bind2 … H) -H /2 width=2 by ex_intro/
+qed-.
+
+lemma cofrees_fwd_flat_sn: ∀I,L,W,U,i. L ⊢ i ~ϵ 𝐅*⦃ⓕ{I}W.U⦄ →
+ L ⊢ i ~ϵ 𝐅*⦃W⦄.
+#I #L #W1 #U #i #H #W2 #HW12 elim (H (ⓕ{I}W2.U)) /2 width=1 by cpys_flat/ -W1
+#X #H elim (lift_inv_flat2 … H) -H /2 width=2 by ex_intro/
+qed-.
+
+lemma cofrees_fwd_flat_dx: ∀I,L,W,U,i. L ⊢ i ~ϵ 𝐅*⦃ⓕ{I}W.U⦄ →
+ L ⊢ i ~ϵ 𝐅*⦃U⦄.
+#I #L #W #U1 #i #H #U2 #HU12 elim (H (ⓕ{I}W.U2)) /2 width=1 by cpys_flat/ -U1
+#X #H elim (lift_inv_flat2 … H) -H /2 width=2 by ex_intro/
+qed-.
+
+(* Basic inversion lemmas ***************************************************)
+
+lemma cofrees_inv_gen: ∀L,U,U0,i. ⦃⋆, L⦄ ⊢ U ▶* U0 → (∀T. ⇧[i, 1] T ≡ U0 → ⊥) →
+ L ⊢ i ~ϵ 𝐅*⦃U⦄ → ⊥.
+#L #U #U0 #i #HU0 #HnU0 #HU elim (HU … HU0) -L -U /2 width=2 by/
+qed-.
+
+lemma cofrees_inv_lref_eq: ∀L,i. L ⊢ i ~ϵ 𝐅*⦃#i⦄ → ⊥.
+#L #i #H elim (H (#i)) -H //
+#X #H elim (lift_inv_lref2_be … H) -H //
+qed-.
+
+lemma cofrees_inv_bind: ∀a,I,L,W,U,i. L ⊢ i ~ϵ 𝐅*⦃ⓑ{a,I}W.U⦄ →
+ L ⊢ i ~ϵ 𝐅*⦃W⦄ ∧ L.ⓑ{I}W ⊢ i+1 ~ϵ 𝐅*⦃U⦄.
+/3 width=7 by cofrees_fwd_bind_sn, cofrees_fwd_bind_dx, conj/ qed-.
+
+lemma cofrees_inv_flat: ∀I,L,W,U,i. L ⊢ i ~ϵ 𝐅*⦃ⓕ{I}W.U⦄ →
+ L ⊢ i ~ϵ 𝐅*⦃W⦄ ∧ L ⊢ i ~ϵ 𝐅*⦃U⦄.
+/3 width=6 by cofrees_fwd_flat_sn, cofrees_fwd_flat_dx, conj/ qed-.
+
+(* Basic Properties *********************************************************)
+
+lemma cofrees_sort: ∀L,i,k. L ⊢ i ~ϵ 𝐅*⦃⋆k⦄.
+#L #i #k #X #H >(cpys_inv_sort1 … H) -X /2 width=2 by ex_intro/
+qed.
+
+lemma cofrees_gref: ∀L,i,p. L ⊢ i ~ϵ 𝐅*⦃§p⦄.
+#L #i #p #X #H >(cpys_inv_gref1 … H) -X /2 width=2 by ex_intro/
+qed.
+
+lemma cofrees_bind: ∀L,V,i. L ⊢ i ~ϵ 𝐅*⦃V⦄ →
+ ∀I,T. L.ⓑ{I}V ⊢ i+1 ~ϵ 𝐅*⦃T⦄ →
+ ∀a. L ⊢ i ~ϵ 𝐅*⦃ⓑ{a,I}V.T⦄.
+#L #W1 #i #HW1 #I #U1 #HU1 #a #X #H elim (cpys_inv_bind1 … H) -H
+#W2 #U2 #HW12 #HU12 #H destruct
+elim (HW1 … HW12) elim (HU1 … HU12) -W1 -U1 /3 width=2 by lift_bind, ex_intro/
+qed.
+
+lemma cofrees_flat: ∀L,V,i. L ⊢ i ~ϵ 𝐅*⦃V⦄ → ∀T. L ⊢ i ~ϵ 𝐅*⦃T⦄ →
+ ∀I. L ⊢ i ~ϵ 𝐅*⦃ⓕ{I}V.T⦄.
+#L #W1 #i #HW1 #U1 #HU1 #I #X #H elim (cpys_inv_flat1 … H) -H
+#W2 #U2 #HW12 #HU12 #H destruct
+elim (HW1 … HW12) elim (HU1 … HU12) -W1 -U1 /3 width=2 by lift_flat, ex_intro/
+qed.
+
+axiom cofrees_dec: ∀L,T,i. Decidable (L ⊢ i ~ϵ 𝐅*⦃T⦄).
+
+(* Basic negated inversion lemmas *******************************************)
+
+lemma frees_inv_bind: ∀a,I,L,V,T,i. (L ⊢ i ~ϵ 𝐅*⦃ⓑ{a,I}V.T⦄ → ⊥) →
+ (L ⊢ i ~ϵ 𝐅*⦃V⦄ → ⊥) ∨ (L.ⓑ{I}V ⊢ i+1 ~ϵ 𝐅*⦃T⦄ → ⊥).
+#a #I #L #W #U #i #H elim (cofrees_dec L W i)
+/4 width=8 by cofrees_bind, or_intror, or_introl/
+qed-.
+
+lemma frees_inv_flat: ∀I,L,V,T,i. (L ⊢ i ~ϵ 𝐅*⦃ⓕ{I}V.T⦄ → ⊥) →
+ (L ⊢ i ~ϵ 𝐅*⦃V⦄ → ⊥) ∨ (L ⊢ i ~ϵ 𝐅*⦃T⦄ → ⊥).
+#I #L #W #U #i #H elim (cofrees_dec L W i)
+/4 width=7 by cofrees_flat, 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/lift_neg.ma".
+include "basic_2/relocation/lift_lift.ma".
+include "basic_2/substitution/cpys.ma".
+include "basic_2/substitution/cofrees_lift.ma".
+
+(* CONTEXT-SENSITIVE EXCLUSION FROM FREE VARIABLES **************************)
+
+(* Alternative definition of frees_ge ***************************************)
+
+(*
+lemma cpys_fwd_nlift2: ∀G,L,U1,U2. ⦃G, L⦄ ⊢ U1 ▶* U2 →
+ ∀i. (∀T2. ⇧[i, 1] T2 ≡ U2 → ⊥) →
+ (∀T1. ⇧[i, 1] T1 ≡ U1 → ⊥) ∨
+ ∃∃I,K,W,j. j < i & ⇩[j]L ≡ K.ⓑ{I}W &
+ (∀V. ⇧[i-j-1, 1] V ≡ W → ⊥) & (∀T1. ⇧[j, 1] T1 ≡ U1 → ⊥).
+#G #L #U1 #U2 #H elim H -G -L -U1 -U2
+[ /3 width=2 by or_introl/
+| #I #G #L #K #V1 #V2 #W2 #j #HLK #_ #HVW2 #IHV12 #i #HnW2
+ elim (lt_or_ge j i) #Hij
+ [ @or_intror (**) @(ex4_4_intro … HLK) //
+ [ #X #HXV elim (lift_trans_le … HXV … HVW ?) -V //
+ #Y #HXY >minus_plus <plus_minus_m_m /2 width=2 by/
+ | -HnW2 /2 width=7 by lift_inv_lref2_be/
+ ]
+ | elim (lift_split … HVW2 i j) -HVW2 //
+ #X #_ #H elim HnW2 -HnW2 //
+ ]
+| #a #I #G #L #W1 #W2 #U1 #U2 #_ #_ #IHW12 #IHU12 #i #H elim (nlift_inv_bind … H) -H
+ [ #HnW2 elim (IHW12 … HnW2) -IHW12 -HnW2 -IHU12
+ [ /4 width=9 by nlift_bind_sn, or_introl/
+ | * /5 width=9 by nlift_bind_sn, ex4_4_intro, or_intror/
+ ]
+ | #HnU2 elim (IHU12 … HnU2) -IHU12 -HnU2 -IHW12
+ [ /4 width=9 by nlift_bind_dx, or_introl/
+ | * #J #K #W #j @(nat_ind_plus … j) -j
+ [ #_ #H lapply (ldrop_inv_pair1 … H) -H
+ #H destruct /4 width=9 by nlift_bind_sn, or_introl/
+ | #j #_ #Hji #HLK #HnW
+ lapply (ldrop_inv_drop1_lt … HLK ?) // -HLK #HLK #HnU1
+ <minus_le_minus_minus_comm in HnW;
+ /5 width=9 by nlift_bind_dx, monotonic_lt_pred, ex4_4_intro, or_intror/
+ ]
+ ]
+ ]
+| #I #G #L #W1 #W2 #U1 #U2 #_ #_ #IHW12 #IHU12 #i #H elim (nlift_inv_flat … H) -H
+ [ #HnW2 elim (IHW12 … HnW2) -IHW12 -HnW2 -IHU12
+ [ /4 width=9 by nlift_flat_sn, or_introl/
+ | * /5 width=9 by nlift_flat_sn, ex4_4_intro, or_intror/
+ ]
+ | #HnU2 elim (IHU12 … HnU2) -IHU12 -HnU2 -IHW12
+ [ /4 width=9 by nlift_flat_dx, or_introl/
+ | * /5 width=9 by nlift_flat_dx, ex4_4_intro, or_intror/
+ ]
+]
+qed-.
+*)
+lemma nlift_frees: ∀L,U,i. (∀T. ⇧[i, 1] T ≡ U → ⊥) → (L ⊢ i ~ϵ 𝐅*⦃U⦄ → ⊥).
+#L #U #i #HnTU #H elim (cofrees_fwd_lift … H) -H /2 width=2 by/
+qed-.
+(*
+lemma frees_inv_ge: ∀L,U,d,i. d ≤ yinj i → (L ⊢ i ~ϵ 𝐅*[d]⦃U⦄ → ⊥) →
+ (∀T. ⇧[i, 1] T ≡ U → ⊥) ∨
+ ∃∃I,K,W,j. d ≤ yinj j & j < i & ⇩[j]L ≡ K.ⓑ{I}W &
+ (K ⊢ i-j-1 ~ϵ 𝐅*[yinj 0]⦃W⦄ → ⊥) & (∀T. ⇧[j, 1] T ≡ U → ⊥).
+#L #U #d #i #Hdi #H @(frees_ind … H) -U /3 width=2 by or_introl/
+#U1 #U2 #HU12 #HU2 *
+[ #HnU2 elim (cpy_fwd_nlift2_ge … HU12 … HnU2) -HU12 -HnU2 /3 width=2 by or_introl/
+ * /5 width=9 by nlift_frees, ex5_4_intro, or_intror/
+| * #I2 #K2 #W2 #j2 #Hdj2 #Hj2i #HLK2 #HnW2 #HnU2 elim (cpy_fwd_nlift2_ge … HU12 … HnU2) -HU12 -HnU2 /4 width=9 by ex5_4_intro, or_intror/
+ * #I1 #K1 #W1 #j1 #Hdj1 #Hj12 #HLK1 #HnW1 #HnU1
+ lapply (ldrop_conf_ge … HLK1 … HLK2 ?) -HLK2 /2 width=1 by lt_to_le/
+ #HK12 lapply (ldrop_inv_drop1_lt … HK12 ?) /2 width=1 by lt_plus_to_minus_r/ -HK12
+ #HK12
+ @or_intror @(ex5_4_intro … HLK1 … HnU1) -HLK1 -HnU1 /2 width=3 by transitive_lt/
+ @(frees_be … HK12 … HnW1) /2 width=1 by arith_k_sn/ -HK12 -HnW1
+ >minus_plus in ⊢ (??(?(?%?)?)??→?); >minus_plus in ⊢ (??(?(??%)?)??→?); >arith_b1 /2 width=1 by/
+]
+qed-.
+
+lemma frees_ind_ge: ∀R:relation4 ynat nat lenv term.
+ (∀d,i,L,U. d ≤ yinj i → (∀T. ⇧[i, 1] T ≡ U → ⊥) → R d i L U) →
+ (∀d,i,j,I,L,K,W,U. d ≤ yinj j → j < i → ⇩[j]L ≡ K.ⓑ{I}W → (K ⊢ i-j-1 ~ϵ 𝐅*[0]⦃W⦄ → ⊥) → (∀T. ⇧[j, 1] T ≡ U → ⊥) → R 0 (i-j-1) K W → R d i L U) →
+ ∀d,i,L,U. d ≤ yinj i → (L ⊢ i ~ϵ 𝐅*[d]⦃U⦄ → ⊥) → R d i L U.
+#R #IH1 #IH2 #d #i #L #U
+generalize in match d; -d generalize in match i; -i
+@(f2_ind … rfw … L U) -L -U
+#n #IHn #L #U #Hn #i #d #Hdi #H elim (frees_inv_ge … H) -H /3 width=2 by/
+-IH1 * #I #K #W #j #Hdj #Hji #HLK #HnW #HnU destruct /4 width=12 by ldrop_fwd_rfw/
+qed-.
+*)
--- /dev/null
+(**************************************************************************)
+(* ___ *)
+(* ||M|| *)
+(* ||A|| A project by Andrea Asperti *)
+(* ||T|| *)
+(* ||I|| Developers: *)
+(* ||T|| The HELM team. *)
+(* ||A|| http://helm.cs.unibo.it *)
+(* \ / *)
+(* \ / This file is distributed under the terms of the *)
+(* v GNU General Public License Version 2 *)
+(* *)
+(**************************************************************************)
+
+include "basic_2/substitution/cpys_lift.ma".
+include "basic_2/substitution/cofrees.ma".
+
+(* CONTEXT-SENSITIVE EXCLUSION FROM FREE VARIABLES **************************)
+
+(* Advanced inversion lemmas ************************************************)
+
+lemma cofrees_inv_lref_lt: ∀L,i,j. L ⊢ i ~ϵ 𝐅*⦃#j⦄ → j < i →
+ ∀I,K,W. ⇩[j]L ≡ K.ⓑ{I}W → K ⊢ i-j-1 ~ϵ 𝐅*⦃W⦄.
+#L #i #j #Hj #Hji #I #K #W1 #HLK #W2 #HW12 elim (lift_total W2 0 (j+1))
+#X2 #HWX2 elim (Hj X2) /2 width=7 by cpys_delta/ -I -L -K -W1
+#Z2 #HZX2 elim (lift_div_le … HWX2 (i-j-1) 1 Z2) -HWX2 /2 width=2 by ex_intro/
+>minus_plus <plus_minus_m_m //
+qed-.
+
+lemma cofrees_inv_lt: ∀L,U,i. L ⊢ i ~ϵ 𝐅*⦃U⦄ → ∀j. (∀T. ⇧[j, 1] T ≡ U → ⊥) →
+ ∀I,K,W. ⇩[j]L ≡ K.ⓑ{I}W → j < i → K ⊢ i-j-1 ~ϵ 𝐅*⦃W⦄.
+#L #U @(f2_ind … rfw … L U) -L -U
+#n #IH #L * *
+[ -IH #k #_ #i #_ #j #H elim (H (⋆k)) -H //
+| -IH #j #_ #i #Hi0 #j0 #H <(nlift_inv_lref_be_SO … H) -j0
+ /2 width=7 by cofrees_inv_lref_lt/
+| -IH #p #_ #i #_ #j #H elim (H (§p)) -H //
+| #a #J #W #U #Hn #i #H1 #j #H2 #I #K #V #HLK #Hji destruct
+ elim (cofrees_inv_bind … H1) -H1 #HW #HU
+ elim (nlift_inv_bind … H2) -H2 [ -HU /3 width=7 by/ ]
+ -HW #HnU lapply (IH … HU … HnU I K V ? ?)
+ /2 width=1 by ldrop_drop, lt_minus_to_plus/ -a -I -J -L -W -U
+ >minus_plus_plus_l //
+| #J #W #U #Hn #i #H1 #j #H2 #I #K #V #HLK #Hji destruct
+ elim (cofrees_inv_flat … H1) -H1 #HW #HU
+ elim (nlift_inv_flat … H2) -H2 [ /3 width=7 by/ ]
+ #HnU @(IH … HU … HnU … HLK) // (**) (* full auto fails *)
+]
+qed-.
+
+(* Advanced properties ******************************************************)
+
+lemma cofrees_lref_gt: ∀L,i,j. i < j → L ⊢ i ~ϵ 𝐅*⦃#j⦄.
+#L #i #j #Hij #X #H elim (cpys_inv_lref1 … H) -H
+[ #H destruct /3 width=2 by lift_lref_ge_minus, ex_intro/
+| * #I #K #V1 #V2 #_ #_ #H -I -L -K -V1
+ elim (lift_split … H i j) /2 width=2 by lt_to_le, ex_intro/
+]
+qed.
+
+lemma cofrees_lref_lt: ∀I,L,K,W,i,j. j < i → ⇩[j] L ≡ K.ⓑ{I}W →
+ K ⊢ (i-j-1) ~ϵ 𝐅*⦃W⦄ → L ⊢ i ~ϵ 𝐅*⦃#j⦄.
+#I #L #K #W1 #i #j #Hji #HLK #HW1 #X #H elim (cpys_inv_lref1 … H) -H
+[ #H destruct /3 width=2 by lift_lref_lt, ex_intro/
+| * #I0 #K0 #W0 #W2 #HLK0 #HW12 #HW2 lapply (ldrop_mono … HLK0 … HLK) -L
+ #H destruct elim (HW1 … HW12) -I -K -W1
+ #V2 #HVW2 elim (lift_trans_le … HVW2 … HW2) -W2 //
+ >minus_plus <plus_minus_m_m /2 width=2 by ex_intro/
+]
+qed.
+
+lemma cofrees_lref_free: ∀L,i,j. |L| ≤ j → j < i → L ⊢ i ~ϵ 𝐅*⦃#j⦄.
+#L #i #j #Hj #Hji #X #H elim (cpys_inv_lref1 … H) -H
+[ #H destruct /3 width=2 by lift_lref_lt, ex_intro/
+| * #I #K #W1 #W2 #HLK lapply (ldrop_fwd_length_lt2 … HLK) -I
+ #H elim (lt_refl_false j) -K -W1 -W2 -X -i /2 width=3 by lt_to_le_to_lt/
+]
+qed.
+
+(* Advanced negated inversion lemmas ****************************************)
+
+lemma frees_inv_lref_lt: ∀L,i,j. j < i → (L ⊢ i ~ϵ 𝐅*⦃#j⦄ → ⊥) →
+ ∃∃I,K,W. ⇩[j] L ≡ K.ⓑ{I}W & (K ⊢ (i-j-1) ~ϵ 𝐅*⦃W⦄ → ⊥).
+#L #i #j #Hji #H elim (lt_or_ge j (|L|)) #Hj
+[ elim (ldrop_O1_lt (Ⓕ) … Hj) -Hj /4 width=9 by cofrees_lref_lt, ex2_3_intro/
+| elim H -H /2 width=5 by cofrees_lref_free/
+]
+qed-.
+
+lemma frees_inv_lref_free: ∀L,i,j. (L ⊢ i ~ϵ 𝐅*⦃#j⦄ → ⊥) → |L| ≤ j → j = i.
+#L #i #j #H #Hj elim (lt_or_eq_or_gt i j) //
+#Hij elim H -H /2 width=5 by cofrees_lref_gt, cofrees_lref_free/
+qed-.
+
+lemma frees_inv_gen: ∀L,U,i. (L ⊢ i ~ϵ 𝐅*⦃U⦄ → ⊥) →
+ ∃∃U0. ⦃⋆, L⦄ ⊢ U ▶* U0 & (∀T. ⇧[i, 1] T ≡ U0 → ⊥).
+#L #U @(f2_ind … rfw … L U) -L -U
+#n #IH #L * *
+[ -IH #k #_ #i #H elim H -H //
+| #j #Hn #i #H elim (lt_or_eq_or_gt i j)
+ [ -n #Hij elim H -H /2 width=4 by cofrees_lref_gt/
+ | -H -n #H destruct /3 width=7 by lift_inv_lref2_be, ex2_intro/
+ | #Hji elim (frees_inv_lref_lt … H) // -H
+ #I #K #W1 #HLK #H elim (IH … H) /2 width=3 by ldrop_fwd_rfw/ -H -n
+ #W2 #HW12 #HnW2 elim (lift_total W2 0 (j+1))
+ #U2 #HWU2 @(ex2_intro … U2) /2 width=7 by cpys_delta/ -I -L -K -W1
+ #T2 #HTU2 elim (lift_div_le … HWU2 (i-j-1) 1 T2) /2 width=2 by/ -W2
+ >minus_plus <plus_minus_m_m //
+ ]
+| -IH #p #_ #i #H elim H -H //
+| #a #I #W #U #Hn #i #H elim (frees_inv_bind … H) -H
+ #H elim (IH … H) // -H -n
+ #X #HX #HnX [ @(ex2_intro … (ⓑ{a,I}X.U)) | @(ex2_intro … (ⓑ{a,I}W.X)) ] (**) (* explicit constructor *)
+ /3 width=9 by cpys_bind, nlift_bind_dx, nlift_bind_sn/
+| #I #W #U #Hn #i #H elim (frees_inv_flat … H) -H
+ #H elim (IH … H) // -H -n
+ #X #HX #HnX [ @(ex2_intro … (ⓕ{I}X.U)) | @(ex2_intro … (ⓕ{I}W.X)) ] (**) (* explicit constructor *)
+ /3 width=8 by cpys_flat, nlift_flat_dx, nlift_flat_sn/
+]
+qed-.
+
+(* Advanced negated properties **********************************************)
+
+lemma frees_lt: ∀I,L,K,W,j. ⇩[j]L ≡ K.ⓑ{I}W →
+ ∀i. j < i → (K ⊢ i-j-1 ~ϵ 𝐅*⦃W⦄ → ⊥) →
+ ∀U. (∀T. ⇧[j, 1] T ≡ U → ⊥) →
+ (L ⊢ i ~ϵ 𝐅*⦃U⦄ → ⊥).
+/4 width=9 by cofrees_inv_lt/ qed-.
+
+(* Relocation properties ****************************************************)
+
+lemma cofrees_lift_be: ∀d,e,i. d ≤ i → i ≤ d + e →
+ ∀L,K,s. ⇩[s, d, e+1] L ≡ K → ∀T,U. ⇧[d, e+1] T ≡ U →
+ L ⊢ i ~ϵ 𝐅*⦃U⦄.
+#d #e #i #Hdi #Hide #L #K #s #HLK #T1 #U1 #HTU1 #U2 #HU12
+elim (cpys_inv_lift1 … HU12 … HLK … HTU1) #T2 #HTU2 #_ -s -L -K -U1 -T1
+elim (lift_split … HTU2 i e) /2 width=2 by ex_intro/
+qed.
+
+lemma cofrees_lift_ge: ∀d,e,i. d + e ≤ i →
+ ∀L,K,s. ⇩[s, d, e] L ≡ K → ∀T,U. ⇧[d, e] T ≡ U →
+ K ⊢ i-e ~ϵ 𝐅*⦃T⦄ → L ⊢ i ~ϵ 𝐅*⦃U⦄.
+#d #e #i #Hdei #L #K #s #HLK #T1 #U1 #HTU1 #HT1 #U2 #HU12
+elim (le_inv_plus_l … Hdei) -Hdei #Hdie #Hei
+elim (cpys_inv_lift1 … HU12 … HLK … HTU1) -s -L #T2 #HTU2 #HT12
+elim (HT1 … HT12) -T1 #V2 #HVT2
+elim (lift_trans_le … HVT2 … HTU2 ?) // <plus_minus_m_m /2 width=2 by 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 *)
+(* *)
+(**************************************************************************)
+
+(* NOTATION FOR THE FORMAL SYSTEM λδ ****************************************)
+
+notation "hvbox( L ⊢ break term 46 i ~ ϵ 𝐅 * ⦃ break term 46 T ⦄ )"
+ non associative with precedence 45
+ for @{ 'CoFreeStar $L $i $T }.
--- /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/cofreestar_4.ma".
+include "basic_2/relocation/lift_neg.ma".
+include "basic_2/substitution/cpys.ma".
+
+(* CONTEXT-SENSITIVE EXCLUSION FROM FREE VARIABLES **************************)
+
+definition cofrees: relation4 ynat nat lenv term ≝
+ λd,i,L,U1. ∀U2. ⦃⋆, L⦄ ⊢ U1 ▶*[d, ∞] U2 → ∃T2. ⇧[i, 1] T2 ≡ U2.
+
+interpretation
+ "context-sensitive exclusion from free variables (term)"
+ 'CoFreeStar L i d T = (cofrees d i L T).
+
+(* Basic forward lemmas *****************************************************)
+
+lemma cofrees_fwd_lift: ∀L,U,d,i. L ⊢ i ~ϵ 𝐅*[d]⦃U⦄ → ∃T. ⇧[i, 1] T ≡ U.
+/2 width=1 by/ qed-.
+
+lemma cofrees_fwd_bind_sn: ∀a,I,L,W,U,i,d. L ⊢ i ~ϵ 𝐅*[d]⦃ⓑ{a,I}W.U⦄ →
+ L ⊢ i ~ϵ 𝐅*[d]⦃W⦄.
+#a #I #L #W1 #U #i #d #H #W2 #HW12 elim (H (ⓑ{a,I}W2.U)) /2 width=1 by cpys_bind/ -W1
+#X #H elim (lift_inv_bind2 … H) -H /2 width=2 by ex_intro/
+qed-.
+
+lemma cofrees_fwd_bind_dx: ∀a,I,L,W,U,i,d. L ⊢ i ~ϵ 𝐅*[d]⦃ⓑ{a,I}W.U⦄ →
+ L.ⓑ{I}W ⊢ i+1 ~ϵ 𝐅*[⫯d]⦃U⦄.
+#a #I #L #W #U1 #i #d #H #U2 #HU12 elim (H (ⓑ{a,I}W.U2)) /2 width=1 by cpys_bind/ -U1
+#X #H elim (lift_inv_bind2 … H) -H /2 width=2 by ex_intro/
+qed-.
+
+lemma cofrees_fwd_flat_sn: ∀I,L,W,U,i,d. L ⊢ i ~ϵ 𝐅*[d]⦃ⓕ{I}W.U⦄ →
+ L ⊢ i ~ϵ 𝐅*[d]⦃W⦄.
+#I #L #W1 #U #i #d #H #W2 #HW12 elim (H (ⓕ{I}W2.U)) /2 width=1 by cpys_flat/ -W1
+#X #H elim (lift_inv_flat2 … H) -H /2 width=2 by ex_intro/
+qed-.
+
+lemma cofrees_fwd_flat_dx: ∀I,L,W,U,i,d. L ⊢ i ~ϵ 𝐅*[d]⦃ⓕ{I}W.U⦄ →
+ L ⊢ i ~ϵ 𝐅*[d]⦃U⦄.
+#I #L #W #U1 #i #d #H #U2 #HU12 elim (H (ⓕ{I}W.U2)) /2 width=1 by cpys_flat/ -U1
+#X #H elim (lift_inv_flat2 … H) -H /2 width=2 by ex_intro/
+qed-.
+
+(* Basic inversion lemmas ***************************************************)
+
+lemma cofrees_inv_gen: ∀L,U,U0,d,i. ⦃⋆, L⦄ ⊢ U ▶*[d, ∞] U0 → (∀T. ⇧[i, 1] T ≡ U0 → ⊥) →
+ L ⊢ i ~ϵ 𝐅*[d]⦃U⦄ → ⊥.
+#L #U #U0 #d #i #HU0 #HnU0 #HU elim (HU … HU0) -L -U -d /2 width=2 by/
+qed-.
+
+lemma cofrees_inv_lref_eq: ∀L,d,i. L ⊢ i ~ϵ 𝐅*[d]⦃#i⦄ → ⊥.
+#L #d #i #H elim (H (#i)) -H //
+#X #H elim (lift_inv_lref2_be … H) -H //
+qed-.
+
+lemma cofrees_inv_bind: ∀a,I,L,W,U,i,d. L ⊢ i ~ϵ 𝐅*[d]⦃ⓑ{a,I}W.U⦄ →
+ L ⊢ i ~ϵ 𝐅*[d]⦃W⦄ ∧ L.ⓑ{I}W ⊢ i+1 ~ϵ 𝐅*[⫯d]⦃U⦄.
+/3 width=8 by cofrees_fwd_bind_sn, cofrees_fwd_bind_dx, conj/ qed-.
+
+lemma cofrees_inv_flat: ∀I,L,W,U,i,d. L ⊢ i ~ϵ 𝐅*[d]⦃ⓕ{I}W.U⦄ →
+ L ⊢ i ~ϵ 𝐅*[d]⦃W⦄ ∧ L ⊢ i ~ϵ 𝐅*[d]⦃U⦄.
+/3 width=7 by cofrees_fwd_flat_sn, cofrees_fwd_flat_dx, conj/ qed-.
+
+(* Basic Properties *********************************************************)
+
+lemma cofrees_lsuby_conf: ∀L1,U,d,i. L1 ⊢ i ~ϵ 𝐅*[d]⦃U⦄ →
+ ∀L2. L1 ⊆[d, ∞] L2 → L2 ⊢ i ~ϵ 𝐅*[d]⦃U⦄.
+/3 width=3 by lsuby_cpys_trans/ qed-.
+
+lemma cofrees_sort: ∀L,d,i,k. L ⊢ i ~ϵ 𝐅*[d]⦃⋆k⦄.
+#L #d #i #k #X #H >(cpys_inv_sort1 … H) -X /2 width=2 by ex_intro/
+qed.
+
+lemma cofrees_gref: ∀L,d,i,p. L ⊢ i ~ϵ 𝐅*[d]⦃§p⦄.
+#L #d #i #p #X #H >(cpys_inv_gref1 … H) -X /2 width=2 by ex_intro/
+qed.
+
+lemma cofrees_bind: ∀L,V,d,i. L ⊢ i ~ϵ 𝐅*[d] ⦃V⦄ →
+ ∀I,T. L.ⓑ{I}V ⊢ i+1 ~ϵ 𝐅*[⫯d]⦃T⦄ →
+ ∀a. L ⊢ i ~ϵ 𝐅*[d]⦃ⓑ{a,I}V.T⦄.
+#L #W1 #d #i #HW1 #I #U1 #HU1 #a #X #H elim (cpys_inv_bind1 … H) -H
+#W2 #U2 #HW12 #HU12 #H destruct
+elim (HW1 … HW12) elim (HU1 … HU12) -W1 -U1 /3 width=2 by lift_bind, ex_intro/
+qed.
+
+lemma cofrees_flat: ∀L,V,d,i. L ⊢ i ~ϵ 𝐅*[d]⦃V⦄ → ∀T. L ⊢ i ~ϵ 𝐅*[d]⦃T⦄ →
+ ∀I. L ⊢ i ~ϵ 𝐅*[d]⦃ⓕ{I}V.T⦄.
+#L #W1 #d #i #HW1 #U1 #HU1 #I #X #H elim (cpys_inv_flat1 … H) -H
+#W2 #U2 #HW12 #HU12 #H destruct
+elim (HW1 … HW12) elim (HU1 … HU12) -W1 -U1 /3 width=2 by lift_flat, ex_intro/
+qed.
+
+lemma cofrees_cpy_trans: ∀L,U1,U2,d. ⦃⋆, L⦄ ⊢ U1 ▶[d, ∞] U2 →
+ ∀i. L ⊢ i ~ϵ 𝐅*[d]⦃U1⦄ → L ⊢ i ~ϵ 𝐅*[d]⦃U2⦄.
+/3 width=3 by cpys_strap2/ qed-.
+
+axiom cofrees_dec: ∀L,T,d,i. Decidable (L ⊢ i ~ϵ 𝐅*[d]⦃T⦄).
+
+(* Basic negated properties *************************************************)
+
+lemma frees_cpy_div: ∀L,U1,U2,d. ⦃⋆, L⦄ ⊢ U1 ▶[d, ∞] U2 →
+ ∀i. (L ⊢ i ~ϵ 𝐅*[d]⦃U2⦄ → ⊥) → (L ⊢ i ~ϵ 𝐅*[d]⦃U1⦄ → ⊥).
+/3 width=7 by cofrees_cpy_trans/ qed-.
+
+(* Basic negated inversion lemmas *******************************************)
+
+lemma frees_inv_bind: ∀a,I,L,V,T,d,i. (L ⊢ i ~ϵ 𝐅*[d]⦃ⓑ{a,I}V.T⦄ → ⊥) →
+ (L ⊢ i ~ϵ 𝐅*[d]⦃V⦄ → ⊥) ∨ (L.ⓑ{I}V ⊢ i+1 ~ϵ 𝐅*[⫯d]⦃T⦄ → ⊥).
+#a #I #L #W #U #d #i #H elim (cofrees_dec L W d i)
+/4 width=9 by cofrees_bind, or_intror, or_introl/
+qed-.
+
+lemma frees_inv_flat: ∀I,L,V,T,d,i. (L ⊢ i ~ϵ 𝐅*[d]⦃ⓕ{I}V.T⦄ → ⊥) →
+ (L ⊢ i ~ϵ 𝐅*[d]⦃V⦄ → ⊥) ∨ (L ⊢ i ~ϵ 𝐅*[d]⦃T⦄ → ⊥).
+#I #L #W #U #d #H elim (cofrees_dec L W d)
+/4 width=8 by cofrees_flat, 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/cpy_nlift.ma".
+include "basic_2/substitution/cofrees_lift.ma".
+
+(* CONTEXT-SENSITIVE EXCLUSION FROM FREE VARIABLES **************************)
+
+(* Alternative definition of frees_ge ***************************************)
+
+lemma nlift_frees: ∀L,U,d,i. (∀T. ⇧[i, 1] T ≡ U → ⊥) → (L ⊢ i ~ϵ 𝐅*[d]⦃U⦄ → ⊥).
+#L #U #d #i #HnTU #H elim (cofrees_fwd_lift … H) -H /2 width=2 by/
+qed-.
+
+lemma frees_inv_ge: ∀L,U,d,i. d ≤ yinj i → (L ⊢ i ~ϵ 𝐅*[d]⦃U⦄ → ⊥) →
+ (∀T. ⇧[i, 1] T ≡ U → ⊥) ∨
+ ∃∃I,K,W,j. d ≤ yinj j & j < i & ⇩[j]L ≡ K.ⓑ{I}W &
+ (K ⊢ i-j-1 ~ϵ 𝐅*[yinj 0]⦃W⦄ → ⊥) & (∀T. ⇧[j, 1] T ≡ U → ⊥).
+#L #U #d #i #Hdi #H @(frees_ind … H) -U /3 width=2 by or_introl/
+#U1 #U2 #HU12 #HU2 *
+[ #HnU2 elim (cpy_fwd_nlift2_ge … HU12 … HnU2) -HU12 -HnU2 /3 width=2 by or_introl/
+ * /5 width=9 by nlift_frees, ex5_4_intro, or_intror/
+| * #I2 #K2 #W2 #j2 #Hdj2 #Hj2i #HLK2 #HnW2 #HnU2 elim (cpy_fwd_nlift2_ge … HU12 … HnU2) -HU12 -HnU2 /4 width=9 by ex5_4_intro, or_intror/
+ * #I1 #K1 #W1 #j1 #Hdj1 #Hj12 #HLK1 #HnW1 #HnU1
+ lapply (ldrop_conf_ge … HLK1 … HLK2 ?) -HLK2 /2 width=1 by lt_to_le/
+ #HK12 lapply (ldrop_inv_drop1_lt … HK12 ?) /2 width=1 by lt_plus_to_minus_r/ -HK12
+ #HK12
+ @or_intror @(ex5_4_intro … HLK1 … HnU1) -HLK1 -HnU1 /2 width=3 by transitive_lt/
+ @(frees_be … HK12 … HnW1) /2 width=1 by arith_k_sn/ -HK12 -HnW1
+ >minus_plus in ⊢ (??(?(?%?)?)??→?); >minus_plus in ⊢ (??(?(??%)?)??→?); >arith_b1 /2 width=1 by/
+]
+qed-.
+
+lemma frees_ind_ge: ∀R:relation4 ynat nat lenv term.
+ (∀d,i,L,U. d ≤ yinj i → (∀T. ⇧[i, 1] T ≡ U → ⊥) → R d i L U) →
+ (∀d,i,j,I,L,K,W,U. d ≤ yinj j → j < i → ⇩[j]L ≡ K.ⓑ{I}W → (K ⊢ i-j-1 ~ϵ 𝐅*[0]⦃W⦄ → ⊥) → (∀T. ⇧[j, 1] T ≡ U → ⊥) → R 0 (i-j-1) K W → R d i L U) →
+ ∀d,i,L,U. d ≤ yinj i → (L ⊢ i ~ϵ 𝐅*[d]⦃U⦄ → ⊥) → R d i L U.
+#R #IH1 #IH2 #d #i #L #U
+generalize in match d; -d generalize in match i; -i
+@(f2_ind … rfw … L U) -L -U
+#n #IHn #L #U #Hn #i #d #Hdi #H elim (frees_inv_ge … H) -H /3 width=2 by/
+-IH1 * #I #K #W #j #Hdj #Hji #HLK #HnW #HnU destruct /4 width=12 by ldrop_fwd_rfw/
+qed-.
--- /dev/null
+(**************************************************************************)
+(* ___ *)
+(* ||M|| *)
+(* ||A|| A project by Andrea Asperti *)
+(* ||T|| *)
+(* ||I|| Developers: *)
+(* ||T|| The HELM team. *)
+(* ||A|| http://helm.cs.unibo.it *)
+(* \ / *)
+(* \ / This file is distributed under the terms of the *)
+(* v GNU General Public License Version 2 *)
+(* *)
+(**************************************************************************)
+
+include "basic_2/substitution/cpys_lift.ma".
+include "basic_2/substitution/cofrees.ma".
+
+(* CONTEXT-SENSITIVE EXCLUSION FROM FREE VARIABLES **************************)
+
+(* Advanced inversion lemmas ************************************************)
+
+lemma cofrees_inv_lref_be: ∀L,d,i,j. L ⊢ i ~ϵ 𝐅*[d]⦃#j⦄ → d ≤ yinj j → j < i →
+ ∀I,K,W. ⇩[j]L ≡ K.ⓑ{I}W → K ⊢ i-j-1 ~ϵ 𝐅*[yinj 0]⦃W⦄.
+#L #d #i #j #Hj #Hdj #Hji #I #K #W1 #HLK #W2 #HW12 elim (lift_total W2 0 (j+1))
+#X2 #HWX2 elim (Hj X2) /2 width=7 by cpys_subst_Y2/ -I -L -K -W1 -d
+#Z2 #HZX2 elim (lift_div_le … HWX2 (i-j-1) 1 Z2) -HWX2 /2 width=2 by ex_intro/
+>minus_plus <plus_minus_m_m //
+qed-.
+
+lemma cofrees_inv_be: ∀L,U,d,i. L ⊢ i ~ϵ 𝐅*[d]⦃U⦄ → ∀j. (∀T. ⇧[j, 1] T ≡ U → ⊥) →
+ ∀I,K,W. ⇩[j]L ≡ K.ⓑ{I}W → d ≤ yinj j → j < i → K ⊢ i-j-1 ~ϵ 𝐅*[yinj 0]⦃W⦄.
+#L #U @(f2_ind … rfw … L U) -L -U
+#n #IH #L * *
+[ -IH #k #_ #d #i #_ #j #H elim (H (⋆k)) -H //
+| -IH #j #_ #d #i #Hi0 #j0 #H <(nlift_inv_lref_be_SO … H) -j0
+ /2 width=9 by cofrees_inv_lref_be/
+| -IH #p #_ #d #i #_ #j #H elim (H (§p)) -H //
+| #a #J #W #U #Hn #d #i #H1 #j #H2 #I #K #V #HLK #Hdj #Hji destruct
+ elim (cofrees_inv_bind … H1) -H1 #HW #HU
+ elim (nlift_inv_bind … H2) -H2 [ -HU /3 width=9 by/ ]
+ -HW #HnU lapply (IH … HU … HnU I K V ? ? ?)
+ /2 width=1 by ldrop_drop, yle_succ, lt_minus_to_plus/ -a -I -J -L -W -U -d
+ >minus_plus_plus_l //
+| #J #W #U #Hn #d #i #H1 #j #H2 #I #K #V #HLK #Hdj #Hji destruct
+ elim (cofrees_inv_flat … H1) -H1 #HW #HU
+ elim (nlift_inv_flat … H2) -H2 [ /3 width=9 by/ ]
+ #HnU @(IH … HU … HnU … HLK) // (**) (* full auto fails *)
+]
+qed-.
+
+(* Advanced properties ******************************************************)
+
+lemma cofrees_lref_skip: ∀L,d,i,j. j < i → yinj j < d → L ⊢ i ~ϵ 𝐅*[d]⦃#j⦄.
+#L #d #i #j #Hji #Hjd #X #H elim (cpys_inv_lref1_Y2 … H) -H
+[ #H destruct /3 width=2 by lift_lref_lt, ex_intro/
+| * #I #K #W1 #W2 #Hdj elim (ylt_yle_false … Hdj) -i -I -L -K -W1 -W2 -X //
+]
+qed.
+
+lemma cofrees_lref_lt: ∀L,d,i,j. i < j → L ⊢ i ~ϵ 𝐅*[d]⦃#j⦄.
+#L #d #i #j #Hij #X #H elim (cpys_inv_lref1_Y2 … H) -H
+[ #H destruct /3 width=2 by lift_lref_ge_minus, ex_intro/
+| * #I #K #V1 #V2 #_ #_ #_ #H -I -L -K -V1 -d
+ elim (lift_split … H i j) /2 width=2 by lt_to_le, ex_intro/
+]
+qed.
+
+lemma cofrees_lref_gt: ∀I,L,K,W,d,i,j. j < i → ⇩[j] L ≡ K.ⓑ{I}W →
+ K ⊢ (i-j-1) ~ϵ 𝐅*[O]⦃W⦄ → L ⊢ i ~ϵ 𝐅*[d]⦃#j⦄.
+#I #L #K #W1 #d #i #j #Hji #HLK #HW1 #X #H elim (cpys_inv_lref1_Y2 … H) -H
+[ #H destruct /3 width=2 by lift_lref_lt, ex_intro/
+| * #I0 #K0 #W0 #W2 #Hdj #HLK0 #HW12 #HW2 lapply (ldrop_mono … HLK0 … HLK) -L
+ #H destruct elim (HW1 … HW12) -I -K -W1 -d
+ #V2 #HVW2 elim (lift_trans_le … HVW2 … HW2) -W2 //
+ >minus_plus <plus_minus_m_m /2 width=2 by ex_intro/
+]
+qed.
+
+lemma cofrees_lref_free: ∀L,d,i,j. |L| ≤ j → j < i → L ⊢ i ~ϵ 𝐅*[d]⦃#j⦄.
+#L #d #i #j #Hj #Hji #X #H elim (cpys_inv_lref1_Y2 … H) -H
+[ #H destruct /3 width=2 by lift_lref_lt, ex_intro/
+| * #I #K #W1 #W2 #_ #HLK lapply (ldrop_fwd_length_lt2 … HLK) -I
+ #H elim (lt_refl_false j) -d -i -K -W1 -W2 -X /2 width=3 by lt_to_le_to_lt/
+]
+qed.
+
+(* Advanced negated inversion lemmas ****************************************)
+
+lemma frees_inv_lref_gt: ∀L,d,i,j. j < i → (L ⊢ i ~ϵ 𝐅*[d]⦃#j⦄ → ⊥) →
+ ∃∃I,K,W. ⇩[j] L ≡ K.ⓑ{I}W & (K ⊢ (i-j-1) ~ϵ 𝐅*[0]⦃W⦄ → ⊥) & d ≤ yinj j.
+#L #d #i #j #Hji #H elim (ylt_split j d) #Hjd
+[ elim H -H /2 width=6 by cofrees_lref_skip/
+| elim (lt_or_ge j (|L|)) #Hj
+ [ elim (ldrop_O1_lt … Hj) -Hj /4 width=10 by cofrees_lref_gt, ex3_3_intro/
+ | elim H -H /2 width=6 by cofrees_lref_free/
+ ]
+]
+qed-.
+
+lemma frees_inv_lref_free: ∀L,d,i,j. (L ⊢ i ~ϵ 𝐅*[d]⦃#j⦄ → ⊥) → |L| ≤ j → j = i.
+#L #d #i #j #H #Hj elim (lt_or_eq_or_gt i j) //
+#Hij elim H -H /2 width=6 by cofrees_lref_lt, cofrees_lref_free/
+qed-.
+
+lemma frees_inv_gen: ∀L,U,d,i. (L ⊢ i ~ϵ 𝐅*[d]⦃U⦄ → ⊥) →
+ ∃∃U0. ⦃⋆, L⦄ ⊢ U ▶*[d, ∞] U0 & (∀T. ⇧[i, 1] T ≡ U0 → ⊥).
+#L #U @(f2_ind … rfw … L U) -L -U
+#n #IH #L * *
+[ -IH #k #_ #d #i #H elim H -H //
+| #j #Hn #d #i #H elim (lt_or_eq_or_gt i j)
+ [ -n #Hij elim H -H /2 width=5 by cofrees_lref_lt/
+ | -H -n #H destruct /3 width=7 by lift_inv_lref2_be, ex2_intro/
+ | #Hji elim (frees_inv_lref_gt … H) // -H
+ #I #K #W1 #HLK #H #Hdj elim (IH … H) /2 width=3 by ldrop_fwd_rfw/ -H -n
+ #W2 #HW12 #HnW2 elim (lift_total W2 0 (j+1))
+ #U2 #HWU2 @(ex2_intro … U2) /2 width=7 by cpys_subst_Y2/ -I -L -K -W1 -d
+ #T2 #HTU2 elim (lift_div_le … HWU2 (i-j-1) 1 T2) /2 width=2 by/ -W2
+ >minus_plus <plus_minus_m_m //
+ ]
+| -IH #p #_ #d #i #H elim H -H //
+| #a #I #W #U #Hn #d #i #H elim (frees_inv_bind … H) -H
+ #H elim (IH … H) // -H -n
+ /4 width=9 by cpys_bind, nlift_bind_dx, nlift_bind_sn, ex2_intro/
+| #I #W #U #Hn #d #i #H elim (frees_inv_flat … H) -H
+ #H elim (IH … H) // -H -n
+ /4 width=9 by cpys_flat, nlift_flat_dx, nlift_flat_sn, ex2_intro/
+]
+qed-.
+
+lemma frees_ind: ∀L,d,i. ∀R:predicate term.
+ (∀U1. (∀T1. ⇧[i, 1] T1 ≡ U1 → ⊥) → R U1) →
+ (∀U1,U2. ⦃⋆, L⦄ ⊢ U1 ▶[d, ∞] U2 → (L ⊢ i ~ϵ 𝐅*[d]⦃U2⦄ → ⊥) → R U2 → R U1) →
+ ∀U. (L ⊢ i ~ϵ 𝐅*[d]⦃U⦄ → ⊥) → R U.
+#L #d #i #R #IH1 #IH2 #U1 #H elim (frees_inv_gen … H) -H
+#U2 #H #HnU2 @(cpys_ind_dx … H) -U1 /4 width=8 by cofrees_inv_gen/
+qed-.
+
+(* Advanced negated properties **********************************************)
+
+lemma frees_be: ∀I,L,K,W,j. ⇩[j]L ≡ K.ⓑ{I}W →
+ ∀i. j < i → (K ⊢ i-j-1 ~ϵ 𝐅*[yinj 0]⦃W⦄ → ⊥) →
+ ∀U. (∀T. ⇧[j, 1] T ≡ U → ⊥) →
+ ∀d. d ≤ yinj j → (L ⊢ i ~ϵ 𝐅*[d]⦃U⦄ → ⊥).
+/4 width=11 by cofrees_inv_be/ qed-.
+
+(* Relocation properties ****************************************************)
+
+lemma cofrees_lift_be: ∀d0,e0,i. d0 ≤ i → i ≤ d0 + e0 →
+ ∀L,K,s. ⇩[s, d0, e0+1] L ≡ K → ∀T,U. ⇧[d0, e0+1] T ≡ U →
+ ∀d. L ⊢ i ~ϵ 𝐅*[d]⦃U⦄.
+#d0 #e0 #i #Hd0i #Hide0 #L #K #s #HLK #T1 #U1 #HTU1 #d #U2 #HU12
+elim (yle_split d0 d) #H1
+[ elim (yle_split d (d0+e0+1)) #H2
+ [ letin cpys_inv ≝ cpys_inv_lift1_ge_up
+ | letin cpys_inv ≝ cpys_inv_lift1_ge
+ ]
+| letin cpys_inv ≝ cpys_inv_lift1_be
+]
+elim (cpys_inv … HU12 … HLK … HTU1) // #T2 #_ #HTU2 -s -L -K -U1 -T1 -d
+elim (lift_split … HTU2 i e0) /2 width=2 by ex_intro/
+qed.
+
+lemma cofrees_lift_ge: ∀d0,e0,i. d0 + e0 ≤ i →
+ ∀L,K,s. ⇩[s, d0, e0] L ≡ K → ∀T,U. ⇧[d0, e0] T ≡ U →
+ ∀d. K ⊢ i-e0 ~ϵ 𝐅*[d-yinj e0]⦃T⦄ → L ⊢ i ~ϵ 𝐅*[d]⦃U⦄.
+#d0 #e0 #i #Hde0i #L #K #s #HLK #T1 #U1 #HTU1 #d #HT1 #U2 #HU12
+elim (le_inv_plus_l … Hde0i) -Hde0i #Hd0ie0 #He0i
+elim (yle_split d0 d) #H1
+[ elim (yle_split d (d0+e0)) #H2
+ [ elim (cpys_inv_lift1_ge_up … HU12 … HLK … HTU1) // >yplus_inj >yminus_Y_inj #T2 #HT12
+ lapply (cpys_weak … HT12 (d-yinj e0) (∞) ? ?) /2 width=1 by yle_plus2_to_minus_inj2/ -HT12
+ | elim (cpys_inv_lift1_ge … HU12 … HLK … HTU1) // #T2
+ ]
+| elim (cpys_inv_lift1_be … HU12 … HLK … HTU1) // >yminus_Y_inj #T2 #HT12
+ lapply (cpys_weak … HT12 (d-yinj e0) (∞) ? ?) // -HT12
+]
+-s -L #HT12 #HTU2
+elim (HT1 … HT12) -T1 #V2 #HVT2
+elim (lift_trans_le … HVT2 … HTU2 ?) // <plus_minus_m_m /2 width=2 by 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 *)
+(* *)
+(**************************************************************************)
+
+(* NOTATION FOR THE FORMAL SYSTEM λδ ****************************************)
+
+notation "hvbox( L ⊢ break term 46 i ~ ϵ 𝐅 * [ break term 46 d ] ⦃ break term 46 T ⦄ )"
+ non associative with precedence 45
+ for @{ 'CoFreeStar $L $i $d $T }.
+++ /dev/null
-(**************************************************************************)
-(* ___ *)
-(* ||M|| *)
-(* ||A|| A project by Andrea Asperti *)
-(* ||T|| *)
-(* ||I|| Developers: *)
-(* ||T|| The HELM team. *)
-(* ||A|| http://helm.cs.unibo.it *)
-(* \ / *)
-(* \ / This file is distributed under the terms of the *)
-(* v GNU General Public License Version 2 *)
-(* *)
-(**************************************************************************)
-
-include "basic_2/substitution/cpys_alt.ma".
-include "basic_2/reduction/cpx.ma".
-
-(* CONTEXT-SENSITIVE EXTENDED PARALLEL REDUCTION FOR TERMS ******************)
-
-(* Properties on local environment refinement for extended substitution *****)
-
-lemma lsuby_cpx_trans: ∀h,g,G. lsub_trans … (cpx h g G) (lsuby 0 (∞)).
-#h #g #G #L1 #T1 #T2 #H elim H -G -L1 -T1 -T2
-[ //
-| /2 width=2 by cpx_sort/
-| #I #G #L1 #K1 #V1 #V2 #W2 #i #HLK1 #_ #HVW2 #IHV12 #L2 #HL12
- elim (lsuby_ldrop_trans_be … HL12 … HLK1) // -HL12 -HLK1 /3 width=7 by cpx_delta/
-|4,9: /4 width=1 by cpx_bind, cpx_beta, lsuby_pair_O_Y/
-|5,7,8: /3 width=1 by cpx_flat, cpx_tau, cpx_ti/
-|6,10: /4 width=3 by cpx_zeta, cpx_theta, lsuby_pair_O_Y/
-]
-qed-.
-
-(* Properties on context-sensitive extended multiple substitution for terms *)
-
-lemma cpys_cpx: ∀h,g,G,L,T1,T2,d,e. ⦃G, L⦄ ⊢ T1 ▶*[d, e] T2 → ⦃G, L⦄ ⊢ T1 ➡[h, g] T2.
-#h #g #G #L #T1 #T2 #d #e #H @(cpys_ind_alt … H) -G -L -T1 -T2 -d -e
-/2 width=7 by cpx_delta, cpx_bind, cpx_flat/
-qed.
-
-lemma cpy_cpx: ∀h,g,G,L,T1,T2,d,e. ⦃G, L⦄ ⊢ T1 ▶[d, e] T2 → ⦃G, L⦄ ⊢ T1 ➡[h, g] T2.
-/3 width=3 by cpy_cpys, cpys_cpx/ qed.
+++ /dev/null
-(**************************************************************************)
-(* ___ *)
-(* ||M|| *)
-(* ||A|| A project by Andrea Asperti *)
-(* ||T|| *)
-(* ||I|| Developers: *)
-(* ||T|| The HELM team. *)
-(* ||A|| http://helm.cs.unibo.it *)
-(* \ / *)
-(* \ / This file is distributed under the terms of the *)
-(* v GNU General Public License Version 2 *)
-(* *)
-(**************************************************************************)
-
-include "basic_2/substitution/cpys_alt.ma".
-include "basic_2/reduction/cpx.ma".
-
-(* CONTEXT-SENSITIVE EXTENDED PARALLEL REDUCTION FOR TERMS ******************)
-
-(* Properties on context-sensitive extended multiple substitution for terms *)
-
-lemma cpys_cpx: ∀h,g,G,L,T1,T2,d,e. ⦃G, L⦄ ⊢ T1 ▶*[d, e] T2 → ⦃G, L⦄ ⊢ T1 ➡[h, g] T2.
-#h #g #G #L #T1 #T2 #d #e #H @(cpys_ind_alt … H) -G -L -T1 -T2 -d -e
-/2 width=7 by cpx_delta, cpx_bind, cpx_flat/
-qed.
-
-lemma cpy_cpx: ∀h,g,G,L,T1,T2,d,e. ⦃G, L⦄ ⊢ T1 ▶[d, e] T2 → ⦃G, L⦄ ⊢ T1 ➡[h, g] T2.
-/3 width=3 by cpy_cpys, cpys_cpx/ qed.
-
-lemma cpx_cpy_trans: ∀h,g,G,L,T1,T. ⦃G, L⦄ ⊢ T1 ➡[h, g] T →
- ∀T2,d,e. ⦃G, L⦄ ⊢ T ▶[d, e] T2 → ⦃G, L⦄ ⊢ T1 ➡[h, g] T2.
-#h #g #G #L #T1 #T #H elim H -G -L -T1 -T
-[ #I #G #L #X #d #e #H elim (cpy_inv_atom1 … H) //
- * /2 width=3 by cpy_cpx/
-| #G #L #k #l #Hkl #X #d #e #H >(cpy_inv_sort1 … H) -X /2 width=2 by cpx_sort/
-| #I #G #L #K #V1 #V #W #i #HLK #_ #HVW #IHV1 #X #d #e #H
- lapply (ldrop_fwd_drop2 … HLK) #H0
- lapply (cpy_weak … H 0 (∞) ? ?) -H // #H
- elim (cpy_inv_lift1_be … H … H0 … HVW) -H -H0 -HVW
- /3 width=7 by cpx_delta/
-| #a #I #G #L #V1 #V #T1 #T #_ #_ #IHV1 #IHT1 #X #d #e #H elim (cpy_inv_bind1 … H) -H
- #V2 #T2 #HV2 #HT2 #H destruct
- /5 width=7 by cpx_bind, lsuby_cpy_trans, lsuby_succ/
-| #I #G #L #V1 #V #T1 #T #_ #_ #IHV1 #IHT1 #X #d #e #H elim (cpy_inv_flat1 … H) -H
- #V2 #T2 #HV2 #HT2 #H destruct /3 width=3 by cpx_flat/
-| #G #L #V1 #U1 #U #T #_ #HTU #IHU1 #T2 #d #e #HT2
- lapply (cpy_weak … HT2 0 (∞) ? ?) -HT2 // #HT2
- elim (lift_total T2 0 1) #U2 #HTU2
- lapply (cpy_lift_be … HT2 (L.ⓓV1) … (Ⓕ) … HTU … HTU2 ? ?) -T
- /3 width=3 by cpx_zeta, ldrop_drop/
-| /3 width=3 by cpx_tau/
-| /3 width=3 by cpx_ti/
-| #a #G #L #V1 #V #W1 #W #T1 #T #_ #_ #_ #IHV1 #IHW1 #IHT1 #X #d #e #HX
- elim (cpy_inv_bind1 … HX) -HX #Y #T2 #HY #HT2 #H destruct
- elim (cpy_inv_flat1 … HY) -HY #W2 #V2 #HW2 #HV2 #H destruct
- /5 width=7 by cpx_beta, lsuby_cpy_trans, lsuby_succ/
-| #a #G #L #V1 #V #U #W1 #W #T1 #T #_ #HVU #_ #_ #IHV1 #IHW1 #IHT1 #X #d #e #HX
- elim (cpy_inv_bind1 … HX) -HX #W2 #Y #HW2 #HY #H destruct
- elim (cpy_inv_flat1 … HY) -HY #U2 #T2 #HU2 #HT2 #H destruct
- lapply (cpy_weak … HU2 0 (∞) ? ?) -HU2 // #HU2
- elim (cpy_inv_lift1_be … HU2 L … HVU) -U
- /5 width=7 by cpx_theta, lsuby_cpy_trans, lsuby_succ, ldrop_drop/
-]
-qed-.
-
-lemma cpx_cpys_trans: ∀h,g,G,L,T1,T. ⦃G, L⦄ ⊢ T1 ➡[h, g] T →
- ∀T2,d,e. ⦃G, L⦄ ⊢ T ▶*[d, e] T2 → ⦃G, L⦄ ⊢ T1 ➡[h, g] T2.
-#h #g #G #L #T1 #T #HT1 #T2 #d #e #H @(cpys_ind … H) -T2
-/2 width=5 by cpx_cpy_trans/
-qed-.
+++ /dev/null
-(**************************************************************************)
-(* ___ *)
-(* ||M|| *)
-(* ||A|| A project by Andrea Asperti *)
-(* ||T|| *)
-(* ||I|| Developers: *)
-(* ||T|| The HELM team. *)
-(* ||A|| http://helm.cs.unibo.it *)
-(* \ / *)
-(* \ / This file is distributed under the terms of the *)
-(* v GNU General Public License Version 2 *)
-(* *)
-(**************************************************************************)
-
-include "basic_2/reduction/cpx_cpys.ma".
-include "basic_2/computation/cpxs.ma".
-
-(* CONTEXT-SENSITIVE EXTENDED PARALLEL COMPUTATION ON TERMS *****************)
-
-(* Properties on local environment refinement for extended substitution *****)
-
-lemma lsuby_cpxs_trans: ∀h,g,G. lsub_trans … (cpxs h g G) (lsuby 0 (∞)).
-/3 width=5 by lsuby_cpx_trans, LTC_lsub_trans/
-qed-.
+++ /dev/null
-include "basic_2/grammar/cl_shift.ma".
-include "basic_2/relocation/ldrop_append.ma".
-
-lemma cpy_append: ∀G,d,e. l_appendable_sn … (cpy d e G).
-#G #d #e #K #T1 #T2 #H elim H -G -K -T1 -T2 -d -e
-/2 width=1 by cpy_atom, cpy_bind, cpy_flat/
-#I #G #K #K0 #V #W #i #d #e #Hdi #Hide #HK0 #HVW #L
-lapply (ldrop_fwd_length_lt2 … HK0) #H
-@(cpy_subst I … (L@@K0) … HVW) // (**) (* /4/ does not work *)
-@(ldrop_O1_append_sn_le … HK0) /2 width=2 by lt_to_le/
-qed-.
-
-lemma cpy_fwd_shift1: ∀G,L1,L,T1,T,d,e. ⦃G, L⦄ ⊢ L1 @@ T1 ▶[d, e] T →
- ∃∃L2,T2. |L1| = |L2| & T = L2 @@ T2.
-#G #L1 @(lenv_ind_dx … L1) -L1 normalize
-[ #L #T1 #T #d #e #HT1
- @(ex2_2_intro … (⋆)) // (**) (* explicit constructor *)
-| #I #L1 #V1 #IH #L #T1 #X #d #e
- >shift_append_assoc normalize #H
- elim (cpy_inv_bind1 … H) -H
- #V0 #T0 #_ #HT10 #H destruct
- elim (IH … HT10) -IH -HT10 #L2 #T2 #HL12 #H destruct
- >append_length >HL12 -HL12
- @(ex2_2_intro … (⋆.ⓑ{I}V0@@L2) T2) [ >append_length ] (**) (* explicit constructor *)
- /2 width=3 by trans_eq/
-]
-qed-.
+++ /dev/null
-lemma cpys_append: ∀G,d,e. l_appendable_sn … (cpys d e G).
-#G #d #e #K #T1 #T2 #H @(cpys_ind … H) -T2
-/3 width=3 by cpys_strap1, cpy_append/
-qed-.
-
-lemma cpys_fwd_shift1: ∀G,L,L1,T1,T,d,e. ⦃G, L⦄ ⊢ L1 @@ T1 ▶*[d, e] T →
- ∃∃L2,T2. |L1| = |L2| & T = L2 @@ T2.
-#G #L #L1 #T1 #T #d #e #H @(cpys_ind … H) -T
-[ /2 width=4 by ex2_2_intro/
-| #T #X #_ #HX * #L0 #T0 #HL10 #H destruct
- elim (cpy_fwd_shift1 … HX) -HX #L2 #T2 #HL02 #H destruct
- /2 width=4 by ex2_2_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/cpy_lift.ma".
-include "basic_2/substitution/cpys.ma".
-include "basic_2/reduction/lpx_ldrop.ma".
-
-(* SN EXTENDED PARALLEL REDUCTION FOR LOCAL ENVIRONMENTS ********************)
-
-(* Properties on context-sensitive extended substitution for terms **********)
-
-lemma cpx_cpy_trans_lpx: ∀h,g,G,L1,T1,T. ⦃G, L1⦄ ⊢ T1 ➡[h, g] T →
- ∀L2. ⦃G, L1⦄ ⊢ ➡[h, g] L2 →
- ∀T2,d,e. ⦃G, L2⦄ ⊢ T ▶[d, e] T2 → ⦃G, L1⦄ ⊢ T1 ➡[h, g] T2.
-#h #g #G #L1 #T1 #T #H elim H -G -L1 -T1 -T
-[ #J #G #L1 #L2 #HL12 #T2 #d #e #H elim (cpy_inv_atom1 … H) -H //
- * #I #K2 #V2 #i #_ #_ #HLK2 #HVT2 #H destruct
- elim (lpx_ldrop_trans_O1 … HL12 … HLK2) -L2 #X #HLK1 #H
- elim (lpx_inv_pair2 … H) -H #K1 #V1 #_ #HV12 #H destruct
- /2 width=7 by cpx_delta/
-| #G #L1 #k #l #Hkl #L2 #_ #X #d #e #H >(cpy_inv_sort1 … H) -X /2 width=2 by cpx_sort/
-| #I #G #L1 #K1 #V1 #V #T #i #HLK1 #_ #HVT #IHV1 #L2 #HL12 #T2 #d #e #HT2
- elim (lpx_ldrop_conf … HLK1 … HL12) -HL12 #X #H #HLK2
- elim (lpx_inv_pair1 … H) -H #K2 #V0 #HK12 #_ #H destruct
- lapply (ldrop_fwd_drop2 … HLK2) -V0 #HLK2
- lapply (cpy_weak … HT2 0 (∞) ? ?) -HT2 // #HT2
- elim (cpy_inv_lift1_be … HT2 … HLK2 … HVT) -HT2 -HLK2 -HVT
- /3 width=7 by cpx_delta/
-| #a #I #G #L1 #V1 #V #T1 #T #HV1 #_ #IHV1 #IHT1 #L2 #HL12 #X #d #e #H elim (cpy_inv_bind1 … H) -H
- #V2 #T2 #HV2 #HT2 #H destruct /4 width=5 by lpx_pair, cpx_bind/
-| #I #G #L1 #V1 #V #T1 #T #_ #_ #IHV1 #IHT1 #L2 #HL12 #X #d #e #H elim (cpy_inv_flat1 … H) -H
- #V2 #T2 #HV2 #HT2 #H destruct /3 width=5 by cpx_flat/
-| #G #L1 #V1 #U1 #U #T #_ #HTU #IHU1 #L2 #HL12 #T2 #d #e #HT2
- lapply (cpy_weak … HT2 0 (∞) ? ?) -HT2 // #HT2
- elim (lift_total T2 0 1) #U2 #HTU2
- lapply (cpy_lift_be … HT2 (L2.ⓓV1) … (Ⓕ) … HTU … HTU2 ? ?) -T
- /4 width=5 by cpx_zeta, lpx_pair, ldrop_drop/
-| /3 width=5 by cpx_tau/
-| /3 width=5 by cpx_ti/
-| #a #G #L1 #V1 #V #W1 #W #T1 #T #HV1 #HW1 #_ #IHV1 #IHW1 #IHT1 #L2 #HL12 #X #d #e #HX
- elim (cpy_inv_bind1 … HX) -HX #Y #T2 #HY #HT2 #H destruct
- elim (cpy_inv_flat1 … HY) -HY #W2 #V2 #HW2 #HV2 #H destruct
- /5 width=11 by lpx_pair, cpx_beta, lsuby_cpy_trans, lsuby_succ/
-| #a #G #L1 #V1 #V #U #W1 #W #T1 #T #_ #HVU #HW1 #_ #IHV1 #IHW1 #IHT1 #L2 #HL12 #X #d #e #HX
- elim (cpy_inv_bind1 … HX) -HX #W2 #Y #HW2 #HY #H destruct
- elim (cpy_inv_flat1 … HY) -HY #U2 #T2 #HU2 #HT2 #H destruct
- lapply (cpy_weak … HU2 0 (∞) ? ?) -HU2 // #HU2
- elim (cpy_inv_lift1_be … HU2 L2 … HVU) -U
- /4 width=7 by lpx_pair, cpx_theta, ldrop_drop/
-]
-qed-.
-
-lemma cpx_cpys_trans_lpx: ∀h,g,G,L1,T1,T. ⦃G, L1⦄ ⊢ T1 ➡[h, g] T →
- ∀L2. ⦃G, L1⦄ ⊢ ➡[h, g] L2 →
- ∀T2,d,e. ⦃G, L2⦄ ⊢ T ▶*[d, e] T2 → ⦃G, L1⦄ ⊢ T1 ➡[h, g] T2.
-#h #g #G #L1 #T1 #T #HT1 #L2 #HL12 #T2 #d #e #H @(cpys_ind … H) -T2
-/2 width=7 by cpx_cpy_trans_lpx/
-qed-.
+++ /dev/null
-(*
-lemma lsuby_weak: ∀L1,L2,d1,e1. L1 ⊑×[d1, e1] L2 →
- ∀d2,e2. d1 ≤ d2 → e2 ≤ e1 → L1 ⊑×[d2, e2] L2.
-#L1 #L2 #d1 #e1 #H elim H -L1 -L2 -d1 -e1 //
-[ #I1 #I2 #L1 #L2 #V1 #V2 #HL12 #_ #d2 #e2 #_ #He21
- >(yle_inv_O2 … He21) -He21
- /4 width=3 by lsuby_fwd_length, lsuby_O1, monotonic_le_plus_l/
-| #I1 #I2 #L1 #L2 #V #e #HL12 #IHL12 #d2 #e2 #_ #He21
- elim (ynat_cases e2) /4 width=3 by lsuby_fwd_length, lsuby_O1, monotonic_le_plus_l/
- * #e0 #H destruct lapply (yle_inv_succ … He21) -He21 #He21
- elim (ynat_cases d2) /3 width=1 by lsuby_pair/
- * #d0 #H destruct @lsuby_succ @IHL12 //
- [ 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/notation/relations/extpsubststar_4.ma".
-include "basic_2/grammar/genv.ma".
-include "basic_2/grammar/cl_shift.ma".
-include "basic_2/relocation/ldrop_append.ma".
-include "basic_2/relocation/lsuby.ma".
-
-(* CONTEXT-SENSITIVE EXTENDED MULTIPLE SUBSTITUTION FOR TERMS ***************)
-
-(* avtivate genv *)
-inductive cpys: relation4 genv lenv term term ≝
-| cpys_atom : ∀I,G,L. cpys G L (⓪{I}) (⓪{I})
-| cpys_delta: ∀I,G,L,K,V,V2,W2,i.
- ⇩[0, i] L ≡ K.ⓑ{I}V → cpys G K V V2 →
- ⇧[0, i + 1] V2 ≡ W2 → cpys G L (#i) W2
-| cpys_bind : ∀a,I,G,L,V1,V2,T1,T2.
- cpys G L V1 V2 → cpys G (L.ⓑ{I}V1) T1 T2 →
- cpys G L (ⓑ{a,I}V1.T1) (ⓑ{a,I}V2.T2)
-| cpys_flat : ∀I,G,L,V1,V2,T1,T2.
- cpys G L V1 V2 → cpys G L T1 T2 →
- cpys G L (ⓕ{I}V1.T1) (ⓕ{I}V2.T2)
-.
-
-interpretation
- "context-sensitive extended multiple substitution (term)"
- 'ExtPSubstStar G L T1 T2 = (cpys G L T1 T2).
-
-(* Basic properties *********************************************************)
-
-lemma lsuby_cpys_trans: ∀G. lsub_trans … (cpys G) lsuby.
-#G #L1 #T1 #T2 #H elim H -G -L1 -T1 -T2
-[ //
-| #I #G #L1 #K1 #V1 #V2 #W2 #i #HLK1 #_ #HVW2 #IHV12 #L2 #HL12
- elim (lsuby_fwd_ldrop2_pair … HL12 … HLK1) -HL12 -HLK1 *
- /3 width=7 by cpys_delta/
-| /4 width=1 by lsuby_pair, cpys_bind/
-| /3 width=1 by cpys_flat/
-]
-qed-.
-
-(* Note: this is "∀L. reflexive … (cpys L)" *)
-lemma cpys_refl: ∀G,T,L. ⦃G, L⦄ ⊢ T ▶*× T.
-#G #T elim T -T // * /2 width=1 by cpys_bind, cpys_flat/
-qed.
-
-lemma cpys_pair_sn: ∀I,G,L,V1,V2. ⦃G, L⦄ ⊢ V1 ▶*× V2 →
- ∀T. ⦃G, L⦄ ⊢ ②{I}V1.T ▶*× ②{I}V2.T.
-* /2 width=1 by cpys_bind, cpys_flat/
-qed.
-
-lemma cpys_bind_ext: ∀G,L,V1,V2. ⦃G, L⦄ ⊢ V1 ▶*× V2 →
- ∀J,T1,T2. ⦃G, L.ⓑ{J}V1⦄ ⊢ T1 ▶*× T2 →
- ∀a,I. ⦃G, L⦄ ⊢ ⓑ{a,I}V1.T1 ▶*× ⓑ{a,I}V2.T2.
-/4 width=4 by lsuby_cpys_trans, cpys_bind, lsuby_pair/ qed.
-
-lemma cpys_delift: ∀I,G,K,V,T1,L,d. ⇩[0, d] L ≡ (K.ⓑ{I}V) →
- ∃∃T2,T. ⦃G, L⦄ ⊢ T1 ▶*× T2 & ⇧[d, 1] T ≡ T2.
-#I #G #K #V #T1 elim T1 -T1
-[ * /2 width=4 by cpys_atom, lift_sort, lift_gref, ex2_2_intro/
- #i #L #d elim (lt_or_eq_or_gt i d) #Hid [1,3: /3 width=4 by cpys_atom, lift_lref_ge_minus, lift_lref_lt, ex2_2_intro/ ]
- destruct
- elim (lift_total V 0 (i+1)) #W #HVW
- elim (lift_split … HVW i i) /3 width=7 by cpys_delta, ex2_2_intro/
-| * [ #a ] #I #W1 #U1 #IHW1 #IHU1 #L #d #HLK
- elim (IHW1 … HLK) -IHW1 #W2 #W #HW12 #HW2
- [ elim (IHU1 (L. ⓑ{I}W1) (d+1)) -IHU1 /3 width=9 by cpys_bind, ldrop_ldrop, lift_bind, ex2_2_intro/
- | elim (IHU1 … HLK) -IHU1 -HLK /3 width=8 by cpys_flat, lift_flat, ex2_2_intro/
- ]
-]
-qed-.
-
-lemma cpys_append: ∀G. l_appendable_sn … (cpys G).
-#G #K #T1 #T2 #H elim H -G -K -T1 -T2
-/2 width=3 by cpys_bind, cpys_flat/
-#I #G #K #K0 #V1 #V2 #W2 #i #HK0 #_ #HVW2 #IHV12 #L
-lapply (ldrop_fwd_length_lt2 … HK0) #H
-@(cpys_delta … I … (L@@K0) V1 … HVW2) //
-@(ldrop_O1_append_sn_le … HK0) /2 width=2 by lt_to_le/ (**) (* /3/ does not work *)
-qed.
-
-(* Basic inversion lemmas ***************************************************)
-
-fact cpys_inv_atom1_aux: ∀G,L,T1,T2. ⦃G, L⦄ ⊢ T1 ▶*× T2 → ∀J. T1 = ⓪{J} →
- T2 = ⓪{J} ∨
- ∃∃I,K,V,V2,i. ⇩[O, i] L ≡ K.ⓑ{I}V & ⦃G, K⦄ ⊢ V ▶*× V2 &
- ⇧[O, i + 1] V2 ≡ T2 & J = LRef i.
-#G #L #T1 #T2 * -L -T1 -T2
-[ #I #G #L #J #H destruct /2 width=1 by or_introl/
-| #I #G #L #K #V #V2 #T2 #i #HLK #HV2 #HVT2 #J #H destruct /3 width=9 by ex4_5_intro, or_intror/
-| #a #I #G #L #V1 #V2 #T1 #T2 #_ #_ #J #H destruct
-| #I #G #L #V1 #V2 #T1 #T2 #_ #_ #J #H destruct
-]
-qed-.
-
-lemma cpys_inv_atom1: ∀J,G,L,T2. ⦃G, L⦄ ⊢ ⓪{J} ▶*× T2 →
- T2 = ⓪{J} ∨
- ∃∃I,K,V,V2,i. ⇩[O, i] L ≡ K.ⓑ{I}V & ⦃G, K⦄ ⊢ V ▶*× V2 &
- ⇧[O, i + 1] V2 ≡ T2 & J = LRef i.
-/2 width=3 by cpys_inv_atom1_aux/ qed-.
-
-lemma cpys_inv_sort1: ∀G,L,T2,k. ⦃G, L⦄ ⊢ ⋆k ▶*× T2 → T2 = ⋆k.
-#G #L #T2 #k #H elim (cpys_inv_atom1 … H) -H // *
-#I #K #V #V2 #i #_ #_ #_ #H destruct
-qed-.
-
-lemma cpys_inv_lref1: ∀G,L,T2,i. ⦃G, L⦄ ⊢ #i ▶*× T2 →
- T2 = #i ∨
- ∃∃I,K,V,V2. ⇩[O, i] L ≡ K. ⓑ{I}V & ⦃G, K⦄ ⊢ V ▶*× V2 &
- ⇧[O, i + 1] V2 ≡ T2.
-#G #L #T2 #i #H elim (cpys_inv_atom1 … H) -H /2 width=1 by or_introl/ *
-#I #K #V #V2 #j #HLK #HV2 #HVT2 #H destruct /3 width=7 by ex3_4_intro, or_intror/
-qed-.
-
-lemma cpys_inv_lref1_ge: ∀G,L,T2,i. ⦃G, L⦄ ⊢ #i ▶*× T2 → |L| ≤ i → T2 = #i.
-#G #L #T2 #i #H elim (cpys_inv_lref1 … H) -H // *
-#I #K #V1 #V2 #HLK #_ #_ #HL -V2 lapply (ldrop_fwd_length_lt2 … HLK) -K -I -V1
-#H elim (lt_refl_false i) /2 width=3 by lt_to_le_to_lt/
-qed-.
-
-lemma cpys_inv_gref1: ∀G,L,T2,p. ⦃G, L⦄ ⊢ §p ▶*× T2 → T2 = §p.
-#G #L #T2 #p #H elim (cpys_inv_atom1 … H) -H // *
-#I #K #V #V2 #i #_ #_ #_ #H destruct
-qed-.
-
-fact cpys_inv_bind1_aux: ∀G,L,U1,U2. ⦃G, L⦄ ⊢ U1 ▶*× U2 →
- ∀a,J,V1,T1. U1 = ⓑ{a,J}V1.T1 →
- ∃∃V2,T2. ⦃G, L⦄ ⊢ V1 ▶*× V2 & ⦃G, L.ⓑ{J}V1⦄ ⊢ T1 ▶*× T2 &
- U2 = ⓑ{a,J}V2.T2.
-#G #L #U1 #U2 * -L -U1 -U2
-[ #I #G #L #b #J #W #U1 #H destruct
-| #I #G #L #K #V #V2 #W2 #i #_ #_ #_ #b #J #W #U1 #H destruct
-| #a #I #G #L #V1 #V2 #T1 #T2 #HV12 #HT12 #b #J #W #U1 #H destruct /2 width=5 by ex3_2_intro/
-| #I #G #L #V1 #V2 #T1 #T2 #_ #_ #b #J #W #U1 #H destruct
-]
-qed-.
-
-lemma cpys_inv_bind1: ∀a,I,G,L,V1,T1,U2. ⦃G, L⦄ ⊢ ⓑ{a,I}V1.T1 ▶*× U2 →
- ∃∃V2,T2. ⦃G, L⦄ ⊢ V1 ▶*× V2 & ⦃G, L.ⓑ{I}V1⦄ ⊢ T1 ▶*× T2 &
- U2 = ⓑ{a,I}V2.T2.
-/2 width=3 by cpys_inv_bind1_aux/ qed-.
-
-lemma cpys_inv_bind1_ext: ∀a,I,G,L,V1,T1,U2. ⦃G, L⦄ ⊢ ⓑ{a,I}V1.T1 ▶*× U2 → ∀J.
- ∃∃V2,T2. ⦃G, L⦄ ⊢ V1 ▶*× V2 & ⦃G, L.ⓑ{J}V1⦄ ⊢ T1 ▶*× T2 &
- U2 = ⓑ{a,I}V2.T2.
-#a #I #G #L #V1 #T1 #U2 #H #J elim (cpys_inv_bind1 … H) -H
-#V2 #T2 #HV12 #HT12 #H destruct
-/4 width=5 by lsuby_cpys_trans, lsuby_pair, ex3_2_intro/
-qed-.
-
-fact cpys_inv_flat1_aux: ∀G,L,U,U2. ⦃G, L⦄ ⊢ U ▶*× U2 →
- ∀J,V1,U1. U = ⓕ{J}V1.U1 →
- ∃∃V2,T2. ⦃G, L⦄ ⊢ V1 ▶*× V2 & ⦃G, L⦄ ⊢ U1 ▶*× T2 &
- U2 = ⓕ{J}V2.T2.
-#G #L #U #U2 * -L -U -U2
-[ #I #G #L #J #W #U1 #H destruct
-| #I #G #L #K #V #V2 #W2 #i #_ #_ #_ #J #W #U1 #H destruct
-| #a #I #G #L #V1 #V2 #T1 #T2 #_ #_ #J #W #U1 #H destruct
-| #I #G #L #V1 #V2 #T1 #T2 #HV12 #HT12 #J #W #U1 #H destruct /2 width=5 by ex3_2_intro/
-]
-qed-.
-
-lemma cpys_inv_flat1: ∀I,G,L,V1,U1,U2. ⦃G, L⦄ ⊢ ⓕ{I}V1.U1 ▶*× U2 →
- ∃∃V2,T2. ⦃G, L⦄ ⊢ V1 ▶*× V2 & ⦃G, L⦄ ⊢ U1 ▶*× T2 &
- U2 = ⓕ{I}V2.T2.
-/2 width=3 by cpys_inv_flat1_aux/ qed-.
-
-(* Basic forward lemmas *****************************************************)
-
-lemma cpys_fwd_bind1: ∀a,I,G,L,V1,T1,T. ⦃G, L⦄ ⊢ ⓑ{a,I}V1.T1 ▶*× T → ∀b,J.
- ∃∃V2,T2. ⦃G, L⦄ ⊢ ⓑ{b,J}V1.T1 ▶*× ⓑ{b,J}V2.T2 &
- T = ⓑ{a,I}V2.T2.
-#a #I #G #L #V1 #T1 #T #H #b #J elim (cpys_inv_bind1_ext … H J) -H
-#V2 #T2 #HV12 #HT12 #H destruct /3 width=4 by cpys_bind, ex2_2_intro/
-qed-.
-
-lemma cpys_fwd_shift1: ∀G,L1,L,T1,T. ⦃G, L⦄ ⊢ L1 @@ T1 ▶*× T →
- ∃∃L2,T2. |L1| = |L2| & T = L2 @@ T2.
-#G #L1 @(lenv_ind_dx … L1) -L1 normalize
-[ #L #T1 #T #HT1 @(ex2_2_intro … (⋆)) // (**) (* explicit constructor *)
-| #I #L1 #V1 #IH #L #T1 #X >shift_append_assoc normalize
- #H elim (cpys_inv_bind1 … H) -H
- #V0 #T0 #_ #HT10 #H destruct
- elim (IH … HT10) -IH -HT10 #L2 #T2 #HL12 #H destruct
- >append_length >HL12 -HL12
- @(ex2_2_intro … (⋆.ⓑ{I}V0@@L2) T2) [ >append_length ] /2 width=3 by trans_eq/ (**) (* explicit constructor *)
-]
-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/lpx_sn_lpx_sn.ma".
-include "basic_2/substitution/fqup.ma".
-include "basic_2/substitution/lpys_ldrop.ma".
-
-(* CONTEXT-SENSITIVE EXTENDED MULTIPLE SUBSTITUTION FOR TERMS ***************)
-
-(* Main properties **********************************************************)
-
-theorem cpys_antisym: ∀G,L,T1,T2. ⦃G, L⦄ ⊢ T1 ▶*× T2 → ⦃G, L⦄ ⊢ T2 ▶*× T1 → T1 = T2.
-#G #L #T1 #T2 #H elim H -G -L -T1 -T2 //
-[ #I #G #L #K #V1 #V2 #W2 #i #HLK #_ #HVW2 #_ #HW2 lapply (ldrop_fwd_ldrop2 … HLK) -I -V1
- #HLK elim (cpys_inv_lift1 … HW2 … HLK … HVW2) -L -HVW2
- #X #H #_ elim (lift_inv_lref2_be … H) -G -K -V2 -W2 -X //
-| #a #I #G #L #V1 #V2 #T1 #T2 #_ #_ #IHV12 #IHT12 #H elim (cpys_inv_bind1 … H) -H
- #V #T #HV2 #HT2 #H destruct
- lapply (IHV12 HV2) #H destruct -IHV12 -HV2 /3 width=1 by eq_f2/
-| #I #G #L #V1 #V2 #T1 #T2 #_ #_ #IHV12 #IHT12 #H elim (cpys_inv_flat1 … H) -H
- #V #T #HV2 #HT2 #H destruct /3 width=1 by eq_f2/
-]
-qed-.
-
-theorem cpys_trans_lpys: ∀G. lpx_sn_transitive (cpys G) (cpys G).
-#G0 #L0 #T0 @(fqup_wf_ind_eq … G0 L0 T0) -G0 -L0 -T0 #G0 #L0 #T0 #IH #G1 #L1 * [|*]
-[ #I #HG #HL #HT #T #H1 #L2 #HL12 #T2 #HT2 destruct
- elim (cpys_inv_atom1 … H1) -H1
- [ #H destruct
- elim (cpys_inv_atom1 … HT2) -HT2
- [ #H destruct //
- | * #I2 #K2 #V #V2 #i #HLK2 #HV2 #HVT2 #H destruct
- elim (lpys_ldrop_trans_O1 … HL12 … HLK2) -L2 #X #HLK1 #H
- elim (lpys_inv_pair2 … H) -H #K1 #V1 #HK12 #HV1 #H destruct
- lapply (fqup_lref … G1 … HLK1) /3 width=10 by cpys_delta/
- ]
- | * #I1 #K1 #V1 #V #i #HLK1 #HV1 #HVT #H destruct
- elim (lpys_ldrop_conf … HLK1 … HL12) -HL12 #X #H #HLK2
- elim (lpys_inv_pair1 … H) -H #K2 #W2 #HK12 #_ #H destruct
- lapply (ldrop_fwd_ldrop2 … HLK2) -W2 #HLK2
- elim (cpys_inv_lift1 … HT2 … HLK2 … HVT) -L2 -T
- lapply (fqup_lref … G1 … HLK1) /3 width=10 by cpys_delta/
- ]
-| #a #I #V1 #T1 #HG #HL #HT #X1 #H1 #L2 #HL12 #X2 #H2
- elim (cpys_inv_bind1 … H1) -H1 #V #T #HV1 #HT1 #H destruct
- elim (cpys_inv_bind1 … H2) -H2 #V2 #T2 #HV2 #HT2 #H destruct
- /4 width=5 by cpys_bind, lpys_pair/
-| #I #V1 #T1 #HG #HL #HT #X1 #H1 #L2 #HL12 #X2 #H2
- elim (cpys_inv_flat1 … H1) -H1 #V #T #HV1 #HT1 #H destruct
- elim (cpys_inv_flat1 … H2) -H2 #V2 #T2 #HV2 #HT2 #H destruct
- /3 width=5 by cpys_flat/
-]
-qed-.
-
-theorem cpys_trans: ∀G,L. Transitive … (cpys G L).
-/2 width=5 by cpys_trans_lpys/ qed-.
-
-(* Advanced properties ******************************************************)
-
-lemma lpys_cpys_trans: ∀G. lsub_trans … (cpys G) (lpys G).
-/2 width=5 by cpys_trans_lpys/ 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/fqus_alt.ma".
-include "basic_2/substitution/cpys.ma".
-
-(* CONTEXT-SENSITIVE EXTENDED MULTIPLE SUBSTITUTION FOR TERMS ***************)
-
-(* Relocation properties ****************************************************)
-
-lemma cpys_lift: ∀G. l_liftable (cpys G).
-#G #K #T1 #T2 #H elim H -G -K -T1 -T2
-[ #I #G #K #L #d #e #_ #U1 #H1 #U2 #H2
- >(lift_mono … H1 … H2) -H1 -H2 //
-| #I #G #K #KV #V #V2 #W2 #i #HKV #HV2 #HVW2 #IHV2 #L #d #e #HLK #U1 #H #U2 #HWU2
- elim (lift_inv_lref1 … H) * #Hid #H destruct
- [ elim (lift_trans_ge … HVW2 … HWU2) -W2 // <minus_plus #W2 #HVW2 #HWU2
- elim (ldrop_trans_le … HLK … HKV) -K /2 width=2 by lt_to_le/ #X #HLK #H
- elim (ldrop_inv_skip2 … H) -H /2 width=1 by lt_plus_to_minus_r/ -Hid #K #Y #HKV #HVY #H destruct /3 width=9 by cpys_delta/
- | lapply (lift_trans_be … HVW2 … HWU2 ? ?) -W2 /2 width=1 by le_S/ >plus_plus_comm_23 #HVU2
- lapply (ldrop_trans_ge_comm … HLK … HKV ?) -K /3 width=7 by cpys_delta/
- ]
-| #a #I #G #K #V1 #V2 #T1 #T2 #_ #_ #IHV12 #IHT12 #L #d #e #HLK #U1 #H1 #U2 #H2
- elim (lift_inv_bind1 … H1) -H1 #VV1 #TT1 #HVV1 #HTT1 #H1 destruct
- elim (lift_inv_bind1 … H2) -H2 #VV2 #TT2 #HVV2 #HTT2 #H2 destruct /4 width=5 by cpys_bind, ldrop_skip/
-| #I #G #K #V1 #V2 #T1 #T2 #_ #_ #IHV12 #IHT12 #L #d #e #HLK #U1 #H1 #U2 #H2
- elim (lift_inv_flat1 … H1) -H1 #VV1 #TT1 #HVV1 #HTT1 #H1 destruct
- elim (lift_inv_flat1 … H2) -H2 #VV2 #TT2 #HVV2 #HTT2 #H2 destruct /3 width=6 by cpys_flat/
-]
-qed.
-
-lemma cpys_inv_lift1: ∀G. l_deliftable_sn (cpys G).
-#G #L #U1 #U2 #H elim H -G -L -U1 -U2
-[ * #G #L #i #K #d #e #_ #T1 #H
- [ lapply (lift_inv_sort2 … H) -H #H destruct /2 width=3 by cpys_atom, lift_sort, ex2_intro/
- | elim (lift_inv_lref2 … H) -H * #Hid #H destruct /3 width=3 by cpys_atom, lift_lref_ge_minus, lift_lref_lt, ex2_intro/
- | lapply (lift_inv_gref2 … H) -H #H destruct /2 width=3 by cpys_atom, lift_gref, ex2_intro/
- ]
-| #I #G #L #LV #V #V2 #W2 #i #HLV #HV2 #HVW2 #IHV2 #K #d #e #HLK #T1 #H
- elim (lift_inv_lref2 … H) -H * #Hid #H destruct
- [ elim (ldrop_conf_lt … HLK … HLV) -L // #L #U #HKL #HLV #HUV
- elim (IHV2 … HLV … HUV) -V #U2 #HUV2 #HU2
- elim (lift_trans_le … HUV2 … HVW2) -V2 // >minus_plus <plus_minus_m_m /3 width=9 by cpys_delta, ex2_intro/
- | elim (le_inv_plus_l … Hid) #Hdie #Hei
- lapply (ldrop_conf_ge … HLK … HLV ?) -L // #HKLV
- elim (lift_split … HVW2 d (i - e + 1)) -HVW2 /3 width=1 by le_S, le_S_S/ -Hid -Hdie
- #V1 #HV1 >plus_minus // <minus_minus /2 width=1 by le_S/ <minus_n_n <plus_n_O /3 width=9 by cpys_delta, ex2_intro/
- ]
-| #a #I #G #L #V1 #V2 #U1 #U2 #_ #_ #IHV12 #IHU12 #K #d #e #HLK #X #H
- elim (lift_inv_bind2 … H) -H #W1 #T1 #HWV1 #HTU1 #H destruct
- elim (IHV12 … HLK … HWV1) -IHV12 #W2 #HW12 #HWV2
- elim (IHU12 … HTU1) -IHU12 -HTU1 /3 width=5 by cpys_bind, ldrop_skip, lift_bind, ex2_intro/
-| #I #G #L #V1 #V2 #U1 #U2 #_ #_ #IHV12 #IHU12 #K #d #e #HLK #X #H
- elim (lift_inv_flat2 … H) -H #W1 #T1 #HWV1 #HTU1 #H destruct
- elim (IHV12 … HLK … HWV1) -V1
- elim (IHU12 … HLK … HTU1) -U1 -HLK /3 width=5 by cpys_flat, lift_flat, ex2_intro/
-]
-qed-.
-
-(* Properties on supclosure *************************************************)
-
-lemma fqu_cpys_trans: ∀G1,G2,L1,L2,T1,T2. ⦃G1, L1, T1⦄ ⊃ ⦃G2, L2, T2⦄ →
- ∀U2. ⦃G2, L2⦄ ⊢ T2 ▶*× U2 →
- ∃∃U1. ⦃G1, L1⦄ ⊢ T1 ▶*× U1 & ⦃G1, L1, U1⦄ ⊃ ⦃G2, L2, U2⦄.
-#G1 #G2 #L1 #L2 #T1 #T2 #H elim H -G1 -G2 -L1 -L2 -T1 -T2
-/3 width=3 by fqu_pair_sn, fqu_bind_dx, fqu_flat_dx, cpys_pair_sn, cpys_bind, cpys_flat, ex2_intro/
-[ #I #G #L #V2 #U2 #HVU2
- elim (lift_total U2 0 1)
- /4 width=7 by fqu_drop, cpys_delta, ldrop_pair, ldrop_ldrop, ex2_intro/
-| #G #L #K #T1 #U1 #e #HLK1 #HTU1 #T2 #HTU2
- elim (lift_total T2 0 (e+1))
- /3 width=11 by cpys_lift, fqu_drop, ex2_intro/
-]
-qed-.
-
-lemma fquq_cpys_trans: ∀G1,G2,L1,L2,T1,T2. ⦃G1, L1, T1⦄ ⊃⸮ ⦃G2, L2, T2⦄ →
- ∀U2. ⦃G2, L2⦄ ⊢ T2 ▶*× U2 →
- ∃∃U1. ⦃G1, L1⦄ ⊢ T1 ▶*× U1 & ⦃G1, L1, U1⦄ ⊃⸮ ⦃G2, L2, U2⦄.
-#G1 #G2 #L1 #L2 #T1 #T2 #H #U2 #HTU2 elim (fquq_inv_gen … H) -H
-[ #HT12 elim (fqu_cpys_trans … HT12 … HTU2) /3 width=3 by fqu_fquq, ex2_intro/
-| * #H1 #H2 #H3 destruct /2 width=3 by ex2_intro/
-]
-qed-.
-
-lemma fqup_cpys_trans: ∀G1,G2,L1,L2,T1,T2. ⦃G1, L1, T1⦄ ⊃+ ⦃G2, L2, T2⦄ →
- ∀U2. ⦃G2, L2⦄ ⊢ T2 ▶*× U2 →
- ∃∃U1. ⦃G1, L1⦄ ⊢ T1 ▶*× U1 & ⦃G1, L1, U1⦄ ⊃+ ⦃G2, L2, U2⦄.
-#G1 #G2 #L1 #L2 #T1 #T2 #H @(fqup_ind … H) -G2 -L2 -T2
-[ #G2 #L2 #T2 #H12 #U2 #HTU2 elim (fqu_cpys_trans … H12 … HTU2) -T2
- /3 width=3 by fqu_fqup, ex2_intro/
-| #G #G2 #L #L2 #T #T2 #_ #HT2 #IHT1 #U2 #HTU2
- elim (fqu_cpys_trans … HT2 … HTU2) -T2 #T2 #HT2 #HTU2
- elim (IHT1 … HT2) -T /3 width=7 by fqup_strap1, ex2_intro/
-]
-qed-.
-
-lemma fqus_cpys_trans: ∀G1,G2,L1,L2,T1,T2. ⦃G1, L1, T1⦄ ⊃* ⦃G2, L2, T2⦄ →
- ∀U2. ⦃G2, L2⦄ ⊢ T2 ▶*× U2 →
- ∃∃U1. ⦃G1, L1⦄ ⊢ T1 ▶*× U1 & ⦃G1, L1, U1⦄ ⊃* ⦃G2, L2, U2⦄.
-#G1 #G2 #L1 #L2 #T1 #T2 #H #U2 #HTU2 elim (fqus_inv_gen … H) -H
-[ #HT12 elim (fqup_cpys_trans … HT12 … HTU2) /3 width=3 by fqup_fqus, ex2_intro/
-| * #H1 #H2 #H3 destruct /2 width=3 by ex2_intro/
-]
-qed-.
-
-lemma fqu_cpys_trans_neq: ∀G1,G2,L1,L2,T1,T2. ⦃G1, L1, T1⦄ ⊃ ⦃G2, L2, T2⦄ →
- ∀U2. ⦃G2, L2⦄ ⊢ T2 ▶*× U2 → (T2 = U2 → ⊥) →
- ∃∃U1. ⦃G1, L1⦄ ⊢ T1 ▶*× U1 & T1 = U1 → ⊥ & ⦃G1, L1, U1⦄ ⊃ ⦃G2, L2, U2⦄.
-#G1 #G2 #L1 #L2 #T1 #T2 #H elim H -G1 -G2 -L1 -L2 -T1 -T2
-[ #I #G #L #V1 #V2 #HV12 #_ elim (lift_total V2 0 1)
- #U2 #HVU2 @(ex3_intro … U2)
- [1,3: /3 width=7 by fqu_drop, cpys_delta, ldrop_pair, ldrop_ldrop/
- | #H destruct /2 width=7 by lift_inv_lref2_be/
- ]
-| #I #G #L #V1 #T #V2 #HV12 #H @(ex3_intro … (②{I}V2.T))
- [1,3: /2 width=4 by fqu_pair_sn, cpys_pair_sn/
- | #H0 destruct /2 width=1 by/
- ]
-| #a #I #G #L #V #T1 #T2 #HT12 #H @(ex3_intro … (ⓑ{a,I}V.T2))
- [1,3: /2 width=4 by fqu_bind_dx, cpys_bind/
- | #H0 destruct /2 width=1 by/
- ]
-| #I #G #L #V #T1 #T2 #HT12 #H @(ex3_intro … (ⓕ{I}V.T2))
- [1,3: /2 width=4 by fqu_flat_dx, cpys_flat/
- | #H0 destruct /2 width=1 by/
- ]
-| #G #L #K #T1 #U1 #e #HLK #HTU1 #T2 #HT12 #H elim (lift_total T2 0 (e+1))
- #U2 #HTU2 @(ex3_intro … U2)
- [1,3: /2 width=9 by cpys_lift, fqu_drop/
- | #H0 destruct /3 width=5 by lift_inj/
-]
-qed-.
-
-lemma fquq_cpys_trans_neq: ∀G1,G2,L1,L2,T1,T2. ⦃G1, L1, T1⦄ ⊃⸮ ⦃G2, L2, T2⦄ →
- ∀U2. ⦃G2, L2⦄ ⊢ T2 ▶*× U2 → (T2 = U2 → ⊥) →
- ∃∃U1. ⦃G1, L1⦄ ⊢ T1 ▶*× U1 & T1 = U1 → ⊥ & ⦃G1, L1, U1⦄ ⊃⸮ ⦃G2, L2, U2⦄.
-#G1 #G2 #L1 #L2 #T1 #T2 #H12 #U2 #HTU2 #H elim (fquq_inv_gen … H12) -H12
-[ #H12 elim (fqu_cpys_trans_neq … H12 … HTU2 H) -T2
- /3 width=4 by fqu_fquq, ex3_intro/
-| * #HG #HL #HT destruct /3 width=4 by ex3_intro/
-]
-qed-.
-
-lemma fqup_cpys_trans_neq: ∀G1,G2,L1,L2,T1,T2. ⦃G1, L1, T1⦄ ⊃+ ⦃G2, L2, T2⦄ →
- ∀U2. ⦃G2, L2⦄ ⊢ T2 ▶*× U2 → (T2 = U2 → ⊥) →
- ∃∃U1. ⦃G1, L1⦄ ⊢ T1 ▶*× U1 & T1 = U1 → ⊥ & ⦃G1, L1, U1⦄ ⊃+ ⦃G2, L2, U2⦄.
-#G1 #G2 #L1 #L2 #T1 #T2 #H @(fqup_ind_dx … H) -G1 -L1 -T1
-[ #G1 #L1 #T1 #H12 #U2 #HTU2 #H elim (fqu_cpys_trans_neq … H12 … HTU2 H) -T2
- /3 width=4 by fqu_fqup, ex3_intro/
-| #G #G1 #L #L1 #T #T1 #H1 #_ #IH12 #U2 #HTU2 #H elim (IH12 … HTU2 H) -T2
- #U1 #HTU1 #H #H12 elim (fqu_cpys_trans_neq … H1 … HTU1 H) -T1
- /3 width=8 by fqup_strap2, ex3_intro/
-]
-qed-.
-
-lemma fqus_cpys_trans_neq: ∀G1,G2,L1,L2,T1,T2. ⦃G1, L1, T1⦄ ⊃* ⦃G2, L2, T2⦄ →
- ∀U2. ⦃G2, L2⦄ ⊢ T2 ▶*× U2 → (T2 = U2 → ⊥) →
- ∃∃U1. ⦃G1, L1⦄ ⊢ T1 ▶*× U1 & T1 = U1 → ⊥ & ⦃G1, L1, U1⦄ ⊃* ⦃G2, L2, U2⦄.
-#G1 #G2 #L1 #L2 #T1 #T2 #H12 #U2 #HTU2 #H elim (fqus_inv_gen … H12) -H12
-[ #H12 elim (fqup_cpys_trans_neq … H12 … HTU2 H) -T2
- /3 width=4 by fqup_fqus, ex3_intro/
-| * #HG #HL #HT destruct /3 width=4 by ex3_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 *)
-(* *)
-(**************************************************************************)
-
-(* NOTATION FOR THE FORMAL SYSTEM λδ ****************************************)
-
-notation "hvbox( L1 break ⊑ × break term 46 L2 )"
- non associative with precedence 45
- for @{ 'ExtLRSubEq $L1 $L2 }.
+++ /dev/null
-(**************************************************************************)
-(* ___ *)
-(* ||M|| *)
-(* ||A|| A project by Andrea Asperti *)
-(* ||T|| *)
-(* ||I|| Developers: *)
-(* ||T|| The HELM team. *)
-(* ||A|| http://helm.cs.unibo.it *)
-(* \ / *)
-(* \ / This file is distributed under the terms of the *)
-(* v GNU General Public License Version 2 *)
-(* *)
-(**************************************************************************)
-
-(* NOTATION FOR THE FORMAL SYSTEM λδ ****************************************)
-
-notation "hvbox( ⦃ term 46 G , break term 46 L1 ⦄ ⊢ ▶ * × break term 46 L2 )"
- non associative with precedence 45
- for @{ 'ExtPSubstSnStar $G $L1 $L2 }.
+++ /dev/null
-(**************************************************************************)
-(* ___ *)
-(* ||M|| *)
-(* ||A|| A project by Andrea Asperti *)
-(* ||T|| *)
-(* ||I|| Developers: *)
-(* ||T|| The HELM team. *)
-(* ||A|| http://helm.cs.unibo.it *)
-(* \ / *)
-(* \ / This file is distributed under the terms of the *)
-(* v GNU General Public License Version 2 *)
-(* *)
-(**************************************************************************)
-
-(* NOTATION FOR THE FORMAL SYSTEM λδ ****************************************)
-
-notation "hvbox( ⦃ term 46 G , break term 46 L ⦄ ⊢ break term 46 T1 break ▶ * × break term 46 T2 )"
- non associative with precedence 45
- for @{ 'ExtPSubstStar $G $L $T1 $T2 }.
+++ /dev/null
-(**************************************************************************)
-(* ___ *)
-(* ||M|| *)
-(* ||A|| A project by Andrea Asperti *)
-(* ||T|| *)
-(* ||I|| Developers: *)
-(* ||T|| The HELM team. *)
-(* ||A|| http://helm.cs.unibo.it *)
-(* \ / *)
-(* \ / This file is distributed under the terms of the *)
-(* v GNU General Public License Version 2 *)
-(* *)
-(**************************************************************************)
-
-include "basic_2/notation/relations/extpsubstsnstar_3.ma".
-include "basic_2/grammar/lpx_sn.ma".
-include "basic_2/substitution/cpys.ma".
-
-(* SN EXTENDED MULTIPLE SUBSTITUTION FOR LOCAL ENVIRONMENTS *****************)
-
-definition lpys: relation3 genv lenv lenv ≝ λG. lpx_sn (cpys G).
-
-interpretation
- "extended multiple substitution (local environment, sn variant)"
- 'ExtPSubstSnStar G L1 L2 = (lpys G L1 L2).
-
-(* Basic inversion lemmas ***************************************************)
-
-lemma lpys_inv_atom1: ∀G,L2. ⦃G, ⋆⦄ ⊢ ▶*× L2 → L2 = ⋆.
-/2 width=4 by lpx_sn_inv_atom1_aux/ qed-.
-
-lemma lpys_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 lpys_inv_atom2: ∀G,L1. ⦃G, L1⦄ ⊢ ▶*× ⋆ → L1 = ⋆.
-/2 width=4 by lpx_sn_inv_atom2_aux/ qed-.
-
-lemma lpys_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-.
-
-lemma lpys_inv_pair: ∀I1,I2,G,L1,L2,V1,V2. ⦃G, L1.ⓑ{I1}V1⦄ ⊢ ▶*× L2.ⓑ{I2}V2 →
- ∧∧ ⦃G, L1⦄ ⊢ ▶*× L2 & ⦃G, L1⦄ ⊢ V1 ▶*× V2 & I1 = I2.
-/2 width=1 by lpx_sn_inv_pair/ qed-.
-
-(* Basic properties *********************************************************)
-
-lemma lpys_refl: ∀G,L. ⦃G, L⦄ ⊢ ▶*× L.
-/2 width=1 by lpx_sn_refl/ qed.
-
-lemma lpys_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.
-
-lemma lpys_append: ∀G,K1,K2. ⦃G, K1⦄ ⊢ ▶*× K2 → ∀L1,L2. ⦃G, L1⦄ ⊢ ▶*× L2 →
- ⦃G, L1 @@ K1⦄ ⊢ ▶*× L2 @@ K2.
-/3 width=1 by lpx_sn_append, cpys_append/ qed.
-
-(* Basic forward lemmas *****************************************************)
-
-lemma lpys_fwd_length: ∀G,L1,L2. ⦃G, L1⦄ ⊢ ▶*× L2 → |L1| = |L2|.
-/2 width=2 by lpx_sn_fwd_length/ qed-.
-
-(* Advanced forward lemmas **************************************************)
-
-lemma lpys_fwd_append1: ∀G,K1,L1,L. ⦃G, K1 @@ L1⦄ ⊢ ▶*× L →
- ∃∃K2,L2. ⦃G, K1⦄ ⊢ ▶*× K2 & L = K2 @@ L2.
-/2 width=2 by lpx_sn_fwd_append1/ qed-.
-
-lemma lpys_fwd_append2: ∀G,L,K2,L2. ⦃G, L⦄ ⊢ ▶*× K2 @@ L2 →
- ∃∃K1,L1. ⦃G, K1⦄ ⊢ ▶*× K2 & L = K1 @@ L1.
-/2 width=2 by lpx_sn_fwd_append2/ 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_lpx_sn.ma".
-include "basic_2/substitution/cpys_lift.ma".
-include "basic_2/substitution/lpys.ma".
-
-(* SN EXTENDED MULTIPLE SUBSTITUTION FOR LOCAL ENVIRONMENTS *****************)
-
-(* Properies on local environment slicing ***********************************)
-
-lemma lpys_ldrop_conf: ∀G. dropable_sn (lpys G).
-/3 width=5 by lpx_sn_deliftable_dropable, cpys_inv_lift1/ qed-.
-
-lemma ldrop_lpys_trans: ∀G. dedropable_sn (lpys G).
-/3 width=9 by lpx_sn_liftable_dedropable, cpys_lift/ qed-.
-
-lemma lpys_ldrop_trans_O1: ∀G. dropable_dx (lpys G).
-/2 width=3 by lpx_sn_dropable/ qed-.
-
-(* Properties on supclosure *************************************************)
-
-lemma fqu_lpys_trans: ∀G1,G2,L1,L2,T1,T2. ⦃G1, L1, T1⦄ ⊃ ⦃G2, L2, T2⦄ →
- ∀K2. ⦃G2, L2⦄ ⊢ ▶*× K2 →
- ∃∃K1,T. ⦃G1, L1⦄ ⊢ ▶*× K1 & ⦃G1, L1⦄ ⊢ T1 ▶*× T & ⦃G1, K1, T⦄ ⊃ ⦃G2, K2, T2⦄.
-#G1 #G2 #L1 #L2 #T1 #T2 #H elim H -G1 -G2 -L1 -L2 -T1 -T2
-/3 width=5 by fqu_lref_O, fqu_pair_sn, fqu_flat_dx, lpys_pair, ex3_2_intro/
-[ #a #I #G2 #L2 #V2 #T2 #X #H elim (lpys_inv_pair1 … H) -H
- #K2 #W2 #HLK2 #HVW2 #H destruct
- /3 width=5 by fqu_fquq, cpys_pair_sn, fqu_bind_dx, ex3_2_intro/
-| #G #L1 #K1 #T1 #U1 #e #HLK1 #HTU1 #K2 #HK12
- elim (ldrop_lpys_trans … HLK1 … HK12) -HK12
- /3 width=7 by fqu_drop, ex3_2_intro/
-]
-qed-.
-
-lemma fquq_lpys_trans: ∀G1,G2,L1,L2,T1,T2. ⦃G1, L1, T1⦄ ⊃⸮ ⦃G2, L2, T2⦄ →
- ∀K2. ⦃G2, L2⦄ ⊢ ▶*× K2 →
- ∃∃K1,T. ⦃G1, L1⦄ ⊢ ▶*× K1 & ⦃G1, L1⦄ ⊢ T1 ▶*× T & ⦃G1, K1, T⦄ ⊃⸮ ⦃G2, K2, T2⦄.
-#G1 #G2 #L1 #L2 #T1 #T2 #H #K2 #HLK2 elim (fquq_inv_gen … H) -H
-[ #HT12 elim (fqu_lpys_trans … HT12 … HLK2) /3 width=5 by fqu_fquq, ex3_2_intro/
-| * #H1 #H2 #H3 destruct /2 width=5 by ex3_2_intro/
-]
-qed-.
-
-lemma lpys_fqu_trans: ∀G1,G2,L1,L2,T1,T2. ⦃G1, L1, T1⦄ ⊃ ⦃G2, L2, T2⦄ →
- ∀K1. ⦃G1, K1⦄ ⊢ ▶*× L1 →
- ∃∃K2,T. ⦃G1, K1⦄ ⊢ T1 ▶*× T & ⦃G1, K1, T⦄ ⊃ ⦃G2, K2, T2⦄ & ⦃G2, K2⦄ ⊢ ▶*× L2.
-#G1 #G2 #L1 #L2 #T1 #T2 #H elim H -G1 -G2 -L1 -L2 -T1 -T2
-/3 width=7 by fqu_pair_sn, fqu_bind_dx, fqu_flat_dx, lpys_pair, ex3_2_intro/
-[ #I #G1 #L1 #V1 #X #H elim (lpys_inv_pair2 … H) -H
- #K1 #W1 #HKL1 #HWV1 #H destruct elim (lift_total V1 0 1)
- /4 width=7 by cpys_delta, fqu_drop, ldrop_ldrop, ex3_2_intro/
-| #G #L1 #K1 #T1 #U1 #e #HLK1 #HTU1 #L0 #HL01
- elim (lpys_ldrop_trans_O1 … HL01 … HLK1) -L1
- /3 width=5 by fqu_drop, ex3_2_intro/
-]
-qed-.
-
-lemma lpys_fquq_trans: ∀G1,G2,L1,L2,T1,T2. ⦃G1, L1, T1⦄ ⊃⸮ ⦃G2, L2, T2⦄ →
- ∀K1. ⦃G1, K1⦄ ⊢ ▶*× L1 →
- ∃∃K2,T. ⦃G1, K1⦄ ⊢ T1 ▶*× T & ⦃G1, K1, T⦄ ⊃⸮ ⦃G2, K2, T2⦄ & ⦃G2, K2⦄ ⊢ ▶*× L2.
-#G1 #G2 #L1 #L2 #T1 #T2 #H #K1 #HKL1 elim (fquq_inv_gen … H) -H
-[ #HT12 elim (lpys_fqu_trans … HT12 … HKL1) /3 width=5 by fqu_fquq, ex3_2_intro/
-| * #H1 #H2 #H3 destruct /2 width=5 by ex3_2_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/substitution/cpys_cpys.ma".
-
-(* SN EXTENDED MULTIPLE SUBSTITUTION FOR LOCAL ENVIRONMENTS *****************)
-
-(* Main properties **********************************************************)
-
-theorem lpys_trans: ∀G. Transitive … (lpys G).
-/3 width=5 by lpx_sn_trans, cpys_trans_lpys/
-qed-.
-
-(* Advanced forward lemmas **************************************************)
-
-lemma cpys_fwd_shift1_ext: ∀G,L1,L,T1,T. ⦃G, L⦄ ⊢ L1 @@ T1 ▶*× T →
- ∃∃L2,T2. ⦃G, L @@ L1⦄ ⊢ ▶*× L @@ L2 & ⦃G, L @@ L1⦄ ⊢ T1 ▶*× T2 &
- T = L2 @@ T2.
-#G #L1 @(lenv_ind_dx … L1) -L1
-[ #L #T1 #T #HT1 @ex3_2_intro
- [3: // |4,5: // |1,2: skip ] (**) (* auto does not work *)
-| #I #L1 #V1 #IH #L #T1 #T >shift_append_assoc #H <append_assoc
- elim (cpys_inv_bind1 … H) -H #V2 #T2 #HV12 #HT12 #H destruct
- elim (IH … HT12) -IH -HT12 #L2 #T #HL12 #HT1 #H destruct
- lapply (lpys_trans … HL12 (L.ⓑ{I}V2@@L2) ?) -HL12 /3 width=1 by lpys_append, lpys_pair/ #HL12
- @(ex3_2_intro … (⋆.ⓑ{I}V2@@L2)) [4: /2 width=3 by trans_eq/ | skip ] <append_assoc // (**) (* explicit constructor *)
-]
-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/extlrsubeq_2.ma".
-include "basic_2/relocation/ldrop.ma".
-
-(* LOCAL ENVIRONMENT REFINEMENT FOR EXTENDED SUBSTITUTION *******************)
-
-inductive lsuby: relation lenv ≝
-| lsuby_atom: ∀L. lsuby L (⋆)
-| lsuby_pair: ∀I1,I2,L1,L2,V. lsuby L1 L2 → lsuby (L1.ⓑ{I1}V) (L2.ⓑ{I2}V)
-.
-
-interpretation
- "local environment refinement (extended substitution)"
- 'ExtLRSubEq L1 L2 = (lsuby L1 L2).
-
-(* Basic properties *********************************************************)
-
-lemma lsuby_refl: ∀L. L ⊑× L.
-#L elim L -L // /2 width=1/
-qed.
-
-(* Basic inversion lemmas ***************************************************)
-
-fact lsuby_inv_atom1_aux: ∀L1,L2. L1 ⊑× L2 → L1 = ⋆ → L2 = ⋆.
-#L1 #L2 * -L1 -L2 //
-#I1 #I2 #L1 #L2 #V #_ #H destruct
-qed-.
-
-lemma lsuby_inv_atom1: ∀L2. ⋆ ⊑× L2 → L2 = ⋆.
-/2 width=3 by lsuby_inv_atom1_aux/ qed-.
-
-fact lsuby_inv_pair1_aux: ∀L1,L2. L1 ⊑× L2 → ∀J1,K1,W. L1 = K1.ⓑ{J1}W →
- L2 = ⋆ ∨ ∃∃I2,K2. K1 ⊑× K2 & L2 = K2.ⓑ{I2}W.
-#L1 #L2 * -L1 -L2
-[ #L #J1 #K1 #W #H destruct /2 width=1 by or_introl/
-| #I1 #I2 #L1 #L2 #V #HL12 #J1 #K1 #W #H destruct /3 width=4 by ex2_2_intro, or_intror/
-]
-qed-.
-
-lemma lsuby_inv_pair1: ∀I1,K1,L2,W. K1.ⓑ{I1}W ⊑× L2 →
- L2 = ⋆ ∨ ∃∃I2,K2. K1 ⊑× K2 & L2 = K2.ⓑ{I2}W.
-/2 width=4 by lsuby_inv_pair1_aux/ qed-.
-
-(* Basic forward lemmas *****************************************************)
-
-lemma lsuby_fwd_length: ∀L1,L2. L1 ⊑× L2 → |L2| ≤ |L1|.
-#L1 #L2 #H elim H -L1 -L2 /2 width=1 by monotonic_le_plus_l/
-qed-.
-
-lemma lsuby_fwd_ldrop2_pair: ∀L1,L2. L1 ⊑× L2 →
- ∀I2,K2,W,i. ⇩[0, i] L2 ≡ K2.ⓑ{I2}W →
- ∃∃I1,K1. K1 ⊑× K2 & ⇩[0, i] L1 ≡ K1.ⓑ{I1}W.
-#L1 #L2 #H elim H -L1 -L2
-[ #L #J2 #K2 #W #i #H
- elim (ldrop_inv_atom1 … H) -H #H destruct
-| #I1 #I2 #L1 #L2 #V #HL12 #IHL12 #J2 #K2 #W #i #H
- elim (ldrop_inv_O1_pair1 … H) -H * #Hi #HLK2 destruct [ -IHL12 | -HL12 ]
- [ /3 width=4 by ldrop_pair, ex2_2_intro/
- | elim (IHL12 … HLK2) -IHL12 -HLK2 * /3 width=4 by ldrop_ldrop_lt, ex2_2_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/lsuby.ma".
-
-(* LOCAL ENVIRONMENT REFINEMENT FOR EXTENDED SUBSTITUTION *******************)
-
-(* Main properties **********************************************************)
-
-theorem lsuby_trans: Transitive … lsuby.
-#L1 #L #H elim H -L1 -L
-[ #L1 #X #H lapply (lsuby_inv_atom1 … H) -H //
-| #I1 #I #L1 #L #V #_ #IHL1 #X #H elim (lsuby_inv_pair1 … H) -H // *
- #I2 #L2 #HL2 #H destruct /3 width=1 by lsuby_pair/
-]
-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/psubststar_4.ma".
+include "basic_2/grammar/genv.ma".
+include "basic_2/substitution/lsuby.ma".
+
+(* CONTEXT-SENSITIVE EXTENDED MULTIPLE SUBSTITUTION FOR TERMS ***************)
+
+(* avtivate genv *)
+inductive cpys: relation4 genv lenv term term ≝
+| cpys_atom : ∀I,G,L. cpys G L (⓪{I}) (⓪{I})
+| cpys_delta: ∀I,G,L,K,V,V2,W2,i.
+ ⇩[i] L ≡ K.ⓑ{I}V → cpys G K V V2 →
+ ⇧[0, i + 1] V2 ≡ W2 → cpys G L (#i) W2
+| cpys_bind : ∀a,I,G,L,V1,V2,T1,T2.
+ cpys G L V1 V2 → cpys G (L.ⓑ{I}V1) T1 T2 →
+ cpys G L (ⓑ{a,I}V1.T1) (ⓑ{a,I}V2.T2)
+| cpys_flat : ∀I,G,L,V1,V2,T1,T2.
+ cpys G L V1 V2 → cpys G L T1 T2 →
+ cpys G L (ⓕ{I}V1.T1) (ⓕ{I}V2.T2)
+.
+
+interpretation
+ "context-sensitive extended multiple substitution (term)"
+ 'PSubstStar G L T1 T2 = (cpys G L T1 T2).
+
+(* Basic properties *********************************************************)
+
+lemma lsuby_cpys_trans: ∀G. lsub_trans … (cpys G) lsuby.
+#G #L1 #T1 #T2 #H elim H -G -L1 -T1 -T2
+[ //
+| #I #G #L1 #K1 #V1 #V2 #W2 #i #HLK1 #_ #HVW2 #IHV12 #L2 #HL12
+ elim (lsuby_ldrop_trans … HL12 … HLK1) -HL12 -HLK1 *
+ /3 width=7 by cpys_delta/
+| /4 width=1 by lsuby_pair, cpys_bind/
+| /3 width=1 by cpys_flat/
+]
+qed-.
+
+(* Note: this is "∀L. reflexive … (cpys L)" *)
+lemma cpys_refl: ∀G,T,L. ⦃G, L⦄ ⊢ T ▶* T.
+#G #T elim T -T // * /2 width=1 by cpys_bind, cpys_flat/
+qed.
+
+lemma cpys_pair_sn: ∀I,G,L,V1,V2. ⦃G, L⦄ ⊢ V1 ▶* V2 →
+ ∀T. ⦃G, L⦄ ⊢ ②{I}V1.T ▶* ②{I}V2.T.
+* /2 width=1 by cpys_bind, cpys_flat/
+qed.
+
+lemma cpys_bind_ext: ∀G,L,V1,V2. ⦃G, L⦄ ⊢ V1 ▶* V2 →
+ ∀J,T1,T2. ⦃G, L.ⓑ{J}V1⦄ ⊢ T1 ▶* T2 →
+ ∀a,I. ⦃G, L⦄ ⊢ ⓑ{a,I}V1.T1 ▶* ⓑ{a,I}V2.T2.
+/4 width=4 by lsuby_cpys_trans, cpys_bind, lsuby_pair/ qed.
+
+lemma cpys_delift: ∀I,G,K,V,T1,L,d. ⇩[d] L ≡ (K.ⓑ{I}V) →
+ ∃∃T2,T. ⦃G, L⦄ ⊢ T1 ▶* T2 & ⇧[d, 1] T ≡ T2.
+#I #G #K #V #T1 elim T1 -T1
+[ * /2 width=4 by cpys_atom, lift_sort, lift_gref, ex2_2_intro/
+ #i #L #d elim (lt_or_eq_or_gt i d) #Hid [1,3: /3 width=4 by cpys_atom, lift_lref_ge_minus, lift_lref_lt, ex2_2_intro/ ]
+ destruct
+ elim (lift_total V 0 (i+1)) #W #HVW
+ elim (lift_split … HVW i i) /3 width=7 by cpys_delta, ex2_2_intro/
+| * [ #a ] #I #W1 #U1 #IHW1 #IHU1 #L #d #HLK
+ elim (IHW1 … HLK) -IHW1 #W2 #W #HW12 #HW2
+ [ elim (IHU1 (L. ⓑ{I}W1) (d+1)) -IHU1 /3 width=9 by cpys_bind, ldrop_drop, lift_bind, ex2_2_intro/
+ | elim (IHU1 … HLK) -IHU1 -HLK /3 width=8 by cpys_flat, lift_flat, ex2_2_intro/
+ ]
+]
+qed-.
+
+(* Basic inversion lemmas ***************************************************)
+
+fact cpys_inv_atom1_aux: ∀G,L,T1,T2. ⦃G, L⦄ ⊢ T1 ▶* T2 → ∀J. T1 = ⓪{J} →
+ T2 = ⓪{J} ∨
+ ∃∃I,K,V,V2,i. ⇩[i] L ≡ K.ⓑ{I}V & ⦃G, K⦄ ⊢ V ▶* V2 &
+ ⇧[O, i + 1] V2 ≡ T2 & J = LRef i.
+#G #L #T1 #T2 * -L -T1 -T2
+[ #I #G #L #J #H destruct /2 width=1 by or_introl/
+| #I #G #L #K #V #V2 #T2 #i #HLK #HV2 #HVT2 #J #H destruct /3 width=9 by ex4_5_intro, or_intror/
+| #a #I #G #L #V1 #V2 #T1 #T2 #_ #_ #J #H destruct
+| #I #G #L #V1 #V2 #T1 #T2 #_ #_ #J #H destruct
+]
+qed-.
+
+lemma cpys_inv_atom1: ∀J,G,L,T2. ⦃G, L⦄ ⊢ ⓪{J} ▶* T2 →
+ T2 = ⓪{J} ∨
+ ∃∃I,K,V,V2,i. ⇩[i] L ≡ K.ⓑ{I}V & ⦃G, K⦄ ⊢ V ▶* V2 &
+ ⇧[O, i + 1] V2 ≡ T2 & J = LRef i.
+/2 width=3 by cpys_inv_atom1_aux/ qed-.
+
+lemma cpys_inv_sort1: ∀G,L,T2,k. ⦃G, L⦄ ⊢ ⋆k ▶* T2 → T2 = ⋆k.
+#G #L #T2 #k #H elim (cpys_inv_atom1 … H) -H // *
+#I #K #V #V2 #i #_ #_ #_ #H destruct
+qed-.
+
+lemma cpys_inv_lref1: ∀G,L,T2,i. ⦃G, L⦄ ⊢ #i ▶* T2 →
+ T2 = #i ∨
+ ∃∃I,K,V,V2. ⇩[i] L ≡ K. ⓑ{I}V & ⦃G, K⦄ ⊢ V ▶* V2 &
+ ⇧[O, i + 1] V2 ≡ T2.
+#G #L #T2 #i #H elim (cpys_inv_atom1 … H) -H /2 width=1 by or_introl/ *
+#I #K #V #V2 #j #HLK #HV2 #HVT2 #H destruct /3 width=7 by ex3_4_intro, or_intror/
+qed-.
+
+lemma cpys_inv_lref1_ge: ∀G,L,T2,i. ⦃G, L⦄ ⊢ #i ▶* T2 → |L| ≤ i → T2 = #i.
+#G #L #T2 #i #H elim (cpys_inv_lref1 … H) -H // *
+#I #K #V1 #V2 #HLK #_ #_ #HL -V2 lapply (ldrop_fwd_length_lt2 … HLK) -K -I -V1
+#H elim (lt_refl_false i) /2 width=3 by lt_to_le_to_lt/
+qed-.
+
+lemma cpys_inv_gref1: ∀G,L,T2,p. ⦃G, L⦄ ⊢ §p ▶* T2 → T2 = §p.
+#G #L #T2 #p #H elim (cpys_inv_atom1 … H) -H // *
+#I #K #V #V2 #i #_ #_ #_ #H destruct
+qed-.
+
+fact cpys_inv_bind1_aux: ∀G,L,U1,U2. ⦃G, L⦄ ⊢ U1 ▶* U2 →
+ ∀a,J,V1,T1. U1 = ⓑ{a,J}V1.T1 →
+ ∃∃V2,T2. ⦃G, L⦄ ⊢ V1 ▶* V2 & ⦃G, L.ⓑ{J}V1⦄ ⊢ T1 ▶* T2 &
+ U2 = ⓑ{a,J}V2.T2.
+#G #L #U1 #U2 * -L -U1 -U2
+[ #I #G #L #b #J #W #U1 #H destruct
+| #I #G #L #K #V #V2 #W2 #i #_ #_ #_ #b #J #W #U1 #H destruct
+| #a #I #G #L #V1 #V2 #T1 #T2 #HV12 #HT12 #b #J #W #U1 #H destruct /2 width=5 by ex3_2_intro/
+| #I #G #L #V1 #V2 #T1 #T2 #_ #_ #b #J #W #U1 #H destruct
+]
+qed-.
+
+lemma cpys_inv_bind1: ∀a,I,G,L,V1,T1,U2. ⦃G, L⦄ ⊢ ⓑ{a,I}V1.T1 ▶* U2 →
+ ∃∃V2,T2. ⦃G, L⦄ ⊢ V1 ▶* V2 & ⦃G, L.ⓑ{I}V1⦄ ⊢ T1 ▶* T2 &
+ U2 = ⓑ{a,I}V2.T2.
+/2 width=3 by cpys_inv_bind1_aux/ qed-.
+
+lemma cpys_inv_bind1_ext: ∀a,I,G,L,V1,T1,U2. ⦃G, L⦄ ⊢ ⓑ{a,I}V1.T1 ▶* U2 → ∀J.
+ ∃∃V2,T2. ⦃G, L⦄ ⊢ V1 ▶* V2 & ⦃G, L.ⓑ{J}V1⦄ ⊢ T1 ▶* T2 &
+ U2 = ⓑ{a,I}V2.T2.
+#a #I #G #L #V1 #T1 #U2 #H #J elim (cpys_inv_bind1 … H) -H
+#V2 #T2 #HV12 #HT12 #H destruct
+/4 width=5 by lsuby_cpys_trans, lsuby_pair, ex3_2_intro/
+qed-.
+
+fact cpys_inv_flat1_aux: ∀G,L,U,U2. ⦃G, L⦄ ⊢ U ▶* U2 →
+ ∀J,V1,U1. U = ⓕ{J}V1.U1 →
+ ∃∃V2,T2. ⦃G, L⦄ ⊢ V1 ▶* V2 & ⦃G, L⦄ ⊢ U1 ▶* T2 &
+ U2 = ⓕ{J}V2.T2.
+#G #L #U #U2 * -L -U -U2
+[ #I #G #L #J #W #U1 #H destruct
+| #I #G #L #K #V #V2 #W2 #i #_ #_ #_ #J #W #U1 #H destruct
+| #a #I #G #L #V1 #V2 #T1 #T2 #_ #_ #J #W #U1 #H destruct
+| #I #G #L #V1 #V2 #T1 #T2 #HV12 #HT12 #J #W #U1 #H destruct /2 width=5 by ex3_2_intro/
+]
+qed-.
+
+(* Note: lemma 1250 *)
+lemma cpys_inv_flat1: ∀I,G,L,V1,U1,U2. ⦃G, L⦄ ⊢ ⓕ{I}V1.U1 ▶* U2 →
+ ∃∃V2,T2. ⦃G, L⦄ ⊢ V1 ▶* V2 & ⦃G, L⦄ ⊢ U1 ▶* T2 &
+ U2 = ⓕ{I}V2.T2.
+/2 width=3 by cpys_inv_flat1_aux/ qed-.
+
+(* Basic forward lemmas *****************************************************)
+
+lemma cpys_fwd_bind1: ∀a,I,G,L,V1,T1,T. ⦃G, L⦄ ⊢ ⓑ{a,I}V1.T1 ▶* T → ∀b,J.
+ ∃∃V2,T2. ⦃G, L⦄ ⊢ ⓑ{b,J}V1.T1 ▶* ⓑ{b,J}V2.T2 &
+ T = ⓑ{a,I}V2.T2.
+#a #I #G #L #V1 #T1 #T #H #b #J elim (cpys_inv_bind1_ext … H J) -H
+#V2 #T2 #HV12 #HT12 #H destruct /3 width=4 by cpys_bind, ex2_2_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_lpx_sn.ma".
+include "basic_2/substitution/fqup.ma".
+include "basic_2/substitution/lpys_ldrop.ma".
+
+(* CONTEXT-SENSITIVE EXTENDED MULTIPLE SUBSTITUTION FOR TERMS ***************)
+
+(* Main properties **********************************************************)
+
+theorem cpys_antisym: ∀G,L,T1,T2. ⦃G, L⦄ ⊢ T1 ▶* T2 → ⦃G, L⦄ ⊢ T2 ▶* T1 → T1 = T2.
+#G #L #T1 #T2 #H elim H -G -L -T1 -T2 //
+[ #I #G #L #K #V1 #V2 #W2 #i #HLK #_ #HVW2 #_ #HW2 lapply (ldrop_fwd_drop2 … HLK) -I -V1
+ #HLK elim (cpys_inv_lift1 … HW2 … HLK … HVW2) -L -HVW2
+ #X #H #_ elim (lift_inv_lref2_be … H) -G -K -V2 -W2 -X //
+| #a #I #G #L #V1 #V2 #T1 #T2 #_ #_ #IHV12 #IHT12 #H elim (cpys_inv_bind1 … H) -H
+ #V #T #HV2 #HT2 #H destruct
+ lapply (IHV12 HV2) #H destruct -IHV12 -HV2 /3 width=1 by eq_f2/
+| #I #G #L #V1 #V2 #T1 #T2 #_ #_ #IHV12 #IHT12 #H elim (cpys_inv_flat1 … H) -H
+ #V #T #HV2 #HT2 #H destruct /3 width=1 by eq_f2/
+]
+qed-.
+
+theorem cpys_trans_lpys: ∀G. lpx_sn_transitive (cpys G) (cpys G).
+#G0 #L0 #T0 @(fqup_wf_ind_eq … G0 L0 T0) -G0 -L0 -T0 #G0 #L0 #T0 #IH #G1 #L1 * [|*]
+[ #I #HG #HL #HT #T #H1 #L2 #HL12 #T2 #HT2 destruct
+ elim (cpys_inv_atom1 … H1) -H1
+ [ #H destruct
+ elim (cpys_inv_atom1 … HT2) -HT2
+ [ #H destruct //
+ | * #I2 #K2 #V #V2 #i #HLK2 #HV2 #HVT2 #H destruct
+ elim (lpys_ldrop_trans_O1 … HL12 … HLK2) -L2 #X #HLK1 #H
+ elim (lpys_inv_pair2 … H) -H #K1 #V1 #HK12 #HV1 #H destruct
+ lapply (fqup_lref … G1 … HLK1) /3 width=10 by cpys_delta/
+ ]
+ | * #I1 #K1 #V1 #V #i #HLK1 #HV1 #HVT #H destruct
+ elim (lpys_ldrop_conf … HLK1 … HL12) -HL12 #X #H #HLK2
+ elim (lpys_inv_pair1 … H) -H #K2 #W2 #HK12 #_ #H destruct
+ lapply (ldrop_fwd_drop2 … HLK2) -W2 #HLK2
+ elim (cpys_inv_lift1 … HT2 … HLK2 … HVT) -L2 -T
+ lapply (fqup_lref … G1 … HLK1) /3 width=10 by cpys_delta/
+ ]
+| #a #I #V1 #T1 #HG #HL #HT #X1 #H1 #L2 #HL12 #X2 #H2
+ elim (cpys_inv_bind1 … H1) -H1 #V #T #HV1 #HT1 #H destruct
+ elim (cpys_inv_bind1 … H2) -H2 #V2 #T2 #HV2 #HT2 #H destruct
+ /4 width=5 by cpys_bind, lpys_pair/
+| #I #V1 #T1 #HG #HL #HT #X1 #H1 #L2 #HL12 #X2 #H2
+ elim (cpys_inv_flat1 … H1) -H1 #V #T #HV1 #HT1 #H destruct
+ elim (cpys_inv_flat1 … H2) -H2 #V2 #T2 #HV2 #HT2 #H destruct
+ /3 width=5 by cpys_flat/
+]
+qed-.
+
+theorem cpys_trans: ∀G,L. Transitive … (cpys G L).
+/2 width=5 by cpys_trans_lpys/ qed-.
+
+(* Advanced properties ******************************************************)
+
+lemma lpys_cpys_trans: ∀G. lsub_trans … (cpys G) (lpys G).
+/2 width=5 by cpys_trans_lpys/ 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/fqus_alt.ma".
+include "basic_2/substitution/cpys.ma".
+
+(* CONTEXT-SENSITIVE EXTENDED MULTIPLE SUBSTITUTION FOR TERMS ***************)
+
+(* Relocation properties ****************************************************)
+
+lemma cpys_lift: ∀G. l_liftable (cpys G).
+#G #K #T1 #T2 #H elim H -G -K -T1 -T2
+[ #I #G #K #L #s #d #e #_ #U1 #H1 #U2 #H2
+ >(lift_mono … H1 … H2) -H1 -H2 //
+| #I #G #K #KV #V #V2 #W2 #i #HKV #HV2 #HVW2 #IHV2 #L #s #d #e #HLK #U1 #H #U2 #HWU2
+ elim (lift_inv_lref1 … H) * #Hid #H destruct
+ [ elim (lift_trans_ge … HVW2 … HWU2) -W2 // <minus_plus #W2 #HVW2 #HWU2
+ elim (ldrop_trans_le … HLK … HKV) -K /2 width=2 by lt_to_le/ #X #HLK #H
+ elim (ldrop_inv_skip2 … H) -H /2 width=1 by lt_plus_to_minus_r/ -Hid #K #Y #HKV #HVY #H destruct /3 width=10 by cpys_delta/
+ | lapply (lift_trans_be … HVW2 … HWU2 ? ?) -W2 /2 width=1 by le_S/ >plus_plus_comm_23 #HVU2
+ lapply (ldrop_trans_ge_comm … HLK … HKV ?) -K /3 width=7 by cpys_delta, ldrop_inv_gen/
+ ]
+| #a #I #G #K #V1 #V2 #T1 #T2 #_ #_ #IHV12 #IHT12 #L #s #d #e #HLK #U1 #H1 #U2 #H2
+ elim (lift_inv_bind1 … H1) -H1 #VV1 #TT1 #HVV1 #HTT1 #H1 destruct
+ elim (lift_inv_bind1 … H2) -H2 #VV2 #TT2 #HVV2 #HTT2 #H2 destruct /4 width=6 by cpys_bind, ldrop_skip/
+| #I #G #K #V1 #V2 #T1 #T2 #_ #_ #IHV12 #IHT12 #L #s #d #e #HLK #U1 #H1 #U2 #H2
+ elim (lift_inv_flat1 … H1) -H1 #VV1 #TT1 #HVV1 #HTT1 #H1 destruct
+ elim (lift_inv_flat1 … H2) -H2 #VV2 #TT2 #HVV2 #HTT2 #H2 destruct /3 width=6 by cpys_flat/
+]
+qed.
+
+lemma cpys_inv_lift1: ∀G. l_deliftable_sn (cpys G).
+#G #L #U1 #U2 #H elim H -G -L -U1 -U2
+[ * #G #L #i #K #s #d #e #_ #T1 #H
+ [ lapply (lift_inv_sort2 … H) -H #H destruct /2 width=3 by cpys_atom, lift_sort, ex2_intro/
+ | elim (lift_inv_lref2 … H) -H * #Hid #H destruct /3 width=3 by cpys_atom, lift_lref_ge_minus, lift_lref_lt, ex2_intro/
+ | lapply (lift_inv_gref2 … H) -H #H destruct /2 width=3 by cpys_atom, lift_gref, ex2_intro/
+ ]
+| #I #G #L #LV #V #V2 #W2 #i #HLV #HV2 #HVW2 #IHV2 #K #s #d #e #HLK #T1 #H
+ elim (lift_inv_lref2 … H) -H * #Hid #H destruct
+ [ elim (ldrop_conf_lt … HLK … HLV) -L // #L #U #HKL #HLV #HUV
+ elim (IHV2 … HLV … HUV) -V #U2 #HUV2 #HU2
+ elim (lift_trans_le … HUV2 … HVW2) -V2 // >minus_plus <plus_minus_m_m /3 width=9 by cpys_delta, ex2_intro/
+ | elim (le_inv_plus_l … Hid) #Hdie #Hei
+ lapply (ldrop_conf_ge … HLK … HLV ?) -L // #HKLV
+ elim (lift_split … HVW2 d (i - e + 1)) -HVW2 /3 width=1 by le_S, le_S_S/ -Hid -Hdie
+ #V1 #HV1 >plus_minus // <minus_minus /2 width=1 by le_S/ <minus_n_n <plus_n_O /3 width=9 by cpys_delta, ex2_intro/
+ ]
+| #a #I #G #L #V1 #V2 #U1 #U2 #_ #_ #IHV12 #IHU12 #K #s #d #e #HLK #X #H
+ elim (lift_inv_bind2 … H) -H #W1 #T1 #HWV1 #HTU1 #H destruct
+ elim (IHV12 … HLK … HWV1) -IHV12 #W2 #HW12 #HWV2
+ elim (IHU12 … HTU1) -IHU12 -HTU1 /3 width=6 by cpys_bind, ldrop_skip, lift_bind, ex2_intro/
+| #I #G #L #V1 #V2 #U1 #U2 #_ #_ #IHV12 #IHU12 #K #s #d #e #HLK #X #H
+ elim (lift_inv_flat2 … H) -H #W1 #T1 #HWV1 #HTU1 #H destruct
+ elim (IHV12 … HLK … HWV1) -V1
+ elim (IHU12 … HLK … HTU1) -U1 -HLK /3 width=5 by cpys_flat, lift_flat, ex2_intro/
+]
+qed-.
+
+(* Properties on supclosure *************************************************)
+
+lemma fqu_cpys_trans: ∀G1,G2,L1,L2,T1,T2. ⦃G1, L1, T1⦄ ⊐ ⦃G2, L2, T2⦄ →
+ ∀U2. ⦃G2, L2⦄ ⊢ T2 ▶* U2 →
+ ∃∃U1. ⦃G1, L1⦄ ⊢ T1 ▶* U1 & ⦃G1, L1, U1⦄ ⊐ ⦃G2, L2, U2⦄.
+#G1 #G2 #L1 #L2 #T1 #T2 #H elim H -G1 -G2 -L1 -L2 -T1 -T2
+/3 width=3 by fqu_pair_sn, fqu_bind_dx, fqu_flat_dx, cpys_pair_sn, cpys_bind, cpys_flat, ex2_intro/
+[ #I #G #L #V2 #U2 #HVU2
+ elim (lift_total U2 0 1)
+ /4 width=7 by fqu_drop, cpys_delta, ldrop_pair, ldrop_drop, ex2_intro/
+| #G #L #K #T1 #U1 #e #HLK1 #HTU1 #T2 #HTU2
+ elim (lift_total T2 0 (e+1))
+ /3 width=11 by cpys_lift, fqu_drop, ex2_intro/
+]
+qed-.
+
+lemma fquq_cpys_trans: ∀G1,G2,L1,L2,T1,T2. ⦃G1, L1, T1⦄ ⊐⸮ ⦃G2, L2, T2⦄ →
+ ∀U2. ⦃G2, L2⦄ ⊢ T2 ▶* U2 →
+ ∃∃U1. ⦃G1, L1⦄ ⊢ T1 ▶* U1 & ⦃G1, L1, U1⦄ ⊐⸮ ⦃G2, L2, U2⦄.
+#G1 #G2 #L1 #L2 #T1 #T2 #H #U2 #HTU2 elim (fquq_inv_gen … H) -H
+[ #HT12 elim (fqu_cpys_trans … HT12 … HTU2) /3 width=3 by fqu_fquq, ex2_intro/
+| * #H1 #H2 #H3 destruct /2 width=3 by ex2_intro/
+]
+qed-.
+
+lemma fqup_cpys_trans: ∀G1,G2,L1,L2,T1,T2. ⦃G1, L1, T1⦄ ⊐+ ⦃G2, L2, T2⦄ →
+ ∀U2. ⦃G2, L2⦄ ⊢ T2 ▶* U2 →
+ ∃∃U1. ⦃G1, L1⦄ ⊢ T1 ▶* U1 & ⦃G1, L1, U1⦄ ⊐+ ⦃G2, L2, U2⦄.
+#G1 #G2 #L1 #L2 #T1 #T2 #H @(fqup_ind … H) -G2 -L2 -T2
+[ #G2 #L2 #T2 #H12 #U2 #HTU2 elim (fqu_cpys_trans … H12 … HTU2) -T2
+ /3 width=3 by fqu_fqup, ex2_intro/
+| #G #G2 #L #L2 #T #T2 #_ #HT2 #IHT1 #U2 #HTU2
+ elim (fqu_cpys_trans … HT2 … HTU2) -T2 #T2 #HT2 #HTU2
+ elim (IHT1 … HT2) -T /3 width=7 by fqup_strap1, ex2_intro/
+]
+qed-.
+
+lemma fqus_cpys_trans: ∀G1,G2,L1,L2,T1,T2. ⦃G1, L1, T1⦄ ⊐* ⦃G2, L2, T2⦄ →
+ ∀U2. ⦃G2, L2⦄ ⊢ T2 ▶* U2 →
+ ∃∃U1. ⦃G1, L1⦄ ⊢ T1 ▶* U1 & ⦃G1, L1, U1⦄ ⊐* ⦃G2, L2, U2⦄.
+#G1 #G2 #L1 #L2 #T1 #T2 #H #U2 #HTU2 elim (fqus_inv_gen … H) -H
+[ #HT12 elim (fqup_cpys_trans … HT12 … HTU2) /3 width=3 by fqup_fqus, ex2_intro/
+| * #H1 #H2 #H3 destruct /2 width=3 by ex2_intro/
+]
+qed-.
+
+lemma fqu_cpys_trans_neq: ∀G1,G2,L1,L2,T1,T2. ⦃G1, L1, T1⦄ ⊐ ⦃G2, L2, T2⦄ →
+ ∀U2. ⦃G2, L2⦄ ⊢ T2 ▶* U2 → (T2 = U2 → ⊥) →
+ ∃∃U1. ⦃G1, L1⦄ ⊢ T1 ▶* U1 & T1 = U1 → ⊥ & ⦃G1, L1, U1⦄ ⊐ ⦃G2, L2, U2⦄.
+#G1 #G2 #L1 #L2 #T1 #T2 #H elim H -G1 -G2 -L1 -L2 -T1 -T2
+[ #I #G #L #V1 #V2 #HV12 #_ elim (lift_total V2 0 1)
+ #U2 #HVU2 @(ex3_intro … U2)
+ [1,3: /3 width=7 by fqu_drop, cpys_delta, ldrop_pair, ldrop_drop/
+ | #H destruct /2 width=7 by lift_inv_lref2_be/
+ ]
+| #I #G #L #V1 #T #V2 #HV12 #H @(ex3_intro … (②{I}V2.T))
+ [1,3: /2 width=4 by fqu_pair_sn, cpys_pair_sn/
+ | #H0 destruct /2 width=1 by/
+ ]
+| #a #I #G #L #V #T1 #T2 #HT12 #H @(ex3_intro … (ⓑ{a,I}V.T2))
+ [1,3: /2 width=4 by fqu_bind_dx, cpys_bind/
+ | #H0 destruct /2 width=1 by/
+ ]
+| #I #G #L #V #T1 #T2 #HT12 #H @(ex3_intro … (ⓕ{I}V.T2))
+ [1,3: /2 width=4 by fqu_flat_dx, cpys_flat/
+ | #H0 destruct /2 width=1 by/
+ ]
+| #G #L #K #T1 #U1 #e #HLK #HTU1 #T2 #HT12 #H elim (lift_total T2 0 (e+1))
+ #U2 #HTU2 @(ex3_intro … U2)
+ [1,3: /2 width=10 by cpys_lift, fqu_drop/
+ | #H0 destruct /3 width=5 by lift_inj/
+]
+qed-.
+
+lemma fquq_cpys_trans_neq: ∀G1,G2,L1,L2,T1,T2. ⦃G1, L1, T1⦄ ⊐⸮ ⦃G2, L2, T2⦄ →
+ ∀U2. ⦃G2, L2⦄ ⊢ T2 ▶* U2 → (T2 = U2 → ⊥) →
+ ∃∃U1. ⦃G1, L1⦄ ⊢ T1 ▶* U1 & T1 = U1 → ⊥ & ⦃G1, L1, U1⦄ ⊐⸮ ⦃G2, L2, U2⦄.
+#G1 #G2 #L1 #L2 #T1 #T2 #H12 #U2 #HTU2 #H elim (fquq_inv_gen … H12) -H12
+[ #H12 elim (fqu_cpys_trans_neq … H12 … HTU2 H) -T2
+ /3 width=4 by fqu_fquq, ex3_intro/
+| * #HG #HL #HT destruct /3 width=4 by ex3_intro/
+]
+qed-.
+
+lemma fqup_cpys_trans_neq: ∀G1,G2,L1,L2,T1,T2. ⦃G1, L1, T1⦄ ⊐+ ⦃G2, L2, T2⦄ →
+ ∀U2. ⦃G2, L2⦄ ⊢ T2 ▶* U2 → (T2 = U2 → ⊥) →
+ ∃∃U1. ⦃G1, L1⦄ ⊢ T1 ▶* U1 & T1 = U1 → ⊥ & ⦃G1, L1, U1⦄ ⊐+ ⦃G2, L2, U2⦄.
+#G1 #G2 #L1 #L2 #T1 #T2 #H @(fqup_ind_dx … H) -G1 -L1 -T1
+[ #G1 #L1 #T1 #H12 #U2 #HTU2 #H elim (fqu_cpys_trans_neq … H12 … HTU2 H) -T2
+ /3 width=4 by fqu_fqup, ex3_intro/
+| #G #G1 #L #L1 #T #T1 #H1 #_ #IH12 #U2 #HTU2 #H elim (IH12 … HTU2 H) -T2
+ #U1 #HTU1 #H #H12 elim (fqu_cpys_trans_neq … H1 … HTU1 H) -T1
+ /3 width=8 by fqup_strap2, ex3_intro/
+]
+qed-.
+
+lemma fqus_cpys_trans_neq: ∀G1,G2,L1,L2,T1,T2. ⦃G1, L1, T1⦄ ⊐* ⦃G2, L2, T2⦄ →
+ ∀U2. ⦃G2, L2⦄ ⊢ T2 ▶* U2 → (T2 = U2 → ⊥) →
+ ∃∃U1. ⦃G1, L1⦄ ⊢ T1 ▶* U1 & T1 = U1 → ⊥ & ⦃G1, L1, U1⦄ ⊐* ⦃G2, L2, U2⦄.
+#G1 #G2 #L1 #L2 #T1 #T2 #H12 #U2 #HTU2 #H elim (fqus_inv_gen … H12) -H12
+[ #H12 elim (fqup_cpys_trans_neq … H12 … HTU2 H) -T2
+ /3 width=4 by fqup_fqus, ex3_intro/
+| * #HG #HL #HT destruct /3 width=4 by ex3_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/notation/relations/psubstsnstar_3.ma".
+include "basic_2/relocation/lpx_sn.ma".
+include "basic_2/substitution/cpys.ma".
+
+(* SN EXTENDED MULTIPLE SUBSTITUTION FOR LOCAL ENVIRONMENTS *****************)
+
+definition lpys: relation3 genv lenv lenv ≝ λG. lpx_sn (cpys G).
+
+interpretation
+ "extended multiple substitution (local environment, sn variant)"
+ 'PSubstSnStar G L1 L2 = (lpys G L1 L2).
+
+(* Basic inversion lemmas ***************************************************)
+
+lemma lpys_inv_atom1: ∀G,L2. ⦃G, ⋆⦄ ⊢ ▶* L2 → L2 = ⋆.
+/2 width=4 by lpx_sn_inv_atom1_aux/ qed-.
+
+lemma lpys_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 lpys_inv_atom2: ∀G,L1. ⦃G, L1⦄ ⊢ ▶* ⋆ → L1 = ⋆.
+/2 width=4 by lpx_sn_inv_atom2_aux/ qed-.
+
+lemma lpys_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-.
+
+lemma lpys_inv_pair: ∀I1,I2,G,L1,L2,V1,V2. ⦃G, L1.ⓑ{I1}V1⦄ ⊢ ▶* L2.ⓑ{I2}V2 →
+ ∧∧ ⦃G, L1⦄ ⊢ ▶* L2 & ⦃G, L1⦄ ⊢ V1 ▶* V2 & I1 = I2.
+/2 width=1 by lpx_sn_inv_pair/ qed-.
+
+(* Basic properties *********************************************************)
+
+lemma lpys_refl: ∀G,L. ⦃G, L⦄ ⊢ ▶* L.
+/2 width=1 by lpx_sn_refl/ qed.
+
+lemma lpys_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 lpys_fwd_length: ∀G,L1,L2. ⦃G, 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/relocation/lpx_sn_ldrop.ma".
+include "basic_2/substitution/cpys_lift.ma".
+include "basic_2/substitution/lpys.ma".
+
+(* SN EXTENDED MULTIPLE SUBSTITUTION FOR LOCAL ENVIRONMENTS *****************)
+
+(* Properies on local environment slicing ***********************************)
+
+lemma lpys_ldrop_conf: ∀G. dropable_sn (lpys G).
+/3 width=6 by lpx_sn_deliftable_dropable, cpys_inv_lift1/ qed-.
+
+lemma ldrop_lpys_trans: ∀G. dedropable_sn (lpys G).
+/3 width=10 by lpx_sn_liftable_dedropable, cpys_lift/ qed-.
+
+lemma lpys_ldrop_trans_O1: ∀G. dropable_dx (lpys G).
+/2 width=3 by lpx_sn_dropable/ qed-.
+
+(* Properties on supclosure *************************************************)
+
+lemma fqu_lpys_trans: ∀G1,G2,L1,L2,T1,T2. ⦃G1, L1, T1⦄ ⊐ ⦃G2, L2, T2⦄ →
+ ∀K2. ⦃G2, L2⦄ ⊢ ▶* K2 →
+ ∃∃K1,T. ⦃G1, L1⦄ ⊢ ▶* K1 & ⦃G1, L1⦄ ⊢ T1 ▶* T & ⦃G1, K1, T⦄ ⊐ ⦃G2, K2, T2⦄.
+#G1 #G2 #L1 #L2 #T1 #T2 #H elim H -G1 -G2 -L1 -L2 -T1 -T2
+/3 width=5 by fqu_lref_O, fqu_pair_sn, fqu_flat_dx, lpys_pair, ex3_2_intro/
+[ #a #I #G2 #L2 #V2 #T2 #X #H elim (lpys_inv_pair1 … H) -H
+ #K2 #W2 #HLK2 #HVW2 #H destruct
+ /3 width=5 by fqu_fquq, cpys_pair_sn, fqu_bind_dx, ex3_2_intro/
+| #G #L1 #K1 #T1 #U1 #e #HLK1 #HTU1 #K2 #HK12
+ elim (ldrop_lpys_trans … HLK1 … HK12) -HK12
+ /3 width=7 by fqu_drop, ex3_2_intro/
+]
+qed-.
+
+lemma fquq_lpys_trans: ∀G1,G2,L1,L2,T1,T2. ⦃G1, L1, T1⦄ ⊐⸮ ⦃G2, L2, T2⦄ →
+ ∀K2. ⦃G2, L2⦄ ⊢ ▶* K2 →
+ ∃∃K1,T. ⦃G1, L1⦄ ⊢ ▶* K1 & ⦃G1, L1⦄ ⊢ T1 ▶* T & ⦃G1, K1, T⦄ ⊐⸮ ⦃G2, K2, T2⦄.
+#G1 #G2 #L1 #L2 #T1 #T2 #H #K2 #HLK2 elim (fquq_inv_gen … H) -H
+[ #HT12 elim (fqu_lpys_trans … HT12 … HLK2) /3 width=5 by fqu_fquq, ex3_2_intro/
+| * #H1 #H2 #H3 destruct /2 width=5 by ex3_2_intro/
+]
+qed-.
+
+lemma lpys_fqu_trans: ∀G1,G2,L1,L2,T1,T2. ⦃G1, L1, T1⦄ ⊐ ⦃G2, L2, T2⦄ →
+ ∀K1. ⦃G1, K1⦄ ⊢ ▶* L1 →
+ ∃∃K2,T. ⦃G1, K1⦄ ⊢ T1 ▶* T & ⦃G1, K1, T⦄ ⊐ ⦃G2, K2, T2⦄ & ⦃G2, K2⦄ ⊢ ▶* L2.
+#G1 #G2 #L1 #L2 #T1 #T2 #H elim H -G1 -G2 -L1 -L2 -T1 -T2
+/3 width=7 by fqu_pair_sn, fqu_bind_dx, fqu_flat_dx, lpys_pair, ex3_2_intro/
+[ #I #G1 #L1 #V1 #X #H elim (lpys_inv_pair2 … H) -H
+ #K1 #W1 #HKL1 #HWV1 #H destruct elim (lift_total V1 0 1)
+ /4 width=7 by cpys_delta, fqu_drop, ldrop_drop, ex3_2_intro/
+| #G #L1 #K1 #T1 #U1 #e #HLK1 #HTU1 #L0 #HL01
+ elim (lpys_ldrop_trans_O1 … HL01 … HLK1) -L1
+ /3 width=5 by fqu_drop, ex3_2_intro/
+]
+qed-.
+
+lemma lpys_fquq_trans: ∀G1,G2,L1,L2,T1,T2. ⦃G1, L1, T1⦄ ⊐⸮ ⦃G2, L2, T2⦄ →
+ ∀K1. ⦃G1, K1⦄ ⊢ ▶* L1 →
+ ∃∃K2,T. ⦃G1, K1⦄ ⊢ T1 ▶* T & ⦃G1, K1, T⦄ ⊐⸮ ⦃G2, K2, T2⦄ & ⦃G2, K2⦄ ⊢ ▶* L2.
+#G1 #G2 #L1 #L2 #T1 #T2 #H #K1 #HKL1 elim (fquq_inv_gen … H) -H
+[ #HT12 elim (lpys_fqu_trans … HT12 … HKL1) /3 width=5 by fqu_fquq, ex3_2_intro/
+| * #H1 #H2 #H3 destruct /2 width=5 by ex3_2_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/substitution/cpys_cpys.ma".
+
+(* SN EXTENDED MULTIPLE SUBSTITUTION FOR LOCAL ENVIRONMENTS *****************)
+
+(* Main properties **********************************************************)
+
+theorem lpys_trans: ∀G. Transitive … (lpys G).
+/3 width=5 by lpx_sn_trans, cpys_trans_lpys/
+qed-.
--- /dev/null
+(**************************************************************************)
+(* ___ *)
+(* ||M|| *)
+(* ||A|| A project by Andrea Asperti *)
+(* ||T|| *)
+(* ||I|| Developers: *)
+(* ||T|| The HELM team. *)
+(* ||A|| http://helm.cs.unibo.it *)
+(* \ / *)
+(* \ / This file is distributed under the terms of the *)
+(* v GNU General Public License Version 2 *)
+(* *)
+(**************************************************************************)
+
+(* NOTATION FOR THE FORMAL SYSTEM λδ ****************************************)
+
+notation "hvbox( L1 break ⊆ break term 46 L2 )"
+ non associative with precedence 45
+ for @{ 'LRSubEq $L1 $L2 }.
--- /dev/null
+(**************************************************************************)
+(* ___ *)
+(* ||M|| *)
+(* ||A|| A project by Andrea Asperti *)
+(* ||T|| *)
+(* ||I|| Developers: *)
+(* ||T|| The HELM team. *)
+(* ||A|| http://helm.cs.unibo.it *)
+(* \ / *)
+(* \ / This file is distributed under the terms of the *)
+(* v GNU General Public License Version 2 *)
+(* *)
+(**************************************************************************)
+
+include "basic_2/notation/relations/lrsubeq_2.ma".
+include "basic_2/relocation/ldrop.ma".
+
+(* LOCAL ENVIRONMENT REFINEMENT FOR EXTENDED SUBSTITUTION *******************)
+
+inductive lsuby: relation lenv ≝
+| lsuby_atom: ∀L. lsuby L (⋆)
+| lsuby_pair: ∀I1,I2,L1,L2,V. lsuby L1 L2 → lsuby (L1.ⓑ{I1}V) (L2.ⓑ{I2}V)
+.
+
+interpretation
+ "local environment refinement (extended substitution)"
+ 'LRSubEq L1 L2 = (lsuby L1 L2).
+
+(* Basic properties *********************************************************)
+
+lemma lsuby_refl: ∀L. L ⊆ L.
+#L elim L -L /2 width=1 by lsuby_pair/
+qed.
+
+lemma lsuby_sym: ∀L1,L2. L1 ⊆ L2 → |L1| = |L2| → L2 ⊆ L1.
+#L1 #L2 #H elim H -L1 -L2
+[ #L1 #H >(length_inv_zero_dx … H) -L1 //
+| #I1 #I2 #L1 #L2 #V #_ #IHL12 #H lapply (injective_plus_l … H) -H
+ /3 width=1 by lsuby_pair/
+]
+qed-.
+
+(* Basic inversion lemmas ***************************************************)
+
+fact lsuby_inv_atom1_aux: ∀L1,L2. L1 ⊆ L2 → L1 = ⋆ → L2 = ⋆.
+#L1 #L2 * -L1 -L2 //
+#I1 #I2 #L1 #L2 #V #_ #H destruct
+qed-.
+
+lemma lsuby_inv_atom1: ∀L2. ⋆ ⊆ L2 → L2 = ⋆.
+/2 width=3 by lsuby_inv_atom1_aux/ qed-.
+
+fact lsuby_inv_pair1_aux: ∀L1,L2. L1 ⊆ L2 → ∀J1,K1,W. L1 = K1.ⓑ{J1}W →
+ L2 = ⋆ ∨ ∃∃I2,K2. K1 ⊆ K2 & L2 = K2.ⓑ{I2}W.
+#L1 #L2 * -L1 -L2
+[ #L #J1 #K1 #W #H destruct /2 width=1 by or_introl/
+| #I1 #I2 #L1 #L2 #V #HL12 #J1 #K1 #W #H destruct /3 width=4 by ex2_2_intro, or_intror/
+]
+qed-.
+
+lemma lsuby_inv_pair1: ∀I1,K1,L2,W. K1.ⓑ{I1}W ⊆ L2 →
+ L2 = ⋆ ∨ ∃∃I2,K2. K1 ⊆ K2 & L2 = K2.ⓑ{I2}W.
+/2 width=4 by lsuby_inv_pair1_aux/ qed-.
+
+fact lsuby_inv_pair2_aux: ∀L1,L2. L1 ⊆ L2 → ∀J2,K2,W. L2 = K2.ⓑ{J2}W →
+ ∃∃I1,K1. K1 ⊆ K2 & L1 = K1.ⓑ{I1}W.
+#L1 #L2 * -L1 -L2
+[ #L #J2 #K2 #W #H destruct
+| #I1 #I2 #L1 #L2 #V #HL12 #J2 #K2 #W #H destruct /2 width=4 by ex2_2_intro/
+]
+qed-.
+
+lemma lsuby_inv_pair2: ∀I2,L1,K2,W. L1 ⊆ K2.ⓑ{I2}W →
+ ∃∃I1,K1. K1 ⊆ K2 & L1 = K1.ⓑ{I1}W.
+/2 width=4 by lsuby_inv_pair2_aux/ qed-.
+
+(* Basic forward lemmas *****************************************************)
+
+lemma lsuby_fwd_length: ∀L1,L2. L1 ⊆ L2 → |L2| ≤ |L1|.
+#L1 #L2 #H elim H -L1 -L2 /2 width=1 by monotonic_le_plus_l/
+qed-.
+
+lemma lsuby_ldrop_trans: ∀L1,L2. L1 ⊆ L2 →
+ ∀I2,K2,W,s,i. ⇩[s, 0, i] L2 ≡ K2.ⓑ{I2}W →
+ ∃∃I1,K1. K1 ⊆ K2 & ⇩[s, 0, i] L1 ≡ K1.ⓑ{I1}W.
+#L1 #L2 #H elim H -L1 -L2
+[ #L #J2 #K2 #W #s #i #H
+ elim (ldrop_inv_atom1 … H) -H #H destruct
+| #I1 #I2 #L1 #L2 #V #HL12 #IHL12 #J2 #K2 #W #s #i #H
+ elim (ldrop_inv_O1_pair1 … H) -H * #Hi #HLK2 destruct [ -IHL12 | -HL12 ]
+ [ /3 width=4 by ldrop_pair, ex2_2_intro/
+ | elim (IHL12 … HLK2) -IHL12 -HLK2 * /3 width=4 by ldrop_drop_lt, ex2_2_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/substitution/lsuby.ma".
+
+(* LOCAL ENVIRONMENT REFINEMENT FOR EXTENDED SUBSTITUTION *******************)
+
+(* Main properties **********************************************************)
+
+theorem lsuby_trans: Transitive … lsuby.
+#L1 #L #H elim H -L1 -L
+[ #L1 #X #H lapply (lsuby_inv_atom1 … H) -H //
+| #I1 #I #L1 #L #V #_ #IHL1 #X #H elim (lsuby_inv_pair1 … H) -H // *
+ #I2 #L2 #HL2 #H destruct /3 width=1 by lsuby_pair/
+]
+qed-.
--- /dev/null
+(**************************************************************************)
+(* ___ *)
+(* ||M|| *)
+(* ||A|| A project by Andrea Asperti *)
+(* ||T|| *)
+(* ||I|| Developers: *)
+(* ||T|| The HELM team. *)
+(* ||A|| http://helm.cs.unibo.it *)
+(* \ / *)
+(* \ / This file is distributed under the terms of the *)
+(* v GNU General Public License Version 2 *)
+(* *)
+(**************************************************************************)
+
+(* NOTATION FOR THE FORMAL SYSTEM λδ ****************************************)
+
+notation "hvbox( ⦃ term 46 G , break term 46 L1 ⦄ ⊢ ▶ * break term 46 L2 )"
+ non associative with precedence 45
+ for @{ 'PSubstSnStar $G $L1 $L2 }.
--- /dev/null
+(**************************************************************************)
+(* ___ *)
+(* ||M|| *)
+(* ||A|| A project by Andrea Asperti *)
+(* ||T|| *)
+(* ||I|| Developers: *)
+(* ||T|| The HELM team. *)
+(* ||A|| http://helm.cs.unibo.it *)
+(* \ / *)
+(* \ / This file is distributed under the terms of the *)
+(* v GNU General Public License Version 2 *)
+(* *)
+(**************************************************************************)
+
+(* NOTATION FOR THE FORMAL SYSTEM λδ ****************************************)
+
+notation "hvbox( ⦃ term 46 G , break term 46 L ⦄ ⊢ break term 46 T1 break ▶ * break term 46 T2 )"
+ non associative with precedence 45
+ for @{ 'PSubstStar $G $L $T1 $T2 }.
--- /dev/null
+(**************************************************************************)
+(* ___ *)
+(* ||M|| *)
+(* ||A|| A project by Andrea Asperti *)
+(* ||T|| *)
+(* ||I|| Developers: *)
+(* ||T|| The HELM team. *)
+(* ||A|| http://helm.cs.unibo.it *)
+(* \ / *)
+(* \ / This file is distributed under the terms of the *)
+(* v GNU General Public License Version 2 *)
+(* *)
+(**************************************************************************)
+
+include "basic_2/substitution/cpys_alt.ma".
+include "basic_2/reduction/cpx.ma".
+
+(* CONTEXT-SENSITIVE EXTENDED PARALLEL REDUCTION FOR TERMS ******************)
+
+(* Properties on local environment refinement for extended substitution *****)
+
+lemma lsuby_cpx_trans: ∀h,g,G. lsub_trans … (cpx h g G) (lsuby 0 (∞)).
+#h #g #G #L1 #T1 #T2 #H elim H -G -L1 -T1 -T2
+[ //
+| /2 width=2 by cpx_sort/
+| #I #G #L1 #K1 #V1 #V2 #W2 #i #HLK1 #_ #HVW2 #IHV12 #L2 #HL12
+ elim (lsuby_ldrop_trans_be … HL12 … HLK1) // -HL12 -HLK1 /3 width=7 by cpx_delta/
+|4,9: /4 width=1 by cpx_bind, cpx_beta, lsuby_pair_O_Y/
+|5,7,8: /3 width=1 by cpx_flat, cpx_tau, cpx_ti/
+|6,10: /4 width=3 by cpx_zeta, cpx_theta, lsuby_pair_O_Y/
+]
+qed-.
+
+(* Properties on context-sensitive extended multiple substitution for terms *)
+
+lemma cpys_cpx: ∀h,g,G,L,T1,T2,d,e. ⦃G, L⦄ ⊢ T1 ▶*[d, e] T2 → ⦃G, L⦄ ⊢ T1 ➡[h, g] T2.
+#h #g #G #L #T1 #T2 #d #e #H @(cpys_ind_alt … H) -G -L -T1 -T2 -d -e
+/2 width=7 by cpx_delta, cpx_bind, cpx_flat/
+qed.
+
+lemma cpy_cpx: ∀h,g,G,L,T1,T2,d,e. ⦃G, L⦄ ⊢ T1 ▶[d, e] T2 → ⦃G, L⦄ ⊢ T1 ➡[h, g] T2.
+/3 width=3 by cpy_cpys, cpys_cpx/ qed.
--- /dev/null
+(**************************************************************************)
+(* ___ *)
+(* ||M|| *)
+(* ||A|| A project by Andrea Asperti *)
+(* ||T|| *)
+(* ||I|| Developers: *)
+(* ||T|| The HELM team. *)
+(* ||A|| http://helm.cs.unibo.it *)
+(* \ / *)
+(* \ / This file is distributed under the terms of the *)
+(* v GNU General Public License Version 2 *)
+(* *)
+(**************************************************************************)
+
+include "basic_2/substitution/cpys_alt.ma".
+include "basic_2/reduction/cpx.ma".
+
+(* CONTEXT-SENSITIVE EXTENDED PARALLEL REDUCTION FOR TERMS ******************)
+
+(* Properties on context-sensitive extended multiple substitution for terms *)
+
+lemma cpys_cpx: ∀h,g,G,L,T1,T2,d,e. ⦃G, L⦄ ⊢ T1 ▶*[d, e] T2 → ⦃G, L⦄ ⊢ T1 ➡[h, g] T2.
+#h #g #G #L #T1 #T2 #d #e #H @(cpys_ind_alt … H) -G -L -T1 -T2 -d -e
+/2 width=7 by cpx_delta, cpx_bind, cpx_flat/
+qed.
+
+lemma cpy_cpx: ∀h,g,G,L,T1,T2,d,e. ⦃G, L⦄ ⊢ T1 ▶[d, e] T2 → ⦃G, L⦄ ⊢ T1 ➡[h, g] T2.
+/3 width=3 by cpy_cpys, cpys_cpx/ qed.
+
+lemma cpx_cpy_trans: ∀h,g,G,L,T1,T. ⦃G, L⦄ ⊢ T1 ➡[h, g] T →
+ ∀T2,d,e. ⦃G, L⦄ ⊢ T ▶[d, e] T2 → ⦃G, L⦄ ⊢ T1 ➡[h, g] T2.
+#h #g #G #L #T1 #T #H elim H -G -L -T1 -T
+[ #I #G #L #X #d #e #H elim (cpy_inv_atom1 … H) //
+ * /2 width=3 by cpy_cpx/
+| #G #L #k #l #Hkl #X #d #e #H >(cpy_inv_sort1 … H) -X /2 width=2 by cpx_sort/
+| #I #G #L #K #V1 #V #W #i #HLK #_ #HVW #IHV1 #X #d #e #H
+ lapply (ldrop_fwd_drop2 … HLK) #H0
+ lapply (cpy_weak … H 0 (∞) ? ?) -H // #H
+ elim (cpy_inv_lift1_be … H … H0 … HVW) -H -H0 -HVW
+ /3 width=7 by cpx_delta/
+| #a #I #G #L #V1 #V #T1 #T #_ #_ #IHV1 #IHT1 #X #d #e #H elim (cpy_inv_bind1 … H) -H
+ #V2 #T2 #HV2 #HT2 #H destruct
+ /5 width=7 by cpx_bind, lsuby_cpy_trans, lsuby_succ/
+| #I #G #L #V1 #V #T1 #T #_ #_ #IHV1 #IHT1 #X #d #e #H elim (cpy_inv_flat1 … H) -H
+ #V2 #T2 #HV2 #HT2 #H destruct /3 width=3 by cpx_flat/
+| #G #L #V1 #U1 #U #T #_ #HTU #IHU1 #T2 #d #e #HT2
+ lapply (cpy_weak … HT2 0 (∞) ? ?) -HT2 // #HT2
+ elim (lift_total T2 0 1) #U2 #HTU2
+ lapply (cpy_lift_be … HT2 (L.ⓓV1) … (Ⓕ) … HTU … HTU2 ? ?) -T
+ /3 width=3 by cpx_zeta, ldrop_drop/
+| /3 width=3 by cpx_tau/
+| /3 width=3 by cpx_ti/
+| #a #G #L #V1 #V #W1 #W #T1 #T #_ #_ #_ #IHV1 #IHW1 #IHT1 #X #d #e #HX
+ elim (cpy_inv_bind1 … HX) -HX #Y #T2 #HY #HT2 #H destruct
+ elim (cpy_inv_flat1 … HY) -HY #W2 #V2 #HW2 #HV2 #H destruct
+ /5 width=7 by cpx_beta, lsuby_cpy_trans, lsuby_succ/
+| #a #G #L #V1 #V #U #W1 #W #T1 #T #_ #HVU #_ #_ #IHV1 #IHW1 #IHT1 #X #d #e #HX
+ elim (cpy_inv_bind1 … HX) -HX #W2 #Y #HW2 #HY #H destruct
+ elim (cpy_inv_flat1 … HY) -HY #U2 #T2 #HU2 #HT2 #H destruct
+ lapply (cpy_weak … HU2 0 (∞) ? ?) -HU2 // #HU2
+ elim (cpy_inv_lift1_be … HU2 L … HVU) -U
+ /5 width=7 by cpx_theta, lsuby_cpy_trans, lsuby_succ, ldrop_drop/
+]
+qed-.
+
+lemma cpx_cpys_trans: ∀h,g,G,L,T1,T. ⦃G, L⦄ ⊢ T1 ➡[h, g] T →
+ ∀T2,d,e. ⦃G, L⦄ ⊢ T ▶*[d, e] T2 → ⦃G, L⦄ ⊢ T1 ➡[h, g] T2.
+#h #g #G #L #T1 #T #HT1 #T2 #d #e #H @(cpys_ind … H) -T2
+/2 width=5 by cpx_cpy_trans/
+qed-.
--- /dev/null
+(**************************************************************************)
+(* ___ *)
+(* ||M|| *)
+(* ||A|| A project by Andrea Asperti *)
+(* ||T|| *)
+(* ||I|| Developers: *)
+(* ||T|| The HELM team. *)
+(* ||A|| http://helm.cs.unibo.it *)
+(* \ / *)
+(* \ / This file is distributed under the terms of the *)
+(* v GNU General Public License Version 2 *)
+(* *)
+(**************************************************************************)
+
+include "basic_2/reduction/cpx_cpys.ma".
+include "basic_2/computation/cpxs.ma".
+
+(* CONTEXT-SENSITIVE EXTENDED PARALLEL COMPUTATION ON TERMS *****************)
+
+(* Properties on local environment refinement for extended substitution *****)
+
+lemma lsuby_cpxs_trans: ∀h,g,G. lsub_trans … (cpxs h g G) (lsuby 0 (∞)).
+/3 width=5 by lsuby_cpx_trans, LTC_lsub_trans/
+qed-.
--- /dev/null
+(**************************************************************************)
+(* ___ *)
+(* ||M|| *)
+(* ||A|| A project by Andrea Asperti *)
+(* ||T|| *)
+(* ||I|| Developers: *)
+(* ||T|| The HELM team. *)
+(* ||A|| http://helm.cs.unibo.it *)
+(* \ / *)
+(* \ / This file is distributed under the terms of the *)
+(* v GNU General Public License Version 2 *)
+(* *)
+(**************************************************************************)
+
+include "basic_2/relocation/cpy_lift.ma".
+include "basic_2/substitution/cpys.ma".
+include "basic_2/reduction/lpx_ldrop.ma".
+
+(* SN EXTENDED PARALLEL REDUCTION FOR LOCAL ENVIRONMENTS ********************)
+
+(* Properties on context-sensitive extended substitution for terms **********)
+
+lemma cpx_cpy_trans_lpx: ∀h,g,G,L1,T1,T. ⦃G, L1⦄ ⊢ T1 ➡[h, g] T →
+ ∀L2. ⦃G, L1⦄ ⊢ ➡[h, g] L2 →
+ ∀T2,d,e. ⦃G, L2⦄ ⊢ T ▶[d, e] T2 → ⦃G, L1⦄ ⊢ T1 ➡[h, g] T2.
+#h #g #G #L1 #T1 #T #H elim H -G -L1 -T1 -T
+[ #J #G #L1 #L2 #HL12 #T2 #d #e #H elim (cpy_inv_atom1 … H) -H //
+ * #I #K2 #V2 #i #_ #_ #HLK2 #HVT2 #H destruct
+ elim (lpx_ldrop_trans_O1 … HL12 … HLK2) -L2 #X #HLK1 #H
+ elim (lpx_inv_pair2 … H) -H #K1 #V1 #_ #HV12 #H destruct
+ /2 width=7 by cpx_delta/
+| #G #L1 #k #l #Hkl #L2 #_ #X #d #e #H >(cpy_inv_sort1 … H) -X /2 width=2 by cpx_sort/
+| #I #G #L1 #K1 #V1 #V #T #i #HLK1 #_ #HVT #IHV1 #L2 #HL12 #T2 #d #e #HT2
+ elim (lpx_ldrop_conf … HLK1 … HL12) -HL12 #X #H #HLK2
+ elim (lpx_inv_pair1 … H) -H #K2 #V0 #HK12 #_ #H destruct
+ lapply (ldrop_fwd_drop2 … HLK2) -V0 #HLK2
+ lapply (cpy_weak … HT2 0 (∞) ? ?) -HT2 // #HT2
+ elim (cpy_inv_lift1_be … HT2 … HLK2 … HVT) -HT2 -HLK2 -HVT
+ /3 width=7 by cpx_delta/
+| #a #I #G #L1 #V1 #V #T1 #T #HV1 #_ #IHV1 #IHT1 #L2 #HL12 #X #d #e #H elim (cpy_inv_bind1 … H) -H
+ #V2 #T2 #HV2 #HT2 #H destruct /4 width=5 by lpx_pair, cpx_bind/
+| #I #G #L1 #V1 #V #T1 #T #_ #_ #IHV1 #IHT1 #L2 #HL12 #X #d #e #H elim (cpy_inv_flat1 … H) -H
+ #V2 #T2 #HV2 #HT2 #H destruct /3 width=5 by cpx_flat/
+| #G #L1 #V1 #U1 #U #T #_ #HTU #IHU1 #L2 #HL12 #T2 #d #e #HT2
+ lapply (cpy_weak … HT2 0 (∞) ? ?) -HT2 // #HT2
+ elim (lift_total T2 0 1) #U2 #HTU2
+ lapply (cpy_lift_be … HT2 (L2.ⓓV1) … (Ⓕ) … HTU … HTU2 ? ?) -T
+ /4 width=5 by cpx_zeta, lpx_pair, ldrop_drop/
+| /3 width=5 by cpx_tau/
+| /3 width=5 by cpx_ti/
+| #a #G #L1 #V1 #V #W1 #W #T1 #T #HV1 #HW1 #_ #IHV1 #IHW1 #IHT1 #L2 #HL12 #X #d #e #HX
+ elim (cpy_inv_bind1 … HX) -HX #Y #T2 #HY #HT2 #H destruct
+ elim (cpy_inv_flat1 … HY) -HY #W2 #V2 #HW2 #HV2 #H destruct
+ /5 width=11 by lpx_pair, cpx_beta, lsuby_cpy_trans, lsuby_succ/
+| #a #G #L1 #V1 #V #U #W1 #W #T1 #T #_ #HVU #HW1 #_ #IHV1 #IHW1 #IHT1 #L2 #HL12 #X #d #e #HX
+ elim (cpy_inv_bind1 … HX) -HX #W2 #Y #HW2 #HY #H destruct
+ elim (cpy_inv_flat1 … HY) -HY #U2 #T2 #HU2 #HT2 #H destruct
+ lapply (cpy_weak … HU2 0 (∞) ? ?) -HU2 // #HU2
+ elim (cpy_inv_lift1_be … HU2 L2 … HVU) -U
+ /4 width=7 by lpx_pair, cpx_theta, ldrop_drop/
+]
+qed-.
+
+lemma cpx_cpys_trans_lpx: ∀h,g,G,L1,T1,T. ⦃G, L1⦄ ⊢ T1 ➡[h, g] T →
+ ∀L2. ⦃G, L1⦄ ⊢ ➡[h, g] L2 →
+ ∀T2,d,e. ⦃G, L2⦄ ⊢ T ▶*[d, e] T2 → ⦃G, L1⦄ ⊢ T1 ➡[h, g] T2.
+#h #g #G #L1 #T1 #T #HT1 #L2 #HL12 #T2 #d #e #H @(cpys_ind … H) -T2
+/2 width=7 by cpx_cpy_trans_lpx/
+qed-.
--- /dev/null
+(*
+lemma lsuby_weak: ∀L1,L2,d1,e1. L1 ⊑×[d1, e1] L2 →
+ ∀d2,e2. d1 ≤ d2 → e2 ≤ e1 → L1 ⊑×[d2, e2] L2.
+#L1 #L2 #d1 #e1 #H elim H -L1 -L2 -d1 -e1 //
+[ #I1 #I2 #L1 #L2 #V1 #V2 #HL12 #_ #d2 #e2 #_ #He21
+ >(yle_inv_O2 … He21) -He21
+ /4 width=3 by lsuby_fwd_length, lsuby_O1, monotonic_le_plus_l/
+| #I1 #I2 #L1 #L2 #V #e #HL12 #IHL12 #d2 #e2 #_ #He21
+ elim (ynat_cases e2) /4 width=3 by lsuby_fwd_length, lsuby_O1, monotonic_le_plus_l/
+ * #e0 #H destruct lapply (yle_inv_succ … He21) -He21 #He21
+ elim (ynat_cases d2) /3 width=1 by lsuby_pair/
+ * #d0 #H destruct @lsuby_succ @IHL12 //
+ [ 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 *)
-(* *)
-(**************************************************************************)
-
-(* NOTATION FOR THE FORMAL SYSTEM λδ ****************************************)
-
-notation "hvbox( L ⊢ break term 46 i ~ ϵ 𝐅 * [ break term 46 d ] ⦃ break term 46 T ⦄ )"
- non associative with precedence 45
- for @{ 'CoFreeStar $L $i $d $T }.
--- /dev/null
+(**************************************************************************)
+(* ___ *)
+(* ||M|| *)
+(* ||A|| A project by Andrea Asperti *)
+(* ||T|| *)
+(* ||I|| Developers: *)
+(* ||T|| The HELM team. *)
+(* ||A|| http://helm.cs.unibo.it *)
+(* \ / *)
+(* \ / This file is distributed under the terms of the *)
+(* v GNU General Public License Version 2 *)
+(* *)
+(**************************************************************************)
+
+(* NOTATION FOR THE FORMAL SYSTEM λδ ****************************************)
+
+notation "hvbox( L ⊢ break term 46 i ϵ 𝐅 * [ break term 46 d ] ⦃ break term 46 T ⦄ )"
+ non associative with precedence 45
+ for @{ 'FreeStar $L $i $d $T }.
--- /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/fqup.ma".
+include "basic_2/substitution/frees_lift.ma".
+include "basic_2/reduction/lpx_ldrop.ma".
+
+(* SN EXTENDED PARALLEL REDUCTION FOR LOCAL ENVIRONMENTS ********************)
+(*
+lemma yle_plus2_to_minus_inj2: ∀x,y:ynat. ∀z:nat. x ≤ y + z → x - z ≤ y.
+/2 width=1 by monotonic_yle_minus_dx/ qed-.
+
+lemma yle_plus2_to_minus_inj1: ∀x,y:ynat. ∀z:nat. x ≤ z + y → x - z ≤ y.
+/2 width=1 by yle_plus2_to_minus_inj2/ qed-.
+
+lemma cofrees_lsuby_conf: ∀L1,U,i. L1 ⊢ i ~ϵ 𝐅*⦃U⦄ →
+ ∀L2. lsuby L1 L2 → L2 ⊢ i ~ϵ 𝐅*⦃U⦄.
+/3 width=3 by lsuby_cpys_trans/ qed-.
+
+lemma lpx_cpx_cofrees_conf: ∀h,g,G,L1,U1,U2. ⦃G, L1⦄ ⊢ U1 ➡[h, g] U2 →
+ ∀L2. ⦃G, L1⦄ ⊢ ➡[h, g] L2 →
+ ∀i. L1 ⊢ i ~ϵ 𝐅*⦃U1⦄ → L2 ⊢ i ~ϵ 𝐅*⦃U2⦄.
+#h #g #G #L1 #U1 @(fqup_wf_ind_eq … G L1 U1) -G -L1 -U1
+#G0 #L0 #U0 #IH #G #L1 * *
+[ -IH #k #HG #HL #HU #U2 #H elim (cpx_inv_sort1 … H) -H
+ [| * #l #_ ] #H destruct //
+| #j #HG #HL #HU #U2 #H #L2 #HL12 #i #Hi elim (cpx_inv_lref1 … H) -H
+ [ #H destruct elim (lt_or_eq_or_gt i j) #Hji
+ [ -IH -HL12 /2 width=4 by cofrees_lref_gt/
+ | -IH -HL12 destruct elim (cofrees_inv_lref_eq … Hi)
+ | elim (lt_or_ge j (|L2|)) /2 width=5 by cofrees_lref_free/ #Hj
+ elim (ldrop_O1_lt (Ⓕ) L1 j) [2: >(lpx_fwd_length … HL12) // ] #I #K1 #W1 #HLK1
+ elim (lpx_ldrop_conf … HLK1 … HL12) -HL12 #Y #H #HLK2
+ elim (lpx_inv_pair1 … H) -H #K2 #W2 #HK12 #HW12 #H destruct
+ lapply (cofrees_inv_lref_lt … Hi … HLK1) -Hi // #HW1
+ lapply (IH … HW12 … HK12 … HW1) /2 width=2 by fqup_lref/ -L1 -K1 -W1 #HW2
+ /2 width=9 by cofrees_lref_lt/ (**) (* full auto too slow *)
+ ]
+ | * #I #K1 #W1 #W0 #HLK1 #HW10 #HW0U2 elim (lt_or_ge j i) #Hji
+ [ lapply (ldrop_fwd_drop2 … HLK1) #H0
+ elim (lpx_ldrop_conf … H0 … HL12) #K2 #HK12 #HLK2
+ @(cofrees_lift_ge … HLK2 … HW0U2) //
+ @(IH … HW10) /2 width=2 by fqup_lref/ -L2 -K2 -W0 -U2 -IH
+ <minus_plus /2 width=7 by cofrees_inv_lref_lt/
+ | -IH lapply (ldrop_fwd_drop2 … HLK1) -HLK1 #HLK1
+ elim (lpx_ldrop_conf … HLK1 … HL12) -I -L1 -W1
+ /2 width=12 by cofrees_lift_be/
+ ]
+ ]
+| -IH #p #HG #HL #HU #U2 #H lapply (cpx_inv_gref1 … H) -H
+ #H destruct //
+| #a #I #W1 #U1 #HG #HL #HU #X #HX #L2 #HL12 #i #Hi destruct
+ elim (cofrees_inv_bind … Hi) -Hi #HW1 #HU1
+ elim (cpx_inv_bind1 … HX) -HX
+ [ * #W2 #U2 #HW12 #HU12 #H destruct /4 width=8 by cofrees_bind, lpx_pair/
+ |
+ ]
+| #I #W1 #X1 #HG #HL #HU #X2 #HX2 #L2 #HL12 #i #Hi destruct
+ elim (cofrees_inv_flat … Hi) -Hi #HW1 #HX1
+ elim (cpx_inv_flat1 … HX2) -HX2 *
+ [ #W2 #U2 #HW12 #HU12 #H destruct /3 width=7 by cofrees_flat/
+ | #HU12 #H destruct /2 width=7 by/
+ | #HW12 #H destruct /2 width=7 by/
+ | #b #W2 #V1 #V2 #U1 #U2 #HW12 #HV12 #HU12 #H1 #H2 #H3 destruct
+ elim (cofrees_inv_bind … HX1) -HX1 #HV1 #HU1
+ @cofrees_bind [ /3 width=7 by cofrees_flat/ ]
+ @(cofrees_lsuby_conf (L2.ⓛV2)) /3 width=7 by lpx_pair, lsuby_succ/
+ |
+
+
+*)
]
qed-.
-(* Note: lemma 1250 *)
lemma cpy_weak_top: ∀G,L,T1,T2,d,e.
⦃G, L⦄ ⊢ T1 ▶[d, e] T2 → ⦃G, L⦄ ⊢ T1 ▶[d, |L| - d] T2.
#G #L #T1 #T2 #d #e #H elim H -G -L -T1 -T2 -d -e //
+++ /dev/null
-(**************************************************************************)
-(* ___ *)
-(* ||M|| *)
-(* ||A|| A project by Andrea Asperti *)
-(* ||T|| *)
-(* ||I|| Developers: *)
-(* ||T|| The HELM team. *)
-(* ||A|| http://helm.cs.unibo.it *)
-(* \ / *)
-(* \ / This file is distributed under the terms of the *)
-(* v GNU General Public License Version 2 *)
-(* *)
-(**************************************************************************)
-
-include "basic_2/notation/relations/cofreestar_4.ma".
-include "basic_2/relocation/lift_neg.ma".
-include "basic_2/substitution/cpys.ma".
-
-(* CONTEXT-SENSITIVE EXCLUSION FROM FREE VARIABLES **************************)
-
-definition cofrees: relation4 ynat nat lenv term ≝
- λd,i,L,U1. ∀U2. ⦃⋆, L⦄ ⊢ U1 ▶*[d, ∞] U2 → ∃T2. ⇧[i, 1] T2 ≡ U2.
-
-interpretation
- "context-sensitive exclusion from free variables (term)"
- 'CoFreeStar L i d T = (cofrees d i L T).
-
-(* Basic forward lemmas *****************************************************)
-
-lemma cofrees_fwd_lift: ∀L,U,d,i. L ⊢ i ~ϵ 𝐅*[d]⦃U⦄ → ∃T. ⇧[i, 1] T ≡ U.
-/2 width=1 by/ qed-.
-
-lemma cofrees_fwd_bind_sn: ∀a,I,L,W,U,i,d. L ⊢ i ~ϵ 𝐅*[d]⦃ⓑ{a,I}W.U⦄ →
- L ⊢ i ~ϵ 𝐅*[d]⦃W⦄.
-#a #I #L #W1 #U #i #d #H #W2 #HW12 elim (H (ⓑ{a,I}W2.U)) /2 width=1 by cpys_bind/ -W1
-#X #H elim (lift_inv_bind2 … H) -H /2 width=2 by ex_intro/
-qed-.
-
-lemma cofrees_fwd_bind_dx: ∀a,I,L,W,U,i,d. L ⊢ i ~ϵ 𝐅*[d]⦃ⓑ{a,I}W.U⦄ →
- L.ⓑ{I}W ⊢ i+1 ~ϵ 𝐅*[⫯d]⦃U⦄.
-#a #I #L #W #U1 #i #d #H #U2 #HU12 elim (H (ⓑ{a,I}W.U2)) /2 width=1 by cpys_bind/ -U1
-#X #H elim (lift_inv_bind2 … H) -H /2 width=2 by ex_intro/
-qed-.
-
-lemma cofrees_fwd_flat_sn: ∀I,L,W,U,i,d. L ⊢ i ~ϵ 𝐅*[d]⦃ⓕ{I}W.U⦄ →
- L ⊢ i ~ϵ 𝐅*[d]⦃W⦄.
-#I #L #W1 #U #i #d #H #W2 #HW12 elim (H (ⓕ{I}W2.U)) /2 width=1 by cpys_flat/ -W1
-#X #H elim (lift_inv_flat2 … H) -H /2 width=2 by ex_intro/
-qed-.
-
-lemma cofrees_fwd_flat_dx: ∀I,L,W,U,i,d. L ⊢ i ~ϵ 𝐅*[d]⦃ⓕ{I}W.U⦄ →
- L ⊢ i ~ϵ 𝐅*[d]⦃U⦄.
-#I #L #W #U1 #i #d #H #U2 #HU12 elim (H (ⓕ{I}W.U2)) /2 width=1 by cpys_flat/ -U1
-#X #H elim (lift_inv_flat2 … H) -H /2 width=2 by ex_intro/
-qed-.
-
-(* Basic inversion lemmas ***************************************************)
-
-lemma cofrees_inv_gen: ∀L,U,U0,d,i. ⦃⋆, L⦄ ⊢ U ▶*[d, ∞] U0 → (∀T. ⇧[i, 1] T ≡ U0 → ⊥) →
- L ⊢ i ~ϵ 𝐅*[d]⦃U⦄ → ⊥.
-#L #U #U0 #d #i #HU0 #HnU0 #HU elim (HU … HU0) -L -U -d /2 width=2 by/
-qed-.
-
-lemma cofrees_inv_lref_eq: ∀L,d,i. L ⊢ i ~ϵ 𝐅*[d]⦃#i⦄ → ⊥.
-#L #d #i #H elim (H (#i)) -H //
-#X #H elim (lift_inv_lref2_be … H) -H //
-qed-.
-
-lemma cofrees_inv_bind: ∀a,I,L,W,U,i,d. L ⊢ i ~ϵ 𝐅*[d]⦃ⓑ{a,I}W.U⦄ →
- L ⊢ i ~ϵ 𝐅*[d]⦃W⦄ ∧ L.ⓑ{I}W ⊢ i+1 ~ϵ 𝐅*[⫯d]⦃U⦄.
-/3 width=8 by cofrees_fwd_bind_sn, cofrees_fwd_bind_dx, conj/ qed-.
-
-lemma cofrees_inv_flat: ∀I,L,W,U,i,d. L ⊢ i ~ϵ 𝐅*[d]⦃ⓕ{I}W.U⦄ →
- L ⊢ i ~ϵ 𝐅*[d]⦃W⦄ ∧ L ⊢ i ~ϵ 𝐅*[d]⦃U⦄.
-/3 width=7 by cofrees_fwd_flat_sn, cofrees_fwd_flat_dx, conj/ qed-.
-
-(* Basic Properties *********************************************************)
-
-lemma cofrees_sort: ∀L,d,i,k. L ⊢ i ~ϵ 𝐅*[d]⦃⋆k⦄.
-#L #d #i #k #X #H >(cpys_inv_sort1 … H) -X /2 width=2 by ex_intro/
-qed.
-
-lemma cofrees_gref: ∀L,d,i,p. L ⊢ i ~ϵ 𝐅*[d]⦃§p⦄.
-#L #d #i #p #X #H >(cpys_inv_gref1 … H) -X /2 width=2 by ex_intro/
-qed.
-
-lemma cofrees_bind: ∀L,V,d,i. L ⊢ i ~ϵ 𝐅*[d] ⦃V⦄ →
- ∀I,T. L.ⓑ{I}V ⊢ i+1 ~ϵ 𝐅*[⫯d]⦃T⦄ →
- ∀a. L ⊢ i ~ϵ 𝐅*[d]⦃ⓑ{a,I}V.T⦄.
-#L #W1 #d #i #HW1 #I #U1 #HU1 #a #X #H elim (cpys_inv_bind1 … H) -H
-#W2 #U2 #HW12 #HU12 #H destruct
-elim (HW1 … HW12) elim (HU1 … HU12) -W1 -U1 /3 width=2 by lift_bind, ex_intro/
-qed.
-
-lemma cofrees_flat: ∀L,V,d,i. L ⊢ i ~ϵ 𝐅*[d]⦃V⦄ → ∀T. L ⊢ i ~ϵ 𝐅*[d]⦃T⦄ →
- ∀I. L ⊢ i ~ϵ 𝐅*[d]⦃ⓕ{I}V.T⦄.
-#L #W1 #d #i #HW1 #U1 #HU1 #I #X #H elim (cpys_inv_flat1 … H) -H
-#W2 #U2 #HW12 #HU12 #H destruct
-elim (HW1 … HW12) elim (HU1 … HU12) -W1 -U1 /3 width=2 by lift_flat, ex_intro/
-qed.
-
-lemma cofrees_cpy_trans: ∀L,U1,U2,d. ⦃⋆, L⦄ ⊢ U1 ▶[d, ∞] U2 →
- ∀i. L ⊢ i ~ϵ 𝐅*[d]⦃U1⦄ → L ⊢ i ~ϵ 𝐅*[d]⦃U2⦄.
-/3 width=3 by cpys_strap2/ qed-.
-
-axiom cofrees_dec: ∀L,T,d,i. Decidable (L ⊢ i ~ϵ 𝐅*[d]⦃T⦄).
-
-(* Basic negated properties *************************************************)
-
-lemma frees_cpy_div: ∀L,U1,U2,d. ⦃⋆, L⦄ ⊢ U1 ▶[d, ∞] U2 →
- ∀i. (L ⊢ i ~ϵ 𝐅*[d]⦃U2⦄ → ⊥) → (L ⊢ i ~ϵ 𝐅*[d]⦃U1⦄ → ⊥).
-/3 width=7 by cofrees_cpy_trans/ qed-.
-
-(* Basic negated inversion lemmas *******************************************)
-
-lemma frees_inv_bind: ∀a,I,L,V,T,d,i. (L ⊢ i ~ϵ 𝐅*[d]⦃ⓑ{a,I}V.T⦄ → ⊥) →
- (L ⊢ i ~ϵ 𝐅*[d]⦃V⦄ → ⊥) ∨ (L.ⓑ{I}V ⊢ i+1 ~ϵ 𝐅*[⫯d]⦃T⦄ → ⊥).
-#a #I #L #W #U #d #i #H elim (cofrees_dec L W d i)
-/4 width=9 by cofrees_bind, or_intror, or_introl/
-qed-.
-
-lemma frees_inv_flat: ∀I,L,V,T,d,i. (L ⊢ i ~ϵ 𝐅*[d]⦃ⓕ{I}V.T⦄ → ⊥) →
- (L ⊢ i ~ϵ 𝐅*[d]⦃V⦄ → ⊥) ∨ (L ⊢ i ~ϵ 𝐅*[d]⦃T⦄ → ⊥).
-#I #L #W #U #d #H elim (cofrees_dec L W d)
-/4 width=8 by cofrees_flat, 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/cpy_nlift.ma".
-include "basic_2/substitution/cofrees_lift.ma".
-
-(* CONTEXT-SENSITIVE EXCLUSION FROM FREE VARIABLES **************************)
-
-(* Alternative definition of frees_ge ***************************************)
-
-lemma nlift_frees: ∀L,U,d,i. (∀T. ⇧[i, 1] T ≡ U → ⊥) → (L ⊢ i ~ϵ 𝐅*[d]⦃U⦄ → ⊥).
-#L #U #d #i #HnTU #H elim (cofrees_fwd_lift … H) -H /2 width=2 by/
-qed-.
-
-lemma frees_inv_ge: ∀L,U,d,i. d ≤ yinj i → (L ⊢ i ~ϵ 𝐅*[d]⦃U⦄ → ⊥) →
- (∀T. ⇧[i, 1] T ≡ U → ⊥) ∨
- ∃∃I,K,W,j. d ≤ yinj j & j < i & ⇩[j]L ≡ K.ⓑ{I}W &
- (K ⊢ i-j-1 ~ϵ 𝐅*[yinj 0]⦃W⦄ → ⊥) & (∀T. ⇧[j, 1] T ≡ U → ⊥).
-#L #U #d #i #Hdi #H @(frees_ind … H) -U /3 width=2 by or_introl/
-#U1 #U2 #HU12 #HU2 *
-[ #HnU2 elim (cpy_fwd_nlift2_ge … HU12 … HnU2) -HU12 -HnU2 /3 width=2 by or_introl/
- * /5 width=9 by nlift_frees, ex5_4_intro, or_intror/
-| * #I2 #K2 #W2 #j2 #Hdj2 #Hj2i #HLK2 #HnW2 #HnU2 elim (cpy_fwd_nlift2_ge … HU12 … HnU2) -HU12 -HnU2 /4 width=9 by ex5_4_intro, or_intror/
- * #I1 #K1 #W1 #j1 #Hdj1 #Hj12 #HLK1 #HnW1 #HnU1
- lapply (ldrop_conf_ge … HLK1 … HLK2 ?) -HLK2 /2 width=1 by lt_to_le/
- #HK12 lapply (ldrop_inv_drop1_lt … HK12 ?) /2 width=1 by lt_plus_to_minus_r/ -HK12
- #HK12
- @or_intror @(ex5_4_intro … HLK1 … HnU1) -HLK1 -HnU1 /2 width=3 by transitive_lt/
- @(frees_be … HK12 … HnW1) /2 width=1 by arith_k_sn/ -HK12 -HnW1
- >minus_plus in ⊢ (??(?(?%?)?)??→?); >minus_plus in ⊢ (??(?(??%)?)??→?); >arith_b1 /2 width=1 by/
-]
-qed-.
-
-lemma frees_ind_ge: ∀R:relation4 ynat nat lenv term.
- (∀d,i,L,U. d ≤ yinj i → (∀T. ⇧[i, 1] T ≡ U → ⊥) → R d i L U) →
- (∀d,i,j,I,L,K,W,U. d ≤ yinj j → j < i → ⇩[j]L ≡ K.ⓑ{I}W → (K ⊢ i-j-1 ~ϵ 𝐅*[0]⦃W⦄ → ⊥) → (∀T. ⇧[j, 1] T ≡ U → ⊥) → R 0 (i-j-1) K W → R d i L U) →
- ∀d,i,L,U. d ≤ yinj i → (L ⊢ i ~ϵ 𝐅*[d]⦃U⦄ → ⊥) → R d i L U.
-#R #IH1 #IH2 #d #i #L #U
-generalize in match d; -d generalize in match i; -i
-@(f2_ind … rfw … L U) -L -U
-#n #IHn #L #U #Hn #i #d #Hdi #H elim (frees_inv_ge … H) -H /3 width=2 by/
--IH1 * #I #K #W #j #Hdj #Hji #HLK #HnW #HnU destruct /4 width=12 by ldrop_fwd_rfw/
-qed-.
+++ /dev/null
-(**************************************************************************)
-(* ___ *)
-(* ||M|| *)
-(* ||A|| A project by Andrea Asperti *)
-(* ||T|| *)
-(* ||I|| Developers: *)
-(* ||T|| The HELM team. *)
-(* ||A|| http://helm.cs.unibo.it *)
-(* \ / *)
-(* \ / This file is distributed under the terms of the *)
-(* v GNU General Public License Version 2 *)
-(* *)
-(**************************************************************************)
-
-include "basic_2/substitution/cpys_lift.ma".
-include "basic_2/substitution/cofrees.ma".
-
-(* CONTEXT-SENSITIVE EXCLUSION FROM FREE VARIABLES **************************)
-
-(* Advanced inversion lemmas ************************************************)
-
-lemma cofrees_inv_lref_be: ∀L,d,i,j. L ⊢ i ~ϵ 𝐅*[d]⦃#j⦄ → d ≤ yinj j → j < i →
- ∀I,K,W. ⇩[j]L ≡ K.ⓑ{I}W → K ⊢ i-j-1 ~ϵ 𝐅*[yinj 0]⦃W⦄.
-#L #d #i #j #Hj #Hdj #Hji #I #K #W1 #HLK #W2 #HW12 elim (lift_total W2 0 (j+1))
-#X2 #HWX2 elim (Hj X2) /2 width=7 by cpys_subst_Y2/ -I -L -K -W1 -d
-#Z2 #HZX2 elim (lift_div_le … HWX2 (i-j-1) 1 Z2) -HWX2 /2 width=2 by ex_intro/
->minus_plus <plus_minus_m_m //
-qed-.
-
-lemma cofrees_inv_be: ∀L,U,d,i. L ⊢ i ~ϵ 𝐅*[d]⦃U⦄ → ∀j. (∀T. ⇧[j, 1] T ≡ U → ⊥) →
- ∀I,K,W. ⇩[j]L ≡ K.ⓑ{I}W → d ≤ yinj j → j < i → K ⊢ i-j-1 ~ϵ 𝐅*[yinj 0]⦃W⦄.
-#L #U @(f2_ind … rfw … L U) -L -U
-#n #IH #L * *
-[ -IH #k #_ #d #i #_ #j #H elim (H (⋆k)) -H //
-| -IH #j #_ #d #i #Hi0 #j0 #H <(nlift_inv_lref_be_SO … H) -j0
- /2 width=9 by cofrees_inv_lref_be/
-| -IH #p #_ #d #i #_ #j #H elim (H (§p)) -H //
-| #a #J #W #U #Hn #d #i #H1 #j #H2 #I #K #V #HLK #Hdj #Hji destruct
- elim (cofrees_inv_bind … H1) -H1 #HW #HU
- elim (nlift_inv_bind … H2) -H2 [ -HU /3 width=9 by/ ]
- -HW #HnU lapply (IH … HU … HnU I K V ? ? ?)
- /2 width=1 by ldrop_drop, yle_succ, lt_minus_to_plus/ -a -I -J -L -W -U -d
- >minus_plus_plus_l //
-| #J #W #U #Hn #d #i #H1 #j #H2 #I #K #V #HLK #Hdj #Hji destruct
- elim (cofrees_inv_flat … H1) -H1 #HW #HU
- elim (nlift_inv_flat … H2) -H2 [ /3 width=9 by/ ]
- #HnU @(IH … HU … HnU … HLK) // (**) (* full auto fails *)
-]
-qed-.
-
-(* Advanced properties ******************************************************)
-
-lemma cofrees_lref_skip: ∀L,d,i,j. j < i → yinj j < d → L ⊢ i ~ϵ 𝐅*[d]⦃#j⦄.
-#L #d #i #j #Hji #Hjd #X #H elim (cpys_inv_lref1_Y2 … H) -H
-[ #H destruct /3 width=2 by lift_lref_lt, ex_intro/
-| * #I #K #W1 #W2 #Hdj elim (ylt_yle_false … Hdj) -i -I -L -K -W1 -W2 -X //
-]
-qed.
-
-lemma cofrees_lref_lt: ∀L,d,i,j. i < j → L ⊢ i ~ϵ 𝐅*[d]⦃#j⦄.
-#L #d #i #j #Hij #X #H elim (cpys_inv_lref1_Y2 … H) -H
-[ #H destruct /3 width=2 by lift_lref_ge_minus, ex_intro/
-| * #I #K #V1 #V2 #_ #_ #_ #H -I -L -K -V1 -d
- elim (lift_split … H i j) /2 width=2 by lt_to_le, ex_intro/
-]
-qed.
-
-lemma cofrees_lref_gt: ∀I,L,K,W,d,i,j. j < i → ⇩[j] L ≡ K.ⓑ{I}W →
- K ⊢ (i-j-1) ~ϵ 𝐅*[O]⦃W⦄ → L ⊢ i ~ϵ 𝐅*[d]⦃#j⦄.
-#I #L #K #W1 #d #i #j #Hji #HLK #HW1 #X #H elim (cpys_inv_lref1_Y2 … H) -H
-[ #H destruct /3 width=2 by lift_lref_lt, ex_intro/
-| * #I0 #K0 #W0 #W2 #Hdj #HLK0 #HW12 #HW2 lapply (ldrop_mono … HLK0 … HLK) -L
- #H destruct elim (HW1 … HW12) -I -K -W1 -d
- #V2 #HVW2 elim (lift_trans_le … HVW2 … HW2) -W2 //
- >minus_plus <plus_minus_m_m /2 width=2 by ex_intro/
-]
-qed.
-
-lemma cofrees_lref_free: ∀L,d,i,j. |L| ≤ j → j < i → L ⊢ i ~ϵ 𝐅*[d]⦃#j⦄.
-#L #d #i #j #Hj #Hji #X #H elim (cpys_inv_lref1_Y2 … H) -H
-[ #H destruct /3 width=2 by lift_lref_lt, ex_intro/
-| * #I #K #W1 #W2 #_ #HLK lapply (ldrop_fwd_length_lt2 … HLK) -I
- #H elim (lt_refl_false j) -d -i -K -W1 -W2 -X /2 width=3 by lt_to_le_to_lt/
-]
-qed.
-
-(* Advanced negated inversion lemmas ****************************************)
-
-lemma frees_inv_lref_gt: ∀L,d,i,j. j < i → (L ⊢ i ~ϵ 𝐅*[d]⦃#j⦄ → ⊥) →
- ∃∃I,K,W. ⇩[j] L ≡ K.ⓑ{I}W & (K ⊢ (i-j-1) ~ϵ 𝐅*[0]⦃W⦄ → ⊥) & d ≤ yinj j.
-#L #d #i #j #Hji #H elim (ylt_split j d) #Hjd
-[ elim H -H /2 width=6 by cofrees_lref_skip/
-| elim (lt_or_ge j (|L|)) #Hj
- [ elim (ldrop_O1_lt … Hj) -Hj /4 width=10 by cofrees_lref_gt, ex3_3_intro/
- | elim H -H /2 width=6 by cofrees_lref_free/
- ]
-]
-qed-.
-
-lemma frees_inv_lref_free: ∀L,d,i,j. (L ⊢ i ~ϵ 𝐅*[d]⦃#j⦄ → ⊥) → |L| ≤ j → j = i.
-#L #d #i #j #H #Hj elim (lt_or_eq_or_gt i j) //
-#Hij elim H -H /2 width=6 by cofrees_lref_lt, cofrees_lref_free/
-qed-.
-
-lemma frees_inv_gen: ∀L,U,d,i. (L ⊢ i ~ϵ 𝐅*[d]⦃U⦄ → ⊥) →
- ∃∃U0. ⦃⋆, L⦄ ⊢ U ▶*[d, ∞] U0 & (∀T. ⇧[i, 1] T ≡ U0 → ⊥).
-#L #U @(f2_ind … rfw … L U) -L -U
-#n #IH #L * *
-[ -IH #k #_ #d #i #H elim H -H //
-| #j #Hn #d #i #H elim (lt_or_eq_or_gt i j)
- [ -n #Hij elim H -H /2 width=5 by cofrees_lref_lt/
- | -H -n #H destruct /3 width=7 by lift_inv_lref2_be, ex2_intro/
- | #Hji elim (frees_inv_lref_gt … H) // -H
- #I #K #W1 #HLK #H #Hdj elim (IH … H) /2 width=3 by ldrop_fwd_rfw/ -H -n
- #W2 #HW12 #HnW2 elim (lift_total W2 0 (j+1))
- #U2 #HWU2 @(ex2_intro … U2) /2 width=7 by cpys_subst_Y2/ -I -L -K -W1 -d
- #T2 #HTU2 elim (lift_div_le … HWU2 (i-j-1) 1 T2) /2 width=2 by/ -W2
- >minus_plus <plus_minus_m_m //
- ]
-| -IH #p #_ #d #i #H elim H -H //
-| #a #I #W #U #Hn #d #i #H elim (frees_inv_bind … H) -H
- #H elim (IH … H) // -H -n
- /4 width=9 by cpys_bind, nlift_bind_dx, nlift_bind_sn, ex2_intro/
-| #I #W #U #Hn #d #i #H elim (frees_inv_flat … H) -H
- #H elim (IH … H) // -H -n
- /4 width=9 by cpys_flat, nlift_flat_dx, nlift_flat_sn, ex2_intro/
-]
-qed-.
-
-lemma frees_ind: ∀L,d,i. ∀R:predicate term.
- (∀U1. (∀T1. ⇧[i, 1] T1 ≡ U1 → ⊥) → R U1) →
- (∀U1,U2. ⦃⋆, L⦄ ⊢ U1 ▶[d, ∞] U2 → (L ⊢ i ~ϵ 𝐅*[d]⦃U2⦄ → ⊥) → R U2 → R U1) →
- ∀U. (L ⊢ i ~ϵ 𝐅*[d]⦃U⦄ → ⊥) → R U.
-#L #d #i #R #IH1 #IH2 #U1 #H elim (frees_inv_gen … H) -H
-#U2 #H #HnU2 @(cpys_ind_dx … H) -U1 /4 width=8 by cofrees_inv_gen/
-qed-.
-
-(* Advanced negated properties **********************************************)
-
-lemma frees_be: ∀I,L,K,W,j. ⇩[j]L ≡ K.ⓑ{I}W →
- ∀i. j < i → (K ⊢ i-j-1 ~ϵ 𝐅*[yinj 0]⦃W⦄ → ⊥) →
- ∀U. (∀T. ⇧[j, 1] T ≡ U → ⊥) →
- ∀d. d ≤ yinj j → (L ⊢ i ~ϵ 𝐅*[d]⦃U⦄ → ⊥).
-/4 width=11 by cofrees_inv_be/ qed-.
--- /dev/null
+(**************************************************************************)
+(* ___ *)
+(* ||M|| *)
+(* ||A|| A project by Andrea Asperti *)
+(* ||T|| *)
+(* ||I|| Developers: *)
+(* ||T|| The HELM team. *)
+(* ||A|| http://helm.cs.unibo.it *)
+(* \ / *)
+(* \ / This file is distributed under the terms of the *)
+(* v GNU General Public License Version 2 *)
+(* *)
+(**************************************************************************)
+
+include "ground_2/ynat/ynat_plus.ma".
+include "basic_2/notation/relations/freestar_4.ma".
+include "basic_2/relocation/lift_neg.ma".
+include "basic_2/relocation/ldrop.ma".
+
+(* CONTEXT-SENSITIVE FREE VARIABLES *****************************************)
+
+inductive frees: relation4 ynat lenv term nat ≝
+| frees_eq: ∀L,U,d,i. (∀T. ⇧[i, 1] T ≡ U → ⊥) → frees d L U i
+| frees_be: ∀I,L,K,U,W,d,i,j. d ≤ yinj j → j < i →
+ (∀T. ⇧[j, 1] T ≡ U → ⊥) → ⇩[j]L ≡ K.ⓑ{I}W →
+ frees 0 K W (i-j-1) → frees d L U i.
+
+interpretation
+ "context-sensitive free variables (term)"
+ 'FreeStar L i d U = (frees d L U i).
+
+(* Basic inversion lemmas ***************************************************)
+
+lemma frees_inv: ∀L,U,d,i. L ⊢ i ϵ 𝐅*[d]⦃U⦄ →
+ (∀T. ⇧[i, 1] T ≡ U → ⊥) ∨
+ ∃∃I,K,W,j. d ≤ yinj j & j < i & (∀T. ⇧[j, 1] T ≡ U → ⊥) &
+ ⇩[j]L ≡ K.ⓑ{I}W & K ⊢ (i-j-1) ϵ 𝐅*[yinj 0]⦃W⦄.
+#L #U #d #i * -L -U -d -i /4 width=9 by ex5_4_intro, or_intror, or_introl/
+qed-.
+
+lemma frees_inv_sort: ∀L,d,i,k. L ⊢ i ϵ 𝐅*[d]⦃⋆k⦄ → ⊥.
+#L #d #i #k #H elim (frees_inv … H) -H [|*] /2 width=2 by/
+qed-.
+
+lemma frees_inv_gref: ∀L,d,i,p. L ⊢ i ϵ 𝐅*[d]⦃§p⦄ → ⊥.
+#L #d #i #p #H elim (frees_inv … H) -H [|*] /2 width=2 by/
+qed-.
+
+lemma frees_inv_lref: ∀L,d,j,i. L ⊢ i ϵ 𝐅*[d]⦃#j⦄ →
+ j = i ∨
+ ∃∃I,K,W. d ≤ yinj j & j < i & ⇩[j] L ≡ K.ⓑ{I}W & K ⊢ (i-j-1) ϵ 𝐅*[yinj 0]⦃W⦄.
+#L #d #x #i #H elim (frees_inv … H) -H
+[ /4 width=2 by nlift_inv_lref_be_SO, or_introl/
+| * #I #K #W #j #Hdj #Hji #Hnx #HLK #HW
+ >(nlift_inv_lref_be_SO … Hnx) -x /3 width=5 by ex4_3_intro, or_intror/
+]
+qed-.
+
+lemma frees_inv_lref_free: ∀L,d,j,i. L ⊢ i ϵ 𝐅*[d]⦃#j⦄ → |L| ≤ j → j = i.
+#L #d #j #i #H #Hj elim (frees_inv_lref … H) -H //
+* #I #K #W #_ #_ #HLK lapply (ldrop_fwd_length_lt2 … HLK) -I
+#H elim (lt_refl_false j) /2 width=3 by lt_to_le_to_lt/
+qed-.
+
+lemma frees_inv_lref_skip: ∀L,d,j,i. L ⊢ i ϵ 𝐅*[d]⦃#j⦄ → yinj j < d → j = i.
+#L #d #j #i #H #Hjd elim (frees_inv_lref … H) -H //
+* #I #K #W #Hdj elim (ylt_yle_false … Hdj) -Hdj //
+qed-.
+
+lemma frees_inv_lref_ge: ∀L,d,j,i. L ⊢ i ϵ 𝐅*[d]⦃#j⦄ → i ≤ j → j = i.
+#L #d #j #i #H #Hij elim (frees_inv_lref … H) -H //
+* #I #K #W #_ #Hji elim (lt_refl_false j) -I -L -K -W -d /2 width=3 by lt_to_le_to_lt/
+qed-.
+
+lemma frees_inv_lref_lt: ∀L,d,j,i.L ⊢ i ϵ 𝐅*[d]⦃#j⦄ → j < i →
+ ∃∃I,K,W. d ≤ yinj j & ⇩[j] L ≡ K.ⓑ{I}W & K ⊢ (i-j-1) ϵ 𝐅*[yinj 0]⦃W⦄.
+#L #d #j #i #H #Hji elim (frees_inv_lref … H) -H
+[ #H elim (lt_refl_false j) //
+| * /2 width=5 by ex3_3_intro/
+]
+qed-.
+
+lemma frees_inv_bind: ∀a,I,L,W,U,d,i. L ⊢ i ϵ 𝐅*[d]⦃ⓑ{a,I}W.U⦄ →
+ L ⊢ i ϵ 𝐅*[d]⦃W⦄ ∨ L.ⓑ{I}W ⊢ i+1 ϵ 𝐅*[⫯d]⦃U⦄ .
+#a #J #L #V #U #d #i #H elim (frees_inv … H) -H
+[ #HnX elim (nlift_inv_bind … HnX) -HnX
+ /4 width=2 by frees_eq, or_intror, or_introl/
+| * #I #K #W #j #Hdj #Hji #HnX #HLK #HW elim (nlift_inv_bind … HnX) -HnX
+ [ /4 width=9 by frees_be, or_introl/
+ | #HnT @or_intror @(frees_be … HnT) -HnT
+ [4,5,6: /2 width=1 by ldrop_drop, yle_succ, lt_minus_to_plus/
+ |7: >minus_plus_plus_l //
+ |*: skip
+ ]
+ ]
+]
+qed-.
+
+lemma frees_inv_flat: ∀I,L,W,U,d,i. L ⊢ i ϵ 𝐅*[d]⦃ⓕ{I}W.U⦄ →
+ L ⊢ i ϵ 𝐅*[d]⦃W⦄ ∨ L ⊢ i ϵ 𝐅*[d]⦃U⦄ .
+#J #L #V #U #d #i #H elim (frees_inv … H) -H
+[ #HnX elim (nlift_inv_flat … HnX) -HnX
+ /4 width=2 by frees_eq, or_intror, or_introl/
+| * #I #K #W #j #Hdj #Hji #HnX #HLK #HW elim (nlift_inv_flat … HnX) -HnX
+ /4 width=9 by frees_be, or_intror, or_introl/
+]
+qed-.
+
+(* Basic properties *********************************************************)
+
+lemma frees_lref_eq: ∀L,d,i. L ⊢ i ϵ 𝐅*[d]⦃#i⦄.
+/3 width=7 by frees_eq, lift_inv_lref2_be/ qed.
+
+lemma frees_lref_be: ∀I,L,K,W,d,i,j. d ≤ yinj j → j < i → ⇩[j]L ≡ K.ⓑ{I}W →
+ K ⊢ i-j-1 ϵ 𝐅*[0]⦃W⦄ → L ⊢ i ϵ 𝐅*[d]⦃#j⦄.
+/3 width=9 by frees_be, lift_inv_lref2_be/ qed.
+
+lemma frees_bind_sn: ∀a,I,L,W,U,d,i. L ⊢ i ϵ 𝐅*[d]⦃W⦄ →
+ L ⊢ i ϵ 𝐅*[d]⦃ⓑ{a,I}W.U⦄.
+#a #I #L #W #U #d #i #H elim (frees_inv … H) -H [|*]
+/4 width=9 by frees_be, frees_eq, nlift_bind_sn/
+qed.
+
+lemma frees_bind_dx: ∀a,I,L,W,U,d,i. L.ⓑ{I}W ⊢ i+1 ϵ 𝐅*[⫯d]⦃U⦄ →
+ L ⊢ i ϵ 𝐅*[d]⦃ⓑ{a,I}W.U⦄.
+#a #J #L #V #U #d #i #H elim (frees_inv … H) -H
+[ /4 width=9 by frees_eq, nlift_bind_dx/
+| * #I #K #W #j #Hdj #Hji #HnU #HLK #HW
+ elim (yle_inv_succ1 … Hdj) -Hdj <yminus_SO2 #Hyj #H
+ lapply (ylt_O … H) -H #Hj
+ >(plus_minus_m_m j 1) in HnU; // <minus_le_minus_minus_comm in HW;
+ /4 width=9 by frees_be, nlift_bind_dx, ldrop_inv_drop1_lt, lt_plus_to_minus/
+]
+qed.
+
+lemma frees_flat_sn: ∀I,L,W,U,d,i. L ⊢ i ϵ 𝐅*[d]⦃W⦄ →
+ L ⊢ i ϵ 𝐅*[d]⦃ⓕ{I}W.U⦄.
+#I #L #W #U #d #i #H elim (frees_inv … H) -H [|*]
+/4 width=9 by frees_be, frees_eq, nlift_flat_sn/
+qed.
+
+lemma frees_flat_dx: ∀I,L,W,U,d,i. L ⊢ i ϵ 𝐅*[d]⦃U⦄ →
+ L ⊢ i ϵ 𝐅*[d]⦃ⓕ{I}W.U⦄.
+#I #L #W #U #d #i #H elim (frees_inv … H) -H [|*]
+/4 width=9 by frees_be, frees_eq, nlift_flat_dx/
+qed.
+
+lemma frees_weak: ∀L,U,d1,i. L ⊢ i ϵ 𝐅*[d1]⦃U⦄ →
+ ∀d2. d2 ≤ d1 → L ⊢ i ϵ 𝐅*[d2]⦃U⦄.
+#L #U #d1 #i #H elim H -L -U -d1 -i
+/3 width=9 by frees_be, frees_eq, yle_trans/
+qed-.
+
+(* Advanced inversion lemmas ************************************************)
+
+lemma frees_inv_bind_O: ∀a,I,L,W,U,i. L ⊢ i ϵ 𝐅*[0]⦃ⓑ{a,I}W.U⦄ →
+ L ⊢ i ϵ 𝐅*[0]⦃W⦄ ∨ L.ⓑ{I}W ⊢ i+1 ϵ 𝐅*[0]⦃U⦄ .
+#a #I #L #W #U #i #H elim (frees_inv_bind … H) -H
+/3 width=3 by frees_weak, 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/ldrop_ldrop.ma".
+include "basic_2/substitution/frees.ma".
+
+(* CONTEXT-SENSITIVE FREE VARIABLES *****************************************)
+
+(* Advanced properties ******************************************************)
+
+lemma frees_dec: ∀L,U,d,i. Decidable (frees d L U i).
+#L #U @(f2_ind … rfw … L U) -L -U
+#n #IH #L * *
+[ -IH /3 width=5 by frees_inv_sort, or_intror/
+| #j #Hn #d #i elim (lt_or_eq_or_gt i j) #Hji
+ [ -n @or_intror #H elim (lt_refl_false i)
+ lapply (frees_inv_lref_ge … H ?) -L -d /2 width=1 by lt_to_le/
+ | -n /2 width=1 by or_introl/
+ | elim (ylt_split j d) #Hdi
+ [ -n @or_intror #H elim (lt_refl_false i)
+ lapply (frees_inv_lref_skip … H ?) -L //
+ | elim (lt_or_ge j (|L|)) #Hj
+ [ elim (ldrop_O1_lt (Ⓕ) L j) // -Hj #I #K #W #HLK destruct
+ elim (IH K W … 0 (i-j-1)) -IH [1,3: /3 width=5 by frees_lref_be, ldrop_fwd_rfw, or_introl/ ] #HnW
+ @or_intror #H elim (frees_inv_lref_lt … H) // #Z #Y #X #_ #HLY -d
+ lapply (ldrop_mono … HLY … HLK) -L #H destruct /2 width=1 by/
+ | -n @or_intror #H elim (lt_refl_false i)
+ lapply (frees_inv_lref_free … H ?) -d //
+ ]
+ ]
+ ]
+| -IH /3 width=5 by frees_inv_gref, or_intror/
+| #a #I #W #U #Hn #d #i destruct
+ elim (IH L W … d i) [1,3: /3 width=1 by frees_bind_sn, or_introl/ ] #HnW
+ elim (IH (L.ⓑ{I}W) U … (⫯d) (i+1)) -IH [1,3: /3 width=1 by frees_bind_dx, or_introl/ ] #HnU
+ @or_intror #H elim (frees_inv_bind … H) -H /2 width=1 by/
+| #I #W #U #Hn #d #i destruct
+ elim (IH L W … d i) [1,3: /3 width=1 by frees_flat_sn, or_introl/ ] #HnW
+ elim (IH L U … d i) -IH [1,3: /3 width=1 by frees_flat_dx, or_introl/ ] #HnU
+ @or_intror #H elim (frees_inv_flat … H) -H /2 width=1 by/
+]
+qed-.
+
+lemma frees_S: ∀L,U,d,i. L ⊢ i ϵ 𝐅*[yinj d]⦃U⦄ → ∀I,K,W. ⇩[d] L ≡ K.ⓑ{I}W →
+ (K ⊢ i-d-1 ϵ 𝐅*[0]⦃W⦄ → ⊥) → L ⊢ i ϵ 𝐅*[⫯d]⦃U⦄.
+#L #U #d #i #H elim (frees_inv … H) -H /3 width=2 by frees_eq/
+* #I #K #W #j #Hdj #Hji #HnU #HLK #HW #I0 #K0 #W0 #HLK0 #HnW0
+lapply (yle_inv_inj … Hdj) -Hdj #Hdj
+elim (le_to_or_lt_eq … Hdj) -Hdj
+[ -I0 -K0 -W0 /3 width=9 by frees_be, yle_inj/
+| -Hji -HnU #H destruct
+ lapply (ldrop_mono … HLK0 … HLK) #H destruct -I
+ elim HnW0 -L -U -HnW0 //
+]
+qed.
+
+(* Note: lemma 1250 *)
+lemma frees_bind_dx_O: ∀a,I,L,W,U,i. L.ⓑ{I}W ⊢ i+1 ϵ 𝐅*[0]⦃U⦄ →
+ L ⊢ i ϵ 𝐅*[0]⦃ⓑ{a,I}W.U⦄.
+#a #I #L #W #U #i #HU elim (frees_dec L W 0 i)
+/4 width=5 by frees_S, frees_bind_dx, frees_bind_sn/
+qed.
(* Alternative definition (not recursive) ***********************************)
theorem lleq_intro_alt: ∀L1,L2,T,d. |L1| = |L2| →
- (∀I1,I2,K1,K2,V1,V2,i. d ≤ yinj i → (L1 ⊢ i ~ϵ 𝐅*[d]⦃T⦄ → ⊥) →
+ (∀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 ∧ V1 = V2
) → L1 ≡[T, d] L2.
theorem lleq_inv_alt: ∀L1,L2,T,d. L1 ≡[T, d] L2 →
|L1| = |L2| ∧
- ∀I1,I2,K1,K2,V1,V2,i. d ≤ yinj i → (L1 ⊢ i ~ϵ 𝐅*[d]⦃T⦄ → ⊥) →
+ ∀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 ∧ V1 = V2.
#L1 #L2 #T #d #H elim (llpx_sn_llpx_sn_alt … H) -H
(* LAZY EQUIVALENCE FOR LOCAL ENVIRONMENTS **********************************)
(* Properties on poinwise union for local environments **********************)
-(*
-lemma llor_lleq_O: ∀R,L1,L2,T. llpx_sn R 0 T L1 L2 →
- ∀L. L1 ⩖[T] L2 ≡ L → L2 ≡[T, 0] L.
-#R #L1 #L2 #T #H1 #L #H2
+
+lemma llpx_sn_llor_dx: ∀R,L1,L2.
+ (∀U,i. L2 ⊢ i ϵ 𝐅*[0]⦃U⦄ → L1 ⊢ i ϵ 𝐅*[0]⦃U⦄) →
+ ∀T. llpx_sn R 0 T L1 L2 → ∀L. L1 ⩖[T] L2 ≡ L → L2 ≡[T, 0] L.
+#R #L1 #L2 #HR #T #H1 #L #H2
elim (llpx_sn_llpx_sn_alt … H1) -H1 #HL12 #IH1
elim H2 -H2 #_ #HL1 #IH2
@lleq_intro_alt // #I2 #I #K2 #K #V2 #V #i #Hi #HnT #HLK2 #HLK
lapply (ldrop_fwd_length_lt2 … HLK) #HiL
elim (ldrop_O1_lt (Ⓕ) L1 i) // -HiL #I1 #K1 #V1 #HLK1
-elim (IH1 … HLK1 HLK2) // -IH1
-[ #H #_ destruct
- elim (IH2 … HLK1 HLK2 HLK) * /2 width=1 by conj/
- #H elim HnT -HnT
-| #H @HnT -HnT
-]
-*)
+elim (IH1 … HLK1 HLK2) -IH1 /2 width=1 by/ #H #_ destruct
+elim (IH2 … HLK1 HLK2 HLK) -IH2 -HLK1 -HLK2 -HLK * /2 width=1 by conj/ #H
+elim H -H /2 width=1 by/
+qed.
(**************************************************************************)
include "basic_2/notation/relations/lazyor_4.ma".
-include "basic_2/substitution/cofrees.ma".
+include "basic_2/substitution/frees.ma".
(* POINTWISE UNION FOR LOCAL ENVIRONMENTS ***********************************)
∧∧ |L1| ≤ |L2| & |L1| = |L|
& (∀I1,I2,I,K1,K2,K,V1,V2,V,i.
⇩[i] L1 ≡ K1.ⓑ{I1}V1 → ⇩[i] L2 ≡ K2.ⓑ{I2}V2 → ⇩[i] L ≡ K.ⓑ{I}V →
- (∧∧ L1 ⊢ i ~ϵ 𝐅*[yinj 0]⦃T⦄ & I1 = I & V1 = V) ∨
- (∧∧ (L1 ⊢ i ~ϵ 𝐅*[yinj 0]⦃T⦄ → ⊥) & I1 = I & V2 = V)
+ (∧∧ (L1 ⊢ i ϵ 𝐅*[yinj 0]⦃T⦄ → ⊥) & I1 = I & V1 = V) ∨
+ (∧∧ L1 ⊢ i ϵ 𝐅*[yinj 0]⦃T⦄ & I1 = I & V2 = V)
).
interpretation
#I1 #I2 #I #K1 #K2 #K #V1 #V2 #V #i #HLK1
elim (ldrop_inv_atom1 … HLK1) -HLK1 #H destruct
qed.
-
-axiom llor_total: ∀L1,L2,T. |L1| ≤ |L2| → ∃L. L1 ⩖[T] L2 ≡ L.
--- /dev/null
+(**************************************************************************)
+(* ___ *)
+(* ||M|| *)
+(* ||A|| A project by Andrea Asperti *)
+(* ||T|| *)
+(* ||I|| Developers: *)
+(* ||T|| The HELM team. *)
+(* ||A|| http://helm.cs.unibo.it *)
+(* \ / *)
+(* \ / This file is distributed under the terms of the *)
+(* v GNU General Public License Version 2 *)
+(* *)
+(**************************************************************************)
+
+include "basic_2/substitution/frees_lift.ma".
+include "basic_2/substitution/llor.ma".
+
+(* POINTWISE UNION FOR LOCAL ENVIRONMENTS ***********************************)
+
+(* Advanced properties ******************************************************)
+
+axiom llor_total: ∀L1,L2,T. |L1| ≤ |L2| → ∃L. L1 ⩖[T] L2 ≡ L.
(* *)
(**************************************************************************)
-include "basic_2/substitution/cofrees_alt.ma".
+include "basic_2/substitution/frees.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: 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⦄ → ⊥) →
+ (∀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 K1 V1 V2
).
#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 //
+#I1 #I2 #K1 #K2 #V1 #V2 #i #Hdi #H #HLK1 #HLK2 elim (frees_inv … 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
+| * #J1 #K10 #W10 #j #Hdj #Hji #HnU #HLK10 #HnW10 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
#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/
+elim (IHU … HLK1 HLK2) /3 width=2 by frees_eq/
#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
}
]
[ { "context-sensitive extended reduction" * } {
- [ "lpx ( ⦃?,?⦄ ⊢ ➡[?,?] ? )" "lpx_ldrop" + "lpx_lleq" + "lpx_aaa" * ]
+ [ "lpx ( ⦃?,?⦄ ⊢ ➡[?,?] ? )" "lpx_ldrop" + "lpx_frees" "lpx_lleq" + "lpx_aaa" * ]
[ "cpx ( ⦃?,?⦄ ⊢ ? ➡[?,?] ? )" "cpx_leq" + "cpx_lift" + "cpx_llpx_sn" + "cpx_lleq" + "cpx_cix" * ]
}
]
}
]
[ { "pointwise union for local environments" * } {
- [ "llor ( ? ⩖[?] ? ≡ ? )" * ]
+ [ "llor ( ? ⩖[?] ? ≡ ? )" "llor_ldrop" * ]
}
]
[ { "context-sensitive exclusion from free variables" * } {
- [ "cofrees ( ? ⊢ ? ~ϵ 𝐅*[?]⦃?⦄ )" "cofrees_alt" + "cofrees_lift" * ]
+ [ "frees ( ? ⊢ ? ϵ 𝐅*[?]⦃?⦄ )" "frees_lift" * ]
}
]
[ { "contxt-sensitive extended multiple substitution" * } {
projects / helm.git / commitdiff