From: Ferruccio Guidi <ferruccio.guidi@unibo.it>
Date: Sun, 27 Mar 2016 16:43:13 +0000 (+0000)
Subject: update in basic_2 and apps_2 ...
X-Git-Tag: make_still_working~621
X-Git-Url: http://matita.cs.unibo.it/gitweb/?p=helm.git;a=commitdiff_plain;h=560e9f41516968588e97bb6ff2049f85a425ac0a

update in basic_2 and apps_2 ...
---

diff --git a/helm/www/lambdadelta/BTM.html b/helm/www/lambdadelta/BTM.html
index 2756b021e..8202086a4 100644
--- 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, 10 Dec 2015 16:13:46 +0100</div>
+    <div xmlns:ld="http://lambdadelta.info/" class="spacer">Last update: Sun, 27 Mar 2016 18:42:30 +0200</div>
   </body>
 </html>
diff --git a/helm/www/lambdadelta/apps_2.html b/helm/www/lambdadelta/apps_2.html
index e6a410d40..35fdff6e8 100644
--- a/helm/www/lambdadelta/apps_2.html
+++ b/helm/www/lambdadelta/apps_2.html
@@ -152,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">1</td>
             <td class="snns italic cyan">characters</td>
-            <td class="snnn right italic cyan">68581</td>
+            <td class="snnn right italic cyan">217</td>
             <td class="snns italic cyan">nodes</td>
-            <td class="ssnn right italic cyan">3637</td>
+            <td class="ssnn right italic cyan">0</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="snnn right italic green">0</td>
             <td class="snns italic green">lemmas</td>
-            <td class="snnn right italic green">1</td>
+            <td class="snnn right italic green">0</td>
             <td class="snns italic green">total</td>
-            <td class="ssnn right italic green">3</td>
+            <td class="ssnn right italic green">0</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">0</td>
             <td class="snss italic yellow">defined</td>
-            <td class="snsn right italic yellow">9</td>
+            <td class="snsn right italic yellow">0</td>
             <td class="snss italic yellow">total</td>
-            <td class="sssn right italic yellow">12</td>
+            <td class="sssn right italic yellow">0</td>
           </tr>
         </tbody>
       </table>
@@ -258,6 +258,6 @@
     <div xmlns:ld="http://lambdadelta.info/" class="spacer">
       <br />
     </div>
-    <div xmlns:ld="http://lambdadelta.info/" class="spacer">Last update: Thu, 10 Dec 2015 16:13:46 +0100</div>
+    <div xmlns:ld="http://lambdadelta.info/" class="spacer">Last update: Sun, 27 Mar 2016 18:42:29 +0200</div>
   </body>
 </html>
diff --git a/helm/www/lambdadelta/basic_1.html b/helm/www/lambdadelta/basic_1.html
index 9e83dd9e2..789062b5c 100644
--- a/helm/www/lambdadelta/basic_1.html
+++ b/helm/www/lambdadelta/basic_1.html
@@ -823,6 +823,6 @@
     <div xmlns:ld="http://lambdadelta.info/" class="spacer">
       <br />
     </div>
-    <div xmlns:ld="http://lambdadelta.info/" class="spacer">Last update: Fri, 04 Mar 2016 16:15:59 +0100</div>
+    <div xmlns:ld="http://lambdadelta.info/" class="spacer">Last update: Sun, 27 Mar 2016 18:42:29 +0200</div>
   </body>
 </html>
diff --git a/helm/www/lambdadelta/basic_2.html b/helm/www/lambdadelta/basic_2.html
index 1b36b571e..4003948a1 100644
--- a/helm/www/lambdadelta/basic_2.html
+++ b/helm/www/lambdadelta/basic_2.html
@@ -144,29 +144,29 @@
           <tr>
             <td class="snns capitalize italic cyan">sizes</td>
             <td class="snns italic cyan">files</td>
-            <td class="snnn right italic cyan">360</td>
+            <td class="snnn right italic cyan">83</td>
             <td class="snns italic cyan">characters</td>
-            <td class="snnn right italic cyan">437272</td>
+            <td class="snnn right italic cyan">55955</td>
             <td class="snns italic cyan">nodes</td>
-            <td class="ssnn right italic cyan">1935835</td>
+            <td class="ssnn right italic cyan">191279</td>
           </tr>
           <tr>
             <td class="snns capitalize italic green">propositions</td>
             <td class="snns italic green">theorems</td>
-            <td class="snnn right italic green">130</td>
+            <td class="snnn right italic green">33</td>
             <td class="snns italic green">lemmas</td>
-            <td class="snnn right italic green">1303</td>
+            <td class="snnn right italic green">211</td>
             <td class="snns italic green">total</td>
-            <td class="ssnn right italic green">1433</td>
+            <td class="ssnn right italic green">244</td>
           </tr>
           <tr>
             <td class="snss capitalize italic yellow">concepts</td>
             <td class="snss italic yellow">declared</td>
-            <td class="snsn right italic yellow">54</td>
+            <td class="snsn right italic yellow">15</td>
             <td class="snss italic yellow">defined</td>
-            <td class="snsn right italic yellow">89</td>
+            <td class="snsn right italic yellow">23</td>
             <td class="snss italic yellow">total</td>
-            <td class="sssn right italic yellow">143</td>
+            <td class="sssn right italic yellow">38</td>
           </tr>
         </tbody>
       </table>
@@ -179,11 +179,24 @@
          for native type assignment.
    </li>
     </ul>
-    <div xmlns:ld="http://lambdadelta.info/" class="head3sn" id="A">Stage "A": "Extending the Applicability Condition"</div>
+    <div xmlns:ld="http://lambdadelta.info/" class="head3sn" id="A2">Stage "A2": "Extending the Applicability Condition"</div>
+    <ul xmlns:ld="http://lambdadelta.info/">
+      <li>
+        <span class="emph alpha">2015 October 9.</span>
+         λδ version 2A2 is started.
+   </li>
+    </ul>
+    <div xmlns:ld="http://lambdadelta.info/" class="head3sn" id="A1">Stage "A1": "Extending the Applicability Condition"</div>
+    <ul xmlns:ld="http://lambdadelta.info/">
+      <li>
+        <span class="emph delta">2015 August 27.</span>
+         λδ version 2A1 appears too complex and is dismissed.
+   </li>
+    </ul>
     <ul xmlns:ld="http://lambdadelta.info/">
       <li>
         <span class="emph gamma">2014 October 28.</span>
