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	181	characters	192119	nodes	993162
propositions	theorems	48	lemmas	642	total	690
concepts	declared	26	defined	44	total	70

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

component	plane	files
rt-transition	parallel qrst-rtransition	fpb ( ⦃?,?,?⦄ ≻[?,?] ⦃?,?,?⦄ )
	t-bound context-sensitive rt-transition	lfpr ( ⦃?,?⦄ ⊢ ➡[?,?] ? )	lfpr_length lfpr_drops lfpr_fqup lfpr_frees lfpr_aaa lfpr_lfpx lfpr_lfpr
		cpr ( ⦃?,?⦄ ⊢ ? ➡[?] ? )	cpr_drops
		cpm ( ⦃?,?⦄ ⊢ ? ➡[?,?] ? )	cpm_simple cpm_drops cpm_lsubr cpm_lfxs cpm_cpx
	uncounted context-sensitive rt-transition	lfpx ( ⦃?,?⦄ ⊢ ⬈[?,?] ? )	lfpx_length lfpx_drops lfpx_fqup lfpx_frees lfpx_aaa
		cpx ( ⦃?,?⦄ ⊢ ? ⬈[?] ? )	cpx_simple cpx_drops cpx_fqus cpx_lsubr cpx_lfxs cpx_lfdeq
	counted context-sensitive rt-transition	cpg ( ⦃?,?⦄ ⊢ ? ⬈[?,?] ? )	cpg_simple cpg_drops cpg_lsubr
static typing	restricted ref. for atomic arity assignment	lsuba ( ? ⊢ ? ⫃⁝ ? )	lsuba_drops lsuba_lsubr lsuba_aaa lsuba_lsuba
	atomic arity assignment	aaa ( ⦃?,?⦄ ⊢ ? ⁝ ? )	aaa_drops aaa_fqus aaa_lfdeq aaa_aaa
	degree-based equivalence for closures on referred entries	ffdeq ( ⦃?,?,?⦄ ≡[?,?] ⦃?,?,?⦄ )	ffdeq_fqup ffdeq_ffdeq
	degree-based equivalence for local environments on referred entries	lfdeq ( ? ≡[?,?,?] ? )	lfdeq_length lfdeq_fqup lfdeq_lfdeq
	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_drops frees_fqup 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_tdeq lifts_lifts
	ranged equivalence for local environments	lreq ( ? ≡[?] ? )	lreq_length lreq_lreq
	generic entrywise extension	lexs ( ? ⦻*[?,?,?] ? )	lexs_length lexs_lexs
syntax	append for local environments	append ( ? @@ ? )	append_length
	degree-based equivalence for terms	deq ( ? ≡[?,?] ? )	deq_deq
	same top term structure	tsts ( ? ≂ ? )	tsts_tsts tsts_vector
	closures	cl_weight ( ♯{?,?,?} )
		cl_restricted_weight ( ♯{?,?} )
	global environments	genv
	local environments	lenv_length ( |?| )
		lenv_weight ( ♯{?} )
		lenv
	terms	term_vector ( Ⓐ?.? )
		term_simple ( 𝐒⦃?⦄ )
		term_weight ( ♯{?} )
		term
	items	item_sd
		item_sh
		item
	atomic arities	aarity