update in basic_2 and ground_2

diff --git a/helm/www/lambdadelta/BTM.html b/helm/www/lambdadelta/BTM.html
index 3f0d5d4279126f41e57f0e27d6e2adf3d813f3ff..b5bc15268c8651a59c0c0323cfe62c231dbc7f65 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: Tue, 11 Feb 2014 22:11:38 +0100</div>
+    <div xmlns:ld="http://lambdadelta.info/" class="spacer">Last update: Fri, 21 Feb 2014 17:37:37 +0100</div>
 </body>
 </html>

diff --git a/helm/www/lambdadelta/apps_2.html b/helm/www/lambdadelta/apps_2.html
index a306d00eac1ee5c2e6a72e913e179b54fe4fb3de..be978d3e6309aba5324a1a2bbdcfddfdda7660fd 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: Tue, 11 Feb 2014 22:11:38 +0100</div>
+    <div xmlns:ld="http://lambdadelta.info/" class="spacer">Last update: Fri, 21 Feb 2014 17:37:37 +0100</div>
 </body>
 </html>

diff --git a/helm/www/lambdadelta/basic_2.html b/helm/www/lambdadelta/basic_2.html
index cf44a00e41927a36ade7768d1e4557bcbe1535bb..b6ba4f2bef310ac3c810e447efcbb2350b58d18b 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">337  </td>
+            <td class="snnn number cyan">327  </td>
             <td class="snns plane cyan">characters</td>
-            <td class="snnn number cyan">575141</td>
+            <td class="snnn number cyan">564871</td>
             <td class="snns plane cyan">nodes</td>
-            <td class="ssnn number cyan">1625856</td>
+            <td class="ssnn number cyan">1606196</td>
           </tr>
           <tr>
             <td class="snns component green">propositions</td>
             <td class="snns plane green">theorems</td>
             <td class="snnn number green">105</td>
             <td class="snns plane green">lemmas</td>
-            <td class="snnn number green">1144</td>
+            <td class="snnn number green">1107</td>
             <td class="snns plane green">total</td>
-            <td class="ssnn number green">1249</td>
+            <td class="ssnn number green">1212</td>
           </tr>
           <tr>
             <td class="snss component yellow">concepts</td>
             <td class="snss plane yellow">declared</td>
-            <td class="snsn number yellow">51</td>
+            <td class="snsn number yellow">52</td>
             <td class="snss plane yellow">defined</td>
-            <td class="snsn number yellow">79</td>
+            <td class="snsn number yellow">76</td>
             <td class="snss plane yellow">total</td>
-            <td class="sssn number yellow">130</td>
+            <td class="sssn number yellow">128</td>
           </tr>
         </tbody>
       </table>
@@ -431,8 +431,24 @@
               <br />
             </td>
             <td class="snns plane cyan">strongly normalizing extended computation</td>
-            <td class="snns file cyan">lsx ( ? ⊢ ⬊*[?,?,?] ? )</td>
-            <td class="snnn file cyan">lsx_cpxs lsx_csx</td>
+            <td class="snns file cyan">lcosx ( ? ⊢ ⧤⬊*[?,?,?] ? )</td>
+            <td class="snnn file cyan">lcosx_cpxs</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">lsx ( ? ⊢ ⋕⬊*[?,?,?,?] ? )</td>
+            <td class="snnn file cyan">lsx_ldrop lsx_cpxs lsx_csx</td>
             <td class="snnn file cyan">
               <br />
             </td>
@@ -565,7 +581,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_cpye lpxs_lleq lpxs_aaa lpxs_cpxs lpxs_lpxs</td>
+            <td class="snnn file cyan">lpxs_ldrop lpxs_lleq lpxs_aaa lpxs_cpxs lpxs_lpxs</td>
             <td class="ssnn file cyan">
               <br />
             </td>
@@ -578,7 +594,7 @@
               <br />
             </td>
             <td class="snns file cyan">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">cpxs_tstc cpxs_tstc_vector cpxs_lift cpxs_cpys cpxs_lleq cpxs_aaa cpxs_cpxs</td>
             <td class="snnn file cyan">
               <br />
             </td>
@@ -672,7 +688,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_cpys lpx_cpye lpx_lleq lpx_aaa</td>
+            <td class="snnn file water">lpx_ldrop lpx_cpys lpx_lleq lpx_aaa</td>
             <td class="snnn file water">
               <br />
             </td>
@@ -702,7 +718,7 @@
             </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">cix_lift</td>
             <td class="snnn file water">
               <br />
             </td>
@@ -716,7 +732,7 @@
             </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">crx_lift</td>
             <td class="snnn file water">
               <br />
             </td>
