helm/www/lambdadelta/basic_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 version 2" />
  10     <title>\lambda\delta version 2</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/basic_2/ (λδ 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
  27
  28    <div xmlns:ld="http://lambdadelta.info/" class="head2sn" id="">Summary of the Specification</div>
  29    <div xmlns:ld="http://lambdadelta.info/" class="text">Here is a numerical acount of the specification's contents
  30          and its timeline.
  31          Nodes are counted according to the "intrinsinc complexity measure"
  32          [F. Guidi: "Procedural Representation of CIC Proof Terms"
  33          Journal of Automated Reasoning 44(1-2), Springer (February 2010),
  34          pp. 53-78].
  35    </div>
  36    <div xmlns:ld="http://lambdadelta.info/" class="text">
  37       <table cellpadding="4" cellspacing="0">
  38         <tbody>
  39           <tr>
  40             <td class="snns component gray">category</td>
  41             <td class="snns plane gray">objects</td>
  42             <td class="snnn number gray">
  43               <br />
  44             </td>
  45             <td class="snnn plane gray">
  46               <br />
  47             </td>
  48             <td class="snnn number gray">
  49               <br />
  50             </td>
  51             <td class="snnn plane gray">
  52               <br />
  53             </td>
  54             <td class="ssnn number gray">
  55               <br />
  56             </td>
  57           </tr>
  58           <tr>
  59             <td class="snns component cyan">sizes</td>
  60             <td class="snns plane cyan">files</td>
  61             <td class="snnn number cyan">367</td>
  62             <td class="snns plane cyan">characters</td>
  63             <td class="snnn number cyan">432045</td>
  64             <td class="snns plane cyan">nodes</td>
  65             <td class="ssnn number cyan">1831215</td>
  66           </tr>
  67           <tr>
  68             <td class="snns component green">propositions</td>
  69             <td class="snns plane green">theorems</td>
  70             <td class="snnn number green">128</td>
  71             <td class="snns plane green">lemmas</td>
  72             <td class="snnn number green">1303</td>
  73             <td class="snns plane green">total</td>
  74             <td class="ssnn number green">1431</td>
  75           </tr>
  76           <tr>
  77             <td class="snss component yellow">concepts</td>
  78             <td class="snss plane yellow">declared</td>
  79             <td class="snsn number yellow">55</td>
  80             <td class="snss plane yellow">defined</td>
  81             <td class="snsn number yellow">82</td>
  82             <td class="snss plane yellow">total</td>
  83             <td class="sssn number yellow">137</td>
  84           </tr>
  85         </tbody>
  86       </table>
  87     </div>
  88    <ul xmlns:ld="http://lambdadelta.info/">
  89       <li>
  90         <span class="date">In progress.</span>
  91          Context-sensitive subject equivalence
  92          for native type assignment.
  93    </li>
  94     </ul>
  95    <ul xmlns:ld="http://lambdadelta.info/">
  96       <li>
  97         <span class="date">2014 June 18.</span>
  98          Preservation of stratified native validity
  99          for context-sensitive computation on terms.
 100    </li>
 101     </ul>
 102    <ul xmlns:ld="http://lambdadelta.info/">
 103       <li>
 104         <span class="date">2014 June 9.</span>
 105          "Big tree" strong normalization
 106          for simply typed terms.
 107    </li>
 108     </ul>
 109    <ul xmlns:ld="http://lambdadelta.info/">
 110       <li>
 111         <span class="date">2014 April 16.</span>
 112          lazy equivalence on local environments
 113          serves as irrelevant step in "big tree" computation on closures
 114          (anniversary milestone).
 115    </li>
 116     </ul>
 117    <ul xmlns:ld="http://lambdadelta.info/">
 118       <li>
 119         <span class="date">2014 January 20.</span>
 120          Parametrized slicing for local environments
 121          comprises both versions of this operation
 122          (one from basic_1, the other used in basic_2 till now).
 123    </li>
 124     </ul>
 125    <ul xmlns:ld="http://lambdadelta.info/">
 126       <li>
 127         <span class="date">2013 August 7.</span>
 128          Passive support for global environments.
 129    </li>
 130     </ul>
 131    <ul xmlns:ld="http://lambdadelta.info/">
 132       <li>
 133         <span class="date">2013 July 27.</span>
 134          Reaxiomatized β-reductum as in extended β-reduction
 135    </li>
 136     </ul>
 137    <ul xmlns:ld="http://lambdadelta.info/">
 138       <li>
 139         <span class="date">2013 July 20.</span>
 140          Context-sensitive extended strong normalization
 141          for simply typed terms.
 142    </li>
 143     </ul>
 144    <ul xmlns:ld="http://lambdadelta.info/">
 145       <li>
 146         <span class="date">2013 April 16.</span>
 147          Reaxiomatized substitution and reduction
 148          commute with respect to subclosure
 149          (anniversary milestone).
 150    </li>
 151     </ul>
 152    <ul xmlns:ld="http://lambdadelta.info/">
 153       <li>
 154         <span class="date">2013 March 16.</span>
 155          Mutual recursive preservation of stratified native validity
 156          for "big tree" computation on closures.
 157    </li>
 158     </ul>
 159    <ul xmlns:ld="http://lambdadelta.info/">
 160       <li>
 161         <span class="date">2012 October 16.</span>
 162          Confluence for context-free parallel reduction on closures.
 163    </li>
 164     </ul>
 165    <ul xmlns:ld="http://lambdadelta.info/">
 166       <li>
 167         <span class="date">2012 July 26.</span>
 168          Term binders polarized to control ζ-reduction (not released).
 169    </li>
 170     </ul>
 171    <ul xmlns:ld="http://lambdadelta.info/">
 172       <li>
 173         <span class="date">2012 April 16.</span>
 174          Context-sensitive subject equivalence
 175          for atomic arity assignment
 176          (anniversary milestone).
 177    </li>
 178     </ul>
 179    <ul xmlns:ld="http://lambdadelta.info/">
 180       <li>
 181         <span class="date">2012 March 15.</span>
 182          Context-sensitive strong normalization
 183          for simply typed terms.
 184    </li>
 185     </ul>
 186    <ul xmlns:ld="http://lambdadelta.info/">
 187       <li>
 188         <span class="date">2012 January 27.</span>
 189          Support for abstract candidates of reducibility.
 190    </li>
 191     </ul>
 192    <ul xmlns:ld="http://lambdadelta.info/">
 193       <li>
 194         <span class="date">2011 September 21.</span>
 195          Confluence for context-sensitive parallel reduction on terms.
 196    </li>
 197     </ul>
 198    <ul xmlns:ld="http://lambdadelta.info/">
 199       <li>
 200         <span class="date">2011 September 6.</span>
 201          Confluence for context-free parallel reduction on terms.
 202    </li>
 203     </ul>
 204    <ul xmlns:ld="http://lambdadelta.info/">
 205       <li>
 206         <span class="date">2011 April 17.</span>
 207          Specification starts.
 208    </li>
 209     </ul>
 210
 211    <div xmlns:ld="http://lambdadelta.info/" class="head2sn" id="">Logical Structure of the Specification</div>
 212    <div xmlns:ld="http://lambdadelta.info/" class="text">The source files are grouped in planes and components
 213          according to the following table.
 214          Notation files covering the whole specification are provided.
 215          The notation for the relations or functions introduced in each file
 216          is shown in parentheses (? are placeholders).
 217    </div>
 218    <div xmlns:ld="http://lambdadelta.info/" class="text">
 219       <table cellpadding="4" cellspacing="0">
 220         <tbody>
 221           <tr>
 222             <td class="snns component gray">component</td>
 223             <td class="snns plane gray">plane</td>
 224             <td class="snns file gray">files</td>
 225             <td class="snnn file gray">
 226               <br />
 227             </td>
 228             <td class="snnn file gray">
 229               <br />
 230             </td>
 231             <td class="ssnn file gray">
 232               <br />
 233             </td>
 234           </tr>
 235           <tr>
 236             <td class="snns component wine">examples</td>
 237             <td class="snns plane wine">terms with special features</td>
 238             <td class="snns file wine">ex_cpr_omega</td>
 239             <td class="snnn file wine">
 240               <br />
 241             </td>
 242             <td class="snnn file wine">
 243               <br />
 244             </td>
 245             <td class="ssnn file wine">
 246               <br />
 247             </td>
 248           </tr>
 249           <tr>
 250             <td class="snns component magenta" />
 251             <td class="snns plane magenta" />
 252             <td class="snns file magenta" />
 253             <td class="snnn file magenta">
 254               <br />
 255             </td>
 256             <td class="snnn file magenta">
 257               <br />
 258             </td>
 259             <td class="ssnn file magenta">
 260               <br />
 261             </td>
 262           </tr>
 263           <tr>
 264             <td class="snns component prune">dynamic typing</td>
 265             <td class="snns plane prune">local env. ref. for stratified native validity</td>
 266             <td class="snns file prune">lsubsv ( ? ⊢ ? ⫃¡[?,?] ? )</td>
 267             <td class="snnn file prune">lsubsv_lsuba lsubsv_lsubd lsubsv_lstas lsubsv_scpds lsubsv_cpcs lsubsv_snv</td>
 268             <td class="snnn file prune">
 269               <br />
 270             </td>
 271             <td class="ssnn file prune">
 272               <br />
 273             </td>
 274           </tr>
 275           <tr>
 276             <td class="nnns component prune">
 277               <br />
 278             </td>
 279             <td class="snns plane prune">stratified native validity</td>
 280             <td class="snns file prune">shnv ( ⦃?,?⦄ ⊢ ? ¡[?,?,?] )</td>
 281             <td class="snnn file prune">shnv_aaa</td>
 282             <td class="snnn file prune">
 283               <br />
 284             </td>
 285             <td class="ssnn file prune">
 286               <br />
 287             </td>
 288           </tr>
 289           <tr>
 290             <td class="nnns component prune">
 291               <br />
 292             </td>
 293             <td class="nnns plane prune">
 294               <br />
 295             </td>
 296             <td class="snns file prune">snv ( ⦃?,?⦄ ⊢ ? ¡[?,?] )</td>
 297             <td class="snnn file prune">snv_lift snv_aaa snv_da_lpr snv_lstas snv_lstas_lpr snv_lpr snv_scpes snv_preserve</td>
 298             <td class="snnn file prune">
 299               <br />
 300             </td>
 301             <td class="ssnn file prune">
 302               <br />
 303             </td>
 304           </tr>
 305           <tr>
 306             <td class="snns component blue">equivalence</td>
 307             <td class="snns plane blue">decomposed extended equivalence</td>
 308             <td class="snns file blue">scpes ( ⦃?,?⦄ ⊢ ? •*⬌*[?,?,?,?] ? )</td>
 309             <td class="snnn file blue">scpes_aaa scpes_cpcs scpes_scpes</td>
 310             <td class="snnn file blue">
 311               <br />
 312             </td>
 313             <td class="ssnn file blue">
 314               <br />
 315             </td>
 316           </tr>
 317           <tr>
 318             <td class="nnns component blue">
 319               <br />
 320             </td>
 321             <td class="snns plane blue">context-sensitive equivalence</td>
 322             <td class="snns file blue">cpcs ( ⦃?,?⦄ ⊢ ? ⬌* ? )</td>
 323             <td class="snnn file blue">cpcs_aaa cpcs_cprs cpcs_cpcs</td>
 324             <td class="snnn file blue">
 325               <br />
 326             </td>
 327             <td class="ssnn file blue">
 328               <br />
 329             </td>
 330           </tr>
 331           <tr>
 332             <td class="snns component sky">conversion</td>
 333             <td class="snns plane sky">context-sensitive conversion</td>
 334             <td class="snns file sky">cpc ( ⦃?,?⦄ ⊢ ? ⬌ ? )</td>
 335             <td class="snnn file sky">cpc_cpc</td>
 336             <td class="snnn file sky">
 337               <br />
 338             </td>
 339             <td class="ssnn file sky">
 340               <br />
 341             </td>
 342           </tr>
 343           <tr>
 344             <td class="snns component cyan">computation</td>
 345             <td class="snns plane cyan">evaluation for context-sensitive extended reduction</td>
 346             <td class="snns file cyan">cpxe ( ⦃?,?⦄ ⊢ ➡*[?,?] 𝐍⦃?⦄ )</td>
 347             <td class="snnn file cyan">
 348               <br />
 349             </td>
 350             <td class="snnn file cyan">
 351               <br />
 352             </td>
 353             <td class="ssnn file cyan">
 354               <br />
 355             </td>
 356           </tr>
 357           <tr>
 358             <td class="nnns component cyan">
 359               <br />
 360             </td>
 361             <td class="snns plane cyan">evaluation for context-sensitive reduction</td>
 362             <td class="snns file cyan">cpre ( ⦃?,?⦄ ⊢ ➡* 𝐍⦃?⦄ )</td>
 363             <td class="snnn file cyan">cpre_cpre</td>
 364             <td class="snnn file cyan">
 365               <br />
 366             </td>
 367             <td class="ssnn file cyan">
 368               <br />
 369             </td>
 370           </tr>
 371           <tr>
 372             <td class="nnns component cyan">
 373               <br />
 374             </td>
 375             <td class="snns plane cyan">strongly normalizing "big tree" computation</td>
 376             <td class="snns file cyan">fsb ( ⦃?,?⦄ ⊢ ⦥[?,?] ? )</td>
 377             <td class="snnn file cyan">fsb_alt ( ⦃?,?⦄ ⊢ ⦥⦥[?,?] ? )</td>
 378             <td class="snnn file cyan">fsb_aaa fsb_csx</td>
 379             <td class="ssnn file cyan">
 380               <br />
 381             </td>
 382           </tr>
 383           <tr>
 384             <td class="nnns component cyan">
 385               <br />
 386             </td>
 387             <td class="snns plane cyan">strongly normalizing extended computation</td>
 388             <td class="snns file cyan">lcosx ( ? ⊢ ~⬊*[?,?,?] ? )</td>
 389             <td class="snnn file cyan">lcosx_cpx</td>
 390             <td class="snnn file cyan">
 391               <br />
 392             </td>
 393             <td class="ssnn file cyan">
 394               <br />
 395             </td>
 396           </tr>
 397           <tr>
 398             <td class="nnns component cyan">
 399               <br />
 400             </td>
 401             <td class="nnns plane cyan">
 402               <br />
 403             </td>
 404             <td class="snns file cyan">lsx ( ? ⊢ ⬊*[?,?,?,?] ? )</td>
 405             <td class="snnn file cyan">lsx_alt ( ? ⊢ ⬊⬊*[?,?,?,?] ? )</td>
 406             <td class="snnn file cyan">lsx_drop lsx_lpx lsx_lpxs llsx_csx</td>
 407             <td class="ssnn file cyan">
 408               <br />
 409             </td>
 410           </tr>
 411           <tr>
 412             <td class="nnns component cyan">
 413               <br />
 414             </td>
 415             <td class="nnns plane cyan">
 416               <br />
 417             </td>
 418             <td class="snns file cyan">csx_vector ( ⦃?,?⦄ ⊢ ⬊*[?,?] ? )</td>
 419             <td class="snnn file cyan">csx_tstc_vector csx_aaa</td>
 420             <td class="snnn file cyan">
 421               <br />
 422             </td>
 423             <td class="ssnn file cyan">
 424               <br />
 425             </td>
 426           </tr>
 427           <tr>
 428             <td class="nnns component cyan">
 429               <br />
 430             </td>
 431             <td class="nnns plane cyan">
 432               <br />
 433             </td>
 434             <td class="snns file cyan">csx ( ⦃?,?⦄ ⊢ ⬊*[?,?] ? )</td>
 435             <td class="snnn file cyan">csx_alt ( ⦃?,?⦄ ⊢ ⬊⬊*[?,?] ? )</td>
 436             <td class="snnn file cyan">csx_lift csx_lleq csx_lpx csx_lpxs csx_fpbs</td>
 437             <td class="ssnn file cyan">
 438               <br />
 439             </td>
 440           </tr>
 441           <tr>
 442             <td class="nnns component cyan">
 443               <br />
 444             </td>
 445             <td class="snns plane cyan">"big tree" parallel computation</td>
 446             <td class="snns file cyan">fpbg ( ⦃?,?,?⦄ &gt;≡[?,?] ⦃?,?,?⦄ )</td>
 447             <td class="snnn file cyan">fpbg_lift fpbg_fleq fpbg_fpbg</td>
 448             <td class="snnn file cyan">
 449               <br />
 450             </td>
 451             <td class="ssnn file cyan">
 452               <br />
 453             </td>
 454           </tr>
 455           <tr>
 456             <td class="nnns component cyan">
 457               <br />
 458             </td>
 459             <td class="nnns plane cyan">
 460               <br />
 461             </td>
 462             <td class="snns file cyan">fpbc ( ⦃?,?,?⦄ ≻≡[?,?] ⦃?,?,?⦄ )</td>
 463             <td class="snnn file cyan">fpbc_fleq fpbc_fpbs</td>
 464             <td class="snnn file cyan">
 465               <br />
 466             </td>
 467             <td class="ssnn file cyan">
 468               <br />
 469             </td>
 470           </tr>
 471           <tr>
 472             <td class="nnns component cyan">
 473               <br />
 474             </td>
 475             <td class="nnns plane cyan">
 476               <br />
 477             </td>
 478             <td class="snns file cyan">fpbu ( ⦃?,?,?⦄ ≻[?,?] ⦃?,?,?⦄ )</td>
 479             <td class="snnn file cyan">fpbu_lift fpbu_lleq</td>
 480             <td class="snnn file cyan">fpbu_fleq</td>
 481             <td class="ssnn file cyan">
 482               <br />
 483             </td>
 484           </tr>
 485           <tr>
 486             <td class="nnns component cyan">
 487               <br />
 488             </td>
 489             <td class="nnns plane cyan">
 490               <br />
 491             </td>
 492             <td class="snns file cyan">fpbs ( ⦃?,?,?⦄ ≥[?,?] ⦃?,?,?⦄ )</td>
 493             <td class="snnn file cyan">fpbs_alt ( ⦃?,?,?⦄ ≥≥[?,?] ⦃?,?,?⦄ )</td>
 494             <td class="snnn file cyan">fpbs_lift fpbs_fleq fpbs_aaa fpbs_fpbs fpbs_ext</td>
 495             <td class="ssnn file cyan">
 496               <br />
 497             </td>
 498           </tr>
 499           <tr>
 500             <td class="nnns component cyan">
 501               <br />
 502             </td>
 503             <td class="snns plane cyan">decomposed extended computation</td>
 504             <td class="snns file cyan">scpds ( ⦃?,?⦄ ⊢ ? •*➡*[?,?,?] ? )</td>
 505             <td class="snnn file cyan">scpds_lift scpds_aaa scpds_scpds</td>
 506             <td class="snnn file cyan">
 507               <br />
 508             </td>
 509             <td class="ssnn file cyan">
 510               <br />
 511             </td>
 512           </tr>
 513           <tr>
 514             <td class="nnns component cyan">
 515               <br />
 516             </td>
 517             <td class="snns plane cyan">context-sensitive extended computation</td>
 518             <td class="snns file cyan">lpxs ( ⦃?,?⦄ ⊢ ➡*[?,?] ? )</td>
 519             <td class="snnn file cyan">lpxs_drop lpxs_lleq lpxs_aaa lpxs_cpxs lpxs_lpxs</td>
 520             <td class="snnn file cyan">
 521               <br />
 522             </td>
 523             <td class="ssnn file cyan">
 524               <br />
 525             </td>
 526           </tr>
 527           <tr>
 528             <td class="nnns component cyan">
 529               <br />
 530             </td>
 531             <td class="nnns plane cyan">
 532               <br />
 533             </td>
 534             <td class="snns file cyan">cpxs ( ⦃?,?⦄ ⊢ ? ➡*[?,?] ? )</td>
 535             <td class="snnn file cyan">cpxs_tstc cpxs_tstc_vector cpxs_leq cpxs_lift cpxs_lleq cpxs_aaa cpxs_cpxs</td>
 536             <td class="snnn file cyan">
 537               <br />
 538             </td>
 539             <td class="ssnn file cyan">
 540               <br />
 541             </td>
 542           </tr>
 543           <tr>
 544             <td class="nnns component cyan">
 545               <br />
 546             </td>
 547             <td class="snns plane cyan">context-sensitive computation</td>
 548             <td class="snns file cyan">lprs ( ⦃?,?⦄ ⊢ ➡* ? )</td>
 549             <td class="snnn file cyan">lprs_drop lprs_cprs lprs_lprs</td>
 550             <td class="snnn file cyan">
 551               <br />
 552             </td>
 553             <td class="ssnn file cyan">
 554               <br />
 555             </td>
 556           </tr>
 557           <tr>
 558             <td class="nnns component cyan">
 559               <br />
 560             </td>
 561             <td class="nnns plane cyan">
 562               <br />
 563             </td>
 564             <td class="snns file cyan">cprs ( ⦃?,?⦄ ⊢ ? ➡* ?)</td>
 565             <td class="snnn file cyan">cprs_lift cprs_cprs</td>
 566             <td class="snnn file cyan">
 567               <br />
 568             </td>
 569             <td class="ssnn file cyan">
 570               <br />
 571             </td>
 572           </tr>
 573           <tr>
 574             <td class="nnns component cyan">
 575               <br />
 576             </td>
 577             <td class="snns plane cyan">local env. ref. for abstract candidates of reducibility</td>
 578             <td class="snns file cyan">lsubc ( ? ⊢ ? ⫃[?] ? )</td>
 579             <td class="snnn file cyan">lsubc_drop lsubc_drops lsubc_lsuba</td>
 580             <td class="snnn file cyan">
 581               <br />
 582             </td>
 583             <td class="ssnn file cyan">
 584               <br />
 585             </td>
 586           </tr>
 587           <tr>
 588             <td class="nnns component cyan">
 589               <br />
 590             </td>
 591             <td class="snns plane cyan">support for abstract computation properties</td>
 592             <td class="snns file cyan">acp</td>
 593             <td class="snnn file cyan">acp_cr ( ⦃?,?,?⦄ ϵ[?] 〚?〛 )</td>
 594             <td class="snnn file cyan">acp_aaa</td>
 595             <td class="ssnn file cyan">
 596               <br />
 597             </td>
 598           </tr>
 599           <tr>
 600             <td class="snns component water">reduction</td>
 601             <td class="snns plane water">"big tree" parallel reduction</td>
 602             <td class="snns file water">fpb ( ⦃?,?,?⦄ ≽[?,?] ⦃?,?,?⦄ )</td>
 603             <td class="snnn file water">fpb_lift fpb_aaa</td>
 604             <td class="snnn file water">
 605               <br />
 606             </td>
 607             <td class="ssnn file water">
 608               <br />
 609             </td>
 610           </tr>
 611           <tr>
 612             <td class="nnns component water">
 613               <br />
 614             </td>
 615             <td class="snns plane water">normal forms for context-sensitive extended reduction</td>
 616             <td class="snns file water">cnx ( ⦃?,?⦄ ⊢ ➡[?,?] 𝐍⦃?⦄ )</td>
 617             <td class="snnn file water">cnx_lift cnx_crx cnx_cix</td>
 618             <td class="snnn file water">
 619               <br />
 620             </td>
 621             <td class="ssnn file water">
 622               <br />
 623             </td>
 624           </tr>
 625           <tr>
 626             <td class="nnns component water">
 627               <br />
 628             </td>
 629             <td class="snns plane water">context-sensitive extended reduction</td>
 630             <td class="snns file water">lpx ( ⦃?,?⦄ ⊢ ➡[?,?] ? )</td>
 631             <td class="snnn file water">lpx_drop lpx_frees</td>
 632             <td class="snnn file water">lpx_lleq lpx_aaa</td>
 633             <td class="ssnn file water">
 634               <br />
 635             </td>
 636           </tr>
 637           <tr>
 638             <td class="nnns component water">
 639               <br />
 640             </td>
 641             <td class="nnns plane water">
 642               <br />
 643             </td>
 644             <td class="snns file water">cpx ( ⦃?,?⦄ ⊢ ? ➡[?,?] ? )</td>
 645             <td class="snnn file water">cpx_leq cpx_lift cpx_llpx_sn cpx_lleq cpx_cix</td>
 646             <td class="snnn file water">
 647               <br />
 648             </td>
 649             <td class="ssnn file water">
 650               <br />
 651             </td>
 652           </tr>
 653           <tr>
 654             <td class="nnns component water">
 655               <br />
 656             </td>
 657             <td class="snns plane water">irreducible forms for context-sensitive extended reduction</td>
 658             <td class="snns file water">cix ( ⦃?,?⦄ ⊢ ➡[?,?] 𝐈⦃?⦄ )</td>
 659             <td class="snnn file water">cix_lift</td>
 660             <td class="snnn file water">
 661               <br />
 662             </td>
 663             <td class="ssnn file water">
 664               <br />
 665             </td>
 666           </tr>
 667           <tr>
 668             <td class="nnns component water">
 669               <br />
 670             </td>
 671             <td class="snns plane water">reducible forms for context-sensitive extended reduction</td>
 672             <td class="snns file water">crx ( ⦃?,?⦄ ⊢ ➡[?,?] 𝐑⦃?⦄ )</td>
 673             <td class="snnn file water">crx_lift</td>
 674             <td class="snnn file water">
 675               <br />
 676             </td>
 677             <td class="ssnn file water">
 678               <br />
 679             </td>
 680           </tr>
 681           <tr>
 682             <td class="nnns component water">
 683               <br />
 684             </td>
 685             <td class="snns plane water">normal forms for context-sensitive reduction</td>
 686             <td class="snns file water">cnr ( ⦃?,?⦄ ⊢ ➡ 𝐍⦃?⦄ )</td>
 687             <td class="snnn file water">cnr_lift cnr_crr cnr_cir</td>
 688             <td class="snnn file water">
 689               <br />
 690             </td>
 691             <td class="ssnn file water">
 692               <br />
 693             </td>
 694           </tr>
 695           <tr>
 696             <td class="nnns component water">
 697               <br />
 698             </td>
 699             <td class="snns plane water">context-sensitive reduction</td>
 700             <td class="snns file water">lpr ( ⦃?,?⦄ ⊢ ➡ ? )</td>
 701             <td class="snnn file water">lpr_drop lpr_lpr</td>
 702             <td class="snnn file water">
 703               <br />
 704             </td>
 705             <td class="ssnn file water">
 706               <br />
 707             </td>
 708           </tr>
 709           <tr>
 710             <td class="nnns component water">
 711               <br />
 712             </td>
 713             <td class="nnns plane water">
 714               <br />
 715             </td>
 716             <td class="snns file water">cpr ( ⦃?,?⦄ ⊢ ? ➡ ? )</td>
 717             <td class="snnn file water">cpr_lift cpr_llpx_sn cpr_cir</td>
 718             <td class="snnn file water">
 719               <br />
 720             </td>
 721             <td class="ssnn file water">
 722               <br />
 723             </td>
 724           </tr>
 725           <tr>
 726             <td class="nnns component water">
 727               <br />
 728             </td>
 729             <td class="snns plane water">irreducible forms for context-sensitive reduction</td>
 730             <td class="snns file water">cir ( ⦃?,?⦄ ⊢ ➡ 𝐈⦃?⦄ )</td>
 731             <td class="snnn file water">cir_lift</td>
 732             <td class="snnn file water">
 733               <br />
 734             </td>
 735             <td class="ssnn file water">
 736               <br />
 737             </td>
 738           </tr>
 739           <tr>
 740             <td class="nnns component water">
 741               <br />
 742             </td>
 743             <td class="snns plane water">reducible forms for context-sensitive reduction</td>
 744             <td class="snns file water">crr ( ⦃?,?⦄ ⊢ ➡ 𝐑⦃?⦄ )</td>
 745             <td class="snnn file water">crr_lift</td>
 746             <td class="snnn file water">
 747               <br />
 748             </td>
 749             <td class="ssnn file water">
 750               <br />
 751             </td>
 752           </tr>
 753           <tr>
 754             <td class="snns component green">unfold</td>
 755             <td class="snns plane green">unfold</td>
 756             <td class="snns file green">unfold ( ⦃?,?⦄ ⊢ ? ⧫* ? )</td>
 757             <td class="snnn file green">
 758               <br />
 759             </td>
 760             <td class="snnn file green">
 761               <br />
 762             </td>
 763             <td class="ssnn file green">
 764               <br />
 765             </td>
 766           </tr>
 767           <tr>
 768             <td class="nnns component green">
 769               <br />
 770             </td>
 771             <td class="snns plane green">iterated static type assignment</td>
 772             <td class="snns file green">lstas ( ⦃?,?⦄ ⊢ ? •*[?,?] ? )</td>
 773             <td class="snnn file green">lstas_alt ( ⦃?,?⦄ ⊢ ? ••*[?,?] ? )</td>
 774             <td class="snnn file green">lstas_lift lstas_aaa lstas_da lstas_lstas</td>
 775             <td class="ssnn file green">
 776               <br />
 777             </td>
 778           </tr>
 779           <tr>
 780             <td class="snns component grass">static typing</td>
 781             <td class="snns plane grass">local env. ref. for degree assignment</td>
 782             <td class="snns file grass">lsubd ( ? ⊢ ? ⫃▪[?,?] ? )</td>
 783             <td class="snnn file grass">lsubd_da lsubd_lsubd</td>
 784             <td class="snnn file grass">
 785               <br />
 786             </td>
 787             <td class="ssnn file grass">
 788               <br />
 789             </td>
 790           </tr>
 791           <tr>
 792             <td class="nnns component grass">
 793               <br />
 794             </td>
 795             <td class="snns plane grass">degree assignment</td>
 796             <td class="snns file grass">da ( ⦃?,?⦄ ⊢ ? ▪[?,?] ? )</td>
 797             <td class="snnn file grass">da_lift da_aaa da_sta da_da</td>
 798             <td class="snnn file grass">
 799               <br />
 800             </td>
 801             <td class="ssnn file grass">
 802               <br />
 803             </td>
 804           </tr>
 805           <tr>
 806             <td class="nnns component grass">
 807               <br />
 808             </td>
 809             <td class="snns plane grass">static type assignment</td>
 810             <td class="snns file grass">sta ( ⦃?,?⦄ ⊢ ? •[?] ? )</td>
 811             <td class="snnn file grass">sta_lift sta_lpx_sn sta_aaa sta_sta</td>
 812             <td class="snnn file grass">
 813               <br />
 814             </td>
 815             <td class="ssnn file grass">
 816               <br />
 817             </td>
 818           </tr>
 819           <tr>
 820             <td class="nnns component grass">
 821               <br />
 822             </td>
 823             <td class="snns plane grass">parameters</td>
 824             <td class="snns file grass">sh</td>
 825             <td class="snnn file grass">sd</td>
 826             <td class="snnn file grass">
 827               <br />
 828             </td>
 829             <td class="ssnn file grass">
 830               <br />
 831             </td>
 832           </tr>
 833           <tr>
 834             <td class="nnns component grass">
 835               <br />
 836             </td>
 837             <td class="snns plane grass">local env. ref. for atomic arity assignment</td>
 838             <td class="snns file grass">lsuba ( ? ⊢ ? ⫃⁝ ? )</td>
 839             <td class="snnn file grass">lsuba_aaa lsuba_lsuba</td>
 840             <td class="snnn file grass">
 841               <br />
 842             </td>
 843             <td class="ssnn file grass">
 844               <br />
 845             </td>
 846           </tr>
 847           <tr>
 848             <td class="nnns component grass">
 849               <br />
 850             </td>
 851             <td class="snns plane grass">atomic arity assignment</td>
 852             <td class="snns file grass">aaa ( ⦃?,?⦄ ⊢ ? ⁝ ? )</td>
 853             <td class="snnn file grass">aaa_lift aaa_lifts aaa_fqus aaa_lleq aaa_aaa</td>
 854             <td class="snnn file grass">
 855               <br />
 856             </td>
 857             <td class="ssnn file grass">
 858               <br />
 859             </td>
 860           </tr>
 861           <tr>
 862             <td class="nnns component grass">
 863               <br />
 864             </td>
 865             <td class="snns plane grass">restricted local env. ref.</td>
 866             <td class="snns file grass">lsubr ( ? ⫃ ? )</td>
 867             <td class="snnn file grass">lsubr_lsubr</td>
 868             <td class="snnn file grass">
 869               <br />
 870             </td>
 871             <td class="ssnn file grass">
 872               <br />
 873             </td>
 874           </tr>
 875           <tr>
 876             <td class="snns component yellow">multiple substitution</td>
 877             <td class="snns plane yellow">lazy equivalence</td>
 878             <td class="snns file yellow">fleq ( ⦃?,?,?⦄ ≡[?] ⦃?,?,?⦄ )</td>
 879             <td class="snnn file yellow">fleq_fleq</td>
 880             <td class="snnn file yellow">
 881               <br />
 882             </td>
 883             <td class="ssnn file yellow">
 884               <br />
 885             </td>
 886           </tr>
 887           <tr>
 888             <td class="nnns component yellow">
 889               <br />
 890             </td>
 891             <td class="nnns plane yellow">
 892               <br />
 893             </td>
 894             <td class="snns file yellow">lleq ( ? ≡[?,?] ? )</td>
 895             <td class="snnn file yellow">lleq_alt lleq_alt_rec lleq_leq lleq_drop lleq_fqus lleq_llor lleq_lleq</td>
 896             <td class="snnn file yellow">
 897               <br />
 898             </td>
 899             <td class="ssnn file yellow">
 900               <br />
 901             </td>
 902           </tr>
 903           <tr>
 904             <td class="nnns component yellow">
 905               <br />
 906             </td>
 907             <td class="snns plane yellow">lazy pointwise extension of a relation</td>
 908             <td class="snns file yellow">llpx_sn</td>
 909             <td class="snnn file yellow">llpx_sn_alt llpx_sn_alt_rec llpx_sn_tc llpx_sn_leq llpx_sn_drop llpx_sn_lpx_sn llpx_sn_frees llpx_sn_llor</td>
 910             <td class="snnn file yellow">
 911               <br />
 912             </td>
 913             <td class="ssnn file yellow">
 914               <br />
 915             </td>
 916           </tr>
 917           <tr>
 918             <td class="nnns component yellow">
 919               <br />
 920             </td>
 921             <td class="snns plane yellow">pointwise union for local environments</td>
 922             <td class="snns file yellow">llor ( ? ⩖[?,?] ? ≡ ? )</td>
 923             <td class="snnn file yellow">llor_alt llor_drop</td>
 924             <td class="snnn file yellow">
 925               <br />
 926             </td>
 927             <td class="ssnn file yellow">
 928               <br />
 929             </td>
 930           </tr>
 931           <tr>
 932             <td class="nnns component yellow">
 933               <br />
 934             </td>
 935             <td class="snns plane yellow">context-sensitive exclusion from free variables</td>
 936             <td class="snns file yellow">frees ( ? ⊢ ? ϵ 𝐅*[?]⦃?⦄ )</td>
 937             <td class="snnn file yellow">frees_append frees_leq frees_lift</td>
 938             <td class="snnn file yellow">
 939               <br />
 940             </td>
 941             <td class="ssnn file yellow">
 942               <br />
 943             </td>
 944           </tr>
 945           <tr>
 946             <td class="nnns component yellow">
 947               <br />
 948             </td>
 949             <td class="snns plane yellow">contxt-sensitive extended multiple substitution</td>
 950             <td class="snns file yellow">cpys ( ⦃?,?⦄ ⊢ ? ▶*[?,?] ? )</td>
 951             <td class="snnn file yellow">cpys_alt ( ⦃?,?⦄ ⊢ ? ▶▶*[?,?] ? )</td>
 952             <td class="snnn file yellow">cpys_lift cpys_cpys</td>
 953             <td class="ssnn file yellow">
 954               <br />
 955             </td>
 956           </tr>
 957           <tr>
 958             <td class="nnns component yellow">
 959               <br />
 960             </td>
 961             <td class="snns plane yellow">iterated structural successor for closures</td>
 962             <td class="snns file yellow">fqus ( ⦃?,?,?⦄ ⊐* ⦃?,?,?⦄ )</td>
 963             <td class="snnn file yellow">fqus_alt fqus_fqus</td>
 964             <td class="snnn file yellow">
 965               <br />
 966             </td>
 967             <td class="ssnn file yellow">
 968               <br />
 969             </td>
 970           </tr>
 971           <tr>
 972             <td class="nnns component yellow">
 973               <br />
 974             </td>
 975             <td class="nnns plane yellow">
 976               <br />
 977             </td>
 978             <td class="snns file yellow">fqup ( ⦃?,?,?⦄ ⊐+ ⦃?,?,?⦄ )</td>
 979             <td class="snnn file yellow">fqup_fqup</td>
 980             <td class="snnn file yellow">
 981               <br />
 982             </td>
 983             <td class="ssnn file yellow">
 984               <br />
 985             </td>
 986           </tr>
 987           <tr>
 988             <td class="nnns component yellow">
 989               <br />
 990             </td>
 991             <td class="snns plane yellow">iterated local env. slicing</td>
 992             <td class="snns file yellow">drops ( ⇩*[?,?] ? ≡ ? )</td>
 993             <td class="snnn file yellow">drops_drop drops_drops</td>
 994             <td class="snnn file yellow">
 995               <br />
 996             </td>
 997             <td class="ssnn file yellow">
 998               <br />
 999             </td>
1000           </tr>
1001           <tr>
1002             <td class="nnns component yellow">
1003               <br />
1004             </td>
1005             <td class="snns plane yellow">generic term relocation</td>
1006             <td class="snns file yellow">lifts_vector ( ⇧*[?] ? ≡ ? )</td>
1007             <td class="snnn file yellow">lifts_lift_vector</td>
1008             <td class="snnn file yellow">
1009               <br />
1010             </td>
1011             <td class="ssnn file yellow">
1012               <br />
1013             </td>
1014           </tr>
1015           <tr>
1016             <td class="nnns component yellow">
1017               <br />
1018             </td>
1019             <td class="nnns plane yellow">
1020               <br />
1021             </td>
1022             <td class="snns file yellow">lifts ( ⇧*[?] ? ≡ ? )</td>
1023             <td class="snnn file yellow">lifts_lift lifts_lifts</td>
1024             <td class="snnn file yellow">
1025               <br />
1026             </td>
1027             <td class="ssnn file yellow">
1028               <br />
1029             </td>
1030           </tr>
1031           <tr>
1032             <td class="nnns component yellow">
1033               <br />
1034             </td>
1035             <td class="snns plane yellow">support for generic relocation</td>
1036             <td class="snns file yellow">gr2 ( @⦃?,?⦄ ≡ ? )</td>
1037             <td class="snnn file yellow">gr2_plus ( ? + ? )</td>
1038             <td class="snnn file yellow">gr2_minus ( ? ▭ ? ≡ ? )</td>
1039             <td class="ssnn file yellow">gr2_gr2</td>
1040           </tr>
1041           <tr>
1042             <td class="snns component orange">substitution</td>
1043             <td class="snns plane orange">structural successor for closures</td>
1044             <td class="snns file orange">fquq ( ⦃?,?,?⦄ ⊐⸮ ⦃?,?,?⦄ )</td>
1045             <td class="snnn file orange">fquq_alt ( ⦃?,?,?⦄ ⊐⊐⸮ ⦃?,?,?⦄ )</td>
1046             <td class="snnn file orange">
1047               <br />
1048             </td>
1049             <td class="ssnn file orange">
1050               <br />
1051             </td>
1052           </tr>
1053           <tr>
1054             <td class="nnns component orange">
1055               <br />
1056             </td>
1057             <td class="nnns plane orange">
1058               <br />
1059             </td>
1060             <td class="snns file orange">fqu ( ⦃?,?,?⦄ ⊐ ⦃?,?,?⦄ )</td>
1061             <td class="snnn file orange">
1062               <br />
1063             </td>
1064             <td class="snnn file orange">
1065               <br />
1066             </td>
1067             <td class="ssnn file orange">
1068               <br />
1069             </td>
1070           </tr>
1071           <tr>
1072             <td class="nnns component orange">
1073               <br />
1074             </td>
1075             <td class="snns plane orange">global env. slicing</td>
1076             <td class="snns file orange">gget ( ⇩[?] ? ≡ ? )</td>
1077             <td class="snnn file orange">gget_gget</td>
1078             <td class="snnn file orange">
1079               <br />
1080             </td>
1081             <td class="ssnn file orange">
1082               <br />
1083             </td>
1084           </tr>
1085           <tr>
1086             <td class="nnns component orange">
1087               <br />
1088             </td>
1089             <td class="snns plane orange">contxt-sensitive extended ordinary substitution</td>
1090             <td class="snns file orange">cpy ( ⦃?,?⦄ ⊢ ? ▶[?,?] ? )</td>
1091             <td class="snnn file orange">cpy_lift cpy_nlift cpy_cpy</td>
1092             <td class="snnn file orange">
1093               <br />
1094             </td>
1095             <td class="ssnn file orange">
1096               <br />
1097             </td>
1098           </tr>
1099           <tr>
1100             <td class="nnns component orange">
1101               <br />
1102             </td>
1103             <td class="snns plane orange">local env. ref. for extended substitution</td>
1104             <td class="snns file orange">lsuby ( ? ⊆[?,?] ? )</td>
1105             <td class="snnn file orange">lsuby_lsuby</td>
1106             <td class="snnn file orange">
1107               <br />
1108             </td>
1109             <td class="ssnn file orange">
1110               <br />
1111             </td>
1112           </tr>
1113           <tr>
1114             <td class="nnns component orange">
1115               <br />
1116             </td>
1117             <td class="snns plane orange">pointwise extension of a relation</td>
1118             <td class="snns file orange">lpx_sn</td>
1119             <td class="snnn file orange">lpx_sn_alt lpx_sn_tc lpx_sn_drop lpx_sn_lpx_sn</td>
1120             <td class="snnn file orange">
1121               <br />
1122             </td>
1123             <td class="ssnn file orange">
1124               <br />
1125             </td>
1126           </tr>
1127           <tr>
1128             <td class="nnns component orange">
1129               <br />
1130             </td>
1131             <td class="snns plane orange">basic local env. slicing</td>
1132             <td class="snns file orange">drop ( ⇩[?,?,?] ? ≡ ? )</td>
1133             <td class="snnn file orange">drop_append drop_leq drop_drop</td>
1134             <td class="snnn file orange">
1135               <br />
1136             </td>
1137             <td class="ssnn file orange">
1138               <br />
1139             </td>
1140           </tr>
1141           <tr>
1142             <td class="nnns component orange">
1143               <br />
1144             </td>
1145             <td class="snns plane orange">basic term relocation</td>
1146             <td class="snns file orange">lift_vector ( ⇧[?,?] ? ≡ ? )</td>
1147             <td class="snnn file orange">lift_lift_vector</td>
1148             <td class="snnn file orange">
1149               <br />
1150             </td>
1151             <td class="ssnn file orange">
1152               <br />
1153             </td>
1154           </tr>
1155           <tr>
1156             <td class="nnns component orange">
1157               <br />
1158             </td>
1159             <td class="nnns plane orange">
1160               <br />
1161             </td>
1162             <td class="snns file orange">lift ( ⇧[?,?] ? ≡ ? )</td>
1163             <td class="snnn file orange">lift_neq lift_lift</td>
1164             <td class="snnn file orange">
1165               <br />
1166             </td>
1167             <td class="ssnn file orange">
1168               <br />
1169             </td>
1170           </tr>
1171           <tr>
1172             <td class="snns component red">grammar</td>
1173             <td class="snns plane red">equivalence for local environments</td>
1174             <td class="snns file red">leq ( ? ⩬[?,?] ? )</td>
1175             <td class="snnn file red">leq_leq</td>
1176             <td class="snnn file red">
1177               <br />
1178             </td>
1179             <td class="ssnn file red">
1180               <br />
1181             </td>
1182           </tr>
1183           <tr>
1184             <td class="nnns component red">
1185               <br />
1186             </td>
1187             <td class="snns plane red">same top term constructor</td>
1188             <td class="snns file red">tstc ( ? ≂ ? )</td>
1189             <td class="snnn file red">tstc_tstc tstc_vector</td>
1190             <td class="snnn file red">
1191               <br />
1192             </td>
1193             <td class="ssnn file red">
1194               <br />
1195             </td>
1196           </tr>
1197           <tr>
1198             <td class="nnns component red">
1199               <br />
1200             </td>
1201             <td class="snns plane red">closures</td>
1202             <td class="snns file red">cl_weight ( ♯{?,?,?} )</td>
1203             <td class="snnn file red">cl_restricted_weight ( ♯{?,?} )</td>
1204             <td class="snnn file red">
1205               <br />
1206             </td>
1207             <td class="ssnn file red">
1208               <br />
1209             </td>
1210           </tr>
1211           <tr>
1212             <td class="nnns component red">
1213               <br />
1214             </td>
1215             <td class="snns plane red">internal syntax</td>
1216             <td class="snns file red">genv</td>
1217             <td class="snnn file red">
1218               <br />
1219             </td>
1220             <td class="snnn file red">
1221               <br />
1222             </td>
1223             <td class="ssnn file red">
1224               <br />
1225             </td>
1226           </tr>
1227           <tr>
1228             <td class="nnns component red">
1229               <br />
1230             </td>
1231             <td class="nnns plane red">
1232               <br />
1233             </td>
1234             <td class="snns file red">lenv</td>
1235             <td class="snnn file red">lenv_weight ( ♯{?} )</td>
1236             <td class="snnn file red">lenv_length ( |?| )</td>
1237             <td class="ssnn file red">lenv_append ( ? @@ ? )</td>
1238           </tr>
1239           <tr>
1240             <td class="nnns component red">
1241               <br />
1242             </td>
1243             <td class="nnns plane red">
1244               <br />
1245             </td>
1246             <td class="snns file red">term</td>
1247             <td class="snnn file red">term_weight ( ♯{?} )</td>
1248             <td class="snnn file red">term_simple ( 𝐒⦃?⦄ )</td>
1249             <td class="ssnn file red">term_vector ( Ⓐ?.? )</td>
1250           </tr>
1251           <tr>
1252             <td class="nnns component red">
1253               <br />
1254             </td>
1255             <td class="nnns plane red">
1256               <br />
1257             </td>
1258             <td class="snns file red">item</td>
1259             <td class="snnn file red">
1260               <br />
1261             </td>
1262             <td class="snnn file red">
1263               <br />
1264             </td>
1265             <td class="ssnn file red">
1266               <br />
1267             </td>
1268           </tr>
1269           <tr>
1270             <td class="nnss component red">
1271               <br />
1272             </td>
1273             <td class="snss plane red">external syntax</td>
1274             <td class="snss file red">aarity</td>
1275             <td class="snsn file red">
1276               <br />
1277             </td>
1278             <td class="snsn file red">
1279               <br />
1280             </td>
1281             <td class="sssn file red">
1282               <br />
1283             </td>
1284           </tr>
1285         </tbody>
1286       </table>
1287     </div>
1288
1289    <div xmlns:ld="http://lambdadelta.info/" class="head2sn" id="">Physical Structure of the Specification</div>
1290    <div xmlns:ld="http://lambdadelta.info/" class="text">The source files are grouped in directories,
1291          one for each component.
1292    </div>
1293    <div class="spacer">
1294       <img class="rule" alt="[Spacer]" title="lambdadelta rainbow rule" src="http://lambdadelta.info/images/rainbow.png" />
1295     </div>
1296     <div xmlns:ld="http://lambdadelta.info/" class="spacer">
1297       <br />
1298     </div>
1299     <div xmlns:ld="http://lambdadelta.info/" class="spacer">
1300       <a href="http://validator.w3.org/check?uri=referer">
1301         <img class="w3c" alt="[Valid XHTML 1.1]" title="Valid XHTML 1.1" src="http://www.w3.org/Icons/valid-xhtml11-blue" />
1302       </a>
1303       <a href="http://jigsaw.w3.org/css-validator/check/referer">
1304         <img class="w3c" alt="[Valid CSS level 2]" title="Valid CSS level 2" src="http://www.w3.org/Icons/valid-css2-blue" />
1305       </a>
1306       <a href="http://www.w3.org/XML/">
1307         <img class="w3c" alt="[Generated from XML via XSL]" title="Generated from XML via XSL" src="http://lambdadelta.info/images/xml_xsl2.png" />
1308       </a>
1309       <a href="http://www.w3.org/Graphics/PNG/">
1310         <img class="w3c" alt="[PNG used here]" title="PNG used here" src="http://lambdadelta.info/images/PNGnow2.png" />
1311       </a>
1312       <a href="http://www.anybrowser.org/campaign/">
1313         <img class="w3c" alt="[Viewable with any browser]" title="Viewable with any browser" src="http://www.anybrowser.org/campaign/bvgraphics/abtfile.png" />
1314       </a>
1315     </div>
1316     <div xmlns:ld="http://lambdadelta.info/" class="spacer">
1317       <br />
1318     </div>
1319     <div xmlns:ld="http://lambdadelta.info/" class="spacer">Last update: Wed, 06 Aug 2014 20:50:29 +0200</div>
1320 </body>
1321 </html>