]> matita.cs.unibo.it Git - helm.git/blob - helm/www/lambdadelta/ground_2.html
the newly generated web pages ...
[helm.git] / helm / www / lambdadelta / ground_2.html
1 <?xml version="1.0" encoding="UTF-8"?>
2 <!DOCTYPE html PUBLIC "-//W3C//DTD XHTML 1.1//EN" "http://www.w3.org/TR/xhtml11/DTD/xhtml11.dtd">
3 <html xmlns="http://www.w3.org/1999/xhtml" dir="ltr" lang="en-us">
4   <head>
5     <meta http-equiv="Content-Language" content="en-us" />
6     <meta http-equiv="Content-Type" content="text/html; charset=UTF-8" />
7     <meta http-equiv="Content-Style-Type" content="text/css" />
8     <meta name="author" content="Ferruccio Guidi" />
9     <meta name="description" content="\lambda\delta home page" />
10     <title>\lambda\delta home page</title>
11     <link rel="stylesheet" type="text/css" href="http://lambdadelta.info/css/ld_web.css" />
12     <link rel="stylesheet" type="text/css" href="http://lambdadelta.info/css/lddl.css" />
13     <link rel="stylesheet" type="text/css" href="http://lambdadelta.info/css/xhtbl.css" />
14     <link rel="shortcut icon" href="http://lambdadelta.info/images/crux_16.ico" />
15   </head>
16   <body lang="en-US">
17     <div class="spacer">
18       <a href="http://lambdadelta.info/">
19         <img class="icon32" alt="[\lambda\delta home]" title="\lambda\delta home" src="http://lambdadelta.info/images/crux_32.png" />
20       </a>
21     </div>
22     <div class="head1">cic:/matita/lambdadelta/ground_2/ (background for λδ version 2)</div>
23     <div class="spacer">
24       <img class="rule" alt="[Spacer]" title="\lambda\delta rainbow rule" src="http://lambdadelta.info/images/rainbow.png" />
25     </div>
26     <div xmlns:ld="http://lambdadelta.info/" class="spacer">
27       <br />
28     </div>
29     <div xmlns:ld="http://lambdadelta.info/" class="text">
30       <table cellpadding="4" cellspacing="0">
31         <tbody>
32           <tr>
33             <td class="snns capitalize italic sky">
34               <a href="http://lambdadelta.info/index.html">home</a>
35             </td>
36             <td class="snns capitalize italic magenta">
37               <a href="http://lambdadelta.info/news.html">news</a>
38             </td>
39             <td class="snns capitalize italic white">
40               <a href="http://lambdadelta.info/specification.html">specification</a>
41             </td>
42             <td class="snnn capitalize italic white">
43               <br />
44             </td>
45             <td class="snnn capitalize italic white">
46               <br />
47             </td>
48             <td class="snns capitalize italic orange">
49               <a href="http://lambdadelta.info/documentation.html">documentation</a>
50             </td>
51             <td class="snns capitalize italic green">
52               <a href="http://lambdadelta.info/implementation.html">implementation</a>
53             </td>
54             <td class="ssnn capitalize italic green">
55               <br />
56             </td>
57           </tr>
58           <tr>
59             <td class="snns capitalize sky">
60               <a href="http://lambdadelta.info/index.html#foreword">foreword</a>
61             </td>
62             <td class="snns capitalize magenta">
63               <a href="http://lambdadelta.info/news.html#milestones">milestones</a>
64             </td>
65             <td class="snns capitalize white">
66               <a href="http://lambdadelta.info/specification.html#v2">version 2</a>
67             </td>
68             <td class="snnn capitalize white">(<a href="http://lambdadelta.info/ground_2.html">background</a> - <a href="http://lambdadelta.info/basic_2.html">core</a> - <a href="http://lambdadelta.info/apps_2.html">applications</a>)</td>
69             <td class="snnn capitalize white">
70               <br />
71             </td>
72             <td class="snns capitalize orange">
73               <a href="http://lambdadelta.info/documentation.html#v2">version 2</a>
74             </td>
75             <td class="snns capitalize green">
76               <a href="http://lambdadelta.info/implementation.html#helena">helena</a>
77             </td>
78             <td class="ssnn capitalize green">
79               <br />
80             </td>
81           </tr>
82           <tr>
83             <td class="snss capitalize sky">
84               <a href="http://lambdadelta.info/index.html#citations">citations</a>
85             </td>
86             <td class="snss capitalize magenta">
87               <a href="http://lambdadelta.info/news.html#visibility">visibility</a>
88             </td>
89             <td class="snss capitalize white">
90               <a href="http://lambdadelta.info/specification.html#v1">version 1</a>
91             </td>
92             <td class="snsn capitalize white">(<a href="http://lambdadelta.info/ground_1.html">background</a> - <a href="http://lambdadelta.info/basic_1.html">core</a>)</td>
93             <td class="snsn capitalize white">(<a href="http://lambdadelta.info/static/matita/lambdadelta/">static HELM directory</a>)</td>
94             <td class="snss capitalize orange">
95               <a href="http://lambdadelta.info/documentation.html#v1">version 1</a>
96             </td>
97             <td class="snss capitalize green">
98               <a href="http://lambdadelta.info/implementation.html#lddl">library</a>
99             </td>
100             <td class="sssn capitalize green">(<a href="http://lambdadelta.info/static/lddl/">static LDDL directory</a>)</td>
101           </tr>
102         </tbody>
103       </table>
104     </div>
105     <div xmlns:ld="http://lambdadelta.info/" class="head2dx" id="summary">Summary of the Specification <img class="icon37" alt="[spacer]" title="\lambda\delta butterfly" src="http://lambdadelta.info/images/b4.png" />
106     </div>
107     <div xmlns:ld="http://lambdadelta.info/" class="text">Here is a numerical account of the specification's contents
108          and its timeline.
109    </div>
110     <div xmlns:ld="http://lambdadelta.info/" class="text">
111       <table cellpadding="4" cellspacing="0">
112         <tbody>
113           <tr>
114             <td class="snns capitalize italic gray">category</td>
115             <td class="snns italic gray">objects</td>
116             <td class="snnn right italic gray">
117               <br />
118             </td>
119             <td class="snnn italic gray">
120               <br />
121             </td>
122             <td class="snnn right italic gray">
123               <br />
124             </td>
125             <td class="snnn italic gray">
126               <br />
127             </td>
128             <td class="ssnn right italic gray">
129               <br />
130             </td>
131           </tr>
132           <tr>
133             <td class="snns capitalize italic cyan">sizes</td>
134             <td class="snns italic cyan">files</td>
135             <td class="snnn right italic cyan">79</td>
136             <td class="snns italic cyan">characters</td>
137             <td class="snnn right italic cyan">96249</td>
138             <td class="snns italic cyan">nodes</td>
139             <td class="ssnn right italic cyan">206180</td>
140           </tr>
141           <tr>
142             <td class="snns capitalize italic green">propositions</td>
143             <td class="snns italic green">theorems</td>
144             <td class="snnn right italic green">23</td>
145             <td class="snns italic green">lemmas</td>
146             <td class="snnn right italic green">495</td>
147             <td class="snns italic green">total</td>
148             <td class="ssnn right italic green">518</td>
149           </tr>
150           <tr>
151             <td class="snss capitalize italic yellow">concepts</td>
152             <td class="snss italic yellow">declared</td>
153             <td class="snsn right italic yellow">53</td>
154             <td class="snss italic yellow">defined</td>
155             <td class="snsn right italic yellow">50</td>
156             <td class="snss italic yellow">total</td>
157             <td class="sssn right italic yellow">103</td>
158           </tr>
159         </tbody>
160       </table>
161     </div>
162     <ul xmlns:ld="http://lambdadelta.info/">
163       <li>
164         <span class="emph alpha">2016 March 4.</span>
165          Platform-independent multiple relocation (rtmap).
166    </li>
167     </ul>
168     <ul xmlns:ld="http://lambdadelta.info/">
169       <li>
170         <span class="emph alpha">2016 January 20.</span>
171          Multiple relocation with streams of naturals.
172    </li>
173     </ul>
174     <ul xmlns:ld="http://lambdadelta.info/">
175       <li>
176         <span class="emph alpha">2015 October 11.</span>
177          Multiple relocation with lists of booleans.
178    </li>
179     </ul>
180     <ul xmlns:ld="http://lambdadelta.info/">
181       <li>
182         <span class="emph alpha">2013 November 27.</span>
183          Natural numbers with infinity (ynat).
184    </li>
185     </ul>
186     <ul xmlns:ld="http://lambdadelta.info/">
187       <li>
188         <span class="emph alpha">2011 August 10.</span>
189          Specification starts.
190    </li>
191     </ul>
192     <div xmlns:ld="http://lambdadelta.info/" class="head2dx" id="structure">Logical Structure of the Specification <img class="icon37" alt="[spacer]" title="\lambda\delta butterfly" src="http://lambdadelta.info/images/b4.png" />
193     </div>
194     <div xmlns:ld="http://lambdadelta.info/" class="text">This table reports the specification's components and their planes.
195    </div>
196     <div xmlns:ld="http://lambdadelta.info/" class="text">
197       <table cellpadding="4" cellspacing="0">
198         <tbody>
199           <tr>
200             <td class="snns top capitalize italic gray">component</td>
201             <td class="snns top italic gray">plane</td>
202             <td class="snns top gray">files</td>
203             <td class="snnn top gray">
204               <br />
205             </td>
206             <td class="snnn top gray">
207               <br />
208             </td>
209             <td class="snnn top gray">
210               <br />
211             </td>
212             <td class="snnn top gray">
213               <br />
214             </td>
215             <td class="snnn top gray">
216               <br />
217             </td>
218             <td class="snnn top gray">
219               <br />
220             </td>
221             <td class="snnn top gray">
222               <br />
223             </td>
224             <td class="snnn top gray">
225               <br />
226             </td>
227             <td class="snnn top gray">
228               <br />
229             </td>
230             <td class="snnn top gray">
231               <br />
232             </td>
233             <td class="snnn top gray">
234               <br />
235             </td>
236             <td class="snnn top gray">
237               <br />
238             </td>
239             <td class="snnn top gray">
240               <br />
241             </td>
242             <td class="snnn top gray">
243               <br />
244             </td>
245             <td class="ssnn top gray">
246               <br />
247             </td>
248           </tr>
249           <tr>
250             <td class="snns top capitalize italic green">natural numbers with infinity</td>
251             <td class="snns top italic green" />
252             <td class="snns top green">ynat ( ∞ )</td>
253             <td class="snnn top green">ynat_pred ( ⫰? )</td>
254             <td class="snnn top green">ynat_succ ( ⫯? )</td>
255             <td class="snnn top green">ynat_le ( ? ≤ ? )</td>
256             <td class="snnn top green">ynat_lt ( ? &lt; ? )</td>
257             <td class="snnn top green">ynat_plus ( ? + ? )</td>
258             <td class="snnn top green">
259               <br />
260             </td>
261             <td class="snnn top green">
262               <br />
263             </td>
264             <td class="snnn top green">
265               <br />
266             </td>
267             <td class="snnn top green">
268               <br />
269             </td>
270             <td class="snnn top green">
271               <br />
272             </td>
273             <td class="snnn top green">
274               <br />
275             </td>
276             <td class="snnn top green">
277               <br />
278             </td>
279             <td class="snnn top green">
280               <br />
281             </td>
282             <td class="snnn top green">
283               <br />
284             </td>
285             <td class="ssnn top green">
286               <br />
287             </td>
288           </tr>
289           <tr>
290             <td class="snns top capitalize italic grass">multiple relocation</td>
291             <td class="snns top italic grass" />
292             <td class="snns top grass">rtmap</td>
293             <td class="snnn top grass">rtmap_eq ( ? ≗ ? )</td>
294             <td class="snnn top grass">rtmap_tl ( ⫱? )</td>
295             <td class="snnn top grass">rtmap_tls ( ⫱*[?]? )</td>
296             <td class="snnn top grass">rtmap_isid ( 𝐈⦃?⦄ )</td>
297             <td class="snnn top grass">rtmap_id</td>
298             <td class="snnn top grass">rtmap_fcla ( 𝐂⦃?⦄ ≡ ? )</td>
299             <td class="snnn top grass">rtmap_isfin ( 𝐅⦃?⦄ )</td>
300             <td class="snnn top grass">rtmap_isuni ( 𝐔⦃?⦄ )</td>
301             <td class="snnn top grass">rtmap_uni ( 𝐔❴?❵ )</td>
302             <td class="snnn top grass">rtmap_sle ( ? ⊆ ? )</td>
303             <td class="snnn top grass">rtmap_sand ( ? ⋒ ? ≡ ? )</td>
304             <td class="snnn top grass">rtmap_sor ( ? ⋓ ? ≡ ? )</td>
305             <td class="snnn top grass">rtmap_at ( @⦃?,?⦄ ≡ ? )</td>
306             <td class="snnn top grass">rtmap_istot ( 𝐓⦃?⦄ )</td>
307             <td class="ssnn top grass">rtmap_after ( ? ⊚ ? ≡ ? )</td>
308           </tr>
309           <tr>
310             <td class="nnns top capitalize italic grass">
311               <br />
312             </td>
313             <td class="nnns top italic grass">
314               <br />
315             </td>
316             <td class="snns top grass">nstream ( ↑? ) ( ⫯? )</td>
317             <td class="snnn top grass">nstream_eq</td>
318             <td class="snnn top grass" />
319             <td class="snnn top grass" />
320             <td class="snnn top grass">nstream_isid</td>
321             <td class="snnn top grass">nstream_id ( 𝐈𝐝 )</td>
322             <td class="snnn top grass" />
323             <td class="snnn top grass" />
324             <td class="snnn top grass" />
325             <td class="snnn top grass" />
326             <td class="snnn top grass" />
327             <td class="snnn top grass">nstream_sand</td>
328             <td class="snnn top grass" />
329             <td class="snnn top grass" />
330             <td class="snnn top grass">nstream_istot ( ?@❴?❵ )</td>
331             <td class="ssnn top grass">nstream_after ( ? ∘ ? )</td>
332           </tr>
333           <tr>
334             <td class="nnns top capitalize italic grass">
335               <br />
336             </td>
337             <td class="nnns top italic grass">
338               <br />
339             </td>
340             <td class="snns top grass">mr2</td>
341             <td class="snnn top grass">mr2_at ( @⦃?,?⦄ ≡ ? )</td>
342             <td class="snnn top grass">mr2_plus ( ? + ? )</td>
343             <td class="snnn top grass">mr2_minus ( ? ▭ ? ≡ ? )</td>
344             <td class="snnn top grass">
345               <br />
346             </td>
347             <td class="snnn top grass">
348               <br />
349             </td>
350             <td class="snnn top grass">
351               <br />
352             </td>
353             <td class="snnn top grass">
354               <br />
355             </td>
356             <td class="snnn top grass">
357               <br />
358             </td>
359             <td class="snnn top grass">
360               <br />
361             </td>
362             <td class="snnn top grass">
363               <br />
364             </td>
365             <td class="snnn top grass">
366               <br />
367             </td>
368             <td class="snnn top grass">
369               <br />
370             </td>
371             <td class="snnn top grass">
372               <br />
373             </td>
374             <td class="snnn top grass">
375               <br />
376             </td>
377             <td class="ssnn top grass">
378               <br />
379             </td>
380           </tr>
381           <tr>
382             <td class="snns top capitalize italic yellow">extensions to the library</td>
383             <td class="snns top italic yellow" />
384             <td class="snns top yellow">stream ( ? @ ? )</td>
385             <td class="snnn top yellow">stream_eq ( ? ≐ ? )</td>
386             <td class="snnn top yellow">stream_hdtl ( ↓? )</td>
387             <td class="snnn top yellow">stream_tls ( ↓*[?]? )</td>
388             <td class="snnn top yellow">
389               <br />
390             </td>
391             <td class="snnn top yellow">
392               <br />
393             </td>
394             <td class="snnn top yellow">
395               <br />
396             </td>
397             <td class="snnn top yellow">
398               <br />
399             </td>
400             <td class="snnn top yellow">
401               <br />
402             </td>
403             <td class="snnn top yellow">
404               <br />
405             </td>
406             <td class="snnn top yellow">
407               <br />
408             </td>
409             <td class="snnn top yellow">
410               <br />
411             </td>
412             <td class="snnn top yellow">
413               <br />
414             </td>
415             <td class="snnn top yellow">
416               <br />
417             </td>
418             <td class="snnn top yellow">
419               <br />
420             </td>
421             <td class="ssnn top yellow">
422               <br />
423             </td>
424           </tr>
425           <tr>
426             <td class="nnns top capitalize italic yellow">
427               <br />
428             </td>
429             <td class="nnns top italic yellow">
430               <br />
431             </td>
432             <td class="snns top yellow">list ( ◊ ) ( ? @ ? ) ( |?| )</td>
433             <td class="snnn top yellow">list2 ( ◊ ) ( {?,?} @ ? ) ( ? @@ ? ) ( |?| )</td>
434             <td class="snnn top yellow">
435               <br />
436             </td>
437             <td class="snnn top yellow">
438               <br />
439             </td>
440             <td class="snnn top yellow">
441               <br />
442             </td>
443             <td class="snnn top yellow">
444               <br />
445             </td>
446             <td class="snnn top yellow">
447               <br />
448             </td>
449             <td class="snnn top yellow">
450               <br />
451             </td>
452             <td class="snnn top yellow">
453               <br />
454             </td>
455             <td class="snnn top yellow">
456               <br />
457             </td>
458             <td class="snnn top yellow">
459               <br />
460             </td>
461             <td class="snnn top yellow">
462               <br />
463             </td>
464             <td class="snnn top yellow">
465               <br />
466             </td>
467             <td class="snnn top yellow">
468               <br />
469             </td>
470             <td class="snnn top yellow">
471               <br />
472             </td>
473             <td class="ssnn top yellow">
474               <br />
475             </td>
476           </tr>
477           <tr>
478             <td class="nnns top capitalize italic yellow">
479               <br />
480             </td>
481             <td class="nnns top italic yellow">
482               <br />
483             </td>
484             <td class="snns top yellow">bool ( Ⓕ ) ( Ⓣ )</td>
485             <td class="snnn top yellow">arith ( ?^? ) ( ⫯? ) ( ⫰? ) ( ? ∨ ? ) ( ? ∧ ? )</td>
486             <td class="snnn top yellow">
487               <br />
488             </td>
489             <td class="snnn top yellow">
490               <br />
491             </td>
492             <td class="snnn top yellow">
493               <br />
494             </td>
495             <td class="snnn top yellow">
496               <br />
497             </td>
498             <td class="snnn top yellow">
499               <br />
500             </td>
501             <td class="snnn top yellow">
502               <br />
503             </td>
504             <td class="snnn top yellow">
505               <br />
506             </td>
507             <td class="snnn top yellow">
508               <br />
509             </td>
510             <td class="snnn top yellow">
511               <br />
512             </td>
513             <td class="snnn top yellow">
514               <br />
515             </td>
516             <td class="snnn top yellow">
517               <br />
518             </td>
519             <td class="snnn top yellow">
520               <br />
521             </td>
522             <td class="snnn top yellow">
523               <br />
524             </td>
525             <td class="ssnn top yellow">
526               <br />
527             </td>
528           </tr>
529           <tr>
530             <td class="nnns top capitalize italic yellow">
531               <br />
532             </td>
533             <td class="nnns top italic yellow">
534               <br />
535             </td>
536             <td class="snns top yellow">star</td>
537             <td class="snnn top yellow">lstar</td>
538             <td class="snnn top yellow">
539               <br />
540             </td>
541             <td class="snnn top yellow">
542               <br />
543             </td>
544             <td class="snnn top yellow">
545               <br />
546             </td>
547             <td class="snnn top yellow">
548               <br />
549             </td>
550             <td class="snnn top yellow">
551               <br />
552             </td>
553             <td class="snnn top yellow">
554               <br />
555             </td>
556             <td class="snnn top yellow">
557               <br />
558             </td>
559             <td class="snnn top yellow">
560               <br />
561             </td>
562             <td class="snnn top yellow">
563               <br />
564             </td>
565             <td class="snnn top yellow">
566               <br />
567             </td>
568             <td class="snnn top yellow">
569               <br />
570             </td>
571             <td class="snnn top yellow">
572               <br />
573             </td>
574             <td class="snnn top yellow">
575               <br />
576             </td>
577             <td class="ssnn top yellow">
578               <br />
579             </td>
580           </tr>
581           <tr>
582             <td class="snns top capitalize italic orange">generated logical decomposables</td>
583             <td class="snns top italic orange" />
584             <td class="snns top orange">xoa ( ∃∃ ) ( ∨∨ ) ( ∧∧ )</td>
585             <td class="snnn top orange">xoa_props ( ⊥ ) ( ⊤ )</td>
586             <td class="snnn top orange">
587               <br />
588             </td>
589             <td class="snnn top orange">
590               <br />
591             </td>
592             <td class="snnn top orange">
593               <br />
594             </td>
595             <td class="snnn top orange">
596               <br />
597             </td>
598             <td class="snnn top orange">
599               <br />
600             </td>
601             <td class="snnn top orange">
602               <br />
603             </td>
604             <td class="snnn top orange">
605               <br />
606             </td>
607             <td class="snnn top orange">
608               <br />
609             </td>
610             <td class="snnn top orange">
611               <br />
612             </td>
613             <td class="snnn top orange">
614               <br />
615             </td>
616             <td class="snnn top orange">
617               <br />
618             </td>
619             <td class="snnn top orange">
620               <br />
621             </td>
622             <td class="snnn top orange">
623               <br />
624             </td>
625             <td class="ssnn top orange">
626               <br />
627             </td>
628           </tr>
629           <tr>
630             <td class="snss top capitalize italic red" />
631             <td class="snss top italic red" />
632             <td class="snss top red">
633               <br />
634             </td>
635             <td class="snsn top red">
636               <br />
637             </td>
638             <td class="snsn top red">
639               <br />
640             </td>
641             <td class="snsn top red">
642               <br />
643             </td>
644             <td class="snsn top red">
645               <br />
646             </td>
647             <td class="snsn top red">
648               <br />
649             </td>
650             <td class="snsn top red">
651               <br />
652             </td>
653             <td class="snsn top red">
654               <br />
655             </td>
656             <td class="snsn top red">
657               <br />
658             </td>
659             <td class="snsn top red">
660               <br />
661             </td>
662             <td class="snsn top red">
663               <br />
664             </td>
665             <td class="snsn top red">
666               <br />
667             </td>
668             <td class="snsn top red">
669               <br />
670             </td>
671             <td class="snsn top red">
672               <br />
673             </td>
674             <td class="snsn top red">
675               <br />
676             </td>
677             <td class="sssn top red">
678               <br />
679             </td>
680           </tr>
681         </tbody>
682       </table>
683     </div>
684     <div class="spacer">
685       <img class="rule" alt="[Spacer]" title="\lambda\delta rainbow rule" src="http://lambdadelta.info/images/rainbow.png" />
686     </div>
687     <div xmlns:ld="http://lambdadelta.info/" class="spacer">
688       <br />
689     </div>
690     <div xmlns:ld="http://lambdadelta.info/" class="spacer">
691       <a href="http://validator.w3.org/check?uri=referer">
692         <img class="w3c" alt="[Valid XHTML 1.1]" title="Valid XHTML 1.1" src="http://www.w3.org/Icons/valid-xhtml11-blue" />
693       </a>
694       <a href="http://jigsaw.w3.org/css-validator/check/referer">
695         <img class="w3c" alt="[Valid CSS level 2]" title="Valid CSS level 2" src="http://www.w3.org/Icons/valid-css2-blue" />
696       </a>
697       <a href="http://www.w3.org/XML/">
698         <img class="w3c" alt="[Generated from XML via XSL]" title="Generated from XML via XSL" src="http://lambdadelta.info/images/xml_xsl2.png" />
699       </a>
700       <a href="http://www.w3.org/Graphics/PNG/">
701         <img class="w3c" alt="[PNG used here]" title="PNG used here" src="http://lambdadelta.info/images/PNGnow2.png" />
702       </a>
703       <a href="http://www.anybrowser.org/campaign/">
704         <img class="w3c" alt="[Viewable with any browser]" title="Viewable with any browser" src="http://www.anybrowser.org/campaign/bvgraphics/abtfile.png" />
705       </a>
706     </div>
707     <div xmlns:ld="http://lambdadelta.info/" class="spacer">
708       <br />
709     </div>
710     <div xmlns:ld="http://lambdadelta.info/" class="spacer">Last update: Thu, 07 Apr 2016 15:45:52 +0200</div>
711   </body>
712 </html>