-         λδ version 2A is released.
+         λδ version 2A1 is released.
    </li>
     </ul>
     <ul xmlns:ld="http://lambdadelta.info/">
@@ -305,7 +318,7 @@
     <ul xmlns:ld="http://lambdadelta.info/">
       <li>
         <span class="emph alpha">2011 April 17.</span>
-         Specification starts.
+         λδ version 2 is started.
    </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/b4.png" />
@@ -330,626 +343,10 @@
             </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">ex_sta_ldec ex_cpr_omega ex_fpbg_refl ex_snv_eta</td>
-            <td class="snnn top wine">
-              <br />
-            </td>
-            <td class="snnn top wine">
-              <br />
-            </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="snnn top magenta">
-              <br />
-            </td>
-            <td class="snnn top magenta">
-              <br />
-            </td>
-            <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">local env. ref. for stratified native validity</td>
-            <td class="snns top prune">lsubsv ( ? ⊢ ? ⫃¡[?,?] ? )</td>
-            <td class="snnn top prune">lsubsv_lsuba lsubsv_lsubd lsubsv_lstas lsubsv_scpds lsubsv_cpcs lsubsv_snv</td>
-            <td class="snnn top prune">
-              <br />
-            </td>
-            <td class="ssnn top prune">
-              <br />
-            </td>
-          </tr>
-          <tr>
-            <td class="nnns top capitalize italic prune">
-              <br />
-            </td>
-            <td class="snns top italic prune">stratified native validity</td>
-            <td class="snns top prune">shnv ( ⦃?,?⦄ ⊢ ? ¡[?,?,?] )</td>
-            <td class="snnn top prune">
-              <br />
-            </td>
-            <td class="snnn top prune">
-              <br />
-            </td>
-            <td class="ssnn top prune">
-              <br />
-            </td>
-          </tr>
-          <tr>
-            <td class="nnns top capitalize italic prune">
-              <br />
-            </td>
-            <td class="nnns top italic prune">
-              <br />
-            </td>
-            <td class="snns top prune">snv ( ⦃?,?⦄ ⊢ ? ¡[?,?] )</td>
-            <td class="snnn top prune">snv_lift snv_aaa snv_da_lpr snv_lstas snv_lstas_lpr snv_lpr snv_fsb snv_scpes snv_preserve</td>
-            <td class="snnn top prune">
-              <br />
-            </td>
-            <td class="ssnn top prune">
-              <br />
-            </td>
-          </tr>
-          <tr>
-            <td class="snns top capitalize italic blue">equivalence</td>
-            <td class="snns top italic blue">decomposed rt-equivalence</td>
-            <td class="snns top blue">scpes ( ⦃?,?⦄ ⊢ ? •*⬌*[?,?,?,?] ? )</td>
-            <td class="snnn top blue">scpes_aaa scpes_cpcs scpes_scpes</td>
-            <td class="snnn top blue">
-              <br />
-            </td>
-            <td class="ssnn top blue">
-              <br />
-            </td>
-          </tr>
-          <tr>
-            <td class="nnns top capitalize italic blue">
-              <br />
-            </td>
-            <td class="snns top italic blue">context-sensitive equivalence</td>
-            <td class="snns top blue">cpcs ( ⦃?,?⦄ ⊢ ? ⬌* ? )</td>
-            <td class="snnn top blue">cpcs_aaa cpcs_cprs cpcs_cpcs</td>
-            <td class="snnn top blue">
-              <br />
-            </td>
-            <td class="ssnn top blue">
-              <br />
-            </td>
-          </tr>
-          <tr>
-            <td class="snns top capitalize italic sky">conversion</td>
-            <td class="snns top italic sky">context-sensitive conversion</td>
-            <td class="snns top sky">cpc ( ⦃?,?⦄ ⊢ ? ⬌ ? )</td>
-            <td class="snnn top sky">cpc_cpc</td>
-            <td class="snnn top sky">
-              <br />
-            </td>
-            <td class="ssnn top sky">
-              <br />
-            </td>
-          </tr>
-          <tr>
-            <td class="snns top capitalize italic cyan">computation</td>
-            <td class="snns top italic cyan">evaluation for context-sensitive rt-reduction</td>
-            <td class="snns top cyan">cpxe ( ⦃?,?⦄ ⊢ ➡*[?,?] 𝐍⦃?⦄ )</td>
-            <td class="snnn top cyan">
-              <br />
-            </td>
-            <td class="snnn top cyan">
-              <br />
-            </td>
-            <td class="ssnn top cyan">
-              <br />
-            </td>
-          </tr>
-          <tr>
-            <td class="nnns top capitalize italic cyan">
-              <br />
-            </td>
-            <td class="snns top italic cyan">evaluation for context-sensitive reduction</td>
-            <td class="snns top cyan">cpre ( ⦃?,?⦄ ⊢ ➡* 𝐍⦃?⦄ )</td>
-            <td class="snnn top cyan">cpre_cpre</td>
-            <td class="snnn top cyan">
-              <br />
-            </td>
-            <td class="ssnn top cyan">
-              <br />
-            </td>
-          </tr>
-          <tr>
-            <td class="nnns top capitalize italic cyan">
-              <br />
-            </td>
-            <td class="snns top italic cyan">strongly normalizing qrst-computation</td>
-            <td class="snns top cyan">fsb ( ⦥[?,?] ⦃?,?,?⦄ )</td>
-            <td class="snnn top cyan">fsb_alt ( ⦥⦥[?,?] ⦃?,?,?⦄ )</td>
-            <td class="snnn top cyan">fsb_aaa fsb_csx</td>
-            <td class="ssnn top cyan">
-              <br />
-            </td>
-          </tr>
-          <tr>
-            <td class="nnns top capitalize italic cyan">
-              <br />
-            </td>
-            <td class="snns top italic cyan">strongly normalizing rt-computation</td>
-            <td class="snns top cyan">lcosx ( ? ⊢ ~⬊*[?,?,?] ? )</td>
-            <td class="snnn top cyan">lcosx_cpx</td>
-            <td class="snnn top cyan">
-              <br />
-            </td>
-            <td class="ssnn top cyan">
-              <br />
-            </td>
-          </tr>
-          <tr>
-            <td class="nnns top capitalize italic cyan">
-              <br />
-            </td>
-            <td class="nnns top italic cyan">
-              <br />
-            </td>
-            <td class="snns top cyan">lsx ( ? ⊢ ⬊*[?,?,?,?] ? )</td>
-            <td class="snnn top cyan">lsx_alt ( ? ⊢ ⬊⬊*[?,?,?,?] ? )</td>
-            <td class="snnn top cyan">lsx_drop lsx_lpx lsx_lpxs llsx_csx</td>
-            <td class="ssnn top cyan">
-              <br />
-            </td>
-          </tr>
-          <tr>
-            <td class="nnns top capitalize italic cyan">
-              <br />
-            </td>
-            <td class="nnns top italic cyan">
-              <br />
-            </td>
-            <td class="snns top cyan">csx_vector ( ⦃?,?⦄ ⊢ ⬊*[?,?] ? )</td>
-            <td class="snnn top cyan">csx_tsts_vector csx_aaa</td>
-            <td class="snnn top cyan">
-              <br />
-            </td>
-            <td class="ssnn top cyan">
-              <br />
-            </td>
-          </tr>
-          <tr>
-            <td class="nnns top capitalize italic cyan">
-              <br />
-            </td>
-            <td class="nnns top italic cyan">
-              <br />
-            </td>
-            <td class="snns top cyan">csx ( ⦃?,?⦄ ⊢ ⬊*[?,?] ? )</td>
-            <td class="snnn top cyan">csx_alt ( ⦃?,?⦄ ⊢ ⬊⬊*[?,?] ? )</td>
-            <td class="snnn top cyan">csx_lift csx_lleq csx_lpx csx_lpxs csx_fpbs</td>
-            <td class="ssnn top cyan">
-              <br />
-            </td>
-          </tr>
-          <tr>
-            <td class="nnns top capitalize italic cyan">
-              <br />
-            </td>
-            <td class="snns top italic cyan">parallel qrst-computation</td>
-            <td class="snns top cyan">fpbg ( ⦃?,?,?⦄ &gt;≡[?,?] ⦃?,?,?⦄ )</td>
-            <td class="snnn top cyan">fpbg_lift fpbg_fleq fpbg_fpbs fpbg_fpbg</td>
-            <td class="snnn top cyan">
-              <br />
-            </td>
-            <td class="ssnn top cyan">
-              <br />
-            </td>
-          </tr>
-          <tr>
-            <td class="nnns top capitalize italic cyan">
-              <br />
-            </td>
-            <td class="nnns top italic cyan">
-              <br />
-            </td>
-            <td class="snns top cyan">fpbs ( ⦃?,?,?⦄ ≥[?,?] ⦃?,?,?⦄ )</td>
-            <td class="snnn top cyan">fpbs_alt ( ⦃?,?,?⦄ ≥≥[?,?] ⦃?,?,?⦄ )</td>
-            <td class="snnn top cyan">fpbs_lift fpbs_aaa fpbs_fpb fpbs_fpbs</td>
-            <td class="ssnn top cyan">
-              <br />
-            </td>
-          </tr>
-          <tr>
-            <td class="nnns top capitalize italic cyan">
-              <br />
-            </td>
-            <td class="snns top italic cyan">decomposed rt-computation</td>
-            <td class="snns top cyan">scpds ( ⦃?,?⦄ ⊢ ? •*➡*[?,?,?] ? )</td>
-            <td class="snnn top cyan">scpds_lift scpds_aaa scpds_scpds</td>
-            <td class="snnn top cyan">
-              <br />
-            </td>
-            <td class="ssnn top cyan">
-              <br />
-            </td>
-          </tr>
-          <tr>
-            <td class="nnns top capitalize italic cyan">
-              <br />
-            </td>
-            <td class="snns top italic cyan">context-sensitive rt-computation</td>
-            <td class="snns top cyan">lpxs ( ⦃?,?⦄ ⊢ ➡*[?,?] ? )</td>
-            <td class="snnn top cyan">lpxs_drop lpxs_lleq lpxs_aaa lpxs_cpxs lpxs_lpxs</td>
-            <td class="snnn top cyan">
-              <br />
-            </td>
-            <td class="ssnn top cyan">
-              <br />
-            </td>
-          </tr>
-          <tr>
-            <td class="nnns top capitalize italic cyan">
-              <br />
-            </td>
-            <td class="nnns top italic cyan">
-              <br />
-            </td>
-            <td class="snns top cyan">cpxs ( ⦃?,?⦄ ⊢ ? ➡*[?,?] ? )</td>
-            <td class="snnn top cyan">cpxs_tsts cpxs_tsts_vector cpxs_lreq cpxs_lift cpxs_lleq cpxs_aaa cpxs_cpxs</td>
-            <td class="snnn top cyan">
-              <br />
-            </td>
-            <td class="ssnn top cyan">
-              <br />
-            </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">lprs ( ⦃?,?⦄ ⊢ ➡* ? )</td>
-            <td class="snnn top cyan">lprs_drop lprs_cprs lprs_lprs</td>
-            <td class="snnn top cyan">
-              <br />
-            </td>
-            <td class="ssnn top cyan">
-              <br />
-            </td>
-          </tr>
-          <tr>
-            <td class="nnns top capitalize italic cyan">
-              <br />
-            </td>
-            <td class="nnns top italic cyan">
-              <br />
-            </td>
-            <td class="snns top cyan">cprs ( ⦃?,?⦄ ⊢ ? ➡* ?)</td>
-            <td class="snnn top cyan">cprs_lift cprs_cprs</td>
-            <td class="snnn top cyan">
-              <br />
-            </td>
-            <td class="ssnn top cyan">
-              <br />
-            </td>
-          </tr>
-          <tr>
-            <td class="nnns top capitalize italic cyan">
-              <br />
-            </td>
-            <td class="snns top italic cyan">local env. ref. for generic reducibility</td>
-            <td class="snns top cyan">lsubc ( ? ⊢ ? ⫃[?] ? )</td>
-            <td class="snnn top cyan">lsubc_drop lsubc_drops lsubc_lsuba</td>
-            <td class="snnn top cyan">
-              <br />
-            </td>
-            <td class="ssnn top cyan">
-              <br />
-            </td>
-          </tr>
-          <tr>
-            <td class="nnns top capitalize italic cyan">
-              <br />
-            </td>
-            <td class="snns top italic cyan">support for generic computation properties</td>
-            <td class="snns top cyan">gcp</td>
-            <td class="snnn top cyan">gcp_cr ( ⦃?,?,?⦄ ϵ[?] 〚?〛 )</td>
-            <td class="snnn top cyan">gcp_aaa</td>
-            <td class="ssnn top cyan">
-              <br />
-            </td>
-          </tr>
-          <tr>
-            <td class="snns top capitalize italic water">reduction</td>
-            <td class="snns top italic water">parallel qrst-reduction</td>
-            <td class="snns top water">fpbq ( ⦃?,?,?⦄ ≽[?,?] ⦃?,?,?⦄ )</td>
-            <td class="snnn top water">fpbq_alt ( ⦃?,?,?⦄ ≽≽[?,?] ⦃?,?,?⦄ )</td>
-            <td class="snnn top water">fpbq_lift fpbq_aaa</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">fpb ( ⦃?,?,?⦄ ≻[?,?] ⦃?,?,?⦄ )</td>
-            <td class="snnn top water">fpb_lift fpb_lleq fpb_fleq</td>
-            <td class="snnn top water">
-              <br />
-            </td>
-            <td class="ssnn top water">
-              <br />
-            </td>
-          </tr>
-          <tr>
-            <td class="nnns top capitalize italic water">
-              <br />
-            </td>
-            <td class="snns top italic water">normal forms for context-sensitive rt-reduction</td>
-            <td class="snns top water">cnx ( ⦃?,?⦄ ⊢ ➡[?,?] 𝐍⦃?⦄ )</td>
-            <td class="snnn top water">cnx_lift cnx_crx cnx_cix</td>
-            <td class="snnn top water">
-              <br />
-            </td>
-            <td class="ssnn top water">
-              <br />
-            </td>
-          </tr>
-          <tr>
-            <td class="nnns top capitalize italic water">
-              <br />
-            </td>
-            <td class="snns top italic water">context-sensitive rt-reduction</td>
-            <td class="snns top water">lpx ( ⦃?,?⦄ ⊢ ➡[?,?] ? )</td>
-            <td class="snnn top water">lpx_drop lpx_frees lpx_lleq lpx_aaa</td>
-            <td class="snnn top water">
-              <br />
-            </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">cpx ( ⦃?,?⦄ ⊢ ? ➡[?,?] ? )</td>
-            <td class="snnn top water">cpx_lreq cpx_lift cpx_llpx_sn cpx_lleq cpx_cix</td>
-            <td class="snnn top water">
-              <br />
-            </td>
-            <td class="ssnn top water">
-              <br />
-            </td>
-          </tr>
-          <tr>
-            <td class="nnns top capitalize italic water">
-              <br />
-            </td>
-            <td class="snns top italic water">irreducible forms for context-sensitive rt-reduction</td>
-            <td class="snns top water">cix ( ⦃?,?⦄ ⊢ ➡[?,?] 𝐈⦃?⦄ )</td>
-            <td class="snnn top water">cix_lift</td>
-            <td class="snnn top water">
-              <br />
-            </td>
-            <td class="ssnn top water">
-              <br />
-            </td>
-          </tr>
-          <tr>
-            <td class="nnns top capitalize italic water">
-              <br />
-            </td>
-            <td class="snns top italic water">reducible forms for context-sensitive rt-reduction</td>
-            <td class="snns top water">crx ( ⦃?,?⦄ ⊢ ➡[?,?] 𝐑⦃?⦄ )</td>
-            <td class="snnn top water">crx_lift</td>
-            <td class="snnn top water">
-              <br />
-            </td>
-            <td class="ssnn top water">
-              <br />
-            </td>
-          </tr>
-          <tr>
-            <td class="nnns top capitalize italic water">
-              <br />
-            </td>
-            <td class="snns top italic water">normal forms for context-sensitive reduction</td>
-            <td class="snns top water">cnr ( ⦃?,?⦄ ⊢ ➡ 𝐍⦃?⦄ )</td>
-            <td class="snnn top water">cnr_lift cnr_crr cnr_cir</td>
-            <td class="snnn top water">
-              <br />
-            </td>
-            <td class="ssnn top water">
-              <br />
-            </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">lpr ( ⦃?,?⦄ ⊢ ➡ ? )</td>
-            <td class="snnn top water">lpr_drop lpr_lpr</td>
-            <td class="snnn top water">
-              <br />
-            </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">cpr ( ⦃?,?⦄ ⊢ ? ➡ ? )</td>
-            <td class="snnn top water">cpr_lift cpr_llpx_sn cpr_cir</td>
-            <td class="snnn top water">
-              <br />
-            </td>
-            <td class="ssnn top water">
-              <br />
-            </td>
-          </tr>
-          <tr>
-            <td class="nnns top capitalize italic water">
-              <br />
-            </td>
-            <td class="snns top italic water">irreducible forms for context-sensitive reduction</td>
-            <td class="snns top water">cir ( ⦃?,?⦄ ⊢ ➡ 𝐈⦃?⦄ )</td>
-            <td class="snnn top water">cir_lift</td>
-            <td class="snnn top water">
-              <br />
-            </td>
-            <td class="ssnn top water">
-              <br />
-            </td>
-          </tr>
-          <tr>
-            <td class="nnns top capitalize italic water">
-              <br />
-            </td>
-            <td class="snns top italic water">reducible forms for context-sensitive reduction</td>
-            <td class="snns top water">crr ( ⦃?,?⦄ ⊢ ➡ 𝐑⦃?⦄ )</td>
-            <td class="snnn top water">crr_lift</td>
-            <td class="snnn top water">
-              <br />
-            </td>
-            <td class="ssnn top water">
-              <br />
-            </td>
-          </tr>
-          <tr>
-            <td class="snns top capitalize italic green">unfold</td>
-            <td class="snns top italic green">unfold</td>
-            <td class="snns top green">unfold ( ⦃?,?⦄ ⊢ ? ⧫* ? )</td>
-            <td class="snnn top green">
-              <br />
-            </td>
-            <td class="snnn top green">
-              <br />
-            </td>
-            <td class="ssnn top green">
-              <br />
-            </td>
-          </tr>
-          <tr>
-            <td class="nnns top capitalize italic green">
-              <br />
-            </td>
-            <td class="snns top italic green">iterated static type assignment</td>
-            <td class="snns top green">lstas ( ⦃?,?⦄ ⊢ ? •*[?,?] ? )</td>
-            <td class="snnn top green">lstas_lift lstas_llpx_sn.ma lstas_aaa lstas_da lstas_lstas</td>
-            <td class="snnn top green">
-              <br />
-            </td>
-            <td class="ssnn top green">
-              <br />
-            </td>
-          </tr>
-          <tr>
-            <td class="snns top capitalize italic grass">static typing</td>
-            <td class="snns top italic grass">local env. ref. for degree assignment</td>
-            <td class="snns top grass">lsubd ( ? ⊢ ? ⫃▪[?,?] ? )</td>
-            <td class="snnn top grass">lsubd_da lsubd_lsubd</td>
-            <td class="snnn top grass">
-              <br />
-            </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">degree assignment</td>
-            <td class="snns top grass">da ( ⦃?,?⦄ ⊢ ? ▪[?,?] ? )</td>
-            <td class="snnn top grass">da_lift da_aaa da_da</td>
-            <td class="snnn top grass">
-              <br />
-            </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">sh</td>
-            <td class="snnn top grass">sd</td>
-            <td class="snnn top grass">
-              <br />
-            </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">local env. ref. for atomic arity assignment</td>
-            <td class="snns top grass">lsuba ( ? ⊢ ? ⫃⁝ ? )</td>
-            <td class="snnn top grass">lsuba_aaa lsuba_lsuba</td>
-            <td class="snnn top grass">
-              <br />
-            </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">atomic arity assignment</td>
-            <td class="snns top grass">aaa ( ⦃?,?⦄ ⊢ ? ⁝ ? )</td>
-            <td class="snnn top grass">aaa_lift aaa_lifts aaa_fqus aaa_lleq aaa_aaa</td>
-            <td class="snnn top grass">
-              <br />
-            </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">restricted local env. ref.</td>
-            <td class="snns top grass">lsubr ( ? ⫃ ? )</td>
-            <td class="snnn top grass">lsubr_lsubr</td>
-            <td class="snnn top grass">
-              <br />
-            </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">lazy equivalence</td>
-            <td class="snns top yellow">fleq ( ⦃?,?,?⦄ ≡[?] ⦃?,?,?⦄ )</td>
-            <td class="snnn top yellow">fleq_fleq</td>
+            <td class="snns top capitalize italic yellow">relocation</td>
+            <td class="snns top italic yellow">ranged equivalence for closures</td>
+            <td class="snns top yellow">freq ( ⦃?,?,?⦄ ≡ ⦃?,?,?⦄ )</td>
+            <td class="snnn top yellow">freq_freq</td>
             <td class="snnn top yellow">
               <br />
             </td>
