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

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

category	objects
sizes	files	30	characters	68581	nodes	62380
propositions	theorems	2	lemmas	187	total	189
concepts	declared	40	defined	25	total	65

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_minus ( ? - ? )	ynat_plus ( ? + ? )	ynat_max	ynat_min
extensions to the library		star	lstar	bool ( Ⓕ ) ( Ⓣ )	arith ( ?^? )	list ( ◊ ) ( ? @ ? ) ( {?,?} @ ? ) ( ? @@ ? ) ( |?| )
generated logical decomposables		xoa ( ∃∃ ) ( ∨∨ ) ( ∧∧ )	xoa_props ( ⊥ ) ( ⊤ )