home	news	documentation	specification			implementation
foreword	milestones	version 2	version 2	(background - core - applications)		library	(static LDDL directory)
citations	visibility	version 1	version 1	(background - core)	(static HELM directory)	helena

Here is a numerical account of the specification's contents and its timeline.

category	objects
sizes	files	360	characters	433402	nodes	1874774
propositions	theorems	130	lemmas	1286	total	1416
concepts	declared	54	defined	89	total	143

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

component	plane	files
examples	terms with special features	ex_sta_ldec ex_cpr_omega ex_fpbg_refl ex_snv_eta
dynamic typing	local env. ref. for stratified native validity	lsubsv ( ? ⊢ ? ⫃¡[?,?] ? )	lsubsv_lsuba lsubsv_lsubd lsubsv_lstas lsubsv_scpds lsubsv_cpcs lsubsv_snv
	stratified native validity	shnv ( ⦃?,?⦄ ⊢ ? ¡[?,?,?] )
		snv ( ⦃?,?⦄ ⊢ ? ¡[?,?] )	snv_lift snv_aaa snv_da_lpr snv_lstas snv_lstas_lpr snv_lpr snv_fsb snv_scpes snv_preserve
equivalence	decomposed rt-equivalence	scpes ( ⦃?,?⦄ ⊢ ? •*⬌*[?,?,?,?] ? )	scpes_aaa scpes_cpcs scpes_scpes
	context-sensitive equivalence	cpcs ( ⦃?,?⦄ ⊢ ? ⬌* ? )	cpcs_aaa cpcs_cprs cpcs_cpcs
conversion	context-sensitive conversion	cpc ( ⦃?,?⦄ ⊢ ? ⬌ ? )	cpc_cpc
computation	evaluation for context-sensitive rt-reduction	cpxe ( ⦃?,?⦄ ⊢ ➡*[?,?] 𝐍⦃?⦄ )
	evaluation for context-sensitive reduction	cpre ( ⦃?,?⦄ ⊢ ➡* 𝐍⦃?⦄ )	cpre_cpre
	strongly normalizing qrst-computation	fsb ( ⦥[?,?] ⦃?,?,?⦄ )	fsb_alt ( ⦥⦥[?,?] ⦃?,?,?⦄ )	fsb_aaa fsb_csx
	strongly normalizing rt-computation	lcosx ( ? ⊢ ~⬊*[?,?,?] ? )	lcosx_cpx
		lsx ( ? ⊢ ⬊*[?,?,?,?] ? )	lsx_alt ( ? ⊢ ⬊⬊*[?,?,?,?] ? )	lsx_drop lsx_lpx lsx_lpxs llsx_csx
		csx_vector ( ⦃?,?⦄ ⊢ ⬊*[?,?] ? )	csx_tsts_vector csx_aaa
		csx ( ⦃?,?⦄ ⊢ ⬊*[?,?] ? )	csx_alt ( ⦃?,?⦄ ⊢ ⬊⬊*[?,?] ? )	csx_lift csx_lleq csx_lpx csx_lpxs csx_fpbs
	parallel qrst-computation	fpbg ( ⦃?,?,?⦄ >≡[?,?] ⦃?,?,?⦄ )	fpbg_lift fpbg_fleq fpbg_fpbs fpbg_fpbg
		fpbs ( ⦃?,?,?⦄ ≥[?,?] ⦃?,?,?⦄ )	fpbs_alt ( ⦃?,?,?⦄ ≥≥[?,?] ⦃?,?,?⦄ )	fpbs_lift fpbs_aaa fpbs_fpb fpbs_fpbs
	decomposed rt-computation	scpds ( ⦃?,?⦄ ⊢ ? •*➡*[?,?,?] ? )	scpds_lift scpds_aaa scpds_scpds
	context-sensitive rt-computation	lpxs ( ⦃?,?⦄ ⊢ ➡*[?,?] ? )	lpxs_drop lpxs_lleq lpxs_aaa lpxs_cpxs lpxs_lpxs
		cpxs ( ⦃?,?⦄ ⊢ ? ➡*[?,?] ? )	cpxs_tsts cpxs_tsts_vector cpxs_lreq cpxs_lift cpxs_lleq cpxs_aaa cpxs_cpxs
	context-sensitive computation	lprs ( ⦃?,?⦄ ⊢ ➡* ? )	lprs_drop lprs_cprs lprs_lprs
		cprs ( ⦃?,?⦄ ⊢ ? ➡* ?)	cprs_lift cprs_cprs
	local env. ref. for generic reducibility	lsubc ( ? ⊢ ? ⫃[?] ? )	lsubc_drop lsubc_drops lsubc_lsuba
	support for generic computation properties	gcp	gcp_cr ( ⦃?,?,?⦄ ϵ[?] 〚?〛 )	gcp_aaa
