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	79	characters	96249	nodes	206180
propositions	theorems	23	lemmas	495	total	518
concepts	declared	53	defined	50	total	103

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_uni ( 𝐔❴?❵ )

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 ( ⊥ ) ( ⊤ )