[\lambda\delta home]
cic:/matita/lambdadelta/ground_2/ (background for ฮปฮด version 2)
[Spacer]

home news specification

documentation implementation
foreword milestones version 2 (background - syntax - 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) 157076 (124) nodes (objects) 355861 (971) intrinsic loss factor 2.3
propositions theorems 46 lemmas 740 total 786
concepts declared 70 defined 78 total 148
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 ( ? ~โŠš ? โ‰˜ ? ) rtmap_basic ( ๐โด?,?โต ) rtmap_basic_after


nstream ( โซฏ? ) ( โ†‘? ) nstream_eq nstream_isid nstream_id ( ๐ˆ๐ ) nstream_sor nstream_istot ( ?@โด?โต ) nstream_after ( ? โˆ˜ ? ) nstream_coafter ( ? ~โˆ˜ ? ) nstream_basic


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 ( โ’บ{?} ) ( ? โจฎ{?} ? ) list_length ( |?| )






















bool ( โ’ป ) ( โ“‰ ) arith ( ?^? ) ( โ†‘? ) ( โ†“? ) ( ? โˆจ ? ) ( ? โˆง ? ) arith_2a arith_2b




















ltc ltc_ctc






















logic ( โŠฅ ) ( โŠค ) relations ( ? โŠ† ? ) functions exteq ( ? โ‰{?,?} ? ) star

















generated library generalization with equality insert_eq






















permutation of quantifiers pull






















logical decomposables xoa ( โˆƒโˆƒ ) ( โˆจโˆจ ) ( โˆงโˆง )












































[Spacer]

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

Last update: Wed, 20 Mar 2019 12:14:01 +0100