![[lambdadelta home]](http://lambdadelta.info/images/crux_32.png "lambdadelta home")
+ Here is a numerical account of the specification's contents
and its timeline.
@@ -125,37 +132,61 @@
sizes
files
- 30
+ 86
characters
- 68581
+ 109249
nodes
- 62380
+ 217872
propositions
theorems
- 2
+ 30
lemmas
- 187
+ 506
total
- 189
+ 536
concepts
declared
- 40
+ 59
defined
- 25
+ 55
total
- 65
+ 114
+ -
+
- + 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).
-
@@ -164,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_shift ( â? )
+ rtc_plus ( ? + ? )
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+ multiple relocation
+ 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 ( ? â ? â¡ ? )
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+ 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 ( ?^? ) ( ⫯? ) ( ⫰? ) ( ? ⨠? ) ( ? ⧠? )
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
- extensions to the library
+
+
+
+
+
+
+ star
+ lstar
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+ generated logical decomposables
star
- lstar
- bool ( â» ) ( â )
- arith ( ?^? )
- list ( â ) ( ? @ ? ) ( {?,?} @ ? ) ( ? @@ ? ) ( |?| )
+ xoa ( ââ ) ( â¨â¨ ) ( â§â§ )
+ xoa_props ( ⥠) ( ⤠)
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
@@ -235,10 +679,35 @@
- generated logical decomposables
+ xoa ( ââ ) ( â¨â¨ ) ( â§â§ )
- xoa_props ( ⥠) ( ⤠)
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
@@ -265,7 +734,7 @@
@@ -290,6 +759,6 @@
-
+ Logical Structure of the Specification
This table reports the specification's components and their planes.
@@ -196,31 +227,444 @@
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
- ![[Spacer]](http://lambdadelta.info/images/rainbow.png "lambdadelta rainbow rule")
+
+
@@ -290,6 +759,6 @@
Last update: Thu, 15 Jan 2015 16:54:45 +0100
+ Last update: Sat, 21 May 2016 22:22:39 +0200