- [ { "unbound context-sensitive parallel rt-transition" * } {
- [ [ "normal form for terms" ] "cnx" + "( ⦃?,?⦄ ⊢ ⬈[?,?] 𝐍⦃?⦄ )" "cnx_simple" + "cnx_drops" + "cnx_cnx" * ]
- [ [ "for lenvs on referred entries" ] "rpx" + "( ⦃?,?⦄ ⊢ ⬈[?,?] ? )" "rpx_length" + "rpx_drops" + "rpx_fqup" + "rpx_fsle" + "rpx_rdeq" + "rpx_lpx" + "rpx_rpx" * ]
- [ [ "for lenvs on all entries" ] "lpx" + "( ⦃?,?⦄ ⊢ ⬈[?] ? )" "lpx_length" + "lpx_drops" + "lpx_fquq" + "lpx_fsle" + "lpx_rdeq" + "lpx_aaa" * ]
- [ [ "for binders" ] "cpx_ext" + "( ⦃?,?⦄ ⊢ ? ⬈[?] ? )" * ]
- [ [ "for terms" ] "cpx" + "( ⦃?,?⦄ ⊢ ? ⬈[?] ? )" "cpx_simple" + "cpx_drops" + "cpx_fqus" + "cpx_lsubr" + "cpx_req" + "cpx_rdeq" + "cpx_fdeq" * ]
+ [ { "extended parallel rst-transition" * } {
+ [ [ "proper for closures" ] "fpbc" + "( ❨?,?,?❩ ≻ ❨?,?,?❩ )" "fpbc_fqup" + "fpbc_feqg" + "fpbc_lpx" + "fpbc_fpb" * ]
+ [ [ "for closures" ] "fpb" + "( ❨?,?,?❩ ≽ ❨?,?,?❩ )" "fpb_fqup" + "fpb_feqg" + "fpb_aaa" + "fpb_lpx" * ]
+ }
+ ]
+ [ { "extended context-sensitive parallel rt-transition" * } {
+ [ [ "normal form for terms" ] "cnx" + "( ❨?,?❩ ⊢ ⬈𝐍 ? )" "cnx_simple" + "cnx_drops" + "cnx_basic" + "cnx_cnx" * ]
+ [ [ "for lenvs on referred entries" ] "rpx" + "( ❨?,?❩ ⊢ ⬈[?] ? )" "rpx_length" + "rpx_drops" + "rpx_fqup" + "rpx_fsle" + "rpx_reqg" + "rpx_reqx" + "rpx_lpx" + "rpx_rpx" * ]
+ [ [ "for lenvs on all entries" ] "lpx" + "( ❨?,?❩ ⊢ ⬈ ? )" "lpx_length" + "lpx_drops" + "lpx_fquq" + "lpx_fsle" + "lpx_reqg" + "lpx_aaa" * ]
+ [ [ "for binders" ] "cpx_ext" + "( ❨?,?❩ ⊢ ? ⬈ ? )" * ]
+ [ [ "for terms" ] "cpx" + "( ❨?,?❩ ⊢ ? ⬈ ? )" "cpx_simple" + "cpx_drops" + "cpx_drops_basic" + "cpx_fqus" + "cpx_lsubr" + "cpx_req" + "cpx_reqg" + "cpx_feqg" * ]