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

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

category	objects
sizes	files	79	characters	97505	nodes	207728
propositions	theorems	23	lemmas	497	total	520
concepts	declared	54	defined	52	total	106

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