reduction	parallel qrst-reduction	fpbq ( ⦃?,?,?⦄ ≽[?,?] ⦃?,?,?⦄ )	fpbq_alt ( ⦃?,?,?⦄ ≽≽[?,?] ⦃?,?,?⦄ )	fpbq_lift fpbq_aaa
		fpb ( ⦃?,?,?⦄ ≻[?,?] ⦃?,?,?⦄ )	fpb_lift fpb_lleq fpb_fleq
	normal forms for context-sensitive rt-reduction	cnx ( ⦃?,?⦄ ⊢ ➡[?,?] 𝐍⦃?⦄ )	cnx_lift cnx_crx cnx_cix
	context-sensitive rt-reduction	lpx ( ⦃?,?⦄ ⊢ ➡[?,?] ? )	lpx_drop lpx_frees lpx_lleq lpx_aaa
		cpx ( ⦃?,?⦄ ⊢ ? ➡[?,?] ? )	cpx_lreq cpx_lift cpx_llpx_sn cpx_lleq cpx_cix
	irreducible forms for context-sensitive rt-reduction	cix ( ⦃?,?⦄ ⊢ ➡[?,?] 𝐈⦃?⦄ )	cix_lift
	reducible forms for context-sensitive rt-reduction	crx ( ⦃?,?⦄ ⊢ ➡[?,?] 𝐑⦃?⦄ )	crx_lift
	normal forms for context-sensitive reduction	cnr ( ⦃?,?⦄ ⊢ ➡ 𝐍⦃?⦄ )	cnr_lift cnr_crr cnr_cir
	context-sensitive reduction	lpr ( ⦃?,?⦄ ⊢ ➡ ? )	lpr_drop lpr_lpr
		cpr ( ⦃?,?⦄ ⊢ ? ➡ ? )	cpr_lift cpr_llpx_sn cpr_cir
	irreducible forms for context-sensitive reduction	cir ( ⦃?,?⦄ ⊢ ➡ 𝐈⦃?⦄ )	cir_lift
	reducible forms for context-sensitive reduction	crr ( ⦃?,?⦄ ⊢ ➡ 𝐑⦃?⦄ )	crr_lift
unfold	unfold	unfold ( ⦃?,?⦄ ⊢ ? ⧫* ? )
	iterated static type assignment	lstas ( ⦃?,?⦄ ⊢ ? •*[?,?] ? )	lstas_lift lstas_llpx_sn.ma lstas_aaa lstas_da lstas_lstas
static typing	local env. ref. for degree assignment	lsubd ( ? ⊢ ? ⫃▪[?,?] ? )	lsubd_da lsubd_lsubd
	degree assignment	da ( ⦃?,?⦄ ⊢ ? ▪[?,?] ? )	da_lift da_aaa da_da
	parameters	sh	sd
	local env. ref. for atomic arity assignment	lsuba ( ? ⊢ ? ⫃⁝ ? )	lsuba_aaa lsuba_lsuba
	atomic arity assignment	aaa ( ⦃?,?⦄ ⊢ ? ⁝ ? )	aaa_lift aaa_lifts aaa_fqus aaa_lleq aaa_aaa
	restricted local env. ref.	lsubr ( ? ⫃ ? )	lsubr_lsubr
