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	77	characters	93671	nodes	198031
propositions	theorems	23	lemmas	472	total	495
concepts	declared	53	defined	49	total	102

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

rtmap

rtmap_eq ( ? ≗ ? )

rtmap_tl ( ⫱? )

rtmap_tls ( ⫱*[?]? )

rtmap_isid ( 𝐈⦃?⦄ )

rtmap_id

rtmap_fcla ( 𝐂⦃?⦄ ≡ ? )

rtmap_isfin ( 𝐅⦃?⦄ )

rtmap_isuni ( 𝐔⦃?⦄ )

rtmap_sle ( ? ⊆ ? )

rtmap_sand ( ? ⋒ ? ≡ ? )

rtmap_sor ( ? ⋓ ? ≡ ? )

rtmap_at ( @⦃?,?⦄ ≡ ? )

rtmap_istot ( 𝐓⦃?⦄ )

rtmap_after ( ? ⊚ ? ≡ ? )

nstream ( ↑? ) ( ⫯? )

nstream_eq

nstream_isid

nstream_id ( 𝐈𝐝 )

nstream_sand

nstream_istot ( ?@❴?❵ )

nstream_after ( ? ∘ ? )

mr2

mr2_at ( @⦃?,?⦄ ≡ ? )

mr2_plus ( ? + ? )

mr2_minus ( ? ▭ ? ≡ ? )

extensions to the library

stream ( ? @ ? )

stream_eq ( ? ≐ ? )

stream_hdtl ( ↓? )

stream_tls ( ↓*[?]? )

list ( ◊ ) ( ? @ ? ) ( |?| )

list2 ( ◊ ) ( {?,?} @ ? ) ( ? @@ ? ) ( |?| )

bool ( Ⓕ ) ( Ⓣ )

arith ( ?^? ) ( ⫯? ) ( ⫰? ) ( ? ∨ ? ) ( ? ∧ ? )

star

lstar

generated logical decomposables

xoa ( ∃∃ ) ( ∨∨ ) ( ∧∧ )

xoa_props ( ⊥ ) ( ⊤ )