From: Ferruccio Guidi <ferruccio.guidi@unibo.it>
Date: Mon, 16 Apr 2012 15:08:39 +0000 (+0000)
Subject: - milestone update in basic_2
X-Git-Tag: make_still_working~1811
X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=commitdiff_plain;h=08db2212621969b85852de3bd0677149135df0fe;p=helm.git

- milestone update in basic_2
- html bugfix in hand written web pages
---

diff --git a/helm/www/lambda_delta/apps_2.html b/helm/www/lambda_delta/apps_2.html
index 847125c5d..206401235 100644
--- a/helm/www/lambda_delta/apps_2.html
+++ b/helm/www/lambda_delta/apps_2.html
@@ -57,6 +57,6 @@
    <div class="text">The source files are grouped in directories,
          one for each component.
    </div>
-   <div class="spacer"><img class="rule" alt="[Spacer]" title="lambda_delta rainbow rule" src="http://lambda-delta.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://lambda-delta.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://lambda-delta.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: 2012-04-04+02:00</div>
+   <div class="spacer"><img class="rule" alt="[Spacer]" title="lambda_delta rainbow rule" src="http://lambda-delta.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://lambda-delta.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://lambda-delta.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: 2012-04-16+02:00</div>
 </body>
 </html>
diff --git a/helm/www/lambda_delta/basic_2.html b/helm/www/lambda_delta/basic_2.html
index a59959ead..758975ef4 100644
--- a/helm/www/lambda_delta/basic_2.html
+++ b/helm/www/lambda_delta/basic_2.html
@@ -29,12 +29,12 @@
    <div class="text">Here is a numerical acount of the specification's contents
          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">132</td><td class="snns plane cyan">bytes</td><td class="snnn number cyan">480527</td><td class="snns plane cyan"><br/></td><td class="ssnn number cyan"><br/></td></tr><tr><td class="snns component green">propositions</td><td class="snns plane green">theorems</td><td class="snnn number green">57</td><td class="snns plane green">lemmas</td><td class="snnn number green">541</td><td class="snns plane green">total</td><td class="ssnn number green">598</td></tr><tr><td class="snss component yellow">concepts</td><td class="snss plane yellow">declared</td><td class="snsn number yellow">31</td><td class="snss plane yellow">defined</td><td class="snsn number yellow">42</td><td class="snss plane yellow">total</td><td class="sssn number yellow">73</td></tr></tbody></table></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">137</td><td class="snns plane cyan">bytes</td><td class="snnn number cyan">491033</td><td class="snns plane cyan"><br/></td><td class="ssnn number cyan"><br/></td></tr><tr><td class="snns component green">propositions</td><td class="snns plane green">theorems</td><td class="snnn number green">59</td><td class="snns plane green">lemmas</td><td class="snnn number green">556</td><td class="snns plane green">total</td><td class="ssnn number green">615</td></tr><tr><td class="snss component yellow">concepts</td><td class="snss plane yellow">declared</td><td class="snsn number yellow">32</td><td class="snss plane yellow">defined</td><td class="snsn number yellow">43</td><td class="snss plane yellow">total</td><td class="sssn number yellow">75</td></tr></tbody></table></div>
    <ul><li><span class="date">In progress.</span>
          Context-sensitive subject equivalence
 	 for native type assignment.
    </li></ul>
-   <ul><li><span class="date">In progress.</span>
+   <ul><li><span class="date">2012 April 16.</span>
          Context-sensitive subject equivalence
 	 for atomic arity assignment.
    </li></ul>
