- class "water"
- [ { "reducibility" * } {
- [ { "context-sensitive focalized reduction" * } {
- [ "cfpr ( ? ⊢ ⦃?,?⦄ ➡ ⦃?,?⦄ )" "cnfpr_ltpss" + "cfpr_aaa" + "cfpr_cpr" + "cfpr_cfpr" * ]
- }
- ]
- [ { "context-free focalized reduction" * } {
- [ "lfpr ( ⦃?⦄ ➡ ⦃?⦄ )" "lfpr_alt ( ⦃?⦄ ➡➡ ⦃?⦄ )" "lfpr_aaa" + "lfpr_cpr" + "lfpr_fpr" + "lfpr_lfpr" * ]
- [ "fpr ( ⦃?,?⦄ ➡ ⦃?,?⦄ )" "fpr_cpr" + "fpr_fpr" * ]
- }
- ]
- [ { "context-sensitive normal forms" * } {
- [ "cnf ( ? ⊢ 𝐍⦃?⦄ )" "cnf_lift" + "cnf_cif" * ]
- }
- ]
- [ { "context-sensitive reduction" * } {
- [ "cpr ( ? ⊢ ? ➡ ? )" "cpr_lift" + "cpr_tpss" + "cpr_ltpss_dx" + "cpr_ltpss_sn" + "cpr_delift" + "cpr_aaa" + "cpr_ltpr" + "cpr_cpr" * ]
- }
- ]
- [ { "context-sensitive reducible forms" * } {
- [ "crf ( ? ⊢ 𝐑⦃?⦄ )" "crf_append" "cif ( ? ⊢ 𝐈⦃?⦄ )" "cif_append" * ]
- }
- ]
- [ { "context-free normal forms" * } {
- [ "thnf ( 𝐇𝐍⦃?⦄ )" * ]
- }
- ]
- [ { "context-free reduction" * } {
- [ "ltpr ( ? ➡ ? )" "ltpr_ldrop" + "ltpr_tps" + "ltpr_ltpss_dx" + "ltpr_ltpss_sn" + "ltpr_aaa" + "ltpr_ltpr" * ]
- [ "tpr ( ? ➡ ? )" "tpr_lift" + "tpr_tps" + "tpr_tpss" + "tpr_delift" + "tpr_tpr" * ]
+ class "cyan"
+ [ { "rt-transition" * } {
+ [ { "context-sensitive parallel t-transition" * } {
+ [ [ "for terms" ] "cpt" + "( ⦃?,?⦄ ⊢ ? ⬆[?,?] ? )" "cpt_drops" + "cpt_fqu" + "cpt_cpm" * ]