From: Ferruccio Guidi Date: Wed, 10 Feb 2016 11:20:14 +0000 (+0000) Subject: pre commit for lexs ... X-Git-Tag: make_still_working~646 X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=commitdiff_plain;h=093a2290feb8244a2397fa4767c283893a59f5e5;p=helm.git pre commit for lexs ... --- diff --git a/matita/matita/contribs/lambdadelta/basic_2/etc_new/lpx_sn/lpx_sn_alt.ma b/matita/matita/contribs/lambdadelta/basic_2/etc_new/lpx_sn/lpx_sn_alt.ma new file mode 100644 index 000000000..5099ffa1a --- /dev/null +++ b/matita/matita/contribs/lambdadelta/basic_2/etc_new/lpx_sn/lpx_sn_alt.ma @@ -0,0 +1,127 @@ +(**************************************************************************) +(* ___ *) +(* ||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/drop.ma". +include "basic_2/substitution/lpx_sn.ma". + +(* SN POINTWISE EXTENSION OF A CONTEXT-SENSITIVE REALTION FOR TERMS *********) + +(* alternative definition of lpx_sn *) +definition lpx_sn_alt: relation3 lenv term term → relation lenv ≝ + λR,L1,L2. |L1| = |L2| ∧ + (∀I1,I2,K1,K2,V1,V2,i. + ⬇[i] L1 ≡ K1.ⓑ{I1}V1 → ⬇[i] L2 ≡ K2.ⓑ{I2}V2 → + I1 = I2 ∧ R K1 V1 V2 + ). + +(* Basic forward lemmas ******************************************************) + +lemma lpx_sn_alt_fwd_length: ∀R,L1,L2. lpx_sn_alt R L1 L2 → |L1| = |L2|. +#R #L1 #L2 #H elim H // +qed-. + +(* Basic inversion lemmas ***************************************************) + +lemma lpx_sn_alt_inv_atom1: ∀R,L2. lpx_sn_alt R (⋆) L2 → L2 = ⋆. +#R #L2 #H lapply (lpx_sn_alt_fwd_length … H) -H +normalize /2 width=1 by length_inv_zero_sn/ +qed-. + +lemma lpx_sn_alt_inv_pair1: ∀R,I,L2,K1,V1. lpx_sn_alt R (K1.ⓑ{I}V1) L2 → + ∃∃K2,V2. lpx_sn_alt R K1 K2 & R K1 V1 V2 & L2 = K2.ⓑ{I}V2. +#R #I1 #L2 #K1 #V1 #H elim H -H +#H #IH elim (length_inv_pos_sn … H) -H +#I2 #K2 #V2 #HK12 #H destruct +elim (IH I1 I2 K1 K2 V1 V2 0) // +#H #HV12 destruct @(ex3_2_intro … K2 V2) // -HV12 +@conj // -HK12 +#J1 #J2 #L1 #L2 #W1 #W2 #i #HKL1 #HKL2 elim (IH J1 J2 L1 L2 W1 W2 (⫯i)) -IH +/2 width=1 by drop_drop, conj/ +qed-. + +lemma lpx_sn_alt_inv_atom2: ∀R,L1. lpx_sn_alt R L1 (⋆) → L1 = ⋆. +#R #L1 #H lapply (lpx_sn_alt_fwd_length … H) -H +normalize /2 width=1 by length_inv_zero_dx/ +qed-. + +lemma lpx_sn_alt_inv_pair2: ∀R,I,L1,K2,V2. lpx_sn_alt R L1 (K2.ⓑ{I}V2) → + ∃∃K1,V1. lpx_sn_alt R K1 K2 & R K1 V1 V2 & L1 = K1.ⓑ{I}V1. +#R #I2 #L1 #K2 #V2 #H elim H -H +#H #IH elim (length_inv_pos_dx … H) -H +#I1 #K1 #V1 #HK12 #H destruct +elim (IH I1 I2 K1 K2 V1 V2 0) // +#H #HV12 destruct @(ex3_2_intro … K1 V1) // -HV12 +@conj // -HK12 +#J1 #J2 #L1 #L2 #W1 #W2 #i #HKL1 #HKL2 elim (IH J1 J2 L1 L2 W1 W2 (⫯i)) -IH +/2 width=1 by drop_drop, conj/ +qed-. + +(* Basic properties *********************************************************) + +lemma lpx_sn_alt_atom: ∀R. lpx_sn_alt R (⋆) (⋆). +#R @conj // +#I1 #I2 #K1 #K2 #V1 #V2 #i #HLK1 elim (drop_inv_atom1 … HLK1) -HLK1 +#H destruct +qed. + +lemma lpx_sn_alt_pair: ∀R,I,L1,L2,V1,V2. + lpx_sn_alt R L1 L2 → R L1 V1 V2 → + lpx_sn_alt R (L1.ⓑ{I}V1) (L2.ⓑ{I}V2). +#R #I #L1 #L2 #V1 #V2 #H #HV12 elim H -H +#HL12 #IH @conj // +#I1 #I2 #K1 #K2 #W1 #W2 #i @(ynat_ind … i) -i +[ #HLK1 #HLK2 + lapply (drop_inv_O2 … HLK1) -HLK1 #H destruct + lapply (drop_inv_O2 … HLK2) -HLK2 #H destruct + /2 width=1 by conj/ +| -HL12 -HV12 /3 width=6 by drop_inv_drop1/ +| #H lapply (drop_fwd_Y2 … H) -H + #H elim (ylt_yle_false … H) -H // +] +qed. + +(* Main properties **********************************************************) + +theorem lpx_sn_lpx_sn_alt: ∀R,L1,L2. lpx_sn R L1 L2 → lpx_sn_alt R L1 L2. +#R #L1 #L2 #H elim H -L1 -L2 +/2 width=1 by lpx_sn_alt_atom, lpx_sn_alt_pair/ +qed. + +(* Main inversion lemmas ****************************************************) + +theorem lpx_sn_alt_inv_lpx_sn: ∀R,L1,L2. lpx_sn_alt R L1 L2 → lpx_sn R L1 L2. +#R #L1 elim L1 -L1 +[ #L2 #H lapply (lpx_sn_alt_inv_atom1 … H) -H // +| #L1 #I #V1 #IH #X #H elim (lpx_sn_alt_inv_pair1 … H) -H + #L2 #V2 #HL12 #HV12 #H destruct /3 width=1 by lpx_sn_pair/ +] +qed-. + +(* alternative definition of lpx_sn *****************************************) + +lemma lpx_sn_intro_alt: ∀R,L1,L2. |L1| = |L2| → + (∀I1,I2,K1,K2,V1,V2,i. + ⬇[i] L1 ≡ K1.ⓑ{I1}V1 → ⬇[i] L2 ≡ K2.ⓑ{I2}V2 → + I1 = I2 ∧ R K1 V1 V2 + ) → lpx_sn R L1 L2. +/4 width=4 by lpx_sn_alt_inv_lpx_sn, conj/ qed. + +lemma lpx_sn_inv_alt: ∀R,L1,L2. lpx_sn R L1 L2 → + |L1| = |L2| ∧ + ∀I1,I2,K1,K2,V1,V2,i. + ⬇[i] L1 ≡ K1.ⓑ{I1}V1 → ⬇[i] L2 ≡ K2.ⓑ{I2}V2 → + I1 = I2 ∧ R K1 V1 V2. +#R #L1 #L2 #H lapply (lpx_sn_lpx_sn_alt … H) -H +#H elim H -H /3 width=4 by conj/ +qed-. diff --git a/matita/matita/contribs/lambdadelta/basic_2/etc_new/lpx_sn/lpx_sn_drop.ma b/matita/matita/contribs/lambdadelta/basic_2/etc_new/lpx_sn/lpx_sn_drop.ma new file mode 100644 index 000000000..f69814078 --- /dev/null +++ b/matita/matita/contribs/lambdadelta/basic_2/etc_new/lpx_sn/lpx_sn_drop.ma @@ -0,0 +1,58 @@ +definition dropable_dx: predicate (relation lenv) ≝ + λR. ∀L1,L2. R L1 L2 → ∀K2,c,k. ⬇[c, 0, k] L2 ≡ K2 → + ∃∃K1. ⬇[c, 0, k] L1 ≡ K1 & R K1 K2. + +lemma dropable_dx_TC: ∀R. dropable_dx R → dropable_dx (TC … R). +#R #HR #L1 #L2 #H elim H -L2 +[ #L2 #HL12 #K2 #c #k #HLK2 elim (HR … HL12 … HLK2) -HR -L2 + /3 width=3 by inj, ex2_intro/ +| #L #L2 #_ #HL2 #IHL1 #K2 #c #k #HLK2 elim (HR … HL2 … HLK2) -HR -L2 + #K #HLK #HK2 elim (IHL1 … HLK) -L + /3 width=5 by step, ex2_intro/ +] +qed-. + + +fact lpx_sn_dropable_aux: ∀R,L2,K2,c,l,k. ⬇[c, l, k] L2 ≡ K2 → ∀L1. lpx_sn R L1 L2 → + l = 0 → ∃∃K1. ⬇[c, 0, k] L1 ≡ K1 & lpx_sn R K1 K2. +#R #L2 #K2 #c #l #k #H elim H -L2 -K2 -l -k +[ #l #k #Hm #X #H >(lpx_sn_inv_atom2 … H) -H + /4 width=3 by drop_atom, lpx_sn_atom, ex2_intro/ +| #I #K2 #V2 #X #H elim (lpx_sn_inv_pair2 … H) -H + #K1 #V1 #HK12 #HV12 #H destruct + /3 width=5 by drop_pair, lpx_sn_pair, ex2_intro/ +| #I #L2 #K2 #V2 #k #_ #IHLK2 #X #H #_ elim (lpx_sn_inv_pair2 … H) -H + #L1 #V1 #HL12 #HV12 #H destruct + elim (IHLK2 … HL12) -L2 /3 width=3 by drop_drop, ex2_intro/ +| #I #L2 #K2 #V2 #W2 #l #k #_ #_ #_ #L1 #_ #H elim (ysucc_inv_O_dx … H) +] +qed-. + +lemma lpx_sn_dropable: ∀R. dropable_dx (lpx_sn R). +/2 width=5 by lpx_sn_dropable_aux/ qed-. + +lemma lpx_sn_drop_trans: ∀R,L1,L2. lpx_sn R L1 L2 → + ∀I,K2,V2,i. ⬇[i] L2 ≡ K2.ⓑ{I}V2 → + ∃∃K1,V1. ⬇[i] L1 ≡ K1.ⓑ{I}V1 & lpx_sn R K1 K2 & R K1 V1 V2. +#R #L1 #L2 #H elim H -L1 -L2 +[ #I0 #K0 #V0 #i #H elim (drop_inv_atom1 … H) -H #H destruct +| #I #K1 #K2 #V1 #V2 #HK12 #HV12 #IHK12 #I0 #K0 #V0 #i #H elim (drop_inv_O1_pair1 … H) * -H + [ -IHK12 #H1 #H2 destruct /3 width=5 by drop_pair, ex3_2_intro/ + | -HK12 -HV12 #Hi #HK10 elim (IHK12 … HK10) -IHK12 -HK10 + /3 width=5 by drop_drop_lt, ex3_2_intro/ + ] +] +qed-. + +lemma lpx_sn_drop_conf: ∀R,L1,L2. lpx_sn R L1 L2 → + ∀I,K1,V1,i. ⬇[i] L1 ≡ K1.ⓑ{I}V1 → + ∃∃K2,V2. ⬇[i] L2 ≡ K2.ⓑ{I}V2 & lpx_sn R K1 K2 & R K1 V1 V2. +#R #L1 #L2 #H elim H -L1 -L2 +[ #I0 #K0 #V0 #i #H elim (drop_inv_atom1 … H) -H #H destruct +| #I #K1 #K2 #V1 #V2 #HK12 #HV12 #IHK12 #I0 #K0 #V0 #i #H elim (drop_inv_O1_pair1 … H) * -H + [ -IHK12 #H1 #H2 destruct /3 width=5 by drop_pair, ex3_2_intro/ + | -HK12 -HV12 #Hi #HK10 elim (IHK12 … HK10) -IHK12 -HK10 + /3 width=5 by drop_drop_lt, ex3_2_intro/ + ] +] +qed-. diff --git a/matita/matita/contribs/lambdadelta/basic_2/relocation/lpx_sn.ma b/matita/matita/contribs/lambdadelta/basic_2/relocation/lpx_sn.ma new file mode 100644 index 000000000..513d62019 --- /dev/null +++ b/matita/matita/contribs/lambdadelta/basic_2/relocation/lpx_sn.ma @@ -0,0 +1,191 @@ +(**************************************************************************) +(* ___ *) +(* ||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/relocation/nstream_sle.ma". +include "basic_2/notation/relations/relationstar_5.ma". +include "basic_2/grammar/lenv.ma". + +(* GENERAL ENTRYWISE EXTENSION OF A CONTEXT-SENSITIVE REALTION FOR TERMS ****) + +(* Basic_2A1: includes: lpx_sn_atom lpx_sn_pair *) +inductive lexs (RS,RO:relation3 lenv term term): rtmap → relation lenv ≝ +| lexs_atom: ∀f. lexs RS RO f (⋆) (⋆) +| lexs_next: ∀I,L1,L2,V1,V2,f. + lexs RS RO f L1 L2 → RS L1 V1 V2 → + lexs RS RO (⫯f) (L1.ⓑ{I}V1) (L2.ⓑ{I}V2) +| lexs_push: ∀I,L1,L2,V1,V2,f. + lexs RS RO f L1 L2 → RO L1 V1 V2 → + lexs RS RO (↑f) (L1.ⓑ{I}V1) (L2.ⓑ{I}V2) +. + +interpretation "general entrywise extension (local environment)" + 'RelationStar RS RO f L1 L2 = (lexs RS RO f L1 L2). + +(* Basic inversion lemmas ***************************************************) + +fact lexs_inv_atom1_aux: ∀RS,RO,X,Y,f. X ⦻*[RS, RO, f] Y → X = ⋆ → Y = ⋆. +#RS #RO #X #Y #f * -X -Y -f // +#I #L1 #L2 #V1 #V2 #f #_ #_ #H destruct +qed-. + +(* Basic_2A1: includes lpx_sn_inv_atom1 *) +lemma lexs_inv_atom1: ∀RS,RO,Y,f. ⋆ ⦻*[RS, RO, f] Y → Y = ⋆. +/2 width=6 by lexs_inv_atom1_aux/ qed-. + +fact lexs_inv_next1_aux: ∀RS,RO,X,Y,f. X ⦻*[RS, RO, f] Y → ∀J,K1,W1,g. X = K1.ⓑ{J}W1 → f = ⫯g → + ∃∃K2,W2. K1 ⦻*[RS, RO, g] K2 & RS K1 W1 W2 & Y = K2.ⓑ{J}W2. +#RS #RO #X #Y #f * -X -Y -f +[ #f #J #K1 #W1 #g #H destruct +| #I #L1 #L2 #V1 #V2 #f #HL #HS #J #K1 #W1 #g #H1 #H2 <(injective_next … H2) -g destruct + /2 width=5 by ex3_2_intro/ +| #I #L1 #L2 #V1 #V2 #f #_ #_ #J #K1 #W1 #g #_ #H elim (discr_push_next … H) +] +qed-. + +(* Basic_2A1: includes lpx_sn_inv_pair1 *) +lemma lexs_inv_next1: ∀RS,RO,J,K1,Y,W1,g. K1.ⓑ{J}W1 ⦻*[RS, RO, ⫯g] Y → + ∃∃K2,W2. K1 ⦻*[RS, RO, g] K2 & RS K1 W1 W2 & Y = K2.ⓑ{J}W2. +/2 width=7 by lexs_inv_next1_aux/ qed-. + + +fact lexs_inv_push1_aux: ∀RS,RO,X,Y,f. X ⦻*[RS, RO, f] Y → ∀J,K1,W1,g. X = K1.ⓑ{J}W1 → f = ↑g → + ∃∃K2,W2. K1 ⦻*[RS, RO, g] K2 & RO K1 W1 W2 & Y = K2.ⓑ{J}W2. +#RS #RO #X #Y #f * -X -Y -f +[ #f #J #K1 #W1 #g #H destruct +| #I #L1 #L2 #V1 #V2 #f #_ #_ #J #K1 #W1 #g #_ #H elim (discr_next_push … H) +| #I #L1 #L2 #V1 #V2 #f #HL #HO #J #K1 #W1 #g #H1 #H2 <(injective_push … H2) -g destruct + /2 width=5 by ex3_2_intro/ +] +qed-. + +lemma lexs_inv_push1: ∀RS,RO,J,K1,Y,W1,g. K1.ⓑ{J}W1 ⦻*[RS, RO, ↑g] Y → + ∃∃K2,W2. K1 ⦻*[RS, RO, g] K2 & RO K1 W1 W2 & Y = K2.ⓑ{J}W2. +/2 width=7 by lexs_inv_push1_aux/ qed-. + +fact lexs_inv_atom2_aux: ∀RS,RO,X,Y,f. X ⦻*[RS, RO, f] Y → Y = ⋆ → X = ⋆. +#RS #RO #X #Y #f * -X -Y -f // +#I #L1 #L2 #V1 #V2 #f #_ #_ #H destruct +qed-. + +(* Basic_2A1: includes lpx_sn_inv_atom2 *) +lemma lexs_inv_atom2: ∀RS,RO,X,f. X ⦻*[RS, RO, f] ⋆ → X = ⋆. +/2 width=6 by lexs_inv_atom2_aux/ qed-. + +fact lexs_inv_next2_aux: ∀RS,RO,X,Y,f. X ⦻*[RS, RO, f] Y → ∀J,K2,W2,g. Y = K2.ⓑ{J}W2 → f = ⫯g → + ∃∃K1,W1. K1 ⦻*[RS, RO, g] K2 & RS K1 W1 W2 & X = K1.ⓑ{J}W1. +#RS #RO #X #Y #f * -X -Y -f +[ #f #J #K2 #W2 #g #H destruct +| #I #L1 #L2 #V1 #V2 #f #HL #HS #J #K2 #W2 #g #H1 #H2 <(injective_next … H2) -g destruct + /2 width=5 by ex3_2_intro/ +| #I #L1 #L2 #V1 #V2 #f #_ #_ #J #K2 #W2 #g #_ #H elim (discr_push_next … H) +] +qed-. + +(* Basic_2A1: includes lpx_sn_inv_pair2 *) +lemma lexs_inv_next2: ∀RS,RO,J,X,K2,W2,g. X ⦻*[RS, RO, ⫯g] K2.ⓑ{J}W2 → + ∃∃K1,W1. K1 ⦻*[RS, RO, g] K2 & RS K1 W1 W2 & X = K1.ⓑ{J}W1. +/2 width=7 by lexs_inv_next2_aux/ qed-. + +fact lexs_inv_push2_aux: ∀RS,RO,X,Y,f. X ⦻*[RS, RO, f] Y → ∀J,K2,W2,g. Y = K2.ⓑ{J}W2 → f = ↑g → + ∃∃K1,W1. K1 ⦻*[RS, RO, g] K2 & RO K1 W1 W2 & X = K1.ⓑ{J}W1. +#RS #RO #X #Y #f * -X -Y -f +[ #f #J #K2 #W2 #g #H destruct +| #I #L1 #L2 #V1 #V2 #f #_ #_ #J #K2 #W2 #g #_ #H elim (discr_next_push … H) +| #I #L1 #L2 #V1 #V2 #f #HL #HO #J #K2 #W2 #g #H1 #H2 <(injective_push … H2) -g destruct + /2 width=5 by ex3_2_intro/ +] +qed-. + +lemma lexs_inv_push2: ∀RS,RO,J,X,K2,W2,g. X ⦻*[RS, RO, ↑g] K2.ⓑ{J}W2 → + ∃∃K1,W1. K1 ⦻*[RS, RO, g] K2 & RO K1 W1 W2 & X = K1.ⓑ{J}W1. +/2 width=7 by lexs_inv_push2_aux/ qed-. + +(* Basic_2A1: includes lpx_sn_inv_pair *) +lemma lexs_inv_next: ∀RS,RO,I1,I2,L1,L2,V1,V2,f. + L1.ⓑ{I1}V1 ⦻*[RS, RO, ⫯f] (L2.ⓑ{I2}V2) → + ∧∧ L1 ⦻*[RS, RO, f] L2 & RS L1 V1 V2 & I1 = I2. +#RS #RO #I1 #I2 #L1 #L2 #V1 #V2 #f #H elim (lexs_inv_next1 … H) -H +#L0 #V0 #HL10 #HV10 #H destruct /2 width=1 by and3_intro/ +qed-. + +lemma lexs_inv_push: ∀RS,RO,I1,I2,L1,L2,V1,V2,f. + L1.ⓑ{I1}V1 ⦻*[RS, RO, ↑f] (L2.ⓑ{I2}V2) → + ∧∧ L1 ⦻*[RS, RO, f] L2 & RO L1 V1 V2 & I1 = I2. +#RS #RO #I1 #I2 #L1 #L2 #V1 #V2 #f #H elim (lexs_inv_push1 … H) -H +#L0 #V0 #HL10 #HV10 #H destruct /2 width=1 by and3_intro/ +qed-. + +(* Basic properties *********************************************************) + +lemma lexs_eq_repl_back: ∀RS,RO,L1,L2. eq_stream_repl_back … (λf. L1 ⦻*[RS, RO, f] L2). +#RS #RO #L1 #L2 #f1 #H elim H -L1 -L2 -f1 // +[ #I #L1 #L2 #V1 #v2 #f1 #_ #HS #IH #f2 #H elim (next_inv_sn … H) -H /3 width=1 by lexs_next/ +| #I #L1 #L2 #V1 #v2 #f1 #_ #HO #IH #f2 #H elim (push_inv_sn … H) -H /3 width=1 by lexs_push/ +] +qed-. + +lemma lexs_eq_repl_fwd: ∀RS,RO,L1,L2. eq_stream_repl_fwd … (λf. L1 ⦻*[RS, RO, f] L2). +#RS #RO #L1 #L2 @eq_stream_repl_sym /2 width=3 by lexs_eq_repl_back/ (**) (* full auto fails *) +qed-. + +(* Basic_2A1: includes: lpx_sn_refl *) +lemma lexs_refl: ∀RS,RO,f. + (∀L. reflexive … (RS L)) → + (∀L. reflexive … (RO L)) → + reflexive … (lexs RS RO f). +#RS #RO #f #HS #HO #L generalize in match f; -f elim L -L // +#L #I #V #IH * * /2 width=1 by lexs_next, lexs_push/ +qed. + +lemma sle_lexs_trans: ∀RS,RO. (∀L,T1,T2. RO L T1 T2 → RS L T1 T2) → + ∀L1,L2,f2. L1 ⦻*[RS, RO, f2] L2 → + ∀f1. f1 ⊆ f2 → L1 ⦻*[RS, RO, f1] L2. +#RS #RO #HR #L1 #L2 #f2 #H elim H -L1 -L2 -f2 // +#I #L1 #L2 #V1 #V2 #f2 #_ #HV12 #IH +[2: * * [2: #n1 ] ] #f1 #H +[ (lpx_sn_inv_atom1 … H) -H + /4 width=4 by drop_atom, lpx_sn_atom, ex3_intro/ +| #I #K1 #V1 #X #H elim (lpx_sn_inv_pair1 … H) -H + #K2 #V2 #HK12 #HV12 #H destruct + lapply (lpx_sn_fwd_length … HK12) + #H @(ex3_intro … (K2.ⓑ{I}V2)) (**) (* explicit constructor *) + /3 width=1 by lpx_sn_pair, lreq_O2/ +| #I #L1 #K1 #V1 #m #_ #IHLK1 #K2 #HK12 elim (IHLK1 … HK12) -K1 + /3 width=5 by drop_drop, lreq_pair, lpx_sn_pair, ex3_intro/ +| #I #L1 #K1 #V1 #W1 #l #m #HLK1 #HWV1 #IHLK1 #X #H + elim (lpx_sn_inv_pair1 … H) -H #K2 #W2 #HK12 #HW12 #H destruct + elim (H2R … HW12 … HLK1 … HWV1) -W1 + elim (IHLK1 … HK12) -K1 + /3 width=6 by drop_skip, lreq_succ, lpx_sn_pair, ex3_intro/ +] +qed-. +*) +include "ground_2/relocation/trace_isun.ma". + +lemma lpx_sn_dropable: ∀R,L2,K2,c,t. ⬇*[c, t] L2 ≡ K2 → 𝐔⦃t⦄ → + ∀L1,u2. lpx_sn R u2 L1 L2 → ∀u1. t ⊚ u1 ≡ u2 → + ∃∃K1. ⬇*[c, t] L1 ≡ K1 & lpx_sn R u1 K1 K2. +#R #L2 #K2 #c #t #H elim H -L2 -K2 -t +[ #t #Ht #_ #X #u2 #H #u1 #Hu elim (lpx_sn_inv_atom2 … H) -H + #H1 #H2 destruct elim (after_inv_empty3 … Hu) -Hu + /4 width=3 by drops_atom, lpx_sn_atom, ex2_intro/ +| #I #L2 #K2 #V2 #t #_ #IH #Ht #X #u2 #H #u1 #Hu elim (lpx_sn_inv_pair2 … H) -H + #L1 #V1 #y2 #x #HL #HV #H1 #H2 destruct elim (after_inv_false1 … Hu) -Hu + #u #H #Hu destruct elim (IH … HL … Hu) -L2 /3 width=3 by drops_drop, isun_inv_false, ex2_intro/ +| #I #L2 #K2 #V2 #W2 #t #_ #HWV #IHLK #Ht #X #u2 #H #u1 #Hu elim (lpx_sn_inv_pair2 … H) -H + #L1 #V1 #y2 #x #HL #HV #H1 #H2 destruct elim (after_inv_true1 … Hu) -Hu + #y1 #y #x2 #H1 #H2 #Hu destruct lapply (isun_inv_true … Ht) -Ht + #Ht elim (IHLK … HL … Hu) -L2 -Hu /2 width=1 by isun_id/ + #K1 #HLK1 #HK12 lapply (lifts_fwd_isid … HWV ?) // -HWV + #H destruct lapply (drops_fwd_isid … HLK1 ?) // + #H destruct + @ex2_intro + [ + | @(drops_skip … HLK1) + | @(lpx_sn_pair … HK12 … HV) + + + lapply (drops_fwd_isid … HLK1 ?) // -HLK1 + 2: + + + + + elim (HR … HV … HLK … HWV) -V1 + elim (IHLK … HL … Hu) -L1 /3 width=5 by drops_skip, lpx_sn_pair, ex2_intro/ + + +] +qed-. diff --git a/matita/matita/contribs/lambdadelta/basic_2/substitution/lpx_sn.ma b/matita/matita/contribs/lambdadelta/basic_2/substitution/lpx_sn.ma deleted file mode 100644 index 82664b828..000000000 --- a/matita/matita/contribs/lambdadelta/basic_2/substitution/lpx_sn.ma +++ /dev/null @@ -1,89 +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/grammar/lenv_length.ma". - -(* SN POINTWISE EXTENSION OF A CONTEXT-SENSITIVE REALTION FOR TERMS *********) - -inductive lpx_sn (R:relation3 lenv term term): relation lenv ≝ -| lpx_sn_atom: lpx_sn R (⋆) (⋆) -| lpx_sn_pair: ∀I,K1,K2,V1,V2. - lpx_sn R K1 K2 → R K1 V1 V2 → - lpx_sn R (K1. ⓑ{I} V1) (K2. ⓑ{I} V2) -. - -(* Basic properties *********************************************************) - -lemma lpx_sn_refl: ∀R. (∀L. reflexive ? (R L)) → reflexive … (lpx_sn R). -#R #HR #L elim L -L /2 width=1 by lpx_sn_atom, lpx_sn_pair/ -qed-. - -(* Basic inversion lemmas ***************************************************) - -fact lpx_sn_inv_atom1_aux: ∀R,L1,L2. lpx_sn R L1 L2 → L1 = ⋆ → L2 = ⋆. -#R #L1 #L2 * -L1 -L2 -[ // -| #I #K1 #K2 #V1 #V2 #_ #_ #H destruct -] -qed-. - -lemma lpx_sn_inv_atom1: ∀R,L2. lpx_sn R (⋆) L2 → L2 = ⋆. -/2 width=4 by lpx_sn_inv_atom1_aux/ qed-. - -fact lpx_sn_inv_pair1_aux: ∀R,L1,L2. lpx_sn R L1 L2 → ∀I,K1,V1. L1 = K1. ⓑ{I} V1 → - ∃∃K2,V2. lpx_sn R K1 K2 & R K1 V1 V2 & L2 = K2. ⓑ{I} V2. -#R #L1 #L2 * -L1 -L2 -[ #J #K1 #V1 #H destruct -| #I #K1 #K2 #V1 #V2 #HK12 #HV12 #J #L #W #H destruct /2 width=5 by ex3_2_intro/ -] -qed-. - -lemma lpx_sn_inv_pair1: ∀R,I,K1,V1,L2. lpx_sn R (K1. ⓑ{I} V1) L2 → - ∃∃K2,V2. lpx_sn R K1 K2 & R K1 V1 V2 & L2 = K2. ⓑ{I} V2. -/2 width=3 by lpx_sn_inv_pair1_aux/ qed-. - -fact lpx_sn_inv_atom2_aux: ∀R,L1,L2. lpx_sn R L1 L2 → L2 = ⋆ → L1 = ⋆. -#R #L1 #L2 * -L1 -L2 -[ // -| #I #K1 #K2 #V1 #V2 #_ #_ #H destruct -] -qed-. - -lemma lpx_sn_inv_atom2: ∀R,L1. lpx_sn R L1 (⋆) → L1 = ⋆. -/2 width=4 by lpx_sn_inv_atom2_aux/ qed-. - -fact lpx_sn_inv_pair2_aux: ∀R,L1,L2. lpx_sn R L1 L2 → ∀I,K2,V2. L2 = K2. ⓑ{I} V2 → - ∃∃K1,V1. lpx_sn R K1 K2 & R K1 V1 V2 & L1 = K1. ⓑ{I} V1. -#R #L1 #L2 * -L1 -L2 -[ #J #K2 #V2 #H destruct -| #I #K1 #K2 #V1 #V2 #HK12 #HV12 #J #K #W #H destruct /2 width=5 by ex3_2_intro/ -] -qed-. - -lemma lpx_sn_inv_pair2: ∀R,I,L1,K2,V2. lpx_sn R L1 (K2. ⓑ{I} V2) → - ∃∃K1,V1. lpx_sn R K1 K2 & R K1 V1 V2 & L1 = K1. ⓑ{I} V1. -/2 width=3 by lpx_sn_inv_pair2_aux/ qed-. - -lemma lpx_sn_inv_pair: ∀R,I1,I2,L1,L2,V1,V2. - lpx_sn R (L1.ⓑ{I1}V1) (L2.ⓑ{I2}V2) → - ∧∧ lpx_sn R L1 L2 & R L1 V1 V2 & I1 = I2. -#R #I1 #I2 #L1 #L2 #V1 #V2 #H elim (lpx_sn_inv_pair1 … H) -H -#L0 #V0 #HL10 #HV10 #H destruct /2 width=1 by and3_intro/ -qed-. - -(* Basic forward lemmas *****************************************************) - -lemma lpx_sn_fwd_length: ∀R,L1,L2. lpx_sn R L1 L2 → |L1| = |L2|. -#R #L1 #L2 #H elim H -L1 -L2 // -qed-. diff --git a/matita/matita/contribs/lambdadelta/basic_2/substitution/lpx_sn_alt.ma b/matita/matita/contribs/lambdadelta/basic_2/substitution/lpx_sn_alt.ma deleted file mode 100644 index 5099ffa1a..000000000 --- a/matita/matita/contribs/lambdadelta/basic_2/substitution/lpx_sn_alt.ma +++ /dev/null @@ -1,127 +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/drop.ma". -include "basic_2/substitution/lpx_sn.ma". - -(* SN POINTWISE EXTENSION OF A CONTEXT-SENSITIVE REALTION FOR TERMS *********) - -(* alternative definition of lpx_sn *) -definition lpx_sn_alt: relation3 lenv term term → relation lenv ≝ - λR,L1,L2. |L1| = |L2| ∧ - (∀I1,I2,K1,K2,V1,V2,i. - ⬇[i] L1 ≡ K1.ⓑ{I1}V1 → ⬇[i] L2 ≡ K2.ⓑ{I2}V2 → - I1 = I2 ∧ R K1 V1 V2 - ). - -(* Basic forward lemmas ******************************************************) - -lemma lpx_sn_alt_fwd_length: ∀R,L1,L2. lpx_sn_alt R L1 L2 → |L1| = |L2|. -#R #L1 #L2 #H elim H // -qed-. - -(* Basic inversion lemmas ***************************************************) - -lemma lpx_sn_alt_inv_atom1: ∀R,L2. lpx_sn_alt R (⋆) L2 → L2 = ⋆. -#R #L2 #H lapply (lpx_sn_alt_fwd_length … H) -H -normalize /2 width=1 by length_inv_zero_sn/ -qed-. - -lemma lpx_sn_alt_inv_pair1: ∀R,I,L2,K1,V1. lpx_sn_alt R (K1.ⓑ{I}V1) L2 → - ∃∃K2,V2. lpx_sn_alt R K1 K2 & R K1 V1 V2 & L2 = K2.ⓑ{I}V2. -#R #I1 #L2 #K1 #V1 #H elim H -H -#H #IH elim (length_inv_pos_sn … H) -H -#I2 #K2 #V2 #HK12 #H destruct -elim (IH I1 I2 K1 K2 V1 V2 0) // -#H #HV12 destruct @(ex3_2_intro … K2 V2) // -HV12 -@conj // -HK12 -#J1 #J2 #L1 #L2 #W1 #W2 #i #HKL1 #HKL2 elim (IH J1 J2 L1 L2 W1 W2 (⫯i)) -IH -/2 width=1 by drop_drop, conj/ -qed-. - -lemma lpx_sn_alt_inv_atom2: ∀R,L1. lpx_sn_alt R L1 (⋆) → L1 = ⋆. -#R #L1 #H lapply (lpx_sn_alt_fwd_length … H) -H -normalize /2 width=1 by length_inv_zero_dx/ -qed-. - -lemma lpx_sn_alt_inv_pair2: ∀R,I,L1,K2,V2. lpx_sn_alt R L1 (K2.ⓑ{I}V2) → - ∃∃K1,V1. lpx_sn_alt R K1 K2 & R K1 V1 V2 & L1 = K1.ⓑ{I}V1. -#R #I2 #L1 #K2 #V2 #H elim H -H -#H #IH elim (length_inv_pos_dx … H) -H -#I1 #K1 #V1 #HK12 #H destruct -elim (IH I1 I2 K1 K2 V1 V2 0) // -#H #HV12 destruct @(ex3_2_intro … K1 V1) // -HV12 -@conj // -HK12 -#J1 #J2 #L1 #L2 #W1 #W2 #i #HKL1 #HKL2 elim (IH J1 J2 L1 L2 W1 W2 (⫯i)) -IH -/2 width=1 by drop_drop, conj/ -qed-. - -(* Basic properties *********************************************************) - -lemma lpx_sn_alt_atom: ∀R. lpx_sn_alt R (⋆) (⋆). -#R @conj // -#I1 #I2 #K1 #K2 #V1 #V2 #i #HLK1 elim (drop_inv_atom1 … HLK1) -HLK1 -#H destruct -qed. - -lemma lpx_sn_alt_pair: ∀R,I,L1,L2,V1,V2. - lpx_sn_alt R L1 L2 → R L1 V1 V2 → - lpx_sn_alt R (L1.ⓑ{I}V1) (L2.ⓑ{I}V2). -#R #I #L1 #L2 #V1 #V2 #H #HV12 elim H -H -#HL12 #IH @conj // -#I1 #I2 #K1 #K2 #W1 #W2 #i @(ynat_ind … i) -i -[ #HLK1 #HLK2 - lapply (drop_inv_O2 … HLK1) -HLK1 #H destruct - lapply (drop_inv_O2 … HLK2) -HLK2 #H destruct - /2 width=1 by conj/ -| -HL12 -HV12 /3 width=6 by drop_inv_drop1/ -| #H lapply (drop_fwd_Y2 … H) -H - #H elim (ylt_yle_false … H) -H // -] -qed. - -(* Main properties **********************************************************) - -theorem lpx_sn_lpx_sn_alt: ∀R,L1,L2. lpx_sn R L1 L2 → lpx_sn_alt R L1 L2. -#R #L1 #L2 #H elim H -L1 -L2 -/2 width=1 by lpx_sn_alt_atom, lpx_sn_alt_pair/ -qed. - -(* Main inversion lemmas ****************************************************) - -theorem lpx_sn_alt_inv_lpx_sn: ∀R,L1,L2. lpx_sn_alt R L1 L2 → lpx_sn R L1 L2. -#R #L1 elim L1 -L1 -[ #L2 #H lapply (lpx_sn_alt_inv_atom1 … H) -H // -| #L1 #I #V1 #IH #X #H elim (lpx_sn_alt_inv_pair1 … H) -H - #L2 #V2 #HL12 #HV12 #H destruct /3 width=1 by lpx_sn_pair/ -] -qed-. - -(* alternative definition of lpx_sn *****************************************) - -lemma lpx_sn_intro_alt: ∀R,L1,L2. |L1| = |L2| → - (∀I1,I2,K1,K2,V1,V2,i. - ⬇[i] L1 ≡ K1.ⓑ{I1}V1 → ⬇[i] L2 ≡ K2.ⓑ{I2}V2 → - I1 = I2 ∧ R K1 V1 V2 - ) → lpx_sn R L1 L2. -/4 width=4 by lpx_sn_alt_inv_lpx_sn, conj/ qed. - -lemma lpx_sn_inv_alt: ∀R,L1,L2. lpx_sn R L1 L2 → - |L1| = |L2| ∧ - ∀I1,I2,K1,K2,V1,V2,i. - ⬇[i] L1 ≡ K1.ⓑ{I1}V1 → ⬇[i] L2 ≡ K2.ⓑ{I2}V2 → - I1 = I2 ∧ R K1 V1 V2. -#R #L1 #L2 #H lapply (lpx_sn_lpx_sn_alt … H) -H -#H elim H -H /3 width=4 by conj/ -qed-. diff --git a/matita/matita/contribs/lambdadelta/basic_2/substitution/lpx_sn_drop.ma b/matita/matita/contribs/lambdadelta/basic_2/substitution/lpx_sn_drop.ma deleted file mode 100644 index 612f16a37..000000000 --- a/matita/matita/contribs/lambdadelta/basic_2/substitution/lpx_sn_drop.ma +++ /dev/null @@ -1,101 +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/drop_lreq.ma". -include "basic_2/substitution/lpx_sn.ma". - -(* SN POINTWISE EXTENSION OF A CONTEXT-SENSITIVE REALTION FOR TERMS *********) - -(* Properties on dropping ****************************************************) - -lemma lpx_sn_drop_conf: ∀R,L1,L2. lpx_sn R L1 L2 → - ∀I,K1,V1,i. ⬇[i] L1 ≡ K1.ⓑ{I}V1 → - ∃∃K2,V2. ⬇[i] L2 ≡ K2.ⓑ{I}V2 & lpx_sn R K1 K2 & R K1 V1 V2. -#R #L1 #L2 #H elim H -L1 -L2 -[ #I0 #K0 #V0 #i #H elim (drop_inv_atom1 … H) -H #H destruct -| #I #K1 #K2 #V1 #V2 #HK12 #HV12 #IHK12 #I0 #K0 #V0 #i #H elim (drop_inv_O1_pair1 … H) * -H - [ -IHK12 #H1 #H2 destruct /3 width=5 by drop_pair, ex3_2_intro/ - | -HK12 -HV12 #Hi #HK10 elim (IHK12 … HK10) -IHK12 -HK10 - /3 width=5 by drop_drop_lt, ex3_2_intro/ - ] -] -qed-. - -lemma lpx_sn_drop_trans: ∀R,L1,L2. lpx_sn R L1 L2 → - ∀I,K2,V2,i. ⬇[i] L2 ≡ K2.ⓑ{I}V2 → - ∃∃K1,V1. ⬇[i] L1 ≡ K1.ⓑ{I}V1 & lpx_sn R K1 K2 & R K1 V1 V2. -#R #L1 #L2 #H elim H -L1 -L2 -[ #I0 #K0 #V0 #i #H elim (drop_inv_atom1 … H) -H #H destruct -| #I #K1 #K2 #V1 #V2 #HK12 #HV12 #IHK12 #I0 #K0 #V0 #i #H elim (drop_inv_O1_pair1 … H) * -H - [ -IHK12 #H1 #H2 destruct /3 width=5 by drop_pair, ex3_2_intro/ - | -HK12 -HV12 #Hi #HK10 elim (IHK12 … HK10) -IHK12 -HK10 - /3 width=5 by drop_drop_lt, ex3_2_intro/ - ] -] -qed-. - -lemma lpx_sn_deliftable_dropable: ∀R. d_deliftable_sn R → dropable_sn (lpx_sn R). -#R #HR #L1 #K1 #s #l #m #H elim H -L1 -K1 -l -m -[ #l #m #Hm #X #H >(lpx_sn_inv_atom1 … H) -H - /4 width=3 by drop_atom, lpx_sn_atom, ex2_intro/ -| #I #K1 #V1 #X #H elim (lpx_sn_inv_pair1 … H) -H - #L2 #V2 #HL12 #HV12 #H destruct - /3 width=5 by drop_pair, lpx_sn_pair, ex2_intro/ -| #I #L1 #K1 #V1 #m #_ #IHLK1 #X #H elim (lpx_sn_inv_pair1 … H) -H - #L2 #V2 #HL12 #HV12 #H destruct - elim (IHLK1 … HL12) -L1 /3 width=3 by drop_drop, ex2_intro/ -| #I #L1 #K1 #V1 #W1 #l #m #HLK1 #HWV1 #IHLK1 #X #H - elim (lpx_sn_inv_pair1 … H) -H #L2 #V2 #HL12 #HV12 #H destruct - elim (HR … HV12 … HLK1 … HWV1) -V1 - elim (IHLK1 … HL12) -L1 /3 width=5 by drop_skip, lpx_sn_pair, ex2_intro/ -] -qed-. - -lemma lpx_sn_liftable_dedropable: ∀R. (∀L. reflexive ? (R L)) → - d_liftable R → dedropable_sn (lpx_sn R). -#R #H1R #H2R #L1 #K1 #s #l #m #H elim H -L1 -K1 -l -m -[ #l #m #Hm #X #H >(lpx_sn_inv_atom1 … H) -H - /4 width=4 by drop_atom, lpx_sn_atom, ex3_intro/ -| #I #K1 #V1 #X #H elim (lpx_sn_inv_pair1 … H) -H - #K2 #V2 #HK12 #HV12 #H destruct - lapply (lpx_sn_fwd_length … HK12) - #H @(ex3_intro … (K2.ⓑ{I}V2)) (**) (* explicit constructor *) - /3 width=1 by lpx_sn_pair, lreq_O2/ -| #I #L1 #K1 #V1 #m #_ #IHLK1 #K2 #HK12 elim (IHLK1 … HK12) -K1 - /3 width=5 by drop_drop, lreq_pair, lpx_sn_pair, ex3_intro/ -| #I #L1 #K1 #V1 #W1 #l #m #HLK1 #HWV1 #IHLK1 #X #H - elim (lpx_sn_inv_pair1 … H) -H #K2 #W2 #HK12 #HW12 #H destruct - elim (H2R … HW12 … HLK1 … HWV1) -W1 - elim (IHLK1 … HK12) -K1 - /3 width=6 by drop_skip, lreq_succ, lpx_sn_pair, ex3_intro/ -] -qed-. - -fact lpx_sn_dropable_aux: ∀R,L2,K2,s,l,m. ⬇[s, l, m] L2 ≡ K2 → ∀L1. lpx_sn R L1 L2 → - l = 0 → ∃∃K1. ⬇[s, 0, m] L1 ≡ K1 & lpx_sn R K1 K2. -#R #L2 #K2 #s #l #m #H elim H -L2 -K2 -l -m -[ #l #m #Hm #X #H >(lpx_sn_inv_atom2 … H) -H - /4 width=3 by drop_atom, lpx_sn_atom, ex2_intro/ -| #I #K2 #V2 #X #H elim (lpx_sn_inv_pair2 … H) -H - #K1 #V1 #HK12 #HV12 #H destruct - /3 width=5 by drop_pair, lpx_sn_pair, ex2_intro/ -| #I #L2 #K2 #V2 #m #_ #IHLK2 #X #H #_ elim (lpx_sn_inv_pair2 … H) -H - #L1 #V1 #HL12 #HV12 #H destruct - elim (IHLK2 … HL12) -L2 /3 width=3 by drop_drop, ex2_intro/ -| #I #L2 #K2 #V2 #W2 #l #m #_ #_ #_ #L1 #_ #H elim (ysucc_inv_O_dx … H) -] -qed-. - -lemma lpx_sn_dropable: ∀R. dropable_dx (lpx_sn R). -/2 width=5 by lpx_sn_dropable_aux/ qed-. diff --git a/matita/matita/contribs/lambdadelta/basic_2/substitution/lpx_sn_tc.ma b/matita/matita/contribs/lambdadelta/basic_2/substitution/lpx_sn_tc.ma index ef4419780..23eaab6ab 100644 --- a/matita/matita/contribs/lambdadelta/basic_2/substitution/lpx_sn_tc.ma +++ b/matita/matita/contribs/lambdadelta/basic_2/substitution/lpx_sn_tc.ma @@ -54,7 +54,7 @@ lemma TC_lpx_sn_inv_atom2: ∀R,L1. TC … (lpx_sn R) L1 (⋆) → L1 = ⋆. ] qed-. -lemma TC_lpx_sn_inv_pair2: ∀R. s_rs_transitive … R (λ_. lpx_sn R) → +lemma TC_lpx_sn_inv_pair2: ∀R. c_rs_transitive … R (λ_. lpx_sn R) → ∀I,L1,K2,V2. TC … (lpx_sn R) L1 (K2.ⓑ{I}V2) → ∃∃K1,V1. TC … (lpx_sn R) K1 K2 & LTC … R K1 V1 V2 & L1 = K1. ⓑ{I} V1. #R #HR #I #L1 #K2 #V2 #H @(TC_ind_dx … L1 H) -L1 @@ -65,7 +65,7 @@ lemma TC_lpx_sn_inv_pair2: ∀R. s_rs_transitive … R (λ_. lpx_sn R) → ] qed-. -lemma TC_lpx_sn_ind: ∀R. s_rs_transitive … R (λ_. lpx_sn R) → +lemma TC_lpx_sn_ind: ∀R. c_rs_transitive … R (λ_. lpx_sn R) → ∀S:relation lenv. S (⋆) (⋆) → ( ∀I,K1,K2,V1,V2. @@ -88,7 +88,7 @@ lemma TC_lpx_sn_inv_atom1: ∀R,L2. TC … (lpx_sn R) (⋆) L2 → L2 = ⋆. ] qed-. -fact TC_lpx_sn_inv_pair1_aux: ∀R. s_rs_transitive … R (λ_. lpx_sn R) → +fact TC_lpx_sn_inv_pair1_aux: ∀R. c_rs_transitive … R (λ_. lpx_sn R) → ∀L1,L2. TC … (lpx_sn R) L1 L2 → ∀I,K1,V1. L1 = K1.ⓑ{I}V1 → ∃∃K2,V2. TC … (lpx_sn R) K1 K2 & LTC … R K1 V1 V2 & L2 = K2. ⓑ{I} V2. @@ -98,12 +98,12 @@ fact TC_lpx_sn_inv_pair1_aux: ∀R. s_rs_transitive … R (λ_. lpx_sn R) → ] qed-. -lemma TC_lpx_sn_inv_pair1: ∀R. s_rs_transitive … R (λ_. lpx_sn R) → +lemma TC_lpx_sn_inv_pair1: ∀R. c_rs_transitive … R (λ_. lpx_sn R) → ∀I,K1,L2,V1. TC … (lpx_sn R) (K1.ⓑ{I}V1) L2 → ∃∃K2,V2. TC … (lpx_sn R) K1 K2 & LTC … R K1 V1 V2 & L2 = K2. ⓑ{I} V2. /2 width=3 by TC_lpx_sn_inv_pair1_aux/ qed-. -lemma TC_lpx_sn_inv_lpx_sn_LTC: ∀R. s_rs_transitive … R (λ_. lpx_sn R) → +lemma TC_lpx_sn_inv_lpx_sn_LTC: ∀R. c_rs_transitive … R (λ_. lpx_sn R) → ∀L1,L2. TC … (lpx_sn R) L1 L2 → lpx_sn (LTC … R) L1 L2. /3 width=4 by TC_lpx_sn_ind, lpx_sn_pair/ qed-.