]> matita.cs.unibo.it Git - helm.git/commitdiff
update in ground_2 and basic_2 ...
authorFerruccio Guidi <ferruccio.guidi@unibo.it>
Fri, 1 Apr 2016 21:31:50 +0000 (21:31 +0000)
committerFerruccio Guidi <ferruccio.guidi@unibo.it>
Fri, 1 Apr 2016 21:31:50 +0000 (21:31 +0000)
helm/www/lambdadelta/BTM.html
helm/www/lambdadelta/apps_2.html
helm/www/lambdadelta/basic_1.html
helm/www/lambdadelta/basic_2.html
helm/www/lambdadelta/documentation.html
helm/www/lambdadelta/ground_1.html
helm/www/lambdadelta/ground_2.html
helm/www/lambdadelta/implementation.html
helm/www/lambdadelta/index.html
helm/www/lambdadelta/news.html
helm/www/lambdadelta/specification.html

index 8202086a4272de83dcb36ebdf5d8fa3fa91b0efd..7f46bd1ef5c5131e78f474ab94b943fc53986aea 100644 (file)
     <div xmlns:ld="http://lambdadelta.info/" class="spacer">
       <br />
     </div>
-    <div xmlns:ld="http://lambdadelta.info/" class="spacer">Last update: Sun, 27 Mar 2016 18:42:30 +0200</div>
+    <div xmlns:ld="http://lambdadelta.info/" class="spacer">Last update: Fri, 01 Apr 2016 23:30:52 +0200</div>
   </body>
 </html>
index 35fdff6e84068f4f3234efd1aabc78b8e2a9f818..a0d1206ed676dae1b6c0411b90e99c22ed721419 100644 (file)
     <div xmlns:ld="http://lambdadelta.info/" class="spacer">
       <br />
     </div>
-    <div xmlns:ld="http://lambdadelta.info/" class="spacer">Last update: Sun, 27 Mar 2016 18:42:29 +0200</div>
+    <div xmlns:ld="http://lambdadelta.info/" class="spacer">Last update: Fri, 01 Apr 2016 23:30:52 +0200</div>
   </body>
 </html>
index 789062b5c081a6bb4b4e316db618378985aa8d9c..f4d0231452917f23da8d4343913fb3ae032d260a 100644 (file)
     <div xmlns:ld="http://lambdadelta.info/" class="spacer">
       <br />
     </div>
-    <div xmlns:ld="http://lambdadelta.info/" class="spacer">Last update: Sun, 27 Mar 2016 18:42:29 +0200</div>
+    <div xmlns:ld="http://lambdadelta.info/" class="spacer">Last update: Fri, 01 Apr 2016 23:30:53 +0200</div>
   </body>
 </html>
index 4003948a122714eaebe56cba462424f74d8ba675..5ae7da3063e1448a8bed8e391e332259463afc03 100644 (file)
           <tr>
             <td class="snns capitalize italic cyan">sizes</td>
             <td class="snns italic cyan">files</td>
-            <td class="snnn right italic cyan">83</td>
+            <td class="snnn right italic cyan">102</td>
             <td class="snns italic cyan">characters</td>
-            <td class="snnn right italic cyan">55955</td>
+            <td class="snnn right italic cyan">69295</td>
             <td class="snns italic cyan">nodes</td>
-            <td class="ssnn right italic cyan">191279</td>
+            <td class="ssnn right italic cyan">245853</td>
           </tr>
           <tr>
             <td class="snns capitalize italic green">propositions</td>
             <td class="snns italic green">theorems</td>
-            <td class="snnn right italic green">33</td>
+            <td class="snnn right italic green">34</td>
             <td class="snns italic green">lemmas</td>
-            <td class="snnn right italic green">211</td>
+            <td class="snnn right italic green">256</td>
             <td class="snns italic green">total</td>
-            <td class="ssnn right italic green">244</td>
+            <td class="ssnn right italic green">290</td>
           </tr>
           <tr>
             <td class="snss capitalize italic yellow">concepts</td>
             <td class="snss italic yellow">declared</td>
-            <td class="snsn right italic yellow">15</td>
+            <td class="snsn right italic yellow">21</td>
             <td class="snss italic yellow">defined</td>
-            <td class="snsn right italic yellow">23</td>
+            <td class="snsn right italic yellow">29</td>
             <td class="snss italic yellow">total</td>
-            <td class="sssn right italic yellow">38</td>
+            <td class="sssn right italic yellow">50</td>
           </tr>
         </tbody>
       </table>
             </td>
           </tr>
           <tr>
