Summary of the Specification [spacer]

Summary of the Specification $\lambda\delta butterfly$

Here is a numerical account of the specification's contents and its timeline. @@ -132,33 +132,39 @@ sizes files - 69 + 95 characters - 83843 + 131558 nodes - 168516 + 304213 propositions theorems - 14 + 37 lemmas - 388 + 626 total - 402 + 663 concepts declared - 42 + 62 defined - 44 + 66 total - 86 + 128

+ 2016 April 18. + Generic rt-transition counter (rtc). +

2016 March 4. @@ -189,7 +195,7 @@ Specification starts.

Logical Structure of the Specification [spacer]

Logical Structure of the Specification $\lambda\delta butterfly$

This table reports the specification's components and their planes.

@@ -227,19 +233,165 @@
+ +
+ + +
+ + +
+ + +
+ + +
+ + +
+ + +
+
- 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_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 ( ? â ? â¡ ? ) + +
+ + +
+ + +
+ + +
+ + +
+ + +
+ + +
+ + +
+ + +
+
@@ -257,50 +409,29 @@ - multiple relocation + natural numbers with infinity - rtmap - rtmap_eq ( ? â ? ) - rtmap_tl ( â«±? ) - rtmap_tls ( â«±*[?]? ) - rtmap_isid ( ðâ¦?â¦ ) - rtmap_id - rtmap_sle ( ? â ? ) - rtmap_sand ( ? â ? â¡ ? ) - rtmap_at ( @â¦?,?â¦ â¡ ? ) - rtmap_istot ( ðâ¦?â¦ ) - rtmap_after ( ? â ? â¡ ? ) - - - + ynat ( â ) + ynat_pred ( â«°? ) + ynat_succ ( â«¯? ) + ynat_le ( ? â¤ ? ) + ynat_lt ( ? < ? ) + ynat_plus ( ? + ? ) +
- +
- nstream ( â? ) ( â«¯? ) - nstream_eq - - - nstream_isid - nstream_id ( ðð ) - - nstream_sand - - nstream_istot ( ?@â´?âµ ) - nstream_after ( ? â ? ) - - - +
- + +
+ +
- mr2 - mr2_at ( @â¦?,?â¦ â¡ ? ) - mr2_plus ( ? + ? ) - mr2_minus ( ? â ? â¡ ? )
@@ -348,6 +479,27 @@
+ +
+ + +
+ + +
+ + +
+ + +
+ + +
+ + +
+
@@ -385,6 +537,27 @@
+ +
+ + +
+ + +
+ + +
+ + +
+ + +
+ + +
+
@@ -397,7 +570,28 @@
bool ( â» ) ( â ) - arith ( ?^? ) ( â«¯? ) ( â«°? ) + arith ( ?^? ) ( â«¯? ) ( â«°? ) ( ? â¨ ? ) ( ? â§ ? ) + +
+ + +
+ + +
+ + +
+ + +
+ + +
+ + +
+
@@ -459,6 +653,27 @@
+ +
+ + +
+ + +
+ + +
+ + +
+ + +
+ + +
+
@@ -492,6 +707,27 @@
+ +
+ + +
+ + +
+ + +
+ + +
+ + +
+ + +
+
@@ -529,6 +765,27 @@
+ +
+ + +
+ + +
+ + +
+ + +
+ + +
+ + +
+
@@ -537,7 +794,7 @@

+ $\lambda\delta rainbow rule$

@@ -562,6 +819,6 @@

Last update: Fri, 04 Mar 2016 20:49:20 +0100

Last update: Thu, 15 Sep 2016 17:33:01 +0200