update in basic_2 and ground_2

diff --git a/helm/www/lambdadelta/BTM.html b/helm/www/lambdadelta/BTM.html
index 2d1bb0ec81973afd104c78312e20b7a491456bcd..3f0d5d4279126f41e57f0e27d6e2adf3d813f3ff 100644 (file)
--- a/helm/www/lambdadelta/BTM.html
+++ b/helm/www/lambdadelta/BTM.html
@@ -223,6 +223,6 @@
     <div xmlns:ld="http://lambdadelta.info/" class="spacer">
       <br />
     </div>
-    <div xmlns:ld="http://lambdadelta.info/" class="spacer">Last update: Mon, 20 Jan 2014 17:00:19 +0100</div>
+    <div xmlns:ld="http://lambdadelta.info/" class="spacer">Last update: Tue, 11 Feb 2014 22:11:38 +0100</div>
 </body>
 </html>

diff --git a/helm/www/lambdadelta/apps_2.html b/helm/www/lambdadelta/apps_2.html
index 14a74209516f0e35cd1e108280bf22fb27c46a6e..a306d00eac1ee5c2e6a72e913e179b54fe4fb3de 100644 (file)
--- a/helm/www/lambdadelta/apps_2.html
+++ b/helm/www/lambdadelta/apps_2.html
@@ -191,6 +191,6 @@
     <div xmlns:ld="http://lambdadelta.info/" class="spacer">
       <br />
     </div>
-    <div xmlns:ld="http://lambdadelta.info/" class="spacer">Last update: Mon, 20 Jan 2014 17:00:19 +0100</div>
+    <div xmlns:ld="http://lambdadelta.info/" class="spacer">Last update: Tue, 11 Feb 2014 22:11:38 +0100</div>
 </body>
 </html>

diff --git a/helm/www/lambdadelta/basic_2.html b/helm/www/lambdadelta/basic_2.html
index 951778d1e289212b14d9d995b7823c31330dec76..cf44a00e41927a36ade7768d1e4557bcbe1535bb 100644 (file)
--- a/helm/www/lambdadelta/basic_2.html
+++ b/helm/www/lambdadelta/basic_2.html
@@ -163,29 +163,29 @@
           <tr>
             <td class="snns component cyan">sizes</td>
             <td class="snns plane cyan">files</td>
-            <td class="snnn number cyan">324  </td>
+            <td class="snnn number cyan">337  </td>
             <td class="snns plane cyan">characters</td>
-            <td class="snnn number cyan">549104</td>
+            <td class="snnn number cyan">575141</td>
             <td class="snns plane cyan">nodes</td>
-            <td class="ssnn number cyan">1564238</td>
+            <td class="ssnn number cyan">1625856</td>
           </tr>
           <tr>
             <td class="snns component green">propositions</td>
             <td class="snns plane green">theorems</td>
-            <td class="snnn number green">103</td>
+            <td class="snnn number green">105</td>
             <td class="snns plane green">lemmas</td>
-            <td class="snnn number green">1089</td>
+            <td class="snnn number green">1144</td>
             <td class="snns plane green">total</td>
-            <td class="ssnn number green">1192</td>
+            <td class="ssnn number green">1249</td>
           </tr>
           <tr>
             <td class="snss component yellow">concepts</td>
             <td class="snss plane yellow">declared</td>
-            <td class="snsn number yellow">50</td>
+            <td class="snsn number yellow">51</td>
             <td class="snss plane yellow">defined</td>
-            <td class="snsn number yellow">77</td>
+            <td class="snsn number yellow">79</td>
             <td class="snss plane yellow">total</td>
-            <td class="sssn number yellow">127</td>
+            <td class="sssn number yellow">130</td>
           </tr>
         </tbody>
       </table>
@@ -388,7 +388,7 @@
           </tr>
           <tr>
             <td class="snns component cyan">computation</td>