@@ -961,11 +358,9 @@
             <td class="nnns top capitalize italic yellow">
               <br />
             </td>
-            <td class="nnns top italic yellow">
-              <br />
-            </td>
-            <td class="snns top yellow">lleq ( ? ≡[?,?] ? )</td>
-            <td class="snnn top yellow">lleq_alt lleq_alt_rec lleq_lreq lleq_drop lleq_fqus lleq_llor lleq_lleq</td>
+            <td class="snns top italic yellow">context-sensitive free variables</td>
+            <td class="snns top yellow">frees ( ? ⊢ 𝐅*⦃?⦄ ≡ ? )</td>
+            <td class="snnn top yellow">frees_weight frees_lreq frees_frees</td>
             <td class="snnn top yellow">
               <br />
             </td>
@@ -977,63 +372,11 @@
             <td class="nnns top capitalize italic yellow">
               <br />
             </td>
-            <td class="snns top italic yellow">lazy pointwise extension of a relation</td>
-            <td class="snns top yellow">llpx_sn</td>
-            <td class="snnn top yellow">llpx_sn_alt llpx_sn_alt_rec llpx_sn_tc llpx_sn_lreq llpx_sn_drop llpx_sn_lpx_sn llpx_sn_frees llpx_sn_llor</td>
+            <td class="snns top italic yellow">generic slicing for local environments</td>
+            <td class="snns top yellow">drops_vector ( ⬇*[?,?] ? ≡ ? )</td>
             <td class="snnn top yellow">
               <br />
             </td>
