- we add an informational page on \lambda\delta version 1 (core)

- web site update

diff --git a/helm/www/lambdadelta/BTM.html b/helm/www/lambdadelta/BTM.html
index e33fe4a914657f5fc890de0cb9af89ea743fbd6c..a436738f28692659711b384c643b65fdfaee7fe8 100644 (file)
--- a/helm/www/lambdadelta/BTM.html
+++ b/helm/www/lambdadelta/BTM.html
@@ -222,6 +222,6 @@
     <div xmlns:ld="http://lambdadelta.info/" class="spacer">
       <br />
     </div>
-    <div xmlns:ld="http://lambdadelta.info/" class="spacer">Last update: Thu, 15 Jan 2015 16:54:45 +0100</div>
+    <div xmlns:ld="http://lambdadelta.info/" class="spacer">Last update: Sun, 18 Jan 2015 17:28:58 +0100</div>
   </body>
 </html>

diff --git a/helm/www/lambdadelta/apps_2.html b/helm/www/lambdadelta/apps_2.html
index 379c28ce3622fc1fdaed55e7f04e19ff9f50b8ce..2e773d14b5fbc9cf1ba639b06f2ea37e4cd52aae 100644 (file)
--- a/helm/www/lambdadelta/apps_2.html
+++ b/helm/www/lambdadelta/apps_2.html
@@ -45,6 +45,9 @@
             <td class="snnn capitalize italic green">
               <br />
             </td>
+            <td class="snnn capitalize italic green">
+              <br />
+            </td>
             <td class="snns capitalize italic green">
               <a href="http://lambdadelta.info/implementation.html">implementation</a>
             </td>
@@ -66,6 +69,9 @@
               <a href="http://lambdadelta.info/specification.html#v2">version 2</a>
             </td>
             <td class="snnn capitalize green">(<a href="http://lambdadelta.info/ground_2.html">background</a> - <a href="http://lambdadelta.info/basic_2.html">core</a> - <a href="http://lambdadelta.info/apps_2.html">applications</a>)</td>
+            <td class="snnn capitalize green">
+              <br />
+            </td>
             <td class="snns capitalize green">
               <a href="http://lambdadelta.info/implementation.html#lddl">library</a>
             </td>
@@ -84,6 +90,7 @@
             <td class="snss capitalize green">
               <a href="http://lambdadelta.info/specification.html#v1">version 1</a>
             </td>
+            <td class="snsn capitalize green">(<a href="http://lambdadelta.info/basic_1.html">core</a>)</td>
             <td class="snsn capitalize green">(<a href="http://lambdadelta.info/static/matita/lambdadelta/">static HELM directory</a>)</td>
             <td class="snss capitalize green">
               <a href="http://lambdadelta.info/implementation.html#helena">helena</a>
@@ -117,7 +124,7 @@
     </ul>
     <div xmlns:ld="http://lambdadelta.info/" class="head2dx" id="summary">Summary of the Specification <img class="icon37" alt="[spacer]" title="lambdadelta butterfly" src="http://lambdadelta.info/images/b4.png" />
     </div>
-    <div xmlns:ld="http://lambdadelta.info/" class="text">Here is a numerical acount of the specification's contents
+    <div xmlns:ld="http://lambdadelta.info/" class="text">Here is a numerical account of the specification's contents
          and its timeline.
    </div>
     <div xmlns:ld="http://lambdadelta.info/" class="text">
@@ -145,29 +152,29 @@
           <tr>
             <td class="snns capitalize italic cyan">sizes</td>
             <td class="snns italic cyan">files</td>
-            <td class="snnn right italic cyan">4</td>
+            <td class="snnn right italic cyan">14</td>
             <td class="snns italic cyan">characters</td>
-            <td class="snnn right italic cyan">68581</td>
+            <td class="snnn right italic cyan">6787</td>
             <td class="snns italic cyan">nodes</td>
-            <td class="ssnn right italic cyan">3637</td>
+            <td class="ssnn right italic cyan">10070</td>
           </tr>
           <tr>
             <td class="snns capitalize italic green">propositions</td>
             <td class="snns italic green">theorems</td>
             <td class="snnn right italic green">2</td>
             <td class="snns italic green">lemmas</td>
-            <td class="snnn right italic green">1</td>
+            <td class="snnn right italic green">4</td>
             <td class="snns italic green">total</td>
-            <td class="ssnn right italic green">3</td>
+            <td class="ssnn right italic green">6</td>
           </tr>
           <tr>
             <td class="snss capitalize italic yellow">concepts</td>
             <td class="snss italic yellow">declared</td>
-            <td class="snsn right italic yellow">3</td>
+            <td class="snsn right italic yellow">6</td>
             <td class="snss italic yellow">defined</td>
-            <td class="snsn right italic yellow">9</td>
+            <td class="snsn right italic yellow">11</td>
             <td class="snss italic yellow">total</td>
-            <td class="sssn right italic yellow">12</td>
+            <td class="sssn right italic yellow">17</td>
           </tr>
         </tbody>
       </table>
@@ -251,6 +258,6 @@
     <div xmlns:ld="http://lambdadelta.info/" class="spacer">
       <br />
     </div>
-    <div xmlns:ld="http://lambdadelta.info/" class="spacer">Last update: Thu, 15 Jan 2015 16:54:45 +0100</div>
+    <div xmlns:ld="http://lambdadelta.info/" class="spacer">Last update: Sun, 18 Jan 2015 17:28:58 +0100</div>
   </body>
 </html>

