+ <td class="snns top capitalize italic sky">uncounted context-sensitive parallel rt-computation</td>
+ <td class="snns top italic sky">refinement for lenvs</td>
+ <td class="snns top sky">lsubsx ( ? ⊢ ? ⊆ⓧ[?,?,?] ? )</td>
+ <td class="ssnn top sky">lsubsx_lfsx lsubsx_lsubsx</td>
+ </tr>
+ <tr>
+ <td class="nnns top capitalize italic sky">
+ <br />
+ </td>
+ <td class="nnns top capitalize italic sky">
+ <br />
+ </td>
+ <td class="snns top italic sky">strongly normalizing for lenvs on referred entries</td>
+ <td class="snns top sky">lfsx ( ? ⊢ ⬈*[?,?,?] 𝐒⦃?⦄ )</td>
+ <td class="ssnn top sky">lfsx_drops lfsx_fqup lfsx_lfpxs lfsx_lfsx</td>
+ </tr>
+ <tr>
+ <td class="nnns top capitalize italic sky">
+ <br />
+ </td>
+ <td class="nnns top capitalize italic sky">
+ <br />
+ </td>
+ <td class="snns top italic sky">strongly normalizing for term vectors</td>
+ <td class="snns top sky">csx_vector ( ⦃?,?⦄ ⊢ ⬈*[?,?] 𝐒⦃?⦄ )</td>
+ <td class="ssnn top sky">csx_cnx_vector csx_csx_vector</td>
+ </tr>
+ <tr>
+ <td class="nnns top capitalize italic sky">
+ <br />
+ </td>
+ <td class="nnns top capitalize italic sky">
+ <br />
+ </td>
+ <td class="snns top italic sky">strongly normalizing for terms</td>
+ <td class="snns top sky">csx ( ⦃?,?⦄ ⊢ ⬈*[?,?] 𝐒⦃?⦄ )</td>
+ <td class="ssnn top sky">csx_simple csx_simple_theq csx_drops csx_lsubr csx_lfdeq csx_aaa csx_gcp csx_gcr csx_lfpx csx_cnx csx_cpxs csx_lfpxs csx_csx</td>
+ </tr>
+ <tr>
+ <td class="nnns top capitalize italic sky">
+ <br />
+ </td>
+ <td class="nnns top capitalize italic sky">
+ <br />
+ </td>
+ <td class="snns top italic sky">for lenvs on referred entries</td>