X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=helm%2Fwww%2Flambdadelta%2Fbasic_2.html;h=5075e40e11bcc0bf86bc321623e146c661b17625;hb=3080bf8226d155d017c5ec5c4e852d952f5b878c;hp=68f455388549923329a0a6a8a2c8cb231e4dc59b;hpb=bb1a03359dfaea6031592d28b9bfb15d797c44e5;p=helm.git

diff --git a/helm/www/lambdadelta/basic_2.html b/helm/www/lambdadelta/basic_2.html
index 68f455388..5075e40e1 100644
--- a/helm/www/lambdadelta/basic_2.html
+++ b/helm/www/lambdadelta/basic_2.html
@@ -6,8 +6,8 @@
     <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 version 2" />
-    <title>\lambda\delta version 2</title>
+    <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" />
@@ -19,19 +19,83 @@
         <img class="icon32" alt="[lambdadelta home]" title="lambdadelta home" src="http://lambdadelta.info/images/crux_32.png" />
       </a>
     </div>
-    <div class="head1">cic:/matita/lambdadelta/basic_2/ (λδ version 2)</div>
+    <div class="head1">cic:/matita/lambdadelta/basic_2/ (core λδ version 2)</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="ssns capitalize italic green">
+              <a href="http://lambdadelta.info/implementation.html">implementation</a>
+            </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="ssns capitalize green">
+              <a href="http://lambdadelta.info/implementation.html#lddl">library</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">
+              <br />
+            </td>
+            <td class="ssss capitalize green">
+              <a href="http://lambdadelta.info/implementation.html#helena">helena</a>
+            </td>
+          </tr>
+        </tbody>
+      </table>
+    </div>
 
 
-   <div xmlns:ld="http://lambdadelta.info/" class="head2sn" id="">Summary of the Specification</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
          and its timeline.
-         Nodes are counted according to the "intrinsinc 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">
       <table cellpadding="4" cellspacing="0">
@@ -58,103 +122,109 @@
           <tr>
             <td class="snns capitalize italic cyan">sizes</td>
             <td class="snns italic cyan">files</td>
-            <td class="snnn right italic cyan">359</td>
+            <td class="snnn right italic cyan">360</td>
             <td class="snns italic cyan">characters</td>
-            <td class="snnn right italic cyan">429712</td>
+            <td class="snnn right italic cyan">433402</td>
             <td class="snns italic cyan">nodes</td>
-            <td class="ssnn right italic cyan">1856521</td>
+            <td class="ssnn right italic cyan">1874774</td>
           </tr>
           <tr>
             <td class="snns capitalize italic green">propositions</td>
             <td class="snns italic green">theorems</td>
-            <td class="snnn right italic green">127</td>
+            <td class="snnn right italic green">130</td>
             <td class="snns italic green">lemmas</td>
-            <td class="snnn right italic green">1273</td>
+            <td class="snnn right italic green">1286</td>
             <td class="snns italic green">total</td>
-            <td class="ssnn right italic green">1400</td>
+            <td class="ssnn right italic green">1416</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="snss italic yellow">defined</td>
-            <td class="snsn right italic yellow">83</td>
+            <td class="snsn right italic yellow">89</td>
             <td class="snss italic yellow">total</td>
-            <td class="sssn right italic yellow">137</td>
+            <td class="sssn right italic yellow">143</td>
           </tr>
         </tbody>
       </table>
     </div>
 
-   <div xmlns:ld="http://lambdadelta.info/" class="head3sn" id="">Stage "B"</div>
+   <div xmlns:ld="http://lambdadelta.info/" class="head3sn" id="B">Stage "B"</div>
    <ul xmlns:ld="http://lambdadelta.info/">
       <li>
-        <span class="date">In progress.</span>
+        <span class="emph alpha">Ongoing.</span>
          Context-sensitive subject equivalence
          for native type assignment.
    </li>
     </ul>
 
-   <div xmlns:ld="http://lambdadelta.info/" class="head3sn" id="">Stage "A": "Weakening the Applicability Condition"</div>
+   <div xmlns:ld="http://lambdadelta.info/" class="head3sn" id="A">Stage "A": "Extending the Applicability Condition"</div>
+   <ul xmlns:ld="http://lambdadelta.info/">
+      <li>
+        <span class="emph gamma">2014 October 28.</span>
+         λδ version 2A is released.
+   </li>
+    </ul>
    <ul xmlns:ld="http://lambdadelta.info/">
       <li>
