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	229	characters	240969	nodes	1182308
propositions	theorems	61	lemmas	805	total	866
concepts	declared	30	defined	66	total	96

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

component	plane	files
rt-computation	uncounted context-sensitive rt-computation	csx_vector ( ⦃?,?⦄ ⊢ ⬈*[?,?] 𝐒⦃?⦄ )
		csx ( ⦃?,?⦄ ⊢ ⬈*[?,?] 𝐒⦃?⦄ )	csx_cnx csx_cpxs csx_csx
		lfpxs ( ⦃?,?⦄ ⊢ ⬈*[?,?] ? )	lfpxs_length lfpxs_fqup lfpxs_cpxs
		cpxs ( ⦃?,?⦄ ⊢ ? ⬈*[?] ? )	cpxs_tdeq cpxs_tsts cpxs_tsts_vector cpxs_drops cpxs_lsubr cpxs_lfpx cpxs_cnx cpxs_cpxs
rt-transition	parallel rst-transition	fpbq ( ⦃?,?,?⦄ ≽[?] ⦃?,?,?⦄ )	fpbq_aaa
		fpb ( ⦃?,?,?⦄ ≻[?,?] ⦃?,?,?⦄ )	fpb_lfdeq
	t-bound context-sensitive rt-transition	lfpr ( ⦃?,?⦄ ⊢ ➡[?,?] ? )	lfpr_length lfpr_drops lfpr_fquq 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 cnx_cnx
		lfpx ( ⦃?,?⦄ ⊢ ⬈[?,?] ? )	lfpx_length lfpx_drops lfpx_fqup lfpx_frees lfpx_lfdeq lfpx_aaa lfpx_lfpx
		cpx ( ⦃?,?⦄ ⊢ ? ⬈[?] ? )	cpx_simple cpx_drops cpx_fqus cpx_lsubr cpx_lfxs
	counted context-sensitive rt-transition	cpg ( ⦃?,?⦄ ⊢ ? ⬈[?,?] ? )	cpg_simple cpg_drops cpg_lsubr
iterated static typing	iterated extension on referred entries	tc_lfxs ( ? ⦻**[?,?] ? )
static typing	generic reducibility	lsubc ( ? ⊢ ? ⫃[?] ? )	lsubc_drops lsubc_lsubr lsubc_lsuba
		gcp_cr ( ⦃?,?,?⦄ ϵ[?] 〚?〛 )	gcp_aaa
		gcp
	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_drops lfdeq_fqup lfdeq_fqus 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_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
	same top term structure	tsts ( ? ⩳[?,?] ? )	tsts_simple tsts_tdeq tsts_tsts tsts_simple_vector
	degree-based equivalence for terms	deq ( ? ≡[?,?] ? )	deq_deq
	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