+class "italic" { 2 }
+(*
+ [ { "normal forms for context-sensitive rt-reduction" * } {
+ [ [ "" ] "cnx_crx" + "cnx_cix" * ]
+ }
+ ]
+ [ { "irreducible forms for context-sensitive rt-reduction" * } {
+ [ [ "" ] "cix ( ⦃?,?⦄ ⊢ ➡[?,?] 𝐈⦃?⦄ )" "cix_lift" * ]
+ }
+ ]
+ [ { "reducible forms for context-sensitive rt-reduction" * } {
+ [ [ "" ] "crx ( ⦃?,?⦄ ⊢ ➡[?,?] 𝐑⦃?⦄ )" "crx_lift" * ]
+ }
+ ]
+ [ { "normal forms for context-sensitive reduction" * } {
+ [ [ "" ] "cnr ( ⦃?,?⦄ ⊢ ➡ 𝐍⦃?⦄ )" "cnr_lift" + "cnr_crr" + "cnr_cir" * ]
+ }
+ ]
+ [ { "irreducible forms for context-sensitive reduction" * } {
+ [ [ "" ] "cir ( ⦃?,?⦄ ⊢ ➡ 𝐈⦃?⦄ )" "cir_lift" * ]
+ }
+ ]
+ [ { "reducible forms for context-sensitive reduction" * } {
+ [ [ "" ] "crr ( ⦃?,?⦄ ⊢ ➡ 𝐑⦃?⦄ )" "crr_lift" * ]
+ }
+ ]
+ [ { "unfold" * } {
+ [ [ "" ] "unfold ( ⦃?,?⦄ ⊢ ? ⧫* ? )" * ]
+ }
+ ]
+ [ { "iterated static type assignment" * } {
+ [ [ "" ] "lstas ( ⦃?,?⦄ ⊢ ? •*[?,?] ? )" "lstas_lift" + "lstas_llpx_sn.ma" + "lstas_aaa" + "lstas_da" + "lstas_lstas" * ]
+ }
+ ]
+ [ { "local env. ref. for degree assignment" * } {
+ [ [ "" ] "lsubd ( ? ⊢ ? ⫃▪[?,?] ? )" "lsubd_da" + "lsubd_lsubd" * ]
+ }
+ ]
+ [ { "degree assignment" * } {
+ [ [ "" ] "da ( ⦃?,?⦄ ⊢ ? ▪[?,?] ? )" "da_lift" + "da_aaa" + "da_da" * ]
+ }
+ ]
+ [ { "context-sensitive multiple rt-substitution" * } {
+ [ [ "" ] "cpys ( ⦃?,?⦄ ⊢ ? ▶*[?,?] ? )" "cpys_alt ( ⦃?,?⦄ ⊢ ? ▶▶*[?,?] ? )" "cpys_lift" + "cpys_cpys" * ]
+ }
+ ]
+ [ { "pointwise union for local environments" * } {
+ [ [ "" ] "llor ( ? ⋓[?,?] ? ≡ ? )" "llor_alt" + "llor_drop" * ]
+ }
+ ]
+ [ { "lazy pointwise extension of a relation" * } {
+ [ [ "" ] "llpx_sn" "llpx_sn_alt" + "llpx_sn_alt_rec" + "llpx_sn_tc" + "llpx_sn_lreq" + "llpx_sn_drop" + "llpx_sn_lpx_sn" + "llpx_sn_frees" + "llpx_sn_llor" * ]
+ }
+ ]
+ [ { "global env. slicing" * } {
+ [ [ "" ] "gget ( ⬇[?] ? ≡ ? )" "gget_gget" * ]
+ }
+ ]
+ [ { "context-sensitive ordinary rt-substitution" * } {
+ [ [ "" ] "cpy ( ⦃?,?⦄ ⊢ ? ▶[?,?] ? )" "cpy_lift" + "cpy_nlift" + "cpy_cpy" * ]
+ }
+ ]
+ [ { "local env. ref. for rt-substitution" * } {
+ [ [ "" ] "lsuby ( ? ⊆[?,?] ? )" "lsuby_lsuby" * ]
+ }
+ ]
+ [ { "pointwise extension of a relation" * } {
+ [ [ "" ] "lpx_sn" "lpx_sn_alt" + "lpx_sn_drop" + "lpx_sn_lpx_sn" * ]
+ }
+ ]
+ [ [ "" ] "cpx_lreq" + "cpr_cir" + "fpb_lift" + "fpbq_lift" ]
+ [ [ "" ] "lleq ( ? ≡[?,?] ? )" "lleq_alt" + "lleq_alt_rec" + "lleq_lreq" + "lleq_drop" + "lleq_fqus" + "lleq_llor" + "lleq_lleq" * ]
+*)