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	units
sizes	characters (files)	315581 (309)	nodes (objects)	1458870 (1431)	intrinsic loss factor	4.6
propositions	theorems	92	lemmas	1085	total	1177
concepts	declared	34	defined	93	total	127

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

component	section	plane	files
rt-conversion	context-sensitive parallel r-conversion	for terms	cpc ( ⦃?,?⦄ ⊢ ? ⬌[?] ? )	cpc_cpc
rt-computation	uncounted context-sensitive parallel rt-computation	refinement for lenvs	lsubsx ( ? ⊢ ? ⊆ⓧ[?,?,?] ? )	lsubsx_lfsx lsubsx_lsubsx
		strongly normalizing for lenvs on referred entries	lfsx ( ? ⊢ ⬈*[?,?,?] 𝐒⦃?⦄ )	lfsx_drops lfsx_fqup lfsx_lfpxs lfsx_lfsx
		strongly normalizing for term vectors	csx_vector ( ⦃?,?⦄ ⊢ ⬈*[?,?] 𝐒⦃?⦄ )	csx_cnx_vector csx_csx_vector
		strongly normalizing for terms	csx ( ⦃?,?⦄ ⊢ ⬈*[?,?] 𝐒⦃?⦄ )	csx_simple csx_simple_theq csx_drops csx_lsubr csx_lfdeq csx_aaa csx_gcp csx_gcr csx_lfpx csx_cnx csx_cpxs csx_lfpxs csx_csx
		for lenvs on referred entries	lfpxs ( ⦃?,?⦄ ⊢ ⬈*[?,?] ? )	lfpxs_length lfpxs_drops lfpxs_fqup lfpxs_lfdeq lfpxs_aaa lfpxs_cpxs lfpxs_lpxs lfpxs_lfpxs
		for lenvs on all entries	lpxs ( ⦃?,?⦄ ⊢ ⬈*[?] ? )
		for terms	cpxs ( ⦃?,?⦄ ⊢ ? ⬈*[?] ? )	cpxs_tdeq cpxs_theq cpxs_theq_vector cpxs_drops cpxs_fqus cpxs_lsubr cpxs_lfdeq cpxs_aaa cpxs_lpx cpxs_lfpx cpxs_cnx cpxs_cpxs
rt-transition	uncounted parallel rst-transition	for closures	fpbq ( ⦃?,?,?⦄ ≽[?] ⦃?,?,?⦄ )	fpbq_aaa
		proper for closures	fpb ( ⦃?,?,?⦄ ≻[?] ⦃?,?,?⦄ )	fpb_lfdeq
	context-sensitive parallel r-transition	for lenvs on referred entries	lfpr ( ⦃?,?⦄ ⊢ ➡[?,?] ? )	lfpr_length lfpr_drops lfpr_fquq lfpr_fqup lfpr_frees lfpr_aaa lfpr_lfpx lfpr_lfpr
		for binders	cpr_ext ( ⦃?,?⦄ ⊢ ? ➡[?] ? )
		for terms	cpr ( ⦃?,?⦄ ⊢ ? ➡[?] ? )	cpr_drops
	t-bound context-sensitive parallel rt-transition	for terms	cpm ( ⦃?,?⦄ ⊢ ? ➡[?,?] ? )	cpm_simple cpm_drops cpm_lsubr cpm_lfxs cpm_cpx
	uncounted context-sensitive parallel rt-transition	normal form for terms	cnx ( ⦃?,?⦄ ⊢ ⬈[?,?] 𝐍⦃?⦄ )	cnx_simple cnx_drops cnx_cnx
		for lenvs on referred entries	lfpx ( ⦃?,?⦄ ⊢ ⬈[?,?] ? )	lfpx_length lfpx_drops lfpx_fqup lfpx_frees lfpx_lfdeq lfpx_aaa lfpx_cpx lfpx_lfpx
		for lenvs on all entries	lpx ( ⦃?,?⦄ ⊢ ⬈[?] ? )
		for binders	cpx_ext ( ⦃?,?⦄ ⊢ ? ⬈[?] ? )
		for terms	cpx ( ⦃?,?⦄ ⊢ ? ⬈[?] ? )	cpx_simple cpx_drops cpx_fqus cpx_lsubr cpx_lfxs cpx_lfeq
	counted context-sensitive parallel rt-transition	for terms	cpg ( ⦃?,?⦄ ⊢ ? ⬈[?,?] ? )	cpg_simple cpg_drops cpg_lsubr
