- update in basic_2 and ground_2

- uodated web site

diff --git a/helm/www/lambdadelta/BTM.html b/helm/www/lambdadelta/BTM.html
index 41f76628565ef2ce917a0976e0fb162e8c1772e6..19f42b340973fcb5614c7e04bf350e597d8901f7 100644 (file)
--- a/helm/www/lambdadelta/BTM.html
+++ b/helm/www/lambdadelta/BTM.html
@@ -223,6 +223,6 @@
     <div xmlns:ld="http://lambdadelta.info/" class="spacer">
       <br />
     </div>
-    <div xmlns:ld="http://lambdadelta.info/" class="spacer">Last update: Sun, 20 Jul 2014 16:13:31 +0200</div>
+    <div xmlns:ld="http://lambdadelta.info/" class="spacer">Last update: Tue, 05 Aug 2014 23:07:40 +0200</div>
 </body>
 </html>

diff --git a/helm/www/lambdadelta/apps_2.html b/helm/www/lambdadelta/apps_2.html
index 32d81ab2b5746ed62a90669051bf2a70088f3b6b..5305296246f7af7976c31018e7e962a88ea246fb 100644 (file)
--- a/helm/www/lambdadelta/apps_2.html
+++ b/helm/www/lambdadelta/apps_2.html
@@ -191,6 +191,6 @@
     <div xmlns:ld="http://lambdadelta.info/" class="spacer">
       <br />
     </div>
-    <div xmlns:ld="http://lambdadelta.info/" class="spacer">Last update: Sun, 20 Jul 2014 16:13:31 +0200</div>
+    <div xmlns:ld="http://lambdadelta.info/" class="spacer">Last update: Tue, 05 Aug 2014 23:07:40 +0200</div>
 </body>
 </html>

diff --git a/helm/www/lambdadelta/basic_2.html b/helm/www/lambdadelta/basic_2.html
index c8959b5cd2d32afb4949119e858425b1c3f4e9de..7b6bf13cff9c472e442aaf8daf16ad2a60656d38 100644 (file)
--- a/helm/www/lambdadelta/basic_2.html
+++ b/helm/www/lambdadelta/basic_2.html
@@ -58,29 +58,29 @@
           <tr>
             <td class="snns component cyan">sizes</td>
             <td class="snns plane cyan">files</td>
-            <td class="snnn number cyan">362</td>
+            <td class="snnn number cyan">367</td>
             <td class="snns plane cyan">characters</td>
-            <td class="snnn number cyan">431129</td>
+            <td class="snnn number cyan">431873</td>
             <td class="snns plane cyan">nodes</td>
-            <td class="ssnn number cyan">1829245</td>
+            <td class="ssnn number cyan">1830977</td>
           </tr>
           <tr>
             <td class="snns component green">propositions</td>
             <td class="snns plane green">theorems</td>
-            <td class="snnn number green">123</td>
+            <td class="snnn number green">128</td>
             <td class="snns plane green">lemmas</td>
-            <td class="snnn number green">1300</td>
+            <td class="snnn number green">1302</td>
             <td class="snns plane green">total</td>
-            <td class="ssnn number green">1423</td>
+            <td class="ssnn number green">1430</td>
           </tr>
           <tr>
             <td class="snss component yellow">concepts</td>
             <td class="snss plane yellow">declared</td>
-            <td class="snsn number yellow">54</td>
+            <td class="snsn number yellow">55</td>
             <td class="snss plane yellow">defined</td>
-            <td class="snsn number yellow">84</td>
+            <td class="snsn number yellow">82</td>
             <td class="snss plane yellow">total</td>
-            <td class="sssn number yellow">138</td>
+            <td class="sssn number yellow">137</td>
           </tr>
         </tbody>
       </table>
@@ -277,8 +277,24 @@
               <br />
             </td>
             <td class="snns plane prune">stratified native validity</td>
+            <td class="snns file prune">hsnv ( ⦃?,?⦄ ⊢ ? ¡[?,?,?] )</td>
+            <td class="snnn file prune">hsnv_aaa</td>
+            <td class="snnn file prune">
+              <br />
+            </td>
+            <td class="ssnn file prune">
+              <br />
+            </td>
+          </tr>
+          <tr>
+            <td class="nnns component prune">
+              <br />
+            </td>
+            <td class="nnns plane prune">
+              <br />
+            </td>
             <td class="snns file prune">snv ( ⦃?,?⦄ ⊢ ? ¡[?,?] )</td>
-            <td class="snnn file prune">snv_lift snv_aaa snv_da_lpr snv_lstas snv_lstas_lpr snv_lpr snv_cpcs snv_preserve</td>
+            <td class="snnn file prune">snv_lift snv_aaa snv_da_lpr snv_lstas snv_lstas_lpr snv_lpr snv_cpes snv_preserve</td>
             <td class="snnn file prune">
               <br />
             </td>
