]
class "cyan"
[ { "computation" * } {
- [ { "context-sensitive extended evaluation" * } {
+ [ { "evaluation for context-sensitive extended reduction" * } {
[ "cpxe ( β¦?,?β¦ β’ β‘*[?,?] πβ¦?β¦ )" * ]
}
]
- [ { "context-sensitive evaluation" * } {
+ [ { "evaluation for context-sensitive reduction" * } {
[ "cpre ( β¦?,?β¦ β’ β‘* πβ¦?β¦ )" "cpre_cpre" * ]
}
]
}
]
[ { "strongly normalizing extended computation" * } {
- [ "lsx ( ? β’ β¬*[?,?,?] ? )" "lsx_cpxs" + "lsx_csx" * ]
+ [ "lsx ( ? β’ β¬*[?,?,?,?] ? )" "lsx_cpxs" + "lsx_csx" * ]
[ "csx_vector ( β¦?,?β¦ β’ β¬*[?,?] ? )" "csx_tstc_vector" + "csx_aaa" * ]
[ "csx ( β¦?,?β¦ β’ β¬*[?,?] ? )" "csx_alt ( β¦?,?β¦ β’ β¬β¬*[?,?] ? )" "csx_lift" + "csx_lpx" + "csx_fpbs" * ]
}
[ "fpb ( β¦?,?,?β¦ β½[?,?] β¦?,?,?β¦ )" "fpb_lift" + "fpb_aaa" * ]
}
]
- [ { "context-sensitive extended normal forms" * } {
- [ "cnx ( β¦?,?β¦ β’ π[?,?]β¦?β¦ )" "cnx_lift" + "cnx_crx" + "cnx_cix" * ]
+ [ { "normal forms for context-sensitive extended reduction" * } {
+ [ "cnx ( β¦?,?β¦ β’ β‘[?,?] πβ¦?β¦ )" "cnx_lift" + "cnx_crx" + "cnx_cix" * ]
}
]
[ { "context-sensitive extended reduction" * } {
- [ "lpx ( β¦?,?β¦ β’ β‘[?,?] ? )" "lpx_ldrop" + "lpx_lleq" + "lpx_aaa" * ]
- [ "cpx ( β¦?,?β¦ β’ ? β‘[?,?] ? )" "cpx_lift" + "cpx_lleq" + "cpx_cix" * ]
+ [ "lpx ( β¦?,?β¦ β’ β‘[?,?] ? )" "lpx_ldrop" + "lpx_cpys" + "lpx_lleq" + "lpx_aaa" * ]
+ [ "cpx ( β¦?,?β¦ β’ ? β‘[?,?] ? )" "cpx_lift" + "cpx_cpys" + "cpx_lleq" + "cpx_cix" * ]
}
]
- [ { "context-sensitive extended irreducible forms" * } {
- [ "cix ( β¦?,?β¦ β’ π[?,?]β¦?β¦ )" "cix_append" + "cix_lift" * ]
+ [ { "irreducible forms for context-sensitive extended reduction" * } {
+ [ "cix ( β¦?,?β¦ β’ β‘[?,?] πβ¦?β¦ )" "cix_append" + "cix_lift" * ]
}
]
- [ { "context-sensitive extended reducible forms" * } {
- [ "crx ( β¦?,?β¦ β’ π[?,?]β¦?β¦ )" "crx_append" + "crx_lift" * ]
+ [ { "reducible forms for context-sensitive extended reduction" * } {
+ [ "crx ( β¦?,?β¦ β’ β‘[?,?] πβ¦?β¦ )" "crx_append" + "crx_lift" * ]
}
]
- [ { "context-sensitive normal forms" * } {
- [ "cnr ( β¦?,?β¦ β’ πβ¦?β¦ )" "cnr_lift" + "cnr_crr" + "cnr_cir" * ]
+ [ { "normal forms for context-sensitive reduction" * } {
+ [ "cnr ( β¦?,?β¦ β’ β‘ πβ¦?β¦ )" "cnr_lift" + "cnr_crr" + "cnr_cir" * ]
}
]
[ { "context-sensitive reduction" * } {
[ "cpr ( β¦?,?β¦ β’ ? β‘ ? )" "cpr_lift" + "cpr_cir" * ]
}
]
- [ { "context-sensitive irreducible forms" * } {
- [ "cir ( β¦?,?β¦ β’ πβ¦?β¦ )" "cir_append" + "cir_lift" * ]
+ [ { "irreducible forms for context-sensitive reduction" * } {
+ [ "cir ( β¦?,?β¦ β’ β‘ πβ¦?β¦ )" "cir_append" + "cir_lift" * ]
}
]
- [ { "context-sensitive reducible forms" * } {
- [ "crr ( β¦?,?β¦ β’ πβ¦?β¦ )" "crr_append" + "crr_lift" * ]
+ [ { "reducible forms for context-sensitive reduction" * } {
+ [ "crr ( β¦?,?β¦ β’ β‘ πβ¦?β¦ )" "crr_append" + "crr_lift" * ]
}
]
}
}
]
[ { "contxt-sensitive extended multiple substitution" * } {
- [ "cpys ( β¦?,?β¦ β’ ? βΆ*Γ[?,?] ? )" "cpys_alt ( β¦?,?β¦ β’ ? βΆβΆ*Γ[?,?] ? )" "cpys_lift" + "cpys_cpys" * ]
+ [ "cpys ( β¦?,?β¦ β’ ? βΆ*[?,?] ? )" "cpys_alt ( β¦?,?β¦ β’ ? βΆβΆ*[?,?] ? )" "cpys_lift" + "cpys_cpys" * ]
}
]
[ { "iterated structural successor for closures" * } {
[ "fqup ( β¦?,?,?β¦ β+ β¦?,?,?β¦ )" "fqup_fqup" * ]
}
]
- [ { "generic local env. slicing" * } {
- [ "ldrops ( β©*[?] ? β‘ ? )" "ldrops_ldrop" + "ldrops_ldrops" * ]
+ [ { "iterated local env. slicing" * } {
+ [ "ldrops ( β©*[?,?] ? β‘ ? )" "ldrops_ldrop" + "ldrops_ldrops" * ]
}
]
[ { "generic term relocation" * } {
class "orange"
[ { "relocation" * } {
[ { "contxt-sensitive extended ordinary substitution" * } {
- [ "cpy ( β¦?,?β¦ β’ ? βΆΓ[?,?] ? )" "cpy_lift" + "cpy_cpy" * ]
+ [ "cpy ( β¦?,?β¦ β’ ? βΆ[?,?] ? )" "cpy_lift" + "cpy_cpy" * ]
}
]
[ { "local env. ref. for extended substitution" * } {
}
]
[ { "basic local env. slicing" * } {
- [ "ldrop ( β©[?,?] ? β‘ ? )" "ldrop_append" + "ldrop_lpx_sn" + "ldrop_ldrop" * ]
+ [ "ldrop ( β©[?,?,?] ? β‘ ? )" "ldrop_append" + "ldrop_lpx_sn" + "ldrop_ldrop" * ]
}
]
[ { "basic term relocation" * } {