Here is a numerical account of the specification's contents
and its timeline.
@@ -132,33 +132,51 @@
sizes |
files |
- 48 |
+ 86 |
characters |
- 66783 |
+ 109249 |
nodes |
- 134126 |
+ 217872 |
propositions |
theorems |
- 9 |
+ 30 |
lemmas |
- 298 |
+ 506 |
total |
- 307 |
+ 536 |
concepts |
declared |
- 47 |
+ 59 |
defined |
- 32 |
+ 55 |
total |
- 79 |
+ 114 |
Logical Structure of the Specification
+
Logical Structure of the Specification
This table reports the specification's components and their planes.
@@ -206,21 +224,123 @@
|
+
+
+ |
+
+
+ |
+
+
+ |
+
+
+ |
+
+
+ |
+
+
+ |
+
+
+ |
+
+
+ |
|
+
+ generic rt-transition counter |
+ |
+ rtc ( â©?,?,?,?⪠) ( ðð ) ( ðð ) ( ðð ) |
+ rtc_shift ( â? ) |
+ rtc_plus ( ? + ? ) |
+
+
+ |
+
+
+ |
+
+
+ |
+
+
+ |
+
+
+ |
+
+
+ |
+
+
+ |
+
+
+ |
+
+
+ |
+
+
+ |
+
+
+ |
+
+
+ |
+
+
+ |
+
multiple relocation |
|
- trace ( �⥠) |
- trace_at ( @�,?⦠⡠? ) |
- trace_after ( ? â ? â¡ ? ) |
- trace_isid ( ðâ¦?⦠) |
- trace_isun ( ðâ¦?⦠) |
- trace_sle ( ? â ? ) |
- trace_sor ( ? â ? â¡ ? ) |
- trace_snot ( â ? ) |
+ 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 ( ? â ? ) |
@@ -242,6 +362,30 @@
|
|
+
+
+ |
+
+
+ |
+
+
+ |
+
+
+ |
+
+
+ |
+
+
+ |
+
+
+ |
+
+
+ |
|
@@ -258,6 +402,30 @@
|
+
+
+ |
+
+
+ |
+
+
+ |
+
+
+ |
+
+
+ |
+
+
+ |
+
+
+ |
+
+
+ |
|
@@ -265,12 +433,196 @@
extensions to the library |
|
+ stream ( ? @ ? ) |
+ stream_eq ( ? â ? ) |
+ stream_hdtl ( â? ) |
+ stream_tls ( â*[?]? ) |
+
+
+ |
+
+
+ |
+
+
+ |
+
+
+ |
+
+
+ |
+
+
+ |
+
+
+ |
+
+
+ |
+
+
+ |
+
+
+ |
+
+
+ |
+
+
+ |
+
+
+
+
+ |
+
+
+ |
+ list ( â ) ( ? @ ? ) ( |?| ) |
+ list2 ( â ) ( {?,?} @ ? ) ( ? @@ ? ) ( |?| ) |
+
+
+ |
+
+
+ |
+
+
+ |
+
+
+ |
+
+
+ |
+
+
+ |
+
+
+ |
+
+
+ |
+
+
+ |
+
+
+ |
+
+
+ |
+
+
+ |
+
+
+ |
+
+
+ |
+
+
+
+
+ |
+
+
+ |
+ bool ( â» ) ( â ) |
+ arith ( ?^? ) ( ⫯? ) ( ⫰? ) ( ? ⨠? ) ( ? ⧠? ) |
+
+
+ |
+
+
+ |
+
+
+ |
+
+
+ |
+
+
+ |
+
+
+ |
+
+
+ |
+
+
+ |
+
+
+ |
+
+
+ |
+
+
+ |
+
+
+ |
+
+
+ |
+
+
+ |
+
+
+
+
+ |
+
+
+ |
star |
lstar |
- bool ( â» ) ( â ) |
- arith ( ?^? ) ( ⫯? ) ( ⫰? ) |
- list ( â ) ( ? @ ? ) ( |?| ) |
- list2 ( â ) ( {?,?} @ ? ) ( ? @@ ? ) ( |?| ) |
+
+
+ |
+
+
+ |
+
+
+ |
+
+
+ |
+
+
+ |
+
+
+ |
+
+
+ |
+
+
+ |
+
+
+ |
+
+
+ |
+
+
+ |
+
+
+ |
|
@@ -298,6 +650,30 @@
|
+
+
+ |
+
+
+ |
+
+
+ |
+
+
+ |
+
+
+ |
+
+
+ |
+
+
+ |
+
+
+ |
|
@@ -326,6 +702,30 @@
|
+
+
+ |
+
+
+ |
+
+
+ |
+
+
+ |
+
+
+ |
+
+
+ |
+
+
+ |
+
+
+ |
|
@@ -334,7 +734,7 @@
-
+
@@ -359,6 +759,6 @@
-
Last update: Fri, 30 Oct 2015 12:45:15 +0100
+
Last update: Sat, 21 May 2016 22:22:39 +0200