-            <td class="ssnn top yellow">
-              <br />
-            </td>
-          </tr>
-          <tr>
-            <td class="nnns top capitalize italic yellow">
-              <br />
-            </td>
-            <td class="snns top italic yellow">pointwise union for local environments</td>
-            <td class="snns top yellow">llor ( ? ⋓[?,?] ? ≡ ? )</td>
-            <td class="snnn top yellow">llor_alt llor_drop</td>
-            <td class="snnn top yellow">
-              <br />
-            </td>
-            <td class="ssnn top yellow">
-              <br />
-            </td>
-          </tr>
-          <tr>
-            <td class="nnns top capitalize italic yellow">
-              <br />
-            </td>
-            <td class="snns top italic yellow">context-sensitive exclusion from free variables</td>
-            <td class="snns top yellow">frees ( ? ⊢ ? ϵ 𝐅*[?]⦃?⦄ )</td>
-            <td class="snnn top yellow">frees_append frees_lreq frees_lift</td>
-            <td class="snnn top yellow">
-              <br />
-            </td>
-            <td class="ssnn top yellow">
-              <br />
-            </td>
-          </tr>
-          <tr>
-            <td class="nnns top capitalize italic yellow">
-              <br />
-            </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>
-            <td class="ssnn top yellow">
-              <br />
-            </td>
-          </tr>
-          <tr>
-            <td class="nnns top capitalize italic yellow">
-              <br />
-            </td>
-            <td class="snns top italic yellow">iterated structural successor for closures</td>
-            <td class="snns top yellow">fqus ( ⦃?,?,?⦄ ⊐* ⦃?,?,?⦄ )</td>
-            <td class="snnn top yellow">fqus_alt fqus_fqus</td>
             <td class="snnn top yellow">
               <br />
             </td>
