Here is a numerical account of the specification's contents
and its timeline.
@@ -132,33 +132,39 @@
sizes |
files |
- 68 |
+ 86 |
characters |
- 83858 |
+ 109249 |
nodes |
- 168408 |
+ 217872 |
propositions |
theorems |
- 14 |
+ 30 |
lemmas |
- 388 |
+ 506 |
total |
- 402 |
+ 536 |
concepts |
declared |
- 42 |
+ 59 |
defined |
- 44 |
+ 55 |
total |
- 86 |
+ 114 |
Logical Structure of the Specification
![lambdadelta butterfly [spacer]](http://lambdadelta.info/images/b4.png)
+
Logical Structure of the Specification
This table reports the specification's components and their planes.
@@ -227,19 +233,126 @@
|
+
+
+ |
+
+
+ |
+
+
+ |
+
+
+ |
+
+
+ |
|
- natural numbers with infinity |
+ generic rt-transition counter |
+ |
+ rtc ( â©?,?,?,?⪠) ( ðð ) ( ðð ) ( ðð ) |
+ rtc_shift ( â? ) |
+ rtc_plus ( ? + ? ) |
+
+
+ |
+
+
+ |
+
+
+ |
+
+
+ |
+
+
+ |
+
+
+ |
+
+
+ |
+
+
+ |
+
+
+ |
+
+
+ |
+
+
+ |
+
+
+ |
+
+
+ |
+
+
+ multiple relocation |
|
- ynat ( â ) |
- ynat_pred ( â«°? ) |
- ynat_succ ( ⫯? ) |
- ynat_le ( ? ⤠? ) |
- ynat_lt ( ? < ? ) |
- ynat_plus ( ? + ? ) |
+ rtmap |
+ rtmap_eq ( ? â ? ) |
+ 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 ( ? â ? â¡ ? ) |
+
+
+
+
+ |
+
+
+ |
+ nstream ( â? ) ( ⫯? ) |
+ nstream_eq |
+ |
+ |
+ nstream_isid |
+ nstream_id ( ðð ) |
+ |
+ |
+ |
+ |
+ |
+ nstream_sand |
+ |
+ |
+ nstream_istot ( ?@â´?âµ ) |
+ nstream_after ( ? â ? ) |
+
+
+
+
+ |
+
+
+ |
+ mr2 |
+ mr2_at ( @�,?⦠⡠? ) |
+ mr2_plus ( ? + ? ) |
+ mr2_minus ( ? â ? â¡ ? ) |
|
@@ -252,55 +365,49 @@
|
-
+ |
|
-
-
- multiple relocation |
- |
- rtmap |
- rtmap_eq ( ? â ? ) |
- rtmap_tl ( â? ) |
- rtmap_minus ( ? - ? ) |
- rtmap_isid ( ðâ¦?⦠) |
- rtmap_id |
- rtmap_sle ( ? â ? ) |
- rtmap_sand ( ? â ? â¡ ? ) |
- rtmap_at ( @�,?⦠⡠? ) |
- rtmap_istot ( ðâ¦?⦠) |
- rtmap_after ( ? â ? â¡ ? ) |
-
-
-
+ |
+
+ |
+
+
+ |
+
+
+ |
+
+
+ |
+
|
-
+ |
+
+ |
+
|
- nstream ( â? ) ( ⫯? ) |
- nstream_eq |
- |
- |
- nstream_isid |
- nstream_id ( ðð ) |
- |
- nstream_sand |
- |
- nstream_istot ( ?@â´?âµ ) |
- nstream_after ( ? â ? ) |
-
+ | natural numbers with infinity |
+ |
+ ynat ( â ) |
+ ynat_pred ( â«°? ) |
+ ynat_succ ( ⫯? ) |
+ ynat_le ( ? ⤠? ) |
+ ynat_lt ( ? < ? ) |
+ ynat_plus ( ? + ? ) |
+
|
-
+ |
+
+ |
+
|
- mr2 |
- mr2_at ( @�,?⦠⡠? ) |
- mr2_plus ( ? + ? ) |
- mr2_minus ( ? â ? â¡ ? ) |
|
@@ -326,8 +433,19 @@
extensions to the library |
|
- stream ( ? @ ? ) ( ? â ? ) |
- stream_hdtl |
+ stream ( ? @ ? ) |
+ stream_eq ( ? â ? ) |
+ stream_hdtl ( â? ) |
+ stream_tls ( â*[?]? ) |
+
+
+ |
+
+
+ |
+
+
+ |
|
@@ -389,6 +507,21 @@
|
+
+
+ |
+
+
+ |
+
+
+ |
+
+
+ |
+
+
+ |
|
@@ -401,7 +534,22 @@
bool ( â» ) ( â ) |
- arith ( ?^? ) ( ⫯? ) ( ⫰? ) |
+ arith ( ?^? ) ( ⫯? ) ( ⫰? ) ( ? ⨠? ) ( ? ⧠? ) |
+
+
+ |
+
+
+ |
+
+
+ |
+
+
+ |
+
+
+ |
|
@@ -463,6 +611,21 @@
|
+
+
+ |
+
+
+ |
+
+
+ |
+
+
+ |
+
+
+ |
|
@@ -496,6 +659,21 @@
|
+
+
+ |
+
+
+ |
+
+
+ |
+
+
+ |
+
+
+ |
|
@@ -533,6 +711,21 @@
|
+
+
+ |
+
+
+ |
+
+
+ |
+
+
+ |
+
+
+ |
|
@@ -541,7 +734,7 @@
-
![lambdadelta rainbow rule [Spacer]](http://lambdadelta.info/images/rainbow.png)
+
@@ -566,6 +759,6 @@
-
Last update: Fri, 04 Mar 2016 16:15:58 +0100
+
Last update: Thu, 19 May 2016 12:17:40 +0200