]> matita.cs.unibo.it Git - helm.git/commitdiff
update in basic_2
authorFerruccio Guidi <ferruccio.guidi@unibo.it>
Sun, 21 Apr 2013 15:53:55 +0000 (15:53 +0000)
committerFerruccio Guidi <ferruccio.guidi@unibo.it>
Sun, 21 Apr 2013 15:53:55 +0000 (15:53 +0000)
helm/www/lambdadelta/BTM.html
helm/www/lambdadelta/apps_2.html
helm/www/lambdadelta/basic_2.html

index 928de2d644b68744458ff63fc1782061b6c50281..078cbbeb23bcd5db0e2cc5eddff27c583262e8d4 100644 (file)
     <div xmlns:ld="http://lambdadelta.info/" class="spacer">
       <br />
     </div>
-    <div xmlns:ld="http://lambdadelta.info/" class="spacer">Last update: Sat, 20 Apr 2013 21:34:40 +0200</div>
+    <div xmlns:ld="http://lambdadelta.info/" class="spacer">Last update: Sun, 21 Apr 2013 17:53:32 +0200</div>
 </body>
 </html>
index 340e2919d66275000bbb95db29e7be0c4c85d771..11b277a34c9afa0266fd0bbbd05c4ca78edc5490 100644 (file)
     <div xmlns:ld="http://lambdadelta.info/" class="spacer">
       <br />
     </div>
-    <div xmlns:ld="http://lambdadelta.info/" class="spacer">Last update: Sat, 20 Apr 2013 21:34:40 +0200</div>
+    <div xmlns:ld="http://lambdadelta.info/" class="spacer">Last update: Sun, 21 Apr 2013 17:53:32 +0200</div>
 </body>
 </html>
index cd756f629a03988a1c1d8f02cc8894a8acd341d6..3353e93a2901cf77068fee7b89c586272b6b8491 100644 (file)
           <tr>
             <td class="snns component cyan">sizes</td>
             <td class="snns plane cyan">files</td>
-            <td class="snnn number cyan">237  </td>
+            <td class="snnn number cyan">213  </td>
             <td class="snns plane cyan">characters</td>
-            <td class="snnn number cyan">420425</td>
+            <td class="snnn number cyan">392008</td>
             <td class="snns plane cyan">nodes</td>
-            <td class="ssnn number cyan">1063117</td>
+            <td class="ssnn number cyan">1052979</td>
           </tr>
           <tr>
             <td class="snns component green">propositions</td>
             <td class="snns plane green">theorems</td>
-            <td class="snnn number green">85</td>
+            <td class="snnn number green">79</td>
             <td class="snns plane green">lemmas</td>
-            <td class="snnn number green">946</td>
+            <td class="snnn number green">875</td>
             <td class="snns plane green">total</td>
-            <td class="ssnn number green">1031</td>
+            <td class="ssnn number green">954</td>
           </tr>
           <tr>
             <td class="snss component yellow">concepts</td>
             <td class="snss plane yellow">declared</td>
             <td class="snsn number yellow">45</td>
             <td class="snss plane yellow">defined</td>
-            <td class="snsn number yellow">80</td>
+            <td class="snsn number yellow">75</td>
             <td class="snss plane yellow">total</td>
-            <td class="sssn number yellow">125</td>
+            <td class="sssn number yellow">120</td>
           </tr>
         </tbody>
       </table>
             </td>
           </tr>
           <tr>
-            <td class="snns component water">reducibility</td>
-            <td class="snns plane water">context-sensitive focalized reduction</td>
-            <td class="snns file water">cfpr ( ? ⊢ ⦃?,?⦄ ➡ ⦃?,?⦄ )</td>
-            <td class="snnn file water">cnfpr_ltpss cfpr_aaa cfpr_cpr cfpr_cfpr</td>
+            <td class="snns component water">reduction</td>
+            <td class="snns plane water">context-sensitive normal forms</td>
+            <td class="snns file water">cnf ( ? ⊢ 𝐍⦃?⦄ )</td>
+            <td class="snnn file water">cnf_liftt cnf_crf cnf_cif</td>
             <td class="snnn file water">
               <br />
             </td>
               <br />
             </td>
           </tr>
