X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=helm%2Fwww%2Flambdadelta%2Fbasic_2.html;h=e3665cc8edb2f2f54d976049b1316781e65d9140;hb=25577a78cccba09974c91fcbfea770091a413382;hp=aac7fea7e869368c235a71ee6a1d2a7324245bce;hpb=37e1b4f314ffae815beca71300688040f8da6939;p=helm.git

diff --git a/helm/www/lambdadelta/basic_2.html b/helm/www/lambdadelta/basic_2.html
index aac7fea7e..e3665cc8e 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">
@@ -60,18 +124,18 @@
             <td class="snns italic cyan">files</td>
             <td class="snnn right italic cyan">360</td>
             <td class="snns italic cyan">characters</td>
-            <td class="snnn right italic cyan">432823</td>
+            <td class="snnn right italic cyan">433402</td>
             <td class="snns italic cyan">nodes</td>
-            <td class="ssnn right italic cyan">1874185</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">130</td>
             <td class="snns italic green">lemmas</td>
-            <td class="snnn right italic green">1288</td>
+            <td class="snnn right italic green">1286</td>
             <td class="snns italic green">total</td>
-            <td class="ssnn right italic green">1418</td>
+            <td class="ssnn right italic green">1416</td>
           </tr>
           <tr>
             <td class="snss capitalize italic yellow">concepts</td>
@@ -86,40 +150,46 @@
       </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="date">2014 September 9.</span>
+        <span class="emph gamma">2014 October 28.</span>
+         λδ version 2A is released.
+   </li>
+    </ul>
+   <ul xmlns:ld="http://lambdadelta.info/">
+      <li>
+        <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>
+        <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>
+        <span class="emph alpha">2014 April 16.</span>
          Lazy equivalence on local environments
 	 addded as q-step to rst-computation on closures
          (anniversary milestone).
@@ -127,7 +197,7 @@
     </ul>
    <ul xmlns:ld="http://lambdadelta.info/">
       <li>
-        <span class="date">2014 January 20.</span>
+        <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).
@@ -135,26 +205,26 @@
     </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>
+        <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>
+        <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 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">
@@ -515,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>
@@ -641,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>
@@ -879,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>
@@ -893,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>
@@ -921,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>
@@ -1117,7 +1184,7 @@
             </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="snnn top orange">drop_append drop_lreq drop_drop</td>
             <td class="snnn top orange">
               <br />
             </td>
@@ -1158,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>
@@ -1273,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>
@@ -1303,6 +1366,6 @@
     <div xmlns:ld="http://lambdadelta.info/" class="spacer">
       <br />
     </div>
-    <div xmlns:ld="http://lambdadelta.info/" class="spacer">Last update: Wed, 22 Oct 2014 20:00:29 +0200</div>
+    <div xmlns:ld="http://lambdadelta.info/" class="spacer">Last update: Tue, 28 Oct 2014 17:45:56 +0100</div>
 </body>
 </html>