-            <td class="snns top capitalize italic yellow">relocation</td>
-            <td class="snns top italic yellow">ranged equivalence for closures</td>
-            <td class="snns top yellow">freq ( ⦃?,?,?⦄ ≡ ⦃?,?,?⦄ )</td>
-            <td class="snnn top yellow">freq_freq</td>
-            <td class="snnn top yellow">
+            <td class="snns top capitalize italic green">static typing</td>
+            <td class="snns top italic green">parameters</td>
+            <td class="snns top green">sh</td>
+            <td class="snnn top green">sd</td>
+            <td class="snnn top green">
               <br />
             </td>
-            <td class="ssnn top yellow">
+            <td class="ssnn top green">
               <br />
             </td>
           </tr>
           <tr>
-            <td class="nnns top capitalize italic yellow">
+            <td class="nnns top capitalize italic green">
               <br />
             </td>
-            <td class="snns top italic yellow">context-sensitive free variables</td>
-            <td class="snns top yellow">frees ( ? ⊢ 𝐅*⦃?⦄ ≡ ? )</td>
-            <td class="snnn top yellow">frees_weight frees_lreq frees_frees</td>
-            <td class="snnn top yellow">
+            <td class="snns top italic green">restricted ref. for local env.</td>
+            <td class="snns top green">lsubr ( ? ⫃ ? )</td>
+            <td class="snnn top green">lsubr_length lsubr_drops lsubr_lsubr</td>
+            <td class="snnn top green">
               <br />
             </td>
-            <td class="ssnn top yellow">
+            <td class="ssnn top green">
               <br />
             </td>
           </tr>
           <tr>
-            <td class="nnns top capitalize italic yellow">
+            <td class="nnns top capitalize italic green">
               <br />
             </td>
-            <td class="snns top italic yellow">generic slicing for local environments</td>
-            <td class="snns top yellow">drops_vector ( ⬇*[?,?] ? ≡ ? )</td>
-            <td class="snnn top yellow">
+            <td class="snns top italic green">ranged equivalence for closures</td>
+            <td class="snns top green">freq ( ⦃?,?,?⦄ ≡ ⦃?,?,?⦄ )</td>
+            <td class="snnn top green">freq_freq</td>
+            <td class="snnn top green">
               <br />
             </td>
+            <td class="ssnn top green">
+              <br />
+            </td>
+          </tr>
+          <tr>
+            <td class="nnns top capitalize italic green">
+              <br />
+            </td>
+            <td class="snns top italic green">context-sensitive free variables</td>
+            <td class="snns top green">frees ( ? ⊢ 𝐅*⦃?⦄ ≡ ? )</td>
+            <td class="snnn top green">frees_weight frees_lreq frees_frees</td>
+            <td class="snnn top green">
+              <br />
+            </td>
+            <td class="ssnn top green">
+              <br />
+            </td>
+          </tr>
+          <tr>
+            <td class="snns top capitalize italic grass">s-computation</td>
+            <td class="snns top italic grass" />
+            <td class="snns top grass">
+              <br />
+            </td>
+            <td class="snnn top grass">
+              <br />
+            </td>
+            <td class="snnn top grass">
+              <br />
+            </td>
+            <td class="ssnn top grass">
+              <br />
+            </td>
+          </tr>
+          <tr>
+            <td class="snns top capitalize italic yellow">s-transition</td>
+            <td class="snns top italic yellow">structural successor for closures</td>
+            <td class="snns top yellow">fquq ( ⦃?,?,?⦄ ⊐⸮ ⦃?,?,?⦄ )</td>
+            <td class="snnn top yellow">fquq_length fquq_weight</td>
             <td class="snnn top yellow">
               <br />
             </td>
             <td class="nnns top italic yellow">
               <br />
             </td>
-            <td class="snns top yellow">drops ( ⬇*[?,?] ? ≡ ? )</td>
-            <td class="snnn top yellow">drops_lstar drops_weight drops_length drops_ceq drops_lexs drops_lreq drops_drops</td>
+            <td class="snns top yellow">fqu ( ⦃?,?,?⦄ ⊐ ⦃?,?,?⦄ )</td>
+            <td class="snnn top yellow">fqu_length fqu_weight</td>
             <td class="snnn top yellow">
               <br />
             </td>
             </td>
           </tr>
           <tr>
-            <td class="nnns top capitalize italic yellow">
+            <td class="snns top capitalize italic orange">relocation</td>
+            <td class="snns top italic orange">generic slicing for local environments</td>
+            <td class="snns top orange">drops_vector ( ⬇*[?,?] ? ≡ ? )</td>
+            <td class="snnn top orange">
               <br />
             </td>
