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	54	characters		nodes	152278
propositions	theorems	15	lemmas	328	total	343
concepts	declared	48	defined	39	total	87

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

component	plane	files
multiple relocation		nstream	nstream_at ( ?@❴?❵ ) ( @⦃?,?⦄ ≡ ? )
		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 ( ◊ ) ( {?,?} @ ? ) ( ? @@ ? ) ( |?| )	stream ( ? @ ? ) ( ? ≐ ? )	stream_hdtl
generated logical decomposables		xoa ( ∃∃ ) ( ∨∨ ) ( ∧∧ )	xoa_props ( ⊥ ) ( ⊤ )