]> matita.cs.unibo.it Git - helm.git/commitdiff
- update in ground_2 and basic_2
authorFerruccio Guidi <ferruccio.guidi@unibo.it>
Tue, 31 May 2016 19:19:40 +0000 (19:19 +0000)
committerFerruccio Guidi <ferruccio.guidi@unibo.it>
Tue, 31 May 2016 19:19:40 +0000 (19:19 +0000)
- updated documentation

13 files changed:
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/download/ld_talk_9s.pdf [new file with mode: 0644]
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
helm/www/lambdadelta/web/home/documentation_2.tbl

index 9c0283b4512ce0a51a6e8e73de1b6e9313004c5c..602ed2c5700c56e88255e245bfbaba500438a9e7 100644 (file)
     <div xmlns:ld="http://lambdadelta.info/" class="spacer">
       <br />
     </div>
-    <div xmlns:ld="http://lambdadelta.info/" class="spacer">Last update: Sun, 22 May 2016 15:25:27 +0200</div>
+    <div xmlns:ld="http://lambdadelta.info/" class="spacer">Last update: Tue, 31 May 2016 21:18:47 +0200</div>
   </body>
 </html>
index 076412946b3e39f2e136194c5bcb408c48e84dba..720fb0deef193974a451f8eb322d4a6e6b53c0cd 100644 (file)
     <div xmlns:ld="http://lambdadelta.info/" class="spacer">
       <br />
     </div>
-    <div xmlns:ld="http://lambdadelta.info/" class="spacer">Last update: Sun, 22 May 2016 15:25:26 +0200</div>
+    <div xmlns:ld="http://lambdadelta.info/" class="spacer">Last update: Tue, 31 May 2016 21:18:47 +0200</div>
   </body>
 </html>
index 95170e646833d808a719d88715690b1918af094e..f6b288778064df3e1e84458509ad53095832be97 100644 (file)
     <div xmlns:ld="http://lambdadelta.info/" class="spacer">
       <br />
     </div>
-    <div xmlns:ld="http://lambdadelta.info/" class="spacer">Last update: Sun, 22 May 2016 15:25:27 +0200</div>
+    <div xmlns:ld="http://lambdadelta.info/" class="spacer">Last update: Tue, 31 May 2016 21:18:48 +0200</div>
   </body>
 </html>
index cbfde33d8998f2eedf37cceafb79f49c3c415f23..5c8b09d636efc67956f64d0349b594554d93c75d 100644 (file)
           <tr>
             <td class="snns capitalize italic cyan">sizes</td>
             <td class="snns italic cyan">files</td>
-            <td class="snnn right italic cyan">143</td>
+            <td class="snnn right italic cyan">150</td>
             <td class="snns italic cyan">characters</td>
-            <td class="snnn right italic cyan">116151</td>
+            <td class="snnn right italic cyan">121855</td>
             <td class="snns italic cyan">nodes</td>
-            <td class="ssnn right italic cyan">607262</td>
+            <td class="ssnn right italic cyan">618445</td>
           </tr>
           <tr>
             <td class="snns capitalize italic green">propositions</td>
             <td class="snns italic green">theorems</td>
-            <td class="snnn right italic green">46</td>
+            <td class="snnn right italic green">45</td>
             <td class="snns italic green">lemmas</td>
-            <td class="snnn right italic green">430</td>
+            <td class="snnn right italic green">458</td>
             <td class="snns italic green">total</td>
-            <td class="ssnn right italic green">476</td>
+            <td class="ssnn right italic green">503</td>
           </tr>
           <tr>
             <td class="snss capitalize italic yellow">concepts</td>
             <td class="snss italic yellow">declared</td>
             <td class="snsn right italic yellow">23</td>
             <td class="snss italic yellow">defined</td>
-            <td class="snsn right italic yellow">33</td>
+            <td class="snsn right italic yellow">34</td>
             <td class="snss italic yellow">total</td>
-            <td class="sssn right italic yellow">56</td>
+            <td class="sssn right italic yellow">57</td>
           </tr>
         </tbody>
       </table>
           <tr>
             <td class="snns top capitalize italic water">rt-transition</td>
             <td class="snns top italic water">uncounted context-sensitive rt-transition</td>
+            <td class="snns top water">lfpx ( ⦃?,?⦄ ⊢ ⬈[?,?] ? )</td>
+            <td class="snnn top water">lfpx_length lfpx_fqup</td>
+            <td class="snnn top water">
+              <br />
+            </td>
+            <td class="ssnn top water">
+              <br />
+            </td>
+          </tr>
+          <tr>
+            <td class="nnns top capitalize italic water">
+              <br />
+            </td>
+            <td class="nnns top italic water">
+              <br />
+            </td>
             <td class="snns top water">cpx ( ⦃?,?⦄ ⊢ ? ⬈[?] ? )</td>
             <td class="snnn top water">cpx_simple cpx_drops cpx_lsubr</td>
             <td class="snnn top water">
             </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">frees_weight frees_lreq frees_drops frees_frees</td>
             <td class="snnn top green">
               <br />
             </td>
     <div xmlns:ld="http://lambdadelta.info/" class="spacer">
       <br />
     </div>
