- [ { "evaluation for context-sensitive rt-reduction" * } {
- [ [ "" ] "cpxe ( ⦃?,?⦄ ⊢ ➡*[?,?] 𝐍⦃?⦄ )" * ]
- }
- ]
- [ { "evaluation for context-sensitive reduction" * } {
- [ [ "" ] "cpre ( ⦃?,?⦄ ⊢ ➡* 𝐍⦃?⦄ )" "cpre_cpre" * ]
- }
- ]
- [ { "strongly normalizing qrst-computation" * } {
- [ [ "" ] "fsb ( ⦥[?,?] ⦃?,?,?⦄ )" "fsb_alt ( ⦥⦥[?,?] ⦃?,?,?⦄ )" "fsb_aaa" + "fsb_csx" * ]
- }
- ]
- [ { "strongly normalizing rt-computation" * } {
- [ [ "" ] "llsx_csx" * ]
- [ [ "" ] "csx_fpbs" * ]
+ [ { "decomposed rt-computation" * } {
+ [ [ "" ] "scpds ( ⦃?,?⦄ ⊢ ? •*➡*[?,?,?] ? )" "scpds_lift" + "scpds_aaa" + "scpds_scpds" * ]