- xhtbl: we added the real concatenation of cells (without added spaces)

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

index 1364b8cfa31eb412475c55aa80d3b44ac87aa2da..9fc581eb9f9323556dc236ad97e45970e7392a11 100644 (file)
--- a/helm/www/lambdadelta/apps_2.html
+++ b/helm/www/lambdadelta/apps_2.html
@@ -1,62 +1,196 @@
  <?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" xmlns:ld="http://lambdadelta.info/" dir="ltr" lang="en-us">
+<html xmlns="http://www.w3.org/1999/xhtml" dir="ltr" lang="en-us">
    <head>
    <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="applications of lambdadelta version 2"/>
-    <title>applications of lambdadelta version 2</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"/>
+    <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="applications of \lambda\delta version 2" />
+    <title>applications of \lambda\delta version 2</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>
    </head>
-  <body lang="en-US"><div class="spacer"><a href="http://lambdadelta.info/"><img class="icon32" alt="[lambdadelta home]" title="lambdadelta home" src="http://lambdadelta.info/images/crux_32.png"/></a></div><div class="head1">cic:/matita/lambdadelta/apps_2/ (applications of λδ version 2)</div><div class="spacer"><img class="rule" alt="[Spacer]" title="lambdadelta rainbow rule" src="http://lambdadelta.info/images/rainbow.png"/></div>
-   <div class="head2">Contents of the Specification</div>
-   <div class="text">This specification comprises a collection of checked
+  <body lang="en-US">
+    <div class="spacer">
+      <a href="http://lambdadelta.info/">
+        <img class="icon32" alt="[lambdadelta home]" title="lambdadelta home" src="http://lambdadelta.info/images/crux_32.png" />
+      </a>
+    </div>
+    <div class="head1">cic:/matita/lambdadelta/apps_2/ (applications of λδ 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="head2sn" id="">Contents of the Specification</div>
+   <div xmlns:ld="http://lambdadelta.info/" class="text">This specification comprises a collection of checked
           applications of λδ version 2.
           applications of λδ version 2.
-        In particular it contains the components below.
+         In particular it contains the components below.
     </div>
     </div>
-   <ul><li><span class="date">MLTT1.</span>
+   <ul xmlns:ld="http://lambdadelta.info/">
+      <li>
+        <span class="date">MLTT1.</span>
           Martin-Löf's Type Theory with one universe
           Martin-Löf's Type Theory with one universe
-        using λδ as theory of expressions.
-   </li></ul>
-   <ul><li><span class="date">Functional.</span>
+         using λδ as theory of expressions.
+   </li>
+    </ul>
+   <ul xmlns:ld="http://lambdadelta.info/">
+      <li>
+        <span class="date">Functional.</span>
           The validation algorithm for λδ as implemented in
           The validation algorithm for λδ as implemented in
-        <a href="http://lambdadelta.info/implementation.html#helena">Helena 0.8</a>.
-   </li></ul>
-   
-   <div class="head2">Summary of the Specification</div>
-   <div class="text">Here is a numerical acount of the specification's contents
+         <a href="http://lambdadelta.info/implementation.html#helena">Helena 0.8</a>.
+   </li>
+    </ul>
+
+   <div xmlns:ld="http://lambdadelta.info/" class="head2sn" id="">Summary of the Specification</div>
+   <div xmlns:ld="http://lambdadelta.info/" class="text">Here is a numerical acount of the specification's contents
           and its timeline.
           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>
-   <div class="text"><table cellpadding="4" cellspacing="0"><tbody><tr><td class="snns component grey">category</td><td class="snns plane grey">objects</td><td class="snnn number grey"><br/></td><td class="snnn plane grey"><br/></td><td class="snnn number grey"><br/></td><td class="snnn plane grey"><br/></td><td class="ssnn number grey"><br/></td></tr><tr><td class="snns component cyan">sizes</td><td class="snns plane cyan">files</td><td class="snnn number cyan">5</td><td class="snns plane cyan">characters</td><td class="snnn number cyan">5613</td><td class="snns plane cyan">nodes</td><td class="ssnn number cyan">10024</td></tr><tr><td class="snns component green">propositions</td><td class="snns plane green">theorems</td><td class="snnn number green">4</td><td class="snns plane green">lemmas</td><td class="snnn number green">1</td><td class="snns plane green">total</td><td class="ssnn number green">5</td></tr><tr><td class="snss component yellow">concepts</td><td class="snss plane yellow">declared</td><td class="snsn number yellow">3</td><td class="snss plane yellow">defined</td><td class="snsn number yellow">10</td><td class="snss plane yellow">total</td><td class="sssn number yellow">13</td></tr></tbody></table></div>
-   <ul><li><span class="date">2012 February 24.</span>
+   <div xmlns:ld="http://lambdadelta.info/" class="text">
+      <table cellpadding="4" cellspacing="0">
+        <tbody>
+          <tr>
+            <td class="snns component gray">category</td>
+            <td class="snns plane gray">objects</td>
+            <td class="snnn number gray">
+              <br />
+            </td>
+            <td class="snnn plane gray">
+              <br />
+            </td>
+            <td class="snnn number gray">
+              <br />
+            </td>
+            <td class="snnn plane gray">
+              <br />
+            </td>
+            <td class="ssnn number gray">
+              <br />
+            </td>
+          </tr>
+          <tr>
+            <td class="snns component cyan">sizes</td>
+            <td class="snns plane cyan">files</td>
+            <td class="snnn number cyan">4</td>
+            <td class="snns plane cyan">characters</td>
+            <td class="snnn number cyan">2567</td>
+            <td class="snns plane cyan">nodes</td>
+            <td class="ssnn number cyan">3637</td>
+          </tr>
+          <tr>
+            <td class="snns component green">propositions</td>
+            <td class="snns plane green">theorems</td>
+            <td class="snnn number green">2</td>
+            <td class="snns plane green">lemmas</td>
+            <td class="snnn number green">1</td>
+            <td class="snns plane green">total</td>
+            <td class="ssnn number green">3</td>
+          </tr>
+          <tr>
+            <td class="snss component yellow">concepts</td>
+            <td class="snss plane yellow">declared</td>
+            <td class="snsn number yellow">3</td>
+            <td class="snss plane yellow">defined</td>
+            <td class="snsn number yellow">9</td>
+            <td class="snss plane yellow">total</td>
+            <td class="sssn number yellow">12</td>
+          </tr>
+        </tbody>
+      </table>
+    </div>
+   <ul xmlns:ld="http://lambdadelta.info/">
+      <li>
+        <span class="date">2012 February 24.</span>
           The Applications directory is started.
           The Applications directory is started.
-   </li></ul>
-   <ul><li><span class="date">2011 December 20.</span>
+   </li>
+    </ul>
+   <ul xmlns:ld="http://lambdadelta.info/">
+      <li>
+        <span class="date">2011 December 20.</span>
           The Functional component is started
           The Functional component is started
-        inside the specification of λδ version 2.
-   </li></ul>
-   <ul><li><span class="date">2011 December 12.</span>
+         inside the specification of λδ version 2.
+   </li>
+    </ul>
+   <ul xmlns:ld="http://lambdadelta.info/">
+      <li>
+        <span class="date">2011 December 12.</span>
           The MLTT1 component is started.
           The MLTT1 component is started.
-   </li></ul>
+   </li>
+    </ul>
  
  
-   <div class="head2">Logical Structure of the Specification</div>
-   <div class="text">The source files are grouped in planes and components
+   <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.
           Each component contains its own notation file.
           according to the following table.
           Each component contains its own notation file.
-        The notation for the relations or functions introduced in each file
-        is shown in parentheses (? are placeholders).
+         The notation for the relations or functions introduced in each file
+         is shown in parentheses (? are placeholders).
     </div>
     </div>
-   <div class="text"><table cellpadding="4" cellspacing="0"><tbody><tr><td class="snns component grey">component</td><td class="snns plane grey">plane</td><td class="snns file grey">files</td><td class="ssnn file grey"><br/></td></tr><tr><td class="snns component orange">MLTT1</td><td class="snns plane orange"/><td class="snns file orange">genv_primitive</td><td class="ssnn file orange">judgement</td></tr><tr><td class="snns component red">functional</td><td class="snns plane red">reduction and type machine</td><td class="snns file red">rtm</td><td class="ssnn file red">rtm_step ( ? ⇨ ? )</td></tr><tr><td class="nnss component red"><br/></td><td class="snss plane red">unfold</td><td class="snss file red">lift ( ↑[?,?] ? )</td><td class="sssn file red">subst ( [?←?] ? )</td></tr></tbody></table></div>
+   <div xmlns:ld="http://lambdadelta.info/" class="text">
+      <table cellpadding="4" cellspacing="0">
+        <tbody>
+          <tr>
+            <td class="snns component gray">component</td>
+            <td class="snns plane gray">plane</td>
+            <td class="snns file gray">files</td>
+            <td class="ssnn file gray">
+              <br />
+            </td>
+          </tr>
+          <tr>
+            <td class="snns component red">functional</td>
+            <td class="snns plane red">reduction and type machine</td>
+            <td class="snns file red">rtm</td>
+            <td class="ssnn file red">rtm_step ( ? ⇨ ? )</td>
+          </tr>
+          <tr>
+            <td class="nnss component red">
+              <br />
+            </td>
+            <td class="snss plane red">relocation</td>
+            <td class="snss file red">lift ( ↑[?,?] ? )</td>
+            <td class="sssn file red">
+              <br />
+            </td>
+          </tr>
+        </tbody>
+      </table>
+    </div>
  
  
-   <div class="head2">Physical Structure of the Specification</div>
-   <div class="text">The source files are grouped in directories,
+   <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>
           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><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: 2013-02-07T20:53:29+01:00</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, 06 Jul 2014 20:28:30 +0200</div>
  </body>
  </html>
  </body>
  </html>