@@ -289,8 +305,8 @@
           <tr>
             <td class="snns component blue">equivalence</td>
             <td class="snns plane blue">decomposed extended equivalence</td>
-            <td class="snns file blue">cpes ( ⦃?,?⦄ ⊢ ? •*⬌*[?,?] ? )</td>
-            <td class="snnn file blue">cpes_cpds</td>
+            <td class="snns file blue">cpes ( ⦃?,?⦄ ⊢ ? •*⬌*[?,?,?,?] ? )</td>
+            <td class="snnn file blue">cpes_aaa cpes_cpcs cpes_cpes</td>
             <td class="snnn file blue">
               <br />
             </td>
@@ -485,7 +501,7 @@
               <br />
             </td>
             <td class="snns plane cyan">decomposed extended computation</td>
-            <td class="snns file cyan">cpds ( ⦃?,?⦄ ⊢ ? •*➡*[?,?] ? )</td>
+            <td class="snns file cyan">cpds ( ⦃?,?⦄ ⊢ ? •*➡*[?,?,?] ? )</td>
             <td class="snnn file cyan">cpds_lift cpds_aaa cpds_cpds</td>
             <td class="snnn file cyan">
               <br />
@@ -1300,6 +1316,6 @@
     <div xmlns:ld="http://lambdadelta.info/" class="spacer">
       <br />
     </div>
-    <div xmlns:ld="http://lambdadelta.info/" class="spacer">Last update: Sun, 20 Jul 2014 16:13:31 +0200</div>
+    <div xmlns:ld="http://lambdadelta.info/" class="spacer">Last update: Tue, 05 Aug 2014 23:07:40 +0200</div>
 </body>
 </html>

diff --git a/helm/www/lambdadelta/documentation.html b/helm/www/lambdadelta/documentation.html
index 7a90b1ba560d016c9fe5d019da1775d48d04e8d3..bc53a2b274a9dd7e53c951ddd9ddb187aa1ae427 100644 (file)
--- a/helm/www/lambdadelta/documentation.html
+++ b/helm/www/lambdadelta/documentation.html
@@ -161,7 +161,7 @@
             <td class="snns top" id="ldV2">
               <span class="date">V2.</span>
             </td>
-            <td class="ssnn top">F. Guidi: <a href="http://lambdadelta.info/version_2.html">lambdadelta_2</a> (revised <span class="date">2014-07</span>). Formal specification for the proof assistant Matita 0.99.2 (scripts). <a href="http://lambdadelta.info/documentation.html#bibtex">BibTeX entry</a>.</td>
+            <td class="ssnn top">F. Guidi: <a href="http://lambdadelta.info/version_2.html">lambdadelta_2</a> (revised <span class="date">2014-08</span>). Formal specification for the proof assistant Matita 0.99.2 (scripts). <a href="http://lambdadelta.info/documentation.html#bibtex">BibTeX entry</a>.</td>
           </tr>
           <tr>
             <td class="nnss top" />
@@ -285,6 +285,18 @@
             </td>
             <td class="ssnn top">F. Guidi: <a href="http://lambdadelta.info/download/ld_talk_1s.pdf">Lambda Tipi sul Lambda Calcolo con Abbreviazioni: una Specifica Certificata</a> (<span class="date">2005-12</span>). Presentation at University of Bologna (slides <span class="date">in Italian</span>).</td>
           </tr>
+          <tr>
+            <td class="nnns top" />
+            <td class="nsnn top">
+              <br />
+            </td>
+          </tr>
+          <tr>
+            <td class="snns top" id="ldV1">
+              <span class="date">V1.</span>
+            </td>
+            <td class="ssnn top">F. Guidi: <a href="http://lambdadelta.info/version_1.html">lambdadelta_1</a> (revised <span class="date">2012-10</span>). Formal specification for the proof assistant Coq 7.3.1 (scripts). <a href="http://lambdadelta.info/documentation.html#bibtex">BibTeX entry</a>.</td>
+          </tr>
           <tr>
             <td class="nnss top" />
             <td class="nssn top">
@@ -321,6 +333,6 @@
     <div xmlns:ld="http://lambdadelta.info/" class="spacer">
       <br />
     </div>
-    <div xmlns:ld="http://lambdadelta.info/" class="spacer">Last update: Sun, 20 Jul 2014 16:55:23 +0200</div>
+    <div xmlns:ld="http://lambdadelta.info/" class="spacer">Last update: Tue, 05 Aug 2014 23:07:40 +0200</div>
 </body>
 </html>

diff --git a/helm/www/lambdadelta/download/lambdadelta_2.tar.gz b/helm/www/lambdadelta/download/lambdadelta_2.tar.gz
index 6dc4aa81c2f4c4789e244b21a2a4c944023d2ed1..9c43092a4e9ed025e5c4bd7e945c95d91244778f 100644 (file)
Binary files a/helm/www/lambdadelta/download/lambdadelta_2.tar.gz and b/helm/www/lambdadelta/download/lambdadelta_2.tar.gz differ

