]> matita.cs.unibo.it Git - helm.git/commitdiff
projects / helm.git / commitdiff
? search:
summary | shortlog | log | commit | commitdiff | tree
raw | patch | inline | side by side (parent: 65c5a37)
- xslt and Makefile improved, web pages regenerated
authorFerruccio Guidi <ferruccio.guidi@unibo.it>
Mon, 11 Mar 2013 12:59:19 +0000 (12:59 +0000)
committerFerruccio Guidi <ferruccio.guidi@unibo.it>
Mon, 11 Mar 2013 12:59:19 +0000 (12:59 +0000)
helm/www/lambdadelta/BTM.html patch | blob | history
helm/www/lambdadelta/Makefile patch | blob | history
helm/www/lambdadelta/apps_2.html patch | blob | history
helm/www/lambdadelta/basic_2.html patch | blob | history
helm/www/lambdadelta/xslt/ld_web.xsl patch | blob | history
helm/www/lambdadelta/xslt/ld_web_root.xsl patch | blob | history
helm/www/lambdadelta/xslt/lddl_library.xsl patch | blob | history

diff --git a/helm/www/lambdadelta/BTM.html b/helm/www/lambdadelta/BTM.html
index 4736b1932f95d0958279ddbe5bb29a9b9dd36d43..c78039c576ee931fbb03c378882c3d047b719421 100644 (file)
--- a/helm/www/lambdadelta/BTM.html
+++ b/helm/www/lambdadelta/BTM.html
@@ -1,25 +1,228 @@
 <?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="BTM"/>
+    <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="BTM" />
     <title>BTM</title>
     <title>BTM</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"/>
+    <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/BTM/</div><div class="spacer"><img class="rule" alt="[Spacer]" title="lambdadelta rainbow rule" src="http://lambdadelta.info/images/rainbow.png"/></div>
-   <div class="head2">Character classes</div>
-   <div class="text">This table shows how the first 45 positive integers
+  <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/BTM/</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="head2">Character classes</div>
+   <div xmlns:ld="http://lambdadelta.info/" class="text">This table shows how the first 45 positive integers
          are distributed in the four classes.
    </div>
          are distributed in the four classes.
    </div>
-   <div class="text"><table cellpadding="4" cellspacing="0"><tbody><tr><td class="snns component grey">class</td><td class="snns text grey">contents</td><td class="snnn number grey"><br/></td><td class="snnn number grey"><br/></td><td class="snnn number grey"><br/></td><td class="snnn number grey"><br/></td><td class="snnn number grey"><br/></td><td class="snnn number grey"><br/></td><td class="snnn number grey"><br/></td><td class="snnn number grey"><br/></td><td class="snnn number grey"><br/></td><td class="snnn number grey"><br/></td><td class="snnn number grey"><br/></td><td class="snnn number grey"><br/></td><td class="snnn number grey"><br/></td><td class="snnn number grey"><br/></td><td class="ssnn number grey"><br/></td></tr><tr><td class="snns component orange">p</td><td class="snns text orange"><br/></td><td class="snnn number orange">1</td><td class="snnn number orange">4</td><td class="snnn number orange">7</td><td class="snnn number orange">10</td><td class="snnn number orange">13</td><td class="snnn number orange">16</td><td class="snnn number orange">19</td><td class="snnn number orange">22</td><td class="snnn number orange">25</td><td class="snnn number orange">28</td><td class="snnn number orange">31</td><td class="snnn number orange">34</td><td class="snnn number orange">37</td><td class="snnn number orange">40</td><td class="ssnn number orange">43</td></tr><tr><td class="snns component green">q</td><td class="snns text green"><br/></td><td class="snnn number green">5</td><td class="snnn number green">11</td><td class="snnn number green">15</td><td class="snnn number green">17</td><td class="snnn number green">23</td><td class="snnn number green">29</td><td class="snnn number green">33</td><td class="snnn number green">35</td><td class="snnn number green">41</td><td class="snnn number green">45</td><td class="snnn number green"><br/></td><td class="snnn number green"><br/></td><td class="snnn number green"><br/></td><td class="snnn number green"><br/></td><td class="ssnn number green"><br/></td></tr><tr><td class="snns component sky">s</td><td class="snns text sky"><br/></td><td class="snnn number sky">2</td><td class="snnn number sky">6</td><td class="snnn number sky">8</td><td class="snnn number sky">14</td><td class="snnn number sky">18</td><td class="snnn number sky">20</td><td class="snnn number sky">24</td><td class="snnn number sky">26</td><td class="snnn number sky">32</td><td class="snnn number sky">38</td><td class="snnn number sky">42</td><td class="snnn number sky">44</td><td class="snnn number sky"><br/></td><td class="snnn number sky"><br/></td><td class="ssnn number sky"><br/></td></tr><tr><td class="snss component magenta">t</td><td class="snss text magenta"><br/></td><td class="snsn number magenta">3</td><td class="snsn number magenta">9</td><td class="snsn number magenta">12</td><td class="snsn number magenta">21</td><td class="snsn number magenta">27</td><td class="snsn number magenta">30</td><td class="snsn number magenta">36</td><td class="snsn number magenta">39</td><td class="snsn number magenta"><br/></td><td class="snsn number magenta"><br/></td><td class="snsn number magenta"><br/></td><td class="snsn number magenta"><br/></td><td class="snsn number magenta"><br/></td><td class="snsn number magenta"><br/></td><td class="sssn number magenta"><br/></td></tr></tbody></table></div>
+   <div xmlns:ld="http://lambdadelta.info/" class="text">
+      <table cellpadding="4" cellspacing="0">
+        <tbody>
+          <tr>
+            <td class="snns component grey">class</td>
+            <td class="snns text grey">contents</td>
+            <td class="snnn number grey">
+              <br />
+            </td>
+            <td class="snnn number grey">
+              <br />
+            </td>
+            <td class="snnn number grey">
+              <br />
+            </td>
+            <td class="snnn number grey">
+              <br />
+            </td>
+            <td class="snnn number grey">
+              <br />
+            </td>
+            <td class="snnn number grey">
+              <br />
+            </td>
+            <td class="snnn number grey">
+              <br />
+            </td>
+            <td class="snnn number grey">
+              <br />
+            </td>
+            <td class="snnn number grey">
+              <br />
+            </td>
+            <td class="snnn number grey">
+              <br />
+            </td>
+            <td class="snnn number grey">
+              <br />
+            </td>
+            <td class="snnn number grey">
+              <br />
+            </td>
+            <td class="snnn number grey">
+              <br />
+            </td>
+            <td class="snnn number grey">
+              <br />
+            </td>
+            <td class="ssnn number grey">
+              <br />
+            </td>
+          </tr>
+          <tr>
+            <td class="snns component orange">p</td>
+            <td class="snns text orange">
+              <br />
+            </td>
+            <td class="snnn number orange">1</td>
+            <td class="snnn number orange">4</td>
+            <td class="snnn number orange">7</td>
+            <td class="snnn number orange">10</td>
+            <td class="snnn number orange">13</td>
+            <td class="snnn number orange">16</td>
+            <td class="snnn number orange">19</td>
+            <td class="snnn number orange">22</td>
+            <td class="snnn number orange">25</td>
+            <td class="snnn number orange">28</td>
+            <td class="snnn number orange">31</td>
+            <td class="snnn number orange">34</td>
+            <td class="snnn number orange">37</td>
+            <td class="snnn number orange">40</td>
+            <td class="ssnn number orange">43</td>
+          </tr>
+          <tr>
+            <td class="snns component green">q</td>
+            <td class="snns text green">
+              <br />
+            </td>
+            <td class="snnn number green">5</td>
+            <td class="snnn number green">11</td>
+            <td class="snnn number green">15</td>
+            <td class="snnn number green">17</td>
+            <td class="snnn number green">23</td>
+            <td class="snnn number green">29</td>
+            <td class="snnn number green">33</td>
+            <td class="snnn number green">35</td>
+            <td class="snnn number green">41</td>
+            <td class="snnn number green">45</td>
+            <td class="snnn number green">
+              <br />
+            </td>
+            <td class="snnn number green">
+              <br />
+            </td>
+            <td class="snnn number green">
+              <br />
+            </td>
+            <td class="snnn number green">
+              <br />
+            </td>
+            <td class="ssnn number green">
+              <br />
+            </td>
+          </tr>
+          <tr>
+            <td class="snns component sky">s</td>
+            <td class="snns text sky">
+              <br />
+            </td>
+            <td class="snnn number sky">2</td>
+            <td class="snnn number sky">6</td>
+            <td class="snnn number sky">8</td>
+            <td class="snnn number sky">14</td>
+            <td class="snnn number sky">18</td>
+            <td class="snnn number sky">20</td>
+            <td class="snnn number sky">24</td>
+            <td class="snnn number sky">26</td>
+            <td class="snnn number sky">32</td>
+            <td class="snnn number sky">38</td>
+            <td class="snnn number sky">42</td>
+            <td class="snnn number sky">44</td>
+            <td class="snnn number sky">
+              <br />
+            </td>
+            <td class="snnn number sky">
+              <br />
+            </td>
+            <td class="ssnn number sky">
+              <br />
+            </td>
+          </tr>
+          <tr>
+            <td class="snss component magenta">t</td>
+            <td class="snss text magenta">
+              <br />
+            </td>
+            <td class="snsn number magenta">3</td>
+            <td class="snsn number magenta">9</td>
+            <td class="snsn number magenta">12</td>
+            <td class="snsn number magenta">21</td>
+            <td class="snsn number magenta">27</td>
+            <td class="snsn number magenta">30</td>
+            <td class="snsn number magenta">36</td>
+            <td class="snsn number magenta">39</td>
+            <td class="snsn number magenta">
+              <br />
+            </td>
+            <td class="snsn number magenta">
+              <br />
+            </td>
+            <td class="snsn number magenta">
+              <br />
+            </td>
+            <td class="snsn number magenta">
+              <br />
+            </td>
+            <td class="snsn number magenta">
+              <br />
+            </td>
+            <td class="snsn number magenta">
+              <br />
+            </td>
+            <td class="sssn number magenta">
+              <br />
+            </td>
+          </tr>
+        </tbody>
+      </table>
+    </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-03-09T23:27:52+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: Mon, 11 Mar 2013 13:47:08 +0100</div>
 </body>
 </html>
 </body>
 </html>
diff --git a/helm/www/lambdadelta/Makefile b/helm/www/lambdadelta/Makefile
index 0da13bb383983d363cceae09549166c85a496ba3..3a34b41d8e159e06386e18f41105c981181d0873 100644 (file)
--- a/helm/www/lambdadelta/Makefile
+++ b/helm/www/lambdadelta/Makefile
@@ -6,7 +6,6 @@ TAGS = www up \
        install-jed install-bib \
 
 LDURL   = http://lambdadelta.info/
        install-jed install-bib \
 
 LDURL   = http://lambdadelta.info/
-LDDLURL = $(LDURL)static/lddl
 
 HOMEDIR = .
 ETCDIR   = etc
 
 HOMEDIR = .
 ETCDIR   = etc
@@ -44,10 +43,25 @@ XMLS = brg_si/grundlagen/l/not.ld.xml \
 LDWEB = ld_web.xsl ld_web_root.xsl ld_web_library.xsl
 
 XMLLINT = xmllint --noout
 LDWEB = ld_web.xsl ld_web_root.xsl ld_web_library.xsl
 
 XMLLINT = xmllint --noout
-XSLT    = xsltproc
+XSLT    = xalan
 XHTBL   = $(XHTBLDIR)/xhtbl.native
 
 XHTBL   = $(XHTBLDIR)/xhtbl.native
 