diff --git a/helm/www/lambdadelta/basic_1.html b/helm/www/lambdadelta/basic_1.html
new file mode 100644 (file)
index 0000000..ffaf8b4
--- /dev/null
+++ b/helm/www/lambdadelta/basic_1.html
@@ -0,0 +1,729 @@
+<?xml version="1.0" encoding="UTF-8"?>
+<!DOCTYPE html PUBLIC "-//W3C//DTD XHTML 1.1//EN" "http://www.w3.org/TR/xhtml11/DTD/xhtml11.dtd">
+<html xmlns="http://www.w3.org/1999/xhtml" dir="ltr" lang="en-us">
+  <head>
+    <meta http-equiv="Content-Language" content="en-us" />
+    <meta http-equiv="Content-Type" content="text/html; charset=UTF-8" />
+    <meta http-equiv="Content-Style-Type" content="text/css" />
+    <meta name="author" content="Ferruccio Guidi" />
+    <meta name="description" content="\lambda\delta home page" />
+    <title>\lambda\delta home page</title>
+    <link rel="stylesheet" type="text/css" href="http://lambdadelta.info/css/ld_web.css" />
+    <link rel="stylesheet" type="text/css" href="http://lambdadelta.info/css/lddl.css" />
+    <link rel="stylesheet" type="text/css" href="http://lambdadelta.info/css/xhtbl.css" />
+    <link rel="shortcut icon" href="http://lambdadelta.info/images/crux_16.ico" />
+  </head>
+  <body lang="en-US">
+    <div class="spacer">
+      <a href="http://lambdadelta.info/">
+        <img class="icon32" alt="[lambdadelta home]" title="lambdadelta home" src="http://lambdadelta.info/images/crux_32.png" />
+      </a>
+    </div>
+    <div class="head1">cic:/BOLOGNA/lambdadelta/basic_1/ (core λδ version 1)</div>
+    <div class="spacer">
+      <img class="rule" alt="[Spacer]" title="lambdadelta rainbow rule" src="http://lambdadelta.info/images/rainbow.png" />
+    </div>
+    <div xmlns:ld="http://lambdadelta.info/" class="spacer">
+      <br />
+    </div>
+    <div xmlns:ld="http://lambdadelta.info/" class="text">
+      <table cellpadding="4" cellspacing="0">
+        <tbody>
+          <tr>
+            <td class="snns capitalize italic sky">
+              <a href="http://lambdadelta.info/index.html">home</a>
+            </td>
+            <td class="snns capitalize italic magenta">
+              <a href="http://lambdadelta.info/news.html">news</a>
+            </td>
+            <td class="snns capitalize italic orange">
+              <a href="http://lambdadelta.info/documentation.html">documentation</a>
+            </td>
+            <td class="snns capitalize italic green">
+              <a href="http://lambdadelta.info/specification.html">specification</a>
+            </td>
+            <td class="snnn capitalize italic green">
+              <br />
+            </td>
+            <td class="snnn capitalize italic green">
+              <br />
+            </td>
+            <td class="snns capitalize italic green">
+              <a href="http://lambdadelta.info/implementation.html">implementation</a>
+            </td>
+            <td class="ssnn capitalize italic green">
+              <br />
+            </td>
+          </tr>
+          <tr>
+            <td class="snns capitalize sky">
+              <a href="http://lambdadelta.info/index.html#foreword">foreword</a>
+            </td>
+            <td class="snns capitalize magenta">
+              <a href="http://lambdadelta.info/news.html#milestones">milestones</a>
+            </td>
+            <td class="snns capitalize orange">
+              <a href="http://lambdadelta.info/documentation.html#v2">version 2</a>
+            </td>
+            <td class="snns capitalize green">
+              <a href="http://lambdadelta.info/specification.html#v2">version 2</a>
+            </td>
+            <td class="snnn capitalize green">(<a href="http://lambdadelta.info/ground_2.html">background</a> - <a href="http://lambdadelta.info/basic_2.html">core</a> - <a href="http://lambdadelta.info/apps_2.html">applications</a>)</td>
+            <td class="snnn capitalize green">
+              <br />
+            </td>
+            <td class="snns capitalize green">
+              <a href="http://lambdadelta.info/implementation.html#lddl">library</a>
+            </td>
+            <td class="ssnn capitalize green">(<a href="http://lambdadelta.info/static/lddl/">static LDDL directory</a>)</td>
+          </tr>
+          <tr>
+            <td class="snss capitalize sky">
+              <a href="http://lambdadelta.info/index.html#citations">citations</a>
+            </td>
+            <td class="snss capitalize magenta">
+              <a href="http://lambdadelta.info/news.html#visibility">visibility</a>
+            </td>
+            <td class="snss capitalize orange">
+              <a href="http://lambdadelta.info/documentation.html#v1">version 1</a>
+            </td>
+            <td class="snss capitalize green">
+              <a href="http://lambdadelta.info/specification.html#v1">version 1</a>
+            </td>
+            <td class="snsn capitalize green">(<a href="http://lambdadelta.info/basic_1.html">core</a>)</td>
+            <td class="snsn capitalize green">(<a href="http://lambdadelta.info/static/matita/lambdadelta/">static HELM directory</a>)</td>
+            <td class="snss capitalize green">
+              <a href="http://lambdadelta.info/implementation.html#helena">helena</a>
+            </td>
+            <td class="sssn capitalize green">
+              <br />
+            </td>
+          </tr>
+        </tbody>
+      </table>
+    </div>
+    <!--   
+   <section>System's Syntax and Behavior</section>
+   <body>This is a summary of the "block structure"
+         of the System's syntactic items and reductions.
+   </body>
+   <table name="basic_1_blk"/>
+   <body>* In terms only.
+         ** In terms and local environments only.
+         *** In global environments only.
+         **** Sort level k in terms only.
+   </body>
+-->
+    <div xmlns:ld="http://lambdadelta.info/" class="head2dx" id="summary">Summary of the Specification <img class="icon37" alt="[spacer]" title="lambdadelta butterfly" src="http://lambdadelta.info/images/b6.png" />
+    </div>
+    <div xmlns:ld="http://lambdadelta.info/" class="text">Here is a numerical account of the specification's contents
+         and its timeline.
+   </div>
+    <!--
+   <table name="basic_1_sum"/>
+-->
+    <ul xmlns:ld="http://lambdadelta.info/">
+      <li>
+        <span class="emph delta">January 2015.</span>
+      Update with with backports from the abandoned specification of λδ version 2.
+   </li>
+    </ul>
+    <ul xmlns:ld="http://lambdadelta.info/">
+      <li>
+        <span class="emph delta">May 2008.</span>
+      Specification is concluded.
+   </li>
+    </ul>
+    <ul xmlns:ld="http://lambdadelta.info/">
+      <li>
+        <span class="emph gamma">November 2006.</span>
+      Decidability of native type assignment, λδ version 1 is released.
+   </li>
+    </ul>
+    <ul xmlns:ld="http://lambdadelta.info/">
+      <li>
+        <span class="emph beta">December 2005.</span>
+      Preservation of native type by reduction, λδ version 1 is announced.
+   </li>
+    </ul>
+    <ul xmlns:ld="http://lambdadelta.info/">
+      <li>
+        <span class="emph alpha">May 2004.</span>
+      Specification starts.
+   </li>
+    </ul>
+    <div xmlns:ld="http://lambdadelta.info/" class="head2dx" id="structure">Logical Structure of the Specification <img class="icon37" alt="[spacer]" title="lambdadelta butterfly" src="http://lambdadelta.info/images/b6.png" />
+    </div>
+    <div xmlns:ld="http://lambdadelta.info/" class="text">This table reports the specification's components and their planes.
+   </div>
+    <div xmlns:ld="http://lambdadelta.info/" class="text">
+      <table cellpadding="4" cellspacing="0">
+        <tbody>
+          <tr>
+            <td class="snns top capitalize italic gray">component</td>
+            <td class="snns top italic gray">plane</td>
+            <td class="snns top gray">files</td>
+            <td class="ssnn top gray">
+              <br />
+            </td>
+          </tr>
+          <tr>
+            <td class="snns top capitalize italic wine">examples</td>
+            <td class="snns top italic wine">terms with special features</td>
+            <td class="snns top wine">
+              <a href="http://lambdadelta.info/static/coq/lambdadelta/basic_1/levels_ex0.txt">levels_ex0</a>
+              <a href="http://lambdadelta.info/static/coq/lambdadelta/basic_1/ty3_ex1.txt">ty3_ex1</a>
+              <a href="http://lambdadelta.info/static/coq/lambdadelta/basic_1/nf2_ex2.txt">nf2_ex2</a>
+            </td>
+            <td class="ssnn top wine">
+              <br />
+            </td>
+          </tr>
+          <tr>
+            <td class="snns top capitalize italic magenta" />
+            <td class="snns top italic magenta" />
+            <td class="snns top magenta" />
+            <td class="ssnn top magenta">
+              <br />
+            </td>
+          </tr>
+          <tr>
+            <td class="snns top capitalize italic prune">dynamic typing</td>
+            <td class="snns top italic prune">well-formed contexts</td>
+            <td class="snns top prune">
+              <a href="http://lambdadelta.info/static/coq/lambdadelta/basic_1/wf3_defs.txt">wf3_defs</a>
+            </td>
+            <td class="ssnn top prune">
+              <a href="http://lambdadelta.info/static/coq/lambdadelta/basic_1/wf3_props.txt">wf3_props</a>
+            </td>
+          </tr>
+          <tr>
+            <td class="nnns top capitalize italic prune">
+              <br />
+            </td>
+            <td class="snns top italic prune">context ref. for native type assignment</td>
+            <td class="snns top prune">
+              <a href="http://lambdadelta.info/static/coq/lambdadelta/basic_1/csubt_defs.txt">csubt_defs</a>
+            </td>
+            <td class="ssnn top prune">
+              <a href="http://lambdadelta.info/static/coq/lambdadelta/basic_1/csubt_props.txt">csubt_props</a>
+              <a href="http://lambdadelta.info/static/coq/lambdadelta/basic_1/csubt_arity_props.txt">csubt_arity_props</a>
+            </td>
+          </tr>
+          <tr>
+            <td class="nnns top capitalize italic prune">
+              <br />
+            </td>
+            <td class="snns top italic prune">native type assignment</td>
+            <td class="snns top prune">
+              <a href="http://lambdadelta.info/static/coq/lambdadelta/basic_1/ty3_defs.txt">ty3_defs</a>
+            </td>
+            <td class="ssnn top prune">
+              <a href="http://lambdadelta.info/static/coq/lambdadelta/basic_1/ty3_props.txt">ty3_props</a>
+              <a href="http://lambdadelta.info/static/coq/lambdadelta/basic_1/ty3_gen.txt">ty3_gen</a>
+              <a href="http://lambdadelta.info/static/coq/lambdadelta/basic_1/ty3_gen_context.txt">ty3_gen_context</a>
+              <a href="http://lambdadelta.info/static/coq/lambdadelta/basic_1/ty3_gen_nf2.txt">ty3_gen_nf2</a>
+              <a href="http://lambdadelta.info/static/coq/lambdadelta/basic_1/ty3_lift.txt">ty3_lift</a>
+              <a href="http://lambdadelta.info/static/coq/lambdadelta/basic_1/ty3_subst0.txt">ty3_subst0</a>
+              <a href="http://lambdadelta.info/static/coq/lambdadelta/basic_1/ty3_arity_props.txt">ty3_arity_props</a>
+              <a href="http://lambdadelta.info/static/coq/lambdadelta/basic_1/ty3_nf2_gen.txt">ty3_nf2_gen</a>
+              <a href="http://lambdadelta.info/static/coq/lambdadelta/basic_1/ty3_sred.txt">ty3_sred</a>
+              <a href="http://lambdadelta.info/static/coq/lambdadelta/basic_1/ty3_sred_props.txt">ty3_sred_props</a>
+              <a href="http://lambdadelta.info/static/coq/lambdadelta/basic_1/ty3_dec.txt">ty3_dec</a>
+            </td>
+          </tr>
+          <tr>
+            <td class="snns top capitalize italic blue">equivalence</td>
+            <td class="snns top italic blue">context-sensitive equivalence</td>
+            <td class="snns top blue">
+              <a href="http://lambdadelta.info/static/coq/lambdadelta/basic_1/pc3_defs.txt">pc3_defs</a>
+            </td>
+            <td class="ssnn top blue">
+              <a href="http://lambdadelta.info/static/coq/lambdadelta/basic_1/pc3_props.txt">pc3_props</a>
+              <a href="http://lambdadelta.info/static/coq/lambdadelta/basic_1/pc3_gen.txt">pc3_gen</a>
+              <a href="http://lambdadelta.info/static/coq/lambdadelta/basic_1/pc3_gen_context.txt">pc3_gen_context</a>
+              <a href="http://lambdadelta.info/static/coq/lambdadelta/basic_1/pc3_subst0.txt">pc3_subst0</a>
+            </td>
+          </tr>
+          <tr>
+            <td class="nnns top capitalize italic blue">
+              <br />
+            </td>
+            <td class="snns top italic blue">context-free equivalence</td>
+            <td class="snns top blue">
+              <a href="http://lambdadelta.info/static/coq/lambdadelta/basic_1/pc1_defs.txt">pc1_defs</a>
+            </td>
+            <td class="ssnn top blue">
+              <a href="http://lambdadelta.info/static/coq/lambdadelta/basic_1/pc1_props.txt">pc1_props</a>
+            </td>
+          </tr>
+          <tr>
+            <td class="snns top capitalize italic sky" />
+            <td class="snns top italic sky" />
+            <td class="snns top sky" />
+            <td class="ssnn top sky">
+              <br />
+            </td>
+          </tr>
+          <tr>
+            <td class="snns top capitalize italic cyan">computation</td>
+            <td class="snns top italic cyan">context ref. for reducibility</td>
+            <td class="snns top cyan">
+              <a href="http://lambdadelta.info/static/coq/lambdadelta/basic_1/csubc_defs.txt">csubc_defs</a>
+            </td>
+            <td class="ssnn top cyan">
+              <a href="http://lambdadelta.info/static/coq/lambdadelta/basic_1/csubc_props.txt">csubc_props</a>
+            </td>
+          </tr>
+          <tr>
+            <td class="nnns top capitalize italic cyan">
+              <br />
+            </td>
+            <td class="snns top italic cyan">reducibility</td>
+            <td class="snns top cyan">
+              <a href="http://lambdadelta.info/static/coq/lambdadelta/basic_1/sc3_defs.txt">sc3_defs</a>
+            </td>
+            <td class="ssnn top cyan">
+              <a href="http://lambdadelta.info/static/coq/lambdadelta/basic_1/sc3_props.txt">sc3_props</a>
+              <a href="http://lambdadelta.info/static/coq/lambdadelta/basic_1/sc3_arity.txt">sc3_arity</a>
+            </td>
+          </tr>
+          <tr>
+            <td class="nnns top capitalize italic cyan">
+              <br />
+            </td>
+            <td class="snns top italic cyan">strongly normalizing computation</td>
+            <td class="snns top cyan">
+              <a href="http://lambdadelta.info/static/coq/lambdadelta/basic_1/sn3_defs.txt">sn3_defs</a>
+            </td>
+            <td class="ssnn top cyan">
+              <a href="http://lambdadelta.info/static/coq/lambdadelta/basic_1/sn3_gen.txt">sn3_gen</a>
+              <a href="http://lambdadelta.info/static/coq/lambdadelta/basic_1/sn3_props.txt">sn3_props</a>
+            </td>
+          </tr>
+          <tr>
+            <td class="nnns top capitalize italic cyan">
+              <br />
+            </td>
+            <td class="snns top italic cyan">context-sensitive computation</td>
+            <td class="snns top cyan">
+              <a href="http://lambdadelta.info/static/coq/lambdadelta/basic_1/pr3_defs.txt">pr3_defs</a>
+            </td>
+            <td class="ssnn top cyan">
+              <a href="http://lambdadelta.info/static/coq/lambdadelta/basic_1/pr3_props.txt">pr3_props</a>
+              <a href="http://lambdadelta.info/static/coq/lambdadelta/basic_1/pr3_gen.txt">pr3_gen</a>
+              <a href="http://lambdadelta.info/static/coq/lambdadelta/basic_1/pr3_gen_context.txt">pr3_gen_context</a>
+              <a href="http://lambdadelta.info/static/coq/lambdadelta/basic_1/pr3_iso.txt">pr3_iso</a>
+              <a href="http://lambdadelta.info/static/coq/lambdadelta/basic_1/pr3_subst1.txt">pr3_subst1</a>
+              <a href="http://lambdadelta.info/static/coq/lambdadelta/basic_1/pr3_confluence.txt">pr3_confluence</a>
+            </td>
+          </tr>
+          <tr>
+            <td class="nnns top capitalize italic cyan">
+              <br />
+            </td>
+            <td class="snns top italic cyan">context-free computation</td>
+            <td class="snns top cyan">
+              <a href="http://lambdadelta.info/static/coq/lambdadelta/basic_1/pr1_defs.txt">pr1_defs</a>
+            </td>
+            <td class="ssnn top cyan">
+              <a href="http://lambdadelta.info/static/coq/lambdadelta/basic_1/pr1_props.txt">pr1_props</a>
+              <a href="http://lambdadelta.info/static/coq/lambdadelta/basic_1/pr1_confluence.txt">pr1_confluence</a>
+            </td>
+          </tr>
+          <tr>
+            <td class="snns top capitalize italic water">reduction</td>
+            <td class="snns top italic water">normal forms for context-sensitive reduction</td>
+            <td class="snns top water">
+              <a href="http://lambdadelta.info/static/coq/lambdadelta/basic_1/nf2_defs.txt">nf2_defs</a>
+            </td>
+            <td class="ssnn top water">
+              <a href="http://lambdadelta.info/static/coq/lambdadelta/basic_1/nf2_props.txt">nf2_props</a>
+              <a href="http://lambdadelta.info/static/coq/lambdadelta/basic_1/nf2_gen.txt">nf2_gen</a>
+              <a href="http://lambdadelta.info/static/coq/lambdadelta/basic_1/nf2_dec.txt">nf2_dec</a>
+            </td>
+          </tr>
+          <tr>
+            <td class="nnns top capitalize italic water">
+              <br />
+            </td>
+            <td class="snns top italic water">context-sensitive reduction</td>
+            <td class="snns top water">
+              <a href="http://lambdadelta.info/static/coq/lambdadelta/basic_1/pr2_defs.txt">pr2_defs</a>
+            </td>
+            <td class="ssnn top water">
+              <a href="http://lambdadelta.info/static/coq/lambdadelta/basic_1/pr2_gen.txt">pr2_gen</a>
+              <a href="http://lambdadelta.info/static/coq/lambdadelta/basic_1/pr2_gen_context.txt">pr2_gen_context</a>
+              <a href="http://lambdadelta.info/static/coq/lambdadelta/basic_1/pr2_lift.txt">pr2_lift</a>
+              <a href="http://lambdadelta.info/static/coq/lambdadelta/basic_1/pr2_subst1.txt">pr2_subst1</a>
+              <a href="http://lambdadelta.info/static/coq/lambdadelta/basic_1/pr2_confluence.txt">pr2_confluence</a>
+            </td>
+          </tr>
+          <tr>
+            <td class="nnns top capitalize italic water">
+              <br />
+            </td>
+            <td class="snns top italic water">normal forms for context-free reduction</td>
+            <td class="snns top water" />
+            <td class="ssnn top water">
+              <a href="http://lambdadelta.info/static/coq/lambdadelta/basic_1/nf0_dec.txt">nf0_dec</a>
+            </td>
+          </tr>
+          <tr>
+            <td class="nnns top capitalize italic water">
+              <br />
+            </td>
+            <td class="snns top italic water">context-free reduction</td>
+            <td class="snns top water">
+              <a href="http://lambdadelta.info/static/coq/lambdadelta/basic_1/wcpr0_defs.txt">wcpr0_defs</a>
+            </td>
+            <td class="ssnn top water">
+              <br />
+            </td>
+          </tr>
+          <tr>
+            <td class="nnns top capitalize italic water">
+              <br />
+            </td>
+            <td class="nnns top italic water">
+              <br />
+            </td>
+            <td class="snns top water">
+              <a href="http://lambdadelta.info/static/coq/lambdadelta/basic_1/pr0_defs.txt">pr0_defs</a>
+            </td>
+            <td class="ssnn top water">
+              <a href="http://lambdadelta.info/static/coq/lambdadelta/basic_1/pr0_gen.txt">pr0_gen</a>
+              <a href="http://lambdadelta.info/static/coq/lambdadelta/basic_1/pr0_lift.txt">pr0_lift</a>
+              <a href="http://lambdadelta.info/static/coq/lambdadelta/basic_1/pr0_subst0.txt">pr0_subst0</a>
+              <a href="http://lambdadelta.info/static/coq/lambdadelta/basic_1/pr0_subst1.txt">pr0_subst1</a>
+              <a href="http://lambdadelta.info/static/coq/lambdadelta/basic_1/pr0_confluence.txt">pr0_confluence</a>
+            </td>
+          </tr>
+          <tr>
+            <td class="snns top capitalize italic green">unfold</td>
+            <td class="snns top italic green">iterated static type assignment</td>
+            <td class="snns top green">
+              <a href="http://lambdadelta.info/static/coq/lambdadelta/basic_1/sty1_defs.txt">sty1_defs</a>
+            </td>
+            <td class="ssnn top green">
+              <a href="http://lambdadelta.info/static/coq/lambdadelta/basic_1/sty1_props.txt">sty1_props</a>
+            </td>
+          </tr>
+          <tr>
+            <td class="snns top capitalize italic grass">static typing</td>
+            <td class="snns top italic grass">static type assignment</td>
+            <td class="snns top grass">
+              <a href="http://lambdadelta.info/static/coq/lambdadelta/basic_1/sty0_defs.txt">sty0_defs</a>
+            </td>
+            <td class="ssnn top grass">
+              <a href="http://lambdadelta.info/static/coq/lambdadelta/basic_1/sty0_props.txt">sty0_props</a>
+            </td>
+          </tr>
+          <tr>
+            <td class="nnns top capitalize italic grass">
+              <br />
+            </td>
+            <td class="snns top italic grass">context ref. for binary arity assignment</td>
+            <td class="snns top grass">
+              <a href="http://lambdadelta.info/static/coq/lambdadelta/basic_1/csuba_defs.txt">csuba_defs</a>
+            </td>
+            <td class="ssnn top grass">
+              <a href="http://lambdadelta.info/static/coq/lambdadelta/basic_1/csuba_props.txt">csuba_props</a>
+            </td>
+          </tr>
+          <tr>
+            <td class="nnns top capitalize italic grass">
+              <br />
+            </td>
+            <td class="snns top italic grass">binary arity assignment</td>
+            <td class="snns top grass">
+              <a href="http://lambdadelta.info/static/coq/lambdadelta/basic_1/arity_defs.txt">arity_defs</a>
+            </td>
+            <td class="ssnn top grass">
+              <a href="http://lambdadelta.info/static/coq/lambdadelta/basic_1/arity_props.txt">arity_props</a>
+              <a href="http://lambdadelta.info/static/coq/lambdadelta/basic_1/arity_gen.txt">arity_gen</a>
+              <a href="http://lambdadelta.info/static/coq/lambdadelta/basic_1/arity_subst0.txt">arity_subst0</a>
+              <a href="http://lambdadelta.info/static/coq/lambdadelta/basic_1/arity_sred.txt">arity_sred</a>
+            </td>
+          </tr>
+          <tr>
+            <td class="nnns top capitalize italic grass">
+              <br />
+            </td>
+            <td class="snns top italic grass">binary arity</td>
+            <td class="snns top grass">
+              <a href="http://lambdadelta.info/static/coq/lambdadelta/basic_1/levels_defs.txt">levels_defs</a>
+              <a href="http://lambdadelta.info/static/coq/lambdadelta/basic_1/llt_defs.txt">llt_defs</a>
+              <a href="http://lambdadelta.info/static/coq/lambdadelta/basic_1/aprem_defs.txt">aprem_defs</a>
+            </td>
+            <td class="ssnn top grass">
+              <br />
+            </td>
+          </tr>
+          <tr>
+            <td class="nnns top capitalize italic grass">
+              <br />
+            </td>
+            <td class="snns top italic grass">parameters</td>
+            <td class="snns top grass">
+              <a href="http://lambdadelta.info/static/coq/lambdadelta/basic_1/parameter_defs.txt">parameter_defs</a>
+            </td>
+            <td class="ssnn top grass">
+              <br />
+            </td>
+          </tr>
+          <tr>
+            <td class="nnns top capitalize italic grass">
+              <br />
+            </td>
+            <td class="snns top italic grass">basic context ref.</td>
+            <td class="snns top grass">
+              <a href="http://lambdadelta.info/static/coq/lambdadelta/basic_1/csubv_defs.txt">csubv_defs</a>
+            </td>
+            <td class="ssnn top grass">
+              <br />
+            </td>
+          </tr>
+          <tr>
+            <td class="snns top capitalize italic yellow">multiple substitution</td>
+            <td class="snns top italic yellow">iterated context slicing</td>
+            <td class="snns top yellow">
+              <a href="http://lambdadelta.info/static/coq/lambdadelta/basic_1/drop1_defs.txt">drop1_defs</a>
+            </td>
+            <td class="ssnn top yellow">
+              <a href="http://lambdadelta.info/static/coq/lambdadelta/basic_1/drop1_props.txt">drop1_props</a>
+            </td>
+          </tr>
+          <tr>
+            <td class="nnns top capitalize italic yellow">
+              <br />
+            </td>
+            <td class="snns top italic yellow">generic term relocation</td>
+            <td class="snns top yellow">
+              <a href="http://lambdadelta.info/static/coq/lambdadelta/basic_1/lift1_defs.txt">lift1_defs</a>
+            </td>
+            <td class="ssnn top yellow">
+              <a href="http://lambdadelta.info/static/coq/lambdadelta/basic_1/lift1_props.txt">lift1_props</a>
+            </td>
+          </tr>
+          <tr>
+            <td class="snns top capitalize italic orange">substitution</td>
+            <td class="snns top italic orange">ordinary substitution</td>
+            <td class="snns top orange">
+              <a href="http://lambdadelta.info/static/coq/lambdadelta/basic_1/subst_defs.txt">subst_defs</a>
+            </td>
+            <td class="ssnn top orange">
+              <a href="http://lambdadelta.info/static/coq/lambdadelta/basic_1/subst_props.txt">subst_props</a>
+            </td>
+          </tr>
+          <tr>
+            <td class="nnns top capitalize italic orange">
+              <br />
+            </td>
+            <td class="nnns top italic orange">
+              <br />
+            </td>
+            <td class="snns top orange">
+              <a href="http://lambdadelta.info/static/coq/lambdadelta/basic_1/csubst1_defs.txt">csubst1_defs</a>
+            </td>
+            <td class="ssnn top orange">
+              <a href="http://lambdadelta.info/static/coq/lambdadelta/basic_1/csubst1_props.txt">csubst1_props</a>
+            </td>
+          </tr>
+          <tr>
+            <td class="nnns top capitalize italic orange">
+              <br />
+            </td>
+            <td class="nnns top italic orange">
+              <br />
+            </td>
+            <td class="snns top orange">
+              <a href="http://lambdadelta.info/static/coq/lambdadelta/basic_1/subst1_defs.txt">subst1_defs</a>
+            </td>
+            <td class="ssnn top orange">
+              <a href="http://lambdadelta.info/static/coq/lambdadelta/basic_1/subst1_gen.txt">subst1_gen</a>
+              <a href="http://lambdadelta.info/static/coq/lambdadelta/basic_1/subst1_lift.txt">subst1_lift</a>
+              <a href="http://lambdadelta.info/static/coq/lambdadelta/basic_1/subst1_subst1.txt">subst1_subst1</a>
+              <a href="http://lambdadelta.info/static/coq/lambdadelta/basic_1/subst1_confluence.txt">subst1_confluence</a>
+            </td>
+          </tr>
+          <tr>
+            <td class="nnns top capitalize italic orange">
+              <br />
+            </td>
+            <td class="snns top italic orange">normal forms for ordinary strict substitution</td>
+            <td class="snns top orange" />
+            <td class="ssnn top orange">
+              <a href="http://lambdadelta.info/static/coq/lambdadelta/basic_1/dnf_dec.txt">dnf_dec</a>
+            </td>
+          </tr>
+          <tr>
+            <td class="nnns top capitalize italic orange">
+              <br />
+            </td>
+            <td class="snns top italic orange">ordinary strict substitution</td>
+            <td class="snns top orange">
+              <a href="http://lambdadelta.info/static/coq/lambdadelta/basic_1/fsubst0_defs.txt">fsubst0_defs</a>
+            </td>
+            <td class="ssnn top orange">
+              <br />
+            </td>
+          </tr>
+          <tr>
+            <td class="nnns top capitalize italic orange">
+              <br />
+            </td>
+            <td class="nnns top italic orange">
+              <br />
+            </td>
+            <td class="snns top orange">
+              <a href="http://lambdadelta.info/static/coq/lambdadelta/basic_1/csubst0_defs.txt">csubst0_defs</a>
+            </td>
+            <td class="ssnn top orange">
+              <br />
+            </td>
+          </tr>
+          <tr>
+            <td class="nnns top capitalize italic orange">
+              <br />
+            </td>
+            <td class="nnns top italic orange">
+              <br />
+            </td>
+            <td class="snns top orange">
+              <a href="http://lambdadelta.info/static/coq/lambdadelta/basic_1/subst0_defs.txt">subst0_defs</a>
+            </td>
+            <td class="ssnn top orange">
+              <a href="http://lambdadelta.info/static/coq/lambdadelta/basic_1/subst0_gen.txt">subst0_gen</a>
+              <a href="http://lambdadelta.info/static/coq/lambdadelta/basic_1/subst0_tlt.txt">subst0_tlt</a>
+              <a href="http://lambdadelta.info/static/coq/lambdadelta/basic_1/subst0_lift.txt">subst0_lift</a>
+              <a href="http://lambdadelta.info/static/coq/lambdadelta/basic_1/subst0_subst0.txt">subst0_subst0</a>
+              <a href="http://lambdadelta.info/static/coq/lambdadelta/basic_1/subst0_confluence.txt">subst0_confluence</a>
+            </td>
+          </tr>
+          <tr>
+            <td class="nnns top capitalize italic orange">
+              <br />
+            </td>
+            <td class="snns top italic orange">basic local env. slicing</td>
+            <td class="snns top orange">
+              <a href="http://lambdadelta.info/static/coq/lambdadelta/basic_1/getl_defs.txt">getl_defs</a>
+            </td>
+            <td class="ssnn top orange">
+              <a href="http://lambdadelta.info/static/coq/lambdadelta/basic_1/getl_props.txt">getl_props</a>
+            </td>
+          </tr>
+          <tr>
+            <td class="nnns top capitalize italic orange">
+              <br />
+            </td>
+            <td class="nnns top italic orange">
+              <br />
+            </td>
+            <td class="snns top orange">
+              <a href="http://lambdadelta.info/static/coq/lambdadelta/basic_1/drop_defs.txt">drop_defs</a>
+            </td>
+            <td class="ssnn top orange">
+              <a href="http://lambdadelta.info/static/coq/lambdadelta/basic_1/drop_props.txt">drop_props</a>
+            </td>
+          </tr>
+          <tr>
+            <td class="nnns top capitalize italic orange">
+              <br />
+            </td>
+            <td class="snns top italic orange">basic term relocation</td>
+            <td class="snns top orange">
+              <a href="http://lambdadelta.info/static/coq/lambdadelta/basic_1/lift_defs.txt">lift_defs</a>
+            </td>
+            <td class="ssnn top orange">
+              <a href="http://lambdadelta.info/static/coq/lambdadelta/basic_1/lift_props.txt">lift_props</a>
+              <a href="http://lambdadelta.info/static/coq/lambdadelta/basic_1/lift_gen.txt">lift_gen</a>
+              <a href="http://lambdadelta.info/static/coq/lambdadelta/basic_1/lift_tlt.txt">lift_tlt</a>
+            </td>
+          </tr>
+          <tr>
+            <td class="snns top capitalize italic red">grammar</td>
+            <td class="snns top italic red">closures</td>
+            <td class="snns top red">
+              <a href="http://lambdadelta.info/static/coq/lambdadelta/basic_1/flt_defs.txt">flt_defs</a>
+            </td>
+            <td class="ssnn top red">
+              <br />
+            </td>
+          </tr>
+          <tr>
+            <td class="nnns top capitalize italic red">
+              <br />
+            </td>
+            <td class="snns top italic red">contexts</td>
+            <td class="snns top red">
+              <a href="http://lambdadelta.info/static/coq/lambdadelta/basic_1/contexts_defs.txt">contexts_defs</a>
+              <a href="http://lambdadelta.info/static/coq/lambdadelta/basic_1/clt_defs.txt">clt_defs</a>
+              <a href="http://lambdadelta.info/static/coq/lambdadelta/basic_1/ctail_defs.txt">ctail_defs</a>
+              <a href="http://lambdadelta.info/static/coq/lambdadelta/basic_1/app_defs.txt">app_defs</a>
+              <a href="http://lambdadelta.info/static/coq/lambdadelta/basic_1/cnt_defs.txt">cnt_defs</a>
+            </td>
+            <td class="ssnn top red">
+              <br />
+            </td>
+          </tr>
+          <tr>
+            <td class="nnns top capitalize italic red">
+              <br />
+            </td>
+            <td class="snns top italic red">terms</td>
+            <td class="snns top red">
+              <a href="http://lambdadelta.info/static/coq/lambdadelta/basic_1/tlist_defs.txt">tlist_defs</a>
+            </td>
+            <td class="ssnn top red">
+              <br />
+            </td>
+          </tr>
+          <tr>
+            <td class="nnss top capitalize italic red">
+              <br />
+            </td>
+            <td class="nnss top italic red">
+              <br />
+            </td>
+            <td class="snss top red">
+              <a href="http://lambdadelta.info/static/coq/lambdadelta/basic_1/terms_defs.txt">terms_defs</a>
+              <a href="http://lambdadelta.info/static/coq/lambdadelta/basic_1/tlt_defs.txt">tlt_defs</a>
+              <a href="http://lambdadelta.info/static/coq/lambdadelta/basic_1/iso_defs.txt">iso_defs</a>
+            </td>
+            <td class="sssn top red">
+              <br />
+            </td>
+          </tr>
+        </tbody>
+      </table>
+    </div>
+    <div class="spacer">
+      <img class="rule" alt="[Spacer]" title="lambdadelta rainbow rule" src="http://lambdadelta.info/images/rainbow.png" />
+    </div>
+    <div xmlns:ld="http://lambdadelta.info/" class="spacer">
+      <br />
+    </div>
+    <div xmlns:ld="http://lambdadelta.info/" class="spacer">
+      <a href="http://validator.w3.org/check?uri=referer">
+        <img class="w3c" alt="[Valid XHTML 1.1]" title="Valid XHTML 1.1" src="http://www.w3.org/Icons/valid-xhtml11-blue" />
+      </a>
+      <a href="http://jigsaw.w3.org/css-validator/check/referer">
+        <img class="w3c" alt="[Valid CSS level 2]" title="Valid CSS level 2" src="http://www.w3.org/Icons/valid-css2-blue" />
+      </a>
+      <a href="http://www.w3.org/XML/">
+        <img class="w3c" alt="[Generated from XML via XSL]" title="Generated from XML via XSL" src="http://lambdadelta.info/images/xml_xsl2.png" />
+      </a>
+      <a href="http://www.w3.org/Graphics/PNG/">
+        <img class="w3c" alt="[PNG used here]" title="PNG used here" src="http://lambdadelta.info/images/PNGnow2.png" />
+      </a>
+      <a href="http://www.anybrowser.org/campaign/">
+        <img class="w3c" alt="[Viewable with any browser]" title="Viewable with any browser" src="http://www.anybrowser.org/campaign/bvgraphics/abtfile.png" />
+      </a>
+    </div>
+    <div xmlns:ld="http://lambdadelta.info/" class="spacer">
+      <br />
+    </div>
+    <div xmlns:ld="http://lambdadelta.info/" class="spacer">Last update: Sun, 18 Jan 2015 17:28:58 +0100</div>
+  </body>
+</html>

