[\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) 152866 (114) nodes (objects) 347696 (948) intrinsic loss factor 2.3
propositions theorems 42 lemmas 724 total 766
concepts declared 68 defined 77 total 145
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 ( ๐โด?,?โต )


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





















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





















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: Fri, 13 Jul 2018 17:34:23 +0200