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	59	characters	86572	nodes	195099
propositions	theorems	17	lemmas	395	total	412
concepts	declared	48	defined	43	total	91

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

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