diff --git a/helm/www/lambdadelta/basic_2.html b/helm/www/lambdadelta/basic_2.html
index d3ea2991a2833f5789cd2701bd86fc1fc3b8646f..16a6a66cec871432c597d8214d37e0cde77f18c6 100644 (file)
--- a/helm/www/lambdadelta/basic_2.html
+++ b/helm/www/lambdadelta/basic_2.html
@@ -45,6 +45,9 @@
             <td class="snnn capitalize italic green">
               <br />
             </td>
+            <td class="snnn capitalize italic green">
+              <br />
+            </td>
             <td class="snns capitalize italic green">
               <a href="http://lambdadelta.info/implementation.html">implementation</a>
             </td>
@@ -66,6 +69,9 @@
               <a href="http://lambdadelta.info/specification.html#v2">version 2</a>
             </td>
             <td class="snnn capitalize green">(<a href="http://lambdadelta.info/ground_2.html">background</a> - <a href="http://lambdadelta.info/basic_2.html">core</a> - <a href="http://lambdadelta.info/apps_2.html">applications</a>)</td>
+            <td class="snnn capitalize green">
+              <br />
+            </td>
             <td class="snns capitalize green">
               <a href="http://lambdadelta.info/implementation.html#lddl">library</a>
             </td>
@@ -84,6 +90,7 @@
             <td class="snss capitalize green">
               <a href="http://lambdadelta.info/specification.html#v1">version 1</a>
             </td>
