From: Ferruccio Guidi Date: Thu, 19 Jan 2017 18:21:51 +0000 (+0000) Subject: - preservation of arity assignment X-Git-Tag: make_still_working~518 X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=commitdiff_plain;h=cbcadc678c098f64e7eac31cb73297558ba37b4a;p=helm.git - preservation of arity assignment - hls orders files by extension and then by name --- diff --git a/matita/matita/contribs/lambdadelta/basic_2/rt_transition/cpg.ma b/matita/matita/contribs/lambdadelta/basic_2/rt_transition/cpg.ma index c704ddf6b..73be2e83d 100644 --- a/matita/matita/contribs/lambdadelta/basic_2/rt_transition/cpg.ma +++ b/matita/matita/contribs/lambdadelta/basic_2/rt_transition/cpg.ma @@ -264,6 +264,25 @@ lemma cpg_inv_cast1: ∀Rt,c,h,G,L,V1,U1,U2. ⦃G, L⦄ ⊢ ⓝV1.U1 ⬈[Rt, c, | ∃∃cV. ⦃G, L⦄ ⊢ V1 ⬈[Rt, cV, h] U2 & c = cV+𝟘𝟙. /2 width=3 by cpg_inv_cast1_aux/ qed-. +(* Advanced inversion lemmas ************************************************) + +lemma cpg_inv_zero1_pair: ∀Rt,c,h,I,G,K,V1,T2. ⦃G, K.ⓑ{I}V1⦄ ⊢ #0 ⬈[Rt, c, h] T2 → + ∨∨ (T2 = #0 ∧ c = 𝟘𝟘) + | ∃∃cV,V2. ⦃G, K⦄ ⊢ V1 ⬈[Rt, cV, h] V2 & ⬆*[1] V2 ≡ T2 & + I = Abbr & c = cV + | ∃∃cV,V2. ⦃G, K⦄ ⊢ V1 ⬈[Rt, cV, h] V2 & ⬆*[1] V2 ≡ T2 & + I = Abst & c = cV+𝟘𝟙. +#Rt #c #h #I #G #K #V1 #T2 #H elim (cpg_inv_zero1 … H) -H /2 width=1 by or3_intro0/ +* #z #Y #X1 #X2 #HX12 #HXT2 #H1 #H2 destruct /3 width=5 by or3_intro1, or3_intro2, ex4_2_intro/ +qed-. + +lemma cpg_inv_lref1_pair: ∀Rt,c,h,I,G,K,V,T2,i. ⦃G, K.ⓑ{I}V⦄ ⊢ #⫯i ⬈[Rt, c, h] T2 → + (T2 = #(⫯i) ∧ c = 𝟘𝟘) ∨ + ∃∃T. ⦃G, K⦄ ⊢ #i ⬈[Rt, c, h] T & ⬆*[1] T ≡ T2. +#Rt #c #h #I #G #L #V #T2 #i #H elim (cpg_inv_lref1 … H) -H /2 width=1 by or_introl/ +* #Z #Y #X #T #HT #HT2 #H destruct /3 width=3 by ex2_intro, or_intror/ +qed-. + (* Basic forward lemmas *****************************************************) lemma cpg_fwd_bind1_minus: ∀Rt,c,h,I,G,L,V1,T1,T. ⦃G, L⦄ ⊢ -ⓑ{I}V1.T1 ⬈[Rt, c, h] T → ∀p. diff --git a/matita/matita/contribs/lambdadelta/basic_2/rt_transition/cpx.ma b/matita/matita/contribs/lambdadelta/basic_2/rt_transition/cpx.ma index 49652d10c..7d20bc47f 100644 --- a/matita/matita/contribs/lambdadelta/basic_2/rt_transition/cpx.ma +++ b/matita/matita/contribs/lambdadelta/basic_2/rt_transition/cpx.ma @@ -187,6 +187,20 @@ qed-. (* Advanced inversion lemmas ************************************************) +lemma cpx_inv_zero1_pair: ∀h,I,G,K,V1,T2. ⦃G, K.ⓑ{I}V1⦄ ⊢ #0 ⬈[h] T2 → + T2 = #0 ∨ + ∃∃V2. ⦃G, K⦄ ⊢ V1 ⬈[h] V2 & ⬆*[1] V2 ≡ T2. +#h #I #G #L #V1 #T2 * #c #H elim (cpg_inv_zero1_pair … H) -H * +/4 width=3 by ex2_intro, ex_intro, or_intror, or_introl/ +qed-. + +lemma cpx_inv_lref1_pair: ∀h,I,G,K,V,T2,i. ⦃G, K.ⓑ{I}V⦄ ⊢ #⫯i ⬈[h] T2 → + T2 = #(⫯i) ∨ + ∃∃T. ⦃G, K⦄ ⊢ #i ⬈[h] T & ⬆*[1] T ≡ T2. +#h #I #G #L #V #T2 #i * #c #H elim (cpg_inv_lref1_pair … H) -H * +/4 width=3 by ex2_intro, ex_intro, or_introl, or_intror/ +qed-. + lemma cpx_inv_flat1: ∀h,I,G,L,V1,U1,U2. ⦃G, L⦄ ⊢ ⓕ{I}V1.U1 ⬈[h] U2 → ∨∨ ∃∃V2,T2. ⦃G, L⦄ ⊢ V1 ⬈[h] V2 & ⦃G, L⦄ ⊢ U1 ⬈[h] T2 & U2 = ⓕ{I}V2.T2 diff --git a/matita/matita/contribs/lambdadelta/basic_2/rt_transition/hls.ml b/matita/matita/contribs/lambdadelta/basic_2/rt_transition/hls.ml index 9c12ae1c7..01f59045d 100644 --- a/matita/matita/contribs/lambdadelta/basic_2/rt_transition/hls.ml +++ b/matita/matita/contribs/lambdadelta/basic_2/rt_transition/hls.ml @@ -15,6 +15,19 @@ let rec read ich = let length l s = max l (String.length s) +let split s = +try + let i = String.rindex s '.' in + if i = 0 then s, "" else + String.sub s 0 i, String.sub s i (String.length s - i) +with Not_found -> s, "" + +let compare s1 s2 = + let n1, e1 = split s1 in + let n2, e2 = split s2 in + let e = String.compare e1 e2 in + if e = 0 then String.compare n1 n2 else e + let write l c s = let pre, post = if List.mem s !hl then color, normal else "", "" in let spc = String.make (l - String.length s) ' ' in @@ -34,8 +47,8 @@ let help = "" let main = Arg.parse [] process help; let files = Sys.readdir "." in - Array.fast_sort String.compare files; let l = Array.fold_left length 0 files in if cols < l then failwith "window too small"; + Array.fast_sort compare files; let c = Array.fold_left (write l) 0 files in - if 0 < c && c < cols then print_newline () + if 0 < c && c < cols then print_newline (); diff --git a/matita/matita/contribs/lambdadelta/basic_2/rt_transition/lfpr_aaa.ma b/matita/matita/contribs/lambdadelta/basic_2/rt_transition/lfpr_aaa.ma new file mode 100644 index 000000000..eb455f036 --- /dev/null +++ b/matita/matita/contribs/lambdadelta/basic_2/rt_transition/lfpr_aaa.ma @@ -0,0 +1,28 @@ +(**************************************************************************) +(* ___ *) +(* ||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/rt_transition/lfpx_aaa.ma". +include "basic_2/rt_transition/lfpr_lfpx.ma". + +(* PARALLEL R-TRANSITION FOR LOCAL ENV.S ON REFERRED ENTRIES ****************) + +(* Properties with atomic arity assignment for terms ************************) + +lemma cpr_aaa_conf: ∀h,G,L,T1,A. ⦃G, L⦄ ⊢ T1 ⁝ A → + ∀T2. ⦃G, L⦄ ⊢ T1 ➡[h] T2 → ⦃G, L⦄ ⊢ T2 ⁝ A. +/3 width=5 by cpx_aaa_conf, cpm_fwd_cpx/ qed-. + +lemma lfpr_aaa_conf: ∀h,G,L1,T,A. ⦃G, L1⦄ ⊢ T ⁝ A → + ∀L2. ⦃G, L1⦄ ⊢ ➡[h, T] L2 → ⦃G, L2⦄ ⊢ T ⁝ A. +/3 width=4 by lfpx_aaa_conf, lfpr_fwd_lfpx/ qed-. diff --git a/matita/matita/contribs/lambdadelta/basic_2/rt_transition/lfpx_aaa.ma b/matita/matita/contribs/lambdadelta/basic_2/rt_transition/lfpx_aaa.ma new file mode 100644 index 000000000..2f90bf27e --- /dev/null +++ b/matita/matita/contribs/lambdadelta/basic_2/rt_transition/lfpx_aaa.ma @@ -0,0 +1,82 @@ +(**************************************************************************) +(* ___ *) +(* ||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/static/aaa_drops.ma". +include "basic_2/static/lsuba_aaa.ma". +include "basic_2/rt_transition/lfpx_fqup.ma". + +(* UNCOUNTED PARALLEL RT-TRANSITION FOR LOCAL ENV.S ON REFERRED ENTRIES *****) + +(* Properties with atomic arity assignment for terms ************************) + +(* Note: lemma 500 *) +(* Basic_2A1: was: cpx_lpx_aaa_conf *) +lemma cpx_aaa_conf_lfpx: ∀h,G,L1,T1,A. ⦃G, L1⦄ ⊢ T1 ⁝ A → + ∀T2. ⦃G, L1⦄ ⊢ T1 ⬈[h] T2 → + ∀L2. ⦃G, L1⦄ ⊢ ⬈[h, T1] L2 → ⦃G, L2⦄ ⊢ T2 ⁝ A. +#h #G #L1 #T1 #A #H elim H -G -L1 -T1 -A +[ #G #L1 #s #X2 #HX + elim (cpx_inv_sort1 … HX) -HX // +| #I #G #L1 #V1 #B #_ #IH #X2 #HX #Y #HY + elim (lfpx_inv_zero_pair_sn … HY) -HY #L2 #V2 #HL12 #HV12 #H destruct + elim (cpx_inv_zero1_pair … HX) -HX + [ #H destruct /3 width=1 by aaa_zero/ + | -HV12 * /4 width=7 by aaa_lifts, drops_refl, drops_drop/ + ] +| #I #G #L1 #V1 #B #i #_ #IH #X2 #HX #Y #HY + elim (lfpx_inv_lref_pair_sn … HY) -HY #L2 #W2 #HL12 #H destruct + elim (cpx_inv_lref1_pair … HX) -HX + [ #H destruct /3 width=1 by aaa_lref/ + | * /4 width=7 by aaa_lifts, drops_refl, drops_drop/ + ] +| #p #G #L1 #V1 #T1 #B #A #_ #_ #IHV #IHT #X2 #HX #L2 #HL12 + elim (lfpx_inv_bind … HL12) -HL12 #HV #HT + elim (cpx_inv_abbr1 … HX) -HX * + [ #V2 #T2 #HV12 #HT12 #H destruct + /4 width=2 by lfpx_pair_repl_dx, aaa_abbr/ + | #T2 #HT12 #HXT2 #H destruct -IHV + /4 width=7 by aaa_inv_lifts, drops_drop, drops_refl/ + ] +| #p #G #L1 #V1 #T1 #B #A #_ #_ #IHV #IHT #X2 #H #L2 #HL12 + elim (lfpx_inv_bind … HL12) -HL12 #HV #HT + elim (cpx_inv_abst1 … H) -H #V2 #T2 #HV12 #HT12 #H destruct + /4 width=2 by lfpx_pair_repl_dx, aaa_abst/ +| #G #L1 #V1 #T1 #B #A #_ #_ #IHV #IHT #X2 #H #L2 #HL12 + elim (lfpx_inv_flat … HL12) -HL12 #HV #HT + elim (cpx_inv_appl1 … H) -H * + [ #V2 #T2 #HV12 #HT12 #H destruct /3 width=3 by aaa_appl/ + | #q #V2 #W1 #W2 #U1 #U2 #HV12 #HW12 #HU12 #H1 #H2 destruct + lapply (IHV … HV12 … HV) -IHV -HV12 -HV #HV2 + lapply (IHT (ⓛ{q}W2.U2) … HT) -IHT -HT /2 width=1 by cpx_bind/ -L1 #H + elim (aaa_inv_abst … H) -H #B0 #A0 #HW1 #HU2 #H destruct + /5 width=6 by lsuba_aaa_trans, lsuba_beta, aaa_abbr, aaa_cast/ + | #q #V #V2 #W1 #W2 #U1 #U2 #HV1 #HV2 #HW12 #HU12 #H1 #H2 destruct + lapply (aaa_lifts G L2 … B … (L2.ⓓW2) … HV2) -HV2 /3 width=2 by drops_drop, drops_refl/ #HV2 + lapply (IHT (ⓓ{q}W2.U2) … HT) -IHT -HT /2 width=1 by cpx_bind/ -L1 #H + elim (aaa_inv_abbr … H) -H /3 width=3 by aaa_abbr, aaa_appl/ + ] +| #G #L1 #V1 #T1 #A #_ #_ #IHV #IHT #X2 #HX #L2 #HL12 + elim (lfpx_inv_flat … HL12) -HL12 #HV #HT + elim (cpx_inv_cast1 … HX) -HX + [ * #V2 #T2 #HV12 #HT12 #H destruct ] /3 width=1 by aaa_cast/ +] +qed-. + +lemma cpx_aaa_conf: ∀h,G,L,T1,A. ⦃G, L⦄ ⊢ T1 ⁝ A → + ∀T2. ⦃G, L⦄ ⊢ T1 ⬈[h] T2 → ⦃G, L⦄ ⊢ T2 ⁝ A. +/2 width=6 by cpx_aaa_conf_lfpx/ qed-. + +lemma lfpx_aaa_conf: ∀h,G,L1,T,A. ⦃G, L1⦄ ⊢ T ⁝ A → + ∀L2. ⦃G, L1⦄ ⊢ ⬈[h, T] L2 → ⦃G, L2⦄ ⊢ T ⁝ A. +/2 width=6 by cpx_aaa_conf_lfpx/ qed-. diff --git a/matita/matita/contribs/lambdadelta/basic_2/rt_transition/lpx_aaa.ma b/matita/matita/contribs/lambdadelta/basic_2/rt_transition/lpx_aaa.ma deleted file mode 100644 index 6f4b3b2a0..000000000 --- a/matita/matita/contribs/lambdadelta/basic_2/rt_transition/lpx_aaa.ma +++ /dev/null @@ -1,83 +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/static/aaa_lift.ma". -include "basic_2/static/lsuba_aaa.ma". -include "basic_2/reduction/lpx_drop.ma". - -(* SN EXTENDED PARALLEL REDUCTION FOR LOCAL ENVIRONMENTS ********************) - -(* Properties on atomic arity assignment for terms **************************) - -(* Note: lemma 500 *) -lemma cpx_lpx_aaa_conf: ∀h,o,G,L1,T1,A. ⦃G, L1⦄ ⊢ T1 ⁝ A → - ∀T2. ⦃G, L1⦄ ⊢ T1 ➡[h, o] T2 → - ∀L2. ⦃G, L1⦄ ⊢ ➡[h, o] L2 → ⦃G, L2⦄ ⊢ T2 ⁝ A. -#h #o #G #L1 #T1 #A #H elim H -G -L1 -T1 -A -[ #o #L1 #s #X #H - elim (cpx_inv_sort1 … H) -H // * // -| #I #G #L1 #K1 #V1 #B #i #HLK1 #_ #IHV1 #X #H #L2 #HL12 - elim (cpx_inv_lref1 … H) -H - [ #H destruct - elim (lpx_drop_conf … HLK1 … HL12) -L1 #X #H #HLK2 - elim (lpx_inv_pair1 … H) -H - #K2 #V2 #HK12 #HV12 #H destruct /3 width=6 by aaa_lref/ - | * #J #Y #Z #V2 #H #HV12 #HV2 - lapply (drop_mono … H … HLK1) -H #H destruct - elim (lpx_drop_conf … HLK1 … HL12) -L1 #Z #H #HLK2 - elim (lpx_inv_pair1 … H) -H #K2 #V0 #HK12 #_ #H destruct - /3 width=8 by aaa_lift, drop_fwd_drop2/ - ] -| #a #G #L1 #V1 #T1 #B #A #_ #_ #IHV1 #IHT1 #X #H #L2 #HL12 - elim (cpx_inv_abbr1 … H) -H * - [ #V2 #T2 #HV12 #HT12 #H destruct /4 width=2 by lpx_pair, aaa_abbr/ - | #T2 #HT12 #HT2 #H destruct -IHV1 - /4 width=8 by lpx_pair, aaa_inv_lift, drop_drop/ - ] -| #a #G #L1 #V1 #T1 #B #A #_ #_ #IHV1 #IHT1 #X #H #L2 #HL12 - elim (cpx_inv_abst1 … H) -H #V2 #T2 #HV12 #HT12 #H destruct - /4 width=1 by lpx_pair, aaa_abst/ -| #G #L1 #V1 #T1 #B #A #_ #_ #IHV1 #IHT1 #X #H #L2 #HL12 - elim (cpx_inv_appl1 … H) -H * - [ #V2 #T2 #HV12 #HT12 #H destruct /3 width=3 by aaa_appl/ - | #b #V2 #W1 #W2 #U1 #U2 #HV12 #HW12 #HU12 #H1 #H2 destruct - lapply (IHV1 … HV12 … HL12) -IHV1 -HV12 #HV2 - lapply (IHT1 (ⓛ{b}W2.U2) … HL12) -IHT1 /2 width=1 by cpx_bind/ -L1 #H - elim (aaa_inv_abst … H) -H #B0 #A0 #HW1 #HU2 #H destruct - /5 width=6 by lsuba_aaa_trans, lsuba_beta, aaa_abbr, aaa_cast/ - | #b #V #V2 #W1 #W2 #U1 #U2 #HV1 #HV2 #HW12 #HU12 #H1 #H2 destruct - lapply (aaa_lift G L2 … B … (L2.ⓓW2) … HV2) -HV2 /2 width=2 by drop_drop/ #HV2 - lapply (IHT1 (ⓓ{b}W2.U2) … HL12) -IHT1 /2 width=1 by cpx_bind/ -L1 #H - elim (aaa_inv_abbr … H) -H /3 width=3 by aaa_abbr, aaa_appl/ - ] -| #G #L1 #V1 #T1 #A #_ #_ #IHV1 #IHT1 #X #H #L2 #HL12 - elim (cpx_inv_cast1 … H) -H - [ * #V2 #T2 #HV12 #HT12 #H destruct /3 width=1 by aaa_cast/ - | -IHV1 /2 width=1 by/ - | -IHT1 /2 width=1 by/ - ] -] -qed-. - -lemma cpx_aaa_conf: ∀h,o,G,L,T1,A. ⦃G, L⦄ ⊢ T1 ⁝ A → ∀T2. ⦃G, L⦄ ⊢ T1 ➡[h, o] T2 → ⦃G, L⦄ ⊢ T2 ⁝ A. -/2 width=7 by cpx_lpx_aaa_conf/ qed-. - -lemma lpx_aaa_conf: ∀h,o,G,L1,T,A. ⦃G, L1⦄ ⊢ T ⁝ A → ∀L2. ⦃G, L1⦄ ⊢ ➡[h, o] L2 → ⦃G, L2⦄ ⊢ T ⁝ A. -/2 width=7 by cpx_lpx_aaa_conf/ qed-. - -lemma cpr_aaa_conf: ∀G,L,T1,A. ⦃G, L⦄ ⊢ T1 ⁝ A → ∀T2. ⦃G, L⦄ ⊢ T1 ➡ T2 → ⦃G, L⦄ ⊢ T2 ⁝ A. -/3 width=5 by cpx_aaa_conf, cpr_cpx/ qed-. - -lemma lpr_aaa_conf: ∀G,L1,T,A. ⦃G, L1⦄ ⊢ T ⁝ A → ∀L2. ⦃G, L1⦄ ⊢ ➡ L2 → ⦃G, L2⦄ ⊢ T ⁝ A. -/3 width=5 by lpx_aaa_conf, lpr_lpx/ qed-. diff --git a/matita/matita/contribs/lambdadelta/basic_2/rt_transition/partial.txt b/matita/matita/contribs/lambdadelta/basic_2/rt_transition/partial.txt index fc1c009ca..716b8611f 100644 --- a/matita/matita/contribs/lambdadelta/basic_2/rt_transition/partial.txt +++ b/matita/matita/contribs/lambdadelta/basic_2/rt_transition/partial.txt @@ -1,6 +1,6 @@ cpg.ma cpg_simple.ma cpg_drops.ma cpg_lsubr.ma cpx.ma cpx_simple.ma cpx_drops.ma cpx_lsubr.ma -lfpx.ma lfpx_length.ma lfpx_drops.ma lfpx_fqup.ma lfpx_frees.ma +lfpx.ma lfpx_length.ma lfpx_drops.ma lfpx_fqup.ma lfpx_frees.ma lfpx_aaa.ma cpm.ma cpm_simple.ma cpm_drops.ma cpm_lsubr.ma cpm_cpx.ma cpr.ma cpr_drops.ma -lfpr.ma lfpr_length.ma lfpr_drops.ma lfpr_fqup.ma lfpr_frees.ma lfpr_lfpx.ma lfpr_lfpr.ma +lfpr.ma lfpr_length.ma lfpr_drops.ma lfpr_fqup.ma lfpr_frees.ma lfpr_aaa.ma lfpr_lfpx.ma lfpr_lfpr.ma 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 c9380ba24..78203c527 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 @@ -138,19 +138,19 @@ table { } ] [ { "context-sensitive rt-reduction" * } { - [ "lpx_lleq" + "lpx_aaa" * ] + [ "lpx_lleq" * ] [ "cpx_lreq" + "cpx_fqus" + "cpx_llpx_sn" + "cpx_lleq" * ] } ] *) [ { "t-bound context-sensitive rt-transition" * } { - [ "lfpr ( ⦃?,?⦄ ⊢ ➡[?,?] ? )" "lfpr_length" + "lfpr_drops" + "lfpr_fqup" + "lfpr_frees" + "lfpr_lfpx" + "lfpr_lfpr" * ] + [ "lfpr ( ⦃?,?⦄ ⊢ ➡[?,?] ? )" "lfpr_length" + "lfpr_drops" + "lfpr_fqup" + "lfpr_frees" + "lfpr_aaa" + "lfpr_lfpx" + "lfpr_lfpr" * ] [ "cpr ( ⦃?,?⦄ ⊢ ? ➡[?] ? )" "cpr_drops" (* + "cpr_llpx_sn" + "cpr_cir" *) * ] [ "cpm ( ⦃?,?⦄ ⊢ ? ➡[?,?] ? )" "cpm_simple" + "cpm_drops" + "cpm_lsubr" + "cpm_cpx" * ] } ] [ { "uncounted context-sensitive rt-transition" * } { - [ "lfpx ( ⦃?,?⦄ ⊢ ⬈[?,?] ? )" "lfpx_length" + "lfpx_drops" + "lfpx_fqup" + "lfpx_frees" * ] + [ "lfpx ( ⦃?,?⦄ ⊢ ⬈[?,?] ? )" "lfpx_length" + "lfpx_drops" + "lfpx_fqup" + "lfpx_frees" + "lfpx_aaa" * ] [ "cpx ( ⦃?,?⦄ ⊢ ? ⬈[?] ? )" "cpx_simple" + "cpx_drops" + "cpx_lsubr" * ] } ]