@@ -1048,22 +391,8 @@
             <td class="nnns top italic yellow">
               <br />
             </td>
-            <td class="snns top yellow">fqup ( ⦃?,?,?⦄ ⊐+ ⦃?,?,?⦄ )</td>
-            <td class="snnn top yellow">fqup_fqup</td>
-            <td class="snnn top yellow">
-              <br />
-            </td>
-            <td class="ssnn top yellow">
-              <br />
-            </td>
-          </tr>
-          <tr>
-            <td class="nnns top capitalize italic yellow">
-              <br />
-            </td>
-            <td class="snns top italic yellow">iterated local env. slicing</td>
             <td class="snns top yellow">drops ( ⬇*[?,?] ? ≡ ? )</td>
-            <td class="snnn top yellow">drops_drop drops_drops</td>
+            <td class="snnn top yellow">drops_lstar drops_weight drops_length drops_ceq drops_lexs drops_lreq drops_drops</td>
             <td class="snnn top yellow">
               <br />
             </td>
@@ -1075,7 +404,7 @@
             <td class="nnns top capitalize italic yellow">
               <br />
             </td>
-            <td class="snns top italic yellow">generic term relocation</td>
+            <td class="snns top italic yellow">generic relocation for terms</td>
             <td class="snns top yellow">lifts_vector ( ⬆*[?] ? ≡ ? )</td>
             <td class="snnn top yellow">lifts_lift_vector</td>
             <td class="snnn top yellow">