-            <td class="snns plane cyan">context-sensitive extended evaluation</td>
+            <td class="snns plane cyan">evaluation for context-sensitive extended reduction</td>
             <td class="snns file cyan">cpxe ( ⦃?,?⦄ ⊢ ➡*[?,?] 𝐍⦃?⦄ )</td>
             <td class="snnn file cyan">
               <br />
@@ -404,7 +404,7 @@
             <td class="nnns component cyan">
               <br />
             </td>
-            <td class="snns plane cyan">context-sensitive evaluation</td>
+            <td class="snns plane cyan">evaluation for context-sensitive reduction</td>
             <td class="snns file cyan">cpre ( ⦃?,?⦄ ⊢ ➡* 𝐍⦃?⦄ )</td>
             <td class="snnn file cyan">cpre_cpre</td>
             <td class="snnn file cyan">
@@ -565,7 +565,7 @@
             <td class="snns plane cyan">context-sensitive extended computation</td>
             <td class="snns file cyan">lpxs ( ⦃?,?⦄ ⊢ ➡*[?,?] ? )</td>
             <td class="snnn file cyan">lpxs_alt ( ⦃?,?⦄ ⊢ ➡➡*[?,?] ? )</td>
-            <td class="snnn file cyan">lpxs_ldrop lpxs_lleq lpxs_aaa lpxs_cpxs lpxs_lpxs</td>
+            <td class="snnn file cyan">lpxs_ldrop lpxs_cpye lpxs_lleq lpxs_aaa lpxs_cpxs lpxs_lpxs</td>
             <td class="ssnn file cyan">
               <br />
             </td>
@@ -578,7 +578,7 @@
               <br />
             </td>
             <td class="snns file cyan">cpxs ( ⦃?,?⦄ ⊢ ? ➡*[?,?] ? )</td>
-            <td class="snnn file cyan">cpxs_tstc cpxs_tstc_vector cpxs_lift cpxs_cpys cpxs_lleq cpxs_aaa cpxs_cpxs</td>
+            <td class="snnn file cyan">cpxs_tstc cpxs_tstc_vector cpxs_lift cpxs_lleq cpxs_aaa cpxs_cpxs</td>
             <td class="snnn file cyan">
               <br />
             </td>
@@ -656,8 +656,8 @@
             <td class="nnns component water">
               <br />
             </td>
-            <td class="snns plane water">context-sensitive extended normal forms</td>
-            <td class="snns file water">cnx ( ⦃?,?⦄ ⊢ 𝐍[?,?]⦃?⦄ )</td>
+            <td class="snns plane water">normal forms for context-sensitive extended reduction</td>
+            <td class="snns file water">cnx ( ⦃?,?⦄ ⊢ ➡[?,?] 𝐍⦃?⦄ )</td>
             <td class="snnn file water">cnx_lift cnx_crx cnx_cix</td>
             <td class="snnn file water">
               <br />
@@ -672,7 +672,7 @@
             </td>
             <td class="snns plane water">context-sensitive extended reduction</td>
             <td class="snns file water">lpx ( ⦃?,?⦄ ⊢ ➡[?,?] ? )</td>
-            <td class="snnn file water">lpx_ldrop lpx_lleq lpx_aaa</td>
+            <td class="snnn file water">lpx_ldrop lpx_cpys lpx_cpye lpx_lleq lpx_aaa</td>
             <td class="snnn file water">
               <br />
             </td>
@@ -700,8 +700,8 @@
             <td class="nnns component water">
               <br />
             </td>
-            <td class="snns plane water">context-sensitive extended irreducible forms</td>
-            <td class="snns file water">cix ( ⦃?,?⦄ ⊢ 𝐈[?,?]⦃?⦄ )</td>
+            <td class="snns plane water">irreducible forms for context-sensitive extended reduction</td>
+            <td class="snns file water">cix ( ⦃?,?⦄ ⊢ ➡[?,?] 𝐈⦃?⦄ )</td>
             <td class="snnn file water">cix_append cix_lift</td>
             <td class="snnn file water">
               <br />