diff --git a/helm/www/lambdadelta/ground_2.html b/helm/www/lambdadelta/ground_2.html
index 9b08ac7df1cc0e405c4e586ea3b660bc22c3929e..b1d1dc18bf63fee70609e01c9008a4d67ec5924b 100644 (file)
--- a/helm/www/lambdadelta/ground_2.html
+++ b/helm/www/lambdadelta/ground_2.html
@@ -56,20 +56,20 @@
           <tr>
             <td class="snns component cyan">sizes</td>
             <td class="snns plane cyan">files</td>
-            <td class="snnn number cyan">29</td>
+            <td class="snnn number cyan">31</td>
             <td class="snns plane cyan">characters</td>
-            <td class="snnn number cyan">46886</td>
+            <td class="snnn number cyan">46619</td>
             <td class="snns plane cyan">nodes</td>
-            <td class="ssnn number cyan">61467</td>
+            <td class="ssnn number cyan">61911</td>
           </tr>
           <tr>
             <td class="snns component green">propositions</td>
             <td class="snns plane green">theorems</td>
             <td class="snnn number green">2</td>
             <td class="snns plane green">lemmas</td>
-            <td class="snnn number green">183</td>
+            <td class="snnn number green">185</td>
             <td class="snns plane green">total</td>
-            <td class="ssnn number green">185</td>
+            <td class="ssnn number green">187</td>
           </tr>
           <tr>
             <td class="snss component yellow">concepts</td>
@@ -234,6 +234,6 @@
     <div xmlns:ld="http://lambdadelta.info/" class="spacer">
       <br />
     </div>
-    <div xmlns:ld="http://lambdadelta.info/" class="spacer">Last update: Sun, 20 Jul 2014 16:13:31 +0200</div>
+    <div xmlns:ld="http://lambdadelta.info/" class="spacer">Last update: Tue, 05 Aug 2014 23:07:40 +0200</div>
 </body>
 </html>

diff --git a/helm/www/lambdadelta/implementation.html b/helm/www/lambdadelta/implementation.html
index 71b5724c5eccc331ff9369069e1e58b396c99f8d..8eacf793043ca51af839ac6d8e0b6e3b55c41090 100644 (file)
--- a/helm/www/lambdadelta/implementation.html
+++ b/helm/www/lambdadelta/implementation.html
@@ -263,6 +263,6 @@
     <div xmlns:ld="http://lambdadelta.info/" class="spacer">
       <br />
     </div>
-    <div xmlns:ld="http://lambdadelta.info/" class="spacer">Last update: Sun, 20 Jul 2014 16:55:23 +0200</div>
+    <div xmlns:ld="http://lambdadelta.info/" class="spacer">Last update: Tue, 05 Aug 2014 23:07:40 +0200</div>
 </body>
 </html>

diff --git a/helm/www/lambdadelta/index.html b/helm/www/lambdadelta/index.html
index 289ed627e472f9fbe5198fbc64aeaeb18faf1b55..9bd1b957e90e6fecdb140b09cec47de2be87ec58 100644 (file)
--- a/helm/www/lambdadelta/index.html
+++ b/helm/www/lambdadelta/index.html
@@ -135,6 +135,6 @@
     <div xmlns:ld="http://lambdadelta.info/" class="spacer">
       <br />
     </div>
-    <div xmlns:ld="http://lambdadelta.info/" class="spacer">Last update: Sun, 20 Jul 2014 16:55:23 +0200</div>
+    <div xmlns:ld="http://lambdadelta.info/" class="spacer">Last update: Tue, 05 Aug 2014 23:07:40 +0200</div>
 </body>
 </html>

diff --git a/helm/www/lambdadelta/news.html b/helm/www/lambdadelta/news.html
index 0f5011f0637ba5955ee5de6fac7fbad25e60135d..bd9bdabf79d5e340a01770470de9869f6ed76aaf 100644 (file)
--- a/helm/www/lambdadelta/news.html
+++ b/helm/www/lambdadelta/news.html
@@ -303,6 +303,6 @@
     <div xmlns:ld="http://lambdadelta.info/" class="spacer">
       <br />
     </div>
-    <div xmlns:ld="http://lambdadelta.info/" class="spacer">Last update: Sun, 20 Jul 2014 16:55:23 +0200</div>
+    <div xmlns:ld="http://lambdadelta.info/" class="spacer">Last update: Tue, 05 Aug 2014 23:07:40 +0200</div>
 </body>
 </html>

