home	news	specification			documentation	implementation
foreword	milestones	version 2	(background - core - applications)		version 2	helena	Open Symbolic Notation (OSN)
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	95	characters	131558	nodes	304213
propositions	theorems	37	lemmas	626	total	663
concepts	declared	62	defined	66	total	128

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

component

plane

files

generic rt-transition counter

rtc ( 〈?,?,?,?〉 ) ( 𝟘𝟘 ) ( 𝟙𝟘 ) ( 𝟘𝟙 )

rtc_isrc ( 𝐑𝐓⦃?, ?⦄ )

rtc_shift ( ↓? )

rtc_max ( ? ∨ ? )

rtc_plus ( ? + ? )

multiple relocation

rtmap

rtmap_eq ( ? ≗ ? )

rtmap_pushs ( ↑*[?]? )

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 ( ? ⊚ ? ≡ ? )

rtmap_coafter ( ? ~⊚ ? ≡ ? )

nstream ( ↑? ) ( ⫯? )

nstream_eq

nstream_isid

nstream_id ( 𝐈𝐝 )

nstream_sand

nstream_istot ( ?@❴?❵ )

nstream_after ( ? ∘ ? )

nstream_coafter ( ? ~∘ ? )

mr2

mr2_at ( @⦃?,?⦄ ≡ ? )

mr2_plus ( ? + ? )

mr2_minus ( ? ▭ ? ≡ ? )

natural numbers with infinity

ynat ( ∞ )

ynat_pred ( ⫰? )

ynat_succ ( ⫯? )

ynat_le ( ? ≤ ? )

ynat_lt ( ? < ? )

ynat_plus ( ? + ? )

extensions to the library

stream ( ? @ ? )

stream_eq ( ? ≐ ? )

stream_hdtl ( ↓? )

stream_tls ( ↓*[?]? )

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

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

bool ( Ⓕ ) ( Ⓣ )

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

star

lstar

generated logical decomposables

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

xoa_props ( ⊥ ) ( ⊤ )