]
[ { "context-sensitive rt-reduction" * } {
[ "lpx_lleq" * ]
- [ "cpx_lreq" + "cpx_fqus" + "cpx_llpx_sn" + "cpx_lleq" * ]
+ [ "cpx_lreq" + "cpx_llpx_sn" + "cpx_lleq" * ]
}
]
*)
]
[ { "uncounted context-sensitive rt-transition" * } {
[ "lfpx ( ⦃?,?⦄ ⊢ ⬈[?,?] ? )" "lfpx_length" + "lfpx_drops" + "lfpx_fqup" + "lfpx_frees" + "lfpx_aaa" * ]
- [ "cpx ( ⦃?,?⦄ ⊢ ? ⬈[?] ? )" "cpx_simple" + "cpx_drops" + "cpx_lsubr" * ]
+ [ "cpx ( ⦃?,?⦄ ⊢ ? ⬈[?] ? )" "cpx_simple" + "cpx_drops" + "cpx_fqus" + "cpx_lsubr" * ]
}
]
[ { "counted context-sensitive rt-transition" * } {
}
]
[ { "atomic arity assignment" * } {
- [ "aaa ( ⦃?,?⦄ ⊢ ? ⁝ ? )" "aaa_drops" + "aaa_fqus" + "aaa_lfeq" + "aaa_aaa" * ]
+ [ "aaa ( ⦃?,?⦄ ⊢ ? ⁝ ? )" "aaa_drops" + "aaa_fqus" + "aaa_lfdeq" + "aaa_aaa" * ]
}
]
- [ { "equivalence for closures on referred entries" * } {
- [ "ffeq ( ⦃?,?,?⦄ ≡ ⦃?,?,?⦄ )" "ffeq_freq" * ]
+ [ { "degree-based equivalence for closures on referred entries" * } {
+ [ "ffdeq ( ⦃?,?,?⦄ ≡[?,?] ⦃?,?,?⦄ )" "ffdeq_fqup" + "ffdeq_ffdeq" * ]
}
]
- [ { "equivalence for local environments on referred entries" * } {
- [ "lfeq ( ? ≡[?] ? )" "lfeq_length" + "lfeq_lreq" + "lfeq_fqup" + "lfeq_lfeq" * ]
+ [ { "degree-based equivalence for local environments on referred entries" * } {
+ [ "lfdeq ( ? ≡[?,?,?] ? )" "lfdeq_length" + "lfdeq_fqup" + "lfdeq_lfdeq" * ]
}
]
[ { "generic extension on referred entries" * } {
}
]
[ { "context-sensitive free variables" * } {
- [ "frees ( ? ⊢ 𝐅*⦃?⦄ ≡ ? )" "frees_weight" + "frees_lreq" + "frees_drops" + "frees_fqup" + "frees_frees" * ]
+ [ "frees ( ? ⊢ 𝐅*⦃?⦄ ≡ ? )" "frees_weight" + "frees_drops" + "frees_fqup" + "frees_frees" * ]
}
]
[ { "restricted ref. for local env." * } {
]
[ { "generic relocation for terms" * } {
[ "lifts_vector ( ⬆*[?] ? ≡ ? )" "lifts_lifts_vector" * ]
- [ "lifts ( ⬆*[?] ? ≡ ? )" "lifts_simple" + "lifts_weight" + "lifts_lifts" * ]
+ [ "lifts ( ⬆*[?] ? ≡ ? )" "lifts_simple" + "lifts_weight" + "lifts_tdeq" + "lifts_lifts" * ]
}
]
[ { "ranged equivalence for local environments" * } {