Here is a numerical acount of the specification's contents
+
Here is a numerical account of the specification's contents
and its timeline.
@@ -132,37 +132,55 @@
| sizes |
files |
- 30 |
+ 79 |
characters |
- 68581 |
+ 96249 |
nodes |
- 62380 |
+ 206180 |
| propositions |
theorems |
- 2 |
+ 23 |
lemmas |
- 187 |
+ 495 |
total |
- 189 |
+ 518 |
| 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).
@@ -203,31 +221,398 @@
|
+
+
+ |
+
+
+ |
+
+
+ |
+
+
+ |
+
+
+ |
+
+
+ |
+
+
+ |
|
- | natural numbers with infinity |
+ natural numbers with infinity |
+ |
+ ynat ( â ) |
+ ynat_pred ( â«°? ) |
+ ynat_succ ( ⫯? ) |
+ ynat_le ( ? ⤠? ) |
+ ynat_lt ( ? < ? ) |
+ ynat_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 ( ? â ? â¡ ? ) |
+
+
+ |
+
+
+ |
+
+
+ |
+
+
+ |
+
+
+ |
+
+
+ |
+
+
+ |
+
+
+ |
+
+
+ |
+
+
+ |
+
+
+ |
+
+
+ |
+
+
+ | 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 ( ⥠) ( ⤠) |
+
+
+ |
+
+
+ |
+
+
+ |
+
+
+ |
+
+
+ |
+
+
+ |
+
+
+ |
+
+
+ |
+
+
+ |
+
+
+ |
|
@@ -242,10 +627,35 @@
- | generated logical decomposables |
+ |
|
- xoa ( ââ ) ( â¨â¨ ) ( â§â§ ) |
- xoa_props ( ⥠) ( ⤠) |
+
+
+ |
+
+
+ |
+
+
+ |
+
+
+ |
+
+
+ |
+
+
+ |
+
+
+ |
+
+
+ |
+
+
+ |
|
@@ -297,6 +707,6 @@
- Last update: Mon, 19 Jan 2015 23:52:51 +0100
+ Last update: Fri, 01 Apr 2016 23:30:52 +0200
![[spacer]](http://lambdadelta.info/images/b4.png "lambdadelta butterfly")