[\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) 156773 (124) nodes (objects) 354238 (966) intrinsic loss factor 2.2
propositions theorems 44 lemmas 737 total 781
concepts declared 71 defined 77 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 ( ๐โด?,?โต )


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: Thu, 08 Nov 2018 17:30:52 +0100