- [ { "restricted local env. ref." * } {
- [ "lsubr ( ? ⫃ ? )" "lsubr_lsubr" * ]
- }
- ]
- }
- ]
- class "yellow"
- [ { "multiple substitution" * } {
- [ { "lazy equivalence" * } {
- [ "fleq ( ⦃?,?,?⦄ ≡[?] ⦃?,?,?⦄ )" "fleq_fleq" * ]
- [ "lleq ( ? ≡[?,?] ? )" "lleq_alt" + "lleq_alt_rec" + "lleq_leq" + "lleq_drop" + "lleq_fqus" + "lleq_llor" + "lleq_lleq" * ]
- }
- ]
- [ { "lazy pointwise extension of a relation" * } {
- [ "llpx_sn" "llpx_sn_alt" + "llpx_sn_alt_rec" + "llpx_sn_tc" + "llpx_sn_leq" + "llpx_sn_drop" + "llpx_sn_lpx_sn" + "llpx_sn_frees" + "llpx_sn_llor" * ]
- }
- ]
- [ { "pointwise union for local environments" * } {
- [ "llor ( ? ⋓[?,?] ? ≡ ? )" "llor_alt" + "llor_drop" * ]
- }
- ]
- [ { "context-sensitive exclusion from free variables" * } {
- [ "frees ( ? ⊢ ? ϵ 𝐅*[?]⦃?⦄ )" "frees_append" + "frees_leq" + "frees_lift" * ]
- }
- ]
- [ { "contxt-sensitive multiple rt-substitution" * } {
- [ "cpys ( ⦃?,?⦄ ⊢ ? ▶*[?,?] ? )" "cpys_alt ( ⦃?,?⦄ ⊢ ? ▶▶*[?,?] ? )" "cpys_lift" + "cpys_cpys" * ]
- }
- ]
- [ { "iterated structural successor for closures" * } {
- [ "fqus ( ⦃?,?,?⦄ ⊐* ⦃?,?,?⦄ )" "fqus_alt" + "fqus_fqus" * ]
- [ "fqup ( ⦃?,?,?⦄ ⊐+ ⦃?,?,?⦄ )" "fqup_fqup" * ]
- }
- ]
- [ { "iterated local env. slicing" * } {
- [ "drops ( ⬇*[?,?] ? ≡ ? )" "drops_drop" + "drops_drops" * ]
- }
- ]
- [ { "generic term relocation" * } {
- [ "lifts_vector ( ⬆*[?] ? ≡ ? )" "lifts_lift_vector" * ]
- [ "lifts ( ⬆*[?] ? ≡ ? )" "lifts_lift" + "lifts_lifts" * ]
- }
- ]
- [ { "support for multiple relocation" * } {
- [ "mr2 ( @⦃?,?⦄ ≡ ? )" "mr2_plus ( ? + ? )" "mr2_minus ( ? ▭ ? ≡ ? )" "mr2_mr2" * ]
- }
- ]
- }
- ]
- class "orange"
- [ { "substitution" * } {
- [ { "structural successor for closures" * } {
- [ "fquq ( ⦃?,?,?⦄ ⊐⸮ ⦃?,?,?⦄ )" "fquq_alt ( ⦃?,?,?⦄ ⊐⊐⸮ ⦃?,?,?⦄ )" * ]
- [ "fqu ( ⦃?,?,?⦄ ⊐ ⦃?,?,?⦄ )" * ]