+            <td class="snsn capitalize green">(<a href="http://lambdadelta.info/basic_1.html">core</a>)</td>
             <td class="snsn capitalize green">(<a href="http://lambdadelta.info/static/matita/lambdadelta/">static HELM directory</a>)</td>
             <td class="snss capitalize green">
               <a href="http://lambdadelta.info/implementation.html#helena">helena</a>
@@ -109,7 +116,7 @@
 -->
     <div xmlns:ld="http://lambdadelta.info/" class="head2dx" id="summary">Summary of the Specification <img class="icon37" alt="[spacer]" title="lambdadelta butterfly" src="http://lambdadelta.info/images/b4.png" />
     </div>
-    <div xmlns:ld="http://lambdadelta.info/" class="text">Here is a numerical acount of the specification's contents
+    <div xmlns:ld="http://lambdadelta.info/" class="text">Here is a numerical account of the specification's contents
          and its timeline.
    </div>
     <div xmlns:ld="http://lambdadelta.info/" class="text">
@@ -141,7 +148,7 @@
             <td class="snns italic cyan">characters</td>
             <td class="snnn right italic cyan">433402</td>
             <td class="snns italic cyan">nodes</td>
-            <td class="ssnn right italic cyan">1874774</td>
+            <td class="ssnn right italic cyan">1874778</td>
           </tr>
           <tr>
             <td class="snns capitalize italic green">propositions</td>