-%.html: BASEURL = --stringparam baseurl $(LDURL)
+ifeq ($(XSLT), xsltproc)
+   XSLT_PARAM := --param
+   XSLT_OUT   := -o
+   XSLT_XSL   :=
+   XSLT_IN    :=
+endif
+
+ifeq ($(XSLT), xalan)
+   XSLT_PARAM := -param
+   XSLT_OUT   := -out
+   XSLT_XSL   := -xsl
+   XSLT_IN    := -in
+   XSLT       += -indent 2
+endif
+
+XSLT += $(XSLT_PARAM) baseurl '"$(LDURL)"' $(XSLT_PARAM) date '"$(shell date -R)"'
 
 define HTML_TEMPLATE
    HTML_$(2)  = $$(HOMEDIR)/$(2).html
 
 define HTML_TEMPLATE
    HTML_$(2)  = $$(HOMEDIR)/$(2).html
@@ -55,7 +69,7 @@ define HTML_TEMPLATE
 
    $$(HTML_$(2)): $(1) $$(XSLS) $$(LDWEB:%=$$(XSLTDIR)/%)
        @echo "  XSLT $$(notdir $$<)"
 
    $$(HTML_$(2)): $(1) $$(XSLS) $$(LDWEB:%=$$(XSLTDIR)/%)
        @echo "  XSLT $$(notdir $$<)"
-       $$(H)$$(XSLT) -o $$@ $$(BASEURL) $$(XSLTDIR)/ld_web.xsl $$<
+       $$(H)$$(XSLT) $$(XSLT_OUT) $$@ $$(XSLT_XSL) $$(XSLTDIR)/ld_web.xsl $$(XSLT_IN) $$<
 endef
 
 ifeq ($(MAKECMDGOALS), www)
 endef
 
 ifeq ($(MAKECMDGOALS), www)
@@ -114,12 +128,10 @@ up:
        @echo "  UPDATE $(REMOTE):$(RDIR)"
        $(H)ssh $(REMOTE) "svn up $(RDIR)"
 
        @echo "  UPDATE $(REMOTE):$(RDIR)"
        $(H)ssh $(REMOTE) "svn up $(RDIR)"
 
-%.ld: BASEURL = --stringparam baseurl $(LDDLURL)
-
 %.ld:
        @echo "  XSLT $@"
        $(H)mkdir -p $(HTMLDIR)/$(@D)
 %.ld:
        @echo "  XSLT $@"
        $(H)mkdir -p $(HTMLDIR)/$(@D)
-       $(H)$(XSLT) -o $(HTMLDIR)/$@.html $(BASEURL) $(XSLTDIR)/lddl.xsl $(XMLDIR)/$@.xml
+       $(H)$(XSLT) $(XSLT_OUT) $(HTMLDIR)/$@.html $(XSLT_XSL) $(XSLTDIR)/lddl.xsl $(XSLT_IN) $(XMLDIR)/$@.xml
 
 %.ldc:
        @echo "  SKIP $@"
 
 %.ldc:
        @echo "  SKIP $@"
diff --git a/helm/www/lambdadelta/apps_2.html b/helm/www/lambdadelta/apps_2.html
index 20e4c26bdcb2dbfbaf368a3c891d88803662b907..975779b5b3e248488261feb01fb14fd96ab2c183 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"/>
+    <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>
     <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"/>
+    <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="head2">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="head2">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.
    </div>
          and its timeline.
    </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">9842</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 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" />
+          </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 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="head2">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 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 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="head2">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-03-09T23:27:52+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: Mon, 11 Mar 2013 13:47:08 +0100</div>
 </body>
 </html>
 </body>
 </html>
diff --git a/helm/www/lambdadelta/basic_2.html b/helm/www/lambdadelta/basic_2.html
index 3955a057459b0ef7f4c297e492f4c705c749a301..eb181a3ee3f03ecdb06c2591641e3997f9c7a045 100644 (file)
--- a/helm/www/lambdadelta/basic_2.html
+++ b/helm/www/lambdadelta/basic_2.html
@@ -1,88 +1,1374 @@
 <?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="lambdadelta version 2"/>
+    <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="lambdadelta version 2" />
     <title>lambdadelta version 2</title>
     <title>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"/>
