lambda_delta version 2

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

category	objects
propositions	theorems	39	lemmas	336
concepts	declared	33	defined	46

The source files are grouped in planes and components according to the following table. The notation for the relations or functions introduced in each file is shown in parentheses.

component	plane	files
functional	reduction and type machine	rtm	rtm_step ( ? ⇨ ? )
	unfold	lift ( ↑[?,?] ? )	subst ( [?←?] ? )
examples
native typing		nty
conversion	context-sensitive conversion	cpcs ( ? ⊢ ? ⬌* ? )
computation	strongly normalizing computation	csn ( ⬇* ? )	csn_cr	csn_aaa
	context-sensitive computation	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
reducibility	context-sensitive reduction	lcpr ( ? ⊢ ➡ ? )
		cpr ( ? ⊢ ? ➡ ? )	cpr_lift	cpr_tpss	cpr_ltpr	cpr_cpr
	context-free normal forms	twhnf ( 𝐖𝐇𝐍[?] )	tnf ( 𝐍[?] )	tnf_tif
	context-free reduction	ltpr ( ? ➡ ? )	ltpr_ldrop
		tpr ( ? ➡ ? )	tpr_lift	tpr_tpss	tpr_tpr
	context-free reducible forms	trf ( 𝐑[?] )	tif ( 𝐈[?] )
static typing	static type assignment	sty	sty_lift	sty_sty
	local env. ref. for atomic arity assignment	lsuba ( ? ÷⊑ ? )	lsuba_ldrop	lsuba_aaa	lsuba_lsuba
	atomic arity assignment	aaa ( ? ⊢ ? ÷ ? )	aaa_lift	aaa_lifts	aaa_aaa
	parameters	sh
unfold	term inverse relocation	delift ( ? ⊢ ? [?,?] ≡ ? )	delift_lift
	partial unfold	ltpss ( ? [?,?] ▶* ? )	ltpss_ldrop	ltpss_tps	ltpss_ltpss
		tpss ( ? ⊢ ? [?,?] ▶* ? )	tpss_lift	tpss_tpss	tpss_ltps
	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
substitution	parallel substitution	ltps ( ? [?,?] ▶ ? )	ltps_ldrop	ltps_tps	ltps_ltps
		tps ( ? ⊢ ? [?,?] ▶ ? )	tps_lift	tps_tps
	global env. slicing	gdrop ( ⇩[?] ? ≡ ? )	gdrop_gdrop
	basic local env. slicing	ldrop ( ⇩[?,?] ? ≡ ? )	ldrop_ldrop
	basic term relocation	lift_vector ( ⇧[?,?] ? ≡ ? )	lift_lift_vector
		lift ( ⇧[?,?] ? ≡ ? )	lift_lift
grammar	local env. ref. for substitution	lsubs ( ? [?,?] ≼ ? )	lsubs_lsubs
	term hom.	thom	thom_thom
	closures	cl_shift ( ? @ ? )	cl_weight ( #[?,?] )
	internal syntax	genv
		lenv	lenv_weight ( #[?] )	lenv_length ( \|?\| )
		term	term_weight ( #[?] )	term_simple ( 𝐒[?] )	term_vector
		item
	external syntax	aarity

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