class "sky"
[ { "rt-computation" * } {
(*
- [ { "evaluation for context-sensitive rt-reduction" * } {
- [ [ "" ] "cpxe ( β¦?,?β¦ β’ β‘*[?,?] πβ¦?β¦ )" * ]
- }
- ]
- [ { "evaluation for context-sensitive reduction" * } {
- [ [ "" ] "cpre ( β¦?,?β¦ β’ β‘* πβ¦?β¦ )" "cpre_cpre" * ]
- }
- ]
- [ { "strongly normalizing qrst-computation" * } {
- [ [ "" ] "fsb ( β¦₯[?,?] β¦?,?,?β¦ )" "fsb_alt ( β¦₯β¦₯[?,?] β¦?,?,?β¦ )" "fsb_aaa" + "fsb_csx" * ]
- }
- ]
- [ { "strongly normalizing rt-computation" * } {
- [ [ "" ] "llsx_csx" * ]
- [ [ "" ] "csx_fpbs" * ]
- }
- ]
- [ { "parallel qrst-computation" * } {
- [ [ "" ] "fpbg ( β¦?,?,?β¦ >β[?,?] β¦?,?,?β¦ )" "fpbg_lift" + "fpbg_fleq" + "fpbg_fpbs" + "fpbg_fpbg" * ]
- [ [ "" ] "fpbs_alt" + "fpbs_aaa" + "fpbs_fpb" + "fpbs_fpbs" * ]
- }
- ]
[ { "decomposed rt-computation" * } {
[ [ "" ] "scpds ( β¦?,?β¦ β’ ? β’*β‘*[?,?,?] ? )" "scpds_lift" + "scpds_aaa" + "scpds_scpds" * ]
}
]
*)
[ { "uncounted context-sensitive parallel rst-computation" * } {
- [ [ "for closures" ] "fpbs" + "( β¦?,?,?β¦ β₯[?,?] β¦?,?,?β¦ )" "fpbs_fqup" + "fpbs_fqus" + "fpbs_cpxs" + "fpbs_lfpxs" * ]
+ [ [ "strongly normalizing for closures" ] "fsb" + "( β₯[?,?] πβ¦?,?,?β¦ )" "fsb_ffdeq" + "fsb_aaa" + "fsb_csx" + "fsb_fpbg" * ]
+ [ [ "proper for closures" ] "fpbg" + "( β¦?,?,?β¦ >[?,?] β¦?,?,?β¦ )" "fpbg_fqup" + "fpbg_cpxs" + "fpbg_lfpxs" + "fpbg_fpbs" + "fpbg_fpbg" * ]
+ [ [ "for closures" ] "fpbs" + "( β¦?,?,?β¦ β₯[?,?] β¦?,?,?β¦ )" "fpbs_fqup" + "fpbs_fqus" + "fpbs_aaa" + "fpbs_cpx" + "fpbs_fpb" + "fpbs_cpxs" + "fpbs_lpxs" + "fpbs_lfpxs" + "fpbs_csx" + "fpbs_fpbs" * ]
}
]
[ { "uncounted context-sensitive parallel rt-computation" * } {
[ [ "refinement for lenvs on selected entries" ] "lsubsx" + "( ? β’ ? ββ§[?,?,?] ? )" "lsubsx_lfsx" + "lsubsx_lsubsx" * ]
[ [ "strongly normalizing for lenvs on referred entries" ] "lfsx" + "( ? β’ β¬*[?,?,?] πβ¦?β¦ )" "lfsx_drops" + "lfsx_fqup" + "lfsx_cpx" + "lfsx_cpxs" + "lfsx_lfpxs" + "lfsx_lfsx" * ]
[ [ "strongly normalizing for term vectors" ] "csx_vector" + "( β¦?,?β¦ β’ β¬*[?,?] πβ¦?β¦ )" "csx_cnx_vector" + "csx_csx_vector" * ]
- [ [ "strongly normalizing for terms" ] "csx" + "( β¦?,?β¦ β’ β¬*[?,?] πβ¦?β¦ )" "csx_simple" + "csx_simple_theq" + "csx_drops" + "csx_fqus" + "csx_lsubr" + "csx_lfdeq" + "csx_aaa" + "csx_gcp" + "csx_gcr" + "csx_lfpx" + "csx_cnx" + "csx_cpxs" + "csx_lfpxs" + "csx_csx" * ]
+ [ [ "strongly normalizing for terms" ] "csx" + "( β¦?,?β¦ β’ β¬*[?,?] πβ¦?β¦ )" "csx_simple" + "csx_simple_theq" + "csx_drops" + "csx_fqus" + "csx_lsubr" + "csx_lfdeq" + "csx_ffdeq" + "csx_aaa" + "csx_gcp" + "csx_gcr" + "csx_lfpx" + "csx_cnx" + "csx_fpbq" + "csx_cpxs" + "csx_lfpxs" + "csx_csx" * ]
[ [ "for lenvs on referred entries" ] "lfpxs" + "( β¦?,?β¦ β’ β¬*[?,?] ? )" "lfpxs_length" + "lfpxs_drops" + "lfpxs_fqup" + "lfpxs_lfdeq" + "lfpxs_ffdeq" + "lfpxs_aaa" + "lfpxs_cpxs" + "lfpxs_lpxs" + "lfpxs_lfpxs" * ]
[ [ "for lenvs on all entries" ] "lpxs" + "( β¦?,?β¦ β’ β¬*[?] ? )" "lpxs_length" + "lpxs_lpx" + "lpxs_cpxs" * ]
[ [ "for binders" ] "cpxs_ext" + "( β¦?,?β¦ β’ ? β¬*[?] ? )" * ]
[ [ "for lenvs on referred entries" ] "lfpx" + "( β¦?,?β¦ β’ β¬[?,?] ? )" "lfpx_length" + "lfpx_drops" + "lfpx_fquq" + "lfpx_fqup" + "lfpx_fsle" + "lfpx_lfdeq" + "lfpx_aaa" + "lfpx_lpx" + "lfpx_lfpx" * ]
[ [ "for lenvs on all entries" ] "lpx" + "( β¦?,?β¦ β’ β¬[?] ? )" * ]
[ [ "for binders" ] "cpx_ext" + "( β¦?,?β¦ β’ ? β¬[?] ? )" * ]
- [ [ "for terms" ] "cpx" + "( β¦?,?β¦ β’ ? β¬[?] ? )" "cpx_simple" + "cpx_drops" + "cpx_fqus" + "cpx_lsubr" + "cpx_lfeq" + "cpx_lfdeq" * ]
+ [ [ "for terms" ] "cpx" + "( β¦?,?β¦ β’ ? β¬[?] ? )" "cpx_simple" + "cpx_drops" + "cpx_fqus" + "cpx_lsubr" + "cpx_lfeq" + "cpx_lfdeq" + "cpx_ffdeq" * ]
}
]
[ { "counted context-sensitive parallel rt-transition" * } {
}
]
[ { "degree-based equivalence" * } {
- [ [ "for closures on referred entries" ] "ffdeq" + "( β¦?,?,?β¦ β[?,?] β¦?,?,?β¦ )" "ffdeq_fqup" + "ffdeq_fqus" + "ffdeq_ffdeq" * ]
+ [ [ "for closures on referred entries" ] "ffdeq" + "( β¦?,?,?β¦ β[?,?] β¦?,?,?β¦ )" "ffdeq_fqup" + "ffdeq_fqus" + "ffdeq_lfeq" + "ffdeq_ffdeq" * ]
[ [ "for lenvs on referred entries" ] "lfdeq" + "( ? β[?,?,?] ? )" "lfdeq_length" + "lfdeq_drops" + "lfdeq_fqup" + "lfdeq_fqus" + "lfdeq_lfeq" + "lfdeq_lfdeq" * ]
}
]
class "italic" { 2 }
(*
+ [ { "evaluation for context-sensitive rt-reduction" * } {
+ [ [ "" ] "cpxe ( β¦?,?β¦ β’ β‘*[?,?] πβ¦?β¦ )" * ]
+ }
+ ]
+ [ { "evaluation for context-sensitive reduction" * } {
+ [ [ "" ] "cpre ( β¦?,?β¦ β’ β‘* πβ¦?β¦ )" "cpre_cpre" * ]
+ }
+ ]
[ { "normal forms for context-sensitive rt-reduction" * } {
[ [ "" ] "cnx_crx" + "cnx_cix" * ]
}
[ [ "" ] "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" * ]
}
[ [ "" ] "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" * ]
*)