This is a summary of the "block structure" of the System's syntactic items and reductions.

domain	block	leader	applicator (with →θ)*	reduction	→ζ *	reference *
{X | Γ ⊢ X : W}	local typed abstraction *	Γ ⊢ +λW	ⓐV	→β	no	#i
	local typed declaration **	Γ ⊢ -λW	ⓐV	→β	no	#i
	global typed declaration ***	Γ ⊢ pλW	no	no	no	$p
	native type annotation *	Γ ⊢ ⓝW	no	no	yes	no
{X | Γ ⊢ X = V}	local abbreviation *	Γ ⊢ +δV	no	local →δ	yes	#i
	local definition **	Γ ⊢ -δV	no	local →δ	no	#i
	global definition ***	Γ ⊢ pδV	no	global →δ	no	$p
no	sort ****	Γ ⊢ ⋆k	no	no	no	no

* In terms only. ** In terms and local environments only. *** In global environments only. **** Sort level k in terms only.

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

category	objects
sizes	files	176	characters	373293	nodes	1085467
propositions	theorems	76	lemmas	780	total	856
concepts	declared	43	defined	71	total	114

The source files are grouped in planes and components according to the following table. A notation file covering the whole specification is provided. The notation for the relations or functions introduced in each file is shown in parentheses (? are placeholders).

component	plane	files
dynamic typing	"big tree" parallel computation	yprs ( ? ⊢ ⦃?,?⦄ ≥[g] ⦃?,?⦄ )	yprs_yprs	ygt ( ? ⊢ ⦃?,?⦄ >[g] ⦃?,?⦄ )	ygt_ygt
	"big tree" parallel reduction	ypr ( ? ⊢ ⦃?,?⦄ ≽[g] ⦃?,?⦄ )	ysc ( ? ⊢ ⦃?,?⦄ ≻[g] ⦃?,?⦄ )
	local env. ref. for stratified native validity	lsubsv ( ? ⊢ ? ¡⊑[?] ? )	lsubsv_ldrop lsubsv_lsuba lsubsv_ssta lsubsv_dxprs lsubsv_cpcs lsubsv_snv
	stratified native validity	snv ( ⦃?,?⦄ ⊢ ? ¡[?] )	snv_lift snv_lpss snv_aaa snv_ssta snv_sstas snv_ssta_lpr snv_lpr snv_cpcs
equivalence	local env. ref. for stratified static type assignment	lsubss ( ? •⊑[?] ? )	lsubss_ldrop lsubss_ssta lsubss_cpcs
	context-sensitive equivalence	cpcs ( ? ⊢ ? ⬌* ? )	cpcs_lpss cpcs_aaa cpcs_cprs cpcs_cpcs
conversion	context-sensitive conversion	cpc ( ? ⊢ ? ⬌ ? )	cpc_cpc
computation	decomposed extended computation	dxprs ( ⦃?,?⦄ ⊢ ? •*➡*[?] ? )	dxprs_lift dxprs_lpss dxprs_aaa dxprs_dxprs
	context-sensitive extended computation	cpxs ( ⦃?,?⦄ ⊢ ? ➡*[?] ? )	cpxs_lift
	weakly normalizing computation	cpe ( ? ⊢ ➡* 𝐍⦃?⦄ )	cpe_cpe
	strongly normalizing computation	csn_vector ( ? ⊢ ⬊* ? )	csn_tstc_vector csn_aaa
		csn ( ? ⊢ ⬊* ? )	csn_alt ( ? ⊢ ⬊⬊* ? )	csn_lift csn_lpr
	context-sensitive computation	lprs ( ? ⊢ ➡* ? )	lprs_alt ( ? ⊢ ➡➡* ? )	lprs_ldrop lprs_lpss lprs_aaa lprs_cprs lprs_lprs
		cprs ( ? ⊢ ? ➡* ?)	cprs_tstc cprs_tstc_vector cprs_lift cprs_lpss cprs_aaa cprs_cprs
	local env. ref. for abstract candidates of reducibility	lsubc ( ? ⊑[?] ? )	lsubc_ldrop lsubc_ldrops lsubc_lsuba
	support for abstract computation properties	acp	acp_cr ( ⦃?,?⦄ ϵ[?] 〚?〛 )	acp_aaa
