}
]
*)
+ [ { "\"big tree\" parallel computation" * } {
+ [ "yprs ( ? ⊢ ⦃?,?⦄ ≥[g] ⦃?,?⦄ )" "yprs_yprs" "ygt ( ? ⊢ ⦃?,?⦄ >[g] ⦃?,?⦄ )" "ygt_ygt" * ]
+ }
+ ]
+ [ { "\"big tree\" parallel reduction" * } {
+ [ "ypr ( ? ⊢ ⦃?,?⦄ ≽[g] ⦃?,?⦄ )" "ysc ( ? ⊢ ⦃?,?⦄ ≻[g] ⦃?,?⦄ )" * ]
+ }
+ ]
[ { "local env. ref. for stratified native validity" * } {
- [ "lsubsv ( ? ⊢ ? ⊩:⊑[?] ? )" "lsubsv_ldrop" "lsubsv_snv" * ]
+ [ "lsubsv ( ? ⊢ ? ⊩:⊑[?] ? )" "lsubsv_ldrop" + "lsubsv_lsuba" + "lsubsv_ssta" + "lsubsv_dxprs" + "lsubsv_cpcs" + "lsubsv_snv" * ]
}
]
[ { "stratified native validity" * } {
[ "fprs ( ⦃?,?⦄ ➡* ⦃?,?⦄ )" "fprs_aaa" + "fprs_fprs" * ]
}
]
- [ { "\"big tree\" parallel computation" * } {
- [ "yprs ( ? ⊢ ⦃?,?⦄ ≥[g] ⦃?,?⦄ )" "yprs_yprs" "ygt ( ? ⊢ ⦃?,?⦄ >[g] ⦃?,?⦄ )" "ygt_ygt" * ]
- }
- ]
[ { "decomposed extended computation" * } {
[ "dxprs ( ⦃?,?⦄ ⊢ ? •*➡*[?] ? )" "dxprs_lift" + "dxprs_ltpss_dx" + "dxprs_ltpss_sn" + "dxprs_aaa" + "dxpr_lsubss" + "dxprs_dxprs" * ]
}
[ "fpr ( ⦃?,?⦄ ➡ ⦃?,?⦄ )" "fpr_cpr" + "fpr_fpr" * ]
}
]
- [ { "\"big tree\" parallel reduction" * } {
- [ "ypr ( ? ⊢ ⦃?,?⦄ ≽[g] ⦃?,?⦄ )" "ysc ( ? ⊢ ⦃?,?⦄ ≻[g] ⦃?,?⦄ )" * ]
- }
- ]
[ { "context-sensitive normal forms" * } {
[ "cnf ( ? ⊢ 𝐍⦃?⦄ )" "cnf_lift" + "cnf_cif" * ]
}