![[lambdadelta home]](http://lambdadelta.info/images/crux_32.png "lambdadelta home")
+ Here is a numerical account of the specification's contents
and its timeline.
@@ -132,37 +132,61 @@
sizes
files
- 30
+ 92
characters
- 68581
+ 125262
nodes
- 62380
+ 265747
propositions
theorems
- 2
+ 33
lemmas
- 187
+ 588
total
- 189
+ 621
concepts
declared
- 40
+ 60
defined
- 25
+ 63
total
- 65
+ 123
+ -
+
- + 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. + Multiple relocation with lists of booleans. + +
- 2013 November 27. - Natural numbers with infinity. + Natural numbers with infinity (ynat).
-
@@ -171,7 +195,7 @@
Specification starts.
Logical Structure of the Specification ![[spacer]](http://lambdadelta.info/images/b4.png "lambdadelta butterfly")
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
- natural numbers with infinity
+ generic rt-transition counter
+ rtc ( â©?,?,?,?⪠) ( ðð ) ( ðð ) ( ðð )
+ rtc_isrc ( ððâ¦?, ?⦠)
+ rtc_shift ( â? )
+ rtc_plus ( ? + ? )
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+ multiple relocation
+ 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 ( ? â ? â¡ ? )
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+ natural numbers with infinity
+ ynat ( â )
+ ynat_pred ( â«°? )
+ ynat_succ ( ⫯? )
+ ynat_le ( ? ⤠? )
+ ynat_lt ( ? < ? )
+ ynat_plus ( ? + ? )
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+ extensions to the library
ynat ( â )
- ynat_pred ( â«°? )
- ynat_succ ( ⫯? )
- ynat_le ( ? ⤠? )
- ynat_lt ( ? < ? )
- ynat_minus ( ? - ? )
- ynat_plus ( ? + ? )
- ynat_max
- ynat_min
+ stream ( ? @ ? )
+ stream_eq ( ? â ? )
+ stream_hdtl ( â? )
+ stream_tls ( â*[?]? )
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+ list ( â ) ( ? @ ? ) ( |?| )
+ list2 ( â ) ( {?,?} @ ? ) ( ? @@ ? ) ( |?| )
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+ bool ( â» ) ( â )
+ arith ( ?^? ) ( ⫯? ) ( ⫰? ) ( ? ⨠? ) ( ? ⧠? )
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+ star
+ lstar
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
- extensions to the library
+ generated logical decomposables
star
- lstar
- bool ( â» ) ( â )
- arith ( ?^? )
- list ( â ) ( ? @ ? ) ( {?,?} @ ? ) ( ? @@ ? ) ( |?| )
+ xoa ( ââ ) ( â¨â¨ ) ( â§â§ )
+ xoa_props ( ⥠) ( ⤠)
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
@@ -242,10 +735,41 @@
- generated logical decomposables
+ xoa ( ââ ) ( â¨â¨ ) ( â§â§ )
- xoa_props ( ⥠) ( ⤠)
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
@@ -272,7 +796,7 @@
@@ -297,6 +821,6 @@
-
+ Logical Structure of the Specification
This table reports the specification's components and their planes.
@@ -203,31 +227,500 @@
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
- ![[Spacer]](http://lambdadelta.info/images/rainbow.png "lambdadelta rainbow rule")
+
+
@@ -297,6 +821,6 @@
Last update: Tue, 20 Jan 2015 18:39:00 +0100
+ Last update: Fri, 22 Jul 2016 19:34:08 +0200