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

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

category	objects
sizes	files	48	characters	66783	nodes	134126
propositions	theorems	9	lemmas	298	total	307
concepts	declared	47	defined	32	total	79

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

component	plane	files
multiple relocation		trace ( ∥?∥ )	trace_at ( @⦃?,?⦄ ≡ ? )	trace_after ( ? ⊚ ? ≡ ? )	trace_isid ( 𝐈⦃?⦄ )	trace_isun ( 𝐔⦃?⦄ )	trace_sle ( ? ⊆ ? )	trace_sor ( ? ⋓ ? ≡ ? )	trace_snot ( ∁ ? )
		mr2	mr2_at ( @⦃?,?⦄ ≡ ? )	mr2_plus ( ? + ? )	mr2_minus ( ? ▭ ? ≡ ? )
natural numbers with infinity		ynat ( ∞ )	ynat_pred ( ⫰? )	ynat_succ ( ⫯? )	ynat_le ( ? ≤ ? )	ynat_lt ( ? < ? )	ynat_plus ( ? + ? )
extensions to the library		star	lstar	bool ( Ⓕ ) ( Ⓣ )	arith ( ?^? ) ( ⫯? ) ( ⫰? )	list ( ◊ ) ( ? @ ? ) ( |?| )	list2 ( ◊ ) ( {?,?} @ ? ) ( ? @@ ? ) ( |?| )
generated logical decomposables		xoa ( ∃∃ ) ( ∨∨ ) ( ∧∧ )	xoa_props ( ⊥ ) ( ⊤ )