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	301	characters	311322	nodes	1450558
propositions	theorems	93	lemmas	1054	total	1147
concepts	declared	34	defined	91	total	125

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 on referred entries for lenvs	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
		on referred entries for lenvs	lfpxs ( ⦃?,?⦄ ⊢ ⬈*[?,?] ? )	lfpxs_length lfpxs_drops lfpxs_fqup lfpxs_lfdeq lfpxs_aaa lfpxs_cpxs lfpxs_lfpxs
		for terms	cpxs ( ⦃?,?⦄ ⊢ ? ⬈*[?] ? )	cpxs_tdeq cpxs_theq cpxs_theq_vector cpxs_drops cpxs_fqus cpxs_lsubr cpxs_lfdeq cpxs_aaa 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 binders	cpx_ext ( ⦃?,?⦄ ⊢ ? ⬈[?] ? )
		for terms	cpx ( ⦃?,?⦄ ⊢ ? ⬈[?] ? )	cpx_simple cpx_drops cpx_fqus cpx_lsubr cpx_lfxs
	counted context-sensitive parallel rt-transition	for terms	cpg ( ⦃?,?⦄ ⊢ ? ⬈[?,?] ? )	cpg_simple cpg_drops cpg_lsubr
iterated static typing	iterated extension 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		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
	syntactic equivalence on referred entries		lfeq ( ? ≡[?] ? )	lfeq_fqup lfeq_lfeq
	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_cext2 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		lex ( ? ⦻[?] ? )
			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