![[spacer]](http://lambdadelta.info/images/b4.png "\lambda\delta butterfly")
+ Summary of the Specification
Here is a numerical account of the specification's contents
and its timeline.
@@ -130,35 +130,41 @@
- sizes
- files
- 79
- characters
- 97505
- nodes
- 207728
+ sizes
+ files
+ 102
+ characters
+ 143239
+ nodes
+ 332273
propositions
theorems
- 23
+ 42
lemmas
- 497
+ 679
total
- 520
+ 721
- concepts
- declared
- 54
- defined
- 52
- total
- 106
+ concepts
+ declared
+ 65
+ defined
+ 70
+ total
+ 135
+ -
+
- + 2016 April 18. + Generic rt-transition counter (rtc). + +
- 2016 March 4. @@ -189,7 +195,7 @@ Specification starts.
Logical Structure of the Specification
+
+
+
+
+
+
+
+
+
+
+
+
+
- natural numbers with infinity
+ generic rt-transition counter
+ rtc ( â©?,?,?,?⪠) ( ðð ) ( ðð ) ( ðð )
+ rtc_isrc ( ððâ¦?, ?⦠)
+ rtc_shift ( â? )
+ rtc_max ( ? ⨠? )
+ rtc_plus ( ? + ? )
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+ multiple relocation
ynat ( â )
- ynat_pred ( â«°? )
- ynat_succ ( ⫯? )
- ynat_le ( ? ⤠? )
- ynat_lt ( ? < ? )
- ynat_plus ( ? + ? )
+ 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_sand ( ? â ? â¡ ? )
+ rtmap_sor ( ? â ? â¡ ? )
+ rtmap_at ( @�,?⦠⡠? )
+ rtmap_istot ( ðâ¦?⦠)
+ rtmap_after ( ? â ? â¡ ? )
+ rtmap_coafter ( ? ~â ? â¡ ? )
+
+
+
+
+
+
+
+
+ nstream ( â? ) ( ⫯? )
+ nstream_eq
+ nstream_isid
+ nstream_id ( ðð )
+ nstream_sor
+ nstream_istot ( ?@â´?âµ )
+ nstream_after ( ? â ? )
+ nstream_coafter ( ? ~â ? )
+
+
+
+
+
+
+
+
+ mr2
+ mr2_at ( @�,?⦠⡠? )
+ mr2_plus ( ? + ? )
+ mr2_minus ( ? â ? â¡ ? )
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
@@ -287,60 +431,20 @@
- multiple relocation
+ natural numbers with infinity
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 ( ? â ? )
-
-
-
+ ynat ( â )
+ ynat_pred ( â«°? )
+ ynat_succ ( ⫯? )
+ ynat_le ( ? ⤠? )
+ ynat_lt ( ? < ? )
+ ynat_plus ( ? + ? )
+
-
+
- mr2
- mr2_at ( @�,?⦠⡠? )
- mr2_plus ( ? + ? )
- mr2_minus ( ? â ? â¡ ? )
@@ -418,6 +522,18 @@
+
+
+
+
+
+
+
+
+
+
+
+
@@ -470,6 +586,18 @@
+
+
+
+
+
+
+
+
+
+
+
+
@@ -522,6 +650,18 @@
+
+
+
+
+
+
+
+
+
+
+
+
@@ -533,7 +673,8 @@
- star
+ relations
+ star
lstar
@@ -574,6 +715,15 @@
+
+
+
+
+
+
+
+
+
@@ -622,6 +772,18 @@
+
+
+
+
+
+
+
+
+
+
+
+
@@ -674,6 +836,18 @@
+
+
+
+
+
+
+
+
+
+
+
+
@@ -707,6 +881,6 @@
-
+ Logical Structure of the Specification
This table reports the specification's components and their planes.
@@ -242,19 +248,157 @@
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
-
-
+
+
+
+
+
+
+
+
+
+
+
+
@@ -574,6 +715,15 @@
+
+
+
+
+
+
+
+
+
+
+
Last update: Sat, 16 Apr 2016 14:53:00 +0200
+ Last update: Mon, 13 Nov 2017 18:11:08 +0100