update in basic_2

[helm.git] / helm / www / lambdadelta / specification.html
diff --git a/helm/www/lambdadelta/specification.html b/helm/www/lambdadelta/specification.html

index 8a41523971cdd4cf00cae1f022f56b2f1bb96282..380924ebdb870f2fe2a2fd0dd792511654fce71b 100644 (file)
--- a/helm/www/lambdadelta/specification.html
+++ b/helm/www/lambdadelta/specification.html
@@ -1,114 +1,9 @@
  <?xml version="1.0" encoding="UTF-8"?>
  <!DOCTYPE html PUBLIC "-//W3C//DTD XHTML 1.1//EN" "http://www.w3.org/TR/xhtml11/DTD/xhtml11.dtd">
  <?xml version="1.0" encoding="UTF-8"?>
  <!DOCTYPE html PUBLIC "-//W3C//DTD XHTML 1.1//EN" "http://www.w3.org/TR/xhtml11/DTD/xhtml11.dtd">
-<html xmlns="http://www.w3.org/1999/xhtml" dir="ltr" lang="en-us">
-  <head>
-    <meta http-equiv="Content-Language" content="en-us" />
-    <meta http-equiv="Content-Type" content="text/html; charset=UTF-8" />
-    <meta http-equiv="Content-Style-Type" content="text/css" />
-    <meta name="author" content="Ferruccio Guidi" />
-    <meta name="description" content="\lambda\delta home page" />
-    <title>\lambda\delta home page</title>
-    <link rel="stylesheet" type="text/css" href="http://lambdadelta.info/css/ld_web.css" />
-    <link rel="stylesheet" type="text/css" href="http://lambdadelta.info/css/lddl.css" />
-    <link rel="stylesheet" type="text/css" href="http://lambdadelta.info/css/xhtbl.css" />
-    <link rel="shortcut icon" href="http://lambdadelta.info/images/crux_16.ico" />
-  </head>
-  <body lang="en-US">
-    <div class="spacer">
-      <a href="http://lambdadelta.info/">
-        <img class="icon32" alt="[lambdadelta home]" title="lambdadelta home" src="http://lambdadelta.info/images/crux_32.png" />
-      </a>
-    </div>
-    <div class="head1">The Formal Systems of the λδ (\lambda\delta) Family</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 white">
-              <a href="http://lambdadelta.info/specification.html">specification</a>
-            </td>
-            <td class="snnn capitalize italic white">
-              <br />
-            </td>
-            <td class="snnn capitalize italic white">
-              <br />
-            </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/implementation.html">implementation</a>
-            </td>
-            <td class="ssnn capitalize italic green">
-              <br />
-            </td>
-          </tr>
-          <tr>
-            <td class="snns capitalize sky">
-              <a href="http://lambdadelta.info/index.html#foreword">foreword</a>
-            </td>
-            <td class="snns capitalize magenta">
-              <a href="http://lambdadelta.info/news.html#milestones">milestones</a>
-            </td>
-            <td class="snns capitalize white">
-              <a href="http://lambdadelta.info/specification.html#v2">version 2</a>
-            </td>
-            <td class="snnn capitalize white">(<a href="http://lambdadelta.info/ground_2.html">background</a> - <a href="http://lambdadelta.info/basic_2.html">core</a> - <a href="http://lambdadelta.info/apps_2.html">applications</a>)</td>
-            <td class="snnn capitalize white">
-              <br />
-            </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/implementation.html#lddl">library</a>
-            </td>
-            <td class="ssnn capitalize green">(<a href="http://lambdadelta.info/static/lddl/">static LDDL directory</a>)</td>
-          </tr>
-          <tr>
-            <td class="snss capitalize sky">
-              <a href="http://lambdadelta.info/index.html#citations">citations</a>
-            </td>
-            <td class="snss capitalize magenta">
-              <a href="http://lambdadelta.info/news.html#visibility">visibility</a>
-            </td>
-            <td class="snss capitalize white">
-              <a href="http://lambdadelta.info/specification.html#v1">version 1</a>
-            </td>
-            <td class="snsn capitalize white">(<a href="http://lambdadelta.info/ground_1.html">background</a> - <a href="http://lambdadelta.info/basic_1.html">core</a>)</td>
-            <td class="snsn capitalize white">(<a href="http://lambdadelta.info/static/matita/lambdadelta/">static HELM directory</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/implementation.html#helena">helena</a>
-            </td>
-            <td class="sssn capitalize green">
-              <br />
-            </td>
-          </tr>
-        </tbody>
-      </table>
-    </div>
-    <div xmlns:ld="http://lambdadelta.info/" class="head2dx" id="specifications">Computer-checked formal specifications <img class="icon37" alt="[spacer]" title="lambdadelta butterfly" src="http://lambdadelta.info/images/b15.png" />
-    </div>
-    <div xmlns:ld="http://lambdadelta.info/" class="text">
+<html xmlns="http://www.w3.org/1999/xhtml" xmlns:ld="http://lambdadelta.info/" dir="ltr" lang="en-us"><head><meta http-equiv="Content-Language" content="en-us"/><meta http-equiv="Content-Type" content="text/html; charset=UTF-8"/><meta http-equiv="Content-Style-Type" content="text/css"/><meta name="author" content="Ferruccio Guidi"/><meta name="description" content="\lambda\delta home page"/><title>\lambda\delta home page</title><link rel="stylesheet" type="text/css" href="http://lambdadelta.info/css/ld_web.css"/><link rel="stylesheet" type="text/css" href="http://lambdadelta.info/css/lddl.css"/><link rel="stylesheet" type="text/css" href="http://lambdadelta.info/css/xhtbl.css"/><link rel="shortcut icon" href="http://lambdadelta.info/images/crux_16.ico"/></head><body lang="en-US"><div class="spacer"><a href="http://lambdadelta.info/"><img class="icon32" alt="[\lambda\delta home]" title="\lambda\delta home" src="http://lambdadelta.info/images/crux_32.png"/></a></div><div class="head1">The Formal Systems of the λδ (\lambda\delta) Family</div><div class="spacer"><img class="rule" alt="[Spacer]" title="\lambda\delta rainbow rule" src="http://lambdadelta.info/images/rainbow.png"/></div><div class="spacer"><br/></div><div class="text"><table cellpadding="4" cellspacing="0"><tbody><tr><td class="snns capitalize italic sky"><a href="http://lambdadelta.info/home.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 white"><a href="http://lambdadelta.info/specification.html">specification</a></td><td class="snnn capitalize italic white"><br/></td><td class="snnn capitalize italic white"><br/></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/implementation.html">implementation</a></td><td class="ssnn capitalize italic green"><br/></td></tr><tr><td class="snns capitalize sky"><a href="http://lambdadelta.info/home.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 white"><a href="http://lambdadelta.info/specification.html#v2">version 2</a></td><td class="snnn capitalize white">(<a href="http://lambdadelta.info/ground_2.html">background</a> - <a href="http://lambdadelta.info/basic_2.html">core</a> - <a href="http://lambdadelta.info/apps_2.html">applications</a>)</td><td class="snnn capitalize white"><br/></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/implementation.html#helena">helena</a></td><td class="ssnn capitalize green"><a href="http://lambdadelta.info/osn/">Open Symbolic Notation (OSN)</a></td></tr><tr><td class="snss capitalize sky"><a href="http://lambdadelta.info/home.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 white"><a href="http://lambdadelta.info/specification.html#v1">version 1</a></td><td class="snsn capitalize white">(<a href="http://lambdadelta.info/ground_1.html">background</a> - <a href="http://lambdadelta.info/basic_1.html">core</a>)</td><td class="snsn capitalize white">(<a href="http://lambdadelta.info/static/matita/lambdadelta/">static HELM directory</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/implementation.html#lddl">library</a></td><td class="sssn capitalize green">(<a href="http://lambdadelta.info/static/lddl/">static LDDL directory</a>)</td></tr></tbody></table></div><div class="head2dx" id="specifications">Computer-checked formal specifications <img class="icon37" alt="[butterfly]" title="\lambda\delta butterfly" src="http://lambdadelta.info/images/b15.png"/></div><div class="text">
        The systems of the λδ family are developed as machine-checked digital specifications,
        and are listed in the next table, which includes the major milestones.
        The systems of the λδ family are developed as machine-checked digital specifications,
        and are listed in the next table, which includes the major milestones.
-   </div>
-    <div xmlns:ld="http://lambdadelta.info/" class="text">
+   </div><div class="text">
        The life cycle of a specification consists of four periods.
        <span class="emph alpha">Alpha:</span>
        the definitions are designed and the major propositions are proved,
        The life cycle of a specification consists of four periods.
        <span class="emph alpha">Alpha:</span>
        the definitions are designed and the major propositions are proved,
@@ -120,268 +15,71 @@
        while major changes and additions are announced and reported on paper.
        <span class="emph delta">Delta:</span>
        after its conclusion, the specification is modified just for maintenance. 
        while major changes and additions are announced and reported on paper.
        <span class="emph delta">Delta:</span>
        after its conclusion, the specification is modified just for maintenance. 
-   </div>
-    <div xmlns:ld="http://lambdadelta.info/" class="text">
-      <table cellpadding="4" cellspacing="0">
-        <tbody>
-          <tr>
-            <td class="snns top capitalize italic gray">version</td>
-            <td class="snnn top capitalize italic gray">name</td>
-            <td class="snnn top capitalize italic gray">developed with</td>
-            <td class="snnn top capitalize italic gray">stage</td>
-            <td class="snnn top capitalize italic gray">started</td>
-            <td class="snnn top capitalize italic gray">announced</td>
-            <td class="snnn top capitalize italic gray">released</td>
-            <td class="snnn top capitalize italic gray">concluded</td>
-            <td class="ssnn top capitalize italic gray">references</td>
-          </tr>
-          <tr>
-            <td class="snns top yellow">
-              <a href="http://lambdadelta.info/specification.html#v3">Version 3</a>
-            </td>
-            <td class="snnn top yellow">"basic_3"</td>
-            <td class="snnn top yellow" />
-            <td class="snnn top yellow" />
-            <td class="snnn top yellow" />
-            <td class="snnn top yellow" />
-            <td class="snnn top yellow" />
-            <td class="snnn top yellow" />
-            <td class="ssnn top yellow">
-              <a href="http://lambdadelta.info/documentation#ldJ3a">J3a</a>
-            </td>
-          </tr>
-          <tr>
-            <td class="snns top orange">
-              <a href="http://lambdadelta.info/specification.html#v2">Version 2</a>
-            </td>
-            <td class="snnn top orange">"basic_2"</td>
-            <td class="snnn top orange">
-              <a href="http://matita.cs.unibo.it/">Matita 0.99.2</a>
-            </td>
-            <td class="snns top orange">"A2"</td>
-            <td class="snnn top orange">October 2015</td>
-            <td class="snnn top orange" />
-            <td class="snnn top orange" />
-            <td class="snnn top orange" />
-            <td class="ssnn top orange">
-              <br />
-            </td>
-          </tr>
-          <tr>
-            <td class="nnns top orange">
-              <br />
-            </td>
-            <td class="nnnn top orange">
-              <br />
-            </td>
-            <td class="nnnn top orange">
-              <br />
-            </td>
-            <td class="snns top orange">"A1"</td>
-            <td class="snnn top orange">April 2011</td>
-            <td class="snnn top orange">June 2014</td>
-            <td class="snnn top orange">October 2014</td>
-            <td class="snnn top orange">August 2015</td>
-            <td class="ssnn top orange">
-              <a href="http://lambdadelta.info/documentation#ldV2a">V2a</a>
-              <a href="http://lambdadelta.info/documentation#ldR2c">R2c</a>
-            </td>
-          </tr>
-          <tr>
-            <td class="snns top orange">Abandoned</td>
-            <td class="snnn top orange" />
-            <td class="snnn top orange">
-              <a href="http://coq.inria.fr/">Coq 7.3.1</a>
-            </td>
-            <td class="snnn top orange" />
-            <td class="snnn top orange">March 2008</td>
-            <td class="snnn top orange" />
-            <td class="snnn top orange" />
-            <td class="snnn top orange">February 2011</td>
-            <td class="ssnn top orange">
-              <br />
-            </td>
-          </tr>
-          <tr>
-            <td class="snss top red">
-              <a href="http://lambdadelta.info/specification.html#v1">Version 1</a>
-            </td>
-            <td class="snsn top red">"basic_1"</td>
-            <td class="snsn top red">
-              <a href="http://coq.inria.fr/">Coq 7.3.1</a>
-            </td>
-            <td class="snsn top red" />
-            <td class="snsn top red">May 2004</td>
-            <td class="snsn top red">December 2005</td>
-            <td class="snsn top red">November 2006</td>
-            <td class="snsn top red">May 2008</td>
-            <td class="sssn top red">
-              <a href="http://lambdadelta.info/documentation#ldV1a">V1a</a>
-              <a href="http://lambdadelta.info/documentation#ldJ1a">J1a</a>
-            </td>
-          </tr>
-        </tbody>
-      </table>
-    </div>
-    <div xmlns:ld="http://lambdadelta.info/" class="text">
+   </div><div class="text"><table cellpadding="4" cellspacing="0"><tbody><tr><td class="snns top capitalize italic gray">version</td><td class="snnn top capitalize italic gray">name</td><td class="snnn top capitalize italic gray">stage</td><td class="snnn top capitalize italic gray">developed with</td><td class="snnn top capitalize italic gray">started</td><td class="snnn top capitalize italic gray">announced</td><td class="snnn top capitalize italic gray">released</td><td class="snnn top capitalize italic gray">concluded</td><td class="ssnn top capitalize italic gray">references</td></tr><tr><td class="snns top yellow"><a href="http://lambdadelta.info/specification.html#v3">Version 3</a></td><td class="snnn top yellow">"basic_3"</td><td class="snnn top yellow"/><td class="snnn top yellow"/><td class="snnn top yellow"/><td class="snnn top yellow"/><td class="snnn top yellow"/><td class="snnn top yellow"/><td class="ssnn top yellow"><a href="http://lambdadelta.info/documentation#ldJ3a">J3a</a></td></tr><tr><td class="snns top orange"><a href="http://lambdadelta.info/specification.html#v2">Version 2</a></td><td class="snnn top orange">"basic_2"</td><td class="snns top orange">"A2"</td><td class="snnn top orange"><a href="http://matita.cs.unibo.it/">Matita 0.99.3</a></td><td class="snnn top orange">October 2015</td><td class="snnn top orange"/><td class="snnn top orange"/><td class="snnn top orange"/><td class="ssnn top orange"/></tr><tr><td class="nnns top orange"><br/></td><td class="nnnn top orange"><br/></td><td class="snns top orange">"A1"</td><td class="snnn top orange"><a href="http://matita.cs.unibo.it/">Matita 0.99.2</a></td><td class="snnn top orange">April 2011</td><td class="snnn top orange">June 2014</td><td class="snnn top orange">October 2014</td><td class="snnn top orange">August 2015</td><td class="ssnn top orange"><a href="http://lambdadelta.info/documentation#ldV2a">V2a</a><a href="http://lambdadelta.info/documentation#ldR2c">R2c</a></td></tr><tr><td class="snns top orange">Abandoned</td><td class="snnn top orange"/><td class="snnn top orange"/><td class="snnn top orange"><a href="http://coq.inria.fr/">Coq 7.3.1</a></td><td class="snnn top orange">March 2008</td><td class="snnn top orange"/><td class="snnn top orange"/><td class="snnn top orange">February 2011</td><td class="ssnn top orange"/></tr><tr><td class="snss top red"><a href="http://lambdadelta.info/specification.html#v1">Version 1</a></td><td class="snsn top red">"basic_1"</td><td class="snsn top red"/><td class="snsn top red"><a href="http://coq.inria.fr/">Coq 7.3.1</a></td><td class="snsn top red">May 2004</td><td class="snsn top red">December 2005</td><td class="snsn top red">November 2006</td><td class="snsn top red">May 2008</td><td class="sssn top red"><a href="http://lambdadelta.info/documentation#ldV1a">V1a</a><a href="http://lambdadelta.info/documentation#ldJ1a">J1a</a></td></tr></tbody></table></div><div class="text">
       Informational pages on the specifications are provided.
       Informational pages on the specifications are provided.
-   </div>
-    <ul xmlns:ld="http://lambdadelta.info/" id="notice1">
-      <li>
-        <span class="emph alpha">Notice on displayed numerical acounts:</span>
+   </div><ul id="notice1"><li><span class="emph alpha">Notice on displayed numerical acounts:</span>
        nodes are counted according to the "intrinsic complexity measure"
        [F. Guidi: "Procedural Representation of CIC Proof Terms"
        Journal of Automated Reasoning 44(1-2), Springer (February 2010), pp. 53-78].       
        nodes are counted according to the "intrinsic complexity measure"
        [F. Guidi: "Procedural Representation of CIC Proof Terms"
        Journal of Automated Reasoning 44(1-2), Springer (February 2010), pp. 53-78].       
-   </li>
-    </ul>
-    <ul xmlns:ld="http://lambdadelta.info/" id="notice2">
-      <li>
-        <span class="emph alpha">Notice on displayed logical structures:</span>
+   </li></ul><ul id="notice2"><li><span class="emph alpha">Notice on displayed logical structures:</span>
        from the logical standpoint, the source scripts are grouped in "planes"
        and these are grouped in "components";
        the notation for the relations or functions
        introduced in each script, is shown in parentheses (? are placeholders).
        from the logical standpoint, the source scripts are grouped in "planes"
        and these are grouped in "components";
        the notation for the relations or functions
        introduced in each script, is shown in parentheses (? are placeholders).
-   </li>
-    </ul>
-    <!-- VERSION 3 =========================================================== -->
-    <div xmlns:ld="http://lambdadelta.info/" class="head3sn" id="v3">
-      <img class="icon37" alt="[spacer]" title="lambdadelta butterfly" src="http://lambdadelta.info/images/b8.png" /> λδ version 3 (proposed)</div>
-    <div xmlns:ld="http://lambdadelta.info/" class="text">
+   </li></ul><!-- VERSION 3 =========================================================== --><div class="head3sn" id="v3"><img class="icon37" alt="[butterfly]" title="\lambda\delta butterfly" src="http://lambdadelta.info/images/b8.png"/> λδ version 3 (proposed)</div><div class="text">
        The formal specification of λδ version 3
        is forthcoming.
        The formal specification of λδ version 3
        is forthcoming.
-   </div>
-    <!-- VERSION 2 =========================================================== -->
-    <div xmlns:ld="http://lambdadelta.info/" class="head3sn" id="v2">
-      <img class="icon37" alt="[spacer]" title="lambdadelta butterfly" src="http://lambdadelta.info/images/b4.png" /> λδ version 2 (active)</div>
-    <div xmlns:ld="http://lambdadelta.info/" class="text">
+   </div><!-- VERSION 2 =========================================================== --><div class="head3sn" id="v2"><img class="icon37" alt="[butterfly]" title="\lambda\delta butterfly" src="http://lambdadelta.info/images/b4.png"/> λδ version 2 (active)</div><div class="text">
        The formal specification of λδ version 2
        is available in the following formats:
        The formal specification of λδ version 2
        is available in the following formats:
-   </div>
-    <ul xmlns:ld="http://lambdadelta.info/" id="source2">
-      <li>
-        <div class="text">
-          <a href="http://lambdadelta.info/download/lambdadelta_2A1.tar.gz">lambdadelta_2A1 for Matita 0.99.2</a>
+   </div><ul id="source2"><li><div class="text"><a href="http://lambdadelta.info/download/lambdadelta_2A1.tar.gz">lambdadelta_2A1 for Matita 0.99.2</a>
           (revised <span class="emph gamma">2014-10</span>).
           Source scripts.
           <a href="http://lambdadelta.info/documentation.html#ldR2c">Documentation (R2c)</a>.
           (revised <span class="emph gamma">2014-10</span>).
           Source scripts.
           <a href="http://lambdadelta.info/documentation.html#ldR2c">Documentation (R2c)</a>.
-      </div>
-        <div class="text">
+      </div><div class="text">
           The scripts are grouped in directories, first by part, then by component.
           The scripts are grouped in directories, first by part, then by component.
-      </div>
-        <div class="text">
-          <span class="emph alpha">Notice:</span>
+      </div><div class="text"><span class="emph alpha">Notice:</span>
           the scripts are checked by the latest version of Matita from
           <a href="http://matita.cs.unibo.it/download.shtml">HELM Subversion repository</a>
           at path &lt;trunk/matita/&gt;.
           the scripts are checked by the latest version of Matita from
           <a href="http://matita.cs.unibo.it/download.shtml">HELM Subversion repository</a>
           at path &lt;trunk/matita/&gt;.
-      </div>
-      </li>
-    </ul>
-    <div xmlns:ld="http://lambdadelta.info/" class="text">
+      </div></li></ul><div class="text">
        Informational pages on the parts of the specification:
        <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>.
        Informational pages on the parts of the specification:
        <a href="http://lambdadelta.info/ground_2.html">Background</a>,
        <a href="http://lambdadelta.info/basic_2.html">Core</a>,
        <a href="http://lambdadelta.info/apps_2.html">Applications</a>.
-   </div>
-    <!-- VERSION 1 =========================================================== -->
-    <div xmlns:ld="http://lambdadelta.info/" class="head3sn" id="v1">
-      <img class="icon37" alt="[spacer]" title="lambdadelta butterfly" src="http://lambdadelta.info/images/b6.png" /> λδ version 1 (superseded)</div>
-    <div xmlns:ld="http://lambdadelta.info/" class="text">
+   </div><!-- VERSION 1 =========================================================== --><div class="head3sn" id="v1"><img class="icon37" alt="[butterfly]" title="\lambda\delta butterfly" src="http://lambdadelta.info/images/b6.png"/> λδ version 1 (superseded)</div><div class="text">
        The formal specification of λδ version 1
        is available in the following formats:
        The formal specification of λδ version 1
        is available in the following formats:
-   </div>
-    <ul xmlns:ld="http://lambdadelta.info/" id="source1">
-      <li>
-        <div class="text">
-          <a href="http://lambdadelta.info/download/lambdadelta_1.tar.gz">lambdadelta_1 for Coq 7.3.1</a>
+   </div><ul id="source1"><li><div class="text"><a href="http://lambdadelta.info/download/lambdadelta_1.tar.gz">lambdadelta_1 for Coq 7.3.1</a>
           (revised <span class="emph delta">2015-09</span>).
           Source scripts.
           <a href="http://lambdadelta.info/documentation.html#ldJ1a">Documentation (J1a)</a>.
           (revised <span class="emph delta">2015-09</span>).
           Source scripts.
           <a href="http://lambdadelta.info/documentation.html#ldJ1a">Documentation (J1a)</a>.
-         <ul>
-            <li>
-              <span class="emph delta">2015 January 15.</span>
+         <ul><li class=""><span class="emph delta">2015 January 15.</span>
              17 new lemmas and former lemma "eq_nat_dec" renamed as "nat_dec_neg".
              17 new lemmas and former lemma "eq_nat_dec" renamed as "nat_dec_neg".
-         </li>
-          </ul>
-        </div>
-        <div class="text">
+         </li></ul></div><div class="text">
           The scripts are grouped in directories, one for each part.
           The scripts are grouped in directories, one for each part.
-      </div>
-      </li>
-    </ul>
-    <ul xmlns:ld="http://lambdadelta.info/" id="static1">
-      <li>
-        <a href="http://lambdadelta.info/static/matita/lambdadelta/">lambdadelta_1 for Matita 0.5</a>
+      </div></li></ul><ul id="static1"><li><a href="http://lambdadelta.info/static/matita/lambdadelta/">lambdadelta_1 for Matita 0.5</a>
        (revised <span class="emph delta">2011-09</span>).
        Static HTML pages generated by the <a href="http://helm.cs.unibo.it/">HELM</a> rendering engine.  
        (revised <span class="emph delta">2011-09</span>).
        Static HTML pages generated by the <a href="http://helm.cs.unibo.it/">HELM</a> rendering engine.  
-      <ul>
-          <li>
-            <a href="http://lambdadelta.info/static/matita/lambdadelta/basic_1/pr3/pr3/pr3_confluence.con.html">
+      <ul><li class=""><a href="http://lambdadelta.info/static/matita/lambdadelta/basic_1/pr3/pr3/pr3_confluence.con.html">
              Confluence of reduction</a>
           (Church-Rosser property).
              Confluence of reduction</a>
           (Church-Rosser property).
-      </li>
-          <li>
-            <a href="http://lambdadelta.info/static/matita/lambdadelta/basic_1/ty3/props/ty3_correct.con.html">
+      </li><li class=""><a href="http://lambdadelta.info/static/matita/lambdadelta/basic_1/ty3/props/ty3_correct.con.html">
              Correctness of types</a>.
              Correctness of types</a>.
-      </li>
-          <li>
-            <a href="http://lambdadelta.info/static/matita/lambdadelta/basic_1/ty3/props/ty3_unique.con.html">
+      </li><li class=""><a href="http://lambdadelta.info/static/matita/lambdadelta/basic_1/ty3/props/ty3_unique.con.html">
              Uniqueness of types up to conversion</a>.
              Uniqueness of types up to conversion</a>.
-      </li>
-          <li>
-            <a href="http://lambdadelta.info/static/matita/lambdadelta/basic_1/ty3/pr3/ty3_sred_pr3.con.html">
+      </li><li class=""><a href="http://lambdadelta.info/static/matita/lambdadelta/basic_1/ty3/pr3/ty3_sred_pr3.con.html">
              Subject reduction of the type assignment</a>.
              Subject reduction of the type assignment</a>.
-      </li>
-          <li>
-            <a href="http://lambdadelta.info/static/matita/lambdadelta/basic_1/ty3/arity_props/ty3_sn3.con.html">
+      </li><li class=""><a href="http://lambdadelta.info/static/matita/lambdadelta/basic_1/ty3/arity_props/ty3_sn3.con.html">
              Strong normalization of the typed terms</a>.
              Strong normalization of the typed terms</a>.
-      </li>
-          <li>
-            <a href="http://lambdadelta.info/static/matita/lambdadelta/basic_1/ty3/dec/ty3_inference.con.html">
+      </li><li class=""><a href="http://lambdadelta.info/static/matita/lambdadelta/basic_1/ty3/dec/ty3_inference.con.html">
              Decidability of the type inference problem</a>.
              Decidability of the type inference problem</a>.
-      </li>
-        </ul>
-      </li>
-    </ul>
-    <ul xmlns:ld="http://lambdadelta.info/" id="dynamic1">
-      <li>
-        <a href="http://mowgli.cs.unibo.it:58080/apply?keys=RT&amp;xmluri=http://helm.cs.unibo.it/helm//html/folder/index.html&amp;prop.media-type=text/html&amp;param.thmedia-type=text/html&amp;param.thkeys=T1%2CT2%2CL%2CE&amp;param.embedkeys=d_c%2CTC1%2CHC2%2CL&amp;param.thencoding=UTF-8&amp;prop.encoding=UTF-8&amp;prop.doctype-public=-//W3C//DTD%20XHTML%201.0%20Transitional//EN&amp;param.doctype-public=-//W3C//DTD%20XHTML%201.0%20Transitional//EN&amp;param.encoding=UTF-8&amp;param.media-type=text/html&amp;param.keys=d_c%2CC1%2CHC2%2CL&amp;profile=default&amp;param.profile=default&amp;param.CICURI=theory:/matita/lambdadelta/">
+      </li></ul></li></ul><ul id="dynamic1"><li><a href="http://mowgli.cs.unibo.it:58080/apply?keys=RT&amp;xmluri=http://helm.cs.unibo.it/helm//html/folder/index.html&amp;prop.media-type=text/html&amp;param.thmedia-type=text/html&amp;param.thkeys=T1%2CT2%2CL%2CE&amp;param.embedkeys=d_c%2CTC1%2CHC2%2CL&amp;param.thencoding=UTF-8&amp;prop.encoding=UTF-8&amp;prop.doctype-public=-//W3C//DTD%20XHTML%201.0%20Transitional//EN&amp;param.doctype-public=-//W3C//DTD%20XHTML%201.0%20Transitional//EN&amp;param.encoding=UTF-8&amp;param.media-type=text/html&amp;param.keys=d_c%2CC1%2CHC2%2CL&amp;profile=default&amp;param.profile=default&amp;param.CICURI=theory:/matita/lambdadelta/">
           lambdadelta_1 for Matita 0.5</a>
        (revised <span class="emph delta">2011-09</span>).
        <a href="http://helm.cs.unibo.it/">HELM</a> directory.
           lambdadelta_1 for Matita 0.5</a>
        (revised <span class="emph delta">2011-09</span>).
        <a href="http://helm.cs.unibo.it/">HELM</a> directory.
-      <span class="emph alpha">Notice: the HELM rendering engine is offline.</span>
-      </li>
-    </ul>
-    <div xmlns:ld="http://lambdadelta.info/" class="text">
+      <span class="emph alpha">Notice: the HELM rendering engine is offline.</span></li></ul><div class="text">
        Informational pages on the parts of the specification:
        <a href="http://lambdadelta.info/ground_1.html">Background</a>,
        <a href="http://lambdadelta.info/basic_1.html">Core</a>.
        Informational pages on the parts of the specification:
        <a href="http://lambdadelta.info/ground_1.html">Background</a>,
        <a href="http://lambdadelta.info/basic_1.html">Core</a>.
-   </div>
-    <div class="spacer">
-      <img class="rule" alt="[Spacer]" title="lambdadelta rainbow rule" src="http://lambdadelta.info/images/rainbow.png" />
-    </div>
-    <div xmlns:ld="http://lambdadelta.info/" class="spacer">
-      <br />
-    </div>
-    <div xmlns:ld="http://lambdadelta.info/" class="spacer">
-      <a href="http://validator.w3.org/check?uri=referer">
-        <img class="w3c" alt="[Valid XHTML 1.1]" title="Valid XHTML 1.1" src="http://www.w3.org/Icons/valid-xhtml11-blue" />
-      </a>
-      <a href="http://jigsaw.w3.org/css-validator/check/referer">
-        <img class="w3c" alt="[Valid CSS level 2]" title="Valid CSS level 2" src="http://www.w3.org/Icons/valid-css2-blue" />
-      </a>
-      <a href="http://www.w3.org/XML/">
-        <img class="w3c" alt="[Generated from XML via XSL]" title="Generated from XML via XSL" src="http://lambdadelta.info/images/xml_xsl2.png" />
-      </a>
-      <a href="http://www.w3.org/Graphics/PNG/">
-        <img class="w3c" alt="[PNG used here]" title="PNG used here" src="http://lambdadelta.info/images/PNGnow2.png" />
-      </a>
-      <a href="http://www.anybrowser.org/campaign/">
-        <img class="w3c" alt="[Viewable with any browser]" title="Viewable with any browser" src="http://www.anybrowser.org/campaign/bvgraphics/abtfile.png" />
-      </a>
-    </div>
-    <div xmlns:ld="http://lambdadelta.info/" class="spacer">
-      <br />
-    </div>
-    <div xmlns:ld="http://lambdadelta.info/" class="spacer">Last update: Sun, 07 Feb 2016 18:51:17 +0100</div>
-  </body>
-</html>
+   </div><div class="spacer"><img class="rule" alt="[Spacer]" title="\lambda\delta rainbow rule" src="http://lambdadelta.info/images/rainbow.png"/></div><div class="spacer"><br/></div><div class="spacer"><a href="http://validator.w3.org/check?uri=referer"><img class="w3c" alt="[Valid XHTML 1.1]" title="Valid XHTML 1.1" src="http://www.w3.org/Icons/valid-xhtml11-blue"/></a><a href="http://jigsaw.w3.org/css-validator/check/referer"><img class="w3c" alt="[Valid CSS level 2]" title="Valid CSS level 2" src="http://www.w3.org/Icons/valid-css2-blue"/></a><a href="http://www.w3.org/XML/"><img class="w3c" alt="[Generated from XML via XSL]" title="Generated from XML via XSL" src="http://lambdadelta.info/images/xml_xsl2.png"/></a><a href="http://www.w3.org/Graphics/PNG/"><img class="w3c" alt="[PNG used here]" title="PNG used here" src="http://lambdadelta.info/images/PNGnow2.png"/></a><a href="http://www.anybrowser.org/campaign/"><img class="w3c" alt="[Viewable with any browser]" title="Viewable with any browser" src="http://www.anybrowser.org/campaign/bvgraphics/abtfile.png"/></a></div><div class="spacer"><br/></div><div class="spacer">Last update: Thu, 09 Mar 2017 13:38:16 +0100</div></body></html>