helm/www/lambdadelta/basic_1.html

   1 <?xml version="1.0" encoding="UTF-8"?>
   2 <!DOCTYPE html PUBLIC "-//W3C//DTD XHTML 1.1//EN" "http://www.w3.org/TR/xhtml11/DTD/xhtml11.dtd">
   3 <html xmlns="http://www.w3.org/1999/xhtml" dir="ltr" lang="en-us">
   4   <head>
   5     <meta http-equiv="Content-Language" content="en-us" />
   6     <meta http-equiv="Content-Type" content="text/html; charset=UTF-8" />
   7     <meta http-equiv="Content-Style-Type" content="text/css" />
   8     <meta name="author" content="Ferruccio Guidi" />
   9     <meta name="description" content="\lambda\delta home page" />
  10     <title>\lambda\delta home page</title>
  11     <link rel="stylesheet" type="text/css" href="http://lambdadelta.info/css/ld_web.css" />
  12     <link rel="stylesheet" type="text/css" href="http://lambdadelta.info/css/lddl.css" />
  13     <link rel="stylesheet" type="text/css" href="http://lambdadelta.info/css/xhtbl.css" />
  14     <link rel="shortcut icon" href="http://lambdadelta.info/images/crux_16.ico" />
  15   </head>
  16   <body lang="en-US">
  17     <div class="spacer">
  18       <a href="http://lambdadelta.info/">
  19         <img class="icon32" alt="[lambdadelta home]" title="lambdadelta home" src="http://lambdadelta.info/images/crux_32.png" />
  20       </a>
  21     </div>
  22     <div class="head1">cic:/BOLOGNA/lambdadelta/basic_1/ (core λδ version 1)</div>
  23     <div class="spacer">
  24       <img class="rule" alt="[Spacer]" title="lambdadelta rainbow rule" src="http://lambdadelta.info/images/rainbow.png" />
  25     </div>
  26     <div xmlns:ld="http://lambdadelta.info/" class="spacer">
  27       <br />
  28     </div>
  29     <div xmlns:ld="http://lambdadelta.info/" class="text">
  30       <table cellpadding="4" cellspacing="0">
  31         <tbody>
  32           <tr>
  33             <td class="snns capitalize italic sky">
  34               <a href="http://lambdadelta.info/index.html">home</a>
  35             </td>
  36             <td class="snns capitalize italic magenta">
  37               <a href="http://lambdadelta.info/news.html">news</a>
  38             </td>
  39             <td class="snns capitalize italic orange">
  40               <a href="http://lambdadelta.info/documentation.html">documentation</a>
  41             </td>
  42             <td class="snns capitalize italic green">
  43               <a href="http://lambdadelta.info/specification.html">specification</a>
  44             </td>
  45             <td class="snnn capitalize italic green">
  46               <br />
  47             </td>
  48             <td class="snnn capitalize italic green">
  49               <br />
  50             </td>
  51             <td class="snns capitalize italic green">
  52               <a href="http://lambdadelta.info/implementation.html">implementation</a>
  53             </td>
  54             <td class="ssnn capitalize italic green">
  55               <br />
  56             </td>
  57           </tr>
  58           <tr>
  59             <td class="snns capitalize sky">
  60               <a href="http://lambdadelta.info/index.html#foreword">foreword</a>
  61             </td>
  62             <td class="snns capitalize magenta">
  63               <a href="http://lambdadelta.info/news.html#milestones">milestones</a>
  64             </td>
  65             <td class="snns capitalize orange">
  66               <a href="http://lambdadelta.info/documentation.html#v2">version 2</a>
  67             </td>
  68             <td class="snns capitalize green">
  69               <a href="http://lambdadelta.info/specification.html#v2">version 2</a>
  70             </td>
  71             <td class="snnn capitalize green">(<a href="http://lambdadelta.info/ground_2.html">background</a> - <a href="http://lambdadelta.info/basic_2.html">core</a> - <a href="http://lambdadelta.info/apps_2.html">applications</a>)</td>
  72             <td class="snnn capitalize green">
  73               <br />
  74             </td>
  75             <td class="snns capitalize green">
  76               <a href="http://lambdadelta.info/implementation.html#lddl">library</a>
  77             </td>
  78             <td class="ssnn capitalize green">(<a href="http://lambdadelta.info/static/lddl/">static LDDL directory</a>)</td>
  79           </tr>
  80           <tr>
  81             <td class="snss capitalize sky">
  82               <a href="http://lambdadelta.info/index.html#citations">citations</a>
  83             </td>
  84             <td class="snss capitalize magenta">
  85               <a href="http://lambdadelta.info/news.html#visibility">visibility</a>
  86             </td>
  87             <td class="snss capitalize orange">
  88               <a href="http://lambdadelta.info/documentation.html#v1">version 1</a>
  89             </td>
  90             <td class="snss capitalize green">
  91               <a href="http://lambdadelta.info/specification.html#v1">version 1</a>
  92             </td>
  93             <td class="snsn capitalize green">(<a href="http://lambdadelta.info/basic_1.html">core</a>)</td>
  94             <td class="snsn capitalize green">(<a href="http://lambdadelta.info/static/matita/lambdadelta/">static HELM directory</a>)</td>
  95             <td class="snss capitalize green">
  96               <a href="http://lambdadelta.info/implementation.html#helena">helena</a>
  97             </td>
  98             <td class="sssn capitalize green">
  99               <br />
 100             </td>
 101           </tr>
 102         </tbody>
 103       </table>
 104     </div>
 105     <!--
 106    <section>System's Syntax and Behavior</section>
 107    <body>This is a summary of the "block structure"
 108          of the System's syntactic items and reductions.
 109    </body>
 110    <table name="basic_1_blk"/>
 111    <body>* In terms only.
 112          ** In terms and local environments only.
 113          *** In global environments only.
 114          **** Sort level k in terms only.
 115    </body>
 116 -->
 117     <div xmlns:ld="http://lambdadelta.info/" class="head2dx" id="summary">Summary of the Specification <img class="icon37" alt="[spacer]" title="lambdadelta butterfly" src="http://lambdadelta.info/images/b6.png" />
 118     </div>
 119     <div xmlns:ld="http://lambdadelta.info/" class="text">Here is a numerical account of the specification's contents
 120          and its timeline.
 121    </div>
 122     <div xmlns:ld="http://lambdadelta.info/" class="text">
 123       <table cellpadding="4" cellspacing="0">
 124         <tbody>
 125           <tr>
 126             <td class="snns capitalize italic gray">category</td>
 127             <td class="snns italic gray">objects</td>
 128             <td class="snnn right italic gray">
 129               <br />
 130             </td>
 131             <td class="snnn italic gray">
 132               <br />
 133             </td>
 134             <td class="snnn right italic gray">
 135               <br />
 136             </td>
 137             <td class="snnn italic gray">
 138               <br />
 139             </td>
 140             <td class="ssnn right italic gray">
 141               <br />
 142             </td>
 143           </tr>
 144           <tr>
 145             <td class="snns capitalize italic cyan">sizes</td>
 146             <td class="snns italic cyan">files</td>
 147             <td class="snnn right italic cyan">120</td>
 148             <td class="snns italic cyan">characters</td>
 149             <td class="snnn right italic cyan">198123</td>
 150             <td class="snns italic cyan">nodes</td>
 151             <td class="ssnn right italic cyan" />
 152           </tr>
 153           <tr>
 154             <td class="snns capitalize italic green">propositions</td>
 155             <td class="snns italic green">theorems</td>
 156             <td class="snnn right italic green">699</td>
 157             <td class="snns italic green">lemmas</td>
 158             <td class="snnn right italic green">29</td>
 159             <td class="snns italic green">total</td>
 160             <td class="ssnn right italic green">728</td>
 161           </tr>
 162           <tr>
 163             <td class="snss capitalize italic yellow">concepts</td>
 164             <td class="snss italic yellow">declared</td>
 165             <td class="snsn right italic yellow">39</td>
 166             <td class="snss italic yellow">defined</td>
 167             <td class="snsn right italic yellow">47</td>
 168             <td class="snss italic yellow">total</td>
 169             <td class="sssn right italic yellow">86</td>
 170           </tr>
 171         </tbody>
 172       </table>
 173     </div>
 174     <ul xmlns:ld="http://lambdadelta.info/">
 175       <li>
 176         <span class="emph delta">January 2015.</span>
 177       Update with backports from the abandoned specification of λδ version 2.
 178    </li>
 179     </ul>
 180     <ul xmlns:ld="http://lambdadelta.info/">
 181       <li>
 182         <span class="emph delta">May 2008.</span>
 183       Specification is concluded.
 184    </li>
 185     </ul>
 186     <ul xmlns:ld="http://lambdadelta.info/">
 187       <li>
 188         <span class="emph gamma">November 2006.</span>
 189       Decidability of native type assignment, λδ version 1 is released.
 190    </li>
 191     </ul>
 192     <ul xmlns:ld="http://lambdadelta.info/">
 193       <li>
 194         <span class="emph beta">December 2005.</span>
 195       Preservation of native type by reduction, λδ version 1 is announced.
 196    </li>
 197     </ul>
 198     <ul xmlns:ld="http://lambdadelta.info/">
 199       <li>
 200         <span class="emph alpha">May 2004.</span>
 201       Specification starts.
 202    </li>
 203     </ul>
 204     <div xmlns:ld="http://lambdadelta.info/" class="head2dx" id="structure">Logical Structure of the Specification <img class="icon37" alt="[spacer]" title="lambdadelta butterfly" src="http://lambdadelta.info/images/b6.png" />
 205     </div>
 206     <div xmlns:ld="http://lambdadelta.info/" class="text">This table reports the specification's components and their planes.
 207    </div>
 208     <div xmlns:ld="http://lambdadelta.info/" class="text">
 209       <table cellpadding="4" cellspacing="0">
 210         <tbody>
 211           <tr>
 212             <td class="snns top capitalize italic gray">component</td>
 213             <td class="snns top italic gray">plane</td>
 214             <td class="snns top gray">files</td>
 215             <td class="ssnn top gray">
 216               <br />
 217             </td>
 218           </tr>
 219           <tr>
 220             <td class="snns top capitalize italic wine">examples</td>
 221             <td class="snns top italic wine">terms with special features</td>
 222             <td class="snns top wine">
 223               <a href="http://lambdadelta.info/static/coq/lambdadelta/basic_1/levels_ex0.txt">levels_ex0</a>
 224               <a href="http://lambdadelta.info/static/coq/lambdadelta/basic_1/ty3_ex1.txt">ty3_ex1</a>
 225               <a href="http://lambdadelta.info/static/coq/lambdadelta/basic_1/nf2_ex2.txt">nf2_ex2</a>
 226             </td>
 227             <td class="ssnn top wine">
 228               <br />
 229             </td>
 230           </tr>
 231           <tr>
 232             <td class="snns top capitalize italic magenta" />
 233             <td class="snns top italic magenta" />
 234             <td class="snns top magenta" />
 235             <td class="ssnn top magenta">
 236               <br />
 237             </td>
 238           </tr>
 239           <tr>
 240             <td class="snns top capitalize italic prune">dynamic typing</td>
 241             <td class="snns top italic prune">well-formed contexts</td>
 242             <td class="snns top prune">
 243               <a href="http://lambdadelta.info/static/coq/lambdadelta/basic_1/wf3_defs.txt">wf3_defs</a>
 244             </td>
 245             <td class="ssnn top prune">
 246               <a href="http://lambdadelta.info/static/coq/lambdadelta/basic_1/wf3_props.txt">wf3_props</a>
 247             </td>
 248           </tr>
 249           <tr>
 250             <td class="nnns top capitalize italic prune">
 251               <br />
 252             </td>
 253             <td class="snns top italic prune">context ref. for native type assignment</td>
 254             <td class="snns top prune">
 255               <a href="http://lambdadelta.info/static/coq/lambdadelta/basic_1/csubt_defs.txt">csubt_defs</a>
 256             </td>
 257             <td class="ssnn top prune">
 258               <a href="http://lambdadelta.info/static/coq/lambdadelta/basic_1/csubt_props.txt">csubt_props</a>
 259               <a href="http://lambdadelta.info/static/coq/lambdadelta/basic_1/csubt_arity_props.txt">csubt_arity_props</a>
 260             </td>
 261           </tr>
 262           <tr>
 263             <td class="nnns top capitalize italic prune">
 264               <br />
 265             </td>
 266             <td class="snns top italic prune">native type assignment</td>
 267             <td class="snns top prune">
 268               <a href="http://lambdadelta.info/static/coq/lambdadelta/basic_1/ty3_defs.txt">ty3_defs</a>
 269             </td>
 270             <td class="ssnn top prune">
 271               <a href="http://lambdadelta.info/static/coq/lambdadelta/basic_1/ty3_props.txt">ty3_props</a>
 272               <a href="http://lambdadelta.info/static/coq/lambdadelta/basic_1/ty3_gen.txt">ty3_gen</a>
 273               <a href="http://lambdadelta.info/static/coq/lambdadelta/basic_1/ty3_gen_context.txt">ty3_gen_context</a>
 274               <a href="http://lambdadelta.info/static/coq/lambdadelta/basic_1/ty3_gen_nf2.txt">ty3_gen_nf2</a>
 275               <a href="http://lambdadelta.info/static/coq/lambdadelta/basic_1/ty3_lift.txt">ty3_lift</a>
 276               <a href="http://lambdadelta.info/static/coq/lambdadelta/basic_1/ty3_subst0.txt">ty3_subst0</a>
 277               <a href="http://lambdadelta.info/static/coq/lambdadelta/basic_1/ty3_arity_props.txt">ty3_arity_props</a>
 278               <a href="http://lambdadelta.info/static/coq/lambdadelta/basic_1/ty3_nf2_gen.txt">ty3_nf2_gen</a>
 279               <a href="http://lambdadelta.info/static/coq/lambdadelta/basic_1/ty3_sred.txt">ty3_sred</a>
 280               <a href="http://lambdadelta.info/static/coq/lambdadelta/basic_1/ty3_sred_props.txt">ty3_sred_props</a>
 281               <a href="http://lambdadelta.info/static/coq/lambdadelta/basic_1/ty3_dec.txt">ty3_dec</a>
 282             </td>
 283           </tr>
 284           <tr>
 285             <td class="snns top capitalize italic blue">equivalence</td>
 286             <td class="snns top italic blue">context-sensitive equivalence</td>
 287             <td class="snns top blue">
 288               <a href="http://lambdadelta.info/static/coq/lambdadelta/basic_1/pc3_defs.txt">pc3_defs</a>
 289             </td>
 290             <td class="ssnn top blue">
 291               <a href="http://lambdadelta.info/static/coq/lambdadelta/basic_1/pc3_props.txt">pc3_props</a>
 292               <a href="http://lambdadelta.info/static/coq/lambdadelta/basic_1/pc3_gen.txt">pc3_gen</a>
 293               <a href="http://lambdadelta.info/static/coq/lambdadelta/basic_1/pc3_gen_context.txt">pc3_gen_context</a>
 294               <a href="http://lambdadelta.info/static/coq/lambdadelta/basic_1/pc3_subst0.txt">pc3_subst0</a>
 295             </td>
 296           </tr>
 297           <tr>
 298             <td class="nnns top capitalize italic blue">
 299               <br />
 300             </td>
 301             <td class="snns top italic blue">context-free equivalence</td>
 302             <td class="snns top blue">
 303               <a href="http://lambdadelta.info/static/coq/lambdadelta/basic_1/pc1_defs.txt">pc1_defs</a>
 304             </td>
 305             <td class="ssnn top blue">
 306               <a href="http://lambdadelta.info/static/coq/lambdadelta/basic_1/pc1_props.txt">pc1_props</a>
 307             </td>
 308           </tr>
 309           <tr>
 310             <td class="snns top capitalize italic sky" />
 311             <td class="snns top italic sky" />
 312             <td class="snns top sky" />
 313             <td class="ssnn top sky">
 314               <br />
 315             </td>
 316           </tr>
 317           <tr>
 318             <td class="snns top capitalize italic cyan">computation</td>
 319             <td class="snns top italic cyan">context ref. for reducibility</td>
 320             <td class="snns top cyan">
 321               <a href="http://lambdadelta.info/static/coq/lambdadelta/basic_1/csubc_defs.txt">csubc_defs</a>
 322             </td>
 323             <td class="ssnn top cyan">
 324               <a href="http://lambdadelta.info/static/coq/lambdadelta/basic_1/csubc_props.txt">csubc_props</a>
 325             </td>
 326           </tr>
 327           <tr>
 328             <td class="nnns top capitalize italic cyan">
 329               <br />
 330             </td>
 331             <td class="snns top italic cyan">reducibility</td>
 332             <td class="snns top cyan">
 333               <a href="http://lambdadelta.info/static/coq/lambdadelta/basic_1/sc3_defs.txt">sc3_defs</a>
 334             </td>
 335             <td class="ssnn top cyan">
 336               <a href="http://lambdadelta.info/static/coq/lambdadelta/basic_1/sc3_props.txt">sc3_props</a>
 337               <a href="http://lambdadelta.info/static/coq/lambdadelta/basic_1/sc3_arity.txt">sc3_arity</a>
 338             </td>
 339           </tr>
 340           <tr>
 341             <td class="nnns top capitalize italic cyan">
 342               <br />
 343             </td>
 344             <td class="snns top italic cyan">strongly normalizing computation</td>
 345             <td class="snns top cyan">
 346               <a href="http://lambdadelta.info/static/coq/lambdadelta/basic_1/sn3_defs.txt">sn3_defs</a>
 347             </td>
 348             <td class="ssnn top cyan">
 349               <a href="http://lambdadelta.info/static/coq/lambdadelta/basic_1/sn3_gen.txt">sn3_gen</a>
 350               <a href="http://lambdadelta.info/static/coq/lambdadelta/basic_1/sn3_props.txt">sn3_props</a>
 351             </td>
 352           </tr>
 353           <tr>
 354             <td class="nnns top capitalize italic cyan">
 355               <br />
 356             </td>
 357             <td class="snns top italic cyan">context-sensitive computation</td>
 358             <td class="snns top cyan">
 359               <a href="http://lambdadelta.info/static/coq/lambdadelta/basic_1/pr3_defs.txt">pr3_defs</a>
 360             </td>
 361             <td class="ssnn top cyan">
 362               <a href="http://lambdadelta.info/static/coq/lambdadelta/basic_1/pr3_props.txt">pr3_props</a>
 363               <a href="http://lambdadelta.info/static/coq/lambdadelta/basic_1/pr3_gen.txt">pr3_gen</a>
 364               <a href="http://lambdadelta.info/static/coq/lambdadelta/basic_1/pr3_gen_context.txt">pr3_gen_context</a>
 365               <a href="http://lambdadelta.info/static/coq/lambdadelta/basic_1/pr3_iso.txt">pr3_iso</a>
 366               <a href="http://lambdadelta.info/static/coq/lambdadelta/basic_1/pr3_subst1.txt">pr3_subst1</a>
 367               <a href="http://lambdadelta.info/static/coq/lambdadelta/basic_1/pr3_confluence.txt">pr3_confluence</a>
 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">context-free computation</td>
 375             <td class="snns top cyan">
 376               <a href="http://lambdadelta.info/static/coq/lambdadelta/basic_1/pr1_defs.txt">pr1_defs</a>
 377             </td>
 378             <td class="ssnn top cyan">
 379               <a href="http://lambdadelta.info/static/coq/lambdadelta/basic_1/pr1_props.txt">pr1_props</a>
 380               <a href="http://lambdadelta.info/static/coq/lambdadelta/basic_1/pr1_confluence.txt">pr1_confluence</a>
 381             </td>
 382           </tr>
 383           <tr>
 384             <td class="snns top capitalize italic water">reduction</td>
 385             <td class="snns top italic water">normal forms for context-sensitive reduction</td>
 386             <td class="snns top water">
 387               <a href="http://lambdadelta.info/static/coq/lambdadelta/basic_1/nf2_defs.txt">nf2_defs</a>
 388             </td>
 389             <td class="ssnn top water">
 390               <a href="http://lambdadelta.info/static/coq/lambdadelta/basic_1/nf2_props.txt">nf2_props</a>
 391               <a href="http://lambdadelta.info/static/coq/lambdadelta/basic_1/nf2_gen.txt">nf2_gen</a>
 392               <a href="http://lambdadelta.info/static/coq/lambdadelta/basic_1/nf2_dec.txt">nf2_dec</a>
 393             </td>
 394           </tr>
 395           <tr>
 396             <td class="nnns top capitalize italic water">
 397               <br />
 398             </td>
 399             <td class="snns top italic water">context-sensitive reduction</td>
 400             <td class="snns top water">
 401               <a href="http://lambdadelta.info/static/coq/lambdadelta/basic_1/pr2_defs.txt">pr2_defs</a>
 402             </td>
 403             <td class="ssnn top water">
 404               <a href="http://lambdadelta.info/static/coq/lambdadelta/basic_1/pr2_gen.txt">pr2_gen</a>
 405               <a href="http://lambdadelta.info/static/coq/lambdadelta/basic_1/pr2_gen_context.txt">pr2_gen_context</a>
 406               <a href="http://lambdadelta.info/static/coq/lambdadelta/basic_1/pr2_lift.txt">pr2_lift</a>
 407               <a href="http://lambdadelta.info/static/coq/lambdadelta/basic_1/pr2_subst1.txt">pr2_subst1</a>
 408               <a href="http://lambdadelta.info/static/coq/lambdadelta/basic_1/pr2_confluence.txt">pr2_confluence</a>
 409             </td>
 410           </tr>
 411           <tr>
 412             <td class="nnns top capitalize italic water">
 413               <br />
 414             </td>
 415             <td class="snns top italic water">normal forms for context-free reduction</td>
 416             <td class="snns top water" />
 417             <td class="ssnn top water">
 418               <a href="http://lambdadelta.info/static/coq/lambdadelta/basic_1/nf0_dec.txt">nf0_dec</a>
 419             </td>
 420           </tr>
 421           <tr>
 422             <td class="nnns top capitalize italic water">
 423               <br />
 424             </td>
 425             <td class="snns top italic water">context-free reduction</td>
 426             <td class="snns top water">
 427               <a href="http://lambdadelta.info/static/coq/lambdadelta/basic_1/wcpr0_defs.txt">wcpr0_defs</a>
 428             </td>
 429             <td class="ssnn top water">
 430               <br />
 431             </td>
 432           </tr>
 433           <tr>
 434             <td class="nnns top capitalize italic water">
 435               <br />
 436             </td>
 437             <td class="nnns top italic water">
 438               <br />
 439             </td>
 440             <td class="snns top water">
 441               <a href="http://lambdadelta.info/static/coq/lambdadelta/basic_1/pr0_defs.txt">pr0_defs</a>
 442             </td>
 443             <td class="ssnn top water">
 444               <a href="http://lambdadelta.info/static/coq/lambdadelta/basic_1/pr0_gen.txt">pr0_gen</a>
 445               <a href="http://lambdadelta.info/static/coq/lambdadelta/basic_1/pr0_lift.txt">pr0_lift</a>
 446               <a href="http://lambdadelta.info/static/coq/lambdadelta/basic_1/pr0_subst0.txt">pr0_subst0</a>
 447               <a href="http://lambdadelta.info/static/coq/lambdadelta/basic_1/pr0_subst1.txt">pr0_subst1</a>
 448               <a href="http://lambdadelta.info/static/coq/lambdadelta/basic_1/pr0_confluence.txt">pr0_confluence</a>
 449             </td>
 450           </tr>
 451           <tr>
 452             <td class="snns top capitalize italic green">unfold</td>
 453             <td class="snns top italic green">iterated static type assignment</td>
 454             <td class="snns top green">
 455               <a href="http://lambdadelta.info/static/coq/lambdadelta/basic_1/sty1_defs.txt">sty1_defs</a>
 456             </td>
 457             <td class="ssnn top green">
 458               <a href="http://lambdadelta.info/static/coq/lambdadelta/basic_1/sty1_props.txt">sty1_props</a>
 459             </td>
 460           </tr>
 461           <tr>
 462             <td class="snns top capitalize italic grass">static typing</td>
 463             <td class="snns top italic grass">static type assignment</td>
 464             <td class="snns top grass">
 465               <a href="http://lambdadelta.info/static/coq/lambdadelta/basic_1/sty0_defs.txt">sty0_defs</a>
 466             </td>
 467             <td class="ssnn top grass">
 468               <a href="http://lambdadelta.info/static/coq/lambdadelta/basic_1/sty0_props.txt">sty0_props</a>
 469             </td>
 470           </tr>
 471           <tr>
 472             <td class="nnns top capitalize italic grass">
 473               <br />
 474             </td>
 475             <td class="snns top italic grass">context ref. for binary arity assignment</td>
 476             <td class="snns top grass">
 477               <a href="http://lambdadelta.info/static/coq/lambdadelta/basic_1/csuba_defs.txt">csuba_defs</a>
 478             </td>
 479             <td class="ssnn top grass">
 480               <a href="http://lambdadelta.info/static/coq/lambdadelta/basic_1/csuba_props.txt">csuba_props</a>
 481             </td>
 482           </tr>
 483           <tr>
 484             <td class="nnns top capitalize italic grass">
 485               <br />
 486             </td>
 487             <td class="snns top italic grass">binary arity assignment</td>
 488             <td class="snns top grass">
 489               <a href="http://lambdadelta.info/static/coq/lambdadelta/basic_1/arity_defs.txt">arity_defs</a>
 490             </td>
 491             <td class="ssnn top grass">
 492               <a href="http://lambdadelta.info/static/coq/lambdadelta/basic_1/arity_props.txt">arity_props</a>
 493               <a href="http://lambdadelta.info/static/coq/lambdadelta/basic_1/arity_gen.txt">arity_gen</a>
 494               <a href="http://lambdadelta.info/static/coq/lambdadelta/basic_1/arity_subst0.txt">arity_subst0</a>
 495               <a href="http://lambdadelta.info/static/coq/lambdadelta/basic_1/arity_sred.txt">arity_sred</a>
 496             </td>
 497           </tr>
 498           <tr>
 499             <td class="nnns top capitalize italic grass">
 500               <br />
 501             </td>
 502             <td class="snns top italic grass">binary arity</td>
 503             <td class="snns top grass">
 504               <a href="http://lambdadelta.info/static/coq/lambdadelta/basic_1/levels_defs.txt">levels_defs</a>
 505               <a href="http://lambdadelta.info/static/coq/lambdadelta/basic_1/llt_defs.txt">llt_defs</a>
 506               <a href="http://lambdadelta.info/static/coq/lambdadelta/basic_1/aprem_defs.txt">aprem_defs</a>
 507             </td>
 508             <td class="ssnn top grass">
 509               <br />
 510             </td>
 511           </tr>
 512           <tr>
 513             <td class="nnns top capitalize italic grass">
 514               <br />
 515             </td>
 516             <td class="snns top italic grass">parameters</td>
 517             <td class="snns top grass">
 518               <a href="http://lambdadelta.info/static/coq/lambdadelta/basic_1/parameter_defs.txt">parameter_defs</a>
 519             </td>
 520             <td class="ssnn top grass">
 521               <br />
 522             </td>
 523           </tr>
 524           <tr>
 525             <td class="nnns top capitalize italic grass">
 526               <br />
 527             </td>
 528             <td class="snns top italic grass">basic context ref.</td>
 529             <td class="snns top grass">
 530               <a href="http://lambdadelta.info/static/coq/lambdadelta/basic_1/csubv_defs.txt">csubv_defs</a>
 531             </td>
 532             <td class="ssnn top grass">
 533               <br />
 534             </td>
 535           </tr>
 536           <tr>
 537             <td class="snns top capitalize italic yellow">multiple substitution</td>
 538             <td class="snns top italic yellow">iterated context slicing</td>
 539             <td class="snns top yellow">
 540               <a href="http://lambdadelta.info/static/coq/lambdadelta/basic_1/drop1_defs.txt">drop1_defs</a>
 541             </td>
 542             <td class="ssnn top yellow">
 543               <a href="http://lambdadelta.info/static/coq/lambdadelta/basic_1/drop1_props.txt">drop1_props</a>
 544             </td>
 545           </tr>
 546           <tr>
 547             <td class="nnns top capitalize italic yellow">
 548               <br />
 549             </td>
 550             <td class="snns top italic yellow">generic term relocation</td>
 551             <td class="snns top yellow">
 552               <a href="http://lambdadelta.info/static/coq/lambdadelta/basic_1/lift1_defs.txt">lift1_defs</a>
 553             </td>
 554             <td class="ssnn top yellow">
 555               <a href="http://lambdadelta.info/static/coq/lambdadelta/basic_1/lift1_props.txt">lift1_props</a>
 556             </td>
 557           </tr>
 558           <tr>
 559             <td class="snns top capitalize italic orange">substitution</td>
 560             <td class="snns top italic orange">ordinary substitution</td>
 561             <td class="snns top orange">
 562               <a href="http://lambdadelta.info/static/coq/lambdadelta/basic_1/subst_defs.txt">subst_defs</a>
 563             </td>
 564             <td class="ssnn top orange">
 565               <a href="http://lambdadelta.info/static/coq/lambdadelta/basic_1/subst_props.txt">subst_props</a>
 566             </td>
 567           </tr>
 568           <tr>
 569             <td class="nnns top capitalize italic orange">
 570               <br />
 571             </td>
 572             <td class="nnns top italic orange">
 573               <br />
 574             </td>
 575             <td class="snns top orange">
 576               <a href="http://lambdadelta.info/static/coq/lambdadelta/basic_1/csubst1_defs.txt">csubst1_defs</a>
 577             </td>
 578             <td class="ssnn top orange">
 579               <a href="http://lambdadelta.info/static/coq/lambdadelta/basic_1/csubst1_props.txt">csubst1_props</a>
 580             </td>
 581           </tr>
 582           <tr>
 583             <td class="nnns top capitalize italic orange">
 584               <br />
 585             </td>
 586             <td class="nnns top italic orange">
 587               <br />
 588             </td>
 589             <td class="snns top orange">
 590               <a href="http://lambdadelta.info/static/coq/lambdadelta/basic_1/subst1_defs.txt">subst1_defs</a>
 591             </td>
 592             <td class="ssnn top orange">
 593               <a href="http://lambdadelta.info/static/coq/lambdadelta/basic_1/subst1_gen.txt">subst1_gen</a>
 594               <a href="http://lambdadelta.info/static/coq/lambdadelta/basic_1/subst1_lift.txt">subst1_lift</a>
 595               <a href="http://lambdadelta.info/static/coq/lambdadelta/basic_1/subst1_subst1.txt">subst1_subst1</a>
 596               <a href="http://lambdadelta.info/static/coq/lambdadelta/basic_1/subst1_confluence.txt">subst1_confluence</a>
 597             </td>
 598           </tr>
 599           <tr>
 600             <td class="nnns top capitalize italic orange">
 601               <br />
 602             </td>
 603             <td class="snns top italic orange">normal forms for ordinary strict substitution</td>
 604             <td class="snns top orange" />
 605             <td class="ssnn top orange">
 606               <a href="http://lambdadelta.info/static/coq/lambdadelta/basic_1/dnf_dec.txt">dnf_dec</a>
 607             </td>
 608           </tr>
 609           <tr>
 610             <td class="nnns top capitalize italic orange">
 611               <br />
 612             </td>
 613             <td class="snns top italic orange">ordinary strict substitution</td>
 614             <td class="snns top orange">
 615               <a href="http://lambdadelta.info/static/coq/lambdadelta/basic_1/fsubst0_defs.txt">fsubst0_defs</a>
 616             </td>
 617             <td class="ssnn top orange">
 618               <br />
 619             </td>
 620           </tr>
 621           <tr>
 622             <td class="nnns top capitalize italic orange">
 623               <br />
 624             </td>
 625             <td class="nnns top italic orange">
 626               <br />
 627             </td>
 628             <td class="snns top orange">
 629               <a href="http://lambdadelta.info/static/coq/lambdadelta/basic_1/csubst0_defs.txt">csubst0_defs</a>
 630             </td>
 631             <td class="ssnn top orange">
 632               <br />
 633             </td>
 634           </tr>
 635           <tr>
 636             <td class="nnns top capitalize italic orange">
 637               <br />
 638             </td>
 639             <td class="nnns top italic orange">
 640               <br />
 641             </td>
 642             <td class="snns top orange">
 643               <a href="http://lambdadelta.info/static/coq/lambdadelta/basic_1/subst0_defs.txt">subst0_defs</a>
 644             </td>
 645             <td class="ssnn top orange">
 646               <a href="http://lambdadelta.info/static/coq/lambdadelta/basic_1/subst0_gen.txt">subst0_gen</a>
 647               <a href="http://lambdadelta.info/static/coq/lambdadelta/basic_1/subst0_tlt.txt">subst0_tlt</a>
 648               <a href="http://lambdadelta.info/static/coq/lambdadelta/basic_1/subst0_lift.txt">subst0_lift</a>
 649               <a href="http://lambdadelta.info/static/coq/lambdadelta/basic_1/subst0_subst0.txt">subst0_subst0</a>
 650               <a href="http://lambdadelta.info/static/coq/lambdadelta/basic_1/subst0_confluence.txt">subst0_confluence</a>
 651             </td>
 652           </tr>
 653           <tr>
 654             <td class="nnns top capitalize italic orange">
 655               <br />
 656             </td>
 657             <td class="snns top italic orange">basic local env. slicing</td>
 658             <td class="snns top orange">
 659               <a href="http://lambdadelta.info/static/coq/lambdadelta/basic_1/getl_defs.txt">getl_defs</a>
 660             </td>
 661             <td class="ssnn top orange">
 662               <a href="http://lambdadelta.info/static/coq/lambdadelta/basic_1/getl_props.txt">getl_props</a>
 663             </td>
 664           </tr>
 665           <tr>
 666             <td class="nnns top capitalize italic orange">
 667               <br />
 668             </td>
 669             <td class="nnns top italic orange">
 670               <br />
 671             </td>
 672             <td class="snns top orange">
 673               <a href="http://lambdadelta.info/static/coq/lambdadelta/basic_1/drop_defs.txt">drop_defs</a>
 674             </td>
 675             <td class="ssnn top orange">
 676               <a href="http://lambdadelta.info/static/coq/lambdadelta/basic_1/drop_props.txt">drop_props</a>
 677             </td>
 678           </tr>
 679           <tr>
 680             <td class="nnns top capitalize italic orange">
 681               <br />
 682             </td>
 683             <td class="snns top italic orange">basic term relocation</td>
 684             <td class="snns top orange">
 685               <a href="http://lambdadelta.info/static/coq/lambdadelta/basic_1/lift_defs.txt">lift_defs</a>
 686             </td>
 687             <td class="ssnn top orange">
 688               <a href="http://lambdadelta.info/static/coq/lambdadelta/basic_1/lift_props.txt">lift_props</a>
 689               <a href="http://lambdadelta.info/static/coq/lambdadelta/basic_1/lift_gen.txt">lift_gen</a>
 690               <a href="http://lambdadelta.info/static/coq/lambdadelta/basic_1/lift_tlt.txt">lift_tlt</a>
 691             </td>
 692           </tr>
 693           <tr>
 694             <td class="snns top capitalize italic red">grammar</td>
 695             <td class="snns top italic red">closures</td>
 696             <td class="snns top red">
 697               <a href="http://lambdadelta.info/static/coq/lambdadelta/basic_1/flt_defs.txt">flt_defs</a>
 698             </td>
 699             <td class="ssnn top red">
 700               <br />
 701             </td>
 702           </tr>
 703           <tr>
 704             <td class="nnns top capitalize italic red">
 705               <br />
 706             </td>
 707             <td class="snns top italic red">contexts</td>
 708             <td class="snns top red">
 709               <a href="http://lambdadelta.info/static/coq/lambdadelta/basic_1/contexts_defs.txt">contexts_defs</a>
 710               <a href="http://lambdadelta.info/static/coq/lambdadelta/basic_1/clt_defs.txt">clt_defs</a>
 711               <a href="http://lambdadelta.info/static/coq/lambdadelta/basic_1/ctail_defs.txt">ctail_defs</a>
 712               <a href="http://lambdadelta.info/static/coq/lambdadelta/basic_1/app_defs.txt">app_defs</a>
 713               <a href="http://lambdadelta.info/static/coq/lambdadelta/basic_1/cnt_defs.txt">cnt_defs</a>
 714             </td>
 715             <td class="ssnn top red">
 716               <br />
 717             </td>
 718           </tr>
 719           <tr>
 720             <td class="nnns top capitalize italic red">
 721               <br />
 722             </td>
 723             <td class="snns top italic red">terms</td>
 724             <td class="snns top red">
 725               <a href="http://lambdadelta.info/static/coq/lambdadelta/basic_1/tlist_defs.txt">tlist_defs</a>
 726             </td>
 727             <td class="ssnn top red">
 728               <br />
 729             </td>
 730           </tr>
 731           <tr>
 732             <td class="nnss top capitalize italic red">
 733               <br />
 734             </td>
 735             <td class="nnss top italic red">
 736               <br />
 737             </td>
 738             <td class="snss top red">
 739               <a href="http://lambdadelta.info/static/coq/lambdadelta/basic_1/terms_defs.txt">terms_defs</a>
 740               <a href="http://lambdadelta.info/static/coq/lambdadelta/basic_1/tlt_defs.txt">tlt_defs</a>
 741               <a href="http://lambdadelta.info/static/coq/lambdadelta/basic_1/iso_defs.txt">iso_defs</a>
 742             </td>
 743             <td class="sssn top red">
 744               <br />
 745             </td>
 746           </tr>
 747         </tbody>
 748       </table>
 749     </div>
 750     <div class="spacer">
 751       <img class="rule" alt="[Spacer]" title="lambdadelta rainbow rule" src="http://lambdadelta.info/images/rainbow.png" />
 752     </div>
 753     <div xmlns:ld="http://lambdadelta.info/" class="spacer">
 754       <br />
 755     </div>
 756     <div xmlns:ld="http://lambdadelta.info/" class="spacer">
 757       <a href="http://validator.w3.org/check?uri=referer">
 758         <img class="w3c" alt="[Valid XHTML 1.1]" title="Valid XHTML 1.1" src="http://www.w3.org/Icons/valid-xhtml11-blue" />
 759       </a>
 760       <a href="http://jigsaw.w3.org/css-validator/check/referer">
 761         <img class="w3c" alt="[Valid CSS level 2]" title="Valid CSS level 2" src="http://www.w3.org/Icons/valid-css2-blue" />
 762       </a>
 763       <a href="http://www.w3.org/XML/">
 764         <img class="w3c" alt="[Generated from XML via XSL]" title="Generated from XML via XSL" src="http://lambdadelta.info/images/xml_xsl2.png" />
 765       </a>
 766       <a href="http://www.w3.org/Graphics/PNG/">
 767         <img class="w3c" alt="[PNG used here]" title="PNG used here" src="http://lambdadelta.info/images/PNGnow2.png" />
 768       </a>
 769       <a href="http://www.anybrowser.org/campaign/">
 770         <img class="w3c" alt="[Viewable with any browser]" title="Viewable with any browser" src="http://www.anybrowser.org/campaign/bvgraphics/abtfile.png" />
 771       </a>
 772     </div>
 773     <div xmlns:ld="http://lambdadelta.info/" class="spacer">
 774       <br />
 775     </div>
 776     <div xmlns:ld="http://lambdadelta.info/" class="spacer">Last update: Mon, 19 Jan 2015 23:52:52 +0100</div>
 777   </body>
 778 </html>