-            <td class="snns top italic yellow">generic relocation for terms</td>
-            <td class="snns top yellow">lifts_vector ( ⬆*[?] ? ≡ ? )</td>
-            <td class="snnn top yellow">lifts_lift_vector</td>
-            <td class="snnn top yellow">
+            <td class="snnn top orange">
               <br />
             </td>
-            <td class="ssnn top yellow">
+            <td class="ssnn top orange">
               <br />
             </td>
           </tr>
           <tr>
-            <td class="nnns top capitalize italic yellow">
+            <td class="nnns top capitalize italic orange">
               <br />
             </td>
-            <td class="nnns top italic yellow">
+            <td class="nnns top italic orange">
               <br />
             </td>
-            <td class="snns top yellow">lifts ( ⬆*[?] ? ≡ ? )</td>
-            <td class="snnn top yellow">lifts_simple lifts_weight lifts_lifts</td>
-            <td class="snnn top yellow">
+            <td class="snns top orange">drops ( ⬇*[?,?] ? ≡ ? )</td>
+            <td class="snnn top orange">drops_lstar drops_weight drops_length drops_ceq drops_lexs drops_lreq drops_drops</td>
+            <td class="snnn top orange">
               <br />
             </td>
-            <td class="ssnn top yellow">
+            <td class="ssnn top orange">
               <br />
             </td>
           </tr>
           <tr>
-            <td class="nnns top capitalize italic yellow">
+            <td class="nnns top capitalize italic orange">
               <br />
             </td>
-            <td class="snns top italic yellow">ranged equivalence for local environments</td>
-            <td class="snns top yellow">lreq ( ? ≡[?] ? )</td>
-            <td class="snnn top yellow">lreq_length lreq_lreq</td>
-            <td class="snnn top yellow">
+            <td class="snns top italic orange">generic relocation for terms</td>
+            <td class="snns top orange">lifts_vector ( ⬆*[?] ? ≡ ? )</td>
+            <td class="snnn top orange">lifts_lifts_vector</td>
+            <td class="snnn top orange">
               <br />
             </td>
-            <td class="ssnn top yellow">
+            <td class="ssnn top orange">
               <br />
             </td>
           </tr>
           <tr>
-            <td class="nnns top capitalize italic yellow">
+            <td class="nnns top capitalize italic orange">
               <br />
             </td>
-            <td class="snns top italic yellow">generic entrywise extension of context-sensitive relations for terma</td>
-            <td class="snns top yellow">lexs ( ? ⦻*[?,?,?] ? )</td>
-            <td class="snnn top yellow">lexs_length lexs_lexs</td>
-            <td class="snnn top yellow">
+            <td class="nnns top italic orange">
               <br />
             </td>
-            <td class="ssnn top yellow">
+            <td class="snns top orange">lifts ( ⬆*[?] ? ≡ ? )</td>
+            <td class="snnn top orange">lifts_simple lifts_weight lifts_lifts</td>
+            <td class="snnn top orange">
+              <br />
+            </td>
+            <td class="ssnn top orange">
               <br />
             </td>
           </tr>
           <tr>
-            <td class="snns top capitalize italic orange" />
-            <td class="snns top italic orange" />
-            <td class="snns top orange">
+            <td class="nnns top capitalize italic orange">
               <br />
             </td>
+            <td class="snns top italic orange">ranged equivalence for local environments</td>
+            <td class="snns top orange">lreq ( ? ≡[?] ? )</td>
+            <td class="snnn top orange">lreq_length lreq_lreq</td>
             <td class="snnn top orange">
               <br />
             </td>
+            <td class="ssnn top orange">
+              <br />
+            </td>
+          </tr>
+          <tr>
+            <td class="nnns top capitalize italic orange">
+              <br />
+            </td>
+            <td class="snns top italic orange">generic entrywise extension of context-sensitive relations for terma</td>
+            <td class="snns top orange">lexs ( ? ⦻*[?,?,?] ? )</td>
+            <td class="snnn top orange">lexs_length lexs_lexs</td>
             <td class="snnn top orange">
               <br />
             </td>
           </tr>
           <tr>
             <td class="snns top capitalize italic red">grammar</td>
+            <td class="snns top italic red">append for local environments</td>
+            <td class="snns top red">append ( ? @@ ? )</td>
+            <td class="snnn top red">append_length</td>
+            <td class="snnn top red">
+              <br />
+            </td>
+            <td class="ssnn top red">
+              <br />
+            </td>
+          </tr>
+          <tr>
+            <td class="nnns top capitalize italic red">
+              <br />
+            </td>
             <td class="snns top italic red">context-sensitive equivalences for terms</td>
             <td class="snns top red">ceq</td>
             <td class="snnn top red">ceq_ceq</td>
             <td class="snns top red">lenv</td>
             <td class="snnn top red">lenv_weight ( ♯{?} )</td>
             <td class="snnn top red">lenv_length ( |?| )</td>
