background for \lambda\delta version 2

Here is a numerical acount of the specification's contents +

+
+

+ + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + +

+ home +	+ news +	+ specification +	+ +	+ +	+ documentation +	+ implementation +	+ +
+ foreword +	+ milestones +	+ version 2 +	(background - core - applications)	+ +	+ version 2 +	+ helena +	+ Open Symbolic Notation (OSN) +
+ citations +	+ visibility +	+ version 1 +	(background - core)	(static HELM directory)	+ version 1 +	+ library +	(static LDDL directory)

Summary of the Specification $\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].

- + @@ -54,59 +130,80 @@ - - - - - - - + + + + + + + - + - + - + - - - - - - - + + + + + + +

category	objects	units
sizes	files	30	characters	68581	nodes	62380	sizes	characters (files)	145725 (104)	nodes (objects)	337452 (911)	intrinsic loss factor	2.3
propositions	theorems	2	42	lemmas	187	693	total	189	735
concepts	declared	40	defined	25	total	65	concepts	declared	66	defined	73	total	139

+ 2016 April 18. + Generic rt-transition counter (rtc). +

- 2013 November 27. - Natural numbers with infinity. + 2016 March 4. + Platform-independent multiple relocation (rtmap).

- 2011 August 10. + 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 $\lambda\delta butterfly$ +

This table reports the specification's components and their planes.

+ + + + + + + + + + + + + - - - - - - - - - - + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + - - + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + @@ -175,9 +818,50 @@ - - - + + + + + + + + + + + + + + @@ -203,13 +887,8 @@

component

plane

files

@@ -130,25 +227,571 @@

+
+

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_isrc ( ððâ¦?, ?â¦ )

rtc_shift ( â? )

rtc_max ( ? â¨ ? )

rtc_plus ( ? + ? )

+
+

multiple relocation

rtmap

rtmap_eq ( ? â ? )

rtmap_pushs ( â*[?]? )

rtmap_nexts ( â«¯*[?]? )

rtmap_tl ( â«±? )

rtmap_tls ( â«±*[?]? )

rtmap_isid ( ðâ¦?â¦ )

rtmap_id

rtmap_isdiv ( ðâ¦?â¦ )

rtmap_fcla ( ðâ¦?â¦ â¡ ? )

rtmap_isfin ( ðâ¦?â¦ )

rtmap_isuni ( ðâ¦?â¦ )

rtmap_uni ( ðâ´?âµ )

rtmap_sle ( ? â ? )

rtmap_sdj ( ? â¥ ? )

rtmap_sand ( ? â ? â¡ ? )

rtmap_sor ( ? â ? â¡ ? )

rtmap_at ( @â¦?,?â¦ â¡ ? )

rtmap_istot ( ðâ¦?â¦ )

rtmap_after ( ? â ? â¡ ? )

rtmap_coafter ( ? ~â ? â¡ ? )

+
+

nstream ( â? ) ( â«¯? )

nstream_eq

nstream_isid

nstream_id ( ðð )

nstream_sor

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

stream ( ? @ ? )

stream_eq ( ? â ? )

stream_hdtl ( â? )

stream_tls ( â*[?]? )

+
+

list ( â ) ( ? @ ? ) ( |?| )

list2 ( â ) ( {?,?} @ ? ) ( ? @@ ? ) ( |?| )

+
+

extensions to the library

arith.ma ( ?^? )

+
+

bool ( â» ) ( â )

arith ( ?^? ) ( â«¯? ) ( â«°? ) ( ? â¨ ? ) ( ? â§ ? )

+
+

relations ( ? â ? )

star

lstar

+
+

generated logical decomposables

xoa ( ââ ) ( â¨â¨ ) ( â§â§ )

xoa_props ( â¥ ) ( â¤ )

+
+

generated logical decomposables

xoa ( ââ ) ( â¨â¨ ) ( â§â§ )

xoa_props ( â¥ ) ( â¤ )

+
+

- -

Physical Structure of the Specification

The source files are grouped in directories, - one for each plane. -

+ $\lambda\delta rainbow rule$

@@ -234,6 +913,6 @@

Last update: Wed, 22 Oct 2014 20:00:29 +0200

- +

Last update: Fri, 24 Nov 2017 21:00:01 +0100