-        <span class="date">2014 September 9.</span>
-         Interated static type assignment defined (more elegantly)
+        <span class="emph beta">2014 September 9.</span>
+         Iterated static type assignment defined (more elegantly)
          as a primitive notion.
    </li>
     </ul>
    <ul xmlns:ld="http://lambdadelta.info/">
       <li>
-        <span class="date">2014 June 18.</span>
+        <span class="emph beta">2014 June 18.</span>
          Preservation of stratified native validity
          for context-sensitive computation on terms.
    </li>
     </ul>
    <ul xmlns:ld="http://lambdadelta.info/">
       <li>
-        <span class="date">2014 June 9.</span>
-         "Big tree" strong normalization
+        <span class="emph alpha">2014 June 9.</span>
+         Strong qrst-normalization
          for simply typed terms.
    </li>
     </ul>
    <ul xmlns:ld="http://lambdadelta.info/">
       <li>
-        <span class="date">2014 April 16.</span>
-         lazy equivalence on local environments
-	 serves as irrelevant step in "big tree" computation on closures
+        <span class="emph alpha">2014 April 16.</span>
+         Lazy equivalence on local environments
+	 addded as q-step to rst-computation on closures
          (anniversary milestone).
    </li>
     </ul>
    <ul xmlns:ld="http://lambdadelta.info/">
       <li>
-        <span class="date">2014 January 20.</span>
-         Parametrized slicing for local environments
+        <span class="emph alpha">2014 January 20.</span>
+         Parametrized slicing of local environments
 	 comprises both versions of this operation
 	 (one from basic_1, the other used in basic_2 till now).
    </li>
     </ul>
    <ul xmlns:ld="http://lambdadelta.info/">
       <li>
-        <span class="date">2013 August 7.</span>
+        <span class="emph alpha">2013 August 7.</span>
          Passive support for global environments.
    </li>
     </ul>
    <ul xmlns:ld="http://lambdadelta.info/">
       <li>
-        <span class="date">2013 July 27.</span>
-         Reaxiomatized β-reductum as in extended β-reduction
+        <span class="emph alpha">2013 July 27.</span>
+         Reaxiomatized β-reductum as in rt-reduction.
    </li>
     </ul>
    <ul xmlns:ld="http://lambdadelta.info/">
       <li>
-        <span class="date">2013 July 20.</span>
-         Context-sensitive extended strong normalization
+        <span class="emph alpha">2013 July 20.</span>
+         Context-sensitive strong rt-normalization
          for simply typed terms.
    </li>
     </ul>
    <ul xmlns:ld="http://lambdadelta.info/">
       <li>
-        <span class="date">2013 April 16.</span>
+        <span class="emph alpha">2013 April 16.</span>
          Reaxiomatized substitution and reduction
          commute with respect to subclosure
          (anniversary milestone).
@@ -162,26 +232,26 @@
     </ul>
    <ul xmlns:ld="http://lambdadelta.info/">
       <li>
-        <span class="date">2013 March 16.</span>
+        <span class="emph alpha">2013 March 16.</span>
          Mutual recursive preservation of stratified native validity
-         for "big tree" computation on closures.
+         for rst-computation on closures.
    </li>
     </ul>
    <ul xmlns:ld="http://lambdadelta.info/">
       <li>
-        <span class="date">2012 October 16.</span>
+        <span class="emph alpha">2012 October 16.</span>
          Confluence for context-free parallel reduction on closures.
    </li>
     </ul>
    <ul xmlns:ld="http://lambdadelta.info/">
       <li>
-        <span class="date">2012 July 26.</span>
+        <span class="emph alpha">2012 July 26.</span>
          Term binders polarized to control ζ-reduction (not released).
    </li>
     </ul>
    <ul xmlns:ld="http://lambdadelta.info/">
       <li>
-        <span class="date">2012 April 16.</span>
+        <span class="emph alpha">2012 April 16.</span>
          Context-sensitive subject equivalence
          for atomic arity assignment
          (anniversary milestone).