-            <td class="ssnn top red">lenv_append ( ? @@ ? )</td>
+            <td class="ssnn top red">
+              <br />
+            </td>
           </tr>
           <tr>
             <td class="nnns top capitalize italic red">
     <div xmlns:ld="http://lambdadelta.info/" class="spacer">
       <br />
     </div>
-    <div xmlns:ld="http://lambdadelta.info/" class="spacer">Last update: Sun, 27 Mar 2016 18:42:29 +0200</div>
+    <div xmlns:ld="http://lambdadelta.info/" class="spacer">Last update: Fri, 01 Apr 2016 23:30:53 +0200</div>
   </body>
 </html>
index e00c7ab8eeae33b15227072f662db20542fcdffd..29a1e83cb0e25db23e88eff0f93b2913fabc0a66 100644 (file)
     <div xmlns:ld="http://lambdadelta.info/" class="spacer">
       <br />
     </div>
-    <div xmlns:ld="http://lambdadelta.info/" class="spacer">Last update: Sun, 27 Mar 2016 18:42:29 +0200</div>
+    <div xmlns:ld="http://lambdadelta.info/" class="spacer">Last update: Fri, 01 Apr 2016 23:30:52 +0200</div>
   </body>
 </html>
index d3e660577ca008b3bb19522fc31b4a09b8e02b3b..a29a85f850f3ee9881e930fb59bd16fe8e845861 100644 (file)
     <div xmlns:ld="http://lambdadelta.info/" class="spacer">
       <br />
     </div>
-    <div xmlns:ld="http://lambdadelta.info/" class="spacer">Last update: Sun, 27 Mar 2016 18:42:29 +0200</div>
+    <div xmlns:ld="http://lambdadelta.info/" class="spacer">Last update: Fri, 01 Apr 2016 23:30:53 +0200</div>
   </body>
 </html>
index 598ae85dc37fe5f365f79b8b27392314a761e6b6..e66ca0d4bfa6f3d328e47411770ce5a5512bb167 100644 (file)
           <tr>
             <td class="snns capitalize italic cyan">sizes</td>
             <td class="snns italic cyan">files</td>
-            <td class="snnn right italic cyan">77</td>
+            <td class="snnn right italic cyan">79</td>
             <td class="snns italic cyan">characters</td>
-            <td class="snnn right italic cyan">93671</td>
+            <td class="snnn right italic cyan">96249</td>
             <td class="snns italic cyan">nodes</td>
-            <td class="ssnn right italic cyan">198031</td>
+            <td class="ssnn right italic cyan">206180</td>
           </tr>
           <tr>
             <td class="snns capitalize italic green">propositions</td>
             <td class="snns italic green">theorems</td>
             <td class="snnn right italic green">23</td>
             <td class="snns italic green">lemmas</td>
-            <td class="snnn right italic green">472</td>
+            <td class="snnn right italic green">495</td>
             <td class="snns italic green">total</td>
-            <td class="ssnn right italic green">495</td>
+            <td class="ssnn right italic green">518</td>
           </tr>
           <tr>
             <td class="snss capitalize italic yellow">concepts</td>
             <td class="snss italic yellow">declared</td>
             <td class="snsn right italic yellow">53</td>
             <td class="snss italic yellow">defined</td>
-            <td class="snsn right italic yellow">49</td>
+            <td class="snsn right italic yellow">50</td>
             <td class="snss italic yellow">total</td>
-            <td class="sssn right italic yellow">102</td>
+            <td class="sssn right italic yellow">103</td>
           </tr>
         </tbody>
       </table>
             <td class="snnn top gray">
               <br />
             </td>
+            <td class="snnn top gray">
+              <br />
+            </td>
             <td class="ssnn top gray">
               <br />
             </td>
             <td class="snnn top green">
               <br />
             </td>
+            <td class="snnn top green">
+              <br />
+            </td>
             <td class="ssnn top green">
               <br />
             </td>
             <td class="snnn top grass">rtmap_fcla ( 𝐂⦃?⦄ ≡ ? )</td>
             <td class="snnn top grass">rtmap_isfin ( 𝐅⦃?⦄ )</td>
             <td class="snnn top grass">rtmap_isuni ( 𝐔⦃?⦄ )</td>
