+ </tr>
+ <tr>
+ <td class="nnns top capitalize italic water">
+ <br />
+ </td>
+ <td class="snns top italic water">reducible forms for context-sensitive reduction</td>
+ <td class="snns top water">crr ( ⦃?,?⦄ ⊢ ➡ 𝐑⦃?⦄ )</td>
+ <td class="snnn top water">crr_lift</td>
+ <td class="snnn top water">
+ <br />
+ </td>
+ <td class="ssnn top water">
+ <br />
+ </td>
+ </tr>
+ <tr>
+ <td class="snns top capitalize italic green">unfold</td>
+ <td class="snns top italic green">unfold</td>
+ <td class="snns top green">unfold ( ⦃?,?⦄ ⊢ ? ⧫* ? )</td>
+ <td class="snnn top green">
+ <br />
+ </td>
+ <td class="snnn top green">
+ <br />
+ </td>
+ <td class="ssnn top green">
+ <br />
+ </td>
+ </tr>
+ <tr>
+ <td class="nnns top capitalize italic green">
+ <br />
+ </td>
+ <td class="snns top italic green">iterated static type assignment</td>
+ <td class="snns top green">lstas ( ⦃?,?⦄ ⊢ ? •*[?,?] ? )</td>
+ <td class="snnn top green">lstas_lift lstas_llpx_sn.ma lstas_aaa lstas_da lstas_lstas</td>
+ <td class="snnn top green">
+ <br />
+ </td>
+ <td class="ssnn top green">
+ <br />
+ </td>
+ </tr>
+ <tr>
+ <td class="snns top capitalize italic grass">static typing</td>
+ <td class="snns top italic grass">local env. ref. for degree assignment</td>
+ <td class="snns top grass">lsubd ( ? ⊢ ? ⫃▪[?,?] ? )</td>
+ <td class="snnn top grass">lsubd_da lsubd_lsubd</td>
+ <td class="snnn top grass">
+ <br />
+ </td>
+ <td class="ssnn top grass">
+ <br />
+ </td>
+ </tr>
+ <tr>
+ <td class="nnns top capitalize italic grass">
+ <br />
+ </td>
+ <td class="snns top italic grass">degree assignment</td>
+ <td class="snns top grass">da ( ⦃?,?⦄ ⊢ ? ▪[?,?] ? )</td>
+ <td class="snnn top grass">da_lift da_aaa da_da</td>
+ <td class="snnn top grass">
+ <br />
+ </td>
+ <td class="ssnn top grass">
+ <br />
+ </td>
+ </tr>
+ <tr>
+ <td class="nnns top capitalize italic grass">
+ <br />
+ </td>
+ <td class="snns top italic grass">parameters</td>
+ <td class="snns top grass">sh</td>
+ <td class="snnn top grass">sd</td>
+ <td class="snnn top grass">
+ <br />
+ </td>
+ <td class="ssnn top grass">
+ <br />
+ </td>
+ </tr>
+ <tr>
+ <td class="nnns top capitalize italic grass">
+ <br />
+ </td>
+ <td class="snns top italic grass">local env. ref. for atomic arity assignment</td>
+ <td class="snns top grass">lsuba ( ? ⊢ ? ⫃⁝ ? )</td>
+ <td class="snnn top grass">lsuba_aaa lsuba_lsuba</td>
+ <td class="snnn top grass">
+ <br />
+ </td>
+ <td class="ssnn top grass">
+ <br />
+ </td>
+ </tr>
+ <tr>
+ <td class="nnns top capitalize italic grass">
+ <br />
+ </td>
+ <td class="snns top italic grass">atomic arity assignment</td>
+ <td class="snns top grass">aaa ( ⦃?,?⦄ ⊢ ? ⁝ ? )</td>
+ <td class="snnn top grass">aaa_lift aaa_lifts aaa_fqus aaa_lleq aaa_aaa</td>
+ <td class="snnn top grass">
+ <br />
+ </td>
+ <td class="ssnn top grass">
+ <br />
+ </td>
+ </tr>
+ <tr>
+ <td class="nnns top capitalize italic grass">
+ <br />
+ </td>
+ <td class="snns top italic grass">restricted local env. ref.</td>
+ <td class="snns top grass">lsubr ( ? ⫃ ? )</td>
+ <td class="snnn top grass">lsubr_lsubr</td>
+ <td class="snnn top grass">
+ <br />
+ </td>
+ <td class="ssnn top grass">
+ <br />
+ </td>
+ </tr>
+ <tr>
+ <td class="snns top capitalize italic yellow">multiple substitution</td>
+ <td class="snns top italic yellow">lazy equivalence</td>
+ <td class="snns top yellow">fleq ( ⦃?,?,?⦄ ≡[?] ⦃?,?,?⦄ )</td>
+ <td class="snnn top yellow">fleq_fleq</td>
+ <td class="snnn top yellow">
+ <br />
+ </td>
+ <td class="ssnn top yellow">
+ <br />
+ </td>
+ </tr>
+ <tr>
+ <td class="nnns top capitalize italic yellow">
+ <br />
+ </td>
+ <td class="nnns top italic yellow">
+ <br />
+ </td>
+ <td class="snns top yellow">lleq ( ? ≡[?,?] ? )</td>
+ <td class="snnn top yellow">lleq_alt lleq_alt_rec lleq_leq lleq_drop lleq_fqus lleq_llor lleq_lleq</td>
+ <td class="snnn top yellow">
+ <br />
+ </td>
+ <td class="ssnn top yellow">