diff --git a/helm/www/lambdadelta/version_1.html b/helm/www/lambdadelta/version_1.html
index e62b68ee98f0c0aa5c0e3d4673038b2cffa49b29..4a107c7c4d3efc6a93c5de6b20f305d29be9a7c1 100644 (file)
--- a/helm/www/lambdadelta/version_1.html
+++ b/helm/www/lambdadelta/version_1.html
@@ -167,6 +167,6 @@
     <div xmlns:ld="http://lambdadelta.info/" class="spacer">
       <br />
     </div>
-    <div xmlns:ld="http://lambdadelta.info/" class="spacer">Last update: Sun, 20 Jul 2014 16:13:31 +0200</div>
+    <div xmlns:ld="http://lambdadelta.info/" class="spacer">Last update: Tue, 05 Aug 2014 23:07:40 +0200</div>
 </body>
 </html>

diff --git a/helm/www/lambdadelta/version_2.html b/helm/www/lambdadelta/version_2.html
index 719331a082330d0af9beff80ffbf0ed846fc6aab..63e5d7506401790f5fabc82b6136e24a51d3fa62 100644 (file)
--- a/helm/www/lambdadelta/version_2.html
+++ b/helm/www/lambdadelta/version_2.html
@@ -91,7 +91,7 @@
    <ul xmlns:ld="http://lambdadelta.info/" id="source">
       <li>
       <a href="http://lambdadelta.info/download/lambdadelta_2.tar.gz">lambdadelta_2 for Matita 0.99.2</a>
-      (revised <span class="date">2014-07</span>).
+      (revised <span class="date">2014-08</span>).
       Source scripts.
    </li>
     </ul>
@@ -131,6 +131,6 @@
     <div xmlns:ld="http://lambdadelta.info/" class="spacer">
       <br />
     </div>
-    <div xmlns:ld="http://lambdadelta.info/" class="spacer">Last update: Sun, 20 Jul 2014 16:13:31 +0200</div>
+    <div xmlns:ld="http://lambdadelta.info/" class="spacer">Last update: Tue, 05 Aug 2014 23:07:40 +0200</div>
 </body>
 </html>

diff --git a/helm/www/lambdadelta/web/home/documentation_1.tbl b/helm/www/lambdadelta/web/home/documentation_1.tbl
index 07114eec287e93ab3c0b15c8057af2d553d7e2e9..11b9ddb311542953780073a4e7aa1d5c40c7bde6 100644 (file)
--- a/helm/www/lambdadelta/web/home/documentation_1.tbl
+++ b/helm/www/lambdadelta/web/home/documentation_1.tbl
@@ -86,6 +86,14 @@ table {
      "<span class=\"date\">in Italian</span>)."
      * }
    ]
+   [ { name "ldV1" "<span class=\"date\">V1.</span>" "" } {
+     "F. Guidi:" +
+     @@("version_1.html" "lambdadelta_1") +
+     "(revised <span class=\"date\">2012-10</span>)." +
+     "Formal specification for the proof assistant Coq 7.3.1 (scripts)." +
+     @@("documentation.html#bibtex" "BibTeX entry") ^ "."
+     * }
+   ]
 }
 
 class "top" [ * ]

diff --git a/helm/www/lambdadelta/web/home/documentation_2.tbl b/helm/www/lambdadelta/web/home/documentation_2.tbl
index 9a50d94d26776b45d4878f2eb0a204e636feaa98..3a41318127b19ed208e520326e5e6b420605bdf8 100644 (file)
--- a/helm/www/lambdadelta/web/home/documentation_2.tbl
+++ b/helm/www/lambdadelta/web/home/documentation_2.tbl
@@ -47,7 +47,7 @@ table {
    [ { name "ldV2" "<span class=\"date\">V2.</span>" "" } {
      "F. Guidi:" +
      @@("version_2.html" "lambdadelta_2") +
-     "(revised <span class=\"date\">2014-07</span>)." +
+     "(revised <span class=\"date\">2014-08</span>)." +
      "Formal specification for the proof assistant Matita 0.99.2 (scripts)." +
      @@("documentation.html#bibtex" "BibTeX entry") ^ "."
      * }

diff --git a/helm/www/lambdadelta/web/home/version_2.ldw.xml b/helm/www/lambdadelta/web/home/version_2.ldw.xml
index 9c002c7c96a90788738f16001172286f31c8c7e0..b760295a3b62fa48e2681437c8529aa4f70aaaef 100644 (file)
--- a/helm/www/lambdadelta/web/home/version_2.ldw.xml
+++ b/helm/www/lambdadelta/web/home/version_2.ldw.xml
@@ -16,7 +16,7 @@
 
    <topitem name="source">
       <rlink to="download/lambdadelta_2.tar.gz">lambdadelta_2 for Matita 0.99.2</rlink>
-      (revised <date date="2014-07"/>).
+      (revised <date date="2014-08"/>).
       Source scripts.
    </topitem>