@@ -189,42 +259,39 @@
     </ul>
    <ul xmlns:ld="http://lambdadelta.info/">
       <li>
-        <span class="date">2012 March 15.</span>
+        <span class="emph alpha">2012 March 15.</span>
          Context-sensitive strong normalization
          for simply typed terms.
    </li>
     </ul>
    <ul xmlns:ld="http://lambdadelta.info/">
       <li>
-        <span class="date">2012 January 27.</span>
+        <span class="emph alpha">2012 January 27.</span>
          Support for abstract candidates of reducibility.
    </li>
     </ul>
    <ul xmlns:ld="http://lambdadelta.info/">
       <li>
-        <span class="date">2011 September 21.</span>
+        <span class="emph alpha">2011 September 21.</span>
          Confluence for context-sensitive parallel reduction on terms.
    </li>
     </ul>
    <ul xmlns:ld="http://lambdadelta.info/">
       <li>
-        <span class="date">2011 September 6.</span>
+        <span class="emph alpha">2011 September 6.</span>
          Confluence for context-free parallel reduction on terms.
    </li>
     </ul>
    <ul xmlns:ld="http://lambdadelta.info/">
       <li>
-        <span class="date">2011 April 17.</span>
+        <span class="emph alpha">2011 April 17.</span>
          Specification starts.
    </li>
     </ul>
 
-   <div xmlns:ld="http://lambdadelta.info/" class="head2sn" id="">Logical Structure of the Specification</div>
-   <div xmlns:ld="http://lambdadelta.info/" class="text">The source files are grouped in planes and components
-         according to the following table.
-         Notation files covering the whole specification are provided.
-         The notation for the relations or functions introduced in each file
-         is shown in parentheses (? are placeholders).
+   <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" />
+    </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">
@@ -246,8 +313,10 @@
           <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</td>
-            <td class="snnn top wine">ex_cpr_omega</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>
@@ -305,7 +374,7 @@
               <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_scpes snv_preserve</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>
@@ -315,7 +384,7 @@
           </tr>
           <tr>
             <td class="snns top capitalize italic blue">equivalence</td>
-            <td class="snns top italic blue">decomposed extended 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">
@@ -353,7 +422,7 @@
           </tr>
           <tr>
             <td class="snns top capitalize italic cyan">computation</td>
-            <td class="snns top italic cyan">evaluation for context-sensitive extended reduction</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 />
@@ -383,9 +452,9 @@
             <td class="nnns top capitalize italic cyan">
               <br />
             </td>
-            <td class="snns top italic cyan">strongly normalizing "big tree" computation</td>
-            <td class="snns top cyan">fsb ( ⦃?,?⦄ ⊢ ⦥[?,?] ? )</td>
-            <td class="snnn top cyan">fsb_alt ( ⦃?,?⦄ ⊢ ⦥⦥[?,?] ? )</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 />
@@ -395,7 +464,7 @@
             <td class="nnns top capitalize italic cyan">
               <br />
             </td>
-            <td class="snns top italic cyan">strongly normalizing extended computation</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">
@@ -453,41 +522,9 @@
             <td class="nnns top capitalize italic cyan">
               <br />
             </td>
-            <td class="snns top italic cyan">"big tree" parallel computation</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_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">fpbc ( ⦃?,?,?⦄ ≻≡[?,?] ⦃?,?,?⦄ )</td>
-            <td class="snnn top cyan">fpbc_fleq fpbc_fpbs</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">fpbu ( ⦃?,?,?⦄ ≻[?,?] ⦃?,?,?⦄ )</td>
-            <td class="snnn top cyan">fpbu_lift fpbu_lleq fpbu_fleq</td>
+            <td class="snnn top cyan">fpbg_lift fpbg_fleq fpbg_fpbs fpbg_fpbg</td>
             <td class="snnn top cyan">
               <br />
             </td>
@@ -504,7 +541,7 @@
             </td>
             <td class="snns top cyan">fpbs ( ⦃?,?,?⦄ ≥[?,?] ⦃?,?,?⦄ )</td>
             <td class="snnn top cyan">fpbs_alt ( ⦃?,?,?⦄ ≥≥[?,?] ⦃?,?,?⦄ )</td>
