[\lambda\delta home]
cic:/matita/lambdadelta/ground_2/ (background for λδ version 2)
[Spacer]

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)
Summary of the Specification [butterfly]
Here is a numerical account of the specification's contents and its timeline.
category units




sizes characters (files) 146052 (104) nodes (objects) 338333 (915) intrinsic loss factor 2.3
propositions theorems 42 lemmas 697 total 739
concepts declared 66 defined 73 total 139
Logical Structure of the Specification [butterfly]
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_nexts ( ⫯*[?]? ) rtmap_tl ( ⫱? ) rtmap_tls ( ⫱*[?]? ) rtmap_isid ( 𝐈⦃?⦄ ) rtmap_id rtmap_isdiv ( 𝛀⦃?⦄ ) rtmap_fcla ( 𝐂⦃?⦄ ≡ ? ) rtmap_isfin ( 𝐅⦃?⦄ ) rtmap_isuni ( 𝐔⦃?⦄ ) rtmap_uni ( 𝐔❴?❵ ) rtmap_sle ( ? ⊆ ? ) rtmap_sdj ( ? ∥ ? ) rtmap_sand ( ? ⋒ ? ≡ ? ) rtmap_sor ( ? ⋓ ? ≡ ? ) rtmap_at ( @⦃?,?⦄ ≡ ? ) rtmap_istot ( 𝐓⦃?⦄ ) rtmap_after ( ? ⊚ ? ≡ ? ) rtmap_coafter ( ? ~⊚ ? ≡ ? )


nstream ( ↑? ) ( ⫯? ) nstream_eq nstream_isid nstream_id ( 𝐈𝐝 ) nstream_sor 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 ( ?^? ) ( ⫯? ) ( ⫰? ) ( ? ∨ ? ) ( ? ∧ ? )




















relations ( ? ⊆ ? ) star lstar

















generated logical decomposables xoa ( ∃∃ ) ( ∨∨ ) ( ∧∧ ) xoa_props ( ⊥ ) ( ⊤ )







































[Spacer]

[Valid XHTML 1.1] [Valid CSS level 2] [Generated from XML via XSL] [PNG used here] [Viewable with any browser]

Last update: Wed, 17 Jan 2018 20:27:13 +0100