]
(*
class "wine"
- [ { "examples" * } {
- [ { "terms with special features" * } {
- [ "ex_sta_ldec" + "ex_cpr_omega" + "ex_fpbg_refl" + "ex_snv_eta" * ]
- }
- ]
- }
- ]
- class "magenta"
[ { "" * } {
[ { "" * } {
[ "" * ]
}
]
*)
- class "prune"
+ class "magenta"
[ { "dynamic typing" * } {
(*
[ { "local env. ref. for native type assignment" * } {
]
}
]
- class "blue"
+ class "prune"
[ { "equivalence" * } {
[ { "decomposed rt-equivalence" * } {
[ "scpes ( ⦃?,?⦄ ⊢ ? •*⬌*[?,?,?,?] ? )" "scpes_aaa" + "scpes_cpcs" + "scpes_scpes" * ]
]
}
]
- class "sky"
+ class "blue"
[ { "conversion" * } {
[ { "context-sensitive conversion" * } {
[ "cpc ( ⦃?,?⦄ ⊢ ? ⬌ ? )" "cpc_cpc" * ]
}
]
*)
- class "cyan"
+ class "sky"
[ { "rt-computation" * } {
(*
[ { "evaluation for context-sensitive rt-reduction" * } {
[ { "uncounted context-sensitive rt-transition" * } {
(*
[ "lpxs ( ⦃?,?⦄ ⊢ ➡*[?,?] ? )" "lpxs_drop" + "lpxs_lleq" + "lpxs_aaa" + "lpxs_cpxs" + "lpxs_lpxs" * ]
- [ "cpxs_tsts" + "cpxs_tsts_vector" + "cpxs_lreq" + "cpxs_lift" + "cpxs_lleq" + "cpxs_aaa" + "cpxs_cpxs" * ]
+ [ "cpxs_lreq" + "cpxs_lleq" + "cpxs_aaa" * ]
*)
- [ "cpxs ( ⦃?,?⦄ ⊢ ? ⬈*[?] ? )" * ]
+ [ "csx_vector ( ⦃?,?⦄ ⊢ ⬈*[?,?] 𝐒⦃?⦄ )" * ]
+ [ "csx ( ⦃?,?⦄ ⊢ ⬈*[?,?] 𝐒⦃?⦄ )" "csx_cnx" + "csx_cpxs" + "csx_csx" * ]
+ [ "lfpxs ( ⦃?,?⦄ ⊢ ⬈*[?,?] ? )" "lfpxs_length" + "lfpxs_fqup" + "lfpxs_cpxs" * ]
+ [ "cpxs ( ⦃?,?⦄ ⊢ ? ⬈*[?] ? )" "cpxs_tdeq" + "cpxs_tsts" + "cpxs_tsts_vector" + "cpxs_drops" + "cpxs_lsubr" + "cpxs_lfpx" + "cpxs_cnx" + "cpxs_cpxs" * ]
}
]
- [ { "generic reducibility" * } {
- [ "lsubc ( ? ⊢ ? ⫃[?] ? )" "lsubc_drop" + "lsubc_drops" + "lsubc_lsubr" + "lsubc_lsuba" * ]
- [ "gcp_cr ( ⦃?,?,?⦄ ϵ[?] 〚?〛 )" "gcp_aaa" * ]
- [ "gcp" *]
- }
- ]
}
]
- class "water"
+ class "cyan"
[ { "rt-transition" * } {
- [ { "parallel qrst-rtransition" * } {
-(* [ "fpbq ( ⦃?,?,?⦄ ≽[?,?] ⦃?,?,?⦄ )" "fpbq_alt ( ⦃?,?,?⦄ ≽≽[?,?] ⦃?,?,?⦄ )" + "fpbq_aaa" * ] *)
+ [ { "parallel rst-transition" * } {
+ [ "fpbq ( ⦃?,?,?⦄ ≽[?] ⦃?,?,?⦄ )" "fpbq_aaa" * ]
[ "fpb ( ⦃?,?,?⦄ ≻[?,?] ⦃?,?,?⦄ )" (* "fpb_lleq" + "fpb_fleq" *) * ]
}
]
-(*
- [ { "context-sensitive rt-reduction" * } {
- [ "lpx_lleq" * ]
- [ "cpx_lleq" * ]
- }
- ]
-*)
[ { "t-bound context-sensitive rt-transition" * } {
[ "lfpr ( ⦃?,?⦄ ⊢ ➡[?,?] ? )" "lfpr_length" + "lfpr_drops" + "lfpr_fqup" + "lfpr_frees" + "lfpr_aaa" + "lfpr_lfpx" + "lfpr_lfpr" * ]
[ "cpr ( ⦃?,?⦄ ⊢ ? ➡[?] ? )" "cpr_drops" * ]
}
]
[ { "uncounted context-sensitive rt-transition" * } {
- [ "cnx ( ⦃?,?⦄ ⊢ ⬈[?,?] 𝐍⦃?⦄ )" "cnx_simple" + "cnx_drops" * ]
- [ "lfpx ( ⦃?,?⦄ ⊢ ⬈[?,?] ? )" "lfpx_length" + "lfpx_drops" + "lfpx_fqup" + "lfpx_frees" + "lfpx_aaa" * ]
- [ "cpx ( ⦃?,?⦄ ⊢ ? ⬈[?] ? )" "cpx_simple" + "cpx_drops" + "cpx_fqus" + "cpx_lsubr" + "cpx_lfxs" + "cpx_lfdeq" * ]
+ [ "cnx ( ⦃?,?⦄ ⊢ ⬈[?,?] 𝐍⦃?⦄ )" "cnx_simple" + "cnx_drops" + "cnx_cnx" * ]
+ [ "lfpx ( ⦃?,?⦄ ⊢ ⬈[?,?] ? )" "lfpx_length" + "lfpx_drops" + "lfpx_fqup" + "lfpx_frees" + "lfpx_lfdeq" + "lfpx_aaa" + "lfpx_lfpx" * ]
+ [ "cpx ( ⦃?,?⦄ ⊢ ? ⬈[?] ? )" "cpx_simple" + "cpx_drops" + "cpx_fqus" + "cpx_lsubr" + "cpx_lfxs" * ]
}
]
[ { "counted context-sensitive rt-transition" * } {
]
}
]
+ class "water"
+ [ { "iterated static typing" * } {
+ [ { "iterated extension on referred entries" * } {
+ [ "tc_lfxs ( ? ⦻**[?,?] ? )" * ]
+ }
+ ]
+ }
+ ]
class "green"
[ { "static typing" * } {
+ [ { "generic reducibility" * } {
+ [ "lsubc ( ? ⊢ ? ⫃[?] ? )" "lsubc_drops" + "lsubc_lsubr" + "lsubc_lsuba" * ]
+ [ "gcp_cr ( ⦃?,?,?⦄ ϵ[?] 〚?〛 )" "gcp_aaa" * ]
+ [ "gcp" *]
+ }
+ ]
[ { "atomic arity assignment" * } {
[ "lsuba ( ? ⊢ ? ⫃⁝ ? )" "lsuba_drops" + "lsuba_lsubr" + "lsuba_aaa" + "lsuba_lsuba" * ]
[ "aaa ( ⦃?,?⦄ ⊢ ? ⁝ ? )" "aaa_drops" + "aaa_fqus" + "aaa_lfdeq" + "aaa_aaa" * ]
]
[ { "context-sensitive free variables" * } {
[ "lsubf ( ⦃?,?⦄ ⫃𝐅* ⦃?,?⦄ )" "lsubf_frees" * ]
- [ "frees ( ? ⊢ 𝐅*⦃?⦄ ≡ ? )" "frees_weight" + "frees_drops" + "frees_fqup" + "frees_frees" * ]
+ [ "frees ( ? ⊢ 𝐅*⦃?⦄ ≡ ? )" "frees_drops" + "frees_fqup" + "frees_frees" * ]
}
]
[ { "restricted ref. for local env." * } {
[ "append ( ? @@ ? )" "append_length" * ]
}
]
- [ { "degree-based equivalence for terms" * } {
- [ "deq ( ? ≡[?,?] ? ) " "deq_deq" * ]
+ [ { "same top term structure" * } {
+ [ "tsts ( ? ⩳[?,?] ? )" "tsts_simple" + "tsts_tdeq" + "tsts_tsts" + "tsts_simple_vector" * ]
}
]
- [ { "same top term structure" * } {
- [ "tsts ( ? ≂ ? )" "tsts_tsts" + "tsts_vector" * ]
+ [ { "degree-based equivalence for terms" * } {
+ [ "deq ( ? ≡[?,?] ? ) " "deq_deq" * ]
}
]
[ { "closures" * } {