[\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 objects




sizes files 95 characters 135595 nodes 314345
propositions theorems 38 lemmas 647 total 685
concepts declared 63 defined 67 total 130
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_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 ( โŠฅ ) ( โŠค )

































[Spacer]

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

Last update: Thu, 02 Mar 2017 17:01:48 +0100