category | objects |
|
|
|
|
|
sizes | files | 360 | characters | 437272 | nodes | 1935835 |
propositions | theorems | 130 | lemmas | 1303 | total | 1433 |
concepts | declared | 54 | defined | 89 | total | 143 |
component | plane | files |
|
|
|
examples | terms with special features | ex_sta_ldec ex_cpr_omega ex_fpbg_refl ex_snv_eta |
|
|
|
|
|
|
|||
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 ( ⦃?,?⦄ ⊢ ? ¡[?,?,?] ) |
|
|
|
|
|
snv ( ⦃?,?⦄ ⊢ ? ¡[?,?] ) | snv_lift snv_aaa snv_da_lpr snv_lstas snv_lstas_lpr snv_lpr snv_fsb snv_scpes snv_preserve |
|
|
equivalence | decomposed rt-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 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 | 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 |
|
|
parallel qrst-computation | fpbg ( ⦃?,?,?⦄ >≡[?,?] ⦃?,?,?⦄ ) | fpbg_lift fpbg_fleq fpbg_fpbs fpbg_fpbg |
|
|
|
|
fpbs ( ⦃?,?,?⦄ ≥[?,?] ⦃?,?,?⦄ ) | fpbs_alt ( ⦃?,?,?⦄ ≥≥[?,?] ⦃?,?,?⦄ ) | fpbs_lift fpbs_aaa fpbs_fpb fpbs_fpbs |
|
|
decomposed rt-computation | scpds ( ⦃?,?⦄ ⊢ ? •*➡*[?,?,?] ? ) | scpds_lift scpds_aaa scpds_scpds |
|
|
|
context-sensitive rt-computation | lpxs ( ⦃?,?⦄ ⊢ ➡*[?,?] ? ) | lpxs_drop lpxs_lleq lpxs_aaa lpxs_cpxs lpxs_lpxs |
|
|
|
|
cpxs ( ⦃?,?⦄ ⊢ ? ➡*[?,?] ? ) | cpxs_tsts cpxs_tsts_vector cpxs_lreq 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 | parallel qrst-reduction | fpbq ( ⦃?,?,?⦄ ≽[?,?] ⦃?,?,?⦄ ) | fpbq_alt ( ⦃?,?,?⦄ ≽≽[?,?] ⦃?,?,?⦄ ) | fpbq_lift fpbq_aaa |
|
|
|
fpb ( ⦃?,?,?⦄ ≻[?,?] ⦃?,?,?⦄ ) | fpb_lift fpb_lleq fpb_fleq |
|
|
|
normal forms for context-sensitive rt-reduction | cnx ( ⦃?,?⦄ ⊢ ➡[?,?] 𝐍⦃?⦄ ) | cnx_lift cnx_crx cnx_cix |
|
|
|
context-sensitive rt-reduction | lpx ( ⦃?,?⦄ ⊢ ➡[?,?] ? ) | lpx_drop lpx_frees lpx_lleq lpx_aaa |
|
|
|
|
cpx ( ⦃?,?⦄ ⊢ ? ➡[?,?] ? ) | cpx_lreq cpx_lift cpx_llpx_sn cpx_lleq cpx_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 |
|
|
|
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_lift lstas_llpx_sn.ma 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_da |
|
|
|
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_lreq 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_lreq 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_lreq frees_lift |
|
|
|
context-sensitive multiple rt-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 |
|
|
|
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_tc lpx_sn_drop lpx_sn_lpx_sn |
|
|
|
basic local env. slicing | drop ( ⬇[?,?,?] ? ≡ ? ) | drop_append drop_lreq drop_drop |
|
|
|
basic term relocation | lift_vector ( ⬆[?,?] ? ≡ ? ) | lift_lift_vector |
|
|
|
|
lift ( ⬆[?,?] ? ≡ ? ) | lift_neq lift_lift |
|
|
grammar | equivalence for local environments | lreq ( ? ⩬[?,?] ? ) | lreq_lreq |
|
|
|
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 |
|
|
|