-            <td class="snnn top cyan">fpbs_lift fpbs_fleq fpbs_aaa fpbs_fpbs fpbs_ext</td>
+            <td class="snnn top cyan">fpbs_lift fpbs_aaa fpbs_fpb fpbs_fpbs</td>
             <td class="ssnn top cyan">
               <br />
             </td>
@@ -513,7 +550,7 @@
             <td class="nnns top capitalize italic cyan">
               <br />
             </td>
-            <td class="snns top italic cyan">decomposed extended computation</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">
@@ -527,7 +564,7 @@
             <td class="nnns top capitalize italic cyan">
               <br />
             </td>
-            <td class="snns top italic cyan">context-sensitive extended computation</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">
@@ -545,7 +582,7 @@
               <br />
             </td>
             <td class="snns top cyan">cpxs ( ⦃?,?⦄ ⊢ ? ➡*[?,?] ? )</td>
-            <td class="snnn top cyan">cpxs_tsts cpxs_tsts_vector cpxs_leq cpxs_lift cpxs_lleq cpxs_aaa cpxs_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>
@@ -611,9 +648,23 @@
           </tr>
           <tr>
             <td class="snns top capitalize italic water">reduction</td>
-            <td class="snns top italic water">"big tree" parallel reduction</td>
-            <td class="snns top water">fpb ( ⦃?,?,?⦄ ≽[?,?] ⦃?,?,?⦄ )</td>
-            <td class="snnn top water">fpb_lift fpb_aaa</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>
@@ -625,7 +676,7 @@
             <td class="nnns top capitalize italic water">
               <br />
             </td>
-            <td class="snns top italic water">normal forms for context-sensitive extended reduction</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">
@@ -639,7 +690,7 @@
             <td class="nnns top capitalize italic water">
               <br />
             </td>
-            <td class="snns top italic water">context-sensitive extended reduction</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">
@@ -657,7 +708,7 @@
               <br />
             </td>
             <td class="snns top water">cpx ( ⦃?,?⦄ ⊢ ? ➡[?,?] ? )</td>
-            <td class="snnn top water">cpx_leq cpx_lift cpx_llpx_sn cpx_lleq cpx_cix</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>
@@ -669,7 +720,7 @@
             <td class="nnns top capitalize italic water">
               <br />
             </td>
-            <td class="snns top italic water">irreducible forms for context-sensitive extended reduction</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">
@@ -683,7 +734,7 @@
             <td class="nnns top capitalize italic water">
               <br />
             </td>
-            <td class="snns top italic water">reducible forms for context-sensitive extended reduction</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">
@@ -895,7 +946,7 @@
               <br />
             </td>
             <td class="snns top yellow">lleq ( ? ≡[?,?] ? )</td>
-            <td class="snnn top yellow">lleq_alt lleq_alt_rec lleq_leq lleq_drop lleq_fqus lleq_llor lleq_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="snnn top yellow">
               <br />
             </td>
@@ -909,7 +960,7 @@
             </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_leq llpx_sn_drop llpx_sn_lpx_sn llpx_sn_frees llpx_sn_llor</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="snnn top yellow">
               <br />
             </td>
@@ -922,7 +973,7 @@
               <br />
             </td>
             <td class="snns top italic yellow">pointwise union for local environments</td>
-            <td class="snns top yellow">llor ( ? ⩖[?,?] ? ≡ ? )</td>
+            <td class="snns top yellow">llor ( ? ⋓[?,?] ? ≡ ? )</td>
             <td class="snnn top yellow">llor_alt llor_drop</td>
             <td class="snnn top yellow">
               <br />
@@ -937,7 +988,7 @@
             </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_leq frees_lift</td>
+            <td class="snnn top yellow">frees_append frees_lreq frees_lift</td>
             <td class="snnn top yellow">
               <br />
             </td>
@@ -949,7 +1000,7 @@
             <td class="nnns top capitalize italic yellow">
               <br />
             </td>
-            <td class="snns top italic yellow">contxt-sensitive extended multiple substitution</td>
+            <td class="snns top italic yellow">contxt-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>
@@ -992,7 +1043,7 @@
               <br />
             </td>
             <td class="snns top italic yellow">iterated local env. slicing</td>
