category | objects |
|
|
|
|
|
sizes | files | 167 | characters | 167321 | nodes | 875248 |
propositions | theorems | 47 | lemmas | 590 | total | 637 |
concepts | declared | 23 | defined | 40 | total | 63 |
component | plane | files |
|
|
|
rt-transition | t-bound context-sensitive rt-transition | lfpr ( ⦃?,?⦄ ⊢ ➡[?,?] ? ) | lfpr_length lfpr_drops lfpr_fqup lfpr_lfpx lfpr_lfpr |
|
|
|
|
cpr ( ⦃?,?⦄ ⊢ ? ➡[?] ? ) | cpr_drops |
|
|
|
|
cpm ( ⦃?,?⦄ ⊢ ? ➡[?,?] ? ) | cpm_simple cpm_drops cpm_lsubr cpm_cpx |
|
|
|
uncounted context-sensitive rt-transition | lfpx ( ⦃?,?⦄ ⊢ ⬈[?,?] ? ) | lfpx_length lfpx_drops lfpx_fqup |
|
|
|
|
cpx ( ⦃?,?⦄ ⊢ ? ⬈[?] ? ) | cpx_simple cpx_drops cpx_lsubr |
|
|
|
counted context-sensitive rt-transition | cpg ( ⦃?,?⦄ ⊢ ? ⬈[?,?] ? ) | cpg_simple cpg_drops cpg_lsubr |
|
|
static typing | parameters | sh | sd |
|
|
|
restricted ref. for atomic arity assignment | lsuba ( ? ⊢ ? ⫃⁝ ? ) | lsuba_drops lsuba_lsubr lsuba_aaa lsuba_lsuba |
|
|
|
atomic arity assignment | aaa ( ⦃?,?⦄ ⊢ ? ⁝ ? ) | aaa_drops aaa_fqus aaa_lfeq aaa_aaa |
|
|
|
restricted ref. for local env. | lsubr ( ? ⫃ ? ) | lsubr_length lsubr_drops lsubr_lsubr |
|
|
|
equivalence for closures on referred entries | ffeq ( ⦃?,?,?⦄ ≡ ⦃?,?,?⦄ ) | ffeq_freq |
|
|
|
equivalence for local environments on referred entries | lfeq ( ? ≡[?] ? ) | lfeq_length lfeq_lreq lfeq_fqup lfeq_lfeq |
|
|
|
generic extension on referred entries | lfxs ( ? ⦻*[?,?] ? ) | lfxs_length lfxs_drops lfxs_fqup lfxs_lfxs |
|
|
|
context-sensitive free variables | frees ( ? ⊢ 𝐅*⦃?⦄ ≡ ? ) | frees_weight frees_lreq frees_drops frees_fqup frees_fqus frees_frees |
|
|
s-computation | iterated structural successor for closures | fqus ( ⦃?,?,?⦄ ⊐* ⦃?,?,?⦄ ) | fqus_weight fqus_drops fqus_fqup fqus_fqus |
|
|
|
|
fqup ( ⦃?,?,?⦄ ⊐+ ⦃?,?,?⦄ ) | fqup_weight fqup_drops fqup_fqup |
|
|
s-transition | structural successor for closures | fquq ( ⦃?,?,?⦄ ⊐⸮ ⦃?,?,?⦄ ) | fquq_length fquq_weight |
|
|
|
|
fqu ( ⦃?,?,?⦄ ⊐ ⦃?,?,?⦄ ) | fqu_length fqu_weight |
|
|
relocation | generic slicing for local environments | drops_vector ( ⬇*[?,?] ? ≡ ? ) ( ⬇*[?] ? ≡ ? ) |
|
|
|
|
|
drops ( ⬇*[?,?] ? ≡ ? ) ( ⬇*[?] ? ≡ ? ) | drops_lstar drops_weight drops_length drops_ceq drops_lexs drops_lreq drops_drops |
|
|
|
generic relocation for terms | lifts_vector ( ⬆*[?] ? ≡ ? ) | lifts_lifts_vector |
|
|
|
|
lifts ( ⬆*[?] ? ≡ ? ) | lifts_simple lifts_weight lifts_lifts |
|
|
|
ranged equivalence for local environments | lreq ( ? ≡[?] ? ) | lreq_length lreq_lreq |
|
|
|
generic entrywise extension | lexs ( ? ⦻*[?,?,?] ? ) | lexs_length lexs_lexs |
|
|
grammar | append for local environments | append ( ? @@ ? ) | append_length |
|
|
|
context-sensitive equivalences for terms | ceq | ceq_ceq |
|
|
|
same top term structure | tsts ( ? ≂ ? ) | tsts_tsts tsts_vector |
|
|
|
closures | cl_weight ( ♯{?,?,?} ) | cl_restricted_weight ( ♯{?,?} ) |
|
|
|
internal syntax | genv |
|
|
|
|
|
lenv | lenv_weight ( ♯{?} ) | lenv_length ( |?| ) |
|
|
|
term | term_weight ( ♯{?} ) | term_simple ( 𝐒⦃?⦄ ) | term_vector ( Ⓐ?.? ) |
|
|
item |
|
|
|
|
external syntax | aarity |
|
|
|