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     <!--
 123    <table name="basic_1_sum"/>
 124 -->
 125     <ul xmlns:ld="http://lambdadelta.info/">
 126       <li>
 127         <span class="emph delta">January 2015.</span>
 128       Update with with backports from the abandoned specification of λδ version 2.
 129    </li>
 130     </ul>
 131     <ul xmlns:ld="http://lambdadelta.info/">
 132       <li>
 133         <span class="emph delta">May 2008.</span>
 134       Specification is concluded.
 135    </li>
 136     </ul>
 137     <ul xmlns:ld="http://lambdadelta.info/">
 138       <li>
 139         <span class="emph gamma">November 2006.</span>
 140       Decidability of native type assignment, λδ version 1 is released.
 141    </li>
 142     </ul>
 143     <ul xmlns:ld="http://lambdadelta.info/">
 144       <li>
 145         <span class="emph beta">December 2005.</span>
 146       Preservation of native type by reduction, λδ version 1 is announced.
 147    </li>
 148     </ul>
 149     <ul xmlns:ld="http://lambdadelta.info/">
 150       <li>
 151         <span class="emph alpha">May 2004.</span>
 152       Specification starts.
 153    </li>
 154     </ul>
 155     <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" />
 156     </div>
 157     <div xmlns:ld="http://lambdadelta.info/" class="text">This table reports the specification's components and their planes.
 158    </div>
 159     <div xmlns:ld="http://lambdadelta.info/" class="text">
 160       <table cellpadding="4" cellspacing="0">
 161         <tbody>
 162           <tr>
 163             <td class="snns top capitalize italic gray">component</td>
 164             <td class="snns top italic gray">plane</td>
 165             <td class="snns top gray">files</td>
 166             <td class="ssnn top gray">
 167               <br />
 168             </td>
 169           </tr>
 170           <tr>
 171             <td class="snns top capitalize italic wine">examples</td>
 172             <td class="snns top italic wine">terms with special features</td>
 173             <td class="snns top wine">
 174               <a href="http://lambdadelta.info/static/coq/lambdadelta/basic_1/levels_ex0.txt">levels_ex0</a>
 175               <a href="http://lambdadelta.info/static/coq/lambdadelta/basic_1/ty3_ex1.txt">ty3_ex1</a>
 176               <a href="http://lambdadelta.info/static/coq/lambdadelta/basic_1/nf2_ex2.txt">nf2_ex2</a>
 177             </td>
 178             <td class="ssnn top wine">
 179               <br />
 180             </td>
 181           </tr>
 182           <tr>
 183             <td class="snns top capitalize italic magenta" />
 184             <td class="snns top italic magenta" />
 185             <td class="snns top magenta" />
 186             <td class="ssnn top magenta">
 187               <br />
 188             </td>
 189           </tr>
 190           <tr>
 191             <td class="snns top capitalize italic prune">dynamic typing</td>
 192             <td class="snns top italic prune">well-formed contexts</td>
 193             <td class="snns top prune">
 194               <a href="http://lambdadelta.info/static/coq/lambdadelta/basic_1/wf3_defs.txt">wf3_defs</a>
 195             </td>
 196             <td class="ssnn top prune">
 197               <a href="http://lambdadelta.info/static/coq/lambdadelta/basic_1/wf3_props.txt">wf3_props</a>
 198             </td>
 199           </tr>
 200           <tr>
 201             <td class="nnns top capitalize italic prune">
 202               <br />
 203             </td>
 204             <td class="snns top italic prune">context ref. for native type assignment</td>
 205             <td class="snns top prune">
 206               <a href="http://lambdadelta.info/static/coq/lambdadelta/basic_1/csubt_defs.txt">csubt_defs</a>
 207             </td>
 208             <td class="ssnn top prune">
 209               <a href="http://lambdadelta.info/static/coq/lambdadelta/basic_1/csubt_props.txt">csubt_props</a>
 210               <a href="http://lambdadelta.info/static/coq/lambdadelta/basic_1/csubt_arity_props.txt">csubt_arity_props</a>
 211             </td>
 212           </tr>
 213           <tr>
 214             <td class="nnns top capitalize italic prune">
 215               <br />
 216             </td>
 217             <td class="snns top italic prune">native type assignment</td>
 218             <td class="snns top prune">
 219               <a href="http://lambdadelta.info/static/coq/lambdadelta/basic_1/ty3_defs.txt">ty3_defs</a>
 220             </td>
 221             <td class="ssnn top prune">
 222               <a href="http://lambdadelta.info/static/coq/lambdadelta/basic_1/ty3_props.txt">ty3_props</a>
 223               <a href="http://lambdadelta.info/static/coq/lambdadelta/basic_1/ty3_gen.txt">ty3_gen</a>
 224               <a href="http://lambdadelta.info/static/coq/lambdadelta/basic_1/ty3_gen_context.txt">ty3_gen_context</a>
 225               <a href="http://lambdadelta.info/static/coq/lambdadelta/basic_1/ty3_gen_nf2.txt">ty3_gen_nf2</a>
 226               <a href="http://lambdadelta.info/static/coq/lambdadelta/basic_1/ty3_lift.txt">ty3_lift</a>
 227               <a href="http://lambdadelta.info/static/coq/lambdadelta/basic_1/ty3_subst0.txt">ty3_subst0</a>
 228               <a href="http://lambdadelta.info/static/coq/lambdadelta/basic_1/ty3_arity_props.txt">ty3_arity_props</a>
 229               <a href="http://lambdadelta.info/static/coq/lambdadelta/basic_1/ty3_nf2_gen.txt">ty3_nf2_gen</a>
 230               <a href="http://lambdadelta.info/static/coq/lambdadelta/basic_1/ty3_sred.txt">ty3_sred</a>
 231               <a href="http://lambdadelta.info/static/coq/lambdadelta/basic_1/ty3_sred_props.txt">ty3_sred_props</a>
 232               <a href="http://lambdadelta.info/static/coq/lambdadelta/basic_1/ty3_dec.txt">ty3_dec</a>
 233             </td>
 234           </tr>
 235           <tr>
 236             <td class="snns top capitalize italic blue">equivalence</td>
 237             <td class="snns top italic blue">context-sensitive equivalence</td>
 238             <td class="snns top blue">
 239               <a href="http://lambdadelta.info/static/coq/lambdadelta/basic_1/pc3_defs.txt">pc3_defs</a>
 240             </td>
 241             <td class="ssnn top blue">
 242               <a href="http://lambdadelta.info/static/coq/lambdadelta/basic_1/pc3_props.txt">pc3_props</a>
 243               <a href="http://lambdadelta.info/static/coq/lambdadelta/basic_1/pc3_gen.txt">pc3_gen</a>
 244               <a href="http://lambdadelta.info/static/coq/lambdadelta/basic_1/pc3_gen_context.txt">pc3_gen_context</a>
 245               <a href="http://lambdadelta.info/static/coq/lambdadelta/basic_1/pc3_subst0.txt">pc3_subst0</a>
 246             </td>
 247           </tr>
 248           <tr>
 249             <td class="nnns top capitalize italic blue">
 250               <br />
 251             </td>
 252             <td class="snns top italic blue">context-free equivalence</td>
 253             <td class="snns top blue">
 254               <a href="http://lambdadelta.info/static/coq/lambdadelta/basic_1/pc1_defs.txt">pc1_defs</a>
 255             </td>
 256             <td class="ssnn top blue">
 257               <a href="http://lambdadelta.info/static/coq/lambdadelta/basic_1/pc1_props.txt">pc1_props</a>
 258             </td>
 259           </tr>
 260           <tr>
 261             <td class="snns top capitalize italic sky" />
 262             <td class="snns top italic sky" />
 263             <td class="snns top sky" />
 264             <td class="ssnn top sky">
 265               <br />
 266             </td>
 267           </tr>
 268           <tr>
 269             <td class="snns top capitalize italic cyan">computation</td>
 270             <td class="snns top italic cyan">context ref. for reducibility</td>
 271             <td class="snns top cyan">
 272               <a href="http://lambdadelta.info/static/coq/lambdadelta/basic_1/csubc_defs.txt">csubc_defs</a>
 273             </td>
 274             <td class="ssnn top cyan">
 275               <a href="http://lambdadelta.info/static/coq/lambdadelta/basic_1/csubc_props.txt">csubc_props</a>
 276             </td>
 277           </tr>
 278           <tr>
 279             <td class="nnns top capitalize italic cyan">
 280               <br />
 281             </td>
 282             <td class="snns top italic cyan">reducibility</td>
 283             <td class="snns top cyan">
 284               <a href="http://lambdadelta.info/static/coq/lambdadelta/basic_1/sc3_defs.txt">sc3_defs</a>
 285             </td>
 286             <td class="ssnn top cyan">
 287               <a href="http://lambdadelta.info/static/coq/lambdadelta/basic_1/sc3_props.txt">sc3_props</a>
 288               <a href="http://lambdadelta.info/static/coq/lambdadelta/basic_1/sc3_arity.txt">sc3_arity</a>
 289             </td>
 290           </tr>
 291           <tr>
 292             <td class="nnns top capitalize italic cyan">
 293               <br />
 294             </td>
 295             <td class="snns top italic cyan">strongly normalizing computation</td>
 296             <td class="snns top cyan">
 297               <a href="http://lambdadelta.info/static/coq/lambdadelta/basic_1/sn3_defs.txt">sn3_defs</a>
 298             </td>
 299             <td class="ssnn top cyan">
 300               <a href="http://lambdadelta.info/static/coq/lambdadelta/basic_1/sn3_gen.txt">sn3_gen</a>
 301               <a href="http://lambdadelta.info/static/coq/lambdadelta/basic_1/sn3_props.txt">sn3_props</a>
 302             </td>
 303           </tr>
 304           <tr>
 305             <td class="nnns top capitalize italic cyan">
 306               <br />
 307             </td>
 308             <td class="snns top italic cyan">context-sensitive computation</td>
 309             <td class="snns top cyan">
 310               <a href="http://lambdadelta.info/static/coq/lambdadelta/basic_1/pr3_defs.txt">pr3_defs</a>
 311             </td>
 312             <td class="ssnn top cyan">
 313               <a href="http://lambdadelta.info/static/coq/lambdadelta/basic_1/pr3_props.txt">pr3_props</a>
 314               <a href="http://lambdadelta.info/static/coq/lambdadelta/basic_1/pr3_gen.txt">pr3_gen</a>
 315               <a href="http://lambdadelta.info/static/coq/lambdadelta/basic_1/pr3_gen_context.txt">pr3_gen_context</a>
 316               <a href="http://lambdadelta.info/static/coq/lambdadelta/basic_1/pr3_iso.txt">pr3_iso</a>
 317               <a href="http://lambdadelta.info/static/coq/lambdadelta/basic_1/pr3_subst1.txt">pr3_subst1</a>
 318               <a href="http://lambdadelta.info/static/coq/lambdadelta/basic_1/pr3_confluence.txt">pr3_confluence</a>
 319             </td>
 320           </tr>
 321           <tr>
 322             <td class="nnns top capitalize italic cyan">
 323               <br />
 324             </td>
 325             <td class="snns top italic cyan">context-free computation</td>
 326             <td class="snns top cyan">
 327               <a href="http://lambdadelta.info/static/coq/lambdadelta/basic_1/pr1_defs.txt">pr1_defs</a>
 328             </td>
 329             <td class="ssnn top cyan">
 330               <a href="http://lambdadelta.info/static/coq/lambdadelta/basic_1/pr1_props.txt">pr1_props</a>
 331               <a href="http://lambdadelta.info/static/coq/lambdadelta/basic_1/pr1_confluence.txt">pr1_confluence</a>
 332             </td>
 333           </tr>
 334           <tr>
 335             <td class="snns top capitalize italic water">reduction</td>
 336             <td class="snns top italic water">normal forms for context-sensitive reduction</td>
 337             <td class="snns top water">
 338               <a href="http://lambdadelta.info/static/coq/lambdadelta/basic_1/nf2_defs.txt">nf2_defs</a>
 339             </td>
 340             <td class="ssnn top water">
 341               <a href="http://lambdadelta.info/static/coq/lambdadelta/basic_1/nf2_props.txt">nf2_props</a>
 342               <a href="http://lambdadelta.info/static/coq/lambdadelta/basic_1/nf2_gen.txt">nf2_gen</a>
 343               <a href="http://lambdadelta.info/static/coq/lambdadelta/basic_1/nf2_dec.txt">nf2_dec</a>
 344             </td>
 345           </tr>
 346           <tr>
 347             <td class="nnns top capitalize italic water">
 348               <br />
 349             </td>
 350             <td class="snns top italic water">context-sensitive reduction</td>
 351             <td class="snns top water">
 352               <a href="http://lambdadelta.info/static/coq/lambdadelta/basic_1/pr2_defs.txt">pr2_defs</a>
 353             </td>
 354             <td class="ssnn top water">
 355               <a href="http://lambdadelta.info/static/coq/lambdadelta/basic_1/pr2_gen.txt">pr2_gen</a>
 356               <a href="http://lambdadelta.info/static/coq/lambdadelta/basic_1/pr2_gen_context.txt">pr2_gen_context</a>
 357               <a href="http://lambdadelta.info/static/coq/lambdadelta/basic_1/pr2_lift.txt">pr2_lift</a>
 358               <a href="http://lambdadelta.info/static/coq/lambdadelta/basic_1/pr2_subst1.txt">pr2_subst1</a>
 359               <a href="http://lambdadelta.info/static/coq/lambdadelta/basic_1/pr2_confluence.txt">pr2_confluence</a>
 360             </td>
 361           </tr>
 362           <tr>
 363             <td class="nnns top capitalize italic water">
 364               <br />
 365             </td>
 366             <td class="snns top italic water">normal forms for context-free reduction</td>
 367             <td class="snns top water" />
 368             <td class="ssnn top water">
 369               <a href="http://lambdadelta.info/static/coq/lambdadelta/basic_1/nf0_dec.txt">nf0_dec</a>
 370             </td>
 371           </tr>
 372           <tr>
 373             <td class="nnns top capitalize italic water">
 374               <br />
 375             </td>
 376             <td class="snns top italic water">context-free reduction</td>
 377             <td class="snns top water">
 378               <a href="http://lambdadelta.info/static/coq/lambdadelta/basic_1/wcpr0_defs.txt">wcpr0_defs</a>
 379             </td>
 380             <td class="ssnn top water">
 381               <br />
 382             </td>
 383           </tr>
 384           <tr>
 385             <td class="nnns top capitalize italic water">
 386               <br />
 387             </td>
 388             <td class="nnns top italic water">
 389               <br />
 390             </td>
 391             <td class="snns top water">
 392               <a href="http://lambdadelta.info/static/coq/lambdadelta/basic_1/pr0_defs.txt">pr0_defs</a>
 393             </td>
 394             <td class="ssnn top water">
 395               <a href="http://lambdadelta.info/static/coq/lambdadelta/basic_1/pr0_gen.txt">pr0_gen</a>
 396               <a href="http://lambdadelta.info/static/coq/lambdadelta/basic_1/pr0_lift.txt">pr0_lift</a>
 397               <a href="http://lambdadelta.info/static/coq/lambdadelta/basic_1/pr0_subst0.txt">pr0_subst0</a>
 398               <a href="http://lambdadelta.info/static/coq/lambdadelta/basic_1/pr0_subst1.txt">pr0_subst1</a>
 399               <a href="http://lambdadelta.info/static/coq/lambdadelta/basic_1/pr0_confluence.txt">pr0_confluence</a>
 400             </td>
 401           </tr>
 402           <tr>
 403             <td class="snns top capitalize italic green">unfold</td>
 404             <td class="snns top italic green">iterated static type assignment</td>
 405             <td class="snns top green">
 406               <a href="http://lambdadelta.info/static/coq/lambdadelta/basic_1/sty1_defs.txt">sty1_defs</a>
 407             </td>
 408             <td class="ssnn top green">
 409               <a href="http://lambdadelta.info/static/coq/lambdadelta/basic_1/sty1_props.txt">sty1_props</a>
 410             </td>
 411           </tr>
 412           <tr>
 413             <td class="snns top capitalize italic grass">static typing</td>
 414             <td class="snns top italic grass">static type assignment</td>
 415             <td class="snns top grass">
 416               <a href="http://lambdadelta.info/static/coq/lambdadelta/basic_1/sty0_defs.txt">sty0_defs</a>
 417             </td>
 418             <td class="ssnn top grass">
 419               <a href="http://lambdadelta.info/static/coq/lambdadelta/basic_1/sty0_props.txt">sty0_props</a>
 420             </td>
 421           </tr>
 422           <tr>
 423             <td class="nnns top capitalize italic grass">
 424               <br />
 425             </td>
 426             <td class="snns top italic grass">context ref. for binary arity assignment</td>
 427             <td class="snns top grass">
 428               <a href="http://lambdadelta.info/static/coq/lambdadelta/basic_1/csuba_defs.txt">csuba_defs</a>
 429             </td>
 430             <td class="ssnn top grass">
 431               <a href="http://lambdadelta.info/static/coq/lambdadelta/basic_1/csuba_props.txt">csuba_props</a>
 432             </td>
 433           </tr>
 434           <tr>
 435             <td class="nnns top capitalize italic grass">
 436               <br />
 437             </td>
 438             <td class="snns top italic grass">binary arity assignment</td>
 439             <td class="snns top grass">
 440               <a href="http://lambdadelta.info/static/coq/lambdadelta/basic_1/arity_defs.txt">arity_defs</a>
 441             </td>
 442             <td class="ssnn top grass">
 443               <a href="http://lambdadelta.info/static/coq/lambdadelta/basic_1/arity_props.txt">arity_props</a>
 444               <a href="http://lambdadelta.info/static/coq/lambdadelta/basic_1/arity_gen.txt">arity_gen</a>
 445               <a href="http://lambdadelta.info/static/coq/lambdadelta/basic_1/arity_subst0.txt">arity_subst0</a>
 446               <a href="http://lambdadelta.info/static/coq/lambdadelta/basic_1/arity_sred.txt">arity_sred</a>
 447             </td>
 448           </tr>
 449           <tr>
 450             <td class="nnns top capitalize italic grass">
 451               <br />
 452             </td>
 453             <td class="snns top italic grass">binary arity</td>
 454             <td class="snns top grass">
 455               <a href="http://lambdadelta.info/static/coq/lambdadelta/basic_1/levels_defs.txt">levels_defs</a>
 456               <a href="http://lambdadelta.info/static/coq/lambdadelta/basic_1/llt_defs.txt">llt_defs</a>
 457               <a href="http://lambdadelta.info/static/coq/lambdadelta/basic_1/aprem_defs.txt">aprem_defs</a>
 458             </td>
 459             <td class="ssnn top grass">
 460               <br />
 461             </td>
 462           </tr>
 463           <tr>
 464             <td class="nnns top capitalize italic grass">
 465               <br />
 466             </td>
 467             <td class="snns top italic grass">parameters</td>
 468             <td class="snns top grass">
 469               <a href="http://lambdadelta.info/static/coq/lambdadelta/basic_1/parameter_defs.txt">parameter_defs</a>
 470             </td>
 471             <td class="ssnn top grass">
 472               <br />
 473             </td>
 474           </tr>
 475           <tr>
 476             <td class="nnns top capitalize italic grass">
 477               <br />
 478             </td>
 479             <td class="snns top italic grass">basic context ref.</td>
 480             <td class="snns top grass">
 481               <a href="http://lambdadelta.info/static/coq/lambdadelta/basic_1/csubv_defs.txt">csubv_defs</a>
 482             </td>
 483             <td class="ssnn top grass">
 484               <br />
 485             </td>
 486           </tr>
 487           <tr>
 488             <td class="snns top capitalize italic yellow">multiple substitution</td>
 489             <td class="snns top italic yellow">iterated context slicing</td>
 490             <td class="snns top yellow">
 491               <a href="http://lambdadelta.info/static/coq/lambdadelta/basic_1/drop1_defs.txt">drop1_defs</a>
 492             </td>
 493             <td class="ssnn top yellow">
 494               <a href="http://lambdadelta.info/static/coq/lambdadelta/basic_1/drop1_props.txt">drop1_props</a>
 495             </td>
 496           </tr>
 497           <tr>
 498             <td class="nnns top capitalize italic yellow">
 499               <br />
 500             </td>
 501             <td class="snns top italic yellow">generic term relocation</td>
 502             <td class="snns top yellow">
 503               <a href="http://lambdadelta.info/static/coq/lambdadelta/basic_1/lift1_defs.txt">lift1_defs</a>
 504             </td>
 505             <td class="ssnn top yellow">
 506               <a href="http://lambdadelta.info/static/coq/lambdadelta/basic_1/lift1_props.txt">lift1_props</a>
 507             </td>
 508           </tr>
 509           <tr>
 510             <td class="snns top capitalize italic orange">substitution</td>
 511             <td class="snns top italic orange">ordinary substitution</td>
 512             <td class="snns top orange">
 513               <a href="http://lambdadelta.info/static/coq/lambdadelta/basic_1/subst_defs.txt">subst_defs</a>
 514             </td>
 515             <td class="ssnn top orange">
 516               <a href="http://lambdadelta.info/static/coq/lambdadelta/basic_1/subst_props.txt">subst_props</a>
 517             </td>
 518           </tr>
 519           <tr>
 520             <td class="nnns top capitalize italic orange">
 521               <br />
 522             </td>
 523             <td class="nnns top italic orange">
 524               <br />
 525             </td>
 526             <td class="snns top orange">
 527               <a href="http://lambdadelta.info/static/coq/lambdadelta/basic_1/csubst1_defs.txt">csubst1_defs</a>
 528             </td>
 529             <td class="ssnn top orange">
 530               <a href="http://lambdadelta.info/static/coq/lambdadelta/basic_1/csubst1_props.txt">csubst1_props</a>
 531             </td>
 532           </tr>
 533           <tr>
 534             <td class="nnns top capitalize italic orange">
 535               <br />
 536             </td>
 537             <td class="nnns top italic orange">
 538               <br />
 539             </td>
 540             <td class="snns top orange">
 541               <a href="http://lambdadelta.info/static/coq/lambdadelta/basic_1/subst1_defs.txt">subst1_defs</a>
 542             </td>
 543             <td class="ssnn top orange">
 544               <a href="http://lambdadelta.info/static/coq/lambdadelta/basic_1/subst1_gen.txt">subst1_gen</a>
 545               <a href="http://lambdadelta.info/static/coq/lambdadelta/basic_1/subst1_lift.txt">subst1_lift</a>
 546               <a href="http://lambdadelta.info/static/coq/lambdadelta/basic_1/subst1_subst1.txt">subst1_subst1</a>
 547               <a href="http://lambdadelta.info/static/coq/lambdadelta/basic_1/subst1_confluence.txt">subst1_confluence</a>
 548             </td>
 549           </tr>
 550           <tr>
 551             <td class="nnns top capitalize italic orange">
 552               <br />
 553             </td>
 554             <td class="snns top italic orange">normal forms for ordinary strict substitution</td>
 555             <td class="snns top orange" />
 556             <td class="ssnn top orange">
 557               <a href="http://lambdadelta.info/static/coq/lambdadelta/basic_1/dnf_dec.txt">dnf_dec</a>
 558             </td>
 559           </tr>
 560           <tr>
 561             <td class="nnns top capitalize italic orange">
 562               <br />
 563             </td>
 564             <td class="snns top italic orange">ordinary strict substitution</td>
 565             <td class="snns top orange">
 566               <a href="http://lambdadelta.info/static/coq/lambdadelta/basic_1/fsubst0_defs.txt">fsubst0_defs</a>
 567             </td>
 568             <td class="ssnn top orange">
 569               <br />
 570             </td>
 571           </tr>
 572           <tr>
 573             <td class="nnns top capitalize italic orange">
 574               <br />
 575             </td>
 576             <td class="nnns top italic orange">
 577               <br />
 578             </td>
 579             <td class="snns top orange">
 580               <a href="http://lambdadelta.info/static/coq/lambdadelta/basic_1/csubst0_defs.txt">csubst0_defs</a>
 581             </td>
 582             <td class="ssnn top orange">
 583               <br />
 584             </td>
 585           </tr>
 586           <tr>
 587             <td class="nnns top capitalize italic orange">
 588               <br />
 589             </td>
 590             <td class="nnns top italic orange">
 591               <br />
 592             </td>
 593             <td class="snns top orange">
 594               <a href="http://lambdadelta.info/static/coq/lambdadelta/basic_1/subst0_defs.txt">subst0_defs</a>
 595             </td>
 596             <td class="ssnn top orange">
 597               <a href="http://lambdadelta.info/static/coq/lambdadelta/basic_1/subst0_gen.txt">subst0_gen</a>
 598               <a href="http://lambdadelta.info/static/coq/lambdadelta/basic_1/subst0_tlt.txt">subst0_tlt</a>
 599               <a href="http://lambdadelta.info/static/coq/lambdadelta/basic_1/subst0_lift.txt">subst0_lift</a>
 600               <a href="http://lambdadelta.info/static/coq/lambdadelta/basic_1/subst0_subst0.txt">subst0_subst0</a>
 601               <a href="http://lambdadelta.info/static/coq/lambdadelta/basic_1/subst0_confluence.txt">subst0_confluence</a>
 602             </td>
 603           </tr>
 604           <tr>
 605             <td class="nnns top capitalize italic orange">
 606               <br />
 607             </td>
 608             <td class="snns top italic orange">basic local env. slicing</td>
 609             <td class="snns top orange">
 610               <a href="http://lambdadelta.info/static/coq/lambdadelta/basic_1/getl_defs.txt">getl_defs</a>
 611             </td>
 612             <td class="ssnn top orange">
 613               <a href="http://lambdadelta.info/static/coq/lambdadelta/basic_1/getl_props.txt">getl_props</a>
 614             </td>
 615           </tr>
 616           <tr>
 617             <td class="nnns top capitalize italic orange">
 618               <br />
 619             </td>
 620             <td class="nnns top italic orange">
 621               <br />
 622             </td>
 623             <td class="snns top orange">
 624               <a href="http://lambdadelta.info/static/coq/lambdadelta/basic_1/drop_defs.txt">drop_defs</a>
 625             </td>
 626             <td class="ssnn top orange">
 627               <a href="http://lambdadelta.info/static/coq/lambdadelta/basic_1/drop_props.txt">drop_props</a>
 628             </td>
 629           </tr>
 630           <tr>
 631             <td class="nnns top capitalize italic orange">
 632               <br />
 633             </td>
 634             <td class="snns top italic orange">basic term relocation</td>
 635             <td class="snns top orange">
 636               <a href="http://lambdadelta.info/static/coq/lambdadelta/basic_1/lift_defs.txt">lift_defs</a>
 637             </td>
 638             <td class="ssnn top orange">
 639               <a href="http://lambdadelta.info/static/coq/lambdadelta/basic_1/lift_props.txt">lift_props</a>
 640               <a href="http://lambdadelta.info/static/coq/lambdadelta/basic_1/lift_gen.txt">lift_gen</a>
 641               <a href="http://lambdadelta.info/static/coq/lambdadelta/basic_1/lift_tlt.txt">lift_tlt</a>
 642             </td>
 643           </tr>
 644           <tr>
 645             <td class="snns top capitalize italic red">grammar</td>
 646             <td class="snns top italic red">closures</td>
 647             <td class="snns top red">
 648               <a href="http://lambdadelta.info/static/coq/lambdadelta/basic_1/flt_defs.txt">flt_defs</a>
 649             </td>
 650             <td class="ssnn top red">
 651               <br />
 652             </td>
 653           </tr>
 654           <tr>
 655             <td class="nnns top capitalize italic red">
 656               <br />
 657             </td>
 658             <td class="snns top italic red">contexts</td>
 659             <td class="snns top red">
 660               <a href="http://lambdadelta.info/static/coq/lambdadelta/basic_1/contexts_defs.txt">contexts_defs</a>
 661               <a href="http://lambdadelta.info/static/coq/lambdadelta/basic_1/clt_defs.txt">clt_defs</a>
 662               <a href="http://lambdadelta.info/static/coq/lambdadelta/basic_1/ctail_defs.txt">ctail_defs</a>
 663               <a href="http://lambdadelta.info/static/coq/lambdadelta/basic_1/app_defs.txt">app_defs</a>
 664               <a href="http://lambdadelta.info/static/coq/lambdadelta/basic_1/cnt_defs.txt">cnt_defs</a>
 665             </td>
 666             <td class="ssnn top red">
 667               <br />
 668             </td>
 669           </tr>
 670           <tr>
 671             <td class="nnns top capitalize italic red">
 672               <br />
 673             </td>
 674             <td class="snns top italic red">terms</td>
 675             <td class="snns top red">
 676               <a href="http://lambdadelta.info/static/coq/lambdadelta/basic_1/tlist_defs.txt">tlist_defs</a>
 677             </td>
 678             <td class="ssnn top red">
 679               <br />
 680             </td>
 681           </tr>
 682           <tr>
 683             <td class="nnss top capitalize italic red">
 684               <br />
 685             </td>
 686             <td class="nnss top italic red">
 687               <br />
 688             </td>
 689             <td class="snss top red">
 690               <a href="http://lambdadelta.info/static/coq/lambdadelta/basic_1/terms_defs.txt">terms_defs</a>
 691               <a href="http://lambdadelta.info/static/coq/lambdadelta/basic_1/tlt_defs.txt">tlt_defs</a>
 692               <a href="http://lambdadelta.info/static/coq/lambdadelta/basic_1/iso_defs.txt">iso_defs</a>
 693             </td>
 694             <td class="sssn top red">
 695               <br />
 696             </td>
 697           </tr>
 698         </tbody>
 699       </table>
 700     </div>
 701     <div class="spacer">
 702       <img class="rule" alt="[Spacer]" title="lambdadelta rainbow rule" src="http://lambdadelta.info/images/rainbow.png" />
 703     </div>
 704     <div xmlns:ld="http://lambdadelta.info/" class="spacer">
 705       <br />
 706     </div>
 707     <div xmlns:ld="http://lambdadelta.info/" class="spacer">
 708       <a href="http://validator.w3.org/check?uri=referer">
 709         <img class="w3c" alt="[Valid XHTML 1.1]" title="Valid XHTML 1.1" src="http://www.w3.org/Icons/valid-xhtml11-blue" />
 710       </a>
 711       <a href="http://jigsaw.w3.org/css-validator/check/referer">
 712         <img class="w3c" alt="[Valid CSS level 2]" title="Valid CSS level 2" src="http://www.w3.org/Icons/valid-css2-blue" />
 713       </a>
 714       <a href="http://www.w3.org/XML/">
 715         <img class="w3c" alt="[Generated from XML via XSL]" title="Generated from XML via XSL" src="http://lambdadelta.info/images/xml_xsl2.png" />
 716       </a>
 717       <a href="http://www.w3.org/Graphics/PNG/">
 718         <img class="w3c" alt="[PNG used here]" title="PNG used here" src="http://lambdadelta.info/images/PNGnow2.png" />
 719       </a>
 720       <a href="http://www.anybrowser.org/campaign/">
 721         <img class="w3c" alt="[Viewable with any browser]" title="Viewable with any browser" src="http://www.anybrowser.org/campaign/bvgraphics/abtfile.png" />
 722       </a>
 723     </div>
 724     <div xmlns:ld="http://lambdadelta.info/" class="spacer">
 725       <br />
 726     </div>
 727     <div xmlns:ld="http://lambdadelta.info/" class="spacer">Last update: Sun, 18 Jan 2015 17:28:58 +0100</div>
 728   </body>
 729 </html>