-          <tr>
-            <td class="nnns component water">
-              <br />
-            </td>
-            <td class="snns plane water">context-free focalized reduction</td>
-            <td class="snns file water">lfpr ( ⦃?⦄ ➡ ⦃?⦄ )</td>
-            <td class="snnn file water">lfpr_alt ( ⦃?⦄ ➡➡ ⦃?⦄ )</td>
-            <td class="snnn file water">lfpr_aaa lfpr_cpr lfpr_fpr lfpr_lfpr</td>
-            <td class="snnn file water">
-              <br />
-            </td>
-            <td class="ssnn file water">
-              <br />
-            </td>
-          </tr>
           <tr>
             <td class="nnns component water">
               <br />
             <td class="nnns plane water">
               <br />
             </td>
-            <td class="snns file water">fpr ( ⦃?,?⦄ ➡ ⦃?,?⦄ )</td>
-            <td class="snnn file water">fpr_cpr fpr_fpr</td>
-            <td class="snnn file water">
-              <br />
-            </td>
+            <td class="snns file water">chnf ( ? ⊢ 𝐇𝐍⦃?⦄ )</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 normal forms</td>
-            <td class="snns file water">cnf ( ? ⊢ 𝐍⦃?⦄ )</td>
-            <td class="snnn file water">cnf_lift cnf_cif</td>
             <td class="snnn file water">
               <br />
             </td>
             <td class="nnns component water">
               <br />
             </td>
-            <td class="snns plane water">revised context-sensitive reduction</td>
+            <td class="snns plane water">context-sensitive reduction</td>
             <td class="snns file water">lpr ( ? ⊢ ➡ ? )</td>
-            <td class="snnn file water">lpr_ldrop lpr_cpr lpr_lpr</td>
+            <td class="snnn file water">lpr_ldrop lpr_cpss lpr_lpss lpr_aaa lpr_cpr lpr_lpr</td>
             <td class="snnn file water">
               <br />
             </td>
               <br />
             </td>
             <td class="snns file water">cpr ( ? ⊢ ? ➡ ? )</td>
-            <td class="snnn file water">cpr_lift</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 reduction</td>
-            <td class="snns file water">cpr ( ? ⊢ ? ➡ ? )</td>
-            <td class="snnn file water">cpr_lift cpr_tpss cpr_ltpss_dx cpr_ltpss_sn cpr_delift cpr_aaa cpr_ltpr cpr_cpr</td>
+            <td class="snnn file water">lpr_tshf cpr_lift cpr_cif</td>
             <td class="snnn file water">
               <br />
             </td>
               <br />
             </td>
           </tr>
-          <tr>
-            <td class="nnns component water">
-              <br />
-            </td>
-            <td class="snns plane water">context-free normal forms</td>
-            <td class="snns file water">thnf ( 𝐇𝐍⦃?⦄ )</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">context-free reduction</td>
-            <td class="snns file water">ltpr ( ? ➡ ? )</td>
-            <td class="snnn file water">ltpr_ldrop ltpr_tps ltpr_tpss ltpr_ltpss_dx ltpr_ltpss_sn ltpr_aaa ltpr_ltpr</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">tpr ( ? ➡ ? )</td>
-            <td class="snnn file water">tpr_lift tpr_delift tpr_tpr</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">unfold</td>
             <td class="snns plane green">restricted parallel computation</td>
     <div xmlns:ld="http://lambdadelta.info/" class="spacer">
       <br />
     </div>
-    <div xmlns:ld="http://lambdadelta.info/" class="spacer">Last update: Sat, 20 Apr 2013 21:34:40 +0200</div>
+    <div xmlns:ld="http://lambdadelta.info/" class="spacer">Last update: Sun, 21 Apr 2013 17:53:32 +0200</div>
 </body>
 </html>