@@ -774,7 +790,7 @@
             </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">cir_lift</td>
             <td class="snnn file water">
               <br />
             </td>
@@ -788,7 +804,7 @@
             </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">crr_lift</td>
             <td class="snnn file water">
               <br />
             </td>
@@ -909,19 +925,7 @@
             <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_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="snnn file yellow">lleq_ldrop lleq_fqus lleq_lleq lleq_ext</td>
             <td class="ssnn file yellow">
               <br />
             </td>
@@ -933,7 +937,7 @@
             <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_cny cpys_cpys</td>
+            <td class="snnn file yellow">cpys_lift cpys_cpys</td>
             <td class="ssnn file yellow">
               <br />
             </td>
@@ -1024,20 +1028,6 @@
           </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="snnn file orange">cpy_lift cpy_cpy</td>
@@ -1052,9 +1042,9 @@
             <td class="nnns component orange">
               <br />
             </td>
-            <td class="snns plane orange">local env. ref. for extended substitution</td>
-            <td class="snns file orange">lsuby ( ? ⊑×[?,?] ? )</td>
-            <td class="snnn file orange">lsuby_lsuby</td>
+            <td class="snns plane orange">restricted local env. ref.</td>
+            <td class="snns file orange">lsubr ( ? ⊑ ? )</td>
+            <td class="snnn file orange">lsubr_lsubr</td>
             <td class="snnn file orange">
               <br />
             </td>
@@ -1066,9 +1056,9 @@
             <td class="nnns component orange">
               <br />
             </td>
-            <td class="snns plane orange">restricted local env. ref.</td>
-            <td class="snns file orange">lsubr ( ? ⊑ ? )</td>
-            <td class="snnn file orange">lsubr_lsubr</td>
+            <td class="snns plane orange">local env. ref. for extended substitution</td>
+            <td class="snns file orange">lsuby ( ? ⊑×[?,?] ? )</td>
+            <td class="snnn file orange">lsuby_lsuby</td>
             <td class="snnn file orange">
               <br />
             </td>
@@ -1128,7 +1118,7 @@
             </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_sn ldrop_ldrop</td>
+            <td class="snnn file orange">ldrop_lpx_sn ldrop_leq ldrop_ldrop</td>
             <td class="snnn file orange">
               <br />
             </td>
@@ -1168,6 +1158,20 @@
           </tr>
           <tr>
             <td class="snns component red">grammar</td>
+            <td class="snns plane red">equivalence for local environments</td>
+            <td class="snns file red">leq ( ? ≃[?,?] ? )</td>
+            <td class="snnn file red">leq_leq</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">pointwise extension of a relation</td>
             <td class="snns file red">lpx_sn</td>
             <td class="snnn file red">lpx_sn_tc lpx_sn_lpx_sn</td>
@@ -1197,8 +1201,8 @@
               <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="snns file red">cl_weight ( ♯{?,?,?} )</td>
+            <td class="snnn file red">cl_restricted_weight ( ♯{?,?} )</td>
             <td class="snnn file red">
               <br />
             </td>
@@ -1314,6 +1318,6 @@
     <div xmlns:ld="http://lambdadelta.info/" class="spacer">
       <br />
     </div>
-    <div xmlns:ld="http://lambdadelta.info/" class="spacer">Last update: Tue, 11 Feb 2014 22:11:38 +0100</div>
+    <div xmlns:ld="http://lambdadelta.info/" class="spacer">Last update: Fri, 21 Feb 2014 17:37:37 +0100</div>
 </body>
 </html>

diff --git a/helm/www/lambdadelta/ground_2.html b/helm/www/lambdadelta/ground_2.html
index 45c5ad29bc2e61611cc00da6eea4925fa34e1118..468fa65788c2208d1166594bdba3250f6ce40d02 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">31  </td>
+            <td class="snnn number cyan">29  </td>
             <td class="snns plane cyan">characters</td>
-            <td class="snnn number cyan">71828</td>
+            <td class="snnn number cyan">72188</td>
             <td class="snns plane cyan">nodes</td>
-            <td class="ssnn number cyan">56616</td>
+            <td class="ssnn number cyan">57742</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">168</td>
+            <td class="snnn number green">171</td>
             <td class="snns plane green">total</td>
-            <td class="ssnn number green">170</td>
+            <td class="ssnn number green">173</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: Tue, 11 Feb 2014 22:11:38 +0100</div>
+    <div xmlns:ld="http://lambdadelta.info/" class="spacer">Last update: Fri, 21 Feb 2014 17:37:37 +0100</div>
 </body>
 </html>