@@ -1093,7 +422,7 @@
               <br />
             </td>
             <td class="snns top yellow">lifts ( ⬆*[?] ? ≡ ? )</td>
-            <td class="snnn top yellow">lifts_lift lifts_lifts</td>
+            <td class="snnn top yellow">lifts_simple lifts_weight lifts_lifts</td>
             <td class="snnn top yellow">
               <br />
             </td>
@@ -1105,135 +434,39 @@
             <td class="nnns top capitalize italic yellow">
               <br />
             </td>
-            <td class="snns top italic yellow">support for multiple relocation</td>
-            <td class="snns top yellow">mr2 ( @⦃?,?⦄ ≡ ? )</td>
-            <td class="snnn top yellow">mr2_plus ( ? + ? )</td>
-            <td class="snnn top yellow">mr2_minus ( ? ▭ ? ≡ ? )</td>
-            <td class="ssnn top yellow">mr2_mr2</td>
-          </tr>
-          <tr>
-            <td class="snns top capitalize italic orange">substitution</td>
-            <td class="snns top italic orange">structural successor for closures</td>
-            <td class="snns top orange">fquq ( ⦃?,?,?⦄ ⊐⸮ ⦃?,?,?⦄ )</td>
-            <td class="snnn top orange">fquq_alt ( ⦃?,?,?⦄ ⊐⊐⸮ ⦃?,?,?⦄ )</td>
-            <td class="snnn top orange">
-              <br />
-            </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">fqu ( ⦃?,?,?⦄ ⊐ ⦃?,?,?⦄ )</td>
-            <td class="snnn top orange">
-              <br />
-            </td>
-            <td class="snnn top orange">
-              <br />
-            </td>
-            <td class="ssnn top orange">
-              <br />
-            </td>
-          </tr>
-          <tr>
-            <td class="nnns top capitalize italic orange">
-              <br />
-            </td>
-            <td class="snns top italic orange">global env. slicing</td>
-            <td class="snns top orange">gget ( ⬇[?] ? ≡ ? )</td>
-            <td class="snnn top orange">gget_gget</td>
-            <td class="snnn top orange">
-              <br />
-            </td>
-            <td class="ssnn top orange">
-              <br />
-            </td>
-          </tr>
-          <tr>
-            <td class="nnns top capitalize italic orange">
-              <br />
-            </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">
-              <br />
-            </td>
-            <td class="ssnn top orange">
-              <br />
-            </td>
-          </tr>
-          <tr>
-            <td class="nnns top capitalize italic orange">
-              <br />
-            </td>
-            <td class="snns top italic orange">local env. ref. for rt-substitution</td>
-            <td class="snns top orange">lsuby ( ? ⊆[?,?] ? )</td>
-            <td class="snnn top orange">lsuby_lsuby</td>
-            <td class="snnn top orange">
-              <br />
-            </td>
-            <td class="ssnn top orange">
-              <br />
-            </td>
-          </tr>
-          <tr>
-            <td class="nnns top capitalize italic orange">
-              <br />
-            </td>
-            <td class="snns top italic orange">pointwise extension of a relation</td>
-            <td class="snns top orange">lpx_sn</td>
-            <td class="snnn top orange">lpx_sn_alt lpx_sn_tc lpx_sn_drop lpx_sn_lpx_sn</td>
-            <td class="snnn top orange">
+            <td class="snns top italic yellow">ranged equivalence for local environments</td>
+            <td class="snns top yellow">lreq ( ? ≡[?] ? )</td>
+            <td class="snnn top yellow">lreq_length lreq_lreq</td>
+            <td class="snnn top yellow">
               <br />
             </td>
-            <td class="ssnn top orange">
+            <td class="ssnn top yellow">
               <br />
             </td>
           </tr>
           <tr>
-            <td class="nnns top capitalize italic orange">
+            <td class="nnns top capitalize italic yellow">
               <br />
             </td>
-            <td class="snns top italic orange">basic local env. slicing</td>
-            <td class="snns top orange">drop ( ⬇[?,?,?] ? ≡ ? )</td>
-            <td class="snnn top orange">drop_append drop_lreq drop_drop</td>
-            <td class="snnn top orange">
+            <td class="snns top italic yellow">generic entrywise extension of context-sensitive relations for terma</td>
+            <td class="snns top yellow">lexs ( ? ⦻*[?,?,?] ? )</td>
+            <td class="snnn top yellow">lexs_length lexs_lexs</td>
+            <td class="snnn top yellow">
               <br />
             </td>
-            <td class="ssnn top orange">
+            <td class="ssnn top yellow">
               <br />
             </td>
           </tr>
           <tr>
-            <td class="nnns top capitalize italic orange">
+            <td class="snns top capitalize italic orange" />
+            <td class="snns top italic orange" />
+            <td class="snns top orange">
               <br />
             </td>
-            <td class="snns top italic orange">basic term relocation</td>
-            <td class="snns top orange">lift_vector ( ⬆[?,?] ? ≡ ? )</td>
-            <td class="snnn top orange">lift_lift_vector</td>
             <td class="snnn top orange">
               <br />
             </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">lift ( ⬆[?,?] ? ≡ ? )</td>
-            <td class="snnn top orange">lift_neq lift_lift</td>
             <td class="snnn top orange">
               <br />
             </td>
@@ -1243,9 +476,9 @@
           </tr>
           <tr>
             <td class="snns top capitalize italic red">grammar</td>
-            <td class="snns top italic red">equivalence for local environments</td>
-            <td class="snns top red">lreq ( ? ⩬[?,?] ? )</td>
-            <td class="snnn top red">lreq_lreq</td>
+            <td class="snns top italic red">context-sensitive equivalences for terms</td>
+            <td class="snns top red">ceq</td>
+            <td class="snnn top red">ceq_ceq</td>
             <td class="snnn top red">
               <br />
             </td>