iterated static typing	iterated generic extension of a context-sensitive relation	for lenvs on referred entries	tc_lfxs ( ? ⦻**[?,?] ? )	tc_lfxs_length tc_lfxs_lex tc_lfxs_drops tc_lfxs_fqup tc_lfxs_tc_lfxs
static typing	generic reducibility	restricted refinement for lenvs	lsubc ( ? ⊢ ? ⫃[?] ? )	lsubc_drops lsubc_lsubr lsubc_lsuba
		candidates	gcp_cr ( ⦃?,?,?⦄ ϵ[?] 〚?〛 )	gcp_aaa
		computation properties	gcp
	atomic arity assignment	restricted refinement for lenvs	lsuba ( ? ⊢ ? ⫃⁝ ? )	lsuba_drops lsuba_lsubr lsuba_aaa lsuba_lsuba
		for terms	aaa ( ⦃?,?⦄ ⊢ ? ⁝ ? )	aaa_drops aaa_fqus aaa_lfdeq aaa_aaa
	degree-based equivalence	for closures on referred entries	ffdeq ( ⦃?,?,?⦄ ≛[?,?] ⦃?,?,?⦄ )	ffdeq_fqup ffdeq_ffdeq
		for lenvs on referred entries	lfdeq ( ? ≛[?,?,?] ? )	lfdeq_length lfdeq_drops lfdeq_fqup lfdeq_fqus lfdeq_lfdeq
	syntactic equivalence	for lenvs on referred entries	lfeq ( ? ≡[?] ? )	lfeq_fqup lfeq_lfeq
	generic extension of a context-sensitive relation	for lenvs on referred entries	lfxs ( ? ⦻*[?,?] ? )	lfxs_length lfxs_drops lfxs_fqup lfxs_lfxs
	context-sensitive free variables	restricted refinement for lenvs	lsubf ( ⦃?,?⦄ ⫃𝐅* ⦃?,?⦄ )	lsubf_lsubr lsubf_frees lsubf_lsubf
		for terms	frees ( ? ⊢ 𝐅*⦃?⦄ ≡ ? )	frees_drops frees_fqup frees_frees
	local environments	restricted refinement	lsubr ( ? ⫃ ? )	lsubr_length lsubr_drops lsubr_lsubr
s-computation	iterated structural successor	for closures	fqus ( ⦃?,?,?⦄ ⊐*[?] ⦃?,?,?⦄ ) ( ⦃?,?,?⦄ ⊐* ⦃?,?,?⦄ )	fqus_weight fqus_drops fqus_fqup fqus_fqus
		proper for closures	fqup ( ⦃?,?,?⦄ ⊐+[?] ⦃?,?,?⦄ ) ( ⦃?,?,?⦄ ⊐+ ⦃?,?,?⦄ )	fqup_weight fqup_drops fqup_fqup
s-transition	structural successor	for closures	fquq ( ⦃?,?,?⦄ ⊐⸮[?] ⦃?,?,?⦄ ) ( ⦃?,?,?⦄ ⊐⸮ ⦃?,?,?⦄ )	fquq_length fquq_weight
		proper for closures	fqu ( ⦃?,?,?⦄ ⊐[?] ⦃?,?,?⦄ ) ( ⦃?,?,?⦄ ⊐ ⦃?,?,?⦄ )	fqu_length fqu_weight
relocation	generic slicing	for lenvs	drops ( ⬇*[?,?] ? ≡ ? ) ( ⬇*[?] ? ≡ ? )	drops_lstar drops_weight drops_length drops_cext2 drops_lexs drops_lreq drops_drops drops_vector
	generic relocation	for binders	lifts_bind ( ⬆*[?] ? ≡ ? )	lifts_weight_bind lifts_lifts_bind
		for term vectors	lifts_vector ( ⬆*[?] ? ≡ ? )	lifts_lifts_vector
		for terms	lifts ( ⬆*[?] ? ≡ ? )	lifts_simple lifts_weight lifts_tdeq lifts_lifts
	syntactic equivalence	for lenvs on selected entries	lreq ( ? ≡[?] ? )	lreq_length lreq_lreq
	generic entrywise extension	for lenvs of one contex-sensitive relation	lex ( ? ⦻[?] ? )	lex_tc
		for lenvs of two contex-sensitive relations	lexs ( ? ⦻*[?,?,?] ? )	lexs_tc 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		tdeq_ext ( ? ≛[?,?] ? ) ( ? ⊢ ? ≛[?,?] ? )
			tdeq ( ? ≛[?,?] ? )	tdeq_tdeq
	closures		cl_weight ( ♯{?,?,?} )
			cl_restricted_weight ( ♯{?,?} )
	global environments		genv
	local environments		ceq_ext	ceq_ext_ceq_ext
			cext2
			lenv_length ( |?| )
			lenv_weight ( ♯{?} )
			lenv
	binders for local environments		ext2	ext2_tc ext2_ext2
			bind	bind_weight
	terms		term_vector ( Ⓐ?.? )
			term_simple ( 𝐒⦃?⦄ )
			term_weight ( ♯{?} )
			term
	items		item_sd
			item_sh
			item
	atomic arities		aarity