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. @@ -112,7 +112,7 @@ category - objects + units
@@ -130,35 +130,53 @@ - sizes - files - 54 - characters - - nodes - 152278 + sizes + characters (files) + 145725 (104) + nodes (objects) + 337452 (911) + intrinsic loss factor + 2.3 propositions theorems - 15 + 42 lemmas - 328 + 693 total - 343 + 735 - concepts - declared - 48 - defined - 39 - total - 87 + concepts + declared + 66 + defined + 73 + total + 139

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

+ 2016 March 4. + Platform-independent multiple relocation (rtmap). +

+ 2016 January 20. + Multiple relocation with streams of naturals. +

2015 October 11. @@ -168,7 +186,7 @@
- 2013 November 27. - Natural numbers with infinity. + Natural numbers with infinity (ynat).
-
Logical Structure of the Specification +
Logical Structure of the Specification $\lambda\delta butterfly$

This table reports the specification's components and their planes.
@@ -206,33 +224,130 @@
+ +
+ + +
+ + +
+ + +
+ + +
+ + +
+ + +
+ + +
+ + +
+ + +
+ + +
+ + +
+ + +
+
- multiple relocation - - nstream - nstream_at ( ?@â´?âµ ) ( @â¦?,?â¦ â¡ ? ) - + 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 ( ? ~â ? â¡ ? ) @@ -241,14 +356,27 @@
- trace ( â¥?â¥ ) - trace_at ( @â¦?,?â¦ â¡ ? ) - trace_after ( ? â ? â¡ ? ) - trace_isid ( ðâ¦?â¦ ) - trace_isun ( ðâ¦?â¦ ) - trace_sle ( ? â ? ) - trace_sor ( ? â ? â¡ ? ) - trace_snot ( â ? ) + nstream ( â? ) ( â«¯? ) + nstream_eq + + + + + nstream_isid + nstream_id ( ðð ) + + + + + + + + + nstream_sor + + nstream_istot ( ?@â´?âµ ) + nstream_after ( ? â ? ) + nstream_coafter ( ? ~â ? ) @@ -270,6 +398,45 @@
+ +
+ + +
+ + +
+ + +
+ + +
+ + +
+ + +
+ + +
+ + +
+ + +
+ + +
+ + +
+ + +
+
@@ -286,6 +453,45 @@
+ +
+ + +
+ + +
+ + +
+ + +
+ + +
+ + +
+ + +
+ + +
+ + +
+ + +
+ + +
+ + +
+
@@ -293,14 +499,260 @@ extensions to the library - star - lstar - bool ( â» ) ( â ) - arith ( ?^? ) ( â«¯? ) ( â«°? ) - list ( â ) ( ? @ ? ) ( |?| ) + stream ( ? @ ? ) + stream_eq ( ? â ? ) + stream_hdtl ( â? ) + stream_tls ( â*[?]? ) + +
+ + +
+ + +
+ + +
+ + +
+ + +
+ + +
+ + +
+ + +
+ + +
+ + +
+ + +
+ + +
+ + +
+ + +
+ + +
+ + +
+ + + + +
+ + +
+ + list ( â ) ( ? @ ? ) ( |?| ) list2 ( â ) ( {?,?} @ ? ) ( ? @@ ? ) ( |?| ) - stream ( ? @ ? ) ( ? â ? ) - stream_hdtl + +
+ + +
+ + +
+ + +
+ + +
+ + +
+ + +
+ + +
+ + +
+ + +
+ + +
+ + +
+ + +
+ + +
+ + +
+ + +
+ + +
+ + +
+ + +
+ + + + +
+ + +
+ + bool ( â» ) ( â ) + arith ( ?^? ) ( â«¯? ) ( â«°? ) ( ? â¨ ? ) ( ? â§ ? ) + +
+ + +
+ + +
+ + +
+ + +
+ + +
+ + +
+ + +
+ + +
+ + +
+ + +
+ + +
+ + +
+ + +
+ + +
+ + +
+ + +
+ + +
+ + +
+ + + + +
+ + +
+ + relations ( ? â ? ) + star + lstar + +
+ + +
+ + +
+ + +
+ + +
+ + +
+ + +
+ + +
+ + +
+ + +
+ + +
+ + +
+ + +
+ + +
+ + +
+ + +
+ + +
+ + +
+ generated logical decomposables @@ -322,6 +774,45 @@
+ +
+ + +
+ + +
+ + +
+ + +
+ + +
+ + +
+ + +
+ + +
+ + +
+ + +
+ + +
+ + +
+
@@ -350,6 +841,45 @@
+ +
+ + +
+ + +
+ + +
+ + +
+ + +
+ + +
+ + +
+ + +
+ + +
+ + +
+ + +
+ + +
+
@@ -358,7 +888,7 @@

- + $\lambda\delta rainbow rule$

@@ -383,6 +913,6 @@

-
Last update: Sat, 23 Jan 2016 00:45:18 +0100
+
Last update: Fri, 24 Nov 2017 21:00:01 +0100