@@ -204,7 +211,7 @@
       <li>
         <span class="emph alpha">2014 April 16.</span>
          Lazy equivalence on local environments
-        addded as q-step to rst-computation on closures
+        added as q-step to rst-computation on closures
          (anniversary milestone).
    </li>
     </ul>
@@ -1012,7 +1019,7 @@
             <td class="nnns top capitalize italic yellow">
               <br />
             </td>
-            <td class="snns top italic yellow">contxt-sensitive multiple rt-substitution</td>
+            <td class="snns top italic yellow">context-sensitive multiple rt-substitution</td>
             <td class="snns top yellow">cpys ( ⦃?,?⦄ ⊢ ? ▶*[?,?] ? )</td>
             <td class="snnn top yellow">cpys_alt ( ⦃?,?⦄ ⊢ ? ▶▶*[?,?] ? )</td>
             <td class="snnn top yellow">cpys_lift cpys_cpys</td>
@@ -1152,7 +1159,7 @@
             <td class="nnns top capitalize italic orange">
               <br />
             </td>
-            <td class="snns top italic orange">contxt-sensitive ordinary rt-substitution</td>
+            <td class="snns top italic orange">context-sensitive ordinary rt-substitution</td>
             <td class="snns top orange">cpy ( ⦃?,?⦄ ⊢ ? ▶[?,?] ? )</td>
             <td class="snnn top orange">cpy_lift cpy_nlift cpy_cpy</td>
             <td class="snnn top orange">
