[ "cprs (? ⊢ ? ➡* ?)" "cprs_lift" "cprs_delift" "cprs_ltpr" "cprs_lcpr" "cprs_cprs" "cprs_lcprs" "cprs_tstc" "cprs_tstc_vector" * ]
}
]
+ [ { "context-free computation" * } {
+ [ "ltprs ( ? ➡* ? )" "ltprs_alt ( ? ➡➡* ? )" "ltprs_ldrop" "ltprs_ltprs" * ]
+ [ "tprs ( ? ➡* ?)" "tprs_lift" "tprs_tprs" * ]
+ }
+ ]
[ { "local env. ref. for abstract candidates of reducibility" * } {
[ "lsubc ( ? ⊑[?] ? )" "lsubc_ldrop" "lsubc_ldrops" "lsubc_lsuba" * ]
}
[ "crf ( ? ⊢ 𝐑⦃?⦄ )" "crf_append" "cif ( ? ⊢ 𝐈⦃?⦄ )" "cif_append" * ]
}
]
+ [ { "focalized reduction" * } {
+ [ "lfpr_alt ( ⦃?⦄ ➡➡ ⦃?⦄ )" * ]
+ [ "fpr ( ⦃?,?⦄ ➡ ⦃?,?⦄ )" * ]
+ }
+ ]
[ { "context-free normal forms" * } {
[ "thnf ( 𝐇𝐍⦃?⦄ )" * ]
}
}
]
[ { "stratified static type assignment" * } {
- [ "ssta ( ⦃?,?⦄ ⊢ ? •[?,?] ? )" "ssta_lift" "ssta_ltpss" "ssta_aaa" "ssta_ssta" * ]
+ [ "ssta ( ⦃?,?⦄ ⊢ ? •[?,?] ? )" "ssta_lift" "ssta_ltpss_dx" "ssta_ltpss_sn" "ssta_aaa" "ssta_ssta" * ]
}
]
[ { "local env. ref. for atomic arity assignment" * } {
}
]
[ { "atomic arity assignment" * } {
- [ "aaa ( ? ⊢ ? ⁝ ? )" "aaa_lift" "aaa_lifts" "aaa_ltpss" "aaa_aaa" * ]
+ [ "aaa ( ? ⊢ ? ⁝ ? )" "aaa_lift" "aaa_lifts" "aaa_ltpss_dx" "aaa_ltpss_sn" "aaa_aaa" * ]
}
]
[ { "parameters" * } {
}
]
[ { "partial unfold" * } {
- [ "ltpss ( ? ▶*[?,?] ? )" "ltpss_ldrop" "ltpss_tps" "ltpss_tpss" "ltpss_ltpss" * ]
+ [ "ltpss_sn ( ? ⊢ ▶*[?,?] ? )" "ltpss_sn_ldrop" "ltpss_sn_tps" "ltpss_sn_tpss" "ltpss_sn_ltpss_sn" "ltpss_sn_alt ( ? ⊢ ▶▶*[?,?] ? )" * ]
+ [ "ltpss_dx ( ? ▶*[?,?] ? )" "ltpss_dx_ldrop" "ltpss_dx_tps" "ltpss_dx_tpss" "ltpss_dx_ltpss_dx" * ]
[ "tpss ( ? ⊢ ? ▶*[?,?] ? )" "tpss_alt ( ? ⊢ ? ▶▶*[?,?] ? )" "tpss_lift" "tpss_tpss" * ]
}
]
}
]
[ { "local env. ref. for substitution" * } {
- [ "lsubs ( ? ≼[?,?] ? )" "lsubs_lsubs" "lsubs_sfr ( ≽[?,?] ? )" * ]
+ [ "lsubs ( ? ≼[?,?] ? )" "(lsubs_lsubs)" "lsubs_sfr ( ≽[?,?] ? )" * ]
}
]
[ { "basic term relocation" * } {
class "red"
[ { "grammar" * } {
[ { "same head term form" * } {
- [ "tshf ( ? ≈ ? )" "tshf_tshf" * ]
+ [ "tshf ( ? ≈ ? )" "(tshf_tshf)" * ]
}
]
[ { "same top term constructor" * } {
]
[ { "internal syntax" * } {
[ "genv" * ]
- [ "lenv" "lenv_weight ( #{?} )" "lenv_length ( |?| )" "lenv_append ( ? @@ ? )" "lenv_px" * ]
+ [ "lenv" "lenv_weight ( #{?} )" "lenv_length ( |?| )" "lenv_append ( ? @@ ? )" "lenv_px" "lenv_px_bi" * ]
[ "term" "term_weight ( #{?} )" "term_simple ( 𝐒⦃?⦄ )" "term_vector" * ]
[ "item" * ]
}