@@ -714,8 +714,8 @@
             <td class="nnns component water">
               <br />
             </td>
-            <td class="snns plane water">context-sensitive extended reducible forms</td>
-            <td class="snns file water">crx ( ⦃?,?⦄ ⊢ 𝐑[?,?]⦃?⦄ )</td>
+            <td class="snns plane water">reducible forms for context-sensitive extended reduction</td>
+            <td class="snns file water">crx ( ⦃?,?⦄ ⊢ ➡[?,?] 𝐑⦃?⦄ )</td>
             <td class="snnn file water">crx_append crx_lift</td>
             <td class="snnn file water">
               <br />
@@ -728,8 +728,8 @@
             <td class="nnns component water">
               <br />
             </td>
-            <td class="snns plane water">context-sensitive normal forms</td>
-            <td class="snns file water">cnr ( ⦃?,?⦄ ⊢ 𝐍⦃?⦄ )</td>
+            <td class="snns plane water">normal forms for context-sensitive reduction</td>
+            <td class="snns file water">cnr ( ⦃?,?⦄ ⊢ ➡ 𝐍⦃?⦄ )</td>
             <td class="snnn file water">cnr_lift cnr_crr cnr_cir</td>
             <td class="snnn file water">
               <br />
@@ -772,8 +772,8 @@
             <td class="nnns component water">
               <br />
             </td>
-            <td class="snns plane water">context-sensitive irreducible forms</td>
-            <td class="snns file water">cir ( ⦃?,?⦄ ⊢ 𝐈⦃?⦄ )</td>
+            <td class="snns plane water">irreducible forms for context-sensitive reduction</td>
+            <td class="snns file water">cir ( ⦃?,?⦄ ⊢ ➡ 𝐈⦃?⦄ )</td>
             <td class="snnn file water">cir_append cir_lift</td>
             <td class="snnn file water">
               <br />
@@ -786,8 +786,8 @@
             <td class="nnns component water">
               <br />
             </td>
-            <td class="snns plane water">context-sensitive reducible forms</td>
-            <td class="snns file water">crr ( ⦃?,?⦄ ⊢ 𝐑⦃?⦄ )</td>
+            <td class="snns plane water">reducible forms for context-sensitive reduction</td>
+            <td class="snns file water">crr ( ⦃?,?⦄ ⊢ ➡ 𝐑⦃?⦄ )</td>
             <td class="snnn file water">crr_append crr_lift</td>
             <td class="snnn file water">
               <br />
@@ -909,7 +909,19 @@
             <td class="snns plane yellow">lazy equivalence for local environments</td>
             <td class="snns file yellow">lleq ( ? ⋕[?,?] ? )</td>
             <td class="snnn file yellow">lleq_alt ( ? ⋕⋕[?,?] ? )</td>
-            <td class="snnn file yellow">lleq_ldrop lleq_fqus lleq_lleq lleq_ext</td>
+            <td class="snnn file yellow">lleq_ldrop lleq_fqus lleq_cpye lleq_lleq lleq_ext</td>
+            <td class="ssnn file yellow">
+              <br />
+            </td>
+          </tr>
+          <tr>
+            <td class="nnns component yellow">
+              <br />
+            </td>
+            <td class="snns plane yellow">evaluation for contxt-sensitive extended substitution</td>
+            <td class="snns file yellow">cpye ( ⦃?,?⦄ ⊢ ? ▶*[?,?] 𝐍⦃?⦄ )</td>
+            <td class="snnn file yellow">cpye_alt ( ⦃?,?⦄ ⊢ ? ▶▶*[?,?] 𝐍⦃?⦄ )</td>
+            <td class="snnn file yellow">cpye_lift cpye_cpye</td>
             <td class="ssnn file yellow">
               <br />
             </td>
@@ -919,9 +931,9 @@
               <br />
             </td>
             <td class="snns plane yellow">contxt-sensitive extended multiple substitution</td>
