[ "lleq ( ? β[?,?] ? )" "lleq_alt" + "lleq_leq" + "lleq_ldrop" + "lleq_fqus" + "lleq_lleq" * ]
}
]
+ [ { "context-sensitive exclusion from free variables" * } {
+ [ "cofrees ( ? β’ ? ~Ο΅ π
*[?]β¦?β¦ )" "cofrees_lift" * ]
+ }
+ ]
+ [ { "contxt-sensitive extended multiple substitution" * } {
+ [ "cpys ( β¦?,?β¦ β’ ? βΆ*[?,?] ? )" "cpys_alt ( β¦?,?β¦ β’ ? βΆβΆ*[?,?] ? )" "cpys_lift" + "cpys_cpys" * ]
+ }
+ ]
[ { "iterated structural successor for closures" * } {
[ "fqus ( β¦?,?,?β¦ β* β¦?,?,?β¦ )" "fqus_alt" + "fqus_fqus" * ]
[ "fqup ( β¦?,?,?β¦ β+ β¦?,?,?β¦ )" "fqup_fqup" * ]
[ "lpx_sn" "lpx_sn_alt" + "lpx_sn_tc" + "lpx_sn_ldrop" + "lpx_sn_lpx_sn" * ]
}
]
- [ { "basic local env. slicing" * } {
+ [ { "contxt-sensitive extended ordinary substitution" * } {
+ [ "cpy ( β¦?,?β¦ β’ ? βΆ[?,?] ? )" "cpy_lift" + "cpy_cpy" * ]
+ }
+ ]
+ [ { "local env. ref. for extended substitution" * } {
+ [ "lsuby ( ? βΓ[?,?] ? )" "lsuby_lsuby" * ]
+ }
+ ]
+ [ { "basic local env. slicing" * } {
[ "ldrop ( β©[?,?,?] ? β‘ ? )" "ldrop_leq" + "ldrop_ldrop" * ]
}
]