-    <div xmlns:ld="http://lambdadelta.info/" class="spacer">Last update: Sun, 22 May 2016 15:25:27 +0200</div>
+    <div xmlns:ld="http://lambdadelta.info/" class="spacer">Last update: Tue, 31 May 2016 21:18:48 +0200</div>
   </body>
 </html>
index bca651cf172de7d70cce64a592b4b82fbf23a5f5..0fedfb1512b615e304f1cfee31e852ad092e10af 100644 (file)
               <br />
             </td>
           </tr>
+          <tr>
+            <td class="snns top" id="ldP2d">
+              <span class="emph alpha">P2d.</span>
+            </td>
+            <td class="ssnn top">F. Guidi: <a href="http://lambdadelta.info/download/ld_talk_9s.pdf">Considerations on Automath in Light of the Grundlagen</a> (<span class="emph beta">2016-05</span>). Presentation at University of Bologna (slides).</td>
+          </tr>
+          <tr>
+            <td class="nnns top" />
+            <td class="nsnn top">
+              <br />
+            </td>
+          </tr>
           <tr>
             <td class="snns top" id="ldP2c">
               <span class="emph alpha">P2c.</span>
     <div xmlns:ld="http://lambdadelta.info/" class="spacer">
       <br />
     </div>
-    <div xmlns:ld="http://lambdadelta.info/" class="spacer">Last update: Sun, 22 May 2016 15:25:26 +0200</div>
+    <div xmlns:ld="http://lambdadelta.info/" class="spacer">Last update: Tue, 31 May 2016 21:18:47 +0200</div>
   </body>
 </html>
diff --git a/helm/www/lambdadelta/download/ld_talk_9s.pdf b/helm/www/lambdadelta/download/ld_talk_9s.pdf
new file mode 100644 (file)
index 0000000..3f7c2be
Binary files /dev/null and b/helm/www/lambdadelta/download/ld_talk_9s.pdf differ
index 5e9c1defa8864a5e1ee518fa33443a8dd4162c05..bf75563e5e35ed01ba01f9987f13368be0804492 100644 (file)
     <div xmlns:ld="http://lambdadelta.info/" class="spacer">
       <br />
     </div>
-    <div xmlns:ld="http://lambdadelta.info/" class="spacer">Last update: Sun, 22 May 2016 15:25:27 +0200</div>
+    <div xmlns:ld="http://lambdadelta.info/" class="spacer">Last update: Tue, 31 May 2016 21:18:48 +0200</div>
   </body>
 </html>
index 4b32a65f670fa340f434d86d36fe5086693e1379..fc266948a2adda6efe5883b411193fbef3f51b7b 100644 (file)
           <tr>
             <td class="snns capitalize italic cyan">sizes</td>
             <td class="snns italic cyan">files</td>
-            <td class="snnn right italic cyan">86</td>
+            <td class="snnn right italic cyan">90</td>
             <td class="snns italic cyan">characters</td>
-            <td class="snnn right italic cyan">109249</td>
+            <td class="snnn right italic cyan">120841</td>
             <td class="snns italic cyan">nodes</td>
-            <td class="ssnn right italic cyan">217872</td>
+            <td class="ssnn right italic cyan">247853</td>
           </tr>
           <tr>
             <td class="snns capitalize italic green">propositions</td>
             <td class="snns italic green">theorems</td>
-            <td class="snnn right italic green">30</td>
+            <td class="snnn right italic green">32</td>
             <td class="snns italic green">lemmas</td>
-            <td class="snnn right italic green">506</td>
+            <td class="snnn right italic green">568</td>
             <td class="snns italic green">total</td>
-            <td class="ssnn right italic green">536</td>
+            <td class="ssnn right italic green">600</td>
           </tr>
           <tr>
             <td class="snss capitalize italic yellow">concepts</td>
             <td class="snss italic yellow">declared</td>
-            <td class="snsn right italic yellow">59</td>
+            <td class="snsn right italic yellow">60</td>
             <td class="snss italic yellow">defined</td>
-            <td class="snsn right italic yellow">55</td>
+            <td class="snsn right italic yellow">58</td>
             <td class="snss italic yellow">total</td>
-            <td class="sssn right italic yellow">114</td>
+            <td class="sssn right italic yellow">118</td>
           </tr>
         </tbody>
       </table>
             <td class="snnn top gray">
               <br />
             </td>
+            <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 water">
               <br />
             </td>
+            <td class="snnn top water">
+              <br />
+            </td>
+            <td class="snnn top water">
+              <br />
+            </td>
             <td class="ssnn top water">
               <br />
             </td>
             <td class="snns top italic green" />
             <td class="snns top green">rtmap</td>
             <td class="snnn top green">rtmap_eq ( ? ≗ ? )</td>
