background for \lambda\delta version 2

X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=helm%2Fwww%2Flambdadelta%2Fground_2.html;h=9fc459b3337e1abf5ce98f6255d408d8383de3eb;hb=a145b5df4a86b3d5f8516a9c1cb76a62f6327151;hp=e6f30399514062194001c94244ad5519034f1085;hpb=c0d87c3cdf879f61aa53e91f43580e9815ae7190;p=helm.git diff --git a/helm/www/lambdadelta/ground_2.html b/helm/www/lambdadelta/ground_2.html index e6f303995..9fc459b33 100644 --- a/helm/www/lambdadelta/ground_2.html +++ b/helm/www/lambdadelta/ground_2.html @@ -6,8 +6,8 @@ - - background for \lambda\delta version 2 + + \lambda\delta home page @@ -16,203 +16,725 @@

[lambdadelta home]

+ $[\lambda\delta home]$

cic:/matita/lambdadelta/ground_2/ (background for Î»Î´ version 2)

-

+ $\lambda\delta rainbow rule$

Summary of the Specification

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 +	+ +
+ 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].

- - - + + - - - - - - - - - - - + + + + + + + - - - - - - - + + + + + + + - - - - - - - + + + + + + +

- 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 $\lambda\delta butterfly$ +

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

- - - + + + + - - - - - - - + + + + + + - - - - - - - - - - + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + - - - + + + + + + + + - - - - - - - + - - - - + + + + + - - - - - - + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + +

natural numbers with infinity

ynat_pred ( â«°? )

ynat_succ ( â«¯? )

ynat_le ( ?â¤? )

ynat_lt ( ?<? )

ynat_minus ( ? - ? )

ynat_plus ( ? + ? )

generic rt-transition counter

rtc ( â©?,?,?,?âª ) ( ðð ) ( ðð ) ( ðð )

rtc_shift ( â? )

rtc_plus ( ? + ? )

multiple relocation

rtmap_eq ( ? â ? )

rtmap_tl ( â«±? )

rtmap_tls ( â«±*[?]? )

rtmap_isid ( ðâ¦?â¦ )

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

rtmap_isfin ( ðâ¦?â¦ )

rtmap_isuni ( ðâ¦?â¦ )

rtmap_uni ( ðâ´?âµ )

rtmap_sle ( ? â ? )

rtmap_sand ( ? â ? â¡ ? )

rtmap_sor ( ? â ? â¡ ? )

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

rtmap_istot ( ðâ¦?â¦ )

rtmap_after ( ? â ? â¡ ? )

nstream ( â? ) ( â«¯? )

nstream_id ( ðð )

nstream_istot ( ?@â´?âµ )

nstream_after ( ? â ? )

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

mr2_plus ( ? + ? )

mr2_minus ( ? â ? â¡ ? )

extensions to the library

arith.ma ( ?^? )

natural numbers with infinity

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 ( ?^? ) ( â«¯? ) ( â«°? ) ( ? â¨ ? ) ( ? â§ ? )

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$

@@ -237,6 +759,6 @@

Last update: Sun, 06 Jul 2014 16:29:26 +0200

Last update: Thu, 19 May 2016 12:17:40 +0200