@@ -1377,6 +1384,6 @@
     <div xmlns:ld="http://lambdadelta.info/" class="spacer">
       <br />
     </div>
-    <div xmlns:ld="http://lambdadelta.info/" class="spacer">Last update: Thu, 15 Jan 2015 16:54:45 +0100</div>
+    <div xmlns:ld="http://lambdadelta.info/" class="spacer">Last update: Sun, 18 Jan 2015 17:28:58 +0100</div>
   </body>
 </html>

diff --git a/helm/www/lambdadelta/documentation.html b/helm/www/lambdadelta/documentation.html
index 71b7318d6ef6b06833f0aafa728c890cf295979f..1bc4c29ae1e164ce30876c87eed8f0f5eb2335c7 100644 (file)
--- a/helm/www/lambdadelta/documentation.html
+++ b/helm/www/lambdadelta/documentation.html
@@ -45,6 +45,9 @@
             <td class="snnn capitalize italic green">
               <br />
             </td>
+            <td class="snnn capitalize italic green">
+              <br />
+            </td>
             <td class="snns capitalize italic green">
               <a href="http://lambdadelta.info/implementation.html">implementation</a>
             </td>
@@ -66,6 +69,9 @@
               <a href="http://lambdadelta.info/specification.html#v2">version 2</a>
             </td>
             <td class="snnn capitalize green">(<a href="http://lambdadelta.info/ground_2.html">background</a> - <a href="http://lambdadelta.info/basic_2.html">core</a> - <a href="http://lambdadelta.info/apps_2.html">applications</a>)</td>
+            <td class="snnn capitalize green">
+              <br />
+            </td>
             <td class="snns capitalize green">
               <a href="http://lambdadelta.info/implementation.html#lddl">library</a>
             </td>
@@ -84,6 +90,7 @@
             <td class="snss capitalize green">
               <a href="http://lambdadelta.info/specification.html#v1">version 1</a>
             </td>
+            <td class="snsn capitalize green">(<a href="http://lambdadelta.info/basic_1.html">core</a>)</td>
             <td class="snsn capitalize green">(<a href="http://lambdadelta.info/static/matita/lambdadelta/">static HELM directory</a>)</td>
             <td class="snss capitalize green">
               <a href="http://lambdadelta.info/implementation.html#helena">helena</a>
@@ -359,6 +366,6 @@
     <div xmlns:ld="http://lambdadelta.info/" class="spacer">
       <br />
     </div>
-    <div xmlns:ld="http://lambdadelta.info/" class="spacer">Last update: Thu, 15 Jan 2015 16:54:44 +0100</div>
+    <div xmlns:ld="http://lambdadelta.info/" class="spacer">Last update: Sun, 18 Jan 2015 17:28:58 +0100</div>
   </body>
 </html>

diff --git a/helm/www/lambdadelta/ground_2.html b/helm/www/lambdadelta/ground_2.html
index 88f2bef4a61f768eacd40473b348d970ed9570c6..89716b51673af3eded4eb536da325a57634bae29 100644 (file)
--- a/helm/www/lambdadelta/ground_2.html
+++ b/helm/www/lambdadelta/ground_2.html
@@ -45,6 +45,9 @@
             <td class="snnn capitalize italic green">
               <br />
             </td>
+            <td class="snnn capitalize italic green">
+              <br />
+            </td>
             <td class="snns capitalize italic green">
               <a href="http://lambdadelta.info/implementation.html">implementation</a>
             </td>
@@ -66,6 +69,9 @@
               <a href="http://lambdadelta.info/specification.html#v2">version 2</a>
             </td>
             <td class="snnn capitalize green">(<a href="http://lambdadelta.info/ground_2.html">background</a> - <a href="http://lambdadelta.info/basic_2.html">core</a> - <a href="http://lambdadelta.info/apps_2.html">applications</a>)</td>
+            <td class="snnn capitalize green">
+              <br />
+            </td>
             <td class="snns capitalize green">
               <a href="http://lambdadelta.info/implementation.html#lddl">library</a>
             </td>
@@ -84,6 +90,7 @@
             <td class="snss capitalize green">
               <a href="http://lambdadelta.info/specification.html#v1">version 1</a>
             </td>
+            <td class="snsn capitalize green">(<a href="http://lambdadelta.info/basic_1.html">core</a>)</td>
             <td class="snsn capitalize green">(<a href="http://lambdadelta.info/static/matita/lambdadelta/">static HELM directory</a>)</td>
             <td class="snss capitalize green">
               <a href="http://lambdadelta.info/implementation.html#helena">helena</a>
@@ -97,7 +104,7 @@
     </div>
     <div xmlns:ld="http://lambdadelta.info/" class="head2dx" id="summary">Summary of the Specification <img class="icon37" alt="[spacer]" title="lambdadelta butterfly" src="http://lambdadelta.info/images/b4.png" />
     </div>
-    <div xmlns:ld="http://lambdadelta.info/" class="text">Here is a numerical acount of the specification's contents
+    <div xmlns:ld="http://lambdadelta.info/" class="text">Here is a numerical account of the specification's contents
          and its timeline.
    </div>
     <div xmlns:ld="http://lambdadelta.info/" class="text">
@@ -127,7 +134,7 @@
             <td class="snns italic cyan">files</td>
             <td class="snnn right italic cyan">30</td>
             <td class="snns italic cyan">characters</td>
-            <td class="snnn right italic cyan">68581</td>
+            <td class="snnn right italic cyan">46649</td>
             <td class="snns italic cyan">nodes</td>
             <td class="ssnn right italic cyan">62380</td>
           </tr>
@@ -290,6 +297,6 @@
     <div xmlns:ld="http://lambdadelta.info/" class="spacer">
       <br />
     </div>
-    <div xmlns:ld="http://lambdadelta.info/" class="spacer">Last update: Thu, 15 Jan 2015 16:54:45 +0100</div>
+    <div xmlns:ld="http://lambdadelta.info/" class="spacer">Last update: Sun, 18 Jan 2015 17:28:58 +0100</div>
   </body>
 </html>

diff --git a/helm/www/lambdadelta/implementation.html b/helm/www/lambdadelta/implementation.html
index b11b5b995bf77582a16d8038bff3806142e295e5..27a1d0f1bb931941c4ba327e9ee324bc4ade4aad 100644 (file)
--- a/helm/www/lambdadelta/implementation.html
+++ b/helm/www/lambdadelta/implementation.html
@@ -45,6 +45,9 @@
             <td class="snnn capitalize italic green">
               <br />
             </td>
+            <td class="snnn capitalize italic green">
+              <br />
+            </td>
             <td class="snns capitalize italic green">
               <a href="http://lambdadelta.info/implementation.html">implementation</a>
             </td>
@@ -66,6 +69,9 @@
               <a href="http://lambdadelta.info/specification.html#v2">version 2</a>
             </td>
             <td class="snnn capitalize green">(<a href="http://lambdadelta.info/ground_2.html">background</a> - <a href="http://lambdadelta.info/basic_2.html">core</a> - <a href="http://lambdadelta.info/apps_2.html">applications</a>)</td>
+            <td class="snnn capitalize green">
+              <br />
+            </td>
             <td class="snns capitalize green">
               <a href="http://lambdadelta.info/implementation.html#lddl">library</a>
             </td>
@@ -84,6 +90,7 @@
             <td class="snss capitalize green">
               <a href="http://lambdadelta.info/specification.html#v1">version 1</a>
             </td>
+            <td class="snsn capitalize green">(<a href="http://lambdadelta.info/basic_1.html">core</a>)</td>
             <td class="snsn capitalize green">(<a href="http://lambdadelta.info/static/matita/lambdadelta/">static HELM directory</a>)</td>
             <td class="snss capitalize green">
               <a href="http://lambdadelta.info/implementation.html#helena">helena</a>
@@ -248,6 +255,6 @@
     <div xmlns:ld="http://lambdadelta.info/" class="spacer">
       <br />
     </div>
-    <div xmlns:ld="http://lambdadelta.info/" class="spacer">Last update: Thu, 15 Jan 2015 16:54:44 +0100</div>
+    <div xmlns:ld="http://lambdadelta.info/" class="spacer">Last update: Sun, 18 Jan 2015 17:28:58 +0100</div>
   </body>
 </html>

