From: Ferruccio Guidi Date: Fri, 23 May 2014 17:30:04 +0000 (+0000) Subject: advances on cofrees allows to prove one direction of X-Git-Tag: make_still_working~922 X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=commitdiff_plain;h=8365510a374c2983c9546296b2337beaaa2866fa;p=helm.git advances on cofrees allows to prove one direction of non-recursive characterization of llpx_sn (finally!) --- diff --git a/matita/matita/contribs/lambdadelta/basic_2/etc/llpx_sn_alt2.etc b/matita/matita/contribs/lambdadelta/basic_2/etc/llpx_sn_alt2.etc deleted file mode 100644 index 5a87c0da3..000000000 --- a/matita/matita/contribs/lambdadelta/basic_2/etc/llpx_sn_alt2.etc +++ /dev/null @@ -1,192 +0,0 @@ -(**************************************************************************) -(* ___ *) -(* ||M|| *) -(* ||A|| A project by Andrea Asperti *) -(* ||T|| *) -(* ||I|| Developers: *) -(* ||T|| The HELM team. *) -(* ||A|| http://helm.cs.unibo.it *) -(* \ / *) -(* \ / This file is distributed under the terms of the *) -(* v GNU General Public License Version 2 *) -(* *) -(**************************************************************************) - -include "basic_2/substitution/cofrees_lift.ma". -include "basic_2/substitution/llpx_sn_alt1.ma". - -(* LAZY SN POINTWISE EXTENSION OF A CONTEXT-SENSITIVE REALTION FOR TERMS ****) - -(* alternative definition of llpx_sn (not recursive) *) -definition llpx_sn_alt2: relation4 bind2 lenv term term → relation4 ynat term lenv lenv ≝ - λR,d,T,L1,L2. |L1| = |L2| ∧ - (∀I1,I2,K1,K2,V1,V2,i. d ≤ yinj i → (L1 ⊢ i ~ϵ 𝐅*[d]⦃T⦄ → ⊥) → - ⇩[i] L1 ≡ K1.ⓑ{I1}V1 → ⇩[i] L2 ≡ K2.ⓑ{I2}V2 → - I1 = I2 ∧ R I1 K1 V1 V2 - ). - -(* Main properties **********************************************************) - -lemma cpy_inv_nlift2_be: ∀G,L,U1,U2,d. ⦃G, L⦄ ⊢ U1 ▶[d, ∞] U2 → ∀i. d ≤ yinj i → - ∀K,s. ⇩[s, i, 1] L ≡ K → - (∀T2. ⇧[i, 1] T2 ≡ U2 → ⊥) → (∀T1. ⇧[i, 1] T1 ≡ U1 → ⊥). -#G #L #U1 #U2 #d #HU12 #i #Hdi #K #s #HLK #HnU2 #T1 #HTU1 -elim (cpy_inv_lift1_be … HU12 … HLK … HTU1) /2 width=2 by/ -qed-. - -lemma cpy_inv_nlift2_ge: ∀G,L,U1,U2,d,e. ⦃G, L⦄ ⊢ U1 ▶[d, e] U2 → - ∀i. d ≤ yinj i → (* yinj i + yinj 1 ≤ d + e → *) - (∀T2. ⇧[i, 1] T2 ≡ U2 → ⊥) → - ∃∃j. d ≤ yinj j & j ≤ i & (∀T1. ⇧[j, 1] T1 ≡ U1 → ⊥). -#G #L #U1 #U2 #d #e #H elim H -G -L -U1 -U2 -d -e -[ #I #G #L #d #e #i #Hdi (* #Hide *) #H @(ex3_intro … i) /2 width=2 by/ -| #I #G #L #K #V #W #j #d #e #Hdj #Hjde #HLK #HVW #i #Hdi (* #Hide *) #HnW - elim (le_or_ge i j) #Hij [2: @(ex3_intro … j) /2 width=7 by lift_inv_lref2_be/ ] - elim (lift_split … HVW i j) -HVW // - #X #_ #H elim HnW -HnW // -| #a #I #G #L #W1 #W2 #U1 #U2 #d #e #_ #_ #IHW12 #IHU12 #i #Hdi #H elim (nlift_inv_bind … H) -H - [ #HnW2 elim (IHW12 … HnW2) -IHW12 -HnW2 -IHU12 // - #j #Hdj #Hji #HnW1 @(ex3_intro … j) /3 width=9 by nlift_bind_sn/ - | #HnU2 elim (IHU12 … HnU2) -IHU12 -HnU2 -IHW12 /2 width=1 by yle_succ/ - #j #Hdj #Hji - >(plus_minus_m_m j 1) in ⊢ (%→?); [2: /3 width=3 by yle_trans, yle_inv_inj/ ] - #HnW1 @(ex3_intro … (j-1)) /3 width=9 by nlift_bind_dx, yle_pred, monotonic_pred/ - ] -| #I #G #L #W1 #W2 #U1 #U2 #d #e #_ #_ #IHW12 #IHU12 #i #Hdi #H elim (nlift_inv_flat … H) -H - [ #HnW2 elim (IHW12 … HnW2) -IHW12 -HnW2 -IHU12 // - #j #Hdj #Hji #HnW1 @(ex3_intro … j) /3 width=8 by nlift_flat_sn/ - | #HnU2 elim (IHU12 … HnU2) -IHU12 -HnU2 -IHW12 // - #j #Hdj #Hji #HnW1 @(ex3_intro … j) /3 width=8 by nlift_flat_dx/ - ] -] -qed-. - -axiom frees_fwd_nlift_ge: ∀L,U,d,i. (L ⊢ i ~ϵ 𝐅*[d]⦃U⦄ → ⊥) → d ≤ yinj i → - ∃∃j. d ≤ yinj j & j ≤ i & (∀T. ⇧[j, 1] T ≡ U → ⊥). - -(* -lemma frees_ind_nlift: ∀L,d. ∀R:relation2 term nat. - (∀U1,i. d ≤ yinj i → (∀T1. ⇧[i, 1] T1 ≡ U1 → ⊥) → R U1 i) → - (∀U1,U2,i,j. d ≤ yinj j → j ≤ i → ⦃⋆, L⦄ ⊢ U1 ▶[d, ∞] U2 → (∀T2. ⇧[i, 1] T2 ≡ U2 → ⊥) → R U2 i → R U1 j) → - ∀U,i. d ≤ yinj i → (L ⊢ i ~ϵ 𝐅*[d]⦃U⦄ → ⊥) → R U i. -#L #d #R #IH1 #IH2 #U1 #i #Hdi #H @(frees_ind … H) -U1 /3 width=4 by/ -#U1 #U2 #HU12 #HnU2 #HU2 @(IH2 … HU12 … HU2) - -qed-. -*)(* -lemma frees_fwd_nlift: ∀L,d. ∀R:relation2 term nat. ( - ∀U1,j. (∀T1. ⇧[j, 1] T1 ≡ U1 → ⊥) ∨ - (∃∃U2,i. d ≤ yinj j → j < i & (L ⊢ j ~ϵ 𝐅*[d]⦃U1⦄ → ⊥) & ⦃⋆, L⦄ ⊢ U1 ▶[d, ∞] U2 & R U1 i - ) → - d ≤ yinj j → R U1 j - ) → - ∀U,i. d ≤ yinj i → (L ⊢ i ~ϵ 𝐅*[d]⦃U⦄ → ⊥) → R U i. -#L #d #R #IHR #U1 #j #Hdj #H elim (frees_inv_gen … H) -H -#U2 #H generalize in match Hdj; -Hdj generalize in match j; -j @(cpys_ind … H) -U2 -[ #j #Hdj #HnU1 @IHR -IHR /3 width=2 by or_introl/ -| #U0 #U2 #HU10 #HU02 #IHU10 #j #Hdj #HnU2 elim (cpy_inv_nlift2_ge … HU02 … Hdj HnU2) -HU02 -HnU2 - #i #Hdi #Hij #HnU0 lapply (IHU10 … HnU0) // -IHU10 - #Hi @IHR -IHR // -Hdj @or_intror - -lemma frees_fwd_nlift: ∀L,U,d,i. d ≤ yinj i → (L ⊢ i ~ϵ 𝐅*[d]⦃U⦄ → ⊥) → - ∃∃j. d ≤ yinj j & j ≤ i & (∀T. ⇧[j, 1] T ≡ U → ⊥). -#L #U1 #d #i #Hdi #H -#U2 #H #HnU2 @(cpys_ind_dx … H) -U1 [ @(ex3_intro … i) /2 width=2 by/ ] -Hdi -HnU2 -#U1 #U0 #HU10 #_ * #j #Hdj #Hji #HnU0 elim (cpy_inv_nlift2_ge … HU10 … Hdj HnU0) -U0 -Hdj -/3 width=5 by transitive_le, ex3_intro/ -qed-. -*) - -theorem llpx_sn_llpx_sn_alt2: ∀R,L1,L2,T,d. llpx_sn R d T L1 L2 → llpx_sn_alt2 R d T L1 L2. -#R #L1 #L2 #U1 #d #H elim (llpx_sn_inv_alt1 … H) -H -#HL12 #IH @conj // -HL12 -#I1 #I2 #K1 #K2 #V1 #V2 #i #Hdi #H #HLK1 #HLK2 -elim (frees_fwd_nlift_ge … H Hdi) -H -Hdi #j #Hdj #Hji #HnU1 -lapply (ldrop_fwd_length_lt2 … HLK1) #HL1 -lapply (ldrop_fwd_length_lt2 … HLK2) #HL2 -lapply (le_to_lt_to_lt … Hji HL1) -HL1 #HL1 -lapply (le_to_lt_to_lt … Hji HL2) -HL2 #HL2 -elim (ldrop_O1_lt L1 j) // #Z1 #Y1 #X1 #HLY1 -elim (ldrop_O1_lt L2 j) // #Z2 #Y2 #X2 #HLY2 - - - - -generalize in match V2; -V2 generalize in match V1; -V1 -generalize in match K2; -K2 generalize in match K1; -K1 -generalize in match I2; -I2 generalize in match I1; -I1 -generalize in match IH; -IH -@(frees_ind_nlift … Hdi H) -U1 -i -[ #U1 #i #Hdi #HnU1 #IH #I1 #I2 #K1 #K2 #V1 #V2 #HLK1 #HLK2 elim (IH … HnU1 HLK1 HLK2) -IH -HnU1 -HLK1 -HLK2 /2 width=1 by conj/ -| #U1 #U2 #i #j #Hdj #Hji #HU12 #HnU2 #IHU12 #IH #I1 #I2 #K1 #K2 #V1 #V2 #HLK1 #HLK2 -(* -*) - @(IHU12) … HLK1 HLK2) - - @(IHU12 … HLK1 HLK2) -IHU02 -I1 -I2 -K1 -K2 -V1 -V2 - #I1 #I2 #K1 #K2 #V1 #V2 #j #Hdj #HnU0 #HLK1 #HLK2 @(IH … HLK1 HLK2) -IH -HLK1 -HLK2 // - - - - elim (frees_fwd_nlift … HnU1) // -HnU1 -Hdi -#j #Hdj #Hji #HnU1 -lapply (ldrop_fwd_length_lt2 … HLK1) #HL1 -lapply (ldrop_fwd_length_lt2 … HLK2) #HL2 -lapply (le_to_lt_to_lt … Hji HL1) -HL1 #HL1 -lapply (le_to_lt_to_lt … Hji HL2) -HL2 #HL2 -elim (ldrop_O1_lt L1 j) // #Z1 #Y1 #X1 #HLY1 -elim (ldrop_O1_lt L2 j) // #Z2 #Y2 #X2 #HLY2 -elim (IH … HnU1 HLY1 HLY2) // #H #HX12 #HY12 destruct - - - - - - - - - - - - - - - - - - - - - - -theorem llpx_sn_llpx_sn_alt2: ∀R,L1,L2,T,d. llpx_sn R d T L1 L2 → llpx_sn_alt2 R d T L1 L2. -#R #L1 #L2 #U1 #d #H @(llpx_sn_ind_alt1 … H) -L1 -L2 -U1 -d -#L1 #L2 #U1 #d #HL12 #IH @conj // -HL12 -#I1 #I2 #K1 #K2 #V1 #V2 #i #Hdi #HnU1 #HLK1 #HLK2 elim (frees_inv_gen … HnU1) -HnU1 -#U2 #H generalize in match IH; -IH @(cpys_ind_dx … H) -U1 -[ #IH #HnU2 elim (IH … HnU2 … HLK1 HLK2) -L1 -L2 -U2 /2 width=1 by conj/ -| #U1 #U0 #HU10 #_ #IHU02 #IH #HnU2 @IHU02 /2 width=2 by/ -I1 -I2 -K1 -K2 -V1 -V2 -U2 -i - #I1 #I2 #K1 #K2 #V1 #V2 #i #Hdi #HnU0 #HLK1 #HLK2 @(IH … HLK1 HLK2) -IH // -R -I2 -L2 -K2 -V2 - @(cpy_inv_nlift2_be … HU10) /2 width=3 by/ - -theorem llpx_sn_llpx_sn_alt2: ∀R,L1,L2,T2,d. llpx_sn R d T2 L1 L2 → - ∀T1. ⦃⋆, L1⦄ ⊢ T1 ▶*[d, ∞] T2 → llpx_sn_alt2 R d T1 L1 L2. -#R #L1 #L2 #U2 #d #H elim (llpx_sn_inv_alt1 … H) -H -#HL12 #IH #U1 #HU12 @conj // -HL12 -#I1 #I2 #K1 #K2 #V1 #V2 #i #Hdi #HnU1 #HLK1 #HLK2 elim (frees_inv_gen … HnU1) -HnU1 -#U2 #H generalize in match IH; -IH @(cpys_ind_dx … H) -U1 -[ #IH #HnU2 elim (IH … HnU2 … HLK1 HLK2) -L1 -L2 -U2 /2 width=1 by conj/ -| #U1 #U0 #HU10 #_ #IHU02 #IH #HnU2 @IHU02 /2 width=2 by/ -I1 -I2 -K1 -K2 -V1 -V2 -U2 -i - #I1 #I2 #K1 #K2 #V1 #V2 #i #Hdi #HnU0 #HLK1 #HLK2 @(IH … HLK1 HLK2) -IH // -R -I2 -L2 -K2 -V2 - @(cpy_inv_nlift2_be … HU10) /2 width=3 by/ - - -theorem llpx_sn_llpx_sn_alt2: ∀R,L1,L2,T,d. llpx_sn R d T L1 L2 → llpx_sn_alt2 R d T L1 L2. -#R #L1 #L2 #U1 #d #H elim (llpx_sn_inv_alt1 … H) -H -#HL12 #IH @conj // -HL12 -#I1 #I2 #K1 #K2 #V1 #V2 #i #Hdi #HnU1 #HLK1 #HLK2 elim (frees_inv_gen … HnU1) -HnU1 -#U2 #H generalize in match IH; -IH @(cpys_ind_dx … H) -U1 -[ #IH #HnU2 elim (IH … HnU2 … HLK1 HLK2) -L1 -L2 -U2 /2 width=1 by conj/ -| #U1 #U0 #HU10 #_ #IHU02 #IH #HnU2 @IHU02 /2 width=2 by/ -I1 -I2 -K1 -K2 -V1 -V2 -U2 -i - #I1 #I2 #K1 #K2 #V1 #V2 #i #Hdi #HnU0 #HLK1 #HLK2 @(IH … HLK1 HLK2) -IH // -R -I2 -L2 -K2 -V2 - @(cpy_inv_nlift2_be … HU10) /2 width=3 by/ diff --git a/matita/matita/contribs/lambdadelta/basic_2/relocation/cpy_nlift.ma b/matita/matita/contribs/lambdadelta/basic_2/relocation/cpy_nlift.ma new file mode 100644 index 000000000..42bb3f146 --- /dev/null +++ b/matita/matita/contribs/lambdadelta/basic_2/relocation/cpy_nlift.ma @@ -0,0 +1,66 @@ +(**************************************************************************) +(* ___ *) +(* ||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/relocation/cpy.ma". + +(* CONTEXT-SENSITIVE EXTENDED ORDINARY SUBSTITUTION FOR TERMS ***************) + +(* Inversion lemmas on negated relocation ***********************************) + +lemma cpy_fwd_nlift2_ge: ∀G,L,U1,U2,d,e. ⦃G, L⦄ ⊢ U1 ▶[d, e] U2 → + ∀i. d ≤ yinj i → (∀T2. ⇧[i, 1] T2 ≡ U2 → ⊥) → + (∀T1. ⇧[i, 1] T1 ≡ U1 → ⊥) ∨ + ∃∃I,K,W,j. d ≤ yinj j & j < i & ⇩[j]L ≡ K.ⓑ{I}W & + (∀V. ⇧[i-j-1, 1] V ≡ W → ⊥) & (∀T1. ⇧[j, 1] T1 ≡ U1 → ⊥). +#G #L #U1 #U2 #d #e #H elim H -G -L -U1 -U2 -d -e +[ /3 width=2 by or_introl/ +| #I #G #L #K #V #W #j #d #e #Hdj #Hjde #HLK #HVW #i #Hdi #HnW + elim (lt_or_ge j i) #Hij + [ @or_intror @(ex5_4_intro … HLK) // -HLK + [ #X #HXV elim (lift_trans_le … HXV … HVW ?) -V // + #Y #HXY >minus_plus (plus_minus_m_m j 1) in ⊢ (%→?); [2: /3 width=3 by yle_trans, yle_inv_inj/ ] + #HnU1 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-. diff --git a/matita/matita/contribs/lambdadelta/basic_2/substitution/cofrees_lift.ma b/matita/matita/contribs/lambdadelta/basic_2/substitution/cofrees_lift.ma index b8e4542a7..7dea71858 100644 --- a/matita/matita/contribs/lambdadelta/basic_2/substitution/cofrees_lift.ma +++ b/matita/matita/contribs/lambdadelta/basic_2/substitution/cofrees_lift.ma @@ -17,6 +17,37 @@ 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 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⦄. @@ -80,7 +111,7 @@ lemma frees_inv_gen: ∀L,U,d,i. (L ⊢ i ~ϵ 𝐅*[d]⦃U⦄ → ⊥) → [ -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=2 by ldrop_fwd_rfw/ -H -n + #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 @@ -103,3 +134,11 @@ lemma frees_ind: ∀L,d,i. ∀R:predicate term. #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-. diff --git a/matita/matita/contribs/lambdadelta/basic_2/substitution/llpx_sn_alt2.ma b/matita/matita/contribs/lambdadelta/basic_2/substitution/llpx_sn_alt2.ma new file mode 100644 index 000000000..8fbc6f8eb --- /dev/null +++ b/matita/matita/contribs/lambdadelta/basic_2/substitution/llpx_sn_alt2.ma @@ -0,0 +1,45 @@ +(**************************************************************************) +(* ___ *) +(* ||M|| *) +(* ||A|| A project by Andrea Asperti *) +(* ||T|| *) +(* ||I|| Developers: *) +(* ||T|| The HELM team. *) +(* ||A|| http://helm.cs.unibo.it *) +(* \ / *) +(* \ / This file is distributed under the terms of the *) +(* v GNU General Public License Version 2 *) +(* *) +(**************************************************************************) + +include "basic_2/substitution/cofrees_alt.ma". +include "basic_2/substitution/llpx_sn_alt1.ma". + +(* LAZY SN POINTWISE EXTENSION OF A CONTEXT-SENSITIVE REALTION FOR TERMS ****) + +(* alternative definition of llpx_sn (not recursive) *) +definition llpx_sn_alt2: relation4 bind2 lenv term term → relation4 ynat term lenv lenv ≝ + λR,d,T,L1,L2. |L1| = |L2| ∧ + (∀I1,I2,K1,K2,V1,V2,i. d ≤ yinj i → (L1 ⊢ i ~ϵ 𝐅*[d]⦃T⦄ → ⊥) → + ⇩[i] L1 ≡ K1.ⓑ{I1}V1 → ⇩[i] L2 ≡ K2.ⓑ{I2}V2 → + I1 = I2 ∧ R I1 K1 V1 V2 + ). + +(* Main properties **********************************************************) + +theorem llpx_sn_llpx_sn_alt2: ∀R,T,L1,L2,d. llpx_sn R d T L1 L2 → llpx_sn_alt2 R d T L1 L2. +#R #U #L1 @(f2_ind … rfw … L1 U) -L1 -U +#n #IHn #L1 #U #Hn #L2 #d #H elim (llpx_sn_inv_alt1 … H) -H +#HL12 #IHU @conj // +#I1 #I2 #K1 #K2 #V1 #V2 #i #Hdi #H #HLK1 #HLK2 elim (frees_inv_ge … H) -H // +[ -n #HnU elim (IHU … HnU HLK1 HLK2) -IHU -HnU -HLK1 -HLK2 /2 width=1 by conj/ +| * #J1 #K10 #W10 #j #Hdj #Hji #HLK10 #HnW10 #HnU destruct + lapply (ldrop_fwd_drop2 … HLK10) #H + lapply (ldrop_conf_ge … H … HLK1 ?) -H /2 width=1 by lt_to_le/