+            <td class="snnn top grass">rtmap_uni ( 𝐔❴?❵ )</td>
             <td class="snnn top grass">rtmap_sle ( ? ⊆ ? )</td>
             <td class="snnn top grass">rtmap_sand ( ? ⋒ ? ≡ ? )</td>
             <td class="snnn top grass">rtmap_sor ( ? ⋓ ? ≡ ? )</td>
             <td class="snnn top grass" />
             <td class="snnn top grass" />
             <td class="snnn top grass" />
+            <td class="snnn top grass" />
             <td class="snnn top grass">nstream_sand</td>
             <td class="snnn top grass" />
             <td class="snnn top grass" />
             <td class="snnn top grass">
               <br />
             </td>
+            <td class="snnn top grass">
+              <br />
+            </td>
             <td class="ssnn top grass">
               <br />
             </td>
             <td class="snnn top yellow">
               <br />
             </td>
+            <td class="snnn top yellow">
+              <br />
+            </td>
             <td class="ssnn top yellow">
               <br />
             </td>
             <td class="snnn top yellow">
               <br />
             </td>
+            <td class="snnn top yellow">
+              <br />
+            </td>
             <td class="ssnn top yellow">
               <br />
             </td>
             <td class="snnn top yellow">
               <br />
             </td>
+            <td class="snnn top yellow">
+              <br />
+            </td>
             <td class="ssnn top yellow">
               <br />
             </td>
             <td class="snnn top yellow">
               <br />
             </td>
+            <td class="snnn top yellow">
+              <br />
+            </td>
             <td class="ssnn top yellow">
               <br />
             </td>
             <td class="snnn top orange">
               <br />
             </td>
+            <td class="snnn top orange">
+              <br />
+            </td>
             <td class="ssnn top orange">
               <br />
             </td>
             <td class="snsn top red">
               <br />
             </td>
+            <td class="snsn top red">
+              <br />
+            </td>
             <td class="sssn top red">
               <br />
             </td>
     <div xmlns:ld="http://lambdadelta.info/" class="spacer">
       <br />
     </div>
-    <div xmlns:ld="http://lambdadelta.info/" class="spacer">Last update: Sun, 27 Mar 2016 18:42:29 +0200</div>
+    <div xmlns:ld="http://lambdadelta.info/" class="spacer">Last update: Fri, 01 Apr 2016 23:30:52 +0200</div>
   </body>
 </html>
index c9551cd119b2efd4abc0bd40e0664e1e8aed3a7a..eda6bd9352ce0bdecbe4595961641d36a877a73d 100644 (file)
     <div xmlns:ld="http://lambdadelta.info/" class="spacer">
       <br />
     </div>
-    <div xmlns:ld="http://lambdadelta.info/" class="spacer">Last update: Sun, 27 Mar 2016 18:42:29 +0200</div>
+    <div xmlns:ld="http://lambdadelta.info/" class="spacer">Last update: Fri, 01 Apr 2016 23:30:52 +0200</div>
   </body>
 </html>
index 14c85248a66dfe13211d6c9c3287af1fcd3c61df..d14a8519b6aa71b2e20c14840f394d5caa195ec8 100644 (file)
     <div xmlns:ld="http://lambdadelta.info/" class="spacer">
       <br />
     </div>
-    <div xmlns:ld="http://lambdadelta.info/" class="spacer">Last update: Sun, 27 Mar 2016 18:42:29 +0200</div>
+    <div xmlns:ld="http://lambdadelta.info/" class="spacer">Last update: Fri, 01 Apr 2016 23:30:52 +0200</div>
   </body>
 </html>
index 11a934d11617d63672bb7fb960b38a1804863b99..3971c904e9908f617455ca7b5effcbc00c5c0099 100644 (file)
     <div xmlns:ld="http://lambdadelta.info/" class="spacer">
       <br />
     </div>
-    <div xmlns:ld="http://lambdadelta.info/" class="spacer">Last update: Sun, 27 Mar 2016 18:42:29 +0200</div>
+    <div xmlns:ld="http://lambdadelta.info/" class="spacer">Last update: Fri, 01 Apr 2016 23:30:52 +0200</div>
   </body>
 </html>
index 1a8dae817d83b546083de303fd4762ef695d3764..41de394776bcc844420082b9933e428e56a0f042 100644 (file)
     <div xmlns:ld="http://lambdadelta.info/" class="spacer">
       <br />
     </div>
-    <div xmlns:ld="http://lambdadelta.info/" class="spacer">Last update: Sun, 27 Mar 2016 18:42:29 +0200</div>
+    <div xmlns:ld="http://lambdadelta.info/" class="spacer">Last update: Fri, 01 Apr 2016 23:30:52 +0200</div>
   </body>
 </html>