home	news	specification			documentation	implementation
foreword	milestones	version 2	(background - core - applications)		version 2	helena
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	150	characters	121855	nodes	618445
propositions	theorems	45	lemmas	458	total	503
concepts	declared	23	defined	34	total	57

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

component	plane	files
rt-transition	uncounted context-sensitive rt-transition	lfpx ( ⦃?,?⦄ ⊢ ⬈[?,?] ? )	lfpx_length 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_fqup lfxs_lfxs
	context-sensitive free variables	frees ( ? ⊢ 𝐅*⦃?⦄ ≡ ? )	frees_weight frees_lreq frees_drops 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