multiple substitution	lazy equivalence	fleq ( ⦃?,?,?⦄ ≡[?] ⦃?,?,?⦄ )	fleq_fleq
		lleq ( ? ≡[?,?] ? )	lleq_alt lleq_alt_rec lleq_lreq lleq_drop lleq_fqus lleq_llor lleq_lleq
	lazy pointwise extension of a relation	llpx_sn	llpx_sn_alt llpx_sn_alt_rec llpx_sn_tc llpx_sn_lreq llpx_sn_drop llpx_sn_lpx_sn llpx_sn_frees llpx_sn_llor
	pointwise union for local environments	llor ( ? ⋓[?,?] ? ≡ ? )	llor_alt llor_drop
	context-sensitive exclusion from free variables	frees ( ? ⊢ ? ϵ 𝐅*[?]⦃?⦄ )	frees_append frees_lreq frees_lift
	context-sensitive multiple rt-substitution	cpys ( ⦃?,?⦄ ⊢ ? ▶*[?,?] ? )	cpys_alt ( ⦃?,?⦄ ⊢ ? ▶▶*[?,?] ? )	cpys_lift cpys_cpys
	iterated structural successor for closures	fqus ( ⦃?,?,?⦄ ⊐* ⦃?,?,?⦄ )	fqus_alt fqus_fqus
		fqup ( ⦃?,?,?⦄ ⊐+ ⦃?,?,?⦄ )	fqup_fqup
	iterated local env. slicing	drops ( ⬇*[?,?] ? ≡ ? )	drops_drop drops_drops
	generic term relocation	lifts_vector ( ⬆*[?] ? ≡ ? )	lifts_lift_vector
		lifts ( ⬆*[?] ? ≡ ? )	lifts_lift lifts_lifts
	support for multiple relocation	mr2 ( @⦃?,?⦄ ≡ ? )	mr2_plus ( ? + ? )	mr2_minus ( ? ▭ ? ≡ ? )	mr2_mr2
substitution	structural successor for closures	fquq ( ⦃?,?,?⦄ ⊐⸮ ⦃?,?,?⦄ )	fquq_alt ( ⦃?,?,?⦄ ⊐⊐⸮ ⦃?,?,?⦄ )
		fqu ( ⦃?,?,?⦄ ⊐ ⦃?,?,?⦄ )
	global env. slicing	gget ( ⬇[?] ? ≡ ? )	gget_gget
	context-sensitive ordinary rt-substitution	cpy ( ⦃?,?⦄ ⊢ ? ▶[?,?] ? )	cpy_lift cpy_nlift cpy_cpy
	local env. ref. for rt-substitution	lsuby ( ? ⊆[?,?] ? )	lsuby_lsuby
	pointwise extension of a relation	lpx_sn	lpx_sn_alt lpx_sn_tc lpx_sn_drop lpx_sn_lpx_sn
	basic local env. slicing	drop ( ⬇[?,?,?] ? ≡ ? )	drop_append drop_lreq drop_drop
	basic term relocation	lift_vector ( ⬆[?,?] ? ≡ ? )	lift_lift_vector
		lift ( ⬆[?,?] ? ≡ ? )	lift_neq lift_lift
grammar	equivalence for local environments	lreq ( ? ⩬[?,?] ? )	lreq_lreq
	same top term structure	tsts ( ? ≂ ? )	tsts_tsts tsts_vector
	closures	cl_weight ( ♯{?,?,?} )	cl_restricted_weight ( ♯{?,?} )
	internal syntax	genv
		lenv	lenv_weight ( ♯{?} )	lenv_length ( |?| )	lenv_append ( ? @@ ? )
		term	term_weight ( ♯{?} )	term_simple ( 𝐒⦃?⦄ )	term_vector ( Ⓐ?.? )
		item
	external syntax	aarity