X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=helm%2Fwww%2Flambdadelta%2Fapps_2.html;h=0d7ed25e3c755e4f9bdb5dc49760fdd1c5561981;hb=f8bf3abd773864388fef5efe599ac77f292a6b9d;hp=1e927ff41c687c33c3f2a6c84e3d66e4d63b783f;hpb=314cfdb2d8d96e61ac0a133b043cf7840e8835ab;p=helm.git diff --git a/helm/www/lambdadelta/apps_2.html b/helm/www/lambdadelta/apps_2.html index 1e927ff41..0d7ed25e3 100644 --- a/helm/www/lambdadelta/apps_2.html +++ b/helm/www/lambdadelta/apps_2.html @@ -1,62 +1,200 @@ - + - - - - - - applications of lambdadelta version 2 - - - - + + + + + + applications of \lambda\delta version 2 + + + + -
[lambdadelta home]
cic:/matita/lambdadelta/apps_2/ (applications of λδ version 2)
[Spacer]
-
Contents of the Specification
-
This specification comprises a collection of checked + +
+ + [lambdadelta home] + +
+
cic:/matita/lambdadelta/apps_2/ (applications of λδ version 2)
+
+ [Spacer] +
+ +
Contents of the Specification
+
This specification comprises a collection of checked applications of λδ version 2. - In particular it contains the components below. + In particular it contains the components below.
- + + +
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" + Journal of Automated Reasoning 44(1-2), Springer (February 2010), + pp. 53-78].
-
categoryobjects




sizesfiles5characters5613nodes10024
propositionstheorems4lemmas1total5
conceptsdeclared3defined10total13
- -
Logical Structure of the Specification
-
The source files are grouped in planes and components + +
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. - The notation for the relations or functions introduced in each file - is shown in parentheses (? are placeholders). + The notation for the relations or functions introduced in each file + is shown in parentheses (? are placeholders).
-
componentplanefiles
MLTT1genv_primitivejudgement
functionalreduction and type machinertmrtm_step ( ? ⇨ ? )

unfoldlift ( ↑[?,?] ? )subst ( [?←?] ? )
+
+ + + + + + + + + + + + + + + + + + + + + +
componentplanefiles +
+
functionalreduction and type machinertmrtm_step ( ? ⇨ ? )
+
+ 		relocationlift ( ↑[?,?] ? ) +
+
+
-
Physical Structure of the Specification
-
The source files are grouped in directories, + +
Physical Structure of the Specification
+
The source files are grouped in directories, one for each component.
-
[Spacer]

[Valid XHTML 1.1][Valid CSS level 2][Generated from XML via XSL][PNG used here][Viewable with any browser]

Last update: 2013-03-03T19:53:30+01:00
+
+ [Spacer] +
+
+
+
+
+ + [Valid XHTML 1.1] + + + [Valid CSS level 2] + + + [Generated from XML via XSL] + + + [PNG used here] + + + [Viewable with any browser] + +
+
+
+
+
Last update: Fri, 04 Jul 2014 19:56:33 +0200