@@ -62,12 +62,12 @@
 	 The notation for the relations or functions introduced in each file
 	 is shown in parentheses (? are placeholders).
    </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="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">examples</td><td class="snns plane prune"><br/></td><td class="snns file prune"><br/></td><td class="snnn file prune"><br/></td><td class="snnn file prune"><br/></td><td class="snnn file prune"><br/></td><td class="snnn file prune"><br/></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">native typing</td><td class="snns plane blue"><br/></td><td class="snns file blue">nty</td><td class="snnn file blue"><br/></td><td class="snnn file blue"><br/></td><td class="snnn file blue"><br/></td><td class="snnn file blue"><br/></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">equivalence</td><td class="snns plane sky">context-sensitive equivalence</td><td class="snns file sky">lcpcs ( ? ⊢ ⬌* ? )</td><td class="snnn file sky">lcpcs_aaa</td><td class="snnn file sky">lcpcs_lcprs</td><td class="snnn file sky">lcpcs_lcpcs</td><td class="snnn file sky"><br/></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">cpcs ( ? ⊢ ? ⬌* ? )</td><td class="snnn file sky">cpcs_cprs</td><td class="snnn file sky">cpcs_cpcs</td><td class="snnn file sky"><br/></td><td class="snnn file sky"><br/></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">conversion</td><td class="snns plane cyan">context-sensitive conversion</td><td class="snns file cyan">lcpc ( ? ⊢ ⬌ ? )</td><td class="snnn file cyan">lcpc_lcpc</td><td class="snnn file cyan"><br/></td><td class="snnn file cyan"><br/></td><td class="snnn file cyan"><br/></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">cpc ( ? ⊢ ? ⬌ ? )</td><td class="snnn file cyan">cpc_cpc</td><td class="snnn file cyan"><br/></td><td class="snnn file cyan"><br/></td><td class="snnn file cyan"><br/></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="snns component water">computation</td><td class="snns plane water">weakly normalizing computation</td><td class="snns file water">cpe ( ? ⊢ ? ⊢ ➡* 𝐍[?] )</td><td class="snnn file water">cpe_cpe</td><td class="snnn file water"><br/></td><td class="snnn file water"><br/></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">strongly normalizing computation</td><td class="snns file water">csn_vector ( ⬇* ? )</td><td class="snnn file water">csn_cpr_vector</td><td class="snnn file water">csn_tstc_vector</td><td class="snnn file water">csn_aaa</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="nnns plane water"><br/></td><td class="snns file water">csn ( ⬇* ? )</td><td class="snnn file water">csn_lift</td><td class="snnn file water">csn_cpr</td><td class="snnn file water">csn_cprs ( ⬇** ? )</td><td class="snnn file water">csn_lcpr</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 computation</td><td class="snns file water">lcprs ( ? ⊢ ➡* ? )</td><td class="snnn file water">lcprs_aaa</td><td class="snnn file water">lcprs_cprs</td><td class="snnn file water">lcprs_lcprs</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="nnns plane water"><br/></td><td class="snns file water">cprs (? ⊢ ? ➡* ?)</td><td class="snnn file water">cprs_lift</td><td class="snnn file water">cprs_ltpr</td><td class="snnn file water">cprs_lcpr</td><td class="snnn file water">cprs_cprs</td><td class="snnn file water">cprs_lcprs</td><td class="snnn file water">cprs_tstc</td><td class="ssnn file water">cprs_tstc_vector</td></tr><tr><td class="nnns component water"><br/></td><td class="snns plane water">local env. ref. for abstract candidates of reducibility</td><td class="snns file water">lsubc ( ? [?] ⊑ ? )</td><td class="snnn file water">lsubc_ldrop</td><td class="snnn file water">lsubc_ldrops</td><td class="snnn file water">lsubc_lsuba</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">support for abstract computation properties</td><td class="snns file water">acp</td><td class="snnn file water">acp_cr ( ⦃?,?⦄ ϵ 〚?〛 )</td><td class="snnn file water">acp_aaa</td><td class="snnn file water"><br/></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="snns component green">reducibility</td><td class="snns plane green">context-sensitive normal forms</td><td class="snns file green">cnf ( ? ⊢ 𝐍[?] )</td><td class="snnn file green">cnf_lift</td><td class="snnn file green"><br/></td><td class="snnn file green"><br/></td><td class="snnn file green"><br/></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="nnns component green"><br/></td><td class="snns plane green">context-sensitive reduction</td><td class="snns file green">lcpr ( ? ⊢ ➡ ? )</td><td class="snnn file green">lcpr_aaa</td><td class="snnn file green">lcpr_cpr</td><td class="snnn file green">lcpr_lcpr</td><td class="snnn file green"><br/></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="nnns component green"><br/></td><td class="nnns plane green"><br/></td><td class="snns file green">cpr ( ? ⊢ ? ➡ ? )</td><td class="snnn file green">cpr_lift</td><td class="snnn file green">cpr_ltpss</td><td class="snnn file green">cpr_ltpr</td><td class="snnn file green">cpr_cpr</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="nnns component green"><br/></td><td class="snns plane green">context-free normal forms</td><td class="snns file green">twhnf ( 𝐖𝐇𝐍[?] )</td><td class="snnn file green">tnf ( 𝐍[?] )</td><td class="snnn file green">tnf_tif</td><td class="snnn file green"><br/></td><td class="snnn file green"><br/></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="nnns component green"><br/></td><td class="snns plane green">context-free reduction</td><td class="snns file green">ltpr ( ? ➡ ? )</td><td class="snnn file green">ltpr_ldrop</td><td class="snnn file green">ltpr_tps</td><td class="snnn file green">ltpr_ltpss</td><td class="snnn file green">ltpr_aaa</td><td class="snnn file green">ltpr_ltpr</td><td class="snnn file green"><br/></td><td class="ssnn file green"><br/></td></tr><tr><td class="nnns component green"><br/></td><td class="nnns plane green"><br/></td><td class="snns file green">tpr ( ? ➡ ? )</td><td class="snnn file green">tpr_lift</td><td class="snnn file green">tpr_tpss</td><td class="snnn file green">tpr_tpr</td><td class="snnn file green"><br/></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="nnns component green"><br/></td><td class="snns plane green">context-free reducible forms</td><td class="snns file green">trf ( 𝐑[?] )</td><td class="snnn file green">tif ( 𝐈[?] )</td><td class="snnn file green"><br/></td><td class="snnn file green"><br/></td><td class="snnn file green"><br/></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">static type assignment</td><td class="snns file grass">sty</td><td class="snnn file grass">sty_lift</td><td class="snnn file grass">sty_sty</td><td class="snnn file grass"><br/></td><td class="snnn file grass"><br/></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</td><td class="snnn file grass">lsuba_aaa</td><td class="snnn file grass">lsuba_lsuba</td><td class="snnn file grass"><br/></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</td><td class="snnn file grass">aaa_ltps</td><td class="snnn file grass">aaa_lifts</td><td class="snnn file grass">aaa_ltpss</td><td class="snnn file grass">aaa_aaa</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"><br/></td><td class="snnn file grass"><br/></td><td class="snnn file grass"><br/></td><td class="snnn file grass"><br/></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">term inverse relocation</td><td class="snns file yellow">delift ( ? ⊢ ? [?,?] ≡ ? )</td><td class="snnn file yellow">delift_lift</td><td class="snnn file yellow"><br/></td><td class="snnn file yellow"><br/></td><td class="snnn file yellow"><br/></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">partial unfold</td><td class="snns file yellow">ltpss ( ? [?,?] ▶* ? )</td><td class="snnn file yellow">ltpss_ldrop</td><td class="snnn file yellow">ltpss_tps</td><td class="snnn file yellow">ltpss_ltpss</td><td class="snnn file yellow"><br/></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_lift</td><td class="snnn file yellow">tpss_tpss</td><td class="snnn file yellow">tpss_ltps</td><td class="snnn file yellow"><br/></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 local env. slicing</td><td class="snns file yellow">ldrops ( ⇩*[?] ? ≡ ? )</td><td class="snnn file yellow">ldrops_ldrop</td><td class="snnn file yellow">ldrops_ldrops</td><td class="snnn file yellow"><br/></td><td class="snnn file yellow"><br/></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="snnn file yellow"><br/></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</td><td class="snnn file yellow">lifts_lifts</td><td class="snnn file yellow"><br/></td><td class="snnn file yellow"><br/></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="snnn file yellow"><br/></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="snns component orange">substitution</td><td class="snns plane orange">parallel substitution</td><td class="snns file orange">ltps ( ? [?,?] ▶ ? )</td><td class="snnn file orange">ltps_ldrop</td><td class="snnn file orange">ltps_tps</td><td class="snnn file orange"><br/></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="nnns plane orange"><br/></td><td class="snns file orange">tps ( ? ⊢ ? [?,?] ▶ ? )</td><td class="snnn file orange">tps_lift</td><td class="snnn file orange">tps_tps</td><td class="snnn file orange"><br/></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">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="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 local env. slicing</td><td class="snns file orange">ldrop ( ⇩[?,?] ? ≡ ? )</td><td class="snnn file orange">ldrop_ldrop</td><td class="snnn file orange"><br/></td><td class="snnn file orange"><br/></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="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="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="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="snns component red">grammar</td><td class="snns plane red">local env. ref. for substitution</td><td class="snns file red">lsubs ( ? [?,?] ≼ ? )</td><td class="snnn file red">lsubs_lsubs</td><td class="snnn file red"><br/></td><td class="snnn file red"><br/></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="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="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="snns plane red">same top term constructor</td><td class="snns file red">tstc ( ? ≃ ? )</td><td class="snnn file red">tstc_tstc</td><td class="snnn file red">tstc_vector</td><td class="snnn file red"><br/></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="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="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="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="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"><br/></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">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="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">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="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="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="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="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">examples</td><td class="snns plane prune"><br/></td><td class="snns file prune"><br/></td><td class="snnn file prune"><br/></td><td class="snnn file prune"><br/></td><td class="snnn file prune"><br/></td><td class="snnn file prune"><br/></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">native typing</td><td class="snns plane blue"><br/></td><td class="snns file blue">nty</td><td class="snnn file blue"><br/></td><td class="snnn file blue"><br/></td><td class="snnn file blue"><br/></td><td class="snnn file blue"><br/></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">equivalence</td><td class="snns plane sky">context-sensitive equivalence</td><td class="snns file sky">lcpcs ( ? ⊢ ⬌* ? )</td><td class="snnn file sky">lcpcs_aaa</td><td class="snnn file sky">lcpcs_lcprs</td><td class="snnn file sky">lcpcs_lcpcs</td><td class="snnn file sky"><br/></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">cpcs ( ? ⊢ ? ⬌* ? )</td><td class="snnn file sky">cpcs_cprs</td><td class="snnn file sky">cpcs_cpcs</td><td class="snnn file sky"><br/></td><td class="snnn file sky"><br/></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">conversion</td><td class="snns plane cyan">context-sensitive conversion</td><td class="snns file cyan">lcpc ( ? ⊢ ⬌ ? )</td><td class="snnn file cyan">lcpc_lcpc</td><td class="snnn file cyan"><br/></td><td class="snnn file cyan"><br/></td><td class="snnn file cyan"><br/></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">cpc ( ? ⊢ ? ⬌ ? )</td><td class="snnn file cyan">cpc_cpc</td><td class="snnn file cyan"><br/></td><td class="snnn file cyan"><br/></td><td class="snnn file cyan"><br/></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="snns component water">computation</td><td class="snns plane water">weakly normalizing computation</td><td class="snns file water">cpe ( ? ⊢ ? ⊢ ➡* 𝐍[?] )</td><td class="snnn file water">cpe_cpe</td><td class="snnn file water"><br/></td><td class="snnn file water"><br/></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">strongly normalizing computation</td><td class="snns file water">csn_vector ( ⬇* ? )</td><td class="snnn file water">csn_cpr_vector</td><td class="snnn file water">csn_tstc_vector</td><td class="snnn file water">csn_aaa</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="nnns plane water"><br/></td><td class="snns file water">csn ( ⬇* ? )</td><td class="snnn file water">csn_lift</td><td class="snnn file water">csn_cpr</td><td class="snnn file water">csn_cprs ( ⬇** ? )</td><td class="snnn file water">csn_lcpr</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 computation</td><td class="snns file water">lcprs ( ? ⊢ ➡* ? )</td><td class="snnn file water">lcprs_aaa</td><td class="snnn file water">lcprs_cprs</td><td class="snnn file water">lcprs_lcprs</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="nnns plane water"><br/></td><td class="snns file water">cprs (? ⊢ ? ➡* ?)</td><td class="snnn file water">cprs_lift</td><td class="snnn file water">cprs_ltpr</td><td class="snnn file water">cprs_lcpr</td><td class="snnn file water">cprs_cprs</td><td class="snnn file water">cprs_lcprs</td><td class="snnn file water">cprs_tstc</td><td class="ssnn file water">cprs_tstc_vector</td></tr><tr><td class="nnns component water"><br/></td><td class="snns plane water">local env. ref. for abstract candidates of reducibility</td><td class="snns file water">lsubc ( ? [?] ⊑ ? )</td><td class="snnn file water">lsubc_ldrop</td><td class="snnn file water">lsubc_ldrops</td><td class="snnn file water">lsubc_lsuba</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">support for abstract computation properties</td><td class="snns file water">acp</td><td class="snnn file water">acp_cr ( ⦃?,?⦄ ϵ 〚?〛 )</td><td class="snnn file water">acp_aaa</td><td class="snnn file water"><br/></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="snns component green">reducibility</td><td class="snns plane green">context-sensitive normal forms</td><td class="snns file green">cnf ( ? ⊢ 𝐍[?] )</td><td class="snnn file green">cnf_lift</td><td class="snnn file green"><br/></td><td class="snnn file green"><br/></td><td class="snnn file green"><br/></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="nnns component green"><br/></td><td class="snns plane green">context-sensitive reduction</td><td class="snns file green">lcpr ( ? ⊢ ➡ ? )</td><td class="snnn file green">lcpr_aaa</td><td class="snnn file green">lcpr_cpr</td><td class="snnn file green">lcpr_lcpr</td><td class="snnn file green"><br/></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="nnns component green"><br/></td><td class="nnns plane green"><br/></td><td class="snns file green">cpr ( ? ⊢ ? ➡ ? )</td><td class="snnn file green">cpr_lift</td><td class="snnn file green">cpr_ltpss</td><td class="snnn file green">cpr_ltpsss</td><td class="snnn file green">cpr_ltpr</td><td class="snnn file green">cpr_cpr</td><td class="snnn file green"><br/></td><td class="ssnn file green"><br/></td></tr><tr><td class="nnns component green"><br/></td><td class="snns plane green">context-free normal forms</td><td class="snns file green">twhnf ( 𝐖𝐇𝐍[?] )</td><td class="snnn file green">tnf ( 𝐍[?] )</td><td class="snnn file green">tnf_tif</td><td class="snnn file green"><br/></td><td class="snnn file green"><br/></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="nnns component green"><br/></td><td class="snns plane green">context-free reduction</td><td class="snns file green">ltpr ( ? ➡ ? )</td><td class="snnn file green">ltpr_ldrop</td><td class="snnn file green">ltpr_tps</td><td class="snnn file green">ltpr_ltpss</td><td class="snnn file green">ltpr_ltpsss</td><td class="snnn file green">ltpr_aaa</td><td class="snnn file green">ltpr_ltpr</td><td class="ssnn file green"><br/></td></tr><tr><td class="nnns component green"><br/></td><td class="nnns plane green"><br/></td><td class="snns file green">tpr ( ? ➡ ? )</td><td class="snnn file green">tpr_lift</td><td class="snnn file green">tpr_tpss</td><td class="snnn file green">tpr_tpr</td><td class="snnn file green"><br/></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="nnns component green"><br/></td><td class="snns plane green">context-free reducible forms</td><td class="snns file green">trf ( 𝐑[?] )</td><td class="snnn file green">tif ( 𝐈[?] )</td><td class="snnn file green"><br/></td><td class="snnn file green"><br/></td><td class="snnn file green"><br/></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">static type assignment</td><td class="snns file grass">sty</td><td class="snnn file grass">sty_lift</td><td class="snnn file grass">sty_sty</td><td class="snnn file grass"><br/></td><td class="snnn file grass"><br/></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</td><td class="snnn file grass">lsuba_aaa</td><td class="snnn file grass">lsuba_lsuba</td><td class="snnn file grass"><br/></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</td><td class="snnn file grass">aaa_lifts</td><td class="snnn file grass">aaa_ltpss</td><td class="snnn file grass">aaa_ltpsss</td><td class="snnn file grass">aaa_aaa</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"><br/></td><td class="snnn file grass"><br/></td><td class="snnn file grass"><br/></td><td class="snnn file grass"><br/></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">term inverse relocation</td><td class="snns file yellow">delift ( ? ⊢ ? [?,?] ≡ ? )</td><td class="snnn file yellow">delift_lift</td><td class="snnn file yellow"><br/></td><td class="snnn file yellow"><br/></td><td class="snnn file yellow"><br/></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">partial unfold</td><td class="snns file yellow">ltpsss ( ? [?,?] ▶** ? )</td><td class="snnn file yellow">ltpsss_ldrop</td><td class="snnn file yellow">ltpsss_tps</td><td class="snnn file yellow">ltpsss_tpss</td><td class="snnn file yellow">ltpsss_ltpsss</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">ltpss ( ? [?,?] ▶* ? )</td><td class="snnn file yellow">ltpss_ldrop</td><td class="snnn file yellow">ltpss_tps</td><td class="snnn file yellow">ltpss_tpss</td><td class="snnn file yellow">ltpss_ltpss</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_lift</td><td class="snnn file yellow">tpss_tpss</td><td class="snnn file yellow">tpss_alt ( ? ⊢ ? [?,?] ▶▶* ? )</td><td class="snnn file yellow"><br/></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 local env. slicing</td><td class="snns file yellow">ldrops ( ⇩*[?] ? ≡ ? )</td><td class="snnn file yellow">ldrops_ldrop</td><td class="snnn file yellow">ldrops_ldrops</td><td class="snnn file yellow"><br/></td><td class="snnn file yellow"><br/></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="snnn file yellow"><br/></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</td><td class="snnn file yellow">lifts_lifts</td><td class="snnn file yellow"><br/></td><td class="snnn file yellow"><br/></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="snnn file yellow"><br/></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="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</td><td class="snnn file orange">tps_tps</td><td class="snnn file orange"><br/></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">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="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 local env. slicing</td><td class="snns file orange">ldrop ( ⇩[?,?] ? ≡ ? )</td><td class="snnn file orange">ldrop_ldrop</td><td class="snnn file orange"><br/></td><td class="snnn file orange"><br/></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="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="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="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="snns component red">grammar</td><td class="snns plane red">local env. ref. for substitution</td><td class="snns file red">lsubs ( ? [?,?] ≼ ? )</td><td class="snnn file red">lsubs_lsubs</td><td class="snnn file red"><br/></td><td class="snnn file red"><br/></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="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="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="snns plane red">same top term constructor</td><td class="snns file red">tstc ( ? ≃ ? )</td><td class="snnn file red">tstc_tstc</td><td class="snnn file red">tstc_vector</td><td class="snnn file red"><br/></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="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="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="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="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"><br/></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">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="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">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="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="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,
          one for each component.
    </div>
