![[lambdadelta home]](http://lambdadelta.info/images/crux_32.png "lambdadelta home")
+
+
+
+ +
+
+
+
+
+ | + home + | ++ news + | ++ specification + | +
+ + |
+
+ + |
+ + documentation + | ++ implementation + | +
+ + |
+
| + foreword + | ++ milestones + | ++ version 2 + | +(background - core - applications) | +
+ + |
+ + version 2 + | ++ helena + | +
+ + |
+
| + citations + | ++ visibility + | ++ version 1 + | +(background - core) | +(static HELM directory) | ++ version 1 + | ++ library + | +(static LDDL directory) | +
Summary of the Specification ![[spacer]](http://lambdadelta.info/images/b4.png "\lambda\delta butterfly")
+
+
+ Here is a numerical account of the specification's contents
and its timeline.
- Nodes are counted according to the "intrinsinc complexity measure"
- [F. Guidi: "Procedural Representation of CIC Proof Terms"
- Journal of Automated Reasoning 44(1-2), Springer (February 2010),
- pp. 53-78].
-
+
-
| category | -objects | -+ | category | +objects | +
|
- + |
|
- + |
|
- + |
|
- + |
|
| sizes | -files | -31 | -characters | -71828 | -nodes | -56616 | +sizes | +files | +86 | +characters | +109249 | +nodes | +217872 |
| propositions | -theorems | -2 | -lemmas | -168 | -total | -170 | +propositions | +theorems | +30 | +lemmas | +506 | +total | +536 |
| concepts | -declared | -40 | -defined | -24 | -total | -64 | +concepts | +declared | +59 | +defined | +55 | +total | +114 |
-
+
- - 2013 November 27. - Natural numbers with infinity. + 2016 April 18. + Generic rt-transition counter (rtc).
- - 2011 August 10. + 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 (ynat). + +
- + 2011 August 10. Specification starts.
-
+
-
+
-
+
-
+
-
+
Logical Structure of the Specification
- The source files are grouped in planes
- according to the following table.
- Notation files covering the whole specification are provided.
- The notation for the relations or functions introduced in each file
- is shown in parentheses (? are placeholders).
+
Logical Structure of the Specification
+
+
+ This table reports the specification's components and their planes.
-
+
-
-
| plane | -files | -+ | component | +plane | +files | +
+ + |
+
|
- + |
|
- + |
|
- + |
|
- + |
|
- + |
|
- + |
|
- + |
+ + |
+
+ + |
+
+ + |
+
+ + |
+
+ + |
+
+ + |
+
|
| natural numbers with infinity | -ynat ( â ) | -ynat_pred ( â«°? ) | -ynat_succ ( ⫯? ) | -ynat_le ( ?â¤? ) | -ynat_lt ( ?<? ) | -ynat_minus ( ? - ? ) | -ynat_plus ( ? + ? ) | -ynat_max | -ynat_min | +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 ( ? â ? â¡ ? ) | +
+ + |
+
+ + |
+
+ + |
+
+ + |
+
+ + |
+
+ + |
+
+ + |
+
+ + |
+
+ + |
+
+ + |
+
+ + |
+
+ + |
||||||||||
| extensions to the library | -arith.ma ( ?^? ) | -+ | natural numbers with infinity | ++ | ynat ( â ) | +ynat_pred ( â«°? ) | +ynat_succ ( ⫯? ) | +ynat_le ( ? ⤠? ) | +ynat_lt ( ? < ? ) | +ynat_plus ( ? + ? ) | +
+ + |
+
|
- + |
|
- + |
|
- + |
|
- + |
|
- + |
|
- + |
|
- + |
+ + |
+
|
| generated logical decomposables | -xoa ( ââ ) ( â¨â¨ ) ( â§â§ ) | -xoa_props ( ⥠) ( ⤠) | -+ | extensions to the library | ++ | stream ( ? @ ? ) | +stream_eq ( ? â ? ) | +stream_hdtl ( â? ) | +stream_tls ( â*[?]? ) | +
|
- + |
|
- + |
|
- + |
|
- + |
|
- + |
|
- + |
+ + |
+
+ + |
+
+ + |
+
+ + |
+
+ + |
+
+ + |
+
|
+ + |
+
+ + |
+ list ( â ) ( ? @ ? ) ( |?| ) | +list2 ( â ) ( {?,?} @ ? ) ( ? @@ ? ) ( |?| ) | +
+ + |
+
+ + |
+
+ + |
+
+ + |
+
+ + |
+
+ + |
+
+ + |
+
+ + |
+
+ + |
+
+ + |
+
+ + |
+
+ + |
+
+ + |
+
+ + |
+ ||||||||||
|
+ + |
+
+ + |
+ bool ( â» ) ( â ) | +arith ( ?^? ) ( ⫯? ) ( â«°? ) ( ? ⨠? ) ( ? ⧠? ) | +
+ + |
+
+ + |
+
+ + |
+
+ + |
+
+ + |
+
+ + |
+
+ + |
+
+ + |
+
+ + |
+
+ + |
+
+ + |
+
+ + |
+
+ + |
+
+ + |
+ ||||||||||
|
+ + |
+
+ + |
+ star | +lstar | +
+ + |
+
+ + |
+
+ + |
+
+ + |
+
+ + |
+
+ + |
+
+ + |
+
+ + |
+
+ + |
+
+ + |
+
+ + |
+
+ + |
+
+ + |
+
+ + |
+ ||||||||||
| generated logical decomposables | ++ | xoa ( ââ ) ( â¨â¨ ) ( â§â§ ) | +xoa_props ( ⥠) ( ⤠) | +
+ + |
+
+ + |
+
+ + |
+
+ + |
+
+ + |
+
+ + |
+
+ + |
+
+ + |
+
+ + |
+
+ + |
+
+ + |
+
+ + |
+
+ + |
+
+ + |
+ ||||||||||
| + | + |
+ + |
+
+ + |
+
+ + |
+
+ + |
+
+ + |
+
+ + |
+
+ + |
+
+ + |
+
+ + |
+
+ + |
+
+ + |
+
+ + |
+
+ + |
+
+ + |
+
+ + |
+
|
Physical Structure of the Specification
- The source files are grouped in directories,
- one for each plane.
-
-
- ![[Spacer]](http://lambdadelta.info/images/rainbow.png "lambdadelta rainbow rule")
+
@@ -234,6 +759,6 @@
-
+
+
@@ -234,6 +759,6 @@
Last update: Tue, 11 Feb 2014 22:11:38 +0100
-
+ Last update: Sat, 21 May 2016 22:22:39 +0200
+