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,37 +132,55 @@ sizes files - 30 + 79 characters - 46649 + 96548 nodes - 62380 + 207514 propositions theorems - 2 + 23 lemmas - 187 + 497 total - 189 + 520 concepts declared - 40 + 53 defined - 25 + 50 total - 65 + 103

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

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

+ 2015 October 11. + Multiple relocation with lists of booleans. +

2013 November 27. - Natural numbers with infinity. + Natural numbers with infinity (ynat).

@@ -171,7 +189,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.

@@ -203,31 +221,350 @@
+ +
+ + +
+ + +
+ + +
+ + +
+ + +
+ + +
+
- natural numbers with infinity + natural numbers with infinity + + ynat ( â ) + ynat_pred ( â«°? ) + ynat_succ ( â«¯? ) + ynat_le ( ? â¤ ? ) + ynat_lt ( ? < ? ) + ynat_plus ( ? + ? ) + +
+ + +
+ + +
+ + +
+ + +
+ + +
+ + +
+ + +
+ + +
+ + +
+ + + + multiple relocation - ynat ( â ) - ynat_pred ( â«°? ) - ynat_succ ( â«¯? ) - ynat_le ( ? â¤ ? ) - ynat_lt ( ? < ? ) - ynat_minus ( ? - ? ) - ynat_plus ( ? + ? ) - ynat_max - ynat_min + 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 ( ? â ? â¡ ? ) + +
+ + +
+ + +
+ + +
+ + +
+ + +
+ + +
+ + +
+ + +
+ + +
+ + +
+ + +
+ extensions to the library + stream ( ? @ ? ) + stream_eq ( ? â ? ) + stream_hdtl ( â? ) + stream_tls ( â*[?]? ) + +
+ + +
+ + +
+ + +
+ + +
+ + +
+ + +
+ + +
+ + +
+ + +
+ + +
+ + +
+ + + + +
+ + +
+ + list ( â ) ( ? @ ? ) ( |?| ) + list2 ( â ) ( {?,?} @ ? ) ( ? @@ ? ) ( |?| ) + +
+ + +
+ + +
+ + +
+ + +
+ + +
+ + +
+ + +
+ + +
+ + +
+ + +
+ + +
+ + +
+ + +
+ + + + +
+ + +
+ + bool ( â» ) ( â ) + arith ( ?^? ) ( â«¯? ) ( â«°? ) ( ? â¨ ? ) ( ? â§ ? ) + +
+ + +
+ + +
+ + +
+ + +
+ + +
+ + +
+ + +
+ + +
+ + +
+ + +
+ + +
+ + +
+ + +
+ + + + +
+ + +
+ star lstar - bool ( â» ) ( â ) - arith ( ?^? ) - list ( â ) ( ? @ ? ) ( {?,?} @ ? ) ( ? @@ ? ) ( |?| ) + +
+ + +
+ + +
+ + +
+ + +
+ + +
+ + +
+ + +
+ + +
+ + +
+
@@ -264,6 +601,27 @@
+ +
+ + +
+ + +
+ + +
+ + +
+ + +
+ + +
+
@@ -295,6 +653,27 @@
+ +
+ + +
+ + +
+ + +
+ + +
+ + +
+ + +
+
@@ -303,7 +682,7 @@

+ $\lambda\delta rainbow rule$

@@ -328,6 +707,6 @@

Last update: Wed, 21 Jan 2015 17:13:08 +0100

Last update: Fri, 08 Apr 2016 22:51:19 +0200