\lambda\delta home page

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	93	characters	135543	nodes	314125
propositions	theorems	38	lemmas	647	total	685
concepts	declared	63	defined	67	total	130

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