-            <td class="snns file yellow">cpys ( ⦃?,?⦄ ⊢ ? ▶*×[?,?] ? )</td>
-            <td class="snnn file yellow">cpys_alt ( ⦃?,?⦄ ⊢ ? ▶▶*×[?,?] ? )</td>
-            <td class="snnn file yellow">cpys_lift cpys_cpys</td>
+            <td class="snns file yellow">cpys ( ⦃?,?⦄ ⊢ ? ▶*[?,?] ? )</td>
+            <td class="snnn file yellow">cpys_alt ( ⦃?,?⦄ ⊢ ? ▶▶*[?,?] ? )</td>
+            <td class="snnn file yellow">cpys_lift cpys_cny cpys_cpys</td>
             <td class="ssnn file yellow">
               <br />
             </td>
@@ -1012,8 +1024,22 @@
           </tr>
           <tr>
             <td class="snns component orange">relocation</td>
+            <td class="snns plane orange">normal forms for context-sensitive extended substitution</td>
+            <td class="snns file orange">cny ( ⦃?,?⦄ ⊢ ▶[?,?] 𝐍⦃?⦄ )</td>
+            <td class="snnn file orange">cny_lift</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">contxt-sensitive extended ordinary substitution</td>
-            <td class="snns file orange">cpy ( ⦃?,?⦄ ⊢ ? ▶×[?,?] ? )</td>
+            <td class="snns file orange">cpy ( ⦃?,?⦄ ⊢ ? ▶[?,?] ? )</td>
             <td class="snnn file orange">cpy_lift cpy_cpy</td>
             <td class="snnn file orange">
               <br />
@@ -1288,6 +1314,6 @@
     <div xmlns:ld="http://lambdadelta.info/" class="spacer">
       <br />
     </div>
-    <div xmlns:ld="http://lambdadelta.info/" class="spacer">Last update: Mon, 20 Jan 2014 17:00:19 +0100</div>
+    <div xmlns:ld="http://lambdadelta.info/" class="spacer">Last update: Tue, 11 Feb 2014 22:11:38 +0100</div>
 </body>
 </html>

diff --git a/helm/www/lambdadelta/ground_2.html b/helm/www/lambdadelta/ground_2.html
index 4dd340fa4a74f76667927225e18e07bfe36b0844..45c5ad29bc2e61611cc00da6eea4925fa34e1118 100644 (file)
--- a/helm/www/lambdadelta/ground_2.html
+++ b/helm/www/lambdadelta/ground_2.html
@@ -56,20 +56,20 @@
           <tr>
             <td class="snns component cyan">sizes</td>
             <td class="snns plane cyan">files</td>
-            <td class="snnn number cyan">29  </td>
+            <td class="snnn number cyan">31  </td>
             <td class="snns plane cyan">characters</td>
-            <td class="snnn number cyan">71585</td>
+            <td class="snnn number cyan">71828</td>
             <td class="snns plane cyan">nodes</td>
-            <td class="ssnn number cyan">58746</td>
+            <td class="ssnn number cyan">56616</td>
           </tr>
           <tr>
             <td class="snns component green">propositions</td>
             <td class="snns plane green">theorems</td>
             <td class="snnn number green">2</td>
             <td class="snns plane green">lemmas</td>
-            <td class="snnn number green">167</td>
+            <td class="snnn number green">168</td>
             <td class="snns plane green">total</td>
-            <td class="ssnn number green">169</td>
+            <td class="ssnn number green">170</td>
           </tr>
           <tr>
             <td class="snss component yellow">concepts</td>
@@ -234,6 +234,6 @@
     <div xmlns:ld="http://lambdadelta.info/" class="spacer">
       <br />
     </div>
-    <div xmlns:ld="http://lambdadelta.info/" class="spacer">Last update: Mon, 20 Jan 2014 17:00:19 +0100</div>
+    <div xmlns:ld="http://lambdadelta.info/" class="spacer">Last update: Tue, 11 Feb 2014 22:11:38 +0100</div>
 </body>
 </html>