}
]
[ { "context-sensitive extended reduction" * } {
- [ "lpx ( ⦃?,?⦄ ⊢ ➡[?,?] ? )" "lpx_ldrop" + "lpx_lleq" + "lpx_aaa" * ]
+ [ "lpx ( ⦃?,?⦄ ⊢ ➡[?,?] ? )" "lpx_ldrop" + "lpx_frees" "lpx_lleq" + "lpx_aaa" * ]
[ "cpx ( ⦃?,?⦄ ⊢ ? ➡[?,?] ? )" "cpx_leq" + "cpx_lift" + "cpx_llpx_sn" + "cpx_lleq" + "cpx_cix" * ]
}
]
}
]
[ { "pointwise union for local environments" * } {
- [ "llor ( ? ⩖[?] ? ≡ ? )" * ]
+ [ "llor ( ? ⩖[?] ? ≡ ? )" "llor_ldrop" * ]
}
]
[ { "context-sensitive exclusion from free variables" * } {
- [ "cofrees ( ? ⊢ ? ~ϵ 𝐅*[?]⦃?⦄ )" "cofrees_alt" + "cofrees_lift" * ]
+ [ "frees ( ? ⊢ ? ϵ 𝐅*[?]⦃?⦄ )" "frees_lift" * ]
}
]
[ { "contxt-sensitive extended multiple substitution" * } {