X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=helm%2Fwww%2Flambdadelta%2Fground_2.html;h=12045bc1ae7eea09b8e15ffc539423c7876a848d;hb=12fd764a3ab9df02fcea5403bdc50387bb648887;hp=6c4c190f77c94bbdea944c6ea8b7b7a56b06ecf5;hpb=a5d21c8955339a48f28c22e0c3cfe43363d39188;p=helm.git diff --git a/helm/www/lambdadelta/ground_2.html b/helm/www/lambdadelta/ground_2.html index 6c4c190f7..12045bc1a 100644 --- a/helm/www/lambdadelta/ground_2.html +++ b/helm/www/lambdadelta/ground_2.html @@ -6,8 +6,8 @@ - - lambdadelta version 2 + + background for \lambda\delta version 2 @@ -23,7 +23,7 @@
[Spacer]
-
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" @@ -35,50 +35,50 @@ - - - + + - - - - - - - - - - - + + + + + + + - - - - - - - + + + + + + + - - - - - - - + + + + + + +
categoryobjects + categoryobjects
+
+
+
+
sizesfiles26 characters65234nodes44240sizesfiles30characters46649nodes62380
propositionstheorems2lemmas115total117propositionstheorems2lemmas187total189
conceptsdeclared40defined24total64conceptsdeclared40defined25total65
@@ -96,7 +96,7 @@ -
Logical Structure of the Specification
+
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. @@ -107,76 +107,96 @@ - - - + + - - - - - + + - - - - - - - - + + + + + + + + + + - - - + + + - - - - - + - - - - + + + + + - - - - @@ -184,7 +204,7 @@
planefiles + planefiles
+
+
+
+
+ +
+
+
+

natural numbers with infinityynat ( ∞ )ynat_pred ( ⫰? )ynat_succ ( ⫯? )ynat_le ( ?≤? )ynat_lt ( ?<? )ynat_minus ( ? - ? )ynat_plus ( ? + ? )natural numbers with infinityynat ( ∞ )ynat_pred ( ⫰? )ynat_succ ( ⫯? )ynat_le ( ?≤? )ynat_lt ( ?<? )ynat_minus ( ? - ? )ynat_plus ( ? + ? )ynat_maxynat_min
extensions to the libraryarith.ma ( ?^? ) + extensions to the libraryarith.ma ( ?^? ) +
+

+
+
+
+
+ +
+

generated logical decomposablesxoa ( ∃∃ ) ( ∨∨ ) ( ∧∧ )xoa_props ( ⊥ ) ( ⊤ ) + generated logical decomposablesxoa ( ∃∃ ) ( ∨∨ ) ( ∧∧ )xoa_props ( ⊥ ) ( ⊤ ) +
+
+
+

+
+
+
+
-
Physical Structure of the Specification
+
Physical Structure of the Specification
The source files are grouped in directories, one for each plane.
@@ -214,6 +234,6 @@

-
Last update: Wed, 04 Dec 2013 16:42:13 +0100
+
Last update: Tue, 30 Sep 2014 16:37:52 +0200