diff --git a/helm/www/lambdadelta/index.html b/helm/www/lambdadelta/index.html
index 34855b0eea6b4f52951da288f303bc4703e1cd8b..d96d0d541780ba72ece099b719a5a6097f5593c9 100644 (file)
--- a/helm/www/lambdadelta/index.html
+++ b/helm/www/lambdadelta/index.html
@@ -45,6 +45,9 @@
             <td class="snnn capitalize italic green">
               <br />
             </td>
+            <td class="snnn capitalize italic green">
+              <br />
+            </td>
             <td class="snns capitalize italic green">
               <a href="http://lambdadelta.info/implementation.html">implementation</a>
             </td>
@@ -66,6 +69,9 @@
               <a href="http://lambdadelta.info/specification.html#v2">version 2</a>
             </td>
             <td class="snnn capitalize green">(<a href="http://lambdadelta.info/ground_2.html">background</a> - <a href="http://lambdadelta.info/basic_2.html">core</a> - <a href="http://lambdadelta.info/apps_2.html">applications</a>)</td>
+            <td class="snnn capitalize green">
+              <br />
+            </td>
             <td class="snns capitalize green">
               <a href="http://lambdadelta.info/implementation.html#lddl">library</a>
             </td>
@@ -84,6 +90,7 @@
             <td class="snss capitalize green">
               <a href="http://lambdadelta.info/specification.html#v1">version 1</a>
             </td>
+            <td class="snsn capitalize green">(<a href="http://lambdadelta.info/basic_1.html">core</a>)</td>
             <td class="snsn capitalize green">(<a href="http://lambdadelta.info/static/matita/lambdadelta/">static HELM directory</a>)</td>
             <td class="snss capitalize green">
               <a href="http://lambdadelta.info/implementation.html#helena">helena</a>
@@ -195,6 +202,6 @@
     <div xmlns:ld="http://lambdadelta.info/" class="spacer">
       <br />
     </div>
-    <div xmlns:ld="http://lambdadelta.info/" class="spacer">Last update: Thu, 15 Jan 2015 16:54:44 +0100</div>
+    <div xmlns:ld="http://lambdadelta.info/" class="spacer">Last update: Sun, 18 Jan 2015 17:28:58 +0100</div>
   </body>
 </html>

diff --git a/helm/www/lambdadelta/news.html b/helm/www/lambdadelta/news.html
index ebd699892fa3db81392f5e6923e33d4db9098187..ce97adae0c20715338ac71cabd166f5acd857716 100644 (file)
--- a/helm/www/lambdadelta/news.html
+++ b/helm/www/lambdadelta/news.html
@@ -45,6 +45,9 @@
             <td class="snnn capitalize italic green">
               <br />
             </td>
+            <td class="snnn capitalize italic green">
+              <br />
+            </td>
             <td class="snns capitalize italic green">
               <a href="http://lambdadelta.info/implementation.html">implementation</a>
             </td>
@@ -66,6 +69,9 @@
               <a href="http://lambdadelta.info/specification.html#v2">version 2</a>
             </td>
             <td class="snnn capitalize green">(<a href="http://lambdadelta.info/ground_2.html">background</a> - <a href="http://lambdadelta.info/basic_2.html">core</a> - <a href="http://lambdadelta.info/apps_2.html">applications</a>)</td>
+            <td class="snnn capitalize green">
+              <br />
+            </td>
             <td class="snns capitalize green">
               <a href="http://lambdadelta.info/implementation.html#lddl">library</a>
             </td>
@@ -84,6 +90,7 @@
             <td class="snss capitalize green">
               <a href="http://lambdadelta.info/specification.html#v1">version 1</a>
             </td>
+            <td class="snsn capitalize green">(<a href="http://lambdadelta.info/basic_1.html">core</a>)</td>
             <td class="snsn capitalize green">(<a href="http://lambdadelta.info/static/matita/lambdadelta/">static HELM directory</a>)</td>
             <td class="snss capitalize green">
               <a href="http://lambdadelta.info/implementation.html#helena">helena</a>
@@ -328,6 +335,6 @@
     <div xmlns:ld="http://lambdadelta.info/" class="spacer">
       <br />
     </div>
-    <div xmlns:ld="http://lambdadelta.info/" class="spacer">Last update: Fri, 16 Jan 2015 16:47:03 +0100</div>
+    <div xmlns:ld="http://lambdadelta.info/" class="spacer">Last update: Sun, 18 Jan 2015 17:28:58 +0100</div>
   </body>
 </html>

diff --git a/helm/www/lambdadelta/specification.html b/helm/www/lambdadelta/specification.html
index 043b472e1fdda1b553768912356c30d3bb34604e..21336180bd7f2188fefdb59c1704e6ceb1e62756 100644 (file)
--- a/helm/www/lambdadelta/specification.html
+++ b/helm/www/lambdadelta/specification.html
@@ -45,6 +45,9 @@
             <td class="snnn capitalize italic green">
               <br />
             </td>
+            <td class="snnn capitalize italic green">
+              <br />
+            </td>
             <td class="snns capitalize italic green">
               <a href="http://lambdadelta.info/implementation.html">implementation</a>
             </td>
@@ -66,6 +69,9 @@
               <a href="http://lambdadelta.info/specification.html#v2">version 2</a>
             </td>
             <td class="snnn capitalize green">(<a href="http://lambdadelta.info/ground_2.html">background</a> - <a href="http://lambdadelta.info/basic_2.html">core</a> - <a href="http://lambdadelta.info/apps_2.html">applications</a>)</td>
+            <td class="snnn capitalize green">
+              <br />
+            </td>
             <td class="snns capitalize green">
               <a href="http://lambdadelta.info/implementation.html#lddl">library</a>
             </td>
@@ -84,6 +90,7 @@
             <td class="snss capitalize green">
               <a href="http://lambdadelta.info/specification.html#v1">version 1</a>
             </td>
+            <td class="snsn capitalize green">(<a href="http://lambdadelta.info/basic_1.html">core</a>)</td>
             <td class="snsn capitalize green">(<a href="http://lambdadelta.info/static/matita/lambdadelta/">static HELM directory</a>)</td>
             <td class="snss capitalize green">
               <a href="http://lambdadelta.info/implementation.html#helena">helena</a>
@@ -171,6 +178,26 @@
         </tbody>
       </table>
     </div>
+    <div xmlns:ld="http://lambdadelta.info/" class="text">
+     Informational pages on the specifications are provided.
+   </div>
+    <ul xmlns:ld="http://lambdadelta.info/" id="">
+      <li>
+        <span class="emph alpha">Notice on displayed numerical acounts:</span>
+      nodes are counted according to the "intrinsic complexity measure"
+      [F. Guidi: "Procedural Representation of CIC Proof Terms"
+      Journal of Automated Reasoning 44(1-2), Springer (February 2010), pp. 53-78].       
+   </li>
+    </ul>
+    <ul xmlns:ld="http://lambdadelta.info/" id="">
+      <li>
+        <span class="emph alpha">Notice on displayed logical structures:</span>
+      from the logical standpoint, the source scripts are grouped in "planes"
+      and these are grouped in "components";
+      the notation for the relations or functions
+      introduced in each script, is shown in parentheses (? are placeholders).
+   </li>
+    </ul>
     <!-- VERSION 2 =========================================================== -->
     <div xmlns:ld="http://lambdadelta.info/" class="head3sn" id="v2">
       <img class="icon37" alt="[spacer]" title="lambdadelta butterfly" src="http://lambdadelta.info/images/b4.png" /> λδ version 2 (active)</div>
@@ -201,19 +228,6 @@
       <a href="http://lambdadelta.info/ground_2.html">Background</a>,
       <a href="http://lambdadelta.info/basic_2.html">Core</a>,
       <a href="http://lambdadelta.info/apps_2.html">Applications</a>.
-   </div>
-    <div xmlns:ld="http://lambdadelta.info/" class="text">
-      <span class="emph alpha">Notice on numerical acounts:</span>
-      nodes are counted according to the "intrinsic complexity measure"
-      [F. Guidi: "Procedural Representation of CIC Proof Terms"
-      Journal of Automated Reasoning 44(1-2), Springer (February 2010), pp. 53-78].       
-   </div>
-    <div xmlns:ld="http://lambdadelta.info/" class="text">
-      <span class="emph alpha">Notice on displayed logical structures:</span>
-      from the logical standpoint, the source scripts are grouped in "planes"
-      and these are grouped in "components";
-      the notation for the relations or functions
-      introduced in each script, is shown in parentheses (? are placeholders).
    </div>
     <!-- VERSION 1 =========================================================== -->
     <div xmlns:ld="http://lambdadelta.info/" class="head3sn" id="v1">
@@ -283,6 +297,10 @@
       <span class="emph alpha">Notice: the HELM rendering engine is offline.</span>
       </li>
     </ul>
+    <div xmlns:ld="http://lambdadelta.info/" class="text">
+      Informational pages on the parts of the specification:
+<!--      <rlink to="ground_2.html">Background</rlink>, --><a href="http://lambdadelta.info/basic_1.html">Core</a>.
+<!--      <rlink to="apps_2.html">Applications</rlink>. --></div>
     <div class="spacer">
       <img class="rule" alt="[Spacer]" title="lambdadelta rainbow rule" src="http://lambdadelta.info/images/rainbow.png" />
     </div>
@@ -309,6 +327,6 @@
     <div xmlns:ld="http://lambdadelta.info/" class="spacer">
       <br />
     </div>
