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	221	characters	212361	nodes	1046022
propositions	theorems	49	lemmas	691	total	740
concepts	declared	29	defined	61	total	90

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

component	plane	files
rt-computation	uncounted context-sensitive rt-transition	cpxs ( ⦃?,?⦄ ⊢ ? ⬈*[?] ? )
	generic reducibility	lsubc ( ? ⊢ ? ⫃[?] ? )	lsubc_drop lsubc_drops lsubc_lsubr lsubc_lsuba
		gcp	gcp_cr ( ⦃?,?,?⦄ ϵ[?] 〚?〛 )	gcp_aaa
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	cnx ( ⦃?,?⦄ ⊢ ⬈[?,?] 𝐍⦃?⦄ )	cnx_simple cnx_drops
		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	atomic arity assignment	lsuba ( ? ⊢ ? ⫃⁝ ? )	lsuba_drops lsuba_lsubr lsuba_aaa lsuba_lsuba
		aaa ( ⦃?,?⦄ ⊢ ? ⁝ ? )	aaa_drops aaa_fqus aaa_lfdeq aaa_aaa
	degree-based equivalence on referred entries	ffdeq ( ⦃?,?,?⦄ ≡[?,?] ⦃?,?,?⦄ )	ffdeq_fqup ffdeq_ffdeq
		lfdeq ( ? ≡[?,?,?] ? )	lfdeq_length lfdeq_fqup lfdeq_lfdeq
	generic extension on referred entries	lfxs ( ? ⦻*[?,?] ? )	lfxs_length lfxs_drops lfxs_fqup lfxs_lfxs
	context-sensitive free variables	lsubf ( ⦃?,?⦄ ⫃𝐅* ⦃?,?⦄ )	lsubf_frees
		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