]> matita.cs.unibo.it Git - helm.git/blobdiff - helm/www/lambdadelta/basic_2.html
- update in basic_2
[helm.git] / helm / www / lambdadelta / basic_2.html
index d8633e5fff7af50c5d7790f94ccddb13c5ccaf59..8726a8ae7af783a0d24a729e2854b367b4db4b20 100644 (file)
             <td class="snns italic cyan">files</td>
             <td class="snnn right italic cyan">367</td>
             <td class="snns italic cyan">characters</td>
-            <td class="snnn right italic cyan">431848</td>
+            <td class="snnn right italic cyan">431944</td>
             <td class="snns italic cyan">nodes</td>
-            <td class="ssnn right italic cyan">1830463</td>
+            <td class="ssnn right italic cyan">1830639</td>
           </tr>
           <tr>
             <td class="snns capitalize italic green">propositions</td>
             <td class="snns italic green">theorems</td>
             <td class="snnn right italic green">128</td>
             <td class="snns italic green">lemmas</td>
-            <td class="snnn right italic green">1303</td>
+            <td class="snnn right italic green">1304</td>
             <td class="snns italic green">total</td>
-            <td class="ssnn right italic green">1431</td>
+            <td class="ssnn right italic green">1432</td>
           </tr>
           <tr>
             <td class="snss capitalize italic yellow">concepts</td>
@@ -85,6 +85,8 @@
         </tbody>
       </table>
     </div>
+
+   <div xmlns:ld="http://lambdadelta.info/" class="head3sn" id="">Stage "B"</div>
    <ul xmlns:ld="http://lambdadelta.info/">
       <li>
         <span class="date">In progress.</span>
@@ -92,6 +94,8 @@
          for native type assignment.
    </li>
     </ul>
+
+   <div xmlns:ld="http://lambdadelta.info/" class="head3sn" id="">Stage "A": "Weakening the Applicability Condition"</div>
    <ul xmlns:ld="http://lambdadelta.info/">
       <li>
         <span class="date">2014 June 18.</span>
               <br />
             </td>
             <td class="snns top cyan">csx_vector ( ⦃?,?⦄ ⊢ ⬊*[?,?] ? )</td>
-            <td class="snnn top cyan">csx_tstc_vector csx_aaa</td>
+            <td class="snnn top cyan">csx_tsts_vector csx_aaa</td>
             <td class="snnn top cyan">
               <br />
             </td>
               <br />
             </td>
             <td class="snns top cyan">cpxs ( ⦃?,?⦄ ⊢ ? ➡*[?,?] ? )</td>
-            <td class="snnn top cyan">cpxs_tstc cpxs_tstc_vector cpxs_leq cpxs_lift cpxs_lleq cpxs_aaa cpxs_cpxs</td>
+            <td class="snnn top cyan">cpxs_tsts cpxs_tsts_vector cpxs_leq cpxs_lift cpxs_lleq cpxs_aaa cpxs_cpxs</td>
             <td class="snnn top cyan">
               <br />
             </td>
             <td class="nnns top capitalize italic cyan">
               <br />
             </td>
-            <td class="snns top italic cyan">local env. ref. for abstract candidates of reducibility</td>
+            <td class="snns top italic cyan">local env. ref. for generic reducibility</td>
             <td class="snns top cyan">lsubc ( ? ⊢ ? ⫃[?] ? )</td>
             <td class="snnn top cyan">lsubc_drop lsubc_drops lsubc_lsuba</td>
             <td class="snnn top cyan">
             <td class="nnns top capitalize italic cyan">
               <br />
             </td>
-            <td class="snns top italic cyan">support for abstract computation properties</td>
-            <td class="snns top cyan">acp</td>
-            <td class="snnn top cyan">acp_cr ( ⦃?,?,?⦄ ϵ[?] 〚?〛 )</td>
-            <td class="snnn top cyan">acp_aaa</td>
+            <td class="snns top italic cyan">support for generic computation properties</td>
+            <td class="snns top cyan">gcp</td>
+            <td class="snnn top cyan">gcp_cr ( ⦃?,?,?⦄ ϵ[?] 〚?〛 )</td>
+            <td class="snnn top cyan">gcp_aaa</td>
             <td class="ssnn top cyan">
               <br />
             </td>
             <td class="nnns top capitalize italic yellow">
               <br />
             </td>
-            <td class="snns top italic yellow">support for generic relocation</td>
-            <td class="snns top yellow">gr2 ( @⦃?,?⦄ ≡ ? )</td>
-            <td class="snnn top yellow">gr2_plus ( ? + ? )</td>
-            <td class="snnn top yellow">gr2_minus ( ? ▭ ? ≡ ? )</td>
-            <td class="ssnn top yellow">gr2_gr2</td>
+            <td class="snns top italic yellow">support for multiple relocation</td>
+            <td class="snns top yellow">mr2 ( @⦃?,?⦄ ≡ ? )</td>
+            <td class="snnn top yellow">mr2_plus ( ? + ? )</td>
+            <td class="snnn top yellow">mr2_minus ( ? ▭ ? ≡ ? )</td>
+            <td class="ssnn top yellow">mr2_mr2</td>
           </tr>
           <tr>
             <td class="snns top capitalize italic orange">substitution</td>
             <td class="nnns top capitalize italic red">
               <br />
             </td>
-            <td class="snns top italic red">same top term constructor</td>
-            <td class="snns top red">tstc ( ? ≂ ? )</td>
-            <td class="snnn top red">tstc_tstc tstc_vector</td>
+            <td class="snns top italic red">same top term structure</td>
+            <td class="snns top red">tsts ( ? ≂ ? )</td>
+            <td class="snnn top red">tsts_tsts tsts_vector</td>
             <td class="snnn top red">
               <br />
             </td>
     <div xmlns:ld="http://lambdadelta.info/" class="spacer">
       <br />
     </div>
-    <div xmlns:ld="http://lambdadelta.info/" class="spacer">Last update: Thu, 07 Aug 2014 19:13:43 +0200</div>
+    <div xmlns:ld="http://lambdadelta.info/" class="spacer">Last update: Sun, 10 Aug 2014 20:37:31 +0200</div>
 </body>
 </html>