]> matita.cs.unibo.it Git - helm.git/blob - helm/www/lambdadelta/ground_2.html
update in ground_2
[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="[lambdadelta home]" title="lambdadelta 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="lambdadelta 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#lddl">library</a>
77             </td>
78             <td class="ssnn capitalize green">(<a href="http://lambdadelta.info/static/lddl/">static LDDL directory</a>)</td>
79           </tr>
80           <tr>
81             <td class="snss capitalize sky">
82               <a href="http://lambdadelta.info/index.html#citations">citations</a>
83             </td>
84             <td class="snss capitalize magenta">
85               <a href="http://lambdadelta.info/news.html#visibility">visibility</a>
86             </td>
87             <td class="snss capitalize white">
88               <a href="http://lambdadelta.info/specification.html#v1">version 1</a>
89             </td>
90             <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>
91             <td class="snsn capitalize white">(<a href="http://lambdadelta.info/static/matita/lambdadelta/">static HELM directory</a>)</td>
92             <td class="snss capitalize orange">
93               <a href="http://lambdadelta.info/documentation.html#v1">version 1</a>
94             </td>
95             <td class="snss capitalize green">
96               <a href="http://lambdadelta.info/implementation.html#helena">helena</a>
97             </td>
98             <td class="sssn capitalize green">
99               <br />
100             </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="lambdadelta 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">77</td>
136             <td class="snns italic cyan">characters</td>
137             <td class="snnn right italic cyan">93034</td>
138             <td class="snns italic cyan">nodes</td>
139             <td class="ssnn right italic cyan">195875</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">14</td>
145             <td class="snns italic green">lemmas</td>
146             <td class="snnn right italic green">434</td>
147             <td class="snns italic green">total</td>
148             <td class="ssnn right italic green">448</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">44</td>
154             <td class="snss italic yellow">defined</td>
155             <td class="snsn right italic yellow">37</td>
156             <td class="snss italic yellow">total</td>
157             <td class="sssn right italic yellow">81</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="lambdadelta 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="ssnn top gray">
243               <br />
244             </td>
245           </tr>
246           <tr>
247             <td class="snns top capitalize italic green">natural numbers with infinity</td>
248             <td class="snns top italic green" />
249             <td class="snns top green">ynat ( ∞ )</td>
250             <td class="snnn top green">ynat_pred ( ⫰? )</td>
251             <td class="snnn top green">ynat_succ ( ⫯? )</td>
252             <td class="snnn top green">ynat_le ( ? ≤ ? )</td>
253             <td class="snnn top green">ynat_lt ( ? &lt; ? )</td>
254             <td class="snnn top green">ynat_plus ( ? + ? )</td>
255             <td class="snnn top green">
256               <br />
257             </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="ssnn top green">
280               <br />
281             </td>
282           </tr>
283           <tr>
284             <td class="snns top capitalize italic grass">multiple relocation</td>
285             <td class="snns top italic grass" />
286             <td class="snns top grass">rtmap</td>
287             <td class="snnn top grass">rtmap_eq ( ? ≗ ? )</td>
288             <td class="snnn top grass">rtmap_tl ( ⫱? )</td>
289             <td class="snnn top grass">rtmap_tls ( ⫱*[?]? )</td>
290             <td class="snnn top grass">rtmap_isid ( 𝐈⦃?⦄ )</td>
291             <td class="snnn top grass">rtmap_id</td>
292             <td class="snnn top grass">rtmap_fcla ( 𝐂⦃?⦄ ≡ ? )</td>
293             <td class="snnn top grass">rtmap_isfin ( 𝐅⦃?⦄ )</td>
294             <td class="snnn top grass">rtmap_isuni ( 𝐔⦃?⦄ )</td>
295             <td class="snnn top grass">rtmap_sle ( ? ⊆ ? )</td>
296             <td class="snnn top grass">rtmap_sand ( ? ⋒ ? ≡ ? )</td>
297             <td class="snnn top grass">rtmap_sor ( ? ⋓ ? ≡ ? )</td>
298             <td class="snnn top grass">rtmap_at ( @⦃?,?⦄ ≡ ? )</td>
299             <td class="snnn top grass">rtmap_istot ( 𝐓⦃?⦄ )</td>
300             <td class="ssnn top grass">rtmap_after ( ? ⊚ ? ≡ ? )</td>
301           </tr>
302           <tr>
303             <td class="nnns top capitalize italic grass">
304               <br />
305             </td>
306             <td class="nnns top italic grass">
307               <br />
308             </td>
309             <td class="snns top grass">nstream ( ↑? ) ( ⫯? )</td>
310             <td class="snnn top grass">nstream_eq</td>
311             <td class="snnn top grass" />
312             <td class="snnn top grass" />
313             <td class="snnn top grass">nstream_isid</td>
314             <td class="snnn top grass">nstream_id ( 𝐈𝐝 )</td>
315             <td class="snnn top grass" />
316             <td class="snnn top grass" />
317             <td class="snnn top grass" />
318             <td class="snnn top grass" />
319             <td class="snnn top grass">nstream_sand</td>
320             <td class="snnn top grass" />
321             <td class="snnn top grass" />
322             <td class="snnn top grass">nstream_istot ( ?@❴?❵ )</td>
323             <td class="ssnn top grass">nstream_after ( ? ∘ ? )</td>
324           </tr>
325           <tr>
326             <td class="nnns top capitalize italic grass">
327               <br />
328             </td>
329             <td class="nnns top italic grass">
330               <br />
331             </td>
332             <td class="snns top grass">mr2</td>
333             <td class="snnn top grass">mr2_at ( @⦃?,?⦄ ≡ ? )</td>
334             <td class="snnn top grass">mr2_plus ( ? + ? )</td>
335             <td class="snnn top grass">mr2_minus ( ? ▭ ? ≡ ? )</td>
336             <td class="snnn top grass">
337               <br />
338             </td>
339             <td class="snnn top grass">
340               <br />
341             </td>
342             <td class="snnn top grass">
343               <br />
344             </td>
345             <td class="snnn top grass">
346               <br />
347             </td>
348             <td class="snnn top grass">
349               <br />
350             </td>
351             <td class="snnn top grass">
352               <br />
353             </td>
354             <td class="snnn top grass">
355               <br />
356             </td>
357             <td class="snnn top grass">
358               <br />
359             </td>
360             <td class="snnn top grass">
361               <br />
362             </td>
363             <td class="snnn top grass">
364               <br />
365             </td>
366             <td class="ssnn top grass">
367               <br />
368             </td>
369           </tr>
370           <tr>
371             <td class="snns top capitalize italic yellow">extensions to the library</td>
372             <td class="snns top italic yellow" />
373             <td class="snns top yellow">stream ( ? @ ? )</td>
374             <td class="snnn top yellow">stream_eq ( ? ≐ ? )</td>
375             <td class="snnn top yellow">stream_hdtl ( ↓? )</td>
376             <td class="snnn top yellow">stream_tls ( ↓*[?]? )</td>
377             <td class="snnn top yellow">
378               <br />
379             </td>
380             <td class="snnn top yellow">
381               <br />
382             </td>
383             <td class="snnn top yellow">
384               <br />
385             </td>
386             <td class="snnn top yellow">
387               <br />
388             </td>
389             <td class="snnn top yellow">
390               <br />
391             </td>
392             <td class="snnn top yellow">
393               <br />
394             </td>
395             <td class="snnn top yellow">
396               <br />
397             </td>
398             <td class="snnn top yellow">
399               <br />
400             </td>
401             <td class="snnn top yellow">
402               <br />
403             </td>
404             <td class="snnn top yellow">
405               <br />
406             </td>
407             <td class="ssnn top yellow">
408               <br />
409             </td>
410           </tr>
411           <tr>
412             <td class="nnns top capitalize italic yellow">
413               <br />
414             </td>
415             <td class="nnns top italic yellow">
416               <br />
417             </td>
418             <td class="snns top yellow">list ( ◊ ) ( ? @ ? ) ( |?| )</td>
419             <td class="snnn top yellow">list2 ( ◊ ) ( {?,?} @ ? ) ( ? @@ ? ) ( |?| )</td>
420             <td class="snnn top yellow">
421               <br />
422             </td>
423             <td class="snnn top yellow">
424               <br />
425             </td>
426             <td class="snnn top yellow">
427               <br />
428             </td>
429             <td class="snnn top yellow">
430               <br />
431             </td>
432             <td class="snnn top yellow">
433               <br />
434             </td>
435             <td class="snnn top yellow">
436               <br />
437             </td>
438             <td class="snnn top yellow">
439               <br />
440             </td>
441             <td class="snnn top yellow">
442               <br />
443             </td>
444             <td class="snnn top yellow">
445               <br />
446             </td>
447             <td class="snnn top yellow">
448               <br />
449             </td>
450             <td class="snnn top yellow">
451               <br />
452             </td>
453             <td class="snnn top yellow">
454               <br />
455             </td>
456             <td class="ssnn top yellow">
457               <br />
458             </td>
459           </tr>
460           <tr>
461             <td class="nnns top capitalize italic yellow">
462               <br />
463             </td>
464             <td class="nnns top italic yellow">
465               <br />
466             </td>
467             <td class="snns top yellow">bool ( Ⓕ ) ( Ⓣ )</td>
468             <td class="snnn top yellow">arith ( ?^? ) ( ⫯? ) ( ⫰? ) ( ? ∨ ? ) ( ? ∧ ? )</td>
469             <td class="snnn top yellow">
470               <br />
471             </td>
472             <td class="snnn top yellow">
473               <br />
474             </td>
475             <td class="snnn top yellow">
476               <br />
477             </td>
478             <td class="snnn top yellow">
479               <br />
480             </td>
481             <td class="snnn top yellow">
482               <br />
483             </td>
484             <td class="snnn top yellow">
485               <br />
486             </td>
487             <td class="snnn top yellow">
488               <br />
489             </td>
490             <td class="snnn top yellow">
491               <br />
492             </td>
493             <td class="snnn top yellow">
494               <br />
495             </td>
496             <td class="snnn top yellow">
497               <br />
498             </td>
499             <td class="snnn top yellow">
500               <br />
501             </td>
502             <td class="snnn top yellow">
503               <br />
504             </td>
505             <td class="ssnn top yellow">
506               <br />
507             </td>
508           </tr>
509           <tr>
510             <td class="nnns top capitalize italic yellow">
511               <br />
512             </td>
513             <td class="nnns top italic yellow">
514               <br />
515             </td>
516             <td class="snns top yellow">star</td>
517             <td class="snnn top yellow">lstar</td>
518             <td class="snnn top yellow">
519               <br />
520             </td>
521             <td class="snnn top yellow">
522               <br />
523             </td>
524             <td class="snnn top yellow">
525               <br />
526             </td>
527             <td class="snnn top yellow">
528               <br />
529             </td>
530             <td class="snnn top yellow">
531               <br />
532             </td>
533             <td class="snnn top yellow">
534               <br />
535             </td>
536             <td class="snnn top yellow">
537               <br />
538             </td>
539             <td class="snnn top yellow">
540               <br />
541             </td>
542             <td class="snnn top yellow">
543               <br />
544             </td>
545             <td class="snnn top yellow">
546               <br />
547             </td>
548             <td class="snnn top yellow">
549               <br />
550             </td>
551             <td class="snnn top yellow">
552               <br />
553             </td>
554             <td class="ssnn top yellow">
555               <br />
556             </td>
557           </tr>
558           <tr>
559             <td class="snns top capitalize italic orange">generated logical decomposables</td>
560             <td class="snns top italic orange" />
561             <td class="snns top orange">xoa ( ∃∃ ) ( ∨∨ ) ( ∧∧ )</td>
562             <td class="snnn top orange">xoa_props ( ⊥ ) ( ⊤ )</td>
563             <td class="snnn top orange">
564               <br />
565             </td>
566             <td class="snnn top orange">
567               <br />
568             </td>
569             <td class="snnn top orange">
570               <br />
571             </td>
572             <td class="snnn top orange">
573               <br />
574             </td>
575             <td class="snnn top orange">
576               <br />
577             </td>
578             <td class="snnn top orange">
579               <br />
580             </td>
581             <td class="snnn top orange">
582               <br />
583             </td>
584             <td class="snnn top orange">
585               <br />
586             </td>
587             <td class="snnn top orange">
588               <br />
589             </td>
590             <td class="snnn top orange">
591               <br />
592             </td>
593             <td class="snnn top orange">
594               <br />
595             </td>
596             <td class="snnn top orange">
597               <br />
598             </td>
599             <td class="ssnn top orange">
600               <br />
601             </td>
602           </tr>
603           <tr>
604             <td class="snss top capitalize italic red" />
605             <td class="snss top italic red" />
606             <td class="snss top red">
607               <br />
608             </td>
609             <td class="snsn top red">
610               <br />
611             </td>
612             <td class="snsn top red">
613               <br />
614             </td>
615             <td class="snsn top red">
616               <br />
617             </td>
618             <td class="snsn top red">
619               <br />
620             </td>
621             <td class="snsn top red">
622               <br />
623             </td>
624             <td class="snsn top red">
625               <br />
626             </td>
627             <td class="snsn top red">
628               <br />
629             </td>
630             <td class="snsn top red">
631               <br />
632             </td>
633             <td class="snsn top red">
634               <br />
635             </td>
636             <td class="snsn top red">
637               <br />
638             </td>
639             <td class="snsn top red">
640               <br />
641             </td>
642             <td class="snsn top red">
643               <br />
644             </td>
645             <td class="snsn top red">
646               <br />
647             </td>
648             <td class="sssn top red">
649               <br />
650             </td>
651           </tr>
652         </tbody>
653       </table>
654     </div>
655     <div class="spacer">
656       <img class="rule" alt="[Spacer]" title="lambdadelta rainbow rule" src="http://lambdadelta.info/images/rainbow.png" />
657     </div>
658     <div xmlns:ld="http://lambdadelta.info/" class="spacer">
659       <br />
660     </div>
661     <div xmlns:ld="http://lambdadelta.info/" class="spacer">
662       <a href="http://validator.w3.org/check?uri=referer">
663         <img class="w3c" alt="[Valid XHTML 1.1]" title="Valid XHTML 1.1" src="http://www.w3.org/Icons/valid-xhtml11-blue" />
664       </a>
665       <a href="http://jigsaw.w3.org/css-validator/check/referer">
666         <img class="w3c" alt="[Valid CSS level 2]" title="Valid CSS level 2" src="http://www.w3.org/Icons/valid-css2-blue" />
667       </a>
668       <a href="http://www.w3.org/XML/">
669         <img class="w3c" alt="[Generated from XML via XSL]" title="Generated from XML via XSL" src="http://lambdadelta.info/images/xml_xsl2.png" />
670       </a>
671       <a href="http://www.w3.org/Graphics/PNG/">
672         <img class="w3c" alt="[PNG used here]" title="PNG used here" src="http://lambdadelta.info/images/PNGnow2.png" />
673       </a>
674       <a href="http://www.anybrowser.org/campaign/">
675         <img class="w3c" alt="[Viewable with any browser]" title="Viewable with any browser" src="http://www.anybrowser.org/campaign/bvgraphics/abtfile.png" />
676       </a>
677     </div>
678     <div xmlns:ld="http://lambdadelta.info/" class="spacer">
679       <br />
680     </div>
681     <div xmlns:ld="http://lambdadelta.info/" class="spacer">Last update: Mon, 21 Mar 2016 20:38:12 +0100</div>
682   </body>
683 </html>