X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=helm%2Fwww%2Flambdadelta%2Fapps_2.html;h=9fc581eb9f9323556dc236ad97e45970e7392a11;hb=2aa295aa37f8fb274f7b640f7627078d9435cefa;hp=3686c50caa6969e6bd9d3d0009cdbb8607331b07;hpb=d3e1cb5ea229da5081fdd6fc3c5182e4bff1d563;p=helm.git diff --git a/helm/www/lambdadelta/apps_2.html b/helm/www/lambdadelta/apps_2.html index 3686c50ca..9fc581eb9 100644 --- a/helm/www/lambdadelta/apps_2.html +++ b/helm/www/lambdadelta/apps_2.html @@ -1,62 +1,196 @@ - + - - - - - - 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-02-11T23:55:23+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: Sun, 06 Jul 2014 20:28:30 +0200