}
]
[ { "strongly normalizing rt-computation" * } {
- [ "lcosx ( ? ⊢ ~⬊*[?,?,?] ? )" "lcosx_cpx" * ]
- [ "lsx_drop" + "lsx_lpx" + "lsx_lpxs" + "llsx_csx" * ]
- [ "csx_lleq" + "csx_lpxs" + "csx_fpbs" * ]
+ [ "llsx_csx" * ]
+ [ "csx_fpbs" * ]
}
]
[ { "parallel qrst-computation" * } {
- [ "fpbg ( â¦\83?,?,?â¦\84 >â\89¡[?,?] ⦃?,?,?⦄ )" "fpbg_lift" + "fpbg_fleq" + "fpbg_fpbs" + "fpbg_fpbg" * ]
+ [ "fpbg ( â¦\83?,?,?â¦\84 >â\89\9b[?,?] ⦃?,?,?⦄ )" "fpbg_lift" + "fpbg_fleq" + "fpbg_fpbs" + "fpbg_fpbg" * ]
[ "fpbs ( ⦃?,?,?⦄ ≥[?,?] ⦃?,?,?⦄ )" "fpbs_alt ( ⦃?,?,?⦄ ≥≥[?,?] ⦃?,?,?⦄ )" "fpbs_lift" + "fpbs_aaa" + "fpbs_fpb" + "fpbs_fpbs" * ]
}
]
[ "cprs ( ⦃?,?⦄ ⊢ ? ➡* ?)" "cprs_lift" + "cprs_cprs" * ]
}
]
-*)
+*)
[ { "uncounted context-sensitive rt-computation" * } {
- [ "lfsx ( ? ⊢ ⬈*[?,?,?] 𝐒⦃?⦄ )" "lfsx_fqup" + "lfsx_lfpxs" + "lfsx_lfsx" * ]
+ [ "lsubsx ( ? ⊢ ? ⊆ⓧ[?,?,?] ? )" "lsubsx_lfsx" + "lsubsx_lsubsx" * ]
+ [ "lfsx ( ? ⊢ ⬈*[?,?,?] 𝐒⦃?⦄ )" "lfsx_drops" + "lfsx_fqup" + "lfsx_lfpxs" + "lfsx_lfsx" * ]
[ "csx_vector ( ⦃?,?⦄ ⊢ ⬈*[?,?] 𝐒⦃?⦄ )" "csx_cnx_vector" + "csx_csx_vector" * ]
- [ "csx ( ⦃?,?⦄ ⊢ ⬈*[?,?] 𝐒⦃?⦄ )" "csx_simple" + "csx_simple_theq" + "csx_drops" + "csx_lsubr" + "csx_aaa" + "csx_gcp" + "csx_gcr" + "csx_lfpx" + "csx_cnx" + "csx_cpxs" + "csx_csx" * ]
+ [ "csx ( ⦃?,?⦄ ⊢ ⬈*[?,?] 𝐒⦃?⦄ )" "csx_simple" + "csx_simple_theq" + "csx_drops" + "csx_lsubr" + "csx_lfdeq" + "csx_aaa" + "csx_gcp" + "csx_gcr" + "csx_lfpx" + "csx_cnx" + "csx_cpxs" + "csx_lfpxs" + "csx_csx" * ]
[ "lfpxs ( ⦃?,?⦄ ⊢ ⬈*[?,?] ? )" "lfpxs_length" + "lfpxs_drops" + "lfpxs_fqup" + "lfpxs_lfdeq" + "lfpxs_aaa" + "lfpxs_cpxs" + "lfpxs_lfpxs" * ]
[ "cpxs ( ⦃?,?⦄ ⊢ ? ⬈*[?] ? )" "cpxs_tdeq" + "cpxs_theq" + "cpxs_theq_vector" + "cpxs_drops" + "cpxs_fqus" + "cpxs_lsubr" + "cpxs_lfdeq" + "cpxs_aaa" + "cpxs_lfpx" + "cpxs_cnx" + "cpxs_cpxs" * ]
}
[ { "rt-transition" * } {
[ { "uncounted rst-transition" * } {
[ "fpbq ( ⦃?,?,?⦄ ≽[?] ⦃?,?,?⦄ )" "fpbq_aaa" * ]
- [ "fpb ( ⦃?,?,?⦄ ≻[?,?] ⦃?,?,?⦄ )" "fpb_lfdeq" * ]
+ [ "fpb ( ⦃?,?,?⦄ ≻[?] ⦃?,?,?⦄ )" "fpb_lfdeq" * ]
}
]
[ { "t-bound context-sensitive rt-transition" * } {
}
]
[ { "degree-based equivalence on referred entries" * } {
- [ "ffdeq ( â¦\83?,?,?â¦\84 â\89¡[?,?] ⦃?,?,?⦄ )" "ffdeq_fqup" + "ffdeq_ffdeq" * ]
- [ "lfdeq ( ? â\89¡[?,?,?] ? )" "lfdeq_length" + "lfdeq_drops" + "lfdeq_fqup" + "lfdeq_fqus" + "lfdeq_lfdeq" * ]
+ [ "ffdeq ( â¦\83?,?,?â¦\84 â\89\9b[?,?] ⦃?,?,?⦄ )" "ffdeq_fqup" + "ffdeq_ffdeq" * ]
+ [ "lfdeq ( ? â\89\9b[?,?,?] ? )" "lfdeq_length" + "lfdeq_drops" + "lfdeq_fqup" + "lfdeq_fqus" + "lfdeq_lfdeq" * ]
}
]
[ { "generic extension on referred entries" * } {
}
]
[ { "generic entrywise extension" * } {
- [ "lexs ( ? ⦻*[?,?,?] ? )" "lexs_length" + "lexs_lexs" * ]
+ [ "lex ( ? ⦻[?] ? )" * ]
+ [ "lexs ( ? ⦻*[?,?,?] ? )" "lexs_tc" + "lexs_length" + "lexs_lexs" * ]
}
]
}
}
]
[ { "degree-based equivalence" * } {
- [ "tdeq_ext ( ? â\89¡[?,?] ? ) ( ? â\8a¢ ? â\89¡[?,?] ? )" * ]
- [ "tdeq ( ? â\89¡[?,?] ? )" "tdeq_tdeq" * ]
+ [ "tdeq_ext ( ? â\89\9b[?,?] ? ) ( ? â\8a¢ ? â\89\9b[?,?] ? )" * ]
+ [ "tdeq ( ? â\89\9b[?,?] ? )" "tdeq_tdeq" * ]
}
]
[ { "closures" * } {
}
]
[ { "local environments" * } {
- [ "lenv_ext2" * ]
+ [ "ceq_ext" "ceq_ext_ceq_ext" * ]
+ [ "cext2" * ]
[ "lenv_length ( |?| )" * ]
[ "lenv_weight ( ♯{?} )" * ]
[ "lenv" * ]
}
]
[ { "binders for local environments" * } {
- [ "ext2" "ext2_ext2" * ]
+ [ "ext2" "ext2_tc" + "ext2_ext2" * ]
[ "bind" "bind_weight" * ]
}
]