-   <div class="spacer"><img class="rule" alt="[Spacer]" title="lambda_delta rainbow rule" src="http://lambda-delta.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://lambda-delta.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://lambda-delta.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: 2012-04-04+02:00</div>
+   <div class="spacer"><img class="rule" alt="[Spacer]" title="lambda_delta rainbow rule" src="http://lambda-delta.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://lambda-delta.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://lambda-delta.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: 2012-04-16+02:00</div>
 </body>
 </html>
diff --git a/helm/www/lambda_delta/implementation.html b/helm/www/lambda_delta/implementation.html
index 8d16e6890..559993c3d 100644
--- a/helm/www/lambda_delta/implementation.html
+++ b/helm/www/lambda_delta/implementation.html
@@ -202,8 +202,6 @@ href="http://helm.cs.unibo.it/websvn/listing.php?repname=helm&amp;path=%2Ftrunk%
                 repository</a>. The Svn revisions containing the stable
               versions
               of&nbsp; Helena are indicated below. <br>
-              <ul>
-              </ul>
               <ul>
                 <li><span style="font-weight: bold;">Version 0.8.2.</span>
                   In
@@ -319,7 +317,7 @@ computer
         height: 31px;" alt="[PNG Used Here]" title="PNG Used Here"
         src="download/PNGnow2.png"><br>
       <br>