+    <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/basic_2/ (λδ 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">System's Syntax and Behavior</div>
-   <div class="text">This is a summary of the "block structure"
+  <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/basic_2/ (λδ 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="head2">System's Syntax and Behavior</div>
+   <div xmlns:ld="http://lambdadelta.info/" class="text">This is a summary of the "block structure"
          of the System's syntactic items and reductions.
    </div>
          of the System's syntactic items and reductions.
    </div>
-   <div class="text"><table cellpadding="4" cellspacing="0"><tbody><tr><td class="snns text grey">domain</td><td class="snns plane grey">block</td><td class="snns text grey">leader</td><td class="snns text grey">applicator (with →θ)*</td><td class="snns text grey">reduction</td><td class="snns text grey">→ζ *</td><td class="ssns text grey">reference *</td></tr><tr><td class="snns text">{X | Γ ⊢ X : W}</td><td class="snns plane wine">local typed abstraction *</td><td class="snns text wine">Γ ⊢ +λW</td><td class="snns text wine">ⓐV</td><td class="snns text wine">→β</td><td class="snns text wine">no</td><td class="ssns text wine">#i</td></tr><tr><td class="nnns text"><br/></td><td class="snns plane magenta">local typed declaration **</td><td class="snns text magenta">Γ ⊢ -λW</td><td class="snns text magenta">ⓐV</td><td class="snns text magenta">→β</td><td class="snns text magenta">no</td><td class="ssns text magenta">#i</td></tr><tr><td class="nnns text"><br/></td><td class="snns plane prune">global typed declaration ***</td><td class="snns text prune">Γ ⊢ pλW</td><td class="snns text prune">no</td><td class="snns text prune">no</td><td class="snns text prune">no</td><td class="ssns text prune">$p</td></tr><tr><td class="nnns text"><br/></td><td class="snns plane blue">native type annotation *</td><td class="snns text blue">Γ ⊢ ⓝW</td><td class="snns text blue">no</td><td class="snns text blue">no</td><td class="snns text blue">yes</td><td class="ssns text blue">no</td></tr><tr><td class="snns text">{X | Γ ⊢ X = V}</td><td class="snns plane sky">local abbreviation *</td><td class="snns text sky">Γ ⊢ +δV</td><td class="snns text sky">no</td><td class="snns text sky">local →δ</td><td class="snns text sky">yes</td><td class="ssns text sky">#i</td></tr><tr><td class="nnns text"><br/></td><td class="snns plane cyan">local definition **</td><td class="snns text cyan">Γ ⊢ -δV</td><td class="snns text cyan">no</td><td class="snns text cyan">local →δ</td><td class="snns text cyan">no</td><td class="ssns text cyan">#i</td></tr><tr><td class="nnns text"><br/></td><td class="snns plane water">global definition ***</td><td class="snns text water">Γ ⊢ pδV</td><td class="snns text water">no</td><td class="snns text water">global →δ</td><td class="snns text water">no</td><td class="ssns text water">$p</td></tr><tr><td class="snss text">no</td><td class="snss plane green">sort ****</td><td class="snss text green">Γ ⊢ ⋆k</td><td class="snss text green">no</td><td class="snss text green">no</td><td class="snss text green">no</td><td class="ssss text green">no</td></tr></tbody></table></div>
-   <div class="text">* In terms only.
-        ** In terms and local environments only.
+   <div xmlns:ld="http://lambdadelta.info/" class="text">
+      <table cellpadding="4" cellspacing="0">
+        <tbody>
+          <tr>
+            <td class="snns text grey">domain</td>
+            <td class="snns plane grey">block</td>
+            <td class="snns text grey">leader</td>
+            <td class="snns text grey">applicator (with →θ)*</td>
+            <td class="snns text grey">reduction</td>
+            <td class="snns text grey">→ζ *</td>
+            <td class="ssns text grey">reference *</td>
+          </tr>
+          <tr>
+            <td class="snns text">{X | Γ ⊢ X : W}</td>
+            <td class="snns plane wine">local typed abstraction *</td>
+            <td class="snns text wine">Γ ⊢ +λW</td>
+            <td class="snns text wine">ⓐV</td>
+            <td class="snns text wine">→β</td>
+            <td class="snns text wine">no</td>
+            <td class="ssns text wine">#i</td>
+          </tr>
+          <tr>
+            <td class="nnns text">
+              <br />
+            </td>
+            <td class="snns plane magenta">local typed declaration **</td>
+            <td class="snns text magenta">Γ ⊢ -λW</td>
+            <td class="snns text magenta">ⓐV</td>
+            <td class="snns text magenta">→β</td>
+            <td class="snns text magenta">no</td>
+            <td class="ssns text magenta">#i</td>
+          </tr>
+          <tr>
+            <td class="nnns text">
+              <br />
+            </td>
+            <td class="snns plane prune">global typed declaration ***</td>
+            <td class="snns text prune">Γ ⊢ pλW</td>
+            <td class="snns text prune">no</td>
+            <td class="snns text prune">no</td>
+            <td class="snns text prune">no</td>
+            <td class="ssns text prune">$p</td>
+          </tr>
+          <tr>
+            <td class="nnns text">
+              <br />
+            </td>
+            <td class="snns plane blue">native type annotation *</td>
+            <td class="snns text blue">Γ ⊢ ⓝW</td>
+            <td class="snns text blue">no</td>
+            <td class="snns text blue">no</td>
+            <td class="snns text blue">yes</td>
+            <td class="ssns text blue">no</td>
+          </tr>
+          <tr>
+            <td class="snns text">{X | Γ ⊢ X = V}</td>
+            <td class="snns plane sky">local abbreviation *</td>
+            <td class="snns text sky">Γ ⊢ +δV</td>
+            <td class="snns text sky">no</td>
+            <td class="snns text sky">local →δ</td>
+            <td class="snns text sky">yes</td>
+            <td class="ssns text sky">#i</td>
+          </tr>
+          <tr>
+            <td class="nnns text">
+              <br />
+            </td>
+            <td class="snns plane cyan">local definition **</td>
+            <td class="snns text cyan">Γ ⊢ -δV</td>
+            <td class="snns text cyan">no</td>
+            <td class="snns text cyan">local →δ</td>
+            <td class="snns text cyan">no</td>
+            <td class="ssns text cyan">#i</td>
+          </tr>
+          <tr>
+            <td class="nnns text">
+              <br />
+            </td>
+            <td class="snns plane water">global definition ***</td>
+            <td class="snns text water">Γ ⊢ pδV</td>
+            <td class="snns text water">no</td>
+            <td class="snns text water">global →δ</td>
+            <td class="snns text water">no</td>
+            <td class="ssns text water">$p</td>
+          </tr>
+          <tr>
+            <td class="snss text">no</td>
+            <td class="snss plane green">sort ****</td>
+            <td class="snss text green">Γ ⊢ ⋆k</td>
+            <td class="snss text green">no</td>
+            <td class="snss text green">no</td>
+            <td class="snss text green">no</td>
+            <td class="ssss text green">no</td>
+          </tr>
+        </tbody>
+      </table>
+    </div>
+   <div xmlns:ld="http://lambdadelta.info/" class="text">* In terms only.
+         ** In terms and local environments only.
          *** In global environments only.
          *** In global environments only.
-         **** Sort level k in terms only. 
+         **** Sort level k in terms only.
    </div>
    </div>
-   
-   <div class="head2">Summary of the Specification</div>
-   <div class="text">Here is a numerical acount of the specification's contents
+
+   <div xmlns:ld="http://lambdadelta.info/" class="head2">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.
    </div>
          and its timeline.
    </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">252</td><td class="snns plane cyan">characters</td><td class="snnn number cyan">483454</td><td class="snns plane cyan">nodes</td><td class="ssnn number cyan">1296744</td></tr><tr><td class="snns component green">propositions</td><td class="snns plane green">theorems</td><td class="snnn number green">85</td><td class="snns plane green">lemmas</td><td class="snnn number green">1119</td><td class="snns plane green">total</td><td class="ssnn number green">1204</td></tr><tr><td class="snss component yellow">concepts</td><td class="snss plane yellow">declared</td><td class="snsn number yellow">46</td><td class="snss plane yellow">defined</td><td class="snsn number yellow">82</td><td class="snss plane yellow">total</td><td class="sssn number yellow">128</td></tr></tbody></table></div>
-   <ul><li><span class="date">In progress.</span>
+   <div xmlns:ld="http://lambdadelta.info/" 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">252</td>
+            <td class="snns plane cyan">characters</td>
+            <td class="snnn number cyan">483453</td>
+            <td class="snns plane cyan">nodes</td>
+            <td class="ssnn number cyan" />
+          </tr>
+          <tr>
+            <td class="snns component green">propositions</td>
+            <td class="snns plane green">theorems</td>
+            <td class="snnn number green">85</td>
+            <td class="snns plane green">lemmas</td>
+            <td class="snnn number green">1119</td>
+            <td class="snns plane green">total</td>
+            <td class="ssnn number green">1204</td>
+          </tr>
+          <tr>
+            <td class="snss component yellow">concepts</td>
+            <td class="snss plane yellow">declared</td>
+            <td class="snsn number yellow">46</td>
+            <td class="snss plane yellow">defined</td>
+            <td class="snsn number yellow">82</td>
+            <td class="snss plane yellow">total</td>
+            <td class="sssn number yellow">128</td>
+          </tr>
+        </tbody>
+      </table>
+    </div>
+   <ul xmlns:ld="http://lambdadelta.info/">
+      <li>
+        <span class="date">In progress.</span>
          Context-sensitive subject equivalence
          Context-sensitive subject equivalence
-        for native type assignment.
-   </li></ul>
-   <ul><li><span class="date">In progress.</span>
+         for native type assignment.
+   </li>
+    </ul>
+   <ul xmlns:ld="http://lambdadelta.info/">
+      <li>
+        <span class="date">In progress.</span>
          Closure of extended context-sensitive computation
          Closure of extended context-sensitive computation
-        for native validity.
-   </li></ul>
-   <ul><li><span class="date">In progress.</span>
+         for native validity.
+   </li>
+    </ul>
+   <ul xmlns:ld="http://lambdadelta.info/">
+      <li>
+        <span class="date">In progress.</span>
          Extended context-sensitive strong normalization
          Extended context-sensitive strong normalization
-        for simply typed terms.
-   </li></ul>
-   <ul><li><span class="date">2012 October 16.</span>
+         for simply typed terms.
+   </li>
+    </ul>
+   <ul xmlns:ld="http://lambdadelta.info/">
+      <li>
+        <span class="date">2012 October 16.</span>
          Confluence for context-free parallel reduction on closures.
          Confluence for context-free parallel reduction on closures.
-   </li></ul>
-   <ul><li><span class="date">2012 July 26.</span>
+   </li>
+    </ul>
+   <ul xmlns:ld="http://lambdadelta.info/">
+      <li>
+        <span class="date">2012 July 26.</span>
          Term binders polarized to control ζ reduction.
          Term binders polarized to control ζ reduction.
-   </li></ul>   
-   <ul><li><span class="date">2012 April 16.</span>
+   </li>
+    </ul>
+   <ul xmlns:ld="http://lambdadelta.info/">
+      <li>
+        <span class="date">2012 April 16.</span>
          Context-sensitive subject equivalence
          Context-sensitive subject equivalence
-        for atomic arity assignment
-        (anniversary milestone).
-   </li></ul>
-   <ul><li><span class="date">2012 March 15.</span>
+         for atomic arity assignment
+         (anniversary milestone).
+   </li>
+    </ul>
+   <ul xmlns:ld="http://lambdadelta.info/">
+      <li>
+        <span class="date">2012 March 15.</span>
          Context-sensitive strong normalization
          Context-sensitive strong normalization
-        for simply typed terms.
-   </li></ul>
-   <ul><li><span class="date">2012 January 27.</span>
+         for simply typed terms.
+   </li>
+    </ul>
+   <ul xmlns:ld="http://lambdadelta.info/">
+      <li>
+        <span class="date">2012 January 27.</span>
          Support for abstract candidates of reducibility.
          Support for abstract candidates of reducibility.
-   </li></ul>
-   <ul><li><span class="date">2011 September 21.</span>
+   </li>
+    </ul>
+   <ul xmlns:ld="http://lambdadelta.info/">
+      <li>
+        <span class="date">2011 September 21.</span>
          Confluence for context-sensitive parallel reduction on terms.
          Confluence for context-sensitive parallel reduction on terms.
-   </li></ul>
-   <ul><li><span class="date">2011 September 6.</span>
+   </li>
+    </ul>
+   <ul xmlns:ld="http://lambdadelta.info/">
+      <li>
+        <span class="date">2011 September 6.</span>
          Confluence for context-free parallel reduction on terms.
          Confluence for context-free parallel reduction on terms.
-   </li></ul>
-   <ul><li><span class="date">2011 April 17.</span>
+   </li>
+    </ul>
+   <ul xmlns:ld="http://lambdadelta.info/">
+      <li>
+        <span class="date">2011 April 17.</span>
          Specification starts.
          Specification starts.
-   </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="head2">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.
          A notation file covering the whole specification is provided.
          according to the following table.
          A notation file covering the whole specification is provided.
-        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="snnn file grey"><br/></td><td class="snnn file grey"><br/></td><td class="snnn file grey"><br/></td><td class="ssnn file grey"><br/></td></tr><tr><td class="snns component prune">dynamic typing</td><td class="snns plane prune">local env. ref. for stratified native validity</td><td class="snns file prune">lsubsv ( ? ⊢ ? ⊩:⊑[?] ? )</td><td class="snnn file prune">lsubsv_ldrop</td><td class="snnn file prune">lsubsv_snv</td><td class="snnn file prune"><br/></td><td class="ssnn file prune"><br/></td></tr><tr><td class="nnns component prune"><br/></td><td class="snns plane prune">stratified native validity</td><td class="snns file prune">snv ( ⦃?,?⦄ ⊩ ? :[?] )</td><td class="snnn file prune">snv_lift snv_ltpss_dx snv_ltpss_sn snv_aaa snv_ssta snv_sstas snv_ssta_ltpr snv_ltpr snv_cpcs</td><td class="snnn file prune"><br/></td><td class="snnn file prune"><br/></td><td class="ssnn file prune"><br/></td></tr><tr><td class="snns component blue">equivalence</td><td class="snns plane blue">focalized equivalence</td><td class="snns file blue">lfpcs ( ⦃?⦄ ⬌* ⦃?⦄ )</td><td class="snnn file blue">lfpcs_aaa lfpcs_fpcs lfpcs_lfprs lfpcs_lfpcs</td><td class="snnn file blue"><br/></td><td class="snnn file blue"><br/></td><td class="ssnn file blue"><br/></td></tr><tr><td class="nnns component blue"><br/></td><td class="nnns plane blue"><br/></td><td class="snns file blue">fpcs ( ⦃?,?⦄ ⬌* ⦃?,?⦄ )</td><td class="snnn file blue">fpcs_aaa fpcs_cpcs fpcs_fprs fpcs_fpcs</td><td class="snnn file blue"><br/></td><td class="snnn file blue"><br/></td><td class="ssnn file blue"><br/></td></tr><tr><td class="nnns component blue"><br/></td><td class="snns plane blue">local env. ref. for context-sensitive equivalence</td><td class="snns file blue">lsubse ( ? ⊢•⊑[?] ? )</td><td class="snnn file blue">lsubse_ldrop lsubse_ssta lsubse_cpcs</td><td class="snnn file blue"><br/></td><td class="snnn file blue"><br/></td><td class="ssnn file blue"><br/></td></tr><tr><td class="nnns component blue"><br/></td><td class="snns plane blue">context-sensitive equivalence</td><td class="snns file blue">cpcs ( ? ⊢ ? ⬌* ? )</td><td class="snnn file blue">cpcs_ltpss_dx cpcs_ltpss_sn cpcs_delift cpcs_aaa cpcs_ltpr cpcs_cprs cpcs_cpcs</td><td class="snnn file blue"><br/></td><td class="snnn file blue"><br/></td><td class="ssnn file blue"><br/></td></tr><tr><td class="snns component sky">conversion</td><td class="snns plane sky">focalized conversion</td><td class="snns file sky">lfpc ( ⦃?⦄ ⬌ ⦃?⦄ )</td><td class="snnn file sky">lfpc_lfpc</td><td class="snnn file sky"><br/></td><td class="snnn file sky"><br/></td><td class="ssnn file sky"><br/></td></tr><tr><td class="nnns component sky"><br/></td><td class="nnns plane sky"><br/></td><td class="snns file sky">fpc ( ⦃?,?⦄ ⬌ ⦃?,?⦄ )</td><td class="snnn file sky">fpc_fpc</td><td class="snnn file sky"><br/></td><td class="snnn file sky"><br/></td><td class="ssnn file sky"><br/></td></tr><tr><td class="nnns component sky"><br/></td><td class="snns plane sky">context-sensitive conversion</td><td class="snns file sky">cpc ( ? ⊢ ? ⬌ ? )</td><td class="snnn file sky">cpc_cpc</td><td class="snnn file sky"><br/></td><td class="snnn file sky"><br/></td><td class="ssnn file sky"><br/></td></tr><tr><td class="snns component cyan">computation</td><td class="snns plane cyan">focalized computation</td><td class="snns file cyan">lfprs ( ⦃?⦄ ➡* ⦃?⦄ )</td><td class="snnn file cyan">lfprs_aaa lfprs_ltprs lfprs_cprs lfprs_fprs lfprs_lfprs</td><td class="snnn file cyan"><br/></td><td class="snnn file cyan"><br/></td><td class="ssnn file cyan"><br/></td></tr><tr><td class="nnns component cyan"><br/></td><td class="nnns plane cyan"><br/></td><td class="snns file cyan">fprs ( ⦃?,?⦄ ➡* ⦃?,?⦄ )</td><td class="snnn file cyan">fprs_aaa fprs_fprs</td><td class="snnn file cyan"><br/></td><td class="snnn file cyan"><br/></td><td class="ssnn file cyan"><br/></td></tr><tr><td class="nnns component cyan"><br/></td><td class="snns plane cyan">"big tree" parallel computation</td><td class="snns file cyan">yprs ( ? ⊢ ⦃?,?⦄ ≥[g] ⦃?,?⦄ )</td><td class="snnn file cyan">yprs_yprs</td><td class="snnn file cyan">ygt ( ? ⊢ ⦃?,?⦄ &gt;[g] ⦃?,?⦄ )</td><td class="snnn file cyan">ygt_ygt</td><td class="ssnn file cyan"><br/></td></tr><tr><td class="nnns component cyan"><br/></td><td class="snns plane cyan">decomposed extended computation</td><td class="snns file cyan">dxprs ( ⦃?,?⦄ ⊢ ? •*➡*[?] ? )</td><td class="snnn file cyan">dxprs_lift dxprs_ltpss_dx dxprs_ltpss_sn dxprs_aaa dxpr_lsubss dxprs_dxprs</td><td class="snnn file cyan"><br/></td><td class="snnn file cyan"><br/></td><td class="ssnn file cyan"><br/></td></tr><tr><td class="nnns component cyan"><br/></td><td class="snns plane cyan">weakly normalizing computation</td><td class="snns file cyan">cpe ( ? ⊢ ➡* 𝐍⦃?⦄ )</td><td class="snnn file cyan">cpe_cpe</td><td class="snnn file cyan"><br/></td><td class="snnn file cyan"><br/></td><td class="ssnn file cyan"><br/></td></tr><tr><td class="nnns component cyan"><br/></td><td class="snns plane cyan">strongly normalizing computation</td><td class="snns file cyan">csn_vector ( ? ⊢ ⬊* ? )</td><td class="snnn file cyan">csn_cpr_vector csn_tstc_vector csn_aaa</td><td class="snnn file cyan"><br/></td><td class="snnn file cyan"><br/></td><td class="ssnn file cyan"><br/></td></tr><tr><td class="nnns component cyan"><br/></td><td class="nnns plane cyan"><br/></td><td class="snns file cyan">csn ( ? ⊢ ⬊* ? )</td><td class="snnn file cyan">csn_alt ( ? ⊢ ⬊⬊* ? )</td><td class="snnn file cyan">csn_lift csn_cpr csn_lfpr</td><td class="snnn file cyan"><br/></td><td class="ssnn file cyan"><br/></td></tr><tr><td class="nnns component cyan"><br/></td><td class="snns plane cyan">context-sensitive computation</td><td class="snns file cyan">cprs (? ⊢ ? ➡* ?)</td><td class="snnn file cyan">cprs_lift cprs_tpss cprs_ltpss_dx cprs_ltpss_sn cprs_delift cprs_aaa cprs_ltpr cprs_lfpr cprs_cprs cprs_lfprs cprs_tstc cprs_tstc_vector</td><td class="snnn file cyan"><br/></td><td class="snnn file cyan"><br/></td><td class="ssnn file cyan"><br/></td></tr><tr><td class="nnns component cyan"><br/></td><td class="snns plane cyan">context-free computation</td><td class="snns file cyan">ltprs ( ? ➡* ? )</td><td class="snnn file cyan">ltprs_alt ( ? ➡➡* ? )</td><td class="snnn file cyan">ltprs_ldrop ltprs_ltprs</td><td class="snnn file cyan"><br/></td><td class="ssnn file cyan"><br/></td></tr><tr><td class="nnns component cyan"><br/></td><td class="nnns plane cyan"><br/></td><td class="snns file cyan">tprs ( ? ➡* ?)</td><td class="snnn file cyan">tprs_lift tprs_tprs</td><td class="snnn file cyan"><br/></td><td class="snnn file cyan"><br/></td><td class="ssnn file cyan"><br/></td></tr><tr><td class="nnns component cyan"><br/></td><td class="snns plane cyan">local env. ref. for abstract candidates of reducibility</td><td class="snns file cyan">lsubc ( ? ⊑[?] ? )</td><td class="snnn file cyan">lsubc_ldrop lsubc_ldrops lsubc_lsuba</td><td class="snnn file cyan"><br/></td><td class="snnn file cyan"><br/></td><td class="ssnn file cyan"><br/></td></tr><tr><td class="nnns component cyan"><br/></td><td class="snns plane cyan">support for abstract computation properties</td><td class="snns file cyan">acp</td><td class="snnn file cyan">acp_cr ( ⦃?,?⦄ ϵ[?] 〚?〛 )</td><td class="snnn file cyan">acp_aaa</td><td class="snnn file cyan"><br/></td><td class="ssnn file cyan"><br/></td></tr><tr><td class="snns component water">reducibility</td><td class="snns plane water">context-sensitive focalized reduction</td><td class="snns file water">cfpr ( ? ⊢ ⦃?,?⦄ ➡ ⦃?,?⦄ )</td><td class="snnn file water">cnfpr_ltpss cfpr_aaa cfpr_cpr cfpr_cfpr</td><td class="snnn file water"><br/></td><td class="snnn file water"><br/></td><td class="ssnn file water"><br/></td></tr><tr><td class="nnns component water"><br/></td><td class="snns plane water">context-free focalized reduction</td><td class="snns file water">lfpr ( ⦃?⦄ ➡ ⦃?⦄ )</td><td class="snnn file water">lfpr_alt ( ⦃?⦄ ➡➡ ⦃?⦄ )</td><td class="snnn file water">lfpr_aaa lfpr_cpr lfpr_fpr lfpr_lfpr</td><td class="snnn file water"><br/></td><td class="ssnn file water"><br/></td></tr><tr><td class="nnns component water"><br/></td><td class="nnns plane water"><br/></td><td class="snns file water">fpr ( ⦃?,?⦄ ➡ ⦃?,?⦄ )</td><td class="snnn file water">fpr_cpr fpr_fpr</td><td class="snnn file water"><br/></td><td class="snnn file water"><br/></td><td class="ssnn file water"><br/></td></tr><tr><td class="nnns component water"><br/></td><td class="snns plane water">"big tree" parallel reduction</td><td class="snns file water">ypr ( ? ⊢ ⦃?,?⦄ ≽[g] ⦃?,?⦄ )</td><td class="snnn file water">ysc ( ? ⊢ ⦃?,?⦄ ≻[g] ⦃?,?⦄ )</td><td class="snnn file water"><br/></td><td class="snnn file water"><br/></td><td class="ssnn file water"><br/></td></tr><tr><td class="nnns component water"><br/></td><td class="snns plane water">context-sensitive normal forms</td><td class="snns file water">cnf ( ? ⊢ 𝐍⦃?⦄ )</td><td class="snnn file water">cnf_lift cnf_cif</td><td class="snnn file water"><br/></td><td class="snnn file water"><br/></td><td class="ssnn file water"><br/></td></tr><tr><td class="nnns component water"><br/></td><td class="snns plane water">context-sensitive reduction</td><td class="snns file water">cpr ( ? ⊢ ? ➡ ? )</td><td class="snnn file water">cpr_lift cpr_tpss cpr_ltpss_dx cpr_ltpss_sn cpr_delift cpr_aaa cpr_ltpr cpr_cpr</td><td class="snnn file water"><br/></td><td class="snnn file water"><br/></td><td class="ssnn file water"><br/></td></tr><tr><td class="nnns component water"><br/></td><td class="snns plane water">context-sensitive reducible forms</td><td class="snns file water">crf ( ? ⊢ 𝐑⦃?⦄ )</td><td class="snnn file water">crf_append</td><td class="snnn file water">cif ( ? ⊢ 𝐈⦃?⦄ )</td><td class="snnn file water">cif_append</td><td class="ssnn file water"><br/></td></tr><tr><td class="nnns component water"><br/></td><td class="snns plane water">context-free normal forms</td><td class="snns file water">thnf ( 𝐇𝐍⦃?⦄ )</td><td class="snnn file water"><br/></td><td class="snnn file water"><br/></td><td class="snnn file water"><br/></td><td class="ssnn file water"><br/></td></tr><tr><td class="nnns component water"><br/></td><td class="snns plane water">context-free reduction</td><td class="snns file water">ltpr ( ? ➡ ? )</td><td class="snnn file water">ltpr_ldrop ltpr_tps ltpr_ltpss_dx ltpr_ltpss_sn ltpr_aaa ltpr_ltpr</td><td class="snnn file water"><br/></td><td class="snnn file water"><br/></td><td class="ssnn file water"><br/></td></tr><tr><td class="nnns component water"><br/></td><td class="nnns plane water"><br/></td><td class="snns file water">tpr ( ? ➡ ? )</td><td class="snnn file water">tpr_lift tpr_tps tpr_tpss tpr_delift tpr_tpr</td><td class="snnn file water"><br/></td><td class="snnn file water"><br/></td><td class="ssnn file water"><br/></td></tr><tr><td class="snns component green">unwind</td><td class="snns plane green">iterated stratified static type assignment</td><td class="snns file green">sstas ( ⦃?,?⦄ ⊢ ? •*[?] ? )</td><td class="snnn file green">sstas_lift sstas_ltpss_dx sstas_ltpss_sn sstas_aaa sstas_lsubss sstas_sstas</td><td class="snnn file green"><br/></td><td class="snnn file green"><br/></td><td class="ssnn file green"><br/></td></tr><tr><td class="snns component grass">static typing</td><td class="snns plane grass">local env. ref. for stratified static type assignment</td><td class="snns file grass">lsubss ( ? •⊑[?] ? )</td><td class="snnn file grass">lsubss_ldrop lsubss_ssta lsubss_lsubss</td><td class="snnn file grass"><br/></td><td class="snnn file grass"><br/></td><td class="ssnn file grass"><br/></td></tr><tr><td class="nnns component grass"><br/></td><td class="snns plane grass">stratified static type assignment</td><td class="snns file grass">ssta ( ⦃?,?⦄ ⊢ ? •[?,?] ? )</td><td class="snnn file grass">ssta_lift ssta_ltpss_dx ssta_ltpss_sn ssta_aaa ssta_ssta</td><td class="snnn file grass"><br/></td><td class="snnn file grass"><br/></td><td class="ssnn file grass"><br/></td></tr><tr><td class="nnns component grass"><br/></td><td class="snns plane grass">local env. ref. for atomic arity assignment</td><td class="snns file grass">lsuba ( ? ⁝⊑ ? )</td><td class="snnn file grass">lsuba_ldrop lsuba_aaa lsuba_lsuba</td><td class="snnn file grass"><br/></td><td class="snnn file grass"><br/></td><td class="ssnn file grass"><br/></td></tr><tr><td class="nnns component grass"><br/></td><td class="snns plane grass">atomic arity assignment</td><td class="snns file grass">aaa ( ? ⊢ ? ⁝ ? )</td><td class="snnn file grass">aaa_lift aaa_lifts aaa_ltpss_dx aaa_ltpss_sn aaa_aaa</td><td class="snnn file grass"><br/></td><td class="snnn file grass"><br/></td><td class="ssnn file grass"><br/></td></tr><tr><td class="nnns component grass"><br/></td><td class="snns plane grass">parameters</td><td class="snns file grass">sh</td><td class="snnn file grass">sd</td><td class="snnn file grass"><br/></td><td class="snnn file grass"><br/></td><td class="ssnn file grass"><br/></td></tr><tr><td class="snns component yellow">unfold</td><td class="snns plane yellow">basic local env. thinning</td><td class="snns file yellow">thin ( ? ▼*[?,?] ≡ ? )</td><td class="snnn file yellow">thin_ldrop thin_delift</td><td class="snnn file yellow"><br/></td><td class="snnn file yellow"><br/></td><td class="ssnn file yellow"><br/></td></tr><tr><td class="nnns component yellow"><br/></td><td class="snns plane yellow">inverse basic term relocation</td><td class="snns file yellow">delift ( ? ⊢ ? ▼*[?,?] ≡ ? )</td><td class="snnn file yellow">delift_alt ( ? ⊢ ? ▼▼*[?,?] ≡ ? )</td><td class="snnn file yellow">delift_lift delift_tpss delift_ltpss delift_delift</td><td class="snnn file yellow"><br/></td><td class="ssnn file yellow"><br/></td></tr><tr><td class="nnns component yellow"><br/></td><td class="snns plane yellow">partial unfold</td><td class="snns file yellow">ltpss_sn ( ? ⊢ ▶*[?,?] ? )</td><td class="snnn file yellow">ltpss_sn_alt ( ? ⊢ ▶▶*[?,?] ? )</td><td class="snnn file yellow">ltpss_sn_ldrop ltpss_sn_tps ltpss_sn_tpss ltpss_sn_ltpss_sn</td><td class="snnn file yellow"><br/></td><td class="ssnn file yellow"><br/></td></tr><tr><td class="nnns component yellow"><br/></td><td class="nnns plane yellow"><br/></td><td class="snns file yellow">ltpss_dx ( ? ▶*[?,?] ? )</td><td class="snnn file yellow">ltpss_dx_ldrop ltpss_dx_tps ltpss_dx_tpss ltpss_dx_ltpss_dx</td><td class="snnn file yellow"><br/></td><td class="snnn file yellow"><br/></td><td class="ssnn file yellow"><br/></td></tr><tr><td class="nnns component yellow"><br/></td><td class="nnns plane yellow"><br/></td><td class="snns file yellow">tpss ( ? ⊢ ? ▶*[?,?] ? )</td><td class="snnn file yellow">tpss_alt ( ? ⊢ ? ▶▶*[?,?] ? )</td><td class="snnn file yellow">tpss_lift</td><td class="snnn file yellow">tpss_tpss</td><td class="ssnn file yellow"><br/></td></tr><tr><td class="nnns component yellow"><br/></td><td class="snns plane yellow">generic local env. slicing</td><td class="snns file yellow">ldrops ( ⇩*[?] ? ≡ ? )</td><td class="snnn file yellow">ldrops_ldrop ldrops_ldrops</td><td class="snnn file yellow"><br/></td><td class="snnn file yellow"><br/></td><td class="ssnn file yellow"><br/></td></tr><tr><td class="nnns component yellow"><br/></td><td class="snns plane yellow">iterated restricted structural predecessor for closures</td><td class="snns file yellow">frsups ( ⦃?,?⦄ ⧁* ⦃?,?⦄ )</td><td class="snnn file yellow">frsups_frsups</td><td class="snnn file yellow"><br/></td><td class="snnn file yellow"><br/></td><td class="ssnn file yellow"><br/></td></tr><tr><td class="nnns component yellow"><br/></td><td class="nnns plane yellow"><br/></td><td class="snns file yellow">frsupp ( ⦃?,?⦄ ⧁+ ⦃?,?⦄ )</td><td class="snnn file yellow">frsupp_frsupp</td><td class="snnn file yellow"><br/></td><td class="snnn file yellow"><br/></td><td class="ssnn file yellow"><br/></td></tr><tr><td class="nnns component yellow"><br/></td><td class="snns plane yellow">generic term relocation</td><td class="snns file yellow">lifts_vector ( ⇧*[?] ? ≡ ? )</td><td class="snnn file yellow">lifts_lift_vector</td><td class="snnn file yellow"><br/></td><td class="snnn file yellow"><br/></td><td class="ssnn file yellow"><br/></td></tr><tr><td class="nnns component yellow"><br/></td><td class="nnns plane yellow"><br/></td><td class="snns file yellow">lifts ( ⇧*[?] ? ≡ ? )</td><td class="snnn file yellow">lifts_lift lifts_lifts</td><td class="snnn file yellow"><br/></td><td class="snnn file yellow"><br/></td><td class="ssnn file yellow"><br/></td></tr><tr><td class="nnns component yellow"><br/></td><td class="snns plane yellow">support for generic relocation</td><td class="snns file yellow">gr2 ( @⦃?,?⦄ ≡ ? )</td><td class="snnn file yellow">gr2_plus ( ? + ? )</td><td class="snnn file yellow">gr2_minus ( ? ▭ ? ≡ ? )</td><td class="snnn file yellow">gr2_gr2</td><td class="ssnn file yellow"><br/></td></tr><tr><td class="snns component orange">substitution</td><td class="snns plane orange">parallel substitution</td><td class="snns file orange">tps ( ? ⊢ ? ▶[?,?] ? )</td><td class="snnn file orange">tps_lift tps_tps</td><td class="snnn file orange"><br/></td><td class="snnn file orange"><br/></td><td class="ssnn file orange"><br/></td></tr><tr><td class="nnns component orange"><br/></td><td class="snns plane orange">global env. slicing</td><td class="snns file orange">gdrop ( ⇩[?] ? ≡ ? )</td><td class="snnn file orange">gdrop_gdrop</td><td class="snnn file orange"><br/></td><td class="snnn file orange"><br/></td><td class="ssnn file orange"><br/></td></tr><tr><td class="nnns component orange"><br/></td><td class="snns plane orange">basic local env. slicing</td><td class="snns file orange">ldrop ( ⇩[?,?] ? ≡ ? )</td><td class="snnn file orange">ldrop_append ldrop_lpx ldrop_sfr ldrop_ldrop</td><td class="snnn file orange"><br/></td><td class="snnn file orange"><br/></td><td class="ssnn file orange"><br/></td></tr><tr><td class="nnns component orange"><br/></td><td class="snns plane orange">local env. ref. for substitution</td><td class="snns file orange">lsubs ( ? ≼[?,?] ? )</td><td class="snnn file orange">(lsubs_lsubs)</td><td class="snnn file orange">lsubs_sfr ( ≽[?,?] ? )</td><td class="snnn file orange"><br/></td><td class="ssnn file orange"><br/></td></tr><tr><td class="nnns component orange"><br/></td><td class="snns plane orange">restricted structural predecessor for closures</td><td class="snns file orange">frsup ( ⦃?,?⦄ ⧁ ⦃?,?⦄ )</td><td class="snnn file orange"><br/></td><td class="snnn file orange"><br/></td><td class="snnn file orange"><br/></td><td class="ssnn file orange"><br/></td></tr><tr><td class="nnns component orange"><br/></td><td class="snns plane orange">basic term relocation</td><td class="snns file orange">lift_vector ( ⇧[?,?] ? ≡ ? )</td><td class="snnn file orange">lift_lift_vector</td><td class="snnn file orange"><br/></td><td class="snnn file orange"><br/></td><td class="ssnn file orange"><br/></td></tr><tr><td class="nnns component orange"><br/></td><td class="nnns plane orange"><br/></td><td class="snns file orange">lift ( ⇧[?,?] ? ≡ ? )</td><td class="snnn file orange">lift_lift</td><td class="snnn file orange"><br/></td><td class="snnn file orange"><br/></td><td class="ssnn file orange"><br/></td></tr><tr><td class="snns component red">grammar</td><td class="snns plane red">same head term form</td><td class="snns file red">tshf ( ? ≈ ? )</td><td class="snnn file red">(tshf_tshf)</td><td class="snnn file red"><br/></td><td class="snnn file red"><br/></td><td class="ssnn file red"><br/></td></tr><tr><td class="nnns component red"><br/></td><td class="snns plane red">same top term constructor</td><td class="snns file red">tstc ( ? ≃ ? )</td><td class="snnn file red">tstc_tstc tstc_vector</td><td class="snnn file red"><br/></td><td class="snnn file red"><br/></td><td class="ssnn file red"><br/></td></tr><tr><td class="nnns component red"><br/></td><td class="snns plane red">closures</td><td class="snns file red">cl_shift ( ? @@ ? )</td><td class="snnn file red">cl_weight ( ♯{?,?} )</td><td class="snnn file red"><br/></td><td class="snnn file red"><br/></td><td class="ssnn file red"><br/></td></tr><tr><td class="nnns component red"><br/></td><td class="snns plane red">internal syntax</td><td class="snns file red">genv</td><td class="snnn file red"><br/></td><td class="snnn file red"><br/></td><td class="snnn file red"><br/></td><td class="ssnn file red"><br/></td></tr><tr><td class="nnns component red"><br/></td><td class="nnns plane red"><br/></td><td class="snns file red">lenv</td><td class="snnn file red">lenv_weight ( ♯{?} )</td><td class="snnn file red">lenv_length ( |?| )</td><td class="snnn file red">lenv_append ( ? @@ ? )</td><td class="ssnn file red">lenv_px lenv_px_bi</td></tr><tr><td class="nnns component red"><br/></td><td class="nnns plane red"><br/></td><td class="snns file red">term</td><td class="snnn file red">term_weight ( ♯{?} )</td><td class="snnn file red">term_simple ( 𝐒⦃?⦄ )</td><td class="snnn file red">term_vector</td><td class="ssnn file red"><br/></td></tr><tr><td class="nnns component red"><br/></td><td class="nnns plane red"><br/></td><td class="snns file red">item</td><td class="snnn file red"><br/></td><td class="snnn file red"><br/></td><td class="snnn file red"><br/></td><td class="ssnn file red"><br/></td></tr><tr><td class="nnss component red"><br/></td><td class="snss plane red">external syntax</td><td class="snss file red">aarity</td><td class="snsn file red"><br/></td><td class="snsn file red"><br/></td><td class="snsn file red"><br/></td><td class="sssn file red"><br/></td></tr></tbody></table></div>
+   <div xmlns:ld="http://lambdadelta.info/" 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="snnn file grey">
+              <br />
+            </td>
+            <td class="snnn file grey">
+              <br />
+            </td>
+            <td class="snnn file grey">
+              <br />
+            </td>
+            <td class="ssnn file grey">
+              <br />
+            </td>
+          </tr>
+          <tr>
+            <td class="snns component prune">dynamic typing</td>
+            <td class="snns plane prune">local env. ref. for stratified native validity</td>
+            <td class="snns file prune">lsubsv ( ? ⊢ ? ⊩:⊑[?] ? )</td>
+            <td class="snnn file prune">lsubsv_ldrop</td>
+            <td class="snnn file prune">lsubsv_snv</td>
+            <td class="snnn file prune">
+              <br />
+            </td>
+            <td class="ssnn file prune">
+              <br />
+            </td>
+          </tr>
+          <tr>
+            <td class="nnns component prune">
+              <br />
+            </td>
+            <td class="snns plane prune">stratified native validity</td>
+            <td class="snns file prune">snv ( ⦃?,?⦄ ⊩ ? :[?] )</td>
+            <td class="snnn file prune">snv_lift snv_ltpss_dx snv_ltpss_sn snv_aaa snv_ssta snv_sstas snv_ssta_ltpr snv_ltpr snv_cpcs</td>
+            <td class="snnn file prune">
+              <br />
+            </td>
+            <td class="snnn file prune">
+              <br />
+            </td>
+            <td class="ssnn file prune">
+              <br />
+            </td>
+          </tr>
+          <tr>
+            <td class="snns component blue">equivalence</td>
+            <td class="snns plane blue">focalized equivalence</td>
+            <td class="snns file blue">lfpcs ( ⦃?⦄ ⬌* ⦃?⦄ )</td>
+            <td class="snnn file blue">lfpcs_aaa lfpcs_fpcs lfpcs_lfprs lfpcs_lfpcs</td>
+            <td class="snnn file blue">
+              <br />
+            </td>
+            <td class="snnn file blue">
+              <br />
+            </td>
+            <td class="ssnn file blue">
+              <br />
+            </td>
+          </tr>
+          <tr>
+            <td class="nnns component blue">
+              <br />
+            </td>
+            <td class="nnns plane blue">
+              <br />
+            </td>
+            <td class="snns file blue">fpcs ( ⦃?,?⦄ ⬌* ⦃?,?⦄ )</td>
+            <td class="snnn file blue">fpcs_aaa fpcs_cpcs fpcs_fprs fpcs_fpcs</td>
+            <td class="snnn file blue">
+              <br />
+            </td>
+            <td class="snnn file blue">
+              <br />
+            </td>
+            <td class="ssnn file blue">
+              <br />
+            </td>
+          </tr>
+          <tr>
+            <td class="nnns component blue">
+              <br />
+            </td>
+            <td class="snns plane blue">local env. ref. for context-sensitive equivalence</td>
+            <td class="snns file blue">lsubse ( ? ⊢•⊑[?] ? )</td>
+            <td class="snnn file blue">lsubse_ldrop lsubse_ssta lsubse_cpcs</td>
+            <td class="snnn file blue">
+              <br />
+            </td>
+            <td class="snnn file blue">
+              <br />
+            </td>
+            <td class="ssnn file blue">
+              <br />
+            </td>
+          </tr>
+          <tr>
+            <td class="nnns component blue">
+              <br />
+            </td>
+            <td class="snns plane blue">context-sensitive equivalence</td>
+            <td class="snns file blue">cpcs ( ? ⊢ ? ⬌* ? )</td>
+            <td class="snnn file blue">cpcs_ltpss_dx cpcs_ltpss_sn cpcs_delift cpcs_aaa cpcs_ltpr cpcs_cprs cpcs_cpcs</td>
+            <td class="snnn file blue">
+              <br />
+            </td>
+            <td class="snnn file blue">
+              <br />
+            </td>
+            <td class="ssnn file blue">
+              <br />
+            </td>
+          </tr>
+          <tr>
+            <td class="snns component sky">conversion</td>
+            <td class="snns plane sky">focalized conversion</td>
+            <td class="snns file sky">lfpc ( ⦃?⦄ ⬌ ⦃?⦄ )</td>
+            <td class="snnn file sky">lfpc_lfpc</td>
+            <td class="snnn file sky">
+              <br />
+            </td>
+            <td class="snnn file sky">
+              <br />
+            </td>
+            <td class="ssnn file sky">
+              <br />
+            </td>
+          </tr>
+          <tr>
+            <td class="nnns component sky">
+              <br />
+            </td>
+            <td class="nnns plane sky">
+              <br />
+            </td>
+            <td class="snns file sky">fpc ( ⦃?,?⦄ ⬌ ⦃?,?⦄ )</td>
+            <td class="snnn file sky">fpc_fpc</td>
+            <td class="snnn file sky">
+              <br />
+            </td>
+            <td class="snnn file sky">
+              <br />
+            </td>
+            <td class="ssnn file sky">
+              <br />
+            </td>
+          </tr>
+          <tr>
+            <td class="nnns component sky">
+              <br />
+            </td>
+            <td class="snns plane sky">context-sensitive conversion</td>
+            <td class="snns file sky">cpc ( ? ⊢ ? ⬌ ? )</td>
+            <td class="snnn file sky">cpc_cpc</td>
+            <td class="snnn file sky">
+              <br />
+            </td>
+            <td class="snnn file sky">
+              <br />
+            </td>
+            <td class="ssnn file sky">
+              <br />
+            </td>
+          </tr>
+          <tr>
+            <td class="snns component cyan">computation</td>
+            <td class="snns plane cyan">focalized computation</td>
+            <td class="snns file cyan">lfprs ( ⦃?⦄ ➡* ⦃?⦄ )</td>
+            <td class="snnn file cyan">lfprs_aaa lfprs_ltprs lfprs_cprs lfprs_fprs lfprs_lfprs</td>
+            <td class="snnn file cyan">
+              <br />
+            </td>
+            <td class="snnn file cyan">
+              <br />
+            </td>
+            <td class="ssnn file cyan">
+              <br />
+            </td>
+          </tr>
+          <tr>
+            <td class="nnns component cyan">
+              <br />
+            </td>
+            <td class="nnns plane cyan">
+              <br />
+            </td>
+            <td class="snns file cyan">fprs ( ⦃?,?⦄ ➡* ⦃?,?⦄ )</td>
+            <td class="snnn file cyan">fprs_aaa fprs_fprs</td>
+            <td class="snnn file cyan">
+              <br />
+            </td>
+            <td class="snnn file cyan">
+              <br />
+            </td>
+            <td class="ssnn file cyan">
+              <br />
+            </td>
+          </tr>
+          <tr>
+            <td class="nnns component cyan">
+              <br />
+            </td>
+            <td class="snns plane cyan">"big tree" parallel computation</td>
+            <td class="snns file cyan">yprs ( ? ⊢ ⦃?,?⦄ ≥[g] ⦃?,?⦄ )</td>
+            <td class="snnn file cyan">yprs_yprs</td>
+            <td class="snnn file cyan">ygt ( ? ⊢ ⦃?,?⦄ &gt;[g] ⦃?,?⦄ )</td>
+            <td class="snnn file cyan">ygt_ygt</td>
+            <td class="ssnn file cyan">
+              <br />
+            </td>
+          </tr>
+          <tr>
+            <td class="nnns component cyan">
+              <br />
+            </td>
+            <td class="snns plane cyan">decomposed extended computation</td>
+            <td class="snns file cyan">dxprs ( ⦃?,?⦄ ⊢ ? •*➡*[?] ? )</td>
+            <td class="snnn file cyan">dxprs_lift dxprs_ltpss_dx dxprs_ltpss_sn dxprs_aaa dxpr_lsubss dxprs_dxprs</td>
+            <td class="snnn file cyan">
+              <br />
+            </td>
+            <td class="snnn file cyan">
+              <br />
+            </td>
+            <td class="ssnn file cyan">
+              <br />
+            </td>
+          </tr>
+          <tr>
+            <td class="nnns component cyan">
+              <br />
+            </td>
+            <td class="snns plane cyan">weakly normalizing computation</td>
+            <td class="snns file cyan">cpe ( ? ⊢ ➡* 𝐍⦃?⦄ )</td>
+            <td class="snnn file cyan">cpe_cpe</td>
+            <td class="snnn file cyan">
+              <br />
+            </td>
+            <td class="snnn file cyan">
+              <br />
+            </td>
+            <td class="ssnn file cyan">
+              <br />
+            </td>
+          </tr>
+          <tr>
+            <td class="nnns component cyan">
+              <br />
+            </td>
+            <td class="snns plane cyan">strongly normalizing computation</td>
+            <td class="snns file cyan">csn_vector ( ? ⊢ ⬊* ? )</td>
+            <td class="snnn file cyan">csn_cpr_vector csn_tstc_vector csn_aaa</td>
+            <td class="snnn file cyan">
+              <br />
+            </td>
+            <td class="snnn file cyan">
+              <br />
+            </td>
+            <td class="ssnn file cyan">
+              <br />
+            </td>
+          </tr>
+          <tr>
+            <td class="nnns component cyan">
+              <br />
+            </td>
+            <td class="nnns plane cyan">
+              <br />
+            </td>
+            <td class="snns file cyan">csn ( ? ⊢ ⬊* ? )</td>
+            <td class="snnn file cyan">csn_alt ( ? ⊢ ⬊⬊* ? )</td>
+            <td class="snnn file cyan">csn_lift csn_cpr csn_lfpr</td>
+            <td class="snnn file cyan">
+              <br />
+            </td>
+            <td class="ssnn file cyan">
+              <br />
+            </td>
+          </tr>
+          <tr>
+            <td class="nnns component cyan">
+              <br />
+            </td>
+            <td class="snns plane cyan">context-sensitive computation</td>
+            <td class="snns file cyan">cprs (? ⊢ ? ➡* ?)</td>
+            <td class="snnn file cyan">cprs_lift cprs_tpss cprs_ltpss_dx cprs_ltpss_sn cprs_delift cprs_aaa cprs_ltpr cprs_lfpr cprs_cprs cprs_lfprs cprs_tstc cprs_tstc_vector</td>
+            <td class="snnn file cyan">
+              <br />
+            </td>
+            <td class="snnn file cyan">
+              <br />
+            </td>
+            <td class="ssnn file cyan">
+              <br />
+            </td>
+          </tr>
+          <tr>
+            <td class="nnns component cyan">
+              <br />
+            </td>
+            <td class="snns plane cyan">context-free computation</td>
+            <td class="snns file cyan">ltprs ( ? ➡* ? )</td>
+            <td class="snnn file cyan">ltprs_alt ( ? ➡➡* ? )</td>
+            <td class="snnn file cyan">ltprs_ldrop ltprs_ltprs</td>
+            <td class="snnn file cyan">
+              <br />
+            </td>
+            <td class="ssnn file cyan">
+              <br />
+            </td>
+          </tr>
+          <tr>
+            <td class="nnns component cyan">
+              <br />
+            </td>
+            <td class="nnns plane cyan">
+              <br />
+            </td>
+            <td class="snns file cyan">tprs ( ? ➡* ?)</td>
+            <td class="snnn file cyan">tprs_lift tprs_tprs</td>
+            <td class="snnn file cyan">
+              <br />
+            </td>
+            <td class="snnn file cyan">
+              <br />
+            </td>
+            <td class="ssnn file cyan">
+              <br />
+            </td>
+          </tr>
+          <tr>
+            <td class="nnns component cyan">
+              <br />
+            </td>
+            <td class="snns plane cyan">local env. ref. for abstract candidates of reducibility</td>
+            <td class="snns file cyan">lsubc ( ? ⊑[?] ? )</td>
+            <td class="snnn file cyan">lsubc_ldrop lsubc_ldrops lsubc_lsuba</td>
+            <td class="snnn file cyan">
+              <br />
+            </td>
+            <td class="snnn file cyan">
+              <br />
+            </td>
+            <td class="ssnn file cyan">
+              <br />
+            </td>
+          </tr>
+          <tr>
+            <td class="nnns component cyan">
+              <br />
+            </td>
+            <td class="snns plane cyan">support for abstract computation properties</td>
+            <td class="snns file cyan">acp</td>
+            <td class="snnn file cyan">acp_cr ( ⦃?,?⦄ ϵ[?] 〚?〛 )</td>
+            <td class="snnn file cyan">acp_aaa</td>
+            <td class="snnn file cyan">
+              <br />
+            </td>
+            <td class="ssnn file cyan">
+              <br />
+            </td>
+          </tr>
+          <tr>
+            <td class="snns component water">reducibility</td>
+            <td class="snns plane water">context-sensitive focalized reduction</td>
+            <td class="snns file water">cfpr ( ? ⊢ ⦃?,?⦄ ➡ ⦃?,?⦄ )</td>
+            <td class="snnn file water">cnfpr_ltpss cfpr_aaa cfpr_cpr cfpr_cfpr</td>
+            <td class="snnn file water">
+              <br />
+            </td>
+            <td class="snnn file water">
+              <br />
+            </td>
+            <td class="ssnn file water">
+              <br />
+            </td>
+          </tr>
+          <tr>
+            <td class="nnns component water">
+              <br />
+            </td>
+            <td class="snns plane water">context-free focalized reduction</td>
+            <td class="snns file water">lfpr ( ⦃?⦄ ➡ ⦃?⦄ )</td>
+            <td class="snnn file water">lfpr_alt ( ⦃?⦄ ➡➡ ⦃?⦄ )</td>
+            <td class="snnn file water">lfpr_aaa lfpr_cpr lfpr_fpr lfpr_lfpr</td>
+            <td class="snnn file water">
+              <br />
+            </td>
+            <td class="ssnn file water">
+              <br />
+            </td>
+          </tr>
+          <tr>
+            <td class="nnns component water">
+              <br />
+            </td>
+            <td class="nnns plane water">
+              <br />
+            </td>
+            <td class="snns file water">fpr ( ⦃?,?⦄ ➡ ⦃?,?⦄ )</td>
+            <td class="snnn file water">fpr_cpr fpr_fpr</td>
+            <td class="snnn file water">
+              <br />
+            </td>
+            <td class="snnn file water">
+              <br />
+            </td>
+            <td class="ssnn file water">
+              <br />
+            </td>
+          </tr>
+          <tr>
+            <td class="nnns component water">
+              <br />
+            </td>
+            <td class="snns plane water">"big tree" parallel reduction</td>
+            <td class="snns file water">ypr ( ? ⊢ ⦃?,?⦄ ≽[g] ⦃?,?⦄ )</td>
+            <td class="snnn file water">ysc ( ? ⊢ ⦃?,?⦄ ≻[g] ⦃?,?⦄ )</td>
+            <td class="snnn file water">
+              <br />
+            </td>
+            <td class="snnn file water">
+              <br />
+            </td>
+            <td class="ssnn file water">
+              <br />
+            </td>
+          </tr>
+          <tr>
+            <td class="nnns component water">
+              <br />
+            </td>
+            <td class="snns plane water">context-sensitive normal forms</td>
+            <td class="snns file water">cnf ( ? ⊢ 𝐍⦃?⦄ )</td>
+            <td class="snnn file water">cnf_lift cnf_cif</td>
+            <td class="snnn file water">
+              <br />
+            </td>
+            <td class="snnn file water">
+              <br />
+            </td>
+            <td class="ssnn file water">
+              <br />
+            </td>
+          </tr>
+          <tr>
+            <td class="nnns component water">
+              <br />
+            </td>
+            <td class="snns plane water">context-sensitive reduction</td>
+            <td class="snns file water">cpr ( ? ⊢ ? ➡ ? )</td>
+            <td class="snnn file water">cpr_lift cpr_tpss cpr_ltpss_dx cpr_ltpss_sn cpr_delift cpr_aaa cpr_ltpr cpr_cpr</td>
+            <td class="snnn file water">
+              <br />
+            </td>
+            <td class="snnn file water">
+              <br />
+            </td>
+            <td class="ssnn file water">
+              <br />
+            </td>
+          </tr>
+          <tr>
+            <td class="nnns component water">
+              <br />
+            </td>
+            <td class="snns plane water">context-sensitive reducible forms</td>
+            <td class="snns file water">crf ( ? ⊢ 𝐑⦃?⦄ )</td>
+            <td class="snnn file water">crf_append</td>
+            <td class="snnn file water">cif ( ? ⊢ 𝐈⦃?⦄ )</td>
+            <td class="snnn file water">cif_append</td>
+            <td class="ssnn file water">
+              <br />
+            </td>
+          </tr>
+          <tr>
+            <td class="nnns component water">
+              <br />
+            </td>
+            <td class="snns plane water">context-free normal forms</td>
+            <td class="snns file water">thnf ( 𝐇𝐍⦃?⦄ )</td>
+            <td class="snnn file water">
+              <br />
+            </td>
+            <td class="snnn file water">
+              <br />
+            </td>
+            <td class="snnn file water">
+              <br />
+            </td>
+            <td class="ssnn file water">
+              <br />
+            </td>
+          </tr>
+          <tr>
+            <td class="nnns component water">
+              <br />
+            </td>
+            <td class="snns plane water">context-free reduction</td>
+            <td class="snns file water">ltpr ( ? ➡ ? )</td>
+            <td class="snnn file water">ltpr_ldrop ltpr_tps ltpr_ltpss_dx ltpr_ltpss_sn ltpr_aaa ltpr_ltpr</td>
+            <td class="snnn file water">
+              <br />
+            </td>
+            <td class="snnn file water">
+              <br />
+            </td>
+            <td class="ssnn file water">
+              <br />
+            </td>
+          </tr>
+          <tr>
+            <td class="nnns component water">
+              <br />
+            </td>
+            <td class="nnns plane water">
+              <br />
+            </td>
+            <td class="snns file water">tpr ( ? ➡ ? )</td>
+            <td class="snnn file water">tpr_lift tpr_tps tpr_tpss tpr_delift tpr_tpr</td>
+            <td class="snnn file water">
+              <br />
+            </td>
+            <td class="snnn file water">
+              <br />
+            </td>
+            <td class="ssnn file water">
+              <br />
+            </td>
+          </tr>
+          <tr>
+            <td class="snns component green">unwind</td>
+            <td class="snns plane green">iterated stratified static type assignment</td>
+            <td class="snns file green">sstas ( ⦃?,?⦄ ⊢ ? •*[?] ? )</td>
+            <td class="snnn file green">sstas_lift sstas_ltpss_dx sstas_ltpss_sn sstas_aaa sstas_lsubss sstas_sstas</td>
+            <td class="snnn file green">
+              <br />
+            </td>
+            <td class="snnn file green">
+              <br />
+            </td>
+            <td class="ssnn file green">
+              <br />
+            </td>
+          </tr>
+          <tr>
+            <td class="snns component grass">static typing</td>
+            <td class="snns plane grass">local env. ref. for stratified static type assignment</td>
+            <td class="snns file grass">lsubss ( ? •⊑[?] ? )</td>
+            <td class="snnn file grass">lsubss_ldrop lsubss_ssta lsubss_lsubss</td>
+            <td class="snnn file grass">
+              <br />
+            </td>
+            <td class="snnn file grass">
+              <br />
+            </td>
+            <td class="ssnn file grass">
+              <br />
+            </td>
+          </tr>
+          <tr>
+            <td class="nnns component grass">
+              <br />
+            </td>
+            <td class="snns plane grass">stratified static type assignment</td>
+            <td class="snns file grass">ssta ( ⦃?,?⦄ ⊢ ? •[?,?] ? )</td>
+            <td class="snnn file grass">ssta_lift ssta_ltpss_dx ssta_ltpss_sn ssta_aaa ssta_ssta</td>
+            <td class="snnn file grass">
+              <br />
+            </td>
+            <td class="snnn file grass">
+              <br />
+            </td>
+            <td class="ssnn file grass">
+              <br />
+            </td>
+          </tr>
+          <tr>
+            <td class="nnns component grass">
+              <br />
+            </td>
+            <td class="snns plane grass">local env. ref. for atomic arity assignment</td>
+            <td class="snns file grass">lsuba ( ? ⁝⊑ ? )</td>
+            <td class="snnn file grass">lsuba_ldrop lsuba_aaa lsuba_lsuba</td>
+            <td class="snnn file grass">
+              <br />
+            </td>
+            <td class="snnn file grass">
+              <br />
+            </td>
+            <td class="ssnn file grass">
+              <br />
+            </td>
+          </tr>
+          <tr>
+            <td class="nnns component grass">
+              <br />
+            </td>
+            <td class="snns plane grass">atomic arity assignment</td>
+            <td class="snns file grass">aaa ( ? ⊢ ? ⁝ ? )</td>
+            <td class="snnn file grass">aaa_lift aaa_lifts aaa_ltpss_dx aaa_ltpss_sn aaa_aaa</td>
+            <td class="snnn file grass">
+              <br />
+            </td>
+            <td class="snnn file grass">
+              <br />
+            </td>
+            <td class="ssnn file grass">
+              <br />
+            </td>
+          </tr>
+          <tr>
+            <td class="nnns component grass">
+              <br />
+            </td>
+            <td class="snns plane grass">parameters</td>
+            <td class="snns file grass">sh</td>
+            <td class="snnn file grass">sd</td>
+            <td class="snnn file grass">
+              <br />
+            </td>
+            <td class="snnn file grass">
+              <br />
+            </td>
+            <td class="ssnn file grass">
+              <br />
+            </td>
+          </tr>
+          <tr>
+            <td class="snns component yellow">unfold</td>
+            <td class="snns plane yellow">basic local env. thinning</td>
+            <td class="snns file yellow">thin ( ? ▼*[?,?] ≡ ? )</td>
+            <td class="snnn file yellow">thin_ldrop thin_delift</td>
+            <td class="snnn file yellow">
+              <br />
+            </td>
+            <td class="snnn file yellow">
+              <br />
+            </td>
+            <td class="ssnn file yellow">
+              <br />
+            </td>
+          </tr>
+          <tr>
+            <td class="nnns component yellow">
+              <br />
+            </td>
+            <td class="snns plane yellow">inverse basic term relocation</td>
+            <td class="snns file yellow">delift ( ? ⊢ ? ▼*[?,?] ≡ ? )</td>
+            <td class="snnn file yellow">delift_alt ( ? ⊢ ? ▼▼*[?,?] ≡ ? )</td>
+            <td class="snnn file yellow">delift_lift delift_tpss delift_ltpss delift_delift</td>
+            <td class="snnn file yellow">
+              <br />
+            </td>
+            <td class="ssnn file yellow">
+              <br />
+            </td>
+          </tr>
+          <tr>
+            <td class="nnns component yellow">
+              <br />
+            </td>
+            <td class="snns plane yellow">partial unfold</td>
+            <td class="snns file yellow">ltpss_sn ( ? ⊢ ▶*[?,?] ? )</td>
+            <td class="snnn file yellow">ltpss_sn_alt ( ? ⊢ ▶▶*[?,?] ? )</td>
+            <td class="snnn file yellow">ltpss_sn_ldrop ltpss_sn_tps ltpss_sn_tpss ltpss_sn_ltpss_sn</td>
+            <td class="snnn file yellow">
+              <br />
+            </td>
+            <td class="ssnn file yellow">
+              <br />
+            </td>
+          </tr>
+          <tr>
+            <td class="nnns component yellow">
+              <br />
+            </td>
+            <td class="nnns plane yellow">
+              <br />
+            </td>
+            <td class="snns file yellow">ltpss_dx ( ? ▶*[?,?] ? )</td>
+            <td class="snnn file yellow">ltpss_dx_ldrop ltpss_dx_tps ltpss_dx_tpss ltpss_dx_ltpss_dx</td>
+            <td class="snnn file yellow">
+              <br />
+            </td>
+            <td class="snnn file yellow">
+              <br />
+            </td>
+            <td class="ssnn file yellow">
+              <br />
+            </td>
+          </tr>
+          <tr>
+            <td class="nnns component yellow">
+              <br />
+            </td>
+            <td class="nnns plane yellow">
+              <br />
+            </td>
+            <td class="snns file yellow">tpss ( ? ⊢ ? ▶*[?,?] ? )</td>
+            <td class="snnn file yellow">tpss_alt ( ? ⊢ ? ▶▶*[?,?] ? )</td>
+            <td class="snnn file yellow">tpss_lift</td>
+            <td class="snnn file yellow">tpss_tpss</td>
+            <td class="ssnn file yellow">
+              <br />
+            </td>
+          </tr>
+          <tr>
+            <td class="nnns component yellow">
+              <br />
+            </td>
+            <td class="snns plane yellow">generic local env. slicing</td>
+            <td class="snns file yellow">ldrops ( ⇩*[?] ? ≡ ? )</td>
+            <td class="snnn file yellow">ldrops_ldrop ldrops_ldrops</td>
+            <td class="snnn file yellow">
+              <br />
+            </td>
+            <td class="snnn file yellow">
+              <br />
+            </td>
+            <td class="ssnn file yellow">
+              <br />
+            </td>
+          </tr>
+          <tr>
+            <td class="nnns component yellow">
+              <br />
+            </td>
+            <td class="snns plane yellow">iterated restricted structural predecessor for closures</td>
+            <td class="snns file yellow">frsups ( ⦃?,?⦄ ⧁* ⦃?,?⦄ )</td>
+            <td class="snnn file yellow">frsups_frsups</td>
+            <td class="snnn file yellow">
+              <br />
+            </td>
+            <td class="snnn file yellow">
+              <br />
+            </td>
+            <td class="ssnn file yellow">
+              <br />
+            </td>
+          </tr>
+          <tr>
+            <td class="nnns component yellow">
+              <br />
+            </td>
+            <td class="nnns plane yellow">
+              <br />
+            </td>
+            <td class="snns file yellow">frsupp ( ⦃?,?⦄ ⧁+ ⦃?,?⦄ )</td>
+            <td class="snnn file yellow">frsupp_frsupp</td>
+            <td class="snnn file yellow">
+              <br />
+            </td>
+            <td class="snnn file yellow">
+              <br />
+            </td>
+            <td class="ssnn file yellow">
+              <br />
+            </td>
+          </tr>
+          <tr>
+            <td class="nnns component yellow">
+              <br />
+            </td>
+            <td class="snns plane yellow">generic term relocation</td>
+            <td class="snns file yellow">lifts_vector ( ⇧*[?] ? ≡ ? )</td>
+            <td class="snnn file yellow">lifts_lift_vector</td>
+            <td class="snnn file yellow">
+              <br />
+            </td>
+            <td class="snnn file yellow">
+              <br />
+            </td>
+            <td class="ssnn file yellow">
+              <br />
+            </td>
+          </tr>
+          <tr>
+            <td class="nnns component yellow">
+              <br />
+            </td>
+            <td class="nnns plane yellow">
+              <br />
+            </td>
+            <td class="snns file yellow">lifts ( ⇧*[?] ? ≡ ? )</td>
+            <td class="snnn file yellow">lifts_lift lifts_lifts</td>
+            <td class="snnn file yellow">
+              <br />
+            </td>
+            <td class="snnn file yellow">
+              <br />
+            </td>
+            <td class="ssnn file yellow">
+              <br />
+            </td>
+          </tr>
+          <tr>
+            <td class="nnns component yellow">
+              <br />
+            </td>
+            <td class="snns plane yellow">support for generic relocation</td>
+            <td class="snns file yellow">gr2 ( @⦃?,?⦄ ≡ ? )</td>
+            <td class="snnn file yellow">gr2_plus ( ? + ? )</td>
+            <td class="snnn file yellow">gr2_minus ( ? ▭ ? ≡ ? )</td>
+            <td class="snnn file yellow">gr2_gr2</td>
+            <td class="ssnn file yellow">
+              <br />
+            </td>
+          </tr>
+          <tr>
+            <td class="snns component orange">substitution</td>
+            <td class="snns plane orange">parallel substitution</td>
+            <td class="snns file orange">tps ( ? ⊢ ? ▶[?,?] ? )</td>
+            <td class="snnn file orange">tps_lift tps_tps</td>
+            <td class="snnn file orange">
+              <br />
+            </td>
+            <td class="snnn file orange">
+              <br />
+            </td>
+            <td class="ssnn file orange">
+              <br />
+            </td>
+          </tr>
+          <tr>
+            <td class="nnns component orange">
+              <br />
+            </td>
+            <td class="snns plane orange">global env. slicing</td>
+            <td class="snns file orange">gdrop ( ⇩[?] ? ≡ ? )</td>
+            <td class="snnn file orange">gdrop_gdrop</td>
+            <td class="snnn file orange">
+              <br />
+            </td>
+            <td class="snnn file orange">
+              <br />
+            </td>
+            <td class="ssnn file orange">
+              <br />
+            </td>
+          </tr>
+          <tr>
+            <td class="nnns component orange">
+              <br />
+            </td>
+            <td class="snns plane orange">basic local env. slicing</td>
+            <td class="snns file orange">ldrop ( ⇩[?,?] ? ≡ ? )</td>
+            <td class="snnn file orange">ldrop_append ldrop_lpx ldrop_sfr ldrop_ldrop</td>
+            <td class="snnn file orange">
+              <br />
+            </td>
+            <td class="snnn file orange">
+              <br />
+            </td>
+            <td class="ssnn file orange">
+              <br />
+            </td>
+          </tr>
+          <tr>
+            <td class="nnns component orange">
+              <br />
+            </td>
+            <td class="snns plane orange">local env. ref. for substitution</td>
+            <td class="snns file orange">lsubs ( ? ≼[?,?] ? )</td>
+            <td class="snnn file orange">(lsubs_lsubs)</td>
+            <td class="snnn file orange">lsubs_sfr ( ≽[?,?] ? )</td>
+            <td class="snnn file orange">
+              <br />
+            </td>
+            <td class="ssnn file orange">
+              <br />
+            </td>
+          </tr>
+          <tr>
+            <td class="nnns component orange">
+              <br />
+            </td>
+            <td class="snns plane orange">restricted structural predecessor for closures</td>
+            <td class="snns file orange">frsup ( ⦃?,?⦄ ⧁ ⦃?,?⦄ )</td>
+            <td class="snnn file orange">
+              <br />
+            </td>
+            <td class="snnn file orange">
+              <br />
+            </td>
+            <td class="snnn file orange">
+              <br />
+            </td>
+            <td class="ssnn file orange">
+              <br />
+            </td>
+          </tr>
+          <tr>
+            <td class="nnns component orange">
+              <br />
+            </td>
+            <td class="snns plane orange">basic term relocation</td>
+            <td class="snns file orange">lift_vector ( ⇧[?,?] ? ≡ ? )</td>
+            <td class="snnn file orange">lift_lift_vector</td>
+            <td class="snnn file orange">
+              <br />
+            </td>
+            <td class="snnn file orange">
+              <br />
+            </td>
+            <td class="ssnn file orange">
+              <br />
+            </td>
+          </tr>
+          <tr>
+            <td class="nnns component orange">
+              <br />
+            </td>
+            <td class="nnns plane orange">
+              <br />
+            </td>
+            <td class="snns file orange">lift ( ⇧[?,?] ? ≡ ? )</td>
+            <td class="snnn file orange">lift_lift</td>
+            <td class="snnn file orange">
+              <br />
+            </td>
+            <td class="snnn file orange">
+              <br />
+            </td>
+            <td class="ssnn file orange">
+              <br />
+            </td>
+          </tr>
+          <tr>
+            <td class="snns component red">grammar</td>
+            <td class="snns plane red">same head term form</td>
+            <td class="snns file red">tshf ( ? ≈ ? )</td>
+            <td class="snnn file red">(tshf_tshf)</td>
+            <td class="snnn file red">
+              <br />
+            </td>
+            <td class="snnn file red">
+              <br />
+            </td>
+            <td class="ssnn file red">
+              <br />
+            </td>
+          </tr>
+          <tr>
+            <td class="nnns component red">
+              <br />
+            </td>
+            <td class="snns plane red">same top term constructor</td>
+            <td class="snns file red">tstc ( ? ≃ ? )</td>
+            <td class="snnn file red">tstc_tstc tstc_vector</td>
+            <td class="snnn file red">
+              <br />
+            </td>
+            <td class="snnn file red">
+              <br />
+            </td>
+            <td class="ssnn file red">
+              <br />
+            </td>
+          </tr>
+          <tr>
+            <td class="nnns component red">
+              <br />
+            </td>
+            <td class="snns plane red">closures</td>
+            <td class="snns file red">cl_shift ( ? @@ ? )</td>
+            <td class="snnn file red">cl_weight ( ♯{?,?} )</td>
+            <td class="snnn file red">
+              <br />
+            </td>
+            <td class="snnn file red">
+              <br />
+            </td>
+            <td class="ssnn file red">
+              <br />
+            </td>
+          </tr>
+          <tr>
+            <td class="nnns component red">
+              <br />
+            </td>
+            <td class="snns plane red">internal syntax</td>
+            <td class="snns file red">genv</td>
+            <td class="snnn file red">
+              <br />
+            </td>
+            <td class="snnn file red">
+              <br />
+            </td>
+            <td class="snnn file red">
+              <br />
+            </td>
+            <td class="ssnn file red">
+              <br />
+            </td>
+          </tr>
+          <tr>
+            <td class="nnns component red">
+              <br />
+            </td>
+            <td class="nnns plane red">
+              <br />
+            </td>
+            <td class="snns file red">lenv</td>
+            <td class="snnn file red">lenv_weight ( ♯{?} )</td>
+            <td class="snnn file red">lenv_length ( |?| )</td>
+            <td class="snnn file red">lenv_append ( ? @@ ? )</td>
+            <td class="ssnn file red">lenv_px lenv_px_bi</td>
+          </tr>
+          <tr>
+            <td class="nnns component red">
+              <br />
+            </td>
+            <td class="nnns plane red">
+              <br />
+            </td>
+            <td class="snns file red">term</td>
+            <td class="snnn file red">term_weight ( ♯{?} )</td>
+            <td class="snnn file red">term_simple ( 𝐒⦃?⦄ )</td>
+            <td class="snnn file red">term_vector</td>
+            <td class="ssnn file red">
+              <br />
+            </td>
+          </tr>
+          <tr>
+            <td class="nnns component red">
+              <br />
+            </td>
+            <td class="nnns plane red">
+              <br />
+            </td>
+            <td class="snns file red">item</td>
+            <td class="snnn file red">
+              <br />
+            </td>
+            <td class="snnn file red">
+              <br />
+            </td>
+            <td class="snnn file red">
+              <br />
+            </td>
+            <td class="ssnn file red">
+              <br />
+            </td>
+          </tr>
+          <tr>
+            <td class="nnss component red">
+              <br />
+            </td>
+            <td class="snss plane red">external syntax</td>
+            <td class="snss file red">aarity</td>
+            <td class="snsn file red">
+              <br />
+            </td>
+            <td class="snsn file red">
+              <br />
+            </td>
+            <td class="snsn file red">
+              <br />
+            </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="head2">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-03-09T23:27:52+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: Mon, 11 Mar 2013 13:47:08 +0100</div>
 </body>
 </html>
 </body>
 </html>
diff --git a/helm/www/lambdadelta/xslt/ld_web.xsl b/helm/www/lambdadelta/xslt/ld_web.xsl
index 288973806cb001899b188388bd0a1a9c7ecf8c94..dd091dcd30927f8cf008d71a9c306648125b0bc8 100644 (file)
--- a/helm/www/lambdadelta/xslt/ld_web.xsl
+++ b/helm/www/lambdadelta/xslt/ld_web.xsl
@@ -5,6 +5,7 @@
 >
 
 <xsl:param name="baseurl"/>
 >
 
 <xsl:param name="baseurl"/>
+<xsl:param name="date"/>
 
 <xsl:include href="xhtbl.xsl"/>
 <xsl:include href="ld_web_library.xsl"/>
 
 <xsl:include href="xhtbl.xsl"/>
 <xsl:include href="ld_web_library.xsl"/>
diff --git a/helm/www/lambdadelta/xslt/ld_web_root.xsl b/helm/www/lambdadelta/xslt/ld_web_root.xsl
index 7c36784c9515e0adfc4babcaa44f347b1dfddc1e..e82b2784b521b049f7a21c27f1c8cba812d40f74 100644 (file)
--- a/helm/www/lambdadelta/xslt/ld_web_root.xsl
+++ b/helm/www/lambdadelta/xslt/ld_web_root.xsl
@@ -2,10 +2,8 @@
 
 <xsl:stylesheet version="1.0"
                 xmlns:xsl="http://www.w3.org/1999/XSL/Transform"
 
 <xsl:stylesheet version="1.0"
                 xmlns:xsl="http://www.w3.org/1999/XSL/Transform"
-               xmlns:date="http://exslt.org/dates-and-times"
                 xmlns:ld="http://lambdadelta.info/"
                 xmlns="http://www.w3.org/1999/xhtml"
                 xmlns:ld="http://lambdadelta.info/"
                 xmlns="http://www.w3.org/1999/xhtml"
-                extension-element-prefixes="date"
 >
 
 <xsl:template match="ld:section">
 >
 
 <xsl:template match="ld:section">
@@ -53,7 +51,7 @@
    <div class="spacer"><br/></div>   
    <div class="spacer">
       <xsl:value-of select="'Last update: '"/> 
    <div class="spacer"><br/></div>   
    <div class="spacer">
       <xsl:value-of select="'Last update: '"/> 
-      <xsl:value-of select="date:date-time()"/>
+      <xsl:value-of select="$date"/>
    </div>
 </xsl:template>
 
    </div>
 </xsl:template>
 
@@ -62,7 +60,7 @@
 </xsl:template>
 
 <xsl:template match="ld:page">
 </xsl:template>
 
 <xsl:template match="ld:page">
-   <html xmlns="http://www.w3.org/1999/xhtml" dir="ltr" lang="en-us"><head>
+   <html xsl:exclude-result-prefixes="ld" 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 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"/>
diff --git a/helm/www/lambdadelta/xslt/lddl_library.xsl b/helm/www/lambdadelta/xslt/lddl_library.xsl
index 9eccd5b85f784caaa9d6bbe7272742bdf68fd26c..ccd977990196e7f79a77f9ecabe6695a094939ed 100644 (file)
--- a/helm/www/lambdadelta/xslt/lddl_library.xsl
+++ b/helm/www/lambdadelta/xslt/lddl_library.xsl
@@ -144,9 +144,14 @@
    </a>
 </xsl:template>
 
    </a>
 </xsl:template>
 
+<xsl:template name="lddlbaseurl">
+   <xsl:value-of select="$baseurl"/>
+   <xsl:value-of select="'static/lddl'"/>
+</xsl:template>
+
 <xsl:template name="uri">
    <xsl:variable name="url">
 <xsl:template name="uri">
    <xsl:variable name="url">
-      <xsl:value-of select="$baseurl"/>
+      <xsl:call-template name="lddlbaseurl">
       <xsl:value-of select="substring-after(@uri,'ld:')"/>
       <xsl:text>.html</xsl:text>
    </xsl:variable>
       <xsl:value-of select="substring-after(@uri,'ld:')"/>
       <xsl:text>.html</xsl:text>
    </xsl:variable>
@@ -249,7 +254,7 @@
    <xsl:param name="path"/>
    <xsl:param name="name"/>
    <xsl:variable name="url">
    <xsl:param name="path"/>
    <xsl:param name="name"/>
    <xsl:variable name="url">
-      <xsl:value-of select="$baseurl"/>
+      <xsl:call-template name="lddlbaseurl">
       <xsl:value-of select="substring-after($path,'ld:')"/>
    </xsl:variable>
    <a href="{$url}"><xsl:value-of select="$name"/></a>
       <xsl:value-of select="substring-after($path,'ld:')"/>
    </xsl:variable>
    <a href="{$url}"><xsl:value-of select="$name"/></a>
Unnamed repository; edit this file 'description' to name the repository.