X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;ds=sidebyside;f=helm%2Fwww%2Flambdadelta%2Fground_2.html;h=125f3385ef2da54cbc8eaea70c48aca95d6fd258;hb=bb1a03359dfaea6031592d28b9bfb15d797c44e5;hp=10b1cdd58370a8bf0a4f628bd6cf7bed40c2782f;hpb=4ce3d9ff25dab34412495bf3dce9484e7d48efa5;p=helm.git diff --git a/helm/www/lambdadelta/ground_2.html b/helm/www/lambdadelta/ground_2.html index 10b1cdd58..125f3385e 100644 --- a/helm/www/lambdadelta/ground_2.html +++ b/helm/www/lambdadelta/ground_2.html @@ -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
+
+
+
+
sizesfiles29 characters72188nodes57742sizesfiles31characters46730nodes62380
propositionstheorems2lemmas171total173propositionstheorems2lemmas187total189
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,96 +107,96 @@ - - - + + - - - - - - - - - - - - - - - - - + + + + + + + + + + - - - + + - - - - - - - - - - - + + + - - - - - - @@ -204,7 +204,7 @@
planefiles + planefiles
+
+
+
+
+
+
+
natural numbers with infinityynat ( ∞ )ynat_pred ( ⫰? )ynat_succ ( ⫯? )ynat_le ( ?≤? )ynat_lt ( ?<? )ynat_minus ( ? - ? )ynat_plus ( ? + ? )ynat_maxynat_minnatural 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.
@@ -234,6 +234,6 @@

-
Last update: Tue, 04 Mar 2014 00:00:09 +0100
+
Last update: Wed, 10 Sep 2014 21:47:00 +0200