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