-      Last update 2012-02-24 by <a
+      Last update 2012-04-16 by <a
         href="http://www.cs.unibo.it/%7Efguidi/">Ferruccio
         Guidi</a><br>
     </div>
diff --git a/helm/www/lambda_delta/news.html b/helm/www/lambda_delta/news.html
index 987949365..10db43f73 100644
--- a/helm/www/lambda_delta/news.html
+++ b/helm/www/lambda_delta/news.html
@@ -45,11 +45,11 @@
               <ul>
                 <li><span style="font-weight: bold;">September 2011.</span>
                   The
-                  denomination "lambda-delta" changes to "lambda_delta".</li>
+                  denomination "lambda-delta" changes to "lambda_delta".
                 <ul>
                   <li>The character "-" is reserved in λδ textual syntax
                     (recognized by <span style="font-style: italic;">Helena
-                      0.8.1</span>).<br>
+                      0.8.1</span>).
                   </li>
                   <li>Eventually, the occurrences of the character "-"
                     will be
@@ -62,23 +62,23 @@
                     on
                     December 2012.<br>
                   </li>
-                </ul>
+                </ul></li>
               </ul>
               <ul>
                 <li><span style="font-weight: bold;">April 2011.</span>
                   The
                   specification of λδ version 2 and related topics is
                   restarted in <a href="http://matita.cs.unibo.it/">Matita
