]> matita.cs.unibo.it Git - helm.git/blob - helm/www/lambdadelta/ground_2.html
8e32d0ff6d6e0edadb81f9ca0f7fb2348fbf7578
[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/home.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/home.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               <a href="http://lambdadelta.info/osn/">Open Symbolic Notation (OSN)</a>
80             </td>
81           </tr>
82           <tr>
83             <td class="snss capitalize sky">
84               <a href="http://lambdadelta.info/home.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="[butterfly]" 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">95</td>
136             <td class="snns italic cyan">characters</td>
137             <td class="snnn right italic cyan">131558</td>
138             <td class="snns italic cyan">nodes</td>
139             <td class="ssnn right italic cyan">304213</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">37</td>
145             <td class="snns italic green">lemmas</td>
146             <td class="snnn right italic green">626</td>
147             <td class="snns italic green">total</td>
148             <td class="ssnn right italic green">663</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">62</td>
154             <td class="snss italic yellow">defined</td>
155             <td class="snsn right italic yellow">66</td>
156             <td class="snss italic yellow">total</td>
157             <td class="sssn right italic yellow">128</td>
158           </tr>
159         </tbody>
160       </table>
161     </div>
162     <ul xmlns:ld="http://lambdadelta.info/">
163       <li>
164         <span class="emph alpha">2016 April 18.</span>
165          Generic rt-transition counter (rtc).
166    </li>
167     </ul>
168     <ul xmlns:ld="http://lambdadelta.info/">
169       <li>
170         <span class="emph alpha">2016 March 4.</span>
171          Platform-independent multiple relocation (rtmap).
172    </li>
173     </ul>
174     <ul xmlns:ld="http://lambdadelta.info/">
175       <li>
176         <span class="emph alpha">2016 January 20.</span>
177          Multiple relocation with streams of naturals.
178    </li>
179     </ul>
180     <ul xmlns:ld="http://lambdadelta.info/">
181       <li>
182         <span class="emph alpha">2015 October 11.</span>
183          Multiple relocation with lists of booleans.
184    </li>
185     </ul>
186     <ul xmlns:ld="http://lambdadelta.info/">
187       <li>
188         <span class="emph alpha">2013 November 27.</span>
189          Natural numbers with infinity (ynat).
190    </li>
191     </ul>
192     <ul xmlns:ld="http://lambdadelta.info/">
193       <li>
194         <span class="emph alpha">2011 August 10.</span>
195          Specification starts.
196    </li>
197     </ul>
198     <div xmlns:ld="http://lambdadelta.info/" class="head2dx" id="structure">Logical Structure of the Specification <img class="icon37" alt="[butterfly]" title="\lambda\delta butterfly" src="http://lambdadelta.info/images/b4.png" />
199     </div>
200     <div xmlns:ld="http://lambdadelta.info/" class="text">This table reports the specification's components and their planes.
201    </div>
202     <div xmlns:ld="http://lambdadelta.info/" class="text">
203       <table cellpadding="4" cellspacing="0">
204         <tbody>
205           <tr>
206             <td class="snns top capitalize italic gray">component</td>
207             <td class="snns top italic gray">plane</td>
208             <td class="snns top gray">files</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="snnn top gray">
246               <br />
247             </td>
248             <td class="snnn top gray">
249               <br />
250             </td>
251             <td class="snnn top gray">
252               <br />
253             </td>
254             <td class="snnn top gray">
255               <br />
256             </td>
257             <td class="ssnn top gray">
258               <br />
259             </td>
260           </tr>
261           <tr>
262             <td class="snns top capitalize italic water">generic rt-transition counter</td>
263             <td class="snns top italic water" />
264             <td class="snns top water">rtc ( 〈?,?,?,?〉 ) ( 𝟘𝟘 ) ( 𝟙𝟘 ) ( 𝟘𝟙 )</td>
265             <td class="snnn top water">rtc_isrc ( 𝐑𝐓⦃?, ?⦄ )</td>
266             <td class="snnn top water">rtc_shift ( ↓? )</td>
267             <td class="snnn top water">rtc_max ( ? ∨ ? )</td>
268             <td class="snnn top water">rtc_plus ( ? + ? )</td>
269             <td class="snnn top water">
270               <br />
271             </td>
272             <td class="snnn top water">
273               <br />
274             </td>
275             <td class="snnn top water">
276               <br />
277             </td>
278             <td class="snnn top water">
279               <br />
280             </td>
281             <td class="snnn top water">
282               <br />
283             </td>
284             <td class="snnn top water">
285               <br />
286             </td>
287             <td class="snnn top water">
288               <br />
289             </td>
290             <td class="snnn top water">
291               <br />
292             </td>
293             <td class="snnn top water">
294               <br />
295             </td>
296             <td class="snnn top water">
297               <br />
298             </td>
299             <td class="snnn top water">
300               <br />
301             </td>
302             <td class="snnn top water">
303               <br />
304             </td>
305             <td class="ssnn top water">
306               <br />
307             </td>
308           </tr>
309           <tr>
310             <td class="snns top capitalize italic green">multiple relocation</td>
311             <td class="snns top italic green" />
312             <td class="snns top green">rtmap</td>
313             <td class="snnn top green">rtmap_eq ( ? ≗ ? )</td>
314             <td class="snnn top green">rtmap_pushs ( ↑*[?]? )</td>
315             <td class="snnn top green">rtmap_tl ( ⫱? )</td>
316             <td class="snnn top green">rtmap_tls ( ⫱*[?]? )</td>
317             <td class="snnn top green">rtmap_isid ( 𝐈⦃?⦄ )</td>
318             <td class="snnn top green">rtmap_id</td>
319             <td class="snnn top green">rtmap_fcla ( 𝐂⦃?⦄ ≡ ? )</td>
320             <td class="snnn top green">rtmap_isfin ( 𝐅⦃?⦄ )</td>
321             <td class="snnn top green">rtmap_isuni ( 𝐔⦃?⦄ )</td>
322             <td class="snnn top green">rtmap_uni ( 𝐔❴?❵ )</td>
323             <td class="snnn top green">rtmap_sle ( ? ⊆ ? )</td>
324             <td class="snnn top green">rtmap_sand ( ? ⋒ ? ≡ ? )</td>
325             <td class="snnn top green">rtmap_sor ( ? ⋓ ? ≡ ? )</td>
326             <td class="snnn top green">rtmap_at ( @⦃?,?⦄ ≡ ? )</td>
327             <td class="snnn top green">rtmap_istot ( 𝐓⦃?⦄ )</td>
328             <td class="snnn top green">rtmap_after ( ? ⊚ ? ≡ ? )</td>
329             <td class="ssnn top green">rtmap_coafter ( ? ~⊚ ? ≡ ? )</td>
330           </tr>
331           <tr>
332             <td class="nnns top capitalize italic green">
333               <br />
334             </td>
335             <td class="nnns top italic green">
336               <br />
337             </td>
338             <td class="snns top green">nstream ( ↑? ) ( ⫯? )</td>
339             <td class="snnn top green">nstream_eq</td>
340             <td class="snnn top green" />
341             <td class="snnn top green" />
342             <td class="snnn top green" />
343             <td class="snnn top green">nstream_isid</td>
344             <td class="snnn top green">nstream_id ( 𝐈𝐝 )</td>
345             <td class="snnn top green" />
346             <td class="snnn top green" />
347             <td class="snnn top green" />
348             <td class="snnn top green" />
349             <td class="snnn top green" />
350             <td class="snnn top green">nstream_sand</td>
351             <td class="snnn top green" />
352             <td class="snnn top green" />
353             <td class="snnn top green">nstream_istot ( ?@❴?❵ )</td>
354             <td class="snnn top green">nstream_after ( ? ∘ ? )</td>
355             <td class="ssnn top green">nstream_coafter ( ? ~∘ ? )</td>
356           </tr>
357           <tr>
358             <td class="nnns top capitalize italic green">
359               <br />
360             </td>
361             <td class="nnns top italic green">
362               <br />
363             </td>
364             <td class="snns top green">mr2</td>
365             <td class="snnn top green">mr2_at ( @⦃?,?⦄ ≡ ? )</td>
366             <td class="snnn top green">mr2_plus ( ? + ? )</td>
367             <td class="snnn top green">mr2_minus ( ? ▭ ? ≡ ? )</td>
368             <td class="snnn top green">
369               <br />
370             </td>
371             <td class="snnn top green">
372               <br />
373             </td>
374             <td class="snnn top green">
375               <br />
376             </td>
377             <td class="snnn top green">
378               <br />
379             </td>
380             <td class="snnn top green">
381               <br />
382             </td>
383             <td class="snnn top green">
384               <br />
385             </td>
386             <td class="snnn top green">
387               <br />
388             </td>
389             <td class="snnn top green">
390               <br />
391             </td>
392             <td class="snnn top green">
393               <br />
394             </td>
395             <td class="snnn top green">
396               <br />
397             </td>
398             <td class="snnn top green">
399               <br />
400             </td>
401             <td class="snnn top green">
402               <br />
403             </td>
404             <td class="snnn top green">
405               <br />
406             </td>
407             <td class="ssnn top green">
408               <br />
409             </td>
410           </tr>
411           <tr>
412             <td class="snns top capitalize italic grass">natural numbers with infinity</td>
413             <td class="snns top italic grass" />
414             <td class="snns top grass">ynat ( ∞ )</td>
415             <td class="snnn top grass">ynat_pred ( ⫰? )</td>
416             <td class="snnn top grass">ynat_succ ( ⫯? )</td>
417             <td class="snnn top grass">ynat_le ( ? ≤ ? )</td>
418             <td class="snnn top grass">ynat_lt ( ? &lt; ? )</td>
419             <td class="snnn top grass">ynat_plus ( ? + ? )</td>
420             <td class="snnn top grass">
421               <br />
422             </td>
423             <td class="snnn top grass">
424               <br />
425             </td>
426             <td class="snnn top grass">
427               <br />
428             </td>
429             <td class="snnn top grass">
430               <br />
431             </td>
432             <td class="snnn top grass">
433               <br />
434             </td>
435             <td class="snnn top grass">
436               <br />
437             </td>
438             <td class="snnn top grass">
439               <br />
440             </td>
441             <td class="snnn top grass">
442               <br />
443             </td>
444             <td class="snnn top grass">
445               <br />
446             </td>
447             <td class="snnn top grass">
448               <br />
449             </td>
450             <td class="snnn top grass">
451               <br />
452             </td>
453             <td class="ssnn top grass">
454               <br />
455             </td>
456           </tr>
457           <tr>
458             <td class="snns top capitalize italic yellow">extensions to the library</td>
459             <td class="snns top italic yellow" />
460             <td class="snns top yellow">stream ( ? @ ? )</td>
461             <td class="snnn top yellow">stream_eq ( ? ≐ ? )</td>
462             <td class="snnn top yellow">stream_hdtl ( ↓? )</td>
463             <td class="snnn top yellow">stream_tls ( ↓*[?]? )</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="snnn top yellow">
474               <br />
475             </td>
476             <td class="snnn top yellow">
477               <br />
478             </td>
479             <td class="snnn top yellow">
480               <br />
481             </td>
482             <td class="snnn top yellow">
483               <br />
484             </td>
485             <td class="snnn top yellow">
486               <br />
487             </td>
488             <td class="snnn top yellow">
489               <br />
490             </td>
491             <td class="snnn top yellow">
492               <br />
493             </td>
494             <td class="snnn top yellow">
495               <br />
496             </td>
497             <td class="snnn top yellow">
498               <br />
499             </td>
500             <td class="snnn top yellow">
501               <br />
502             </td>
503             <td class="ssnn top yellow">
504               <br />
505             </td>
506           </tr>
507           <tr>
508             <td class="nnns top capitalize italic yellow">
509               <br />
510             </td>
511             <td class="nnns top italic yellow">
512               <br />
513             </td>
514             <td class="snns top yellow">list ( ◊ ) ( ? @ ? ) ( |?| )</td>
515             <td class="snnn top yellow">list2 ( ◊ ) ( {?,?} @ ? ) ( ? @@ ? ) ( |?| )</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="snnn top yellow">
526               <br />
527             </td>
528             <td class="snnn top yellow">
529               <br />
530             </td>
531             <td class="snnn top yellow">
532               <br />
533             </td>
534             <td class="snnn top yellow">
535               <br />
536             </td>
537             <td class="snnn top yellow">
538               <br />
539             </td>
540             <td class="snnn top yellow">
541               <br />
542             </td>
543             <td class="snnn top yellow">
544               <br />
545             </td>
546             <td class="snnn top yellow">
547               <br />
548             </td>
549             <td class="snnn top yellow">
550               <br />
551             </td>
552             <td class="snnn top yellow">
553               <br />
554             </td>
555             <td class="snnn top yellow">
556               <br />
557             </td>
558             <td class="snnn top yellow">
559               <br />
560             </td>
561             <td class="ssnn top yellow">
562               <br />
563             </td>
564           </tr>
565           <tr>
566             <td class="nnns top capitalize italic yellow">
567               <br />
568             </td>
569             <td class="nnns top italic yellow">
570               <br />
571             </td>
572             <td class="snns top yellow">bool ( Ⓕ ) ( Ⓣ )</td>
573             <td class="snnn top yellow">arith ( ?^? ) ( ⫯? ) ( ⫰? ) ( ? ∨ ? ) ( ? ∧ ? )</td>
574             <td class="snnn top yellow">
575               <br />
576             </td>
577             <td class="snnn top yellow">
578               <br />
579             </td>
580             <td class="snnn top yellow">
581               <br />
582             </td>
583             <td class="snnn top yellow">
584               <br />
585             </td>
586             <td class="snnn top yellow">
587               <br />
588             </td>
589             <td class="snnn top yellow">
590               <br />
591             </td>
592             <td class="snnn top yellow">
593               <br />
594             </td>
595             <td class="snnn top yellow">
596               <br />
597             </td>
598             <td class="snnn top yellow">
599               <br />
600             </td>
601             <td class="snnn top yellow">
602               <br />
603             </td>
604             <td class="snnn top yellow">
605               <br />
606             </td>
607             <td class="snnn top yellow">
608               <br />
609             </td>
610             <td class="snnn top yellow">
611               <br />
612             </td>
613             <td class="snnn top yellow">
614               <br />
615             </td>
616             <td class="snnn top yellow">
617               <br />
618             </td>
619             <td class="ssnn top yellow">
620               <br />
621             </td>
622           </tr>
623           <tr>
624             <td class="nnns top capitalize italic yellow">
625               <br />
626             </td>
627             <td class="nnns top italic yellow">
628               <br />
629             </td>
630             <td class="snns top yellow">star</td>
631             <td class="snnn top yellow">lstar</td>
632             <td class="snnn top yellow">
633               <br />
634             </td>
635             <td class="snnn top yellow">
636               <br />
637             </td>
638             <td class="snnn top yellow">
639               <br />
640             </td>
641             <td class="snnn top yellow">
642               <br />
643             </td>
644             <td class="snnn top yellow">
645               <br />
646             </td>
647             <td class="snnn top yellow">
648               <br />
649             </td>
650             <td class="snnn top yellow">
651               <br />
652             </td>
653             <td class="snnn top yellow">
654               <br />
655             </td>
656             <td class="snnn top yellow">
657               <br />
658             </td>
659             <td class="snnn top yellow">
660               <br />
661             </td>
662             <td class="snnn top yellow">
663               <br />
664             </td>
665             <td class="snnn top yellow">
666               <br />
667             </td>
668             <td class="snnn top yellow">
669               <br />
670             </td>
671             <td class="snnn top yellow">
672               <br />
673             </td>
674             <td class="snnn top yellow">
675               <br />
676             </td>
677             <td class="ssnn top yellow">
678               <br />
679             </td>
680           </tr>
681           <tr>
682             <td class="snns top capitalize italic orange">generated logical decomposables</td>
683             <td class="snns top italic orange" />
684             <td class="snns top orange">xoa ( ∃∃ ) ( ∨∨ ) ( ∧∧ )</td>
685             <td class="snnn top orange">xoa_props ( ⊥ ) ( ⊤ )</td>
686             <td class="snnn top orange">
687               <br />
688             </td>
689             <td class="snnn top orange">
690               <br />
691             </td>
692             <td class="snnn top orange">
693               <br />
694             </td>
695             <td class="snnn top orange">
696               <br />
697             </td>
698             <td class="snnn top orange">
699               <br />
700             </td>
701             <td class="snnn top orange">
702               <br />
703             </td>
704             <td class="snnn top orange">
705               <br />
706             </td>
707             <td class="snnn top orange">
708               <br />
709             </td>
710             <td class="snnn top orange">
711               <br />
712             </td>
713             <td class="snnn top orange">
714               <br />
715             </td>
716             <td class="snnn top orange">
717               <br />
718             </td>
719             <td class="snnn top orange">
720               <br />
721             </td>
722             <td class="snnn top orange">
723               <br />
724             </td>
725             <td class="snnn top orange">
726               <br />
727             </td>
728             <td class="snnn top orange">
729               <br />
730             </td>
731             <td class="ssnn top orange">
732               <br />
733             </td>
734           </tr>
735           <tr>
736             <td class="snss top capitalize italic red" />
737             <td class="snss top italic red" />
738             <td class="snss top red">
739               <br />
740             </td>
741             <td class="snsn top red">
742               <br />
743             </td>
744             <td class="snsn top red">
745               <br />
746             </td>
747             <td class="snsn top red">
748               <br />
749             </td>
750             <td class="snsn top red">
751               <br />
752             </td>
753             <td class="snsn top red">
754               <br />
755             </td>
756             <td class="snsn top red">
757               <br />
758             </td>
759             <td class="snsn top red">
760               <br />
761             </td>
762             <td class="snsn top red">
763               <br />
764             </td>
765             <td class="snsn top red">
766               <br />
767             </td>
768             <td class="snsn top red">
769               <br />
770             </td>
771             <td class="snsn top red">
772               <br />
773             </td>
774             <td class="snsn top red">
775               <br />
776             </td>
777             <td class="snsn top red">
778               <br />
779             </td>
780             <td class="snsn top red">
781               <br />
782             </td>
783             <td class="snsn top red">
784               <br />
785             </td>
786             <td class="snsn top red">
787               <br />
788             </td>
789             <td class="sssn top red">
790               <br />
791             </td>
792           </tr>
793         </tbody>
794       </table>
795     </div>
796     <div class="spacer">
797       <img class="rule" alt="[Spacer]" title="\lambda\delta rainbow rule" src="http://lambdadelta.info/images/rainbow.png" />
798     </div>
799     <div xmlns:ld="http://lambdadelta.info/" class="spacer">
800       <br />
801     </div>
802     <div xmlns:ld="http://lambdadelta.info/" class="spacer">
803       <a href="http://validator.w3.org/check?uri=referer">
804         <img class="w3c" alt="[Valid XHTML 1.1]" title="Valid XHTML 1.1" src="http://www.w3.org/Icons/valid-xhtml11-blue" />
805       </a>
806       <a href="http://jigsaw.w3.org/css-validator/check/referer">
807         <img class="w3c" alt="[Valid CSS level 2]" title="Valid CSS level 2" src="http://www.w3.org/Icons/valid-css2-blue" />
808       </a>
809       <a href="http://www.w3.org/XML/">
810         <img class="w3c" alt="[Generated from XML via XSL]" title="Generated from XML via XSL" src="http://lambdadelta.info/images/xml_xsl2.png" />
811       </a>
812       <a href="http://www.w3.org/Graphics/PNG/">
813         <img class="w3c" alt="[PNG used here]" title="PNG used here" src="http://lambdadelta.info/images/PNGnow2.png" />
814       </a>
815       <a href="http://www.anybrowser.org/campaign/">
816         <img class="w3c" alt="[Viewable with any browser]" title="Viewable with any browser" src="http://www.anybrowser.org/campaign/bvgraphics/abtfile.png" />
817       </a>
818     </div>
819     <div xmlns:ld="http://lambdadelta.info/" class="spacer">
820       <br />
821     </div>
822     <div xmlns:ld="http://lambdadelta.info/" class="spacer">Last update: Mon, 16 Jan 2017 12:25:24 +0100</div>
823   </body>
824 </html>