-    <div xmlns:ld="http://lambdadelta.info/" class="spacer">Last update: Fri, 16 Jan 2015 16:47:03 +0100</div>
+    <div xmlns:ld="http://lambdadelta.info/" class="spacer">Last update: Sun, 18 Jan 2015 17:41:31 +0100</div>
   </body>
 </html>

diff --git a/helm/www/lambdadelta/web/home/sitemap.tbl b/helm/www/lambdadelta/web/home/sitemap.tbl
index 091a90a734dda06c14c8416c7171d1b826b8a6da..8d6b24e85cfd0a97fbaf922669ef4c33068e4ec2 100644 (file)
--- a/helm/www/lambdadelta/web/home/sitemap.tbl
+++ b/helm/www/lambdadelta/web/home/sitemap.tbl
@@ -24,6 +24,7 @@ table [
         @@("apps_2" "applications") ^ ")"
       * ]
       [ @@("specification#v1" "version 1")
+        "(" ^ @@("basic_1" "core") ^ ")"
         "(" ^ @@("static/matita/lambdadelta/" "static HELM directory") ^ ")"
       * ]
    }

diff --git a/helm/www/lambdadelta/web/home/specification.ldw.xml b/helm/www/lambdadelta/web/home/specification.ldw.xml
index 9712c9a83a58685fcfd3a679034c17deaed95fff..5c7813d8312de724f16ec869fc187f16df991a64 100644 (file)
--- a/helm/www/lambdadelta/web/home/specification.ldw.xml
+++ b/helm/www/lambdadelta/web/home/specification.ldw.xml
@@ -28,6 +28,23 @@
    </body>
    <table name="versions"/>
 
+   <body>
+     Informational pages on the specifications are provided.
+   </body>
+   <topitem>
+      <notice class="alpha" notice="Notice on displayed numerical acounts:"/>
+      nodes are counted according to the "intrinsic complexity measure"
+      [F. Guidi: "Procedural Representation of CIC Proof Terms"
+      Journal of Automated Reasoning 44(1-2), Springer (February 2010), pp. 53-78].       
+   </topitem>
+   <topitem>
+      <notice class="alpha" notice="Notice on displayed logical structures:"/>
+      from the logical standpoint, the source scripts are grouped in "planes"
+      and these are grouped in "components";
+      the notation for the relations or functions
+      introduced in each script, is shown in parentheses (? are placeholders).
+   </topitem>
+
 <!-- VERSION 2 =========================================================== -->
 
    <subsection name="v2"><version2-icon/>λδ version 2 (active)</subsection>
@@ -59,19 +76,6 @@
       <rlink to="basic_2.html">Core</rlink>,
       <rlink to="apps_2.html">Applications</rlink>.
    </body>
-   <body>
-      <notice class="alpha" notice="Notice on numerical acounts:"/>
-      nodes are counted according to the "intrinsic complexity measure"
-      [F. Guidi: "Procedural Representation of CIC Proof Terms"
-      Journal of Automated Reasoning 44(1-2), Springer (February 2010), pp. 53-78].       
-   </body>
-   <body>
-      <notice class="alpha" notice="Notice on displayed logical structures:"/>
-      from the logical standpoint, the source scripts are grouped in "planes"
-      and these are grouped in "components";
-      the notation for the relations or functions
-      introduced in each script, is shown in parentheses (? are placeholders).
-   </body>
 
 <!-- VERSION 1 =========================================================== -->
 
@@ -130,5 +134,12 @@
       <notice class="alpha" notice="Notice: the HELM rendering engine is offline."/>
    </topitem>
 
+   <body>
+      Informational pages on the parts of the specification:
+<!--      <rlink to="ground_2.html">Background</rlink>, -->
+      <rlink to="basic_1.html">Core</rlink>.
+<!--      <rlink to="apps_2.html">Applications</rlink>. -->
+   </body>
+
    <footer/>
 </page>

diff --git a/matita/matita/contribs/lambdadelta/apps_2/web/apps_2.ldw.xml b/matita/matita/contribs/lambdadelta/apps_2/web/apps_2.ldw.xml
index dada75abda7b38e11af837a4401ee4a6aca8873f..027c6b1d9ae42ddbbea1cfa55d38ef8741b984be 100644 (file)
--- a/matita/matita/contribs/lambdadelta/apps_2/web/apps_2.ldw.xml
+++ b/matita/matita/contribs/lambdadelta/apps_2/web/apps_2.ldw.xml
@@ -24,7 +24,7 @@
    </topitem>
 
    <section4 name="summary">Summary of the Specification</section4>
-   <body>Here is a numerical acount of the specification's contents
+   <body>Here is a numerical account of the specification's contents
          and its timeline.
    </body>
    <table name="apps_2_sum"/>

diff --git a/matita/matita/contribs/lambdadelta/apps_2/web/apps_2_src.tbl b/matita/matita/contribs/lambdadelta/apps_2/web/apps_2_src.tbl
index 29d687e7f494b147524581219dd6e12af79cc169..9a19a7715e1ed7b7fbd743581df32008a9493801 100644 (file)
--- a/matita/matita/contribs/lambdadelta/apps_2/web/apps_2_src.tbl
+++ b/matita/matita/contribs/lambdadelta/apps_2/web/apps_2_src.tbl
@@ -13,7 +13,7 @@ table {
    class "orange"
    [ { "MLTT1" * } {
         [ { "" * } {
-             [ "genv_primitive" "judgement" * ]
+             [ "genv_primitive" "judgment" * ]
           }
         ]
      }

diff --git a/matita/matita/contribs/lambdadelta/basic_2/web/basic_2.ldw.xml b/matita/matita/contribs/lambdadelta/basic_2/web/basic_2.ldw.xml
index 6b5037b8554376e6edfb40aeb51a2822c4ef9816..93b218306e06c7ad5155beec47dc471d36d0ac88 100644 (file)
--- a/matita/matita/contribs/lambdadelta/basic_2/web/basic_2.ldw.xml
+++ b/matita/matita/contribs/lambdadelta/basic_2/web/basic_2.ldw.xml
@@ -20,7 +20,7 @@
 -->
 
    <section4 name="summary">Summary of the Specification</section4>
-   <body>Here is a numerical acount of the specification's contents
+   <body>Here is a numerical account of the specification's contents
          and its timeline.
    </body>
    <table name="basic_2_sum"/>
@@ -49,7 +49,7 @@
    </news>
    <news class="alpha" date="2014 April 16.">
          Lazy equivalence on local environments
-        addded as q-step to rst-computation on closures
+        added as q-step to rst-computation on closures
          (anniversary milestone).
    </news>
    <news class="alpha" date="2014 January 20.">

diff --git a/matita/matita/contribs/lambdadelta/basic_2/web/basic_2_src.tbl b/matita/matita/contribs/lambdadelta/basic_2/web/basic_2_src.tbl
index 0714b94ecefc1e3baf1d2872d2a5004452fb1b36..fe54a52feb9631a7dfe318ce43a7204561d6fc65 100644 (file)
--- a/matita/matita/contribs/lambdadelta/basic_2/web/basic_2_src.tbl
+++ b/matita/matita/contribs/lambdadelta/basic_2/web/basic_2_src.tbl
@@ -229,7 +229,7 @@ table {
              [ "frees ( ? ⊢ ? ϵ 𝐅*[?]⦃?⦄ )" "frees_append" + "frees_lreq" + "frees_lift" * ]
           }
         ]
-        [ { "contxt-sensitive multiple rt-substitution" * } {
+        [ { "context-sensitive multiple rt-substitution" * } {
              [ "cpys ( ⦃?,?⦄ ⊢ ? ▶*[?,?] ? )" "cpys_alt ( ⦃?,?⦄ ⊢ ? ▶▶*[?,?] ? )" "cpys_lift" + "cpys_cpys" * ]
           }
         ]
@@ -264,7 +264,7 @@ table {
              [ "gget ( ⬇[?] ? ≡ ? )" "gget_gget" * ]
           }
         ]
-        [ { "contxt-sensitive ordinary rt-substitution" * } {
+        [ { "context-sensitive ordinary rt-substitution" * } {
              [ "cpy ( ⦃?,?⦄ ⊢ ? ▶[?,?] ? )" "cpy_lift" + "cpy_nlift" + "cpy_cpy" * ]
           }
         ]

diff --git a/matita/matita/contribs/lambdadelta/ground_2/web/ground_2.ldw.xml b/matita/matita/contribs/lambdadelta/ground_2/web/ground_2.ldw.xml
index 9c79f972cc8cace2043141b0df286092a8556d41..af06ffa1df8fb992de2d578758cfd5e087a657ab 100644 (file)
--- a/matita/matita/contribs/lambdadelta/ground_2/web/ground_2.ldw.xml
+++ b/matita/matita/contribs/lambdadelta/ground_2/web/ground_2.ldw.xml
@@ -8,7 +8,7 @@
    <sitemap name="sitemap"/>
 
    <section4 name="summary">Summary of the Specification</section4>
-   <body>Here is a numerical acount of the specification's contents
+   <body>Here is a numerical account of the specification's contents
          and its timeline.
    </body>
    <table name="ground_2_sum"/>