From: Ferruccio Guidi Date: Mon, 7 Apr 2014 19:53:54 +0000 (+0000) Subject: some resuls on pointwise extensions (all of them are now in the X-Git-Tag: make_still_working~941 X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=commitdiff_plain;h=a76f56fdad6348b167376093920650379c9936d4;p=helm.git some resuls on pointwise extensions (all of them are now in the "relocation" component --- diff --git a/matita/matita/contribs/lambdadelta/basic_2/computation/lprs.ma b/matita/matita/contribs/lambdadelta/basic_2/computation/lprs.ma index 6e8431959..c3d7203df 100644 --- a/matita/matita/contribs/lambdadelta/basic_2/computation/lprs.ma +++ b/matita/matita/contribs/lambdadelta/basic_2/computation/lprs.ma @@ -13,7 +13,7 @@ (**************************************************************************) include "basic_2/notation/relations/predsnstar_3.ma". -include "basic_2/grammar/lpx_sn_tc.ma". +include "basic_2/relocation/lpx_sn_tc.ma". include "basic_2/reduction/lpr.ma". (* SN PARALLEL COMPUTATION ON LOCAL ENVIRONMENTS ****************************) diff --git a/matita/matita/contribs/lambdadelta/basic_2/etc/llpx_sn/lift_neg.etc b/matita/matita/contribs/lambdadelta/basic_2/etc/llpx_sn/lift_neg.etc deleted file mode 100644 index 220748ed3..000000000 --- a/matita/matita/contribs/lambdadelta/basic_2/etc/llpx_sn/lift_neg.etc +++ /dev/null @@ -1,60 +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/relocation/lift.ma". - -(* BASIC TERM RELOCATION ****************************************************) - -(* Properties on negated basic relocation ***********************************) - -lemma nlift_lref_be_SO: ∀X,i. ⇧[i, 1] X ≡ #i → ⊥. -/2 width=7 by lift_inv_lref2_be/ qed-. - -lemma nlift_bind_sn: ∀W,d,e. (∀V. ⇧[d, e] V ≡ W → ⊥) → - ∀a,I,U. (∀X. ⇧[d, e] X ≡ ⓑ{a,I}W.U → ⊥). -#W #d #e #HW #a #I #U #X #H elim (lift_inv_bind2 … H) -H /2 width=2 by/ -qed-. - -lemma nlift_bind_dx: ∀U,d,e. (∀T. ⇧[d+1, e] T ≡ U → ⊥) → - ∀a,I,W. (∀X. ⇧[d, e] X ≡ ⓑ{a,I}W.U → ⊥). -#U #d #e #HU #a #I #W #X #H elim (lift_inv_bind2 … H) -H /2 width=2 by/ -qed-. - -lemma nlift_flat_sn: ∀W,d,e. (∀V. ⇧[d, e] V ≡ W → ⊥) → - ∀I,U. (∀X. ⇧[d, e] X ≡ ⓕ{I}W.U → ⊥). -#W #d #e #HW #I #U #X #H elim (lift_inv_flat2 … H) -H /2 width=2 by/ -qed-. - -lemma nlift_flat_dx: ∀U,d,e. (∀T. ⇧[d, e] T ≡ U → ⊥) → - ∀I,W. (∀X. ⇧[d, e] X ≡ ⓕ{I}W.U → ⊥). -#U #d #e #HU #I #W #X #H elim (lift_inv_flat2 … H) -H /2 width=2 by/ -qed-. - -(* Inversion lemmas on negated basic relocation *****************************) - -lemma nlift_inv_bind: ∀a,I,W,U,d,e. (∀X. ⇧[d, e] X ≡ ⓑ{a,I}W.U → ⊥) → - (∀V. ⇧[d, e] V ≡ W → ⊥) ∨ (∀T. ⇧[d+1, e] T ≡ U → ⊥). -#a #I #W #U #d #e #H elim (is_lift_dec W d e) -[ * /4 width=2 by lift_bind, or_intror/ -| /4 width=2 by ex_intro, or_introl/ -] -qed-. - -lemma nlift_inv_flat: ∀I,W,U,d,e. (∀X. ⇧[d, e] X ≡ ⓕ{I}W.U → ⊥) → - (∀V. ⇧[d, e] V ≡ W → ⊥) ∨ (∀T. ⇧[d, e] T ≡ U → ⊥). -#I #W #U #d #e #H elim (is_lift_dec W d e) -[ * /4 width=2 by lift_flat, or_intror/ -| /4 width=2 by ex_intro, or_introl/ -] -qed-. diff --git a/matita/matita/contribs/lambdadelta/basic_2/etc/llpx_sn/lleq_alt.etc b/matita/matita/contribs/lambdadelta/basic_2/etc/llpx_sn/lleq_alt.etc deleted file mode 100644 index ccf131d5a..000000000 --- a/matita/matita/contribs/lambdadelta/basic_2/etc/llpx_sn/lleq_alt.etc +++ /dev/null @@ -1,41 +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/relocation/llpx_sn_alt.ma". -include "basic_2/relocation/lleq.ma". - -(* LAZY EQUIVALENCE FOR LOCAL ENVIRONMENTS **********************************) - -(* Alternative definition ***************************************************) - -theorem lleq_intro_alt: ∀L1,L2,T,d. |L1| = |L2| → - (∀I1,I2,K1,K2,V1,V2,i. d ≤ yinj i → (∀U. ⇧[i, 1] U ≡ T → ⊥) → - ⇩[i] L1 ≡ K1.ⓑ{I1}V1 → ⇩[i] L2 ≡ K2.ⓑ{I2}V2 → - ∧∧ I1 = I2 & V1 = V2 & K1 ⋕[V1, 0] K2 - ) → L1 ⋕[T, d] L2. -#L1 #L2 #T #d #HL12 #IH @llpx_sn_intro_alt // -HL12 -#I1 #I2 #K1 #K2 #HLK1 #HLK2 #i #Hid #HnT #HLK1 #HLK2 -elim (IH … HnT HLK1 HLK2) -IH -HnT -HLK1 -HLK2 /2 width=1 by and3_intro/ -qed. - -theorem lleq_fwd_alt: ∀L1,L2,T,d. L1 ⋕[T, d] L2 → - |L1| = |L2| ∧ - ∀I1,I2,K1,K2,V1,V2,i. d ≤ yinj i → (∀U. ⇧[i, 1] U ≡ T → ⊥) → - ⇩[i] L1 ≡ K1.ⓑ{I1}V1 → ⇩[i] L2 ≡ K2.ⓑ{I2}V2 → - ∧∧ I1 = I2 & V1 = V2 & K1 ⋕[V1, 0] K2. -#L1 #L2 #T #d #H elim (llpx_sn_fwd_alt … H) -H -#HL12 #IH @conj // -#I1 #I2 #K1 #K2 #HLK1 #HLK2 #i #Hid #HnT #HLK1 #HLK2 -elim (IH … HnT HLK1 HLK2) -IH -HnT -HLK1 -HLK2 /2 width=1 by and3_intro/ -qed-. diff --git a/matita/matita/contribs/lambdadelta/basic_2/etc/llpx_sn/llpx_sn_alt.etc b/matita/matita/contribs/lambdadelta/basic_2/etc/llpx_sn/llpx_sn_alt.etc deleted file mode 100644 index 4356553ff..000000000 --- a/matita/matita/contribs/lambdadelta/basic_2/etc/llpx_sn/llpx_sn_alt.etc +++ /dev/null @@ -1,250 +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/relocation/lift_neg.ma". -include "basic_2/relocation/ldrop_ldrop.ma". -include "basic_2/relocation/llpx_sn.ma". - -(* LAZY SN POINTWISE EXTENSION OF A CONTEXT-SENSITIVE REALTION FOR TERMS ****) - -(* alternative definition of llpx_sn_alt *) -inductive llpx_sn_alt (R:relation3 lenv term term): relation4 ynat term lenv lenv ≝ -| llpx_sn_alt_intro: ∀L1,L2,T,d. - (∀I1,I2,K1,K2,V1,V2,i. d ≤ yinj i → (∀U. ⇧[i, 1] U ≡ T → ⊥) → - ⇩[i] L1 ≡ K1.ⓑ{I1}V1 → ⇩[i] L2 ≡ K2.ⓑ{I2}V2 → I1 = I2 ∧ R K1 V1 V2 - ) → - (∀I1,I2,K1,K2,V1,V2,i. d ≤ yinj i → (∀U. ⇧[i, 1] U ≡ T → ⊥) → - ⇩[i] L1 ≡ K1.ⓑ{I1}V1 → ⇩[i] L2 ≡ K2.ⓑ{I2}V2 → llpx_sn_alt R 0 V1 K1 K2 - ) → |L1| = |L2| → llpx_sn_alt R d T L1 L2 -. - -(* Basic forward lemmas ******************************************************) - -lemma llpx_sn_alt_fwd_gen: ∀R,L1,L2,T,d. llpx_sn_alt R d T L1 L2 → - |L1| = |L2| ∧ - ∀I1,I2,K1,K2,V1,V2,i. d ≤ yinj i → (∀U. ⇧[i, 1] U ≡ T → ⊥) → - ⇩[i] L1 ≡ K1.ⓑ{I1}V1 → ⇩[i] L2 ≡ K2.ⓑ{I2}V2 → - ∧∧ I1 = I2 & R K1 V1 V2 & llpx_sn_alt R 0 V1 K1 K2. -#R #L1 #L2 #T #d * -L1 -L2 -T -d -#L1 #L2 #T #d #IH1 #IH2 #HL12 @conj // -#I1 #I2 #K1 #K2 #HLK1 #HLK2 #i #Hid #HnT #HLK1 #HLK2 -elim (IH1 … HnT HLK1 HLK2) -IH1 /4 width=8 by and3_intro/ -qed-. - -lemma llpx_sn_alt_fwd_length: ∀R,L1,L2,T,d. llpx_sn_alt R d T L1 L2 → |L1| = |L2|. -#R #L1 #L2 #T #d * -L1 -L2 -T -d // -qed-. - -fact llpx_sn_alt_fwd_lref_aux: ∀R,L1,L2,X,d. llpx_sn_alt R d X L1 L2 → ∀i. X = #i → - ∨∨ |L1| ≤ i ∧ |L2| ≤ i - | yinj i < d - | ∃∃I,K1,K2,V1,V2. ⇩[i] L1 ≡ K1.ⓑ{I}V1 & - ⇩[i] L2 ≡ K2.ⓑ{I}V2 & - llpx_sn_alt R (yinj 0) V1 K1 K2 & - R K1 V1 V2 & d ≤ yinj i. -#R #L1 #L2 #X #d * -L1 -L2 -X -d -#L1 #L2 #X #d #H1X #H2X #HL12 #i #H destruct -elim (lt_or_ge i (|L1|)) /3 width=1 by or3_intro0, conj/ -elim (ylt_split i d) /3 width=1 by or3_intro1/ -#Hdi #HL1 elim (ldrop_O1_lt … HL1) #I1 #K1 #V1 #HLK1 -elim (ldrop_O1_lt L2 i) // #I2 #K2 #V2 #HLK2 -elim (H1X … HLK1 HLK2) -H1X /2 width=3 by nlift_lref_be_SO/ #H #HV12 destruct -lapply (H2X … HLK1 HLK2) -H2X /2 width=3 by nlift_lref_be_SO/ -/3 width=9 by or3_intro2, ex5_5_intro/ -qed-. - -lemma llpx_sn_alt_fwd_lref: ∀R,L1,L2,d,i. llpx_sn_alt R d (#i) L1 L2 → - ∨∨ |L1| ≤ i ∧ |L2| ≤ i - | yinj i < d - | ∃∃I,K1,K2,V1,V2. ⇩[i] L1 ≡ K1.ⓑ{I}V1 & - ⇩[i] L2 ≡ K2.ⓑ{I}V2 & - llpx_sn_alt R (yinj 0) V1 K1 K2 & - R K1 V1 V2 & d ≤ yinj i. -/2 width=3 by llpx_sn_alt_fwd_lref_aux/ qed-. - -(* Basic inversion lemmas ****************************************************) - -fact llpx_sn_alt_inv_flat_aux: ∀R,L1,L2,X,d. llpx_sn_alt R d X L1 L2 → - ∀I,V,T. X = ⓕ{I}V.T → - llpx_sn_alt R d V L1 L2 ∧ llpx_sn_alt R d T L1 L2. -#R #L1 #L2 #X #d * -L1 -L2 -X -d -#L1 #L2 #X #d #H1X #H2X #HL12 -#I #V #T #H destruct -@conj @llpx_sn_alt_intro // -HL12 -/4 width=8 by nlift_flat_sn, nlift_flat_dx/ -qed-. - -lemma llpx_sn_alt_inv_flat: ∀R,I,L1,L2,V,T,d. llpx_sn_alt R d (ⓕ{I}V.T) L1 L2 → - llpx_sn_alt R d V L1 L2 ∧ llpx_sn_alt R d T L1 L2. -/2 width=4 by llpx_sn_alt_inv_flat_aux/ qed-. - -fact llpx_sn_alt_inv_bind_aux: ∀R,L1,L2,X,d. llpx_sn_alt R d X L1 L2 → - ∀a,I,V,T. X = ⓑ{a,I}V.T → - llpx_sn_alt R d V L1 L2 ∧ llpx_sn_alt R (⫯d) T (L1.ⓑ{I}V) (L2.ⓑ{I}V). -#R #L1 #L2 #X #d * -L1 -L2 -X -d -#L1 #L2 #X #d #H1X #H2X #HL12 -#a #I #V #T #H destruct -@conj @llpx_sn_alt_intro [3,6: normalize /2 width=1 by eq_f2/ ] -HL12 -#I1 #I2 #K1 #K2 #W1 #W2 #i #Hdi #H #HLK1 #HLK2 -[1,2: /4 width=9 by nlift_bind_sn/ ] -lapply (yle_inv_succ1 … Hdi) -Hdi * #Hdi #Hi -lapply (ldrop_inv_drop1_lt … HLK1 ?) -HLK1 /2 width=1 by ylt_O/ #HLK1 -lapply (ldrop_inv_drop1_lt … HLK2 ?) -HLK2 /2 width=1 by ylt_O/ #HLK2 -[ @(H1X … HLK1 HLK2) | @(H2X … HLK1 HLK2) ] // -I1 -I2 -L1 -L2 -K1 -K2 -W1 -W2 -@nlift_bind_dx (lpx_sn_inv_atom1 … H1) -X1 - >(lpx_sn_inv_atom1 … H2) -X2 /2 width=3/ -| #L0 #I #V0 #Hn #X1 #H1 #X2 #H2 destruct - elim (lpx_sn_inv_pair1 … H1) -H1 #L1 #V1 #HL01 #HV01 #H destruct - elim (lpx_sn_inv_pair1 … H2) -H2 #L2 #V2 #HL02 #HV02 #H destruct - elim (IH … HL01 … HL02) -IH normalize // #L #HL1 #HL2 - elim (HR12 … HV01 … HV02 … HL01 … HL02) -L0 -V0 /3 width=5/ -] -qed-. diff --git a/matita/matita/contribs/lambdadelta/basic_2/grammar/lpx_sn_tc.ma b/matita/matita/contribs/lambdadelta/basic_2/grammar/lpx_sn_tc.ma deleted file mode 100644 index 6dc76e174..000000000 --- a/matita/matita/contribs/lambdadelta/basic_2/grammar/lpx_sn_tc.ma +++ /dev/null @@ -1,119 +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/lpx_sn.ma". - -(* SN POINTWISE EXTENSION OF A CONTEXT-SENSITIVE REALTION FOR TERMS *********) - -(* Properties on transitive_closure *****************************************) - -lemma TC_lpx_sn_pair_refl: ∀R. (∀L. reflexive … (R L)) → - ∀L1,L2. TC … (lpx_sn R) L1 L2 → - ∀I,V. TC … (lpx_sn R) (L1. ⓑ{I} V) (L2. ⓑ{I} V). -#R #HR #L1 #L2 #H @(TC_star_ind … L2 H) -L2 -[ /2 width=1 by lpx_sn_refl/ -| /3 width=1 by TC_reflexive, lpx_sn_refl/ -| /3 width=5 by lpx_sn_pair, step/ -] -qed-. - -lemma TC_lpx_sn_pair: ∀R. (∀L. reflexive … (R L)) → - ∀I,L1,L2. TC … (lpx_sn R) L1 L2 → - ∀V1,V2. LTC … R L1 V1 V2 → - TC … (lpx_sn R) (L1. ⓑ{I} V1) (L2. ⓑ{I} V2). -#R #HR #I #L1 #L2 #HL12 #V1 #V2 #H @(TC_star_ind_dx … V1 H) -V1 // -[ /2 width=1 by TC_lpx_sn_pair_refl/ -| /4 width=3 by TC_strap, lpx_sn_pair, lpx_sn_refl/ -] -qed-. - -lemma lpx_sn_LTC_TC_lpx_sn: ∀R. (∀L. reflexive … (R L)) → - ∀L1,L2. lpx_sn (LTC … R) L1 L2 → - TC … (lpx_sn R) L1 L2. -#R #HR #L1 #L2 #H elim H -L1 -L2 -/2 width=1 by TC_lpx_sn_pair, lpx_sn_atom, inj/ -qed-. - -(* Inversion lemmas on transitive closure ***********************************) - -lemma TC_lpx_sn_inv_atom2: ∀R,L1. TC … (lpx_sn R) L1 (⋆) → L1 = ⋆. -#R #L1 #H @(TC_ind_dx … L1 H) -L1 -[ /2 width=2 by lpx_sn_inv_atom2/ -| #L1 #L #HL1 #_ #IHL2 destruct /2 width=2 by lpx_sn_inv_atom2/ -] -qed-. - -lemma TC_lpx_sn_inv_pair2: ∀R. s_rs_transitive … R (λ_. lpx_sn R) → - ∀I,L1,K2,V2. TC … (lpx_sn R) L1 (K2.ⓑ{I}V2) → - ∃∃K1,V1. TC … (lpx_sn R) K1 K2 & LTC … R K1 V1 V2 & L1 = K1. ⓑ{I} V1. -#R #HR #I #L1 #K2 #V2 #H @(TC_ind_dx … L1 H) -L1 -[ #L1 #H elim (lpx_sn_inv_pair2 … H) -H /3 width=5 by inj, ex3_2_intro/ -| #L1 #L #HL1 #_ * #K #V #HK2 #HV2 #H destruct - elim (lpx_sn_inv_pair2 … HL1) -HL1 #K1 #V1 #HK1 #HV1 #H destruct - lapply (HR … HV2 … HK1) -HR -HV2 /3 width=5 by TC_strap, ex3_2_intro/ -] -qed-. - -lemma TC_lpx_sn_ind: ∀R. s_rs_transitive … R (λ_. lpx_sn R) → - ∀S:relation lenv. - S (⋆) (⋆) → ( - ∀I,K1,K2,V1,V2. - TC … (lpx_sn R) K1 K2 → LTC … R K1 V1 V2 → - S K1 K2 → S (K1.ⓑ{I}V1) (K2.ⓑ{I}V2) - ) → - ∀L2,L1. TC … (lpx_sn R) L1 L2 → S L1 L2. -#R #HR #S #IH1 #IH2 #L2 elim L2 -L2 -[ #X #H >(TC_lpx_sn_inv_atom2 … H) -X // -| #L2 #I #V2 #IHL2 #X #H - elim (TC_lpx_sn_inv_pair2 … H) // -H -HR - #L1 #V1 #HL12 #HV12 #H destruct /3 width=1 by/ -] -qed-. - -lemma TC_lpx_sn_inv_atom1: ∀R,L2. TC … (lpx_sn R) (⋆) L2 → L2 = ⋆. -#R #L2 #H elim H -L2 -[ /2 width=2 by lpx_sn_inv_atom1/ -| #L #L2 #_ #HL2 #IHL1 destruct /2 width=2 by lpx_sn_inv_atom1/ -] -qed-. - -fact TC_lpx_sn_inv_pair1_aux: ∀R. s_rs_transitive … R (λ_. lpx_sn R) → - ∀L1,L2. TC … (lpx_sn R) L1 L2 → - ∀I,K1,V1. L1 = K1.ⓑ{I}V1 → - ∃∃K2,V2. TC … (lpx_sn R) K1 K2 & LTC … R K1 V1 V2 & L2 = K2. ⓑ{I} V2. -#R #HR #L1 #L2 #H @(TC_lpx_sn_ind … H) // -HR -L1 -L2 -[ #J #K #W #H destruct -| #I #L1 #L2 #V1 #V2 #HL12 #HV12 #_ #J #K #W #H destruct /2 width=5 by ex3_2_intro/ -] -qed-. - -lemma TC_lpx_sn_inv_pair1: ∀R. s_rs_transitive … R (λ_. lpx_sn R) → - ∀I,K1,L2,V1. TC … (lpx_sn R) (K1.ⓑ{I}V1) L2 → - ∃∃K2,V2. TC … (lpx_sn R) K1 K2 & LTC … R 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) → - ∀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-. - -(* Forward lemmas on transitive closure *************************************) - -lemma TC_lpx_sn_fwd_length: ∀R,L1,L2. TC … (lpx_sn R) L1 L2 → |L1| = |L2|. -#R #L1 #L2 #H elim H -L2 -[ #L2 #HL12 >(lpx_sn_fwd_length … HL12) -HL12 // -| #L #L2 #_ #HL2 #IHL1 - >IHL1 -L1 >(lpx_sn_fwd_length … HL2) -HL2 // -] -qed-. diff --git a/matita/matita/contribs/lambdadelta/basic_2/notation/relations/lazyor_4.ma b/matita/matita/contribs/lambdadelta/basic_2/notation/relations/lazyor_4.ma new file mode 100644 index 000000000..cc97e6bbe --- /dev/null +++ b/matita/matita/contribs/lambdadelta/basic_2/notation/relations/lazyor_4.ma @@ -0,0 +1,19 @@ +(**************************************************************************) +(* ___ *) +(* ||M|| *) +(* ||A|| A project by Andrea Asperti *) +(* ||T|| *) +(* ||I|| Developers: *) +(* ||T|| The HELM team. *) +(* ||A|| http://helm.cs.unibo.it *) +(* \ / *) +(* \ / This file is distributed under the terms of the *) +(* v GNU General Public License Version 2 *) +(* *) +(**************************************************************************) + +(* NOTATION FOR THE FORMAL SYSTEM λδ ****************************************) + +notation "hvbox( L1 ⩖ break [ term 46 T ] break term 46 L2 ≡ break term 46 L )" + non associative with precedence 45 + for @{ 'LazyOr $L1 $T $L2 $L }. diff --git a/matita/matita/contribs/lambdadelta/basic_2/reduction/lpr.ma b/matita/matita/contribs/lambdadelta/basic_2/reduction/lpr.ma index 7bcf22df5..01966eefb 100644 --- a/matita/matita/contribs/lambdadelta/basic_2/reduction/lpr.ma +++ b/matita/matita/contribs/lambdadelta/basic_2/reduction/lpr.ma @@ -13,7 +13,7 @@ (**************************************************************************) include "basic_2/notation/relations/predsn_3.ma". -include "basic_2/grammar/lpx_sn.ma". +include "basic_2/relocation/lpx_sn.ma". include "basic_2/reduction/cpr.ma". (* SN PARALLEL REDUCTION FOR LOCAL ENVIRONMENTS *****************************) diff --git a/matita/matita/contribs/lambdadelta/basic_2/reduction/lpr_ldrop.ma b/matita/matita/contribs/lambdadelta/basic_2/reduction/lpr_ldrop.ma index 4156df6ea..c8443e08b 100644 --- a/matita/matita/contribs/lambdadelta/basic_2/reduction/lpr_ldrop.ma +++ b/matita/matita/contribs/lambdadelta/basic_2/reduction/lpr_ldrop.ma @@ -12,8 +12,8 @@ (* *) (**************************************************************************) +include "basic_2/relocation/lpx_sn_ldrop.ma". include "basic_2/relocation/fquq_alt.ma". -include "basic_2/relocation/ldrop_lpx_sn.ma". include "basic_2/reduction/cpr_lift.ma". include "basic_2/reduction/lpr.ma". diff --git a/matita/matita/contribs/lambdadelta/basic_2/reduction/lpr_lpr.ma b/matita/matita/contribs/lambdadelta/basic_2/reduction/lpr_lpr.ma index 7b65286ab..2f653c61b 100644 --- a/matita/matita/contribs/lambdadelta/basic_2/reduction/lpr_lpr.ma +++ b/matita/matita/contribs/lambdadelta/basic_2/reduction/lpr_lpr.ma @@ -12,7 +12,7 @@ (* *) (**************************************************************************) -include "basic_2/grammar/lpx_sn_lpx_sn.ma". +include "basic_2/relocation/lpx_sn_lpx_sn.ma". include "basic_2/substitution/fqup.ma". include "basic_2/reduction/lpr_ldrop.ma". diff --git a/matita/matita/contribs/lambdadelta/basic_2/relocation/ldrop_lpx_sn.ma b/matita/matita/contribs/lambdadelta/basic_2/relocation/ldrop_lpx_sn.ma deleted file mode 100644 index c392bf54c..000000000 --- a/matita/matita/contribs/lambdadelta/basic_2/relocation/ldrop_lpx_sn.ma +++ /dev/null @@ -1,104 +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/lpx_sn.ma". -include "basic_2/relocation/ldrop_leq.ma". - -(* DROPPING *****************************************************************) - -(* Properties on sn pointwise extension *************************************) - -lemma lpx_sn_ldrop_conf: ∀R,L1,L2. lpx_sn R L1 L2 → - ∀I,K1,V1,i. ⇩[i] L1 ≡ K1.ⓑ{I}V1 → - ∃∃K2,V2. ⇩[i] L2 ≡ K2.ⓑ{I}V2 & lpx_sn R K1 K2 & R K1 V1 V2. -#R #L1 #L2 #H elim H -L1 -L2 -[ #I0 #K0 #V0 #i #H elim (ldrop_inv_atom1 … H) -H #H destruct -| #I #K1 #K2 #V1 #V2 #HK12 #HV12 #IHK12 #I0 #K0 #V0 #i #H elim (ldrop_inv_O1_pair1 … H) * -H - [ -IHK12 #H1 #H2 destruct /3 width=5 by ldrop_pair, ex3_2_intro/ - | -HK12 -HV12 #Hi #HK10 elim (IHK12 … HK10) -IHK12 -HK10 - /3 width=5 by ldrop_drop_lt, ex3_2_intro/ - ] -] -qed-. - -lemma lpx_sn_ldrop_trans: ∀R,L1,L2. lpx_sn R L1 L2 → - ∀I,K2,V2,i. ⇩[i] L2 ≡ K2.ⓑ{I}V2 → - ∃∃K1,V1. ⇩[i] L1 ≡ K1.ⓑ{I}V1 & lpx_sn R K1 K2 & R K1 V1 V2. -#R #L1 #L2 #H elim H -L1 -L2 -[ #I0 #K0 #V0 #i #H elim (ldrop_inv_atom1 … H) -H #H destruct -| #I #K1 #K2 #V1 #V2 #HK12 #HV12 #IHK12 #I0 #K0 #V0 #i #H elim (ldrop_inv_O1_pair1 … H) * -H - [ -IHK12 #H1 #H2 destruct /3 width=5 by ldrop_pair, ex3_2_intro/ - | -HK12 -HV12 #Hi #HK10 elim (IHK12 … HK10) -IHK12 -HK10 - /3 width=5 by ldrop_drop_lt, ex3_2_intro/ - ] -] -qed-. - -lemma lpx_sn_deliftable_dropable: ∀R. l_deliftable_sn R → dropable_sn (lpx_sn R). -#R #HR #L1 #K1 #s #d #e #H elim H -L1 -K1 -d -e -[ #d #e #He #X #H >(lpx_sn_inv_atom1 … H) -H - /4 width=3 by ldrop_atom, lpx_sn_atom, ex2_intro/ -| #I #K1 #V1 #X #H elim (lpx_sn_inv_pair1 … H) -H - #L2 #V2 #HL12 #HV12 #H destruct - /3 width=5 by ldrop_pair, lpx_sn_pair, ex2_intro/ -| #I #L1 #K1 #V1 #e #_ #IHLK1 #X #H elim (lpx_sn_inv_pair1 … H) -H - #L2 #V2 #HL12 #HV12 #H destruct - elim (IHLK1 … HL12) -L1 /3 width=3 by ldrop_drop, ex2_intro/ -| #I #L1 #K1 #V1 #W1 #d #e #HLK1 #HWV1 #IHLK1 #X #H - elim (lpx_sn_inv_pair1 … H) -H #L2 #V2 #HL12 #HV12 #H destruct - elim (HR … HV12 … HLK1 … HWV1) -V1 - elim (IHLK1 … HL12) -L1 /3 width=5 by ldrop_skip, lpx_sn_pair, ex2_intro/ -] -qed-. - -lemma lpx_sn_liftable_dedropable: ∀R. (∀L. reflexive ? (R L)) → - l_liftable R → dedropable_sn (lpx_sn R). -#R #H1R #H2R #L1 #K1 #s #d #e #H elim H -L1 -K1 -d -e -[ #d #e #He #X #H >(lpx_sn_inv_atom1 … H) -H - /4 width=4 by ldrop_atom, lpx_sn_atom, ex3_intro/ -| #I #K1 #V1 #X #H elim (lpx_sn_inv_pair1 … H) -H - #K2 #V2 #HK12 #HV12 #H destruct - lapply (lpx_sn_fwd_length … HK12) - #H @(ex3_intro … (K2.ⓑ{I}V2)) (**) (* explicit constructor *) - /3 width=1 by lpx_sn_pair, monotonic_le_plus_l/ - @leq_O2 normalize // -| #I #L1 #K1 #V1 #e #_ #IHLK1 #K2 #HK12 elim (IHLK1 … HK12) -K1 - /3 width=5 by ldrop_drop, leq_pair, lpx_sn_pair, ex3_intro/ -| #I #L1 #K1 #V1 #W1 #d #e #HLK1 #HWV1 #IHLK1 #X #H - elim (lpx_sn_inv_pair1 … H) -H #K2 #W2 #HK12 #HW12 #H destruct - elim (lift_total W2 d e) #V2 #HWV2 - lapply (H2R … HW12 … HLK1 … HWV1 … HWV2) -W1 - elim (IHLK1 … HK12) -K1 - /3 width=6 by ldrop_skip, leq_succ, lpx_sn_pair, ex3_intro/ -] -qed-. - -fact lpx_sn_dropable_aux: ∀R,L2,K2,s,d,e. ⇩[s, d, e] L2 ≡ K2 → ∀L1. lpx_sn R L1 L2 → - d = 0 → ∃∃K1. ⇩[s, 0, e] L1 ≡ K1 & lpx_sn R K1 K2. -#R #L2 #K2 #s #d #e #H elim H -L2 -K2 -d -e -[ #d #e #He #X #H >(lpx_sn_inv_atom2 … H) -H - /4 width=3 by ldrop_atom, lpx_sn_atom, ex2_intro/ -| #I #K2 #V2 #X #H elim (lpx_sn_inv_pair2 … H) -H - #K1 #V1 #HK12 #HV12 #H destruct - /3 width=5 by ldrop_pair, lpx_sn_pair, ex2_intro/ -| #I #L2 #K2 #V2 #e #_ #IHLK2 #X #H #_ elim (lpx_sn_inv_pair2 … H) -H - #L1 #V1 #HL12 #HV12 #H destruct - elim (IHLK2 … HL12) -L2 /3 width=3 by ldrop_drop, ex2_intro/ -| #I #L2 #K2 #V2 #W2 #d #e #_ #_ #_ #L1 #_ - (lpx_sn_inv_atom1 … H) -H + /4 width=3 by ldrop_atom, lpx_sn_atom, ex2_intro/ +| #I #K1 #V1 #X #H elim (lpx_sn_inv_pair1 … H) -H + #L2 #V2 #HL12 #HV12 #H destruct + /3 width=5 by ldrop_pair, lpx_sn_pair, ex2_intro/ +| #I #L1 #K1 #V1 #e #_ #IHLK1 #X #H elim (lpx_sn_inv_pair1 … H) -H + #L2 #V2 #HL12 #HV12 #H destruct + elim (IHLK1 … HL12) -L1 /3 width=3 by ldrop_drop, ex2_intro/ +| #I #L1 #K1 #V1 #W1 #d #e #HLK1 #HWV1 #IHLK1 #X #H + elim (lpx_sn_inv_pair1 … H) -H #L2 #V2 #HL12 #HV12 #H destruct + elim (HR … HV12 … HLK1 … HWV1) -V1 + elim (IHLK1 … HL12) -L1 /3 width=5 by ldrop_skip, lpx_sn_pair, ex2_intro/ +] +qed-. + +lemma lpx_sn_liftable_dedropable: ∀R. (∀L. reflexive ? (R L)) → + l_liftable R → dedropable_sn (lpx_sn R). +#R #H1R #H2R #L1 #K1 #s #d #e #H elim H -L1 -K1 -d -e +[ #d #e #He #X #H >(lpx_sn_inv_atom1 … H) -H + /4 width=4 by ldrop_atom, lpx_sn_atom, ex3_intro/ +| #I #K1 #V1 #X #H elim (lpx_sn_inv_pair1 … H) -H + #K2 #V2 #HK12 #HV12 #H destruct + lapply (lpx_sn_fwd_length … HK12) + #H @(ex3_intro … (K2.ⓑ{I}V2)) (**) (* explicit constructor *) + /3 width=1 by lpx_sn_pair, monotonic_le_plus_l/ + @leq_O2 normalize // +| #I #L1 #K1 #V1 #e #_ #IHLK1 #K2 #HK12 elim (IHLK1 … HK12) -K1 + /3 width=5 by ldrop_drop, leq_pair, lpx_sn_pair, ex3_intro/ +| #I #L1 #K1 #V1 #W1 #d #e #HLK1 #HWV1 #IHLK1 #X #H + elim (lpx_sn_inv_pair1 … H) -H #K2 #W2 #HK12 #HW12 #H destruct + elim (lift_total W2 d e) #V2 #HWV2 + lapply (H2R … HW12 … HLK1 … HWV1 … HWV2) -W1 + elim (IHLK1 … HK12) -K1 + /3 width=6 by ldrop_skip, leq_succ, lpx_sn_pair, ex3_intro/ +] +qed-. + +fact lpx_sn_dropable_aux: ∀R,L2,K2,s,d,e. ⇩[s, d, e] L2 ≡ K2 → ∀L1. lpx_sn R L1 L2 → + d = 0 → ∃∃K1. ⇩[s, 0, e] L1 ≡ K1 & lpx_sn R K1 K2. +#R #L2 #K2 #s #d #e #H elim H -L2 -K2 -d -e +[ #d #e #He #X #H >(lpx_sn_inv_atom2 … H) -H + /4 width=3 by ldrop_atom, lpx_sn_atom, ex2_intro/ +| #I #K2 #V2 #X #H elim (lpx_sn_inv_pair2 … H) -H + #K1 #V1 #HK12 #HV12 #H destruct + /3 width=5 by ldrop_pair, lpx_sn_pair, ex2_intro/ +| #I #L2 #K2 #V2 #e #_ #IHLK2 #X #H #_ elim (lpx_sn_inv_pair2 … H) -H + #L1 #V1 #HL12 #HV12 #H destruct + elim (IHLK2 … HL12) -L2 /3 width=3 by ldrop_drop, ex2_intro/ +| #I #L2 #K2 #V2 #W2 #d #e #_ #_ #_ #L1 #_ + (lpx_sn_inv_atom1 … H1) -X1 + >(lpx_sn_inv_atom1 … H2) -X2 /2 width=3/ +| #L0 #I #V0 #Hn #X1 #H1 #X2 #H2 destruct + elim (lpx_sn_inv_pair1 … H1) -H1 #L1 #V1 #HL01 #HV01 #H destruct + elim (lpx_sn_inv_pair1 … H2) -H2 #L2 #V2 #HL02 #HV02 #H destruct + elim (IH … HL01 … HL02) -IH normalize // #L #HL1 #HL2 + elim (HR12 … HV01 … HV02 … HL01 … HL02) -L0 -V0 /3 width=5/ +] +qed-. diff --git a/matita/matita/contribs/lambdadelta/basic_2/relocation/lpx_sn_tc.ma b/matita/matita/contribs/lambdadelta/basic_2/relocation/lpx_sn_tc.ma new file mode 100644 index 000000000..e994bf076 --- /dev/null +++ b/matita/matita/contribs/lambdadelta/basic_2/relocation/lpx_sn_tc.ma @@ -0,0 +1,119 @@ +(**************************************************************************) +(* ___ *) +(* ||M|| *) +(* ||A|| A project by Andrea Asperti *) +(* ||T|| *) +(* ||I|| Developers: *) +(* ||T|| The HELM team. *) +(* ||A|| http://helm.cs.unibo.it *) +(* \ / *) +(* \ / This file is distributed under the terms of the *) +(* v GNU General Public License Version 2 *) +(* *) +(**************************************************************************) + +include "basic_2/relocation/lpx_sn.ma". + +(* SN POINTWISE EXTENSION OF A CONTEXT-SENSITIVE REALTION FOR TERMS *********) + +(* Properties on transitive_closure *****************************************) + +lemma TC_lpx_sn_pair_refl: ∀R. (∀L. reflexive … (R L)) → + ∀L1,L2. TC … (lpx_sn R) L1 L2 → + ∀I,V. TC … (lpx_sn R) (L1. ⓑ{I} V) (L2. ⓑ{I} V). +#R #HR #L1 #L2 #H @(TC_star_ind … L2 H) -L2 +[ /2 width=1 by lpx_sn_refl/ +| /3 width=1 by TC_reflexive, lpx_sn_refl/ +| /3 width=5 by lpx_sn_pair, step/ +] +qed-. + +lemma TC_lpx_sn_pair: ∀R. (∀L. reflexive … (R L)) → + ∀I,L1,L2. TC … (lpx_sn R) L1 L2 → + ∀V1,V2. LTC … R L1 V1 V2 → + TC … (lpx_sn R) (L1. ⓑ{I} V1) (L2. ⓑ{I} V2). +#R #HR #I #L1 #L2 #HL12 #V1 #V2 #H @(TC_star_ind_dx … V1 H) -V1 // +[ /2 width=1 by TC_lpx_sn_pair_refl/ +| /4 width=3 by TC_strap, lpx_sn_pair, lpx_sn_refl/ +] +qed-. + +lemma lpx_sn_LTC_TC_lpx_sn: ∀R. (∀L. reflexive … (R L)) → + ∀L1,L2. lpx_sn (LTC … R) L1 L2 → + TC … (lpx_sn R) L1 L2. +#R #HR #L1 #L2 #H elim H -L1 -L2 +/2 width=1 by TC_lpx_sn_pair, lpx_sn_atom, inj/ +qed-. + +(* Inversion lemmas on transitive closure ***********************************) + +lemma TC_lpx_sn_inv_atom2: ∀R,L1. TC … (lpx_sn R) L1 (⋆) → L1 = ⋆. +#R #L1 #H @(TC_ind_dx … L1 H) -L1 +[ /2 width=2 by lpx_sn_inv_atom2/ +| #L1 #L #HL1 #_ #IHL2 destruct /2 width=2 by lpx_sn_inv_atom2/ +] +qed-. + +lemma TC_lpx_sn_inv_pair2: ∀R. s_rs_transitive … R (λ_. lpx_sn R) → + ∀I,L1,K2,V2. TC … (lpx_sn R) L1 (K2.ⓑ{I}V2) → + ∃∃K1,V1. TC … (lpx_sn R) K1 K2 & LTC … R K1 V1 V2 & L1 = K1. ⓑ{I} V1. +#R #HR #I #L1 #K2 #V2 #H @(TC_ind_dx … L1 H) -L1 +[ #L1 #H elim (lpx_sn_inv_pair2 … H) -H /3 width=5 by inj, ex3_2_intro/ +| #L1 #L #HL1 #_ * #K #V #HK2 #HV2 #H destruct + elim (lpx_sn_inv_pair2 … HL1) -HL1 #K1 #V1 #HK1 #HV1 #H destruct + lapply (HR … HV2 … HK1) -HR -HV2 /3 width=5 by TC_strap, ex3_2_intro/ +] +qed-. + +lemma TC_lpx_sn_ind: ∀R. s_rs_transitive … R (λ_. lpx_sn R) → + ∀S:relation lenv. + S (⋆) (⋆) → ( + ∀I,K1,K2,V1,V2. + TC … (lpx_sn R) K1 K2 → LTC … R K1 V1 V2 → + S K1 K2 → S (K1.ⓑ{I}V1) (K2.ⓑ{I}V2) + ) → + ∀L2,L1. TC … (lpx_sn R) L1 L2 → S L1 L2. +#R #HR #S #IH1 #IH2 #L2 elim L2 -L2 +[ #X #H >(TC_lpx_sn_inv_atom2 … H) -X // +| #L2 #I #V2 #IHL2 #X #H + elim (TC_lpx_sn_inv_pair2 … H) // -H -HR + #L1 #V1 #HL12 #HV12 #H destruct /3 width=1 by/ +] +qed-. + +lemma TC_lpx_sn_inv_atom1: ∀R,L2. TC … (lpx_sn R) (⋆) L2 → L2 = ⋆. +#R #L2 #H elim H -L2 +[ /2 width=2 by lpx_sn_inv_atom1/ +| #L #L2 #_ #HL2 #IHL1 destruct /2 width=2 by lpx_sn_inv_atom1/ +] +qed-. + +fact TC_lpx_sn_inv_pair1_aux: ∀R. s_rs_transitive … R (λ_. lpx_sn R) → + ∀L1,L2. TC … (lpx_sn R) L1 L2 → + ∀I,K1,V1. L1 = K1.ⓑ{I}V1 → + ∃∃K2,V2. TC … (lpx_sn R) K1 K2 & LTC … R K1 V1 V2 & L2 = K2. ⓑ{I} V2. +#R #HR #L1 #L2 #H @(TC_lpx_sn_ind … H) // -HR -L1 -L2 +[ #J #K #W #H destruct +| #I #L1 #L2 #V1 #V2 #HL12 #HV12 #_ #J #K #W #H destruct /2 width=5 by ex3_2_intro/ +] +qed-. + +lemma TC_lpx_sn_inv_pair1: ∀R. s_rs_transitive … R (λ_. lpx_sn R) → + ∀I,K1,L2,V1. TC … (lpx_sn R) (K1.ⓑ{I}V1) L2 → + ∃∃K2,V2. TC … (lpx_sn R) K1 K2 & LTC … R 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) → + ∀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-. + +(* Forward lemmas on transitive closure *************************************) + +lemma TC_lpx_sn_fwd_length: ∀R,L1,L2. TC … (lpx_sn R) L1 L2 → |L1| = |L2|. +#R #L1 #L2 #H elim H -L2 +[ #L2 #HL12 >(lpx_sn_fwd_length … HL12) -HL12 // +| #L #L2 #_ #HL2 #IHL1 + >IHL1 -L1 >(lpx_sn_fwd_length … HL2) -HL2 // +] +qed-. diff --git a/matita/matita/contribs/lambdadelta/basic_2/substitution/lleq_alt.ma b/matita/matita/contribs/lambdadelta/basic_2/substitution/lleq_alt.ma new file mode 100644 index 000000000..470fa107f --- /dev/null +++ b/matita/matita/contribs/lambdadelta/basic_2/substitution/lleq_alt.ma @@ -0,0 +1,41 @@ +(**************************************************************************) +(* ___ *) +(* ||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/llpx_sn_alt.ma". +include "basic_2/substitution/lleq.ma". + +(* LAZY EQUIVALENCE FOR LOCAL ENVIRONMENTS **********************************) + +(* Alternative definition ***************************************************) + +theorem lleq_intro_alt: ∀L1,L2,T,d. |L1| = |L2| → + (∀I1,I2,K1,K2,V1,V2,i. d ≤ yinj i → (∀U. ⇧[i, 1] U ≡ T → ⊥) → + ⇩[i] L1 ≡ K1.ⓑ{I1}V1 → ⇩[i] L2 ≡ K2.ⓑ{I2}V2 → + ∧∧ I1 = I2 & V1 = V2 & K1 ⋕[V1, 0] K2 + ) → L1 ⋕[T, d] L2. +#L1 #L2 #T #d #HL12 #IH @llpx_sn_intro_alt // -HL12 +#I1 #I2 #K1 #K2 #V1 #V2 #i #Hid #HnT #HLK1 #HLK2 +elim (IH … HnT HLK1 HLK2) -IH -HnT -HLK1 -HLK2 /2 width=1 by and3_intro/ +qed. + +theorem lleq_inv_gen: ∀L1,L2,T,d. L1 ⋕[T, d] L2 → + |L1| = |L2| ∧ + ∀I1,I2,K1,K2,V1,V2,i. d ≤ yinj i → (∀U. ⇧[i, 1] U ≡ T → ⊥) → + ⇩[i] L1 ≡ K1.ⓑ{I1}V1 → ⇩[i] L2 ≡ K2.ⓑ{I2}V2 → + ∧∧ I1 = I2 & V1 = V2 & K1 ⋕[V1, 0] K2. +#L1 #L2 #T #d #H elim (llpx_sn_inv_gen … H) -H +#HL12 #IH @conj // +#I1 #I2 #K1 #K2 #V1 #V2 #i #Hid #HnT #HLK1 #HLK2 +elim (IH … HnT HLK1 HLK2) -IH -HnT -HLK1 -HLK2 /2 width=1 by and3_intro/ +qed-. diff --git a/matita/matita/contribs/lambdadelta/basic_2/web/basic_2_src.tbl b/matita/matita/contribs/lambdadelta/basic_2/web/basic_2_src.tbl index a5f14f196..f65ec6eee 100644 --- a/matita/matita/contribs/lambdadelta/basic_2/web/basic_2_src.tbl +++ b/matita/matita/contribs/lambdadelta/basic_2/web/basic_2_src.tbl @@ -213,7 +213,7 @@ table { [ { "substitution" * } { [ { "lazy equivalence" * } { [ "fleq ( ⦃?,?,?⦄ ⋕[?] ⦃?,?,?⦄ )" "fleq_fleq" * ] - [ "lleq ( ? ⋕[?,?] ? )" "lleq_leq" + "lleq_ldrop" + "lleq_fqus" + "lleq_lleq" * ] + [ "lleq ( ? ⋕[?,?] ? )" "lleq_alt" + "lleq_leq" + "lleq_ldrop" + "lleq_fqus" + "lleq_lleq" * ] } ] [ { "iterated structural successor for closures" * } { @@ -248,7 +248,7 @@ table { } ] [ { "lazy pointwise extension of a relation" * } { - [ "llpx_sn" "llpx_sn_tc" + "llpx_sn_leq" + "llpx_sn_ldrop" + "llpx_sn_lpx_sn" * ] + [ "llpx_sn" "llpx_sn_alt" + "llpx_sn_tc" + "llpx_sn_leq" + "llpx_sn_ldrop" + "llpx_sn_lpx_sn" * ] } ] [ { "basic local env. slicing" * } { @@ -257,7 +257,7 @@ table { ] [ { "basic term relocation" * } { [ "lift_vector ( ⇧[?,?] ? ≡ ? )" "lift_lift_vector" * ] - [ "lift ( ⇧[?,?] ? ≡ ? )" "lift_lift" * ] + [ "lift ( ⇧[?,?] ? ≡ ? )" "lift_neq" + "lift_lift" * ] } ] } @@ -269,7 +269,7 @@ table { } ] [ { "pointwise extension of a relation" * } { - [ "lpx_sn" "lpx_sn_tc" + "lpx_sn_lpx_sn" * ] + [ "lpx_sn" "lpx_sn_alt" + "lpx_sn_tc" + "lpx_sn_lpx_sn" * ] } ] [ { "same top term constructor" * } {