X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=helm%2Fwww%2Flambdadelta%2Fapps_2.html;h=ee0a068907d5d6931b1c67cd15b8585b944edf20;hb=f46a888221e68830773251aa134f3da13c5b9e3c;hp=b3301124aecbd6b3e16752e4a4c5b7aff98794ce;hpb=b2c1a95861424ba23e491e2b258f7413efbc1fba;p=helm.git diff --git a/helm/www/lambdadelta/apps_2.html b/helm/www/lambdadelta/apps_2.html index b3301124a..ee0a06890 100644 --- a/helm/www/lambdadelta/apps_2.html +++ b/helm/www/lambdadelta/apps_2.html @@ -6,8 +6,8 @@ - - applications of lambdadelta version 2 + + applications of \lambda\delta version 2 @@ -23,7 +23,7 @@
[Spacer]
-
Contents of the Specification
+
Contents of the Specification
This specification comprises a collection of checked applications of λδ version 2. In particular it contains the components below. @@ -43,62 +43,62 @@ -
Summary of the Specification
+
Summary of the Specification
Here is a numerical acount 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" + 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]. + pp. 53-78].
- - - + + - - - - - - - - - - - + + + + + + + - - - - - - - + + + + + + + - - - - - - - + + + + + + +
categoryobjects + categoryobjects
+
+
+
+
sizesfiles4 characters3922nodes3861sizesfiles4characters2567nodes3637
propositionstheorems2lemmas1total3propositionstheorems2lemmas1total3
conceptsdeclared3defined9total12conceptsdeclared3defined9total12
@@ -123,7 +123,7 @@ -
Logical Structure of the Specification
+
Logical Structure of the Specification
The source files are grouped in planes and components according to the following table. Each component contains its own notation file. @@ -134,26 +134,26 @@ - - - - + + + - - - - + + + + - - - - + + @@ -161,7 +161,7 @@
componentplanefiles + componentplanefiles
functionalreduction and type machinertmrtm_step ( ? ⇨ ? )functionalreduction and type machinertmrtm_step ( ? ⇨ ? )
+
relocationlift ( ↑[?,?] ? ) + relocationlift ( ↑[?,?] ? )
-
Physical Structure of the Specification
+
Physical Structure of the Specification
The source files are grouped in directories, one for each component.
@@ -191,6 +191,6 @@

-
Last update: Wed, 07 Aug 2013 23:40:05 +0200
+
Last update: Wed, 10 Sep 2014 14:46:05 +0200