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	268	characters	269075	nodes	1271298
propositions	theorems	71	lemmas	928	total	999
concepts	declared	33	defined	78	total	111

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

component	plane	files
conversion	context-sensitive r-conversion	cpc ( ⦃?,?⦄ ⊢ ? ⬌[?] ? )	cpc_cpc
rt-computation	uncounted context-sensitive rt-computation	lfsx ( ? ⊢ ⬈*[?,?,?] 𝐒⦃?⦄ )	lfsx_fqup lfsx_lfpxs lfsx_lfsx
		csx_vector ( ⦃?,?⦄ ⊢ ⬈*[?,?] 𝐒⦃?⦄ )	csx_cnx_vector csx_csx_vector
		csx ( ⦃?,?⦄ ⊢ ⬈*[?,?] 𝐒⦃?⦄ )	csx_simple csx_simple_theq csx_drops csx_lsubr csx_aaa csx_gcp csx_gcr csx_lfpx csx_cnx csx_cpxs csx_csx
		lfpxs ( ⦃?,?⦄ ⊢ ⬈*[?,?] ? )	lfpxs_length lfpxs_drops lfpxs_fqup lfpxs_lfdeq lfpxs_aaa lfpxs_cpxs lfpxs_lfpxs
		cpxs ( ⦃?,?⦄ ⊢ ? ⬈*[?] ? )	cpxs_tdeq cpxs_theq cpxs_theq_vector cpxs_drops cpxs_lsubr cpxs_aaa cpxs_lfpx cpxs_cnx cpxs_cpxs
rt-transition	uncounted 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 ( ? ⦻**[?,?] ? )	tc_lfxs_length tc_lfxs_drops tc_lfxs_fqup tc_lfxs_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	lifts_bind ( ⬆*[?] ? ≡ ? )	lifts_weight_bind lifts_lifts_bind
		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
	head equivalence for terms	theq ( ? ⩳[?,?] ? )	theq_simple theq_tdeq theq_theq theq_simple_vector
	degree-based equivalence for terms	deq ( ? ≡[?,?] ? )	deq_deq
	closures	cl_weight ( ♯{?,?,?} )
		cl_restricted_weight ( ♯{?,?} )
	global environments	genv
	local environments	lenv_ext2
		lenv_length ( |?| )
		lenv_weight ( ♯{?} )
		lenv
	binders for local environments	bind_ext2
		bind	bind_weight
	terms	term_vector ( Ⓐ?.? )
		term_simple ( 𝐒⦃?⦄ )
		term_weight ( ♯{?} )
		term
	items	item_sd
		item_sh
		item
	atomic arities	aarity