@@ -1384,6 +617,6 @@
     <div xmlns:ld="http://lambdadelta.info/" class="spacer">
       <br />
     </div>
-    <div xmlns:ld="http://lambdadelta.info/" class="spacer">Last update: Sun, 06 Sep 2015 21:40:58 +0200</div>
+    <div xmlns:ld="http://lambdadelta.info/" class="spacer">Last update: Sun, 27 Mar 2016 18:42:29 +0200</div>
   </body>
 </html>
diff --git a/helm/www/lambdadelta/documentation.html b/helm/www/lambdadelta/documentation.html
index e800db393..e00c7ab8e 100644
--- a/helm/www/lambdadelta/documentation.html
+++ b/helm/www/lambdadelta/documentation.html
@@ -389,6 +389,6 @@
     <div xmlns:ld="http://lambdadelta.info/" class="spacer">
       <br />
     </div>
-    <div xmlns:ld="http://lambdadelta.info/" class="spacer">Last update: Fri, 04 Mar 2016 16:15:58 +0100</div>
+    <div xmlns:ld="http://lambdadelta.info/" class="spacer">Last update: Sun, 27 Mar 2016 18:42:29 +0200</div>
   </body>
 </html>
diff --git a/helm/www/lambdadelta/etc/Makefile b/helm/www/lambdadelta/etc/Makefile
new file mode 100644
index 000000000..da91d0f82
--- /dev/null
+++ b/helm/www/lambdadelta/etc/Makefile
@@ -0,0 +1,14 @@
+FIND = find Environment -name "*.xml"
+
+GREP = grep -h "<Abst"
+
+SED = sed -e "s/^ *//g"
+
+SORT = sort
+
+UNIQ = uniq
+
+all: abst.txt
+
+abst.txt:
+	@$(FIND) | xargs $(GREP) | $(SED) | $(SORT) | $(UNIQ) > abst.txt
diff --git a/helm/www/lambdadelta/etc/abst.txt b/helm/www/lambdadelta/etc/abst.txt
new file mode 100644
index 000000000..4a2ef683c
--- /dev/null
+++ b/helm/www/lambdadelta/etc/abst.txt
@@ -0,0 +1,59 @@
+Restricted abstractions in layer 1
+
+<Abst name="P" layer="1" side-degree="1" main-degree="0" side-position="0" main-position="1"> SB TP
+<Abst name="P" layer="1" side-degree="1" main-degree="0" side-position="1" main-position="1"> SB PP
+
+<Abst name="P" layer="1" side-degree="1" main-degree="1" side-position="0" main-position="0"> SS TT
+<Abst name="P" layer="1" side-degree="1" main-degree="1" side-position="0" main-position="1"> SS TP
+<Abst name="P" layer="1" side-degree="1" main-degree="1" side-position="1" main-position="0"> SS PT
+<Abst name="P" layer="1" side-degree="1" main-degree="1" side-position="1" main-position="1"> SS PP
+
+Restricted abstractions in layer 2
+
+<Abst name="P" layer="2" side-degree="1" main-degree="1" side-position="0" main-position="1"> SB TP
+<Abst name="P" layer="2" side-degree="1" main-degree="1" side-position="1" main-position="1"> SB PP
+
+<Abst name="P" layer="2" side-degree="1" main-degree="2" side-position="0" main-position="0"> SS TT
+<Abst name="P" layer="2" side-degree="1" main-degree="2" side-position="0" main-position="1"> SS TP
+<Abst name="P" layer="2" side-degree="1" main-degree="2" side-position="1" main-position="0"> SS PT
+<Abst name="P" layer="2" side-degree="1" main-degree="2" side-position="1" main-position="1"> SS PP
+
+Unrestricted abstractions in layer 1
+
+<Abst name="Y" layer="1" side-degree="0" main-degree="0" side-position="0" main-position="0">
+<Abst name="Y" layer="1" side-degree="0" main-degree="0" side-position="0" main-position="1">
+<Abst name="Y" layer="1" side-degree="0" main-degree="0" side-position="1" main-position="0">
+
+<Abst name="Y" layer="1" side-degree="0" main-degree="1" side-position="0" main-position="0">
+<Abst name="Y" layer="1" side-degree="0" main-degree="1" side-position="0" main-position="1">
+<Abst name="Y" layer="1" side-degree="0" main-degree="1" side-position="1" main-position="0">
+<Abst name="Y" layer="1" side-degree="0" main-degree="1" side-position="1" main-position="1">
+
+<Abst name="Y" layer="1" side-degree="1" main-degree="0" side-position="0" main-position="1">
+
+<Abst name="Y" layer="1" side-degree="1" main-degree="1" side-position="0" main-position="0">
+<Abst name="Y" layer="1" side-degree="1" main-degree="1" side-position="0" main-position="1">
+<Abst name="Y" layer="1" side-degree="1" main-degree="1" side-position="1" main-position="0">
+<Abst name="Y" layer="1" side-degree="1" main-degree="1" side-position="1" main-position="1">
+
+Unrestricted abstractions in layer 2
+
+<Abst name="Y" layer="2" side-degree="0" main-degree="1" side-position="0" main-position="0">
+<Abst name="Y" layer="2" side-degree="0" main-degree="1" side-position="0" main-position="1">
+<Abst name="Y" layer="2" side-degree="0" main-degree="1" side-position="1" main-position="0">
+<Abst name="Y" layer="2" side-degree="0" main-degree="1" side-position="1" main-position="1">
+
+<Abst name="Y" layer="2" side-degree="0" main-degree="2" side-position="0" main-position="0">
+<Abst name="Y" layer="2" side-degree="0" main-degree="2" side-position="0" main-position="1">
+<Abst name="Y" layer="2" side-degree="0" main-degree="2" side-position="1" main-position="0">
+<Abst name="Y" layer="2" side-degree="0" main-degree="2" side-position="1" main-position="1">
+
+<Abst name="Y" layer="2" side-degree="1" main-degree="1" side-position="0" main-position="0">
+<Abst name="Y" layer="2" side-degree="1" main-degree="1" side-position="0" main-position="1">
+<Abst name="Y" layer="2" side-degree="1" main-degree="1" side-position="1" main-position="0">
+<Abst name="Y" layer="2" side-degree="1" main-degree="1" side-position="1" main-position="1">
+
+<Abst name="Y" layer="2" side-degree="1" main-degree="2" side-position="0" main-position="0">
+<Abst name="Y" layer="2" side-degree="1" main-degree="2" side-position="0" main-position="1">
+<Abst name="Y" layer="2" side-degree="1" main-degree="2" side-position="1" main-position="0">
+<Abst name="Y" layer="2" side-degree="1" main-degree="2" side-position="1" main-position="1">
diff --git a/helm/www/lambdadelta/ground_1.html b/helm/www/lambdadelta/ground_1.html
index b9976bfa7..d3e660577 100644
--- a/helm/www/lambdadelta/ground_1.html
+++ b/helm/www/lambdadelta/ground_1.html
@@ -291,6 +291,6 @@
     <div xmlns:ld="http://lambdadelta.info/" class="spacer">
       <br />
     </div>