-                    0.5</a>.</li>
-                <ul>
+                    0.5</a>.
+		<ul>
                   <li><a href="apps_2.html">Here</a> is a page about
                     the
                     topics related to the specification (Applications).</li>
                   <li><a href="basic_2.html">Here</a> is a page about
                     the
-                    specification (Core).<br>
+                    specification (Core).
                   </li>
-                </ul>
+                </ul></li>
               </ul>
               <ul>
                 <li><span style="font-weight: bold;">December 2010.</span>
@@ -279,7 +279,7 @@ relocation functions: <span style="font-style: italic;">s</span>, <span
         height: 31px;" alt="[PNG Used Here]" title="PNG Used Here"
         src="download/PNGnow2.png"><br>
       <br>
-      Last update 2012-03-15 by <a
+      Last update 2012-04-16 by <a
         href="http://www.cs.unibo.it/%7Efguidi/">Ferruccio
         Guidi</a><br>
     </div>
diff --git a/helm/www/lambda_delta/web/home/basic_2.ldw.xml b/helm/www/lambda_delta/web/home/basic_2.ldw.xml
index db9898b6d..f9f240048 100644
--- a/helm/www/lambda_delta/web/home/basic_2.ldw.xml
+++ b/helm/www/lambda_delta/web/home/basic_2.ldw.xml
@@ -25,7 +25,7 @@
          Context-sensitive subject equivalence
 	 for native type assignment.
    </news>