reduction	context-sensitive extended reduction	lpx ( ⦃?,?⦄ ⊢ ➡[?] ? )	lpx_ldrop lpx_aaa
		cpx ( ⦃?,?⦄ ⊢ ? ➡[?] ? )	cpx_lift
	context-sensitive normal forms	cnf ( ? ⊢ 𝐍⦃?⦄ )	cnf_liftt cnf_crf cnf_cif
	context-sensitive reduction	lpr ( ? ⊢ ➡ ? )	lpr_ldrop lpr_lpss lpr_lpr
		cpr ( ? ⊢ ? ➡ ? )	cpr_lift cpr_cif
	context-sensitive reducible forms	crf ( ? ⊢ 𝐑⦃?⦄ )	crf_append	cif ( ? ⊢ 𝐈⦃?⦄ )	cif_append
unfold	restricted parallel computation	lpqs ( ? ⊢ ➤* ? )	lpqs_ldrop lpqs_cpqs lpqs_lpqs
		cpqs ( ? ⊢ ? ➤* ? )	cpqs_lift
	unfold	unfold ( ? ⊢ ? ⧫* ? )
	iterated stratified static type assignment	sstas ( ⦃?,?⦄ ⊢ ? •*[?] ? )	sstas_lift sstas_lpss sstas_aaa sstas_sstas
static typing	stratified static type assignment	ssta ( ⦃?,?⦄ ⊢ ? •[?,?] ? )	ssta_lift ssta_lpss ssta_aaa ssta_ssta
	local env. ref. for atomic arity assignment	lsuba ( ? ⁝⊑ ? )	lsuba_ldrop lsuba_aaa lsuba_lsuba
	atomic arity assignment	aaa ( ? ⊢ ? ⁝ ? )	aaa_lift aaa_lifts aaa_lpss aaa_aaa
	parameters	sh	sd
substitution	parallel substitution	lpss ( ? ⊢ ▶* ? )	lpss_ldrop lpss_cpss lpss_lpss
		cpss ( ? ⊢ ? ▶* ? )	cpss_lift
	local env. ref. for substitution	lsubr ( ? ⊑ ? )	lsubr_lsubr
	iterated structural successor for closures	fsups ( ⦃?,?⦄ ⊃* ⦃?,?⦄ )	fsups_fsups
		fsupp ( ⦃?,?⦄ ⊃+ ⦃?,?⦄ )	fsupp_fsupp
	generic local env. slicing	ldrops ( ⇩*[?] ? ≡ ? )	ldrops_ldrop ldrops_ldrops
	generic term relocation	lifts_vector ( ⇧*[?] ? ≡ ? )	lifts_lift_vector
		lifts ( ⇧*[?] ? ≡ ? )	lifts_lift lifts_lifts
	support for generic relocation	gr2 ( @⦃?,?⦄ ≡ ? )	gr2_plus ( ? + ? )	gr2_minus ( ? ▭ ? ≡ ? )	gr2_gr2
relocation	structural successor for closures	fsup ( ⦃?,?⦄ ⊃ ⦃?,?⦄ )	fsupq ( ⦃?,?⦄ ⊃⸮ ⦃?,?⦄ )	fsupq_alt
	global env. slicing	gdrop ( ⇩[?] ? ≡ ? )	gdrop_gdrop
	basic local env. slicing	ldrop ( ⇩[?,?] ? ≡ ? )	ldrop_append ldrop_lpx_sn ldrop_ldrop
	basic term relocation	lift_vector ( ⇧[?,?] ? ≡ ? )	lift_lift_vector
		lift ( ⇧[?,?] ? ≡ ? )	lift_lift
grammar	pointwise extension of a relation	lpx_sn	lpx_sn_tc lpx_sn_lpx_sn
	same top term constructor	tstc ( ? ≃ ? )	tstc_tstc tstc_vector
	closures	cl_shift ( ? @@ ? )	cl_weight ( ♯{?,?} )
	internal syntax	genv
		lenv	lenv_weight ( ♯{?} )	lenv_length ( |?| )	lenv_append ( ? @@ ? )
		term	term_weight ( ♯{?} )	term_simple ( 𝐒⦃?⦄ )	term_vector
		item
	external syntax	aarity

The source files are grouped in directories, one for each component.