-            <td class="snns top yellow">drops ( ⇩*[?,?] ? ≡ ? )</td>
+            <td class="snns top yellow">drops ( ⬇*[?,?] ? ≡ ? )</td>
             <td class="snnn top yellow">drops_drop drops_drops</td>
             <td class="snnn top yellow">
               <br />
@@ -1006,7 +1057,7 @@
               <br />
             </td>
             <td class="snns top italic yellow">generic term relocation</td>
-            <td class="snns top yellow">lifts_vector ( ⇧*[?] ? ≡ ? )</td>
+            <td class="snns top yellow">lifts_vector ( ⬆*[?] ? ≡ ? )</td>
             <td class="snnn top yellow">lifts_lift_vector</td>
             <td class="snnn top yellow">
               <br />
@@ -1022,7 +1073,7 @@
             <td class="nnns top italic yellow">
               <br />
             </td>
-            <td class="snns top yellow">lifts ( ⇧*[?] ? ≡ ? )</td>
+            <td class="snns top yellow">lifts ( ⬆*[?] ? ≡ ? )</td>
             <td class="snnn top yellow">lifts_lift lifts_lifts</td>
             <td class="snnn top yellow">
               <br />
@@ -1076,7 +1127,7 @@
               <br />
             </td>
             <td class="snns top italic orange">global env. slicing</td>
-            <td class="snns top orange">gget ( ⇩[?] ? ≡ ? )</td>
+            <td class="snns top orange">gget ( ⬇[?] ? ≡ ? )</td>
             <td class="snnn top orange">gget_gget</td>
             <td class="snnn top orange">
               <br />
@@ -1089,7 +1140,7 @@
             <td class="nnns top capitalize italic orange">
               <br />
             </td>
-            <td class="snns top italic orange">contxt-sensitive extended ordinary substitution</td>
+            <td class="snns top italic orange">contxt-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">
@@ -1103,7 +1154,7 @@
             <td class="nnns top capitalize italic orange">
               <br />
             </td>
-            <td class="snns top italic orange">local env. ref. for extended substitution</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">
@@ -1132,8 +1183,8 @@
               <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_leq drop_drop</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">
               <br />
             </td>
@@ -1146,7 +1197,7 @@
               <br />
             </td>
             <td class="snns top italic orange">basic term relocation</td>
-            <td class="snns top orange">lift_vector ( ⇧[?,?] ? ≡ ? )</td>
+            <td class="snns top orange">lift_vector ( ⬆[?,?] ? ≡ ? )</td>
             <td class="snnn top orange">lift_lift_vector</td>
             <td class="snnn top orange">
               <br />
@@ -1162,7 +1213,7 @@
             <td class="nnns top italic orange">
               <br />
             </td>
-            <td class="snns top orange">lift ( ⇧[?,?] ? ≡ ? )</td>
+            <td class="snns top orange">lift ( ⬆[?,?] ? ≡ ? )</td>
             <td class="snnn top orange">lift_neq lift_lift</td>
             <td class="snnn top orange">
               <br />
@@ -1174,8 +1225,8 @@
           <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">leq ( ? ⩬[?,?] ? )</td>
-            <td class="snnn top red">leq_leq</td>
+            <td class="snns top red">lreq ( ? ⩬[?,?] ? )</td>
+            <td class="snnn top red">lreq_lreq</td>
             <td class="snnn top red">
               <br />
             </td>
@@ -1289,10 +1340,6 @@
       </table>
     </div>
 
-   <div xmlns:ld="http://lambdadelta.info/" class="head2sn" id="">Physical Structure of the Specification</div>
-   <div xmlns:ld="http://lambdadelta.info/" class="text">The source files are grouped in directories,
-         one for each component.
-   </div>
    <div class="spacer">
       <img class="rule" alt="[Spacer]" title="lambdadelta rainbow rule" src="http://lambdadelta.info/images/rainbow.png" />
     </div>
@@ -1319,6 +1366,6 @@
     <div xmlns:ld="http://lambdadelta.info/" class="spacer">
       <br />
     </div>
-    <div xmlns:ld="http://lambdadelta.info/" class="spacer">Last update: Wed, 10 Sep 2014 21:47:00 +0200</div>
+    <div xmlns:ld="http://lambdadelta.info/" class="spacer">Last update: Tue, 04 Nov 2014 16:21:23 +0100</div>
 </body>
 </html>