From e4be4188d549da5fde54cdc37a6fb4eb2469c15b Mon Sep 17 00:00:00 2001 From: Ferruccio Guidi Date: Tue, 18 Feb 2014 17:34:38 +0000 Subject: [PATCH] - a reinforement in a lemma on ldrop allows to prove a lemma on lsx :) - some renaming --- .../basic_2/computation/lprs_ldrop.ma | 1 + .../basic_2/computation/lpxs_ldrop.ma | 1 + .../basic_2/computation/lsx_ldrop.ma | 32 +++++++++++++++ .../basic_2/computation/lsx_lpxs.ma | 15 +++++++ .../lambdadelta/basic_2/reduction/cpx_cpys.ma | 2 +- .../lambdadelta/basic_2/relocation/cpy.ma | 4 +- .../lambdadelta/basic_2/relocation/ldrop.ma | 40 ++++++++++++++----- .../basic_2/relocation/ldrop_lpx_sn.ma | 11 +++-- .../basic_2/relocation/ldrop_lsuby.ma | 29 ++++++++++++++ .../lambdadelta/basic_2/relocation/lsuby.ma | 29 +------------- .../basic_2/substitution/cpys_alt.ma | 2 +- .../basic_2/substitution/lleq_lleq.ma | 8 ++++ .../lambdadelta/basic_2/web/basic_2_src.tbl | 12 +++--- 13 files changed, 133 insertions(+), 53 deletions(-) create mode 100644 matita/matita/contribs/lambdadelta/basic_2/computation/lsx_ldrop.ma create mode 100644 matita/matita/contribs/lambdadelta/basic_2/relocation/ldrop_lsuby.ma diff --git a/matita/matita/contribs/lambdadelta/basic_2/computation/lprs_ldrop.ma b/matita/matita/contribs/lambdadelta/basic_2/computation/lprs_ldrop.ma index f03d3f0e8..a728ad0ab 100644 --- a/matita/matita/contribs/lambdadelta/basic_2/computation/lprs_ldrop.ma +++ b/matita/matita/contribs/lambdadelta/basic_2/computation/lprs_ldrop.ma @@ -12,6 +12,7 @@ (* *) (**************************************************************************) +include "basic_2/relocation/ldrop_lsuby.ma". include "basic_2/reduction/lpr_ldrop.ma". include "basic_2/computation/lprs.ma". diff --git a/matita/matita/contribs/lambdadelta/basic_2/computation/lpxs_ldrop.ma b/matita/matita/contribs/lambdadelta/basic_2/computation/lpxs_ldrop.ma index d8c489017..95afc7c3b 100644 --- a/matita/matita/contribs/lambdadelta/basic_2/computation/lpxs_ldrop.ma +++ b/matita/matita/contribs/lambdadelta/basic_2/computation/lpxs_ldrop.ma @@ -12,6 +12,7 @@ (* *) (**************************************************************************) +include "basic_2/relocation/ldrop_lsuby.ma". include "basic_2/reduction/lpx_ldrop.ma". include "basic_2/computation/lpxs.ma". diff --git a/matita/matita/contribs/lambdadelta/basic_2/computation/lsx_ldrop.ma b/matita/matita/contribs/lambdadelta/basic_2/computation/lsx_ldrop.ma new file mode 100644 index 000000000..261168b92 --- /dev/null +++ b/matita/matita/contribs/lambdadelta/basic_2/computation/lsx_ldrop.ma @@ -0,0 +1,32 @@ +(**************************************************************************) +(* ___ *) +(* ||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/lleq_ldrop.ma". +include "basic_2/computation/lsx.ma". + +(* SN EXTENDED STRONGLY NORMALIZING LOCAL ENVIRONMENTS **********************) + +(* Advanced properties ******************************************************) + +lemma lsx_lref_free: ∀h,g,G,L,d,i. |L| ≤ i → G ⊢ ⋕⬊*[h, g, #i, d] L. +#h #g #G #L1 #d #i #HL1 @lsx_intro +#L2 #HL12 #H elim H -H +/4 width=6 by lpxs_fwd_length, lleq_free, le_repl_sn_aux/ +qed. + +lemma lsx_lref_skip: ∀h,g,G,L,d,i. yinj i < d → G ⊢ ⋕⬊*[h, g, #i, d] L. +#h #g #G #L1 #d #i #HL1 @lsx_intro +#L2 #HL12 #H elim H -H +/3 width=4 by lpxs_fwd_length, lleq_skip/ +qed. diff --git a/matita/matita/contribs/lambdadelta/basic_2/computation/lsx_lpxs.ma b/matita/matita/contribs/lambdadelta/basic_2/computation/lsx_lpxs.ma index 2130d8b51..8f2603102 100644 --- a/matita/matita/contribs/lambdadelta/basic_2/computation/lsx_lpxs.ma +++ b/matita/matita/contribs/lambdadelta/basic_2/computation/lsx_lpxs.ma @@ -89,6 +89,21 @@ lemma lsx_flat: ∀h,g,I,G,L,V,d. G ⊢ ⋕⬊*[h, g, V, d] L → (* Advanced forward lemmas **************************************************) +lemma lsx_fwd_lref_be: ∀h,g,I,G,L,d,i. d ≤ yinj i → G ⊢ ⋕⬊*[h, g, #i, d] L → + ∀K,V. ⇩[i] L ≡ K.ⓑ{I}V → G ⊢ ⋕⬊*[h, g, V, 0] K. +#h #g #I #G #L #d #i #Hdi #H @(lsx_ind … H) -L +#L1 #_ #IHL1 #K1 #V #HLK1 @lsx_intro +#K2 #HK12 #HnK12 lapply (ldrop_fwd_drop2 … HLK1) +#H2LK1 elim (ldrop_lpxs_trans … H2LK1 … HK12) -H2LK1 -HK12 +#L2 #HL12 #H2LK2 #HL21 elim (lsuby_ldrop_trans_be … HL21 … HLK1) -HL21 /2 width=1 by ylt_inj/ +#J #Y #_ #HLK2 lapply (ldrop_fwd_drop2 … HLK2) +#HY lapply (ldrop_mono … HY … H2LK2) -HY -H2LK2 #H destruct +elim (lpxs_ldrop_conf … HLK1 … HL12) #Y #H #HY +elim (lpxs_inv_pair1 … H) -H #Z #X #_ #_ #H destruct +lapply (ldrop_mono … HY … HLK2) -HY #H destruct +/4 width=10 by lleq_inv_lref_ge/ +qed-. + lemma lsx_fwd_bind_dx: ∀h,g,a,I,G,L,V,T,d. G ⊢ ⋕⬊*[h, g, ⓑ{a,I}V.T, d] L → G ⊢ ⋕⬊*[h, g, T, ⫯d] L.ⓑ{I}V. #h #g #a #I #G #L #V1 #T #d #H @(lsx_ind … H) -L diff --git a/matita/matita/contribs/lambdadelta/basic_2/reduction/cpx_cpys.ma b/matita/matita/contribs/lambdadelta/basic_2/reduction/cpx_cpys.ma index fa1d4e8d2..3b38ee6ab 100644 --- a/matita/matita/contribs/lambdadelta/basic_2/reduction/cpx_cpys.ma +++ b/matita/matita/contribs/lambdadelta/basic_2/reduction/cpx_cpys.ma @@ -24,7 +24,7 @@ lemma lsuby_cpx_trans: ∀h,g,G. lsub_trans … (cpx h g G) (lsuby 0 (∞)). [ // | /2 width=2 by cpx_sort/ | #I #G #L1 #K1 #V1 #V2 #W2 #i #HLK1 #_ #HVW2 #IHV12 #L2 #HL12 - elim (lsuby_fwd_ldrop2_be … HL12 … HLK1) // -HL12 -HLK1 /3 width=7 by cpx_delta/ + 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/ diff --git a/matita/matita/contribs/lambdadelta/basic_2/relocation/cpy.ma b/matita/matita/contribs/lambdadelta/basic_2/relocation/cpy.ma index 66852c667..3709db1d7 100644 --- a/matita/matita/contribs/lambdadelta/basic_2/relocation/cpy.ma +++ b/matita/matita/contribs/lambdadelta/basic_2/relocation/cpy.ma @@ -15,7 +15,7 @@ include "ground_2/ynat/ynat_max.ma". include "basic_2/notation/relations/psubst_6.ma". include "basic_2/grammar/genv.ma". -include "basic_2/relocation/lsuby.ma". +include "basic_2/relocation/ldrop.ma". (* CONTEXT-SENSITIVE EXTENDED ORDINARY SUBSTITUTION FOR TERMS ***************) @@ -41,7 +41,7 @@ lemma lsuby_cpy_trans: ∀G,d,e. lsub_trans … (cpy d e G) (lsuby d e). #G #d #e #L1 #T1 #T2 #H elim H -G -L1 -T1 -T2 -d -e [ // | #I #G #L1 #K1 #V #W #i #d #e #Hdi #Hide #HLK1 #HVW #L2 #HL12 - elim (lsuby_fwd_ldrop2_be … HL12 … HLK1) -HL12 -HLK1 /2 width=5 by cpy_subst/ + elim (lsuby_ldrop_trans_be … HL12 … HLK1) -HL12 -HLK1 /2 width=5 by cpy_subst/ | /4 width=1 by lsuby_succ, cpy_bind/ | /3 width=1 by cpy_flat/ ] diff --git a/matita/matita/contribs/lambdadelta/basic_2/relocation/ldrop.ma b/matita/matita/contribs/lambdadelta/basic_2/relocation/ldrop.ma index af0172fdb..b4b2ee3be 100644 --- a/matita/matita/contribs/lambdadelta/basic_2/relocation/ldrop.ma +++ b/matita/matita/contribs/lambdadelta/basic_2/relocation/ldrop.ma @@ -17,9 +17,9 @@ include "ground_2/lib/lstar.ma". include "basic_2/notation/relations/rdrop_5.ma". include "basic_2/notation/relations/rdrop_4.ma". include "basic_2/notation/relations/rdrop_3.ma". -include "basic_2/grammar/lenv_length.ma". include "basic_2/grammar/cl_restricted_weight.ma". include "basic_2/relocation/lift.ma". +include "basic_2/relocation/lsuby.ma". (* BASIC SLICING FOR LOCAL ENVIRONMENTS *************************************) @@ -60,7 +60,7 @@ definition dropable_sn: predicate (relation lenv) ≝ definition dedropable_sn: predicate (relation lenv) ≝ λR. ∀L1,K1,s,d,e. ⇩[s, d, e] L1 ≡ K1 → ∀K2. R K1 K2 → - ∃∃L2. R L1 L2 & ⇩[s, d, e] L2 ≡ K2. + ∃∃L2. R L1 L2 & ⇩[s, d, e] L2 ≡ K2 & L2 ⊑×[d, e] L1. definition dropable_dx: predicate (relation lenv) ≝ λR. ∀L1,L2. R L1 L2 → ∀K2,s,e. ⇩[s, 0, e] L2 ≡ K2 → @@ -250,15 +250,6 @@ lemma dropable_sn_TC: ∀R. dropable_sn R → dropable_sn (TC … R). ] qed-. -lemma dedropable_sn_TC: ∀R. dedropable_sn R → dedropable_sn (TC … R). -#R #HR #L1 #K1 #s #d #e #HLK1 #K2 #H elim H -K2 -[ #K2 #HK12 elim (HR … HLK1 … HK12) -HR -K1 - /3 width=3 by inj, ex2_intro/ -| #K #K2 #_ #HK2 * #L #HL1 #HLK elim (HR … HLK … HK2) -HR -K - /3 width=3 by step, ex2_intro/ -] -qed-. - lemma dropable_dx_TC: ∀R. dropable_dx R → dropable_dx (TC … R). #R #HR #L1 #L2 #H elim H -L2 [ #L2 #HL12 #K2 #s #e #HLK2 elim (HR … HL12 … HLK2) -HR -L2 @@ -279,6 +270,33 @@ lemma l_deliftable_sn_llstar: ∀R. l_deliftable_sn R → ] qed-. +lemma lsuby_ldrop_trans_be: ∀L1,L2,d,e. L1 ⊑×[d, e] L2 → + ∀I2,K2,W,s,i. ⇩[s, 0, i] L2 ≡ K2.ⓑ{I2}W → + d ≤ i → i < d + e → + ∃∃I1,K1. K1 ⊑×[0, ⫰(d+e-i)] K2 & ⇩[s, 0, i] L1 ≡ K1.ⓑ{I1}W. +#L1 #L2 #d #e #H elim H -L1 -L2 -d -e +[ #L1 #d #e #J2 #K2 #W #s #i #H + elim (ldrop_inv_atom1 … H) -H #H destruct +| #I1 #I2 #L1 #L2 #V1 #V2 #_ #_ #J2 #K2 #W #s #i #_ #_ #H + elim (ylt_yle_false … H) // +| #I1 #I2 #L1 #L2 #V #e #HL12 #IHL12 #J2 #K2 #W #s #i #H #_ >yplus_O1 + elim (ldrop_inv_O1_pair1 … H) -H * #Hi #HLK1 [ -IHL12 | -HL12 ] + [ #_ destruct -I2 >ypred_succ + /2 width=4 by ldrop_pair, ex2_2_intro/ + | lapply (ylt_inv_O1 i ?) /2 width=1 by ylt_inj/ + #H yminus_succ yplus_succ1 #H lapply (ylt_inv_succ … H) -H + #Hide lapply (ldrop_inv_drop1_lt … HLK2 ?) -HLK2 /2 width=1 by ylt_O/ + #HLK1 elim (IHL12 … HLK1) -IHL12 -HLK1 yminus_SO2 + /4 width=4 by ylt_O, ldrop_drop_lt, ex2_2_intro/ +] +qed-. + (* Basic forvard lemmas *****************************************************) (* Basic_1: was: drop_S *) 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 index 0bf892c33..127f92cc0 100644 --- a/matita/matita/contribs/lambdadelta/basic_2/relocation/ldrop_lpx_sn.ma +++ b/matita/matita/contribs/lambdadelta/basic_2/relocation/ldrop_lpx_sn.ma @@ -40,17 +40,20 @@ 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=3 by ldrop_atom, lpx_sn_atom, ex2_intro/ + /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 - /3 width=5 by ldrop_pair, lpx_sn_pair, ex2_intro/ + lapply (lpx_sn_fwd_length … HK12) + #H @(ex3_intro … (K2.ⓑ{I}V2)) (**) (* explicit constructor *) + /3 width=1 by lsuby_O1, lpx_sn_pair, monotonic_le_plus_l/ | #I #L1 #K1 #V1 #e #_ #IHLK1 #K2 #HK12 elim (IHLK1 … HK12) -K1 - /3 width=5 by ldrop_drop, lpx_sn_pair, ex2_intro/ + /3 width=5 by ldrop_drop, lsuby_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=5 by ldrop_skip, lpx_sn_pair, ex2_intro/ + elim (IHLK1 … HK12) -K1 + /3 width=6 by ldrop_skip, lsuby_succ, lpx_sn_pair, ex3_intro/ ] qed-. diff --git a/matita/matita/contribs/lambdadelta/basic_2/relocation/ldrop_lsuby.ma b/matita/matita/contribs/lambdadelta/basic_2/relocation/ldrop_lsuby.ma new file mode 100644 index 000000000..fdcca5a3d --- /dev/null +++ b/matita/matita/contribs/lambdadelta/basic_2/relocation/ldrop_lsuby.ma @@ -0,0 +1,29 @@ +(**************************************************************************) +(* ___ *) +(* ||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_lsuby.ma". +include "basic_2/relocation/ldrop.ma". + +(* BASIC SLICING FOR LOCAL ENVIRONMENTS *************************************) + +(* Properties on local environment refinement for extended substitution *****) + +lemma dedropable_sn_TC: ∀R. dedropable_sn R → dedropable_sn (TC … R). +#R #HR #L1 #K1 #s #d #e #HLK1 #K2 #H elim H -K2 +[ #K2 #HK12 elim (HR … HLK1 … HK12) -HR -K1 + /3 width=4 by inj, ex3_intro/ +| #K #K2 #_ #HK2 * #L #H1L1 #HLK #H2L1 elim (HR … HLK … HK2) -HR -K + /3 width=6 by lsuby_trans, step, ex3_intro/ +] +qed-. diff --git a/matita/matita/contribs/lambdadelta/basic_2/relocation/lsuby.ma b/matita/matita/contribs/lambdadelta/basic_2/relocation/lsuby.ma index f6bab12f8..34212a6c7 100644 --- a/matita/matita/contribs/lambdadelta/basic_2/relocation/lsuby.ma +++ b/matita/matita/contribs/lambdadelta/basic_2/relocation/lsuby.ma @@ -14,7 +14,7 @@ include "ground_2/ynat/ynat_plus.ma". include "basic_2/notation/relations/extlrsubeq_4.ma". -include "basic_2/relocation/ldrop.ma". +include "basic_2/grammar/lenv_length.ma". (* LOCAL ENVIRONMENT REFINEMENT FOR EXTENDED SUBSTITUTION *******************) @@ -206,30 +206,3 @@ lemma lsuby_inv_succ2: ∀I2,K2,L1,V2,d,e. L1 ⊑×[d, e] K2.ⓑ{I2}V2 → 0 < d lemma lsuby_fwd_length: ∀L1,L2,d,e. L1 ⊑×[d, e] L2 → |L2| ≤ |L1|. #L1 #L2 #d #e #H elim H -L1 -L2 -d -e normalize /2 width=1 by le_S_S/ qed-. - -lemma lsuby_fwd_ldrop2_be: ∀L1,L2,d,e. L1 ⊑×[d, e] L2 → - ∀I2,K2,W,s,i. ⇩[s, 0, i] L2 ≡ K2.ⓑ{I2}W → - d ≤ i → i < d + e → - ∃∃I1,K1. K1 ⊑×[0, ⫰(d+e-i)] K2 & ⇩[s, 0, i] L1 ≡ K1.ⓑ{I1}W. -#L1 #L2 #d #e #H elim H -L1 -L2 -d -e -[ #L1 #d #e #J2 #K2 #W #s #i #H - elim (ldrop_inv_atom1 … H) -H #H destruct -| #I1 #I2 #L1 #L2 #V1 #V2 #_ #_ #J2 #K2 #W #s #i #_ #_ #H - elim (ylt_yle_false … H) // -| #I1 #I2 #L1 #L2 #V #e #HL12 #IHL12 #J2 #K2 #W #s #i #H #_ >yplus_O1 - elim (ldrop_inv_O1_pair1 … H) -H * #Hi #HLK1 [ -IHL12 | -HL12 ] - [ #_ destruct -I2 >ypred_succ - /2 width=4 by ldrop_pair, ex2_2_intro/ - | lapply (ylt_inv_O1 i ?) /2 width=1 by ylt_inj/ - #H yminus_succ yplus_succ1 #H lapply (ylt_inv_succ … H) -H - #Hide lapply (ldrop_inv_drop1_lt … HLK2 ?) -HLK2 /2 width=1 by ylt_O/ - #HLK1 elim (IHL12 … HLK1) -IHL12 -HLK1 yminus_SO2 - /4 width=4 by ylt_O, ldrop_drop_lt, ex2_2_intro/ -] -qed-. diff --git a/matita/matita/contribs/lambdadelta/basic_2/substitution/cpys_alt.ma b/matita/matita/contribs/lambdadelta/basic_2/substitution/cpys_alt.ma index 6a5e2694c..e297be698 100644 --- a/matita/matita/contribs/lambdadelta/basic_2/substitution/cpys_alt.ma +++ b/matita/matita/contribs/lambdadelta/basic_2/substitution/cpys_alt.ma @@ -41,7 +41,7 @@ lemma lsuby_cpysa_trans: ∀G,d,e. lsub_trans … (cpysa d e G) (lsuby d e). #G #d #e #L1 #T1 #T2 #H elim H -G -L1 -T1 -T2 -d -e [ // | #I #G #L1 #K1 #V1 #V2 #W2 #i #d #e #Hdi #Hide #HLK1 #_ #HVW2 #IHV12 #L2 #HL12 - elim (lsuby_fwd_ldrop2_be … HL12 … HLK1) -HL12 -HLK1 /3 width=7 by cpysa_subst/ + elim (lsuby_ldrop_trans_be … HL12 … HLK1) -HL12 -HLK1 /3 width=7 by cpysa_subst/ | /4 width=1 by lsuby_succ, cpysa_bind/ | /3 width=1 by cpysa_flat/ ] diff --git a/matita/matita/contribs/lambdadelta/basic_2/substitution/lleq_lleq.ma b/matita/matita/contribs/lambdadelta/basic_2/substitution/lleq_lleq.ma index 01e08e9f9..ca8035680 100644 --- a/matita/matita/contribs/lambdadelta/basic_2/substitution/lleq_lleq.ma +++ b/matita/matita/contribs/lambdadelta/basic_2/substitution/lleq_lleq.ma @@ -85,6 +85,14 @@ lemma lleq_inv_lref_ge_sn: ∀L1,L2,d,i. L1 ⋕[#i, d] L2 → d ≤ i → /3 width=4 by lleq_sym, ex2_2_intro/ qed-. +lemma lleq_inv_lref_ge: ∀L1,L2,d,i. L1 ⋕[#i, d] L2 → d ≤ i → + ∀I1,I2,K1,K2,V. + ⇩[i] L1 ≡ K1.ⓑ{I1}V → ⇩[i] L2 ≡ K2.ⓑ{I2}V → K1 ⋕[V, 0] K2. +#L1 #L2 #d #i #HL12 #Hdi #I1 #I2 #K1 #K2 #V #HLK1 #HLK2 +elim (lleq_inv_lref_ge_sn … HL12 … HLK1) // -L1 -d +#J #Y #HY lapply (ldrop_mono … HY … HLK2) -L2 -i #H destruct // +qed-. + (* Advanced properties ******************************************************) lemma lleq_dec: ∀T,L1,L2,d. Decidable (L1 ⋕[T, d] L2). 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 de9939c00..bb8ab1587 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 @@ -84,7 +84,7 @@ table { } ] [ { "strongly normalizing extended computation" * } { - [ "lsx ( ? ⊢ ⬊*[?,?,?,?] ? )" "lsx_cpxs" + "lsx_csx" * ] + [ "lsx ( ? ⊢ ⬊*[?,?,?,?] ? )" "lsx_ldrop" + "lsx_cpxs" + "lsx_csx" * ] [ "csx_vector ( ⦃?,?⦄ ⊢ ⬊*[?,?] ? )" "csx_tstc_vector" + "csx_aaa" * ] [ "csx ( ⦃?,?⦄ ⊢ ⬊*[?,?] ? )" "csx_alt ( ⦃?,?⦄ ⊢ ⬊⬊*[?,?] ? )" "csx_lift" + "csx_lpx" + "csx_fpbs" * ] } @@ -242,10 +242,6 @@ table { [ "cpy ( ⦃?,?⦄ ⊢ ? ▶[?,?] ? )" "cpy_lift" + "cpy_cpy" * ] } ] - [ { "local env. ref. for extended substitution" * } { - [ "lsuby ( ? ⊑×[?,?] ? )" "lsuby_lsuby" * ] - } - ] [ { "restricted local env. ref." * } { [ "lsubr ( ? ⊑ ? )" "lsubr_lsubr" * ] } @@ -260,7 +256,11 @@ table { } ] [ { "basic local env. slicing" * } { - [ "ldrop ( ⇩[?,?,?] ? ≡ ? )" "ldrop_append" + "ldrop_lpx_sn" + "ldrop_ldrop" * ] + [ "ldrop ( ⇩[?,?,?] ? ≡ ? )" "ldrop_append" + "ldrop_lpx_sn" + "ldrop_lsuby" + "ldrop_ldrop" * ] + } + ] + [ { "local env. ref. for extended substitution" * } { + [ "lsuby ( ? ⊑×[?,?] ? )" "lsuby_lsuby" * ] } ] [ { "basic term relocation" * } { -- 2.39.2