category | objects |
|
|
|
|
|
sizes | files | 367 | characters | 431944 | nodes | 1830639 |
propositions | theorems | 128 | lemmas | 1304 | total | 1432 |
concepts | declared | 55 | defined | 84 | total | 139 |
component | plane | files |
|
|
|
examples | terms with special features | ex_cpr_omega |
|
|
|
|
|
|
|||
dynamic typing | local env. ref. for stratified native validity | lsubsv ( ? ⊢ ? ⫃¡[?,?] ? ) | lsubsv_lsuba lsubsv_lsubd lsubsv_lstas lsubsv_scpds lsubsv_cpcs lsubsv_snv |
|
|
|
stratified native validity | shnv ( ⦃?,?⦄ ⊢ ? ¡[?,?,?] ) | shnv_aaa |
|
|
|
|
snv ( ⦃?,?⦄ ⊢ ? ¡[?,?] ) | snv_lift snv_aaa snv_da_lpr snv_lstas snv_lstas_lpr snv_lpr snv_scpes snv_preserve |
|
|
equivalence | decomposed extended equivalence | scpes ( ⦃?,?⦄ ⊢ ? •*⬌*[?,?,?,?] ? ) | scpes_aaa scpes_cpcs scpes_scpes |
|
|
|
context-sensitive equivalence | cpcs ( ⦃?,?⦄ ⊢ ? ⬌* ? ) | cpcs_aaa cpcs_cprs cpcs_cpcs |
|
|
conversion | context-sensitive conversion | cpc ( ⦃?,?⦄ ⊢ ? ⬌ ? ) | cpc_cpc |
|
|
computation | evaluation for context-sensitive extended reduction | cpxe ( ⦃?,?⦄ ⊢ ➡*[?,?] 𝐍⦃?⦄ ) |
|
|
|
|
evaluation for context-sensitive reduction | cpre ( ⦃?,?⦄ ⊢ ➡* 𝐍⦃?⦄ ) | cpre_cpre |
|
|
|
strongly normalizing "big tree" computation | fsb ( ⦃?,?⦄ ⊢ ⦥[?,?] ? ) | fsb_alt ( ⦃?,?⦄ ⊢ ⦥⦥[?,?] ? ) | fsb_aaa fsb_csx |
|
|
strongly normalizing extended computation | lcosx ( ? ⊢ ~⬊*[?,?,?] ? ) | lcosx_cpx |
|
|
|
|
lsx ( ? ⊢ ⬊*[?,?,?,?] ? ) | lsx_alt ( ? ⊢ ⬊⬊*[?,?,?,?] ? ) | lsx_drop lsx_lpx lsx_lpxs llsx_csx |
|
|
|
csx_vector ( ⦃?,?⦄ ⊢ ⬊*[?,?] ? ) | csx_tsts_vector csx_aaa |
|
|
|
|
csx ( ⦃?,?⦄ ⊢ ⬊*[?,?] ? ) | csx_alt ( ⦃?,?⦄ ⊢ ⬊⬊*[?,?] ? ) | csx_lift csx_lleq csx_lpx csx_lpxs csx_fpbs |
|
|
"big tree" parallel computation | fpbg ( ⦃?,?,?⦄ >≡[?,?] ⦃?,?,?⦄ ) | fpbg_lift fpbg_fleq fpbg_fpbg |
|
|
|
|
fpbc ( ⦃?,?,?⦄ ≻≡[?,?] ⦃?,?,?⦄ ) | fpbc_fleq fpbc_fpbs |
|
|
|
|
fpbu ( ⦃?,?,?⦄ ≻[?,?] ⦃?,?,?⦄ ) | fpbu_lift fpbu_lleq fpbu_fleq |
|
|
|
|
fpbs ( ⦃?,?,?⦄ ≥[?,?] ⦃?,?,?⦄ ) | fpbs_alt ( ⦃?,?,?⦄ ≥≥[?,?] ⦃?,?,?⦄ ) | fpbs_lift fpbs_fleq fpbs_aaa fpbs_fpbs fpbs_ext |
|
|
decomposed extended computation | scpds ( ⦃?,?⦄ ⊢ ? •*➡*[?,?,?] ? ) | scpds_lift scpds_aaa scpds_scpds |
|
|
|
context-sensitive extended computation | lpxs ( ⦃?,?⦄ ⊢ ➡*[?,?] ? ) | lpxs_drop lpxs_lleq lpxs_aaa lpxs_cpxs lpxs_lpxs |
|
|
|
|
cpxs ( ⦃?,?⦄ ⊢ ? ➡*[?,?] ? ) | cpxs_tsts cpxs_tsts_vector cpxs_leq cpxs_lift cpxs_lleq cpxs_aaa cpxs_cpxs |
|
|
|
context-sensitive computation | lprs ( ⦃?,?⦄ ⊢ ➡* ? ) | lprs_drop lprs_cprs lprs_lprs |
|
|
|
|
cprs ( ⦃?,?⦄ ⊢ ? ➡* ?) | cprs_lift cprs_cprs |
|
|
|
local env. ref. for generic reducibility | lsubc ( ? ⊢ ? ⫃[?] ? ) | lsubc_drop lsubc_drops lsubc_lsuba |
|
|
|
support for generic computation properties | gcp | gcp_cr ( ⦃?,?,?⦄ ϵ[?] 〚?〛 ) | gcp_aaa |
|
reduction | "big tree" parallel reduction | fpb ( ⦃?,?,?⦄ ≽[?,?] ⦃?,?,?⦄ ) | fpb_lift fpb_aaa |
|
|
|
normal forms for context-sensitive extended reduction | cnx ( ⦃?,?⦄ ⊢ ➡[?,?] 𝐍⦃?⦄ ) | cnx_lift cnx_crx cnx_cix |
|
|
|
context-sensitive extended reduction | lpx ( ⦃?,?⦄ ⊢ ➡[?,?] ? ) | lpx_drop lpx_frees lpx_lleq lpx_aaa |
|
|
|
|
cpx ( ⦃?,?⦄ ⊢ ? ➡[?,?] ? ) | cpx_leq cpx_lift cpx_llpx_sn cpx_lleq cpx_cix |
|
|
|
irreducible forms for context-sensitive extended reduction | cix ( ⦃?,?⦄ ⊢ ➡[?,?] 𝐈⦃?⦄ ) | cix_lift |
|
|
|
reducible forms for context-sensitive extended reduction | crx ( ⦃?,?⦄ ⊢ ➡[?,?] 𝐑⦃?⦄ ) | crx_lift |
|
|
|
normal forms for context-sensitive reduction | cnr ( ⦃?,?⦄ ⊢ ➡ 𝐍⦃?⦄ ) | cnr_lift cnr_crr cnr_cir |
|
|
|
context-sensitive reduction | lpr ( ⦃?,?⦄ ⊢ ➡ ? ) | lpr_drop lpr_lpr |
|
|
|
|
cpr ( ⦃?,?⦄ ⊢ ? ➡ ? ) | cpr_lift cpr_llpx_sn cpr_cir |
|
|
|
irreducible forms for context-sensitive reduction | cir ( ⦃?,?⦄ ⊢ ➡ 𝐈⦃?⦄ ) | cir_lift |
|
|
|
reducible forms for context-sensitive reduction | crr ( ⦃?,?⦄ ⊢ ➡ 𝐑⦃?⦄ ) | crr_lift |
|
|
unfold | unfold | unfold ( ⦃?,?⦄ ⊢ ? ⧫* ? ) |
|
|
|
|
iterated static type assignment | lstas ( ⦃?,?⦄ ⊢ ? •*[?,?] ? ) | lstas_alt ( ⦃?,?⦄ ⊢ ? ••*[?,?] ? ) | lstas_lift lstas_aaa lstas_da lstas_lstas |
|
static typing | local env. ref. for degree assignment | lsubd ( ? ⊢ ? ⫃▪[?,?] ? ) | lsubd_da lsubd_lsubd |
|
|
|
degree assignment | da ( ⦃?,?⦄ ⊢ ? ▪[?,?] ? ) | da_lift da_aaa da_sta da_da |
|
|
|
static type assignment | sta ( ⦃?,?⦄ ⊢ ? •[?] ? ) | sta_lift sta_lpx_sn sta_aaa sta_sta |
|
|
|
parameters | sh | sd |
|
|
|
local env. ref. for atomic arity assignment | lsuba ( ? ⊢ ? ⫃⁝ ? ) | lsuba_aaa lsuba_lsuba |
|
|
|
atomic arity assignment | aaa ( ⦃?,?⦄ ⊢ ? ⁝ ? ) | aaa_lift aaa_lifts aaa_fqus aaa_lleq aaa_aaa |
|
|
|
restricted local env. ref. | lsubr ( ? ⫃ ? ) | lsubr_lsubr |
|
|
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 extended multiple 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 |
substitution | structural successor for closures | fquq ( ⦃?,?,?⦄ ⊐⸮ ⦃?,?,?⦄ ) | fquq_alt ( ⦃?,?,?⦄ ⊐⊐⸮ ⦃?,?,?⦄ ) |
|
|
|
|
fqu ( ⦃?,?,?⦄ ⊐ ⦃?,?,?⦄ ) |
|
|
|
|
global env. slicing | gget ( ⇩[?] ? ≡ ? ) | gget_gget |
|
|
|
contxt-sensitive extended ordinary substitution | cpy ( ⦃?,?⦄ ⊢ ? ▶[?,?] ? ) | cpy_lift cpy_nlift cpy_cpy |
|
|
|
local env. ref. for extended substitution | lsuby ( ? ⊆[?,?] ? ) | lsuby_lsuby |
|
|
|
pointwise extension of a relation | lpx_sn | lpx_sn_alt lpx_sn_tc lpx_sn_drop lpx_sn_lpx_sn |
|
|
|
basic local env. slicing | drop ( ⇩[?,?,?] ? ≡ ? ) | drop_append drop_leq drop_drop |
|
|
|
basic term relocation | lift_vector ( ⇧[?,?] ? ≡ ? ) | lift_lift_vector |
|
|
|
|
lift ( ⇧[?,?] ? ≡ ? ) | lift_neq lift_lift |
|
|
grammar | equivalence for local environments | leq ( ? ⩬[?,?] ? ) | leq_leq |
|
|
|
same top term structure | tsts ( ? ≂ ? ) | tsts_tsts tsts_vector |
|
|
|
closures | cl_weight ( ♯{?,?,?} ) | cl_restricted_weight ( ♯{?,?} ) |
|
|
|
internal syntax | genv |
|
|
|
|
|
lenv | lenv_weight ( ♯{?} ) | lenv_length ( |?| ) | lenv_append ( ? @@ ? ) |
|
|
term | term_weight ( ♯{?} ) | term_simple ( 𝐒⦃?⦄ ) | term_vector ( Ⓐ?.? ) |
|
|
item |
|
|
|
|
external syntax | aarity |
|
|
|