+            <td class="snnn top green">rtmap_pushs ( ↑*[?]? )</td>
             <td class="snnn top green">rtmap_tl ( ⫱? )</td>
             <td class="snnn top green">rtmap_tls ( ⫱*[?]? )</td>
             <td class="snnn top green">rtmap_isid ( 𝐈⦃?⦄ )</td>
             <td class="snnn top green">rtmap_sor ( ? ⋓ ? ≡ ? )</td>
             <td class="snnn top green">rtmap_at ( @⦃?,?⦄ ≡ ? )</td>
             <td class="snnn top green">rtmap_istot ( 𝐓⦃?⦄ )</td>
-            <td class="ssnn top green">rtmap_after ( ? ⊚ ? ≡ ? )</td>
+            <td class="snnn top green">rtmap_after ( ? ⊚ ? ≡ ? )</td>
+            <td class="ssnn top green">rtmap_coafter ( ? ~⊚ ? ≡ ? )</td>
           </tr>
           <tr>
             <td class="nnns top capitalize italic green">
             <td class="snnn top green">nstream_eq</td>
             <td class="snnn top green" />
             <td class="snnn top green" />
+            <td class="snnn top green" />
             <td class="snnn top green">nstream_isid</td>
             <td class="snnn top green">nstream_id ( 𝐈𝐝 )</td>
             <td class="snnn top green" />
             <td class="snnn top green" />
             <td class="snnn top green" />
             <td class="snnn top green">nstream_istot ( ?@❴?❵ )</td>
-            <td class="ssnn top green">nstream_after ( ? ∘ ? )</td>
+            <td class="snnn top green">nstream_after ( ? ∘ ? )</td>
+            <td class="ssnn top green" />
           </tr>
           <tr>
             <td class="nnns top capitalize italic green">
             <td class="snnn top green">
               <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">
               <br />
             </td>
+            <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="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="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="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="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="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="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, 22 May 2016 15:25:27 +0200</div>
+    <div xmlns:ld="http://lambdadelta.info/" class="spacer">Last update: Tue, 31 May 2016 21:18:47 +0200</div>
   </body>
 </html>
index c1593ebc3700b0d0cf874b1e9ff8ee9daf5a4674..6bf8c301f008dcc3d300fba505bcc8e6d51c97c2 100644 (file)
     <div xmlns:ld="http://lambdadelta.info/" class="spacer">
       <br />
     </div>
-    <div xmlns:ld="http://lambdadelta.info/" class="spacer">Last update: Sun, 22 May 2016 15:25:26 +0200</div>
+    <div xmlns:ld="http://lambdadelta.info/" class="spacer">Last update: Tue, 31 May 2016 21:18:47 +0200</div>
   </body>
 </html>
index 36ac7c63096ef24b6343ad1b1af97261a3596a7a..b3e330c9fe9867b7b1618e0c1ca59bd1f30bab08 100644 (file)
     <div xmlns:ld="http://lambdadelta.info/" class="spacer">
       <br />
     </div>
-    <div xmlns:ld="http://lambdadelta.info/" class="spacer">Last update: Sun, 22 May 2016 15:25:26 +0200</div>
+    <div xmlns:ld="http://lambdadelta.info/" class="spacer">Last update: Tue, 31 May 2016 21:18:47 +0200</div>
   </body>
 </html>
index 6ea5beda9c7b4ac8d06a58335b5806f6ae380ce3..6101558d2c81939a22c92e5c9dfb59d2c39c47fd 100644 (file)
     <div xmlns:ld="http://lambdadelta.info/" class="spacer">
       <br />
     </div>
-    <div xmlns:ld="http://lambdadelta.info/" class="spacer">Last update: Sun, 22 May 2016 15:25:26 +0200</div>
+    <div xmlns:ld="http://lambdadelta.info/" class="spacer">Last update: Tue, 31 May 2016 21:18:47 +0200</div>
   </body>
 </html>
index 4095590fbd5e925557b57089ce2885a679ffba9f..ec0d85773faf619b0cfd0c8ab78f9c5a66d81c9a 100644 (file)
     <div xmlns:ld="http://lambdadelta.info/" class="spacer">
       <br />
     </div>
-    <div xmlns:ld="http://lambdadelta.info/" class="spacer">Last update: Sun, 22 May 2016 15:25:26 +0200</div>
+    <div xmlns:ld="http://lambdadelta.info/" class="spacer">Last update: Tue, 31 May 2016 21:18:47 +0200</div>
   </body>
 </html>
index c61d2b6a08f36847ad102afe149c77ead5901225..3e59b57e63466f5dd3272788ee433ccb32fae2b8 100644 (file)
@@ -44,6 +44,14 @@ table {
      @@("documentation.html#bibtex" "BibTeX entry") ^ "."
      * }
    ] 
+   [ { name "ldP2d" "<span class=\"emph alpha\">P2d.</span>" "" } {
+     "F. Guidi:" + 
+     @@("download/ld_talk_9s.pdf"
+     "Considerations on Automath in Light of the Grundlagen") +
+     "(<span class=\"emph beta\">2016-05</span>)." +
+     "Presentation at University of Bologna (slides)."
+     * }
+   ]
    [ { name "ldP2c" "<span class=\"emph alpha\">P2c.</span>" "" } {
      "F. Guidi:" + 
      @@("download/ld_talk_8s.pdf"