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	210	characters	207234	nodes	980390
propositions	theorems	62	lemmas	732	total	794
concepts	declared	31	defined	77	total	108

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

component	plane	files
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_lsubr lsubf_frees lsubf_lsubf
		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_ext2 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	tdeq ( ? ≡[?,?] ? )	tdeq_ext tdeq_tdeq
	closures	cl_weight ( ♯{?,?,?} )
		cl_restricted_weight ( ♯{?,?} )
	global environments	genv
	local environments	lenv_ext2
		lenv_length ( |?| )
		lenv_weight ( ♯{?} )
		lenv
	binders for local environments	ext2	ext2_ext2
		bind	bind_weight
	terms	term_vector ( Ⓐ?.? )
		term_simple ( 𝐒⦃?⦄ )
		term_weight ( ♯{?} )
		term
	items	item_sd
		item_sh
		item
	atomic arities	aarity