- [ { "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" * ]
- }
- ]
- [ { "parallel qrst-computation" * } {
- [ [ "" ] "fpbg ( β¦?,?,?β¦ >β[?,?] β¦?,?,?β¦ )" "fpbg_lift" + "fpbg_fleq" + "fpbg_fpbs" + "fpbg_fpbg" * ]
- [ [ "" ] "fpbs_alt" + "fpbs_aaa" + "fpbs_fpb" + "fpbs_fpbs" * ]
- }
- ]