-    <div xmlns:ld="http://lambdadelta.info/" class="spacer">Last update: Fri, 04 Mar 2016 16:15:59 +0100</div>
+    <div xmlns:ld="http://lambdadelta.info/" class="spacer">Last update: Sun, 27 Mar 2016 18:42:29 +0200</div>
   </body>
 </html>
diff --git a/helm/www/lambdadelta/ground_2.html b/helm/www/lambdadelta/ground_2.html
index b6e10865c..598ae85dc 100644
--- a/helm/www/lambdadelta/ground_2.html
+++ b/helm/www/lambdadelta/ground_2.html
@@ -134,27 +134,27 @@
             <td class="snns italic cyan">files</td>
             <td class="snnn right italic cyan">77</td>
             <td class="snns italic cyan">characters</td>
-            <td class="snnn right italic cyan">93034</td>
+            <td class="snnn right italic cyan">93671</td>
             <td class="snns italic cyan">nodes</td>
-            <td class="ssnn right italic cyan">195875</td>
+            <td class="ssnn right italic cyan">198031</td>
           </tr>
           <tr>
             <td class="snns capitalize italic green">propositions</td>
             <td class="snns italic green">theorems</td>
-            <td class="snnn right italic green">14</td>
+            <td class="snnn right italic green">23</td>
             <td class="snns italic green">lemmas</td>
-            <td class="snnn right italic green">434</td>
+            <td class="snnn right italic green">472</td>
             <td class="snns italic green">total</td>
-            <td class="ssnn right italic green">448</td>
+            <td class="ssnn right italic green">495</td>
           </tr>
           <tr>
             <td class="snss capitalize italic yellow">concepts</td>
             <td class="snss italic yellow">declared</td>
-            <td class="snsn right italic yellow">44</td>
+            <td class="snsn right italic yellow">53</td>
             <td class="snss italic yellow">defined</td>
-            <td class="snsn right italic yellow">37</td>
+            <td class="snsn right italic yellow">49</td>
             <td class="snss italic yellow">total</td>
-            <td class="sssn right italic yellow">81</td>
+            <td class="sssn right italic yellow">102</td>
           </tr>
         </tbody>
       </table>
@@ -678,6 +678,6 @@
     <div xmlns:ld="http://lambdadelta.info/" class="spacer">
       <br />
     </div>
-    <div xmlns:ld="http://lambdadelta.info/" class="spacer">Last update: Mon, 21 Mar 2016 20:38:12 +0100</div>
+    <div xmlns:ld="http://lambdadelta.info/" class="spacer">Last update: Sun, 27 Mar 2016 18:42:29 +0200</div>
   </body>
 </html>
diff --git a/helm/www/lambdadelta/implementation.html b/helm/www/lambdadelta/implementation.html
index 5b941c5d0..c9551cd11 100644
--- a/helm/www/lambdadelta/implementation.html
+++ b/helm/www/lambdadelta/implementation.html
@@ -291,6 +291,6 @@
     <div xmlns:ld="http://lambdadelta.info/" class="spacer">
       <br />
     </div>
-    <div xmlns:ld="http://lambdadelta.info/" class="spacer">Last update: Fri, 04 Mar 2016 16:15:58 +0100</div>
+    <div xmlns:ld="http://lambdadelta.info/" class="spacer">Last update: Sun, 27 Mar 2016 18:42:29 +0200</div>
   </body>
 </html>
diff --git a/helm/www/lambdadelta/index.html b/helm/www/lambdadelta/index.html
index a25006067..14c85248a 100644
--- a/helm/www/lambdadelta/index.html
+++ b/helm/www/lambdadelta/index.html
@@ -276,6 +276,6 @@
     <div xmlns:ld="http://lambdadelta.info/" class="spacer">
       <br />
     </div>
-    <div xmlns:ld="http://lambdadelta.info/" class="spacer">Last update: Fri, 04 Mar 2016 16:15:58 +0100</div>
+    <div xmlns:ld="http://lambdadelta.info/" class="spacer">Last update: Sun, 27 Mar 2016 18:42:29 +0200</div>
   </body>
 </html>
diff --git a/helm/www/lambdadelta/news.html b/helm/www/lambdadelta/news.html
index 66edcf343..11a934d11 100644
--- a/helm/www/lambdadelta/news.html
+++ b/helm/www/lambdadelta/news.html
@@ -380,6 +380,6 @@
     <div xmlns:ld="http://lambdadelta.info/" class="spacer">
       <br />
     </div>
-    <div xmlns:ld="http://lambdadelta.info/" class="spacer">Last update: Fri, 04 Mar 2016 16:15:58 +0100</div>
+    <div xmlns:ld="http://lambdadelta.info/" class="spacer">Last update: Sun, 27 Mar 2016 18:42:29 +0200</div>
   </body>
 </html>
diff --git a/helm/www/lambdadelta/specification.html b/helm/www/lambdadelta/specification.html
index 83528ee96..1a8dae817 100644
--- a/helm/www/lambdadelta/specification.html
+++ b/helm/www/lambdadelta/specification.html
@@ -382,6 +382,6 @@
     <div xmlns:ld="http://lambdadelta.info/" class="spacer">
       <br />
     </div>
-    <div xmlns:ld="http://lambdadelta.info/" class="spacer">Last update: Fri, 04 Mar 2016 16:15:58 +0100</div>
+    <div xmlns:ld="http://lambdadelta.info/" class="spacer">Last update: Sun, 27 Mar 2016 18:42:29 +0200</div>
   </body>
 </html>