-   <news date="In progress.">
+   <news date="2012 April 16.">
          Context-sensitive subject equivalence
 	 for atomic arity assignment.
    </news>
diff --git a/helm/www/lambda_delta/web/home/basic_2_src.tbl b/helm/www/lambda_delta/web/home/basic_2_src.tbl
index 5fad93b37..f95e9681b 100644
--- a/helm/www/lambda_delta/web/home/basic_2_src.tbl
+++ b/helm/www/lambda_delta/web/home/basic_2_src.tbl
@@ -77,7 +77,7 @@ table {
 	]	
 	[ { "context-sensitive reduction" * } {
 	     [ "lcpr ( ? ⊢ ➡ ? )" "lcpr_aaa" "lcpr_cpr" "lcpr_lcpr" * ]
-	     [ "cpr ( ? ⊢ ? ➡ ? )" "cpr_lift" "cpr_ltpss" "cpr_ltpr" "cpr_cpr" * ]
+	     [ "cpr ( ? ⊢ ? ➡ ? )" "cpr_lift" "cpr_ltpss" "cpr_ltpsss" "cpr_ltpr" "cpr_cpr" * ]
 	  }
         ]
         [ { "context-free normal forms" * } {
@@ -85,7 +85,7 @@ table {
           }
 	]
         [ { "context-free reduction" * } {
-	     [ "ltpr ( ? ➡ ? )" "ltpr_ldrop" "ltpr_tps" "ltpr_ltpss" "ltpr_aaa" "ltpr_ltpr" * ]
+	     [ "ltpr ( ? ➡ ? )" "ltpr_ldrop" "ltpr_tps" "ltpr_ltpss" "ltpr_ltpsss" "ltpr_aaa" "ltpr_ltpr" * ]
 	     [ "tpr ( ? ➡ ? )"  "tpr_lift" "tpr_tpss" "tpr_tpr" * ]
           }
 	]
@@ -106,7 +106,7 @@ table {
 	  }
         ]
         [ { "atomic arity assignment" * } {
-	     [ "aaa ( ? ⊢ ? ÷ ? )" "aaa_lift" "aaa_ltps" "aaa_lifts" "aaa_ltpss" "aaa_aaa" * ]
+	     [ "aaa ( ? ⊢ ? ÷ ? )" "aaa_lift" "aaa_lifts" "aaa_ltpss" "aaa_ltpsss" "aaa_aaa" * ]
 	  }
         ]
         [ { "parameters" * } {
@@ -122,8 +122,9 @@ table {
           }
 	]
 	[ { "partial unfold" * } {
-             [ "ltpss ( ? [?,?] ▶* ? )" "ltpss_ldrop" "ltpss_tps" "ltpss_ltpss" * ] 
-	     [ "tpss ( ? ⊢ ? [?,?] ▶* ? )" "tpss_lift" "tpss_tpss" * ]
+             [ "ltpsss ( ? [?,?] ▶** ? )" "ltpsss_ldrop" "ltpsss_tps" "ltpsss_tpss" "ltpsss_ltpsss" * ] 
+             [ "ltpss ( ? [?,?] ▶* ? )" "ltpss_ldrop" "ltpss_tps" "ltpss_tpss" "ltpss_ltpss" * ] 
+	     [ "tpss ( ? ⊢ ? [?,?] ▶* ? )" "tpss_lift" "tpss_tpss" "tpss_alt ( ? ⊢ ? [?,?] ▶▶* ? )" * ]
           }
 	]
 	[ { "generic local env. slicing" * } {