home	news	specification			documentation	implementation
foreword	milestones	version 2	(background - core - applications)		version 2	helena	Open Symbolic Notation (OSN)
citations	visibility	version 1	(background - core)	(static HELM directory)	version 1	library	(static LDDL directory)

Here is a numerical account of the specification's contents and its timeline.

category	objects
sizes	files	157	characters	138411	nodes	711276
propositions	theorems	45	lemmas	506	total	551
concepts	declared	23	defined	38	total	61

This table reports the specification's components and their planes.

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
	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
	restricted ref. for context-sensitive free variables	lsubf ( ⦃?,?⦄ ⫃𝐅* ⦃?,?⦄ )	lsubf_frees
	context-sensitive free variables	frees ( ? ⊢ 𝐅*⦃?⦄ ≡ ? )	frees_weight frees_lreq frees_drops frees_fqup frees_fqus frees_frees
	restricted ref. for local env.	lsubr ( ? ⫃ ? )	lsubr_length lsubr_drops lsubr_lsubr
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