helm/style/mmlextension.xsl

   1 <?xml version="1.0"?>
   2
   3 <!-- Copyright (C) 2000, HELM Team                                     -->
   4 <!--                                                                   -->
   5 <!-- This file is part of HELM, an Hypertextual, Electronic            -->
   6 <!-- Library of Mathematics, developed at the Computer Science         -->
   7 <!-- Department, University of Bologna, Italy.                         -->
   8 <!--                                                                   -->
   9 <!-- HELM is free software; you can redistribute it and/or             -->
  10 <!-- modify it under the terms of the GNU General Public License       -->
  11 <!-- as published by the Free Software Foundation; either version 2    -->
  12 <!-- of the License, or (at your option) any later version.            -->
  13 <!--                                                                   -->
  14 <!-- HELM is distributed in the hope that it will be useful,           -->
  15 <!-- but WITHOUT ANY WARRANTY; without even the implied warranty of    -->
  16 <!-- MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE.  See the     -->
  17 <!-- GNU General Public License for more details.                      -->
  18 <!--                                                                   -->
  19 <!-- You should have received a copy of the GNU General Public License -->
  20 <!-- along with HELM; if not, write to the Free Software               -->
  21 <!-- Foundation, Inc., 59 Temple Place - Suite 330, Boston,            -->
  22 <!-- MA  02111-1307, USA.                                              -->
  23 <!--                                                                   -->
  24 <!-- For details, see the HELM World-Wide-Web page,                    -->
  25 <!-- http://cs.unibo.it/helm/.                                         -->
  26
  27 <!--***********************************************************************-->
  28 <!-- Extension to the XSLT version 0.07 of MathML content to presentation: -->
  29 <!-- First draft: February 19 2000, Andrea Asperti, Irene Schena           -->
  30 <!-- Revised: March 3 2000, Irene Schena                                   -->
  31 <!-- Revised: March 15 2000, Claudio Sacerdoti Coen, Irene Schena          -->
  32 <!-- Revised: March 21 2000, Irene Schena                                  -->
  33 <!--***********************************************************************-->
  34
  35 <!-- NOTE: the namespace declaration has to be done in the stylesheets
  36 which generates the toplevel element (see for instance xlink) -->
  37 <xsl:stylesheet version="1.0" xmlns:xsl="http://www.w3.org/1999/XSL/Transform"
  38                               xmlns:m="http://www.w3.org/1998/Math/MathML"
  39                               xmlns:helm="http://www.cs.unibo.it/helm"
  40                               xmlns:xlink="http://www.w3.org/1999/xlink">
  41
  42 <!-- OLD: <xsl:import href="mml2mmlv1_0.xsl"/> -->
  43 <xsl:import href="mmlctop.xsl-0.14"/>
  44
  45 <xsl:import href="mmltheoryextension.xsl"/>
  46
  47 <xsl:param name="explodeall" select="false()"/>
  48
  49 <!--***********************************************************************-->
  50 <!-- Parameter affecting line-breaking                                     -->
  51 <!--***********************************************************************-->
  52
  53 <xsl:variable name="framewidth" select="35"/>
  54
  55 <!--***********************************************************************-->
  56 <!-- Gli oggetti sono stampati come mtext all'interno di una marca toplevel-->
  57 <!-- math ma al di fuori di semantics. Ora vi sono tanti semantics quanti  -->
  58 <!-- sono i termini: la presentation per un termine e' generata come primo -->
  59 <!-- figlio di un semantics e l'originario content viene inserito nel      -->
  60 <!-- nel secondo figlio di semantics, annotation-xml                       -->
  61 <!--***********************************************************************-->
  62
  63 <!--**********************-->
  64 <!--        OBJECTS       -->
  65 <!--**********************-->
  66
  67 <xsl:param name="type" select="'standalone'"/>
  68
  69 <xsl:template match="/">
  70  <xsl:choose>
  71   <xsl:when test="$type = 'standalone'">
  72    <xsl:apply-templates select="*"/>
  73   </xsl:when>
  74   <xsl:otherwise>
  75    <to_be_embedded>
  76     <xsl:apply-templates select="*"/>
  77    </to_be_embedded>
  78   </xsl:otherwise>
  79  </xsl:choose>
  80 </xsl:template>
  81
  82 <!-- DEFINITION -->
  83
  84 <xsl:template match="Definition">
  85     <m:math>
  86      <m:mtable align="baseline 1" equalrows="false" columnalign="left" helm:xref="{@helm:xref}">
  87       <m:mtr>
  88        <m:mtd>
  89         <m:mrow>
  90          <m:mtext>DEFINITION <xsl:value-of select="@name"/>(<xsl:if test="string(./Params) != &quot;&quot;"><xsl:value-of select="Params"/></xsl:if>) OF TYPE</m:mtext>
  91         </m:mrow>
  92        </m:mtd>
  93       </m:mtr>
  94       <m:mtr>
  95        <m:mtd>
  96         <m:mrow>
  97          <m:mphantom><m:mtext>__</m:mtext></m:mphantom>
  98          <xsl:apply-templates select="type/*[1]"/>
  99         </m:mrow>
 100        </m:mtd>
 101       </m:mtr>
 102       <m:mtr>
 103        <m:mtd>
 104         <m:mrow>
 105          <m:mtext>AS</m:mtext>
 106         </m:mrow>
 107        </m:mtd>
 108       </m:mtr>
 109       <m:mtr>
 110        <m:mtd>
 111         <m:mrow>
 112          <m:mphantom><m:mtext>__</m:mtext></m:mphantom>
 113          <xsl:apply-templates select="body/*[1]"/>
 114         </m:mrow>
 115        </m:mtd>
 116       </m:mtr>
 117      </m:mtable>
 118     </m:math>
 119 </xsl:template>
 120
 121 <!-- AXIOM -->
 122
 123 <xsl:template match="Axiom">
 124     <m:math>
 125      <m:mtable align="baseline 1" equalrows="false" columnalign="left" helm:xref="{@helm:xref}">
 126       <m:mtr>
 127        <m:mtd>
 128         <m:mrow>
 129          <m:mtext>AXIOM <xsl:value-of select="@name"/>(<xsl:if test="string(./Params) != &quot;&quot;"><xsl:value-of select="Params"/></xsl:if>) OF TYPE</m:mtext>
 130         </m:mrow>
 131        </m:mtd>
 132       </m:mtr>
 133       <m:mtr>
 134        <m:mtd>
 135         <m:mrow>
 136          <m:mphantom><m:mtext>__</m:mtext></m:mphantom>
 137          <xsl:apply-templates select="type/*[1]"/>
 138         </m:mrow>
 139        </m:mtd>
 140       </m:mtr>
 141      </m:mtable>
 142     </m:math>
 143 </xsl:template>
 144
 145 <!-- UNFINISHED PROOF -->
 146
 147 <xsl:template match="CurrentProof">
 148     <m:math>
 149      <m:mtable align="baseline 1" equalrows="false" columnalign="left" helm:xref="{@helm:xref}">
 150       <m:mtr>
 151        <m:mtd>
 152         <m:mrow>
 153          <m:mtext>UNFINISHED PROOF <xsl:value-of select="@name"/>(<xsl:if test="string(./Params) != &quot;&quot;"><xsl:value-of select="Params"/></xsl:if>)</m:mtext>
 154         </m:mrow>
 155        </m:mtd>
 156       </m:mtr>
 157       <m:mtr>
 158        <m:mtd>
 159         <m:mrow>
 160          <m:mtext>THESIS:</m:mtext>
 161         </m:mrow>
 162        </m:mtd>
 163       </m:mtr>
 164       <m:mtr>
 165        <m:mtd>
 166         <m:mrow>
 167          <m:mphantom><m:mtext>__</m:mtext></m:mphantom>
 168          <xsl:apply-templates select="type/*[1]"/>
 169         </m:mrow>
 170        </m:mtd>
 171       </m:mtr>
 172       <m:mtr>
 173        <m:mtd>
 174         <m:mrow>
 175          <m:mtext>CONJECTURES:</m:mtext>
 176         </m:mrow>
 177        </m:mtd>
 178       </m:mtr>
 179       <xsl:for-each select="Conjecture">
 180       <m:mtr>
 181        <m:mtd>
 182         <m:mrow>
 183          <m:mphantom><m:mtext>__</m:mtext></m:mphantom>
 184          <m:mtext><xsl:value-of select="./@no"/>:</m:mtext>
 185          <xsl:apply-templates select="./*[1]"/>
 186         </m:mrow>
 187        </m:mtd>
 188       </m:mtr>
 189       </xsl:for-each>
 190       <m:mtr>
 191        <m:mtd>
 192         <m:mrow>
 193          <m:mtext>CORRESPONDING PROOF:</m:mtext>
 194         </m:mrow>
 195        </m:mtd>
 196       </m:mtr>
 197       <m:mtr>
 198        <m:mtd>
 199         <m:mrow>
 200          <m:mphantom><m:mtext>__</m:mtext></m:mphantom>
 201          <xsl:apply-templates select="body/*[1]"/>
 202         </m:mrow>
 203        </m:mtd>
 204       </m:mtr>
 205      </m:mtable>
 206     </m:math>
 207 </xsl:template>
 208
 209 <!-- MUTUAL INDUCTIVE DEFINITION -->
 210
 211 <xsl:template match="InductiveDefinition">
 212     <m:math>
 213      <m:mtable align="baseline 1" equalrows="false" columnalign="left" helm:xref="{@helm:xref}">
 214      <xsl:for-each select="InductiveType">
 215       <m:mtr>
 216        <m:mtd>
 217         <m:mrow>
 218          <xsl:choose>
 219          <xsl:when test="position() = 1">
 220           <xsl:choose>
 221           <xsl:when test="string(./@inductive) = &quot;true&quot;">
 222            <m:mtext>INDUCTIVE DEFINITION</m:mtext>
 223           </xsl:when>
 224           <xsl:otherwise>
 225            <m:mtext>COINDUCTIVE DEFINITION</m:mtext>
 226           </xsl:otherwise>
 227           </xsl:choose>
 228          </xsl:when>
 229          <xsl:otherwise>
 230           <m:mtext>AND</m:mtext>
 231          </xsl:otherwise>
 232          </xsl:choose>
 233          <m:mphantom><m:mtext>_</m:mtext></m:mphantom>
 234          <m:mtext><xsl:value-of select="./@name"/>(<xsl:if test="string(../Params) != &quot;&quot;"><xsl:value-of select="../Params"/></xsl:if>)</m:mtext>
 235         </m:mrow>
 236        </m:mtd>
 237       </m:mtr>
 238       <m:mtr>
 239        <m:mtd>
 240         <m:mrow>
 241          <m:mphantom><m:mtext>__</m:mtext></m:mphantom>
 242          <m:mtext>[</m:mtext>
 243          <xsl:choose>
 244          <xsl:when test="string(../Param) != &quot;&quot;">
 245           <m:mtable align="baseline 1" equalrows="false" columnalign="left">
 246            <xsl:for-each select="../Param">
 247             <m:mtr>
 248              <m:mtd>
 249               <m:mrow>
 250                <m:mi><xsl:value-of select="./@name"/></m:mi>
 251                <m:mo>:</m:mo>
 252                <xsl:apply-templates select="*"/>
 253               </m:mrow>
 254              </m:mtd>
 255             </m:mtr>
 256            </xsl:for-each>
 257             <m:mtr>
 258              <m:mtd>
 259               <m:mrow>
 260                <m:mtext>]</m:mtext>
 261               </m:mrow>
 262              </m:mtd>
 263             </m:mtr>
 264           </m:mtable>
 265          </xsl:when>
 266          <xsl:otherwise>
 267           <m:mtext>]</m:mtext>
 268          </xsl:otherwise>
 269          </xsl:choose>
 270         </m:mrow>
 271        </m:mtd>
 272       </m:mtr>
 273       <m:mtr>
 274        <m:mtd>
 275         <m:mrow>
 276          <m:mtext>OF ARITY</m:mtext>
 277         </m:mrow>
 278        </m:mtd>
 279       </m:mtr>
 280       <m:mtr>
 281        <m:mtd>
 282         <m:mrow>
 283          <m:mphantom><m:mtext>__</m:mtext></m:mphantom>
 284          <xsl:apply-templates select="./arity/*[1]"/>
 285         </m:mrow>
 286        </m:mtd>
 287       </m:mtr>
 288       <m:mtr>
 289        <m:mtd>
 290         <m:mrow>
 291          <m:mtext>BUILT FROM</m:mtext>
 292         </m:mrow>
 293        </m:mtd>
 294       </m:mtr>
 295       <xsl:for-each select="./Constructor">
 296       <m:mtr>
 297        <m:mtd>
 298         <m:mrow>
 299          <xsl:choose>
 300          <xsl:when test="position() = 1">
 301           <m:mphantom><m:mtext>__</m:mtext></m:mphantom>
 302          </xsl:when>
 303          <xsl:otherwise>
 304           <m:mtext>|</m:mtext>
 305           <m:mphantom><m:mtext>_</m:mtext></m:mphantom>
 306          </xsl:otherwise>
 307          </xsl:choose>
 308          <m:mtext><xsl:value-of select="./@name"/> OF</m:mtext>
 309          <m:mphantom><m:mtext>_</m:mtext></m:mphantom>
 310          <xsl:apply-templates select="./*[1]"/>
 311         </m:mrow>
 312        </m:mtd>
 313       </m:mtr>
 314       </xsl:for-each>
 315      </xsl:for-each>
 316      </m:mtable>
 317     </m:math>
 318 </xsl:template>
 319
 320 <!-- VARIABLE -->
 321
 322 <xsl:template match="Variable">
 323     <m:math>
 324      <m:mtable align="baseline 1" equalrows="false" columnalign="left" helm:xref="{@helm:xref}">
 325       <m:mtr>
 326        <m:mtd>
 327         <m:mrow>
 328          <m:mtext>VARIABLE <xsl:value-of select="@name"/> OF TYPE</m:mtext>
 329         </m:mrow>
 330        </m:mtd>
 331       </m:mtr>
 332       <m:mtr>
 333        <m:mtd>
 334         <m:mrow>
 335          <m:mphantom><m:mtext>__</m:mtext></m:mphantom>
 336          <xsl:apply-templates select="type/*[1]"/>
 337         </m:mrow>
 338        </m:mtd>
 339       </m:mtr>
 340       <xsl:if test="name(*[1])='body'">
 341        <m:mtr>
 342         <m:mtd>
 343          <m:mrow>
 344           <m:mtext>AS</m:mtext>
 345          </m:mrow>
 346         </m:mtd>
 347        </m:mtr>
 348        <m:mtr>
 349         <m:mtd>
 350          <m:mrow>
 351           <m:mphantom><m:mtext>__</m:mtext></m:mphantom>
 352           <xsl:apply-templates select="body/*[1]"/>
 353          </m:mrow>
 354         </m:mtd>
 355        </m:mtr>
 356       </xsl:if>
 357      </m:mtable>
 358     </m:math>
 359 </xsl:template>
 360
 361 <!--**********************-->
 362 <!--        TERMS         -->
 363 <!--**********************-->
 364
 365 <xsl:template match="m:bvar">
 366  <xsl:choose>
 367   <xsl:when test="m:type">
 368    <xsl:variable name="charlength">
 369     <xsl:apply-templates select="m:ci" mode="charcount"/>
 370    </xsl:variable>
 371    <xsl:choose>
 372     <xsl:when test="$charlength >= $framewidth">
 373      <m:mtable align="baseline 1" equalrows="false" columnalign="left">
 374       <m:mtr>
 375        <m:mtd>
 376         <m:mrow>
 377          <xsl:apply-templates select="m:ci"/>
 378          <m:mo>:</m:mo>
 379         </m:mrow>
 380        </m:mtd>
 381       </m:mtr>
 382       <m:mtr>
 383        <m:mtd>
 384         <m:mrow>
 385          <xsl:apply-templates select="m:type"/>
 386         </m:mrow>
 387        </m:mtd>
 388       </m:mtr>
 389      </m:mtable>
 390     </xsl:when>
 391     <xsl:otherwise>
 392      <m:mrow>
 393       <xsl:apply-templates select="m:ci"/>
 394       <m:mo>:</m:mo>
 395       <xsl:apply-templates select="m:type"/>
 396      </m:mrow>
 397     </xsl:otherwise>
 398    </xsl:choose>
 399   </xsl:when>
 400   <xsl:otherwise>
 401    <xsl:apply-templates select="m:ci"/>
 402   </xsl:otherwise>
 403  </xsl:choose>
 404 </xsl:template>
 405
 406
 407 <!-- CSYMBOL -->
 408
 409 <xsl:template match="m:apply[m:csymbol]">
 410 <xsl:param name="nopar" select="0"/>
 411     <xsl:variable name="name"><xsl:value-of select="m:csymbol"/></xsl:variable>
 412     <xsl:variable name="charlength"><xsl:apply-templates select="m:csymbol" mode="charcount"/></xsl:variable>
 413     <m:mrow>
 414      <xsl:if test="@helm:xref">
 415       <xsl:attribute name="m:xref"><xsl:value-of select="@id"/></xsl:attribute>
 416      </xsl:if>
 417      <xsl:choose>
 418       <!-- FORALL -->
 419       <xsl:when test="$name='forall'">
 420        <xsl:choose>
 421        <xsl:when test="$charlength >= $framewidth">
 422         <m:mtable align="baseline 1" equalrows="false" columnalign="left">
 423          <m:mtr>
 424           <m:mtd>
 425            <m:mrow>
 426             <m:mo mathcolor="Blue">&#8704;</m:mo>
 427             <xsl:apply-templates select="m:bvar"/>
 428            </m:mrow>
 429           </m:mtd>
 430          </m:mtr>
 431          <m:mtr>
 432           <m:mtd>
 433            <m:mrow>
 434             <m:mo>.</m:mo>
 435             <xsl:apply-templates select="*[position()=3]"/>
 436            </m:mrow>
 437           </m:mtd>
 438          </m:mtr>
 439         </m:mtable>
 440        </xsl:when>
 441        <xsl:otherwise>
 442         <m:mo mathcolor="Blue">&#8704;</m:mo>
 443         <xsl:apply-templates select="m:bvar/m:ci"/>
 444         <m:mo>:</m:mo>
 445         <xsl:apply-templates select="m:bvar/m:type"/>
 446         <m:mo>.</m:mo>
 447         <xsl:apply-templates select="*[position()=3]"/>
 448        </xsl:otherwise>
 449        </xsl:choose>
 450       </xsl:when>
 451       <!-- LET-IN -->
 452       <xsl:when test="$name='let_in'">
 453        <xsl:choose>
 454        <xsl:when test="$charlength >= $framewidth">
 455         <m:mtable align="baseline 1" equalrows="false" columnalign="left">
 456          <m:mtr>
 457           <m:mtd>
 458            <m:mrow>
 459             <m:mo>LET</m:mo>
 460             <m:mphantom><m:mtext>_</m:mtext></m:mphantom>
 461             <xsl:apply-templates select="m:bvar"/>
 462            </m:mrow>
 463           </m:mtd>
 464          </m:mtr>
 465          <m:mtr>
 466           <m:mtd>
 467            <m:mrow>
 468             <m:mo>=</m:mo>
 469             <xsl:apply-templates select="*[position()=3]"/>
 470            </m:mrow>
 471           </m:mtd>
 472          </m:mtr>
 473          <m:mtr>
 474           <m:mtd>
 475            <m:mrow>
 476             <m:mo>IN</m:mo>
 477             <m:mphantom><m:mtext>_</m:mtext></m:mphantom>
 478             <xsl:apply-templates select="*[position()=4]"/>
 479            </m:mrow>
 480           </m:mtd>
 481          </m:mtr>
 482         </m:mtable>
 483        </xsl:when>
 484        <xsl:otherwise>
 485         <m:mo>LET</m:mo>
 486         <m:mphantom><m:mtext>_</m:mtext></m:mphantom>
 487         <xsl:apply-templates select="m:bvar/m:ci"/>
 488         <m:mo>=</m:mo>
 489         <xsl:apply-templates select="*[position()=3]"/>
 490         <m:mphantom><m:mtext>_</m:mtext></m:mphantom>
 491         <m:mtext>IN</m:mtext>
 492         <m:mphantom><m:mtext>_</m:mtext></m:mphantom>
 493         <xsl:apply-templates select="*[position()=4]"/>
 494        </xsl:otherwise>
 495        </xsl:choose>
 496       </xsl:when>
 497       <!-- PROD -->
 498       <xsl:when test="$name='prod'">
 499        <xsl:choose>
 500        <xsl:when test="$charlength >= $framewidth">
 501         <m:mtable align="baseline 1" equalrows="false" columnalign="left">
 502          <m:mtr>
 503           <m:mtd>
 504            <m:mrow>
 505             <m:mo mathcolor="Blue">&#x03a0;</m:mo>
 506             <xsl:apply-templates select="m:bvar"/>
 507            </m:mrow>
 508           </m:mtd>
 509          </m:mtr>
 510          <m:mtr>
 511           <m:mtd>
 512            <m:mrow>
 513             <m:mo>.</m:mo>
 514             <xsl:apply-templates select="*[position()=3]"/>
 515            </m:mrow>
 516           </m:mtd>
 517          </m:mtr>
 518         </m:mtable>
 519        </xsl:when>
 520        <xsl:otherwise>
 521         <m:mo mathcolor="Blue">&#x03a0;</m:mo>
 522         <xsl:apply-templates select="m:bvar/m:ci"/>
 523         <m:mo>:</m:mo>
 524         <xsl:apply-templates select="m:bvar/m:type"/>
 525         <m:mo>.</m:mo>
 526         <xsl:apply-templates select="*[position()=3]"/>
 527        </xsl:otherwise>
 528        </xsl:choose>
 529       </xsl:when>
 530       <!-- ARROW -->
 531       <xsl:when test="$name='arrow'">
 532        <xsl:choose>
 533        <xsl:when test="$charlength >= $framewidth">
 534         <m:mtable align="baseline 1" equalrows="false" columnalign="left">
 535          <m:mtr>
 536           <m:mtd>
 537            <m:mrow>
 538             <xsl:if test="$nopar=0">
 539              <m:mo stretchy="false">(</m:mo>
 540             </xsl:if>
 541             <xsl:apply-templates select="*[position()=2]"/>
 542            </m:mrow>
 543           </m:mtd>
 544          </m:mtr>
 545          <m:mtr>
 546           <m:mtd>
 547            <m:mrow>
 548             <m:mo mathmathcolor="Blue">&#x2192;</m:mo>
 549             <xsl:choose>
 550             <xsl:when test="*[position()=3]/m:csymbol">
 551              <xsl:variable name="nextp"><xsl:value-of select="*[position()=3]/m:csymbol"/></xsl:variable>
 552              <xsl:choose>
 553              <xsl:when test="$nextp='arrow'">
 554               <xsl:apply-templates select="*[position()=3]"><xsl:with-param name="nopar" select="1"/></xsl:apply-templates>
 555              </xsl:when>
 556              <xsl:otherwise>
 557               <xsl:apply-templates select="*[position()=3]"/>
 558              </xsl:otherwise>
 559              </xsl:choose>
 560             </xsl:when>
 561             <xsl:otherwise>
 562              <xsl:apply-templates select="*[position()=3]"/>
 563             </xsl:otherwise>
 564             </xsl:choose>
 565            </m:mrow>
 566           </m:mtd>
 567          </m:mtr>
 568          <xsl:if test="$nopar=0">
 569          <m:mtr>
 570           <m:mtd>
 571            <m:mrow>
 572             <m:mo stretchy="false">)</m:mo>
 573            </m:mrow>
 574           </m:mtd>
 575          </m:mtr>
 576          </xsl:if>
 577         </m:mtable>
 578        </xsl:when>
 579        <xsl:otherwise>
 580         <xsl:if test="$nopar=0">
 581          <m:mo stretchy="false">(</m:mo>
 582         </xsl:if>
 583         <xsl:apply-templates select="*[position()=2]"/>
 584         <m:mo mathcolor="Blue">&#x2192;</m:mo>
 585         <xsl:choose>
 586         <xsl:when test="*[position()=3]/m:csymbol">
 587          <xsl:variable name="nextp"><xsl:value-of select="*[position()=3]/m:csymbol"/></xsl:variable>
 588          <xsl:choose>
 589          <xsl:when test="$nextp='arrow'">
 590           <xsl:apply-templates select="*[position()=3]"><xsl:with-param name="nopar" select="1"/></xsl:apply-templates>
 591          </xsl:when>
 592          <xsl:otherwise>
 593           <xsl:apply-templates select="*[position()=3]"/>
 594          </xsl:otherwise>
 595          </xsl:choose>
 596         </xsl:when>
 597         <xsl:otherwise>
 598          <xsl:apply-templates select="*[position()=3]"/>
 599         </xsl:otherwise>
 600         </xsl:choose>
 601         <xsl:if test="$nopar=0">
 602          <m:mo stretchy="false">)</m:mo>
 603         </xsl:if>
 604        </xsl:otherwise>
 605        </xsl:choose>
 606       </xsl:when>
 607       <!-- APP -->
 608       <xsl:when test="$name='app'">
 609        <xsl:choose>
 610        <xsl:when test="$charlength >= $framewidth">
 611         <m:mtable align="baseline 1" equalrows="false" columnalign="left">
 612          <m:mtr>
 613           <m:mtd>
 614            <m:mrow>
 615             <m:mo stretchy="false">(</m:mo>
 616             <xsl:apply-templates select="*[position()=2]"/>
 617            </m:mrow>
 618           </m:mtd>
 619          </m:mtr>
 620          <xsl:for-each select="*[position()>2]">
 621          <m:mtr>
 622           <m:mtd>
 623            <m:mrow>
 624             <m:mphantom><m:mtext>(</m:mtext></m:mphantom>
 625             <xsl:apply-templates select="."/>
 626            </m:mrow>
 627           </m:mtd>
 628          </m:mtr>
 629          </xsl:for-each>
 630          <m:mtr>
 631           <m:mtd>
 632            <m:mrow>
 633             <m:mo stretchy="false">)</m:mo>
 634            </m:mrow>
 635           </m:mtd>
 636          </m:mtr>
 637         </m:mtable>
 638        </xsl:when>
 639        <xsl:otherwise>
 640         <m:mo stretchy="false">(</m:mo>
 641         <xsl:apply-templates select="*[position()=2]"/>
 642         <xsl:for-each select="*[position()>2]">
 643          <m:mphantom><m:mtext>_</m:mtext></m:mphantom>
 644          <xsl:apply-templates select="."/>
 645         </xsl:for-each>
 646         <m:mo stretchy="false">)</m:mo>
 647        </xsl:otherwise>
 648        </xsl:choose>
 649       </xsl:when>
 650       <!-- CAST -->
 651       <xsl:when test="$name='cast'">
 652        <xsl:choose>
 653        <xsl:when test="$charlength >= $framewidth">
 654         <m:mtable align="baseline 1" equalrows="false" columnalign="left">
 655          <m:mtr>
 656           <m:mtd>
 657            <m:mrow>
 658             <m:mo stretchy="false">(</m:mo>
 659             <xsl:apply-templates select="*[position()=2]"/>
 660            </m:mrow>
 661           </m:mtd>
 662          </m:mtr>
 663          <m:mtr>
 664           <m:mtd>
 665            <m:mrow>
 666             <m:mo mathcolor="Maroon">:></m:mo>
 667             <xsl:apply-templates select="*[position()=3]"/>
 668            </m:mrow>
 669           </m:mtd>
 670          </m:mtr>
 671          <m:mtr>
 672           <m:mtd>
 673            <m:mrow>
 674             <m:mo stretchy="false">)</m:mo>
 675            </m:mrow>
 676           </m:mtd>
 677          </m:mtr>
 678         </m:mtable>
 679        </xsl:when>
 680        <xsl:otherwise>
 681         <m:mo stretchy="false">(</m:mo>
 682         <xsl:apply-templates select="*[position()=2]"/>
 683         <m:mo mathcolor="Maroon">:></m:mo>
 684         <xsl:apply-templates select="*[position()=3]"/>
 685         <m:mo stretchy="false">)</m:mo>
 686        </xsl:otherwise>
 687        </xsl:choose>
 688       </xsl:when>
 689       <!-- PROP -->
 690       <xsl:when test="$name='Prop'">
 691        <m:mo>Prop</m:mo>
 692       </xsl:when>
 693       <!-- SET -->
 694       <xsl:when test="$name='Set'">
 695        <m:mo>Set</m:mo>
 696       </xsl:when>
 697       <!-- TYPE -->
 698       <xsl:when test="$name='Type'">
 699        <m:mo>Type</m:mo>
 700       </xsl:when>
 701       <!-- MUTCASE -->
 702       <xsl:when test="$name='mutcase'">
 703        <xsl:choose>
 704        <xsl:when test="$charlength >= $framewidth">
 705         <xsl:variable name="charlength"><xsl:apply-templates select="*[position()=2]" mode="charcount"><xsl:with-param name="nosibling" select="1"/></xsl:apply-templates></xsl:variable>
 706         <m:mtable align="baseline 1" equalrows="false" columnalign="left">
 707          <m:mtr>
 708           <m:mtd>
 709            <m:mrow>
 710             <m:mo>&lt;</m:mo>
 711             <xsl:apply-templates select="*[position()=2]"/>
 712             <xsl:if test="$framewidth > $charlength">
 713              <m:mo>&gt;</m:mo>
 714              <m:mo>CASES</m:mo>
 715              <m:mphantom><m:mtext>_</m:mtext></m:mphantom>
 716              <xsl:apply-templates select="*[position()=3]"/>
 717             </xsl:if>
 718            </m:mrow>
 719           </m:mtd>
 720          </m:mtr>
 721          <xsl:if test="$charlength >= $framewidth">
 722          <m:mtr>
 723           <m:mtd>
 724            <m:mrow>
 725             <m:mo>&gt;</m:mo>
 726             <m:mo>CASES</m:mo>
 727             <m:mphantom><m:mtext>_</m:mtext></m:mphantom>
 728             <xsl:apply-templates select="*[position()=3]"/>
 729            </m:mrow>
 730           </m:mtd>
 731          </m:mtr>
 732          </xsl:if>
 733          <m:mtr>
 734           <m:mtd>
 735            <m:mrow>
 736             <m:mo>OF</m:mo>
 737            </m:mrow>
 738           </m:mtd>
 739          </m:mtr>
 740          <xsl:for-each select="piecewise/piece">
 741          <xsl:variable name="charlength"><xsl:apply-templates select="./*[2]" mode="charcount"><xsl:with-param name="nosibling" select="1"/></xsl:apply-templates></xsl:variable>
 742          <m:mtr>
 743           <m:mtd>
 744            <m:mrow>
 745             <xsl:choose>
 746             <xsl:when test="position() = 1">
 747               <m:mphantom><m:mtext>|</m:mtext></m:mphantom>
 748             </xsl:when>
 749             <xsl:otherwise>
 750              <m:mo stretchy="false">|</m:mo>
 751             </xsl:otherwise>
 752             </xsl:choose>
 753             <m:mphantom><m:mtext>_</m:mtext></m:mphantom>
 754             <xsl:apply-templates select="./*[2]"/>
 755             <xsl:if test="$framewidth > $charlength">
 756              <m:mo mathcolor="Green">&#x21d2;</m:mo>
 757              <xsl:apply-templates select="./*[1]"/>
 758             </xsl:if>
 759            </m:mrow>
 760           </m:mtd>
 761          </m:mtr>
 762          <xsl:if test="$charlength >= $framewidth">
 763          <m:mtr>
 764           <m:mtd>
 765            <m:mrow>
 766             <m:mphantom><m:mtext>|_</m:mtext></m:mphantom>
 767             <m:mo mathcolor="Green">&#x21d2;</m:mo>
 768             <xsl:apply-templates select="./*[1]"/>
 769            </m:mrow>
 770           </m:mtd>
 771          </m:mtr>
 772          </xsl:if>
 773         </xsl:for-each>
 774          <m:mtr>
 775           <m:mtd>
 776            <m:mrow>
 777             <m:mo>END</m:mo>
 778            </m:mrow>
 779           </m:mtd>
 780          </m:mtr>
 781         </m:mtable>
 782        </xsl:when>
 783        <xsl:otherwise>
 784         <m:mo>&lt;</m:mo><xsl:apply-templates select="*[position()=2]"/><m:mo>&gt;</m:mo>
 785         <m:mo>CASES</m:mo>
 786         <m:mphantom><m:mtext>_</m:mtext></m:mphantom>
 787         <xsl:apply-templates select="*[position()=3]"/>
 788         <m:mphantom><m:mtext>_</m:mtext></m:mphantom>
 789         <m:mo>OF</m:mo>
 790         <xsl:for-each select="piecewise/piece">
 791          <xsl:choose>
 792          <xsl:when test="position() != 1">
 793           <m:mo stretchy="false">|</m:mo>
 794          </xsl:when>
 795          </xsl:choose>
 796          <xsl:apply-templates select="./*[2]"/>
 797          <m:mo mathcolor="Green">&#x21d2;</m:mo>
 798          <xsl:apply-templates select="./*[1]"/>
 799         </xsl:for-each>
 800         <m:mphantom><m:mtext>_</m:mtext></m:mphantom>
 801         <m:mo>END</m:mo>
 802        </xsl:otherwise>
 803        </xsl:choose>
 804       </xsl:when>
 805       <!-- FIX -->
 806       <xsl:when test="$name='fix'">
 807        <xsl:choose>
 808        <xsl:when test="$charlength >= $framewidth">
 809         <m:mtable align="baseline 1" equalrows="false" columnalign="left">
 810          <m:mtr>
 811           <m:mtd>
 812            <m:mrow>
 813             <m:mo>FIX</m:mo>
 814             <m:mphantom><m:mtext>_</m:mtext></m:mphantom>
 815             <m:mi><xsl:value-of select="m:ci"/></m:mi>
 816             <m:mo stretchy="false">{</m:mo>
 817            </m:mrow>
 818           </m:mtd>
 819          </m:mtr>
 820          <m:mtr>
 821           <m:mtd>
 822            <m:mrow>
 823             <m:mphantom><m:mtext>__</m:mtext></m:mphantom>
 824             <m:mtable align="baseline 1" equalrows="false" columnalign="left">
 825             <xsl:for-each select="m:bvar">
 826              <xsl:variable name="charlength"><xsl:apply-templates select="m:type" mode="charcount"><xsl:with-param name="nosibling" select="1"/></xsl:apply-templates></xsl:variable>
 827              <m:mtr>
 828               <m:mtd>
 829                <m:mrow>
 830                 <m:mi><xsl:value-of select="m:ci"/></m:mi>
 831                 <m:mo>:</m:mo>
 832                 <xsl:if test="$framewidth > $charlength">
 833                  <xsl:apply-templates select="m:type"/>
 834                 </xsl:if>
 835                </m:mrow>
 836               </m:mtd>
 837              </m:mtr>
 838              <xsl:if test="$charlength >= $framewidth">
 839              <m:mtr>
 840               <m:mtd>
 841                <m:mrow>
 842                 <m:mphantom><m:mtext>:=</m:mtext></m:mphantom>
 843                 <xsl:apply-templates select="m:type"/>
 844                </m:mrow>
 845               </m:mtd>
 846              </m:mtr>
 847              </xsl:if>
 848              <m:mtr>
 849               <m:mtd>
 850                <m:mrow>
 851                 <m:mo>:=</m:mo>
 852                 <xsl:apply-templates select="following-sibling::*[position()=1]"/>
 853                </m:mrow>
 854               </m:mtd>
 855              </m:mtr>
 856             </xsl:for-each>
 857             </m:mtable>
 858            </m:mrow>
 859           </m:mtd>
 860          </m:mtr>
 861          <m:mtr>
 862           <m:mtd>
 863            <m:mrow>
 864             <m:mo stretchy="false">}</m:mo>
 865            </m:mrow>
 866           </m:mtd>
 867          </m:mtr>
 868         </m:mtable>
 869        </xsl:when>
 870        <xsl:otherwise>
 871         <m:mo>FIX</m:mo>
 872         <m:mi><xsl:value-of select="m:ci"/></m:mi>
 873         <m:mo stretchy="false">{</m:mo>
 874         <m:mtable align="baseline 1" equalrows="false" columnalign="left">
 875         <xsl:for-each select="m:bvar">
 876          <m:mtr>
 877           <m:mtd>
 878            <m:mrow>
 879             <m:mi><xsl:value-of select="m:ci"/></m:mi>
 880             <m:mo>:</m:mo>
 881             <xsl:apply-templates select="m:type"/>
 882             <m:mo>:=</m:mo>
 883             <xsl:apply-templates select="following-sibling::*[position() = 1]"/>
 884             <xsl:if test="position()=last()">
 885              <m:mo stretchy="false">}</m:mo>
 886             </xsl:if>
 887            </m:mrow>
 888           </m:mtd>
 889          </m:mtr>
 890          </xsl:for-each>
 891         </m:mtable>
 892        </xsl:otherwise>
 893        </xsl:choose>
 894       </xsl:when>
 895       <!-- COFIX -->
 896       <xsl:when test="$name='cofix'">
 897        <xsl:choose>
 898        <xsl:when test="$charlength >= $framewidth">
 899         <m:mtable align="baseline 1" equalrows="false" columnalign="left">
 900          <m:mtr>
 901           <m:mtd>
 902            <m:mrow>
 903             <m:mo>COFIX</m:mo>
 904             <m:mphantom><m:mtext>_</m:mtext></m:mphantom>
 905             <m:mi><xsl:value-of select="m:ci"/></m:mi>
 906             <m:mo stretchy="false">{</m:mo>
 907            </m:mrow>
 908           </m:mtd>
 909          </m:mtr>
 910          <m:mtr>
 911           <m:mtd>
 912            <m:mrow>
 913             <m:mphantom><m:mtext>__</m:mtext></m:mphantom>
 914             <m:mtable align="baseline 1" equalrows="false" columnalign="left">
 915             <xsl:for-each select="m:bvar">
 916              <xsl:variable name="charlength"><xsl:apply-templates select="m:type" mode="charcount"><xsl:with-param name="nosibling" select="1"/></xsl:apply-templates></xsl:variable>
 917              <m:mtr>
 918               <m:mtd>
 919                <m:mrow>
 920                 <m:mi><xsl:value-of select="m:ci"/></m:mi>
 921                 <m:mo>:</m:mo>
 922                 <xsl:if test="$framewidth > $charlength">
 923                  <xsl:apply-templates select="m:type"/>
 924                 </xsl:if>
 925                </m:mrow>
 926               </m:mtd>
 927              </m:mtr>
 928              <xsl:if test="$charlength >= $framewidth">
 929              <m:mtr>
 930               <m:mtd>
 931                <m:mrow>
 932                 <m:mphantom><m:mtext>:=</m:mtext></m:mphantom>
 933                 <xsl:apply-templates select="m:type"/>
 934                </m:mrow>
 935               </m:mtd>
 936              </m:mtr>
 937              </xsl:if>
 938              <m:mtr>
 939               <m:mtd>
 940                <m:mrow>
 941                 <m:mo>:=</m:mo>
 942                 <xsl:apply-templates select="following-sibling::*[position() = 1]"/>
 943                </m:mrow>
 944               </m:mtd>
 945              </m:mtr>
 946             </xsl:for-each>
 947             </m:mtable>
 948            </m:mrow>
 949           </m:mtd>
 950          </m:mtr>
 951          <m:mtr>
 952           <m:mtd>
 953            <m:mrow>
 954             <m:mo stretchy="false">}</m:mo>
 955            </m:mrow>
 956           </m:mtd>
 957          </m:mtr>
 958         </m:mtable>
 959        </xsl:when>
 960        <xsl:otherwise>
 961         <m:mo>COFIX</m:mo>
 962         <m:mi><xsl:value-of select="m:ci"/></m:mi>
 963         <m:mo stretchy="false">{</m:mo>
 964         <m:mtable align="baseline 1" equalrows="false" columnalign="left">
 965         <xsl:for-each select="m:bvar">
 966          <m:mtr>
 967           <m:mtd>
 968            <m:mrow>
 969             <m:mi><xsl:value-of select="m:ci"/></m:mi>
 970             <m:mo>:</m:mo>
 971             <xsl:apply-templates select="m:type"/>
 972             <m:mo>:=</m:mo>
 973             <xsl:apply-templates select="following-sibling::*[position() = 1]"/>
 974             <xsl:if test="position()=last()">
 975              <m:mo stretchy="false">}</m:mo>
 976             </xsl:if>
 977            </m:mrow>
 978           </m:mtd>
 979          </m:mtr>
 980          </xsl:for-each>
 981         </m:mtable>
 982        </xsl:otherwise>
 983        </xsl:choose>
 984       </xsl:when>
 985       <!-- ***************************************** -->
 986       <!-- *********** PROOF ELEMENTS ************** -->
 987       <!-- ***************************************** -->
 988       <!-- PROOF -->
 989       <xsl:when test="$name='proof'">
 990        <m:maction actiontype="toggle">
 991         <!-- CSC: next if until the annotationHelper can handle mactions -->
 992         <xsl:if test="not($explodeall)">
 993          <!-- Details hided (default) -->
 994          <m:mtable align="baseline 1" equalrows="false" columnalign="left">
 995           <m:mtr>
 996            <m:mtd>
 997             <m:mrow>
 998              <m:mtext mathcolor="Maroon">We&#x00a0;can&#x00a0;prove</m:mtext>
 999              <m:mphantom><m:mtext>_</m:mtext></m:mphantom>
1000              <xsl:apply-templates select="*[position()=3]"/>
1001              <m:mrow>
1002               <m:mphantom><m:mtext>_</m:mtext></m:mphantom>
1003               <m:mtext mathcolor="Green">(explain)</m:mtext>
1004              </m:mrow>
1005             </m:mrow>
1006            </m:mtd>
1007           </m:mtr>
1008          </m:mtable>
1009         </xsl:if>
1010         <!-- Show details -->
1011         <m:mtable align="baseline 1" equalrows="false" columnalign="left">
1012          <m:mtr>
1013           <m:mtd>
1014            <m:mrow>
1015             <xsl:apply-templates select="*[position()=2]"/>
1016            </m:mrow>
1017           </m:mtd>
1018          </m:mtr>
1019          <m:mtr>
1020           <m:mtd>
1021            <m:mrow>
1022             <m:mtext mathcolor="Maroon">we&#x00a0;proved</m:mtext>
1023             <m:mphantom><m:mtext>_</m:mtext></m:mphantom>
1024             <xsl:apply-templates select="*[position()=3]"/>
1025             <m:mrow>
1026              <m:mphantom>
1027               <m:mtext>_</m:mtext>
1028              </m:mphantom>
1029              <m:mtext mathcolor="Green">(hide&#x00a0;details)</m:mtext>
1030             </m:mrow>
1031            </m:mrow>
1032           </m:mtd>
1033          </m:mtr>
1034         </m:mtable>
1035        </m:maction>
1036       </xsl:when>
1037       <!-- LETIN1 -->
1038       <xsl:when test="$name='letin1'">
1039         <m:mtable align="baseline 1" equalrows="false" columnalign="left">
1040          <m:mtr>
1041           <m:mtd>
1042            <m:mrow>
1043             <xsl:apply-templates select="*[2]"/>
1044            </m:mrow>
1045           </m:mtd>
1046          </m:mtr>
1047          <m:mtr>
1048           <m:mtd>
1049            <m:mrow>
1050             <xsl:apply-templates select="*[3]"/>
1051            </m:mrow>
1052           </m:mtd>
1053          </m:mtr>
1054         </m:mtable>
1055       </xsl:when>
1056       <xsl:when test="$name='by_induction'">
1057        <m:mtable align="baseline 1" equalrows="false" columnalign="left">
1058         <m:mtr>
1059          <m:mtd>
1060           <m:mrow>
1061            <m:mtext mathcolor="red">We&#x00a0;prove</m:mtext>
1062            <m:mphantom><m:mtext>_</m:mtext></m:mphantom>
1063            <xsl:apply-templates select="../*[3]"/>
1064           </m:mrow>
1065          </m:mtd>
1066         </m:mtr>
1067         <m:mtr>
1068          <m:mtd>
1069           <m:mrow>
1070            <m:mtext mathcolor="red">by&#x00a0;induction&#x00a0;on</m:mtext>
1071            <m:mphantom><m:mtext>_</m:mtext></m:mphantom>
1072            <xsl:apply-templates
1073             select="*[position()=last()]/*[position()=last()]"/>
1074           </m:mrow>
1075          </m:mtd>
1076         </m:mtr>
1077         <m:mtr>
1078          <m:mtd>
1079           <m:mrow>
1080            <m:mtable align="baseline 1" equalrows="false" columnalign="left">
1081             <xsl:for-each select="*[position()>3 and not(position()=last())]">
1082              <m:mtr>
1083               <m:mtd>
1084                <m:mrow>
1085                 <xsl:apply-templates select="."/>
1086                </m:mrow>
1087               </m:mtd>
1088              </m:mtr>
1089             </xsl:for-each>
1090            </m:mtable>
1091           </m:mrow>
1092          </m:mtd>
1093         </m:mtr>
1094        </m:mtable>
1095       </xsl:when>
1096       <!-- inductive_case -->
1097       <xsl:when test="$name='inductive_case'">
1098        <m:mtable align="baseline 1" equalrows="false" columnalign="left">
1099         <m:mtr>
1100          <m:mtd>
1101           <m:mrow>
1102            <m:mtext mathcolor="red">Case</m:mtext>
1103            <m:mphantom><m:mtext>_</m:mtext></m:mphantom>
1104            <xsl:apply-templates select="*[2]"/>
1105           </m:mrow>
1106          </m:mtd>
1107         </m:mtr>
1108         <m:mtr>
1109          <m:mtd>
1110           <m:mrow>
1111            <m:mphantom><m:mtext>_</m:mtext></m:mphantom>
1112            <m:mtable align="baseline 1" equalrows="false" columnalign="left">
1113             <xsl:if test="*[3]/*[position()>1]">
1114              <m:mtr>
1115               <m:mtd>
1116                <m:mrow>
1117                 <m:mtext mathcolor="red">By&#x00a0;induction&#x00a0;hypothesis,&#x00a0;we&#x00a0;have:</m:mtext>
1118                </m:mrow>
1119               </m:mtd>
1120              </m:mtr>
1121              <m:mtr>
1122               <m:mtd>
1123                <m:mrow>
1124                 <m:mphantom><m:mtext>_</m:mtext></m:mphantom>
1125                 <xsl:for-each select="*[3]/*[position()>1]">
1126                  <m:mo stretchy="false">(</m:mo>
1127                  <xsl:apply-templates select="m:ci"/>
1128                  <m:mo stretchy="false">) </m:mo>
1129                  <m:mphantom><m:mtext>_</m:mtext></m:mphantom>
1130                  <xsl:apply-templates select="m:type"/>
1131                 </xsl:for-each>
1132                </m:mrow>
1133               </m:mtd>
1134              </m:mtr>
1135             </xsl:if>
1136             <m:mtr>
1137              <m:mtd>
1138               <m:mrow>
1139                <xsl:apply-templates select="*[4]"/>
1140               </m:mrow>
1141              </m:mtd>
1142             </m:mtr>
1143            </m:mtable>
1144           </m:mrow>
1145          </m:mtd>
1146         </m:mtr>
1147        </m:mtable>
1148       </xsl:when>
1149       <!-- case_lhs  -->
1150       <xsl:when test="$name='case_lhs'">
1151        <m:mrow>
1152         <xsl:choose>
1153          <xsl:when test="count(*)=2">
1154           <xsl:apply-templates select="*[2]"/>
1155          </xsl:when>
1156          <xsl:otherwise>
1157           <m:mo stretchy="false">(</m:mo>
1158           <xsl:apply-templates select="*[2]"/>
1159           <xsl:for-each select="m:bvar">
1160            <m:mphantom><m:mtext>_</m:mtext></m:mphantom>
1161            <xsl:apply-templates select="*[1]"/>
1162            <m:mtext>:</m:mtext>
1163            <xsl:apply-templates select="m:type/*[1]"/>
1164           </xsl:for-each>
1165           <m:mo stretchy="false">)</m:mo>
1166          </xsl:otherwise>
1167         </xsl:choose>
1168        </m:mrow>
1169       </xsl:when>
1170       <!-- false_ind  -->
1171       <xsl:when test="$name='false_ind'">
1172        <m:mtable align="baseline 1" equalrows="false" columnalign="left">
1173         <m:mtr>
1174          <m:mtd>
1175           <m:mrow>
1176            <xsl:apply-templates select="*[3]"/>
1177           </m:mrow>
1178          </m:mtd>
1179         </m:mtr>
1180         <m:mtr>
1181          <m:mtd>
1182           <m:mrow>
1183            <m:mtext mathcolor="Red">Contradiction.</m:mtext>
1184           </m:mrow>
1185          </m:mtd>
1186         </m:mtr>
1187        </m:mtable>
1188       </xsl:when>
1189       <!-- LET-IN -->
1190       <xsl:when test="$name='letin'">
1191         <m:mtable align="baseline 1" equalrows="false" columnalign="left">
1192          <!-- <xsl:for-each select="APPLY[m:csymbol and (string(m:csymbol)='let')]"> -->
1193          <xsl:for-each select="*[(last() > position()) and (position()>1)]">
1194          <m:mtr>
1195           <m:mtd>
1196            <m:mrow>
1197             <xsl:apply-templates select="."/>
1198            </m:mrow>
1199           </m:mtd>
1200          </m:mtr>
1201          </xsl:for-each>
1202          <m:mtr>
1203           <m:mtd>
1204            <m:mrow>
1205             <xsl:apply-templates select="*[position()=last()]"/>
1206            </m:mrow>
1207           </m:mtd>
1208          </m:mtr>
1209         </m:mtable>
1210       </xsl:when>
1211       <!-- LET -->
1212       <xsl:when test="$name='let'">
1213        <m:mtext>(</m:mtext>
1214        <xsl:apply-templates select="m:ci"/>
1215        <m:mtext>) </m:mtext>
1216        <xsl:apply-templates select="*[3]"/>
1217       </xsl:when>
1218       <!-- RW_STEP -->
1219       <xsl:when test="$name='rw_step'">
1220         <m:mtable align="baseline 1" equalrows="false" columnalign="left">
1221          <m:mtr>
1222           <m:mtd>
1223            <m:mrow>
1224             <xsl:choose>
1225              <xsl:when test="name(*[2])='m:apply'">
1226               <xsl:apply-templates select="*[2]"/>
1227              </xsl:when>
1228              <xsl:otherwise>
1229               <m:mtext>Consider</m:mtext>
1230               <m:mphantom><m:mtext>_</m:mtext></m:mphantom>
1231               <xsl:apply-templates select="*[2]"/>
1232              </xsl:otherwise>
1233             </xsl:choose>
1234            </m:mrow>
1235           </m:mtd>
1236          </m:mtr>
1237          <m:mtr>
1238           <m:mtd>
1239            <m:mrow>
1240             <m:mtext>Rewrite</m:mtext>
1241             <m:mphantom><m:mtext>_</m:mtext></m:mphantom>
1242             <xsl:apply-templates select="*[3]"/>
1243             <m:mphantom><m:mtext>_</m:mtext></m:mphantom>
1244             <m:mtext>with</m:mtext>
1245             <m:mphantom><m:mtext>_</m:mtext></m:mphantom>
1246             <xsl:apply-templates select="*[4]"/>
1247             <m:mphantom><m:mtext>_</m:mtext></m:mphantom>
1248             <m:mtext>by</m:mtext>
1249             <m:mphantom><m:mtext>_</m:mtext></m:mphantom>
1250             <xsl:apply-templates select="*[5]"/>
1251            </m:mrow>
1252           </m:mtd>
1253          </m:mtr>
1254         </m:mtable>
1255       </xsl:when>
1256       <!-- not existing any more
1257       <xsl:when test="$name='thread'">
1258         <m:mtable align="baseline 1" equalrows="false" columnalign="left">
1259          <m:mtr>
1260           <m:mtd>
1261            <m:mrow>
1262             <xsl:choose>
1263              <xsl:when test="name(*[last()])='m:apply'">
1264               <xsl:apply-templates select="*[last()]"/>
1265              </xsl:when>
1266              <xsl:otherwise>
1267               <m:mtext>Consider</m:mtext>
1268               <m:mphantom><m:mtext>_</m:mtext></m:mphantom>
1269               <xsl:apply-templates select="*[last()]"/>
1270              </xsl:otherwise>
1271             </xsl:choose>
1272            </m:mrow>
1273           </m:mtd>
1274          </m:mtr>
1275          <xsl:apply-templates mode="thread" select="*[(last()-2)]"/>
1276         </m:mtable>
1277       </xsl:when>
1278       -->
1279       <!-- REWRITE_AND_APPLY -->
1280       <xsl:when test="$name='rewrite_and_apply'">
1281         <m:mtable align="baseline 1" equalrows="false" columnalign="left">
1282          <m:mtr>
1283           <m:mtd>
1284            <m:mrow>
1285             <xsl:apply-templates select="*[2]"/>
1286            </m:mrow>
1287           </m:mtd>
1288          </m:mtr>
1289          <m:mtr>
1290           <m:mtd>
1291            <m:mrow>
1292             <m:mtext>Then&#x00a0;apply&#x00a0;it&#x00a0;to</m:mtext>
1293             <m:mphantom><m:mtext>_</m:mtext></m:mphantom>
1294             <xsl:apply-templates select="*[position()>2]"/>
1295            </m:mrow>
1296           </m:mtd>
1297          </m:mtr>
1298        </m:mtable>
1299       </xsl:when>
1300       <!-- AND_IND -->
1301       <xsl:when test="$name='and_ind'">
1302         <m:mtable align="baseline 1" equalrows="false" columnalign="left">
1303          <m:mtr>
1304           <m:mtd>
1305            <m:mrow>
1306             <xsl:choose>
1307              <xsl:when test="name(*[2])='m:apply'">
1308               <xsl:apply-templates select="*[2]"/>
1309              </xsl:when>
1310              <xsl:otherwise>
1311               <m:mtext>Consider</m:mtext>
1312               <m:mphantom><m:mtext>_</m:mtext></m:mphantom>
1313               <xsl:apply-templates select="*[2]"/>
1314              </xsl:otherwise>
1315             </xsl:choose>
1316            </m:mrow>
1317           </m:mtd>
1318          </m:mtr>
1319          <m:mtr>
1320           <m:mtd>
1321            <m:mrow>
1322             <m:mtext>In&#x00a0;particular,&#x00a0;we&#x00a0;have</m:mtext>
1323            </m:mrow>
1324           </m:mtd>
1325          </m:mtr>
1326          <m:mtr>
1327           <m:mtd>
1328            <m:mrow>
1329             <m:mtext>(</m:mtext>
1330             <xsl:apply-templates select="*[3]"/>
1331             <m:mtext>)</m:mtext>
1332             <m:mphantom><m:mtext>_</m:mtext></m:mphantom>
1333             <xsl:apply-templates select="*[4]"/>
1334             </m:mrow>
1335           </m:mtd>
1336          </m:mtr>
1337          <m:mtr>
1338           <m:mtd>
1339            <m:mrow>
1340             <m:mtext>(</m:mtext>
1341             <xsl:apply-templates select="*[5]"/>
1342             <m:mtext>)</m:mtext>
1343             <m:mphantom><m:mtext>_</m:mtext></m:mphantom>
1344             <xsl:apply-templates select="*[6]"/>
1345             </m:mrow>
1346           </m:mtd>
1347          </m:mtr>
1348          <m:mtr>
1349           <m:mtd>
1350            <m:mrow>
1351             <xsl:apply-templates select="*[7]"/>
1352            </m:mrow>
1353           </m:mtd>
1354          </m:mtr>
1355         </m:mtable>
1356       </xsl:when>
1357       <!-- full_or_ind -->
1358       <xsl:when test="$name='full_or_ind'">
1359         <m:mtable align="baseline 1" equalrows="false" columnalign="left">
1360          <m:mtr>
1361           <m:mtd>
1362            <m:mrow>
1363             <xsl:choose>
1364              <xsl:when test="name(*[2])='m:apply'">
1365               <xsl:apply-templates select="*[2]"/>
1366              </xsl:when>
1367              <xsl:otherwise>
1368               <m:mtext>Consider</m:mtext>
1369               <m:mphantom><m:mtext>_</m:mtext></m:mphantom>
1370               <xsl:apply-templates select="*[2]"/>
1371              </xsl:otherwise>
1372             </xsl:choose>
1373            </m:mrow>
1374           </m:mtd>
1375          </m:mtr>
1376          <m:mtr>
1377           <m:mtd>
1378            <m:mrow>
1379             <m:mtext>We&#x00a0;proceed&#x00a0;by&#x00a0;cases&#x00a0;to&#x00a0;prove</m:mtext>
1380             <m:mphantom><m:mtext>_</m:mtext></m:mphantom>
1381             <xsl:apply-templates select="*[3]"/>
1382            </m:mrow>
1383           </m:mtd>
1384          </m:mtr>
1385          <m:mtr>
1386           <m:mtd>
1387            <m:mrow>
1388             <m:mtext>Left:&#x00a0;suppose</m:mtext>
1389             <m:mphantom><m:mtext>_</m:mtext></m:mphantom>
1390             <m:mo stretchy="false">(</m:mo>
1391             <xsl:apply-templates select="*[4]/m:bvar/m:ci"/>
1392             <m:mo stretchy="false">)</m:mo>
1393             <m:mphantom><m:mtext>_</m:mtext></m:mphantom>
1394             <xsl:apply-templates select="*[4]/m:bvar/m:type/*[1]"/>
1395            </m:mrow>
1396           </m:mtd>
1397          </m:mtr>
1398          <m:mtr>
1399           <m:mtd>
1400            <m:mrow>
1401             <m:mphantom><m:mtext>_</m:mtext></m:mphantom>
1402             <xsl:apply-templates select="*[4]/*[3]"/>
1403            </m:mrow>
1404           </m:mtd>
1405          </m:mtr>
1406          <m:mtr>
1407           <m:mtd>
1408            <m:mrow>
1409             <m:mtext>Right:&#x00a0;suppose</m:mtext>
1410             <m:mphantom><m:mtext>_</m:mtext></m:mphantom>
1411             <m:mo stretchy="false">(</m:mo>
1412             <xsl:apply-templates select="*[5]/m:bvar/m:ci"/>
1413             <m:mo stretchy="false">)</m:mo>
1414             <m:mphantom><m:mtext>_</m:mtext></m:mphantom>
1415             <xsl:apply-templates select="*[5]/m:bvar/m:type/*[1]"/>
1416            </m:mrow>
1417           </m:mtd>
1418          </m:mtr>
1419          <m:mtr>
1420           <m:mtd>
1421            <m:mrow>
1422             <xsl:apply-templates select="*[5]/*[3]"/>
1423            </m:mrow>
1424           </m:mtd>
1425          </m:mtr>
1426         </m:mtable>
1427       </xsl:when>
1428       <!-- OR_IND -->
1429       <xsl:when test="$name='or_ind'">
1430         <m:mtable align="baseline 1" equalrows="false" columnalign="left">
1431          <m:mtr>
1432           <m:mtd>
1433            <m:mrow>
1434             <xsl:choose>
1435              <xsl:when test="name(*[2])='m:apply'">
1436               <xsl:apply-templates select="*[2]"/>
1437              </xsl:when>
1438              <xsl:otherwise>
1439               <m:mtext>Consider</m:mtext>
1440               <m:mphantom><m:mtext>_</m:mtext></m:mphantom>
1441               <xsl:apply-templates select="*[2]"/>
1442              </xsl:otherwise>
1443             </xsl:choose>
1444            </m:mrow>
1445           </m:mtd>
1446          </m:mtr>
1447          <m:mtr>
1448           <m:mtd>
1449            <m:mrow>
1450             <m:mtext>We&#x00a0;prove</m:mtext>
1451             <m:mphantom><m:mtext>_</m:mtext></m:mphantom>
1452             <xsl:apply-templates select="*[3]"/>
1453             <m:mphantom><m:mtext>_</m:mtext></m:mphantom>
1454             <m:mtext>by&#x00a0;cases:</m:mtext>
1455            </m:mrow>
1456           </m:mtd>
1457          </m:mtr>
1458          <m:mtr>
1459           <m:mtd>
1460            <m:mrow>
1461             <m:mtext>Left</m:mtext>
1462             <xsl:apply-templates select="*[4]"/>
1463            </m:mrow>
1464           </m:mtd>
1465          </m:mtr>
1466          <m:mtr>
1467           <m:mtd>
1468            <m:mrow>
1469             <m:mtext>Right</m:mtext>
1470             <xsl:apply-templates select="*[5]"/>
1471            </m:mrow>
1472           </m:mtd>
1473          </m:mtr>
1474         </m:mtable>
1475       </xsl:when>
1476       <!-- EX_IND -->
1477       <xsl:when test="$name='ex_ind'">
1478         <m:mtable align="baseline 1" equalrows="false" columnalign="left">
1479          <m:mtr>
1480           <m:mtd>
1481            <m:mrow>
1482             <xsl:choose>
1483              <xsl:when test="name(*[2])='m:apply'">
1484               <xsl:apply-templates select="*[2]"/>
1485              </xsl:when>
1486              <xsl:otherwise>
1487               <m:mtext>Consider</m:mtext>
1488               <m:mphantom><m:mtext>_</m:mtext></m:mphantom>
1489               <xsl:apply-templates select="*[2]"/>
1490              </xsl:otherwise>
1491             </xsl:choose>
1492            </m:mrow>
1493           </m:mtd>
1494          </m:mtr>
1495          <m:mtr>
1496           <m:mtd>
1497            <m:mrow>
1498             <m:mtext>Let</m:mtext>
1499             <m:mphantom><m:mtext>_</m:mtext></m:mphantom>
1500             <xsl:apply-templates select="*[3]"/>
1501             <m:mtext>:</m:mtext>
1502             <xsl:apply-templates select="*[4]"/>
1503             <m:mphantom><m:mtext>_</m:mtext></m:mphantom>
1504             <m:mtext>such&#x00a0;that</m:mtext>
1505             <m:mphantom><m:mtext>_</m:mtext></m:mphantom>
1506             <m:mtext>(</m:mtext>
1507              <xsl:apply-templates select="*[5]"/>
1508             <m:mtext>)</m:mtext>
1509             <m:mphantom><m:mtext>_</m:mtext></m:mphantom>
1510             <xsl:apply-templates select="*[6]"/>
1511            </m:mrow>
1512           </m:mtd>
1513          </m:mtr>
1514          <m:mtr>
1515           <m:mtd>
1516            <m:mrow>
1517             <xsl:apply-templates select="*[7]"/>
1518            </m:mrow>
1519           </m:mtd>
1520          </m:mtr>
1521         </m:mtable>
1522       </xsl:when>
1523       <!-- ***************************************** -->
1524       <!-- *********** NOTATIONS ******************* -->
1525       <!-- ***************************************** -->
1526       <!-- subst -->
1527       <xsl:when test="$name='subst'">
1528         <xsl:apply-templates select="*[3]"/>
1529         <m:mo>&#xe8a0;</m:mo>
1530         <m:mrow>
1531          <m:mo stretchy="false">[</m:mo>
1532          <m:mrow>
1533           <xsl:apply-templates select="*[4]"/>
1534           <m:mo mathcolor="green">
1535            <xsl:if test="$id != ''">
1536             <xsl:attribute name="m:xref"><xsl:value-of select="$id"/></xsl:attribute>
1537            </xsl:if>&#8592;</m:mo>
1538           <xsl:apply-templates select="*[2]"/>
1539          </m:mrow>
1540          <m:mo stretchy="false">]</m:mo>
1541         </m:mrow>
1542       </xsl:when>
1543       <!-- lift -->
1544       <xsl:when test="$name='lift'">
1545         <m:msup>
1546          <m:mo mathcolor="green">
1547           <xsl:if test="$id != ''">
1548            <xsl:attribute name="m:xref"><xsl:value-of select="$id"/></xsl:attribute>
1549           </xsl:if>&#8593;</m:mo>
1550          <xsl:apply-templates select="*[2]"/>
1551         </m:msup>
1552         <m:mrow>
1553          <m:mo stretchy="false">(</m:mo>
1554          <xsl:apply-templates select="*[3]"/>
1555          <m:mo stretchy="false">)</m:mo>
1556         </m:mrow>
1557       </xsl:when>
1558       <!-- lift_with_base -->
1559       <xsl:when test="$name='lift_with_base'">
1560         <m:msubsup>
1561          <m:mo mathcolor="green">
1562           <xsl:if test="$id != ''">
1563            <xsl:attribute name="m:xref"><xsl:value-of select="$id"/></xsl:attribute>
1564           </xsl:if>&#8593;</m:mo>
1565          <xsl:apply-templates select="*[3]"/>
1566          <xsl:apply-templates select="*[4]"/>
1567         </m:msubsup>
1568         <m:mrow>
1569          <m:mo stretchy="false">(</m:mo>
1570          <xsl:apply-templates select="*[2]"/>
1571          <m:mo stretchy="false">)</m:mo>
1572         </m:mrow>
1573       </xsl:when>
1574       <!-- beta_red1 -->
1575       <xsl:when test="$name='beta_red1'">
1576         <xsl:apply-templates select="*[2]"/>
1577         <m:munder>
1578          <m:mo mathcolor="green">
1579           <xsl:if test="$id != ''">
1580            <xsl:attribute name="m:xref"><xsl:value-of select="$id"/></xsl:attribute>
1581           </xsl:if>&#8594;</m:mo>
1582           <m:mi mathcolor="green">&#946;</m:mi>
1583         </m:munder>
1584         <xsl:apply-templates select="*[3]"/>
1585       </xsl:when>
1586       <!-- beta_red -->
1587       <xsl:when test="$name='beta_red'">
1588         <xsl:apply-templates select="*[2]"/>
1589         <m:munderover>
1590          <m:mo mathcolor="green">
1591           <xsl:if test="$id != ''">
1592            <xsl:attribute name="m:xref"><xsl:value-of select="$id"/></xsl:attribute>
1593           </xsl:if>&#8594;</m:mo>
1594           <m:mi mathcolor="green">&#946;</m:mi>
1595           <m:mi mathcolor="green">*</m:mi>
1596         </m:munderover>
1597         <xsl:apply-templates select="*[3]"/>
1598       </xsl:when>
1599       <!-- par_beta_red1 -->
1600       <xsl:when test="$name='par_beta_red1'">
1601         <xsl:apply-templates select="*[2]"/>
1602         <m:munder>
1603          <m:mo mathcolor="green">
1604           <xsl:if test="$id != ''">
1605            <xsl:attribute name="m:xref"><xsl:value-of select="$id"/></xsl:attribute>
1606           </xsl:if>&#8658;</m:mo>
1607           <m:mi mathcolor="green">&#946;</m:mi>
1608         </m:munder>
1609         <xsl:apply-templates select="*[3]"/>
1610       </xsl:when>
1611       <!-- par_beta_red -->
1612       <xsl:when test="$name='par_beta_red'">
1613         <xsl:apply-templates select="*[2]"/>
1614         <m:munderover>
1615          <m:mo mathcolor="green">
1616           <xsl:if test="$id != ''">
1617            <xsl:attribute name="m:xref"><xsl:value-of select="$id"/></xsl:attribute>
1618           </xsl:if>&#8658;</m:mo>
1619           <m:mi mathcolor="green">&#946;</m:mi>
1620           <m:mi mathcolor="green">*</m:mi>
1621         </m:munderover>
1622         <xsl:apply-templates select="*[3]"/>
1623       </xsl:when>
1624       <!-- forgetful -->
1625       <xsl:when test="$name='forgetful'">
1626        <m:mfenced open="|" close="|">
1627         <xsl:if test="$id != ''">
1628          <xsl:attribute name="m:xref"><xsl:value-of select="$id"/></xsl:attribute>
1629         </xsl:if>
1630         <xsl:apply-templates select="*[2]"/>
1631        </m:mfenced>
1632       </xsl:when>
1633       <!-- isomorphic -->
1634       <xsl:when test="$name='isomorphic'">
1635         <xsl:apply-templates select="*[2]"/>
1636         <m:mo mathcolor="green">
1637          <xsl:if test="$id != ''">
1638           <xsl:attribute name="m:xref"><xsl:value-of select="$id"/></xsl:attribute>
1639          </xsl:if>&#8773;</m:mo>
1640         <xsl:apply-templates select="*[3]"/>
1641       </xsl:when>
1642       <!-- interp -->
1643       <xsl:when test="$name='forgetful'">
1644        <m:mfenced open="[" close="]">
1645         <xsl:if test="$id != ''">
1646          <xsl:attribute name="m:xref"><xsl:value-of select="$id"/></xsl:attribute>
1647         </xsl:if>
1648         <xsl:apply-templates select="*[2]"/>
1649        </m:mfenced>
1650       </xsl:when>
1651
1652       <!-- ERROR -->
1653       <xsl:otherwise>
1654        <m:mi>ERROR</m:mi>
1655       </xsl:otherwise>
1656      </xsl:choose>
1657     </m:mrow>
1658 </xsl:template>
1659
1660 <!-- Il modo Thread non esiste piu'
1661 <xsl:template match="*" mode="thread">
1662  <xsl:variable name="name"><xsl:value-of select="following-sibling::*[position()=1]/m:csymbol"/></xsl:variable>
1663  <xsl:choose>
1664   <xsl:when test="$name='rw_step'">
1665          <m:mtr>
1666           <m:mtd>
1667            <m:mrow>
1668             <m:mtext>Rewrite</m:mtext>
1669             <m:mphantom><m:mtext>_</m:mtext></m:mphantom>
1670             <xsl:apply-templates select="following-sibling::*[position()=1]/*[2]"/>
1671             <m:mphantom><m:mtext>_</m:mtext></m:mphantom>
1672             <m:mtext>with</m:mtext>
1673             <m:mphantom><m:mtext>_</m:mtext></m:mphantom>
1674             <xsl:apply-templates select="following-sibling::*[position()=1]/*[3]"/>
1675             <m:mphantom><m:mtext>_</m:mtext></m:mphantom>
1676             <m:mtext>by</m:mtext>
1677             <m:mphantom><m:mtext>_</m:mtext></m:mphantom>
1678             <xsl:apply-templates select="following-sibling::*[position()=1]/*[4]"/>
1679            </m:mrow>
1680           </m:mtd>
1681          </m:mtr>
1682          <m:mtr>
1683           <m:mtd>
1684            <m:mrow>
1685             <m:mtext mathcolor="Maroon">we&#x00a0;get</m:mtext>
1686             <m:mphantom><m:mtext>_</m:mtext></m:mphantom>
1687             <xsl:apply-templates select="."/>
1688            </m:mrow>
1689           </m:mtd>
1690          </m:mtr>
1691    </xsl:when>
1692    <xsl:otherwise>
1693          <m:mtr>
1694           <m:mtd>
1695            <m:mrow>
1696             <xsl:apply-templates select="following-sibling::*[position()=1]"/>
1697            </m:mrow>
1698           </m:mtd>
1699          </m:mtr>
1700          <m:mtr>
1701           <m:mtd>
1702            <m:mrow>
1703             <m:mtext mathcolor="Maroon">we&#x00a0;get</m:mtext>
1704             <m:mphantom><m:mtext>_</m:mtext></m:mphantom>
1705             <xsl:apply-templates select="."/>
1706            </m:mrow>
1707           </m:mtd>
1708          </m:mtr>
1709     </xsl:otherwise>
1710    </xsl:choose>
1711          <xsl:apply-templates mode="thread" select="preceding-sibling::*[position()=2]"/>
1712 </xsl:template>
1713 -->
1714
1715 <!-- LAMBDA -->
1716
1717 <xsl:template match="m:lambda">
1718     <xsl:variable name="charlength"><xsl:apply-templates select="*[position()=1]" mode="charcount"/></xsl:variable>
1719     <m:mrow m:xref="{@id}">
1720      <xsl:choose>
1721      <xsl:when test="$charlength >= $framewidth">
1722       <m:mtable align="baseline 1" equalrows="false" columnalign="left">
1723         <m:mtr>
1724           <m:mtd>
1725            <m:mrow>
1726             <m:mo mathcolor="Red">&#x03bb;</m:mo>
1727             <xsl:apply-templates select="m:bvar"/>
1728            </m:mrow>
1729           </m:mtd>
1730          </m:mtr>
1731        <m:mtr>
1732         <m:mtd>
1733          <m:mrow>
1734           <m:mo>.</m:mo>
1735           <xsl:apply-templates select="*[position()=2]"/>
1736          </m:mrow>
1737         </m:mtd>
1738        </m:mtr>
1739       </m:mtable>
1740      </xsl:when>
1741      <xsl:otherwise>
1742       <m:mo mathcolor="Red">&#x03bb;</m:mo>
1743       <xsl:apply-templates select="m:bvar/m:ci"/>
1744       <m:mo>:</m:mo>
1745       <xsl:apply-templates select="m:bvar/m:type"/>
1746       <m:mo>.</m:mo>
1747       <xsl:apply-templates select="*[position()=2]"/>
1748      </xsl:otherwise>
1749      </xsl:choose>
1750     </m:mrow>
1751 </xsl:template>
1752
1753 <!-- *********************************** -->
1754 <!-- BASE SET OF MATHML CONTENT ELEMENTS -->
1755 <!-- *********************************** -->
1756
1757 <!-- Logic -->
1758
1759 <xsl:template match = "m:apply[m:eq[1]]">
1760  <xsl:variable name="charlength">
1761   <xsl:apply-templates select="*[1]" mode="charcount"/>
1762  </xsl:variable>
1763  <xsl:choose>
1764   <xsl:when test="$charlength >= $framewidth">
1765    <m:mtable align="baseline 1" equalrows="false" columnalign="left">
1766     <xsl:if test="@helm:xref">
1767      <xsl:attribute name="m:xref">
1768       <xsl:value-of select="@id"/>
1769      </xsl:attribute>
1770     </xsl:if>
1771     <m:mtr>
1772      <m:mtd>
1773       <m:mrow>
1774        <m:mo stretchy="false">(</m:mo>
1775        <xsl:apply-templates select="*[position()=2]"/>
1776       </m:mrow>
1777      </m:mtd>
1778     </m:mtr>
1779     <xsl:for-each select = "*[position()>2]">
1780      <m:mtr>
1781       <m:mtd>
1782        <m:mrow>
1783         <m:mphantom><m:mtext>__</m:mtext></m:mphantom>
1784         <m:mo m:xref="{m:in/@id}">=</m:mo>
1785         <xsl:apply-templates select="."/>
1786        </m:mrow>
1787       </m:mtd>
1788      </m:mtr>
1789     </xsl:for-each>
1790     <m:mtr>
1791      <m:mtd>
1792       <m:mrow>
1793        <m:mo stretchy="false">)</m:mo>
1794       </m:mrow>
1795      </m:mtd>
1796     </m:mtr>
1797    </m:mtable>
1798   </xsl:when>
1799   <xsl:otherwise>
1800    <xsl:apply-imports/>
1801   </xsl:otherwise>
1802  </xsl:choose>
1803 </xsl:template>
1804
1805
1806 <xsl:template match = "m:apply[m:and[1]|m:or[1]
1807           |m:geq[1]|m:leq[1]|m:gt[1]|m:lt[1]
1808           |m:in[1]|m:intesect[1]|m:union[1]|m:subset[1]
1809           |m:prsubset|m:setdiff[1]]">
1810  <xsl:variable name="symbol">
1811   <xsl:choose>
1812    <xsl:when test="m:and[1]">
1813     <xsl:value-of select="'&#8743;'"/>
1814    </xsl:when>
1815    <xsl:when test="m:or[1]">
1816     <xsl:value-of select="'&#8744;'"/>
1817    </xsl:when>
1818    <xsl:when test="m:geq[1]">
1819     <xsl:value-of select="'&#8805;'"/>
1820    </xsl:when>
1821    <xsl:when test="m:leq[1]">
1822     <xsl:value-of select="'&#8804;'"/>
1823    </xsl:when>
1824    <xsl:when test="m:gt[1]">
1825     <xsl:value-of select="'&#62;'"/>
1826    </xsl:when>
1827    <xsl:when test="m:lt[1]">
1828     <xsl:value-of select="'&#60;&#32;'"/>
1829    </xsl:when>
1830    <xsl:when test="m:eq[1]">
1831     <xsl:value-of select="'&#61;'"/>
1832    </xsl:when>
1833    <xsl:when test="m:in[1]">
1834     <xsl:value-of select="'&#x02208;'"/>
1835    </xsl:when>
1836    <xsl:when test="m:subset[1]">
1837     <xsl:value-of select="'&#x02286;'"/>
1838    </xsl:when>
1839    <xsl:when test="m:prsubset[1]">
1840     <xsl:value-of select="'&#x02282;'"/>
1841    </xsl:when>
1842    <xsl:when test="m:intersect[1]">
1843     <xsl:value-of select="'&#x022C2;'"/>
1844    </xsl:when>
1845    <xsl:when test="m:union[1]">
1846     <xsl:value-of select="'&#x022C3;'"/>
1847    </xsl:when>
1848    <xsl:when test="m:setdiff[1]">
1849     <xsl:value-of select="'&#x02216;'"/>
1850    </xsl:when>
1851   </xsl:choose>
1852  </xsl:variable>
1853  <xsl:variable name="charlength">
1854   <xsl:apply-templates select="*[1]" mode="charcount"/>
1855  </xsl:variable>
1856  <xsl:choose>
1857   <xsl:when test="$charlength >= $framewidth">
1858    <m:mtable align="baseline 1" equalrows="false" columnalign="left">
1859     <xsl:if test="@helm:xref">
1860      <xsl:attribute name="m:xref">
1861       <xsl:value-of select="@id"/>
1862      </xsl:attribute>
1863     </xsl:if>
1864     <m:mtr>
1865      <m:mtd>
1866       <m:mrow>
1867        <m:mo stretchy="false">(</m:mo>
1868        <xsl:apply-templates select="*[position()=2]"/>
1869       </m:mrow>
1870      </m:mtd>
1871     </m:mtr>
1872     <xsl:for-each select = "*[position()>2]">
1873      <m:mtr>
1874       <m:mtd>
1875        <m:mrow>
1876         <m:mphantom><m:mtext>__</m:mtext></m:mphantom>
1877         <m:mo m:xref="{*[1]/@id}"><xsl:value-of select="$symbol"/></m:mo>
1878         <xsl:apply-templates select="."/>
1879        </m:mrow>
1880       </m:mtd>
1881      </m:mtr>
1882     </xsl:for-each>
1883     <m:mtr>
1884      <m:mtd>
1885       <m:mrow>
1886        <m:mo stretchy="false">)</m:mo>
1887       </m:mrow>
1888      </m:mtd>
1889     </m:mtr>
1890    </m:mtable>
1891   </xsl:when>
1892   <xsl:otherwise>
1893    <xsl:apply-imports/>
1894   </xsl:otherwise>
1895  </xsl:choose>
1896 </xsl:template>
1897
1898 <xsl:template match = "m:set">
1899  <xsl:choose>
1900   <xsl:when test="count(child::*) = 0">
1901    <m:mi>&#x02205;</m:mi>
1902   </xsl:when>
1903   <xsl:otherwise>
1904    <xsl:variable name="charlength">
1905     <xsl:apply-templates select="*[1]" mode="charcount"/>
1906    </xsl:variable>
1907    <xsl:choose>
1908     <xsl:when test="$charlength >= $framewidth">
1909      <xsl:choose>
1910       <xsl:when test="name(*[1]) = 'm:bvar'">
1911        <m:mtable align="baseline 1" equalrows="false" columnalign="left">
1912         <m:mtr>
1913          <m:mtd>
1914           <m:mrow>
1915            <m:mo stretchy="false">{</m:mo>
1916            <xsl:apply-templates select="*[position()=1]"/>
1917           </m:mrow>
1918          </m:mtd>
1919         </m:mtr>
1920         <m:mtr>
1921          <m:mtd>
1922           <m:mrow>
1923            <m:mphantom><m:mtext>{</m:mtext></m:mphantom>
1924            <m:mo stretchy="false">|</m:mo>
1925            <xsl:apply-templates select="m:condition/*[1]"/>
1926           </m:mrow>
1927          </m:mtd>
1928         </m:mtr>
1929         <m:mtr>
1930          <m:mtd>
1931           <m:mrow>
1932            <m:mo stretchy="false">}</m:mo>
1933           </m:mrow>
1934          </m:mtd>
1935         </m:mtr>
1936        </m:mtable>
1937       </xsl:when>
1938       <xsl:otherwise>
1939        <m:mtable align="baseline 1" equalrows="false" columnalign="left">
1940         <m:mtr>
1941          <m:mtd>
1942           <m:mrow>
1943            <m:mo stretchy="false">{</m:mo>
1944            <xsl:apply-templates select="*[position()=1]"/>
1945            <xsl:if test="position() != last()">
1946             <mo>,</mo>
1947            </xsl:if>
1948           </m:mrow>
1949          </m:mtd>
1950         </m:mtr>
1951         <xsl:for-each select = "*[position()>2]">
1952          <m:mtr>
1953           <m:mtd>
1954            <m:mrow>
1955             <m:mphantom><m:mtext>{</m:mtext></m:mphantom>
1956             <xsl:apply-templates select="."/>
1957             <xsl:if test="position() != last()">
1958              <mo>,</mo>
1959             </xsl:if>
1960            </m:mrow>
1961           </m:mtd>
1962          </m:mtr>
1963         </xsl:for-each>
1964         <m:mtr>
1965          <m:mtd>
1966           <m:mrow>
1967            <m:mo stretchy="false">}</m:mo>
1968           </m:mrow>
1969          </m:mtd>
1970         </m:mtr>
1971        </m:mtable>
1972       </xsl:otherwise>
1973      </xsl:choose>
1974     </xsl:when>
1975     <xsl:otherwise>
1976      <xsl:apply-imports/>
1977     </xsl:otherwise>
1978    </xsl:choose>
1979   </xsl:otherwise>
1980  </xsl:choose>
1981 </xsl:template>
1982
1983 <xsl:template match = "m:apply[m:card[1]]">
1984   <m:mfenced open="|" close="|" stretchy="false">
1985     <xsl:if test="($SEM_SW=$SEM_XREF or $SEM_SW=$SEM_XREF_EXT) and @id">
1986       <xsl:attribute name="m:xref">
1987         <xsl:value-of select="@id"/>
1988       </xsl:attribute>
1989     </xsl:if>
1990   <xsl:apply-templates select="*[2]"/>
1991   </m:mfenced>
1992 </xsl:template>
1993
1994 <!-- *********************************** -->
1995 <!--          PROOF ELEMENTS             -->
1996 <!-- *********************************** -->
1997
1998
1999
2000 <!--**********************-->
2001 <!--       COUNTING       -->
2002 <!--**********************-->
2003
2004 <xsl:template match="m:cn|m:and|m:or|m:not|m:exists|m:eq|m:lt|m:leq|m:gt|m:geq
2005  |m:in|m:notin|m:intersect|m:union|m:subset|m:prsubset|m:card|m:setdiff
2006  |m:plus|m:minus|m:times" mode="charcount">
2007 <xsl:param name="incurrent_length" select="0"/>
2008     <xsl:choose>
2009     <xsl:when test="$framewidth > ($incurrent_length + 3 + string-length())">
2010      <xsl:variable name="siblength">
2011       <xsl:apply-templates select="following-sibling::*[position()=1]" mode="charcount">
2012        <xsl:with-param name="incurrent_length" select="$incurrent_length + string-length()"/>
2013       </xsl:apply-templates>
2014      </xsl:variable>
2015      <xsl:choose>
2016      <xsl:when test="string($siblength) = &quot;&quot;">
2017       <xsl:value-of select="$incurrent_length + 3 + string-length()"/>
2018      </xsl:when>
2019      <xsl:otherwise>
2020       <xsl:value-of select="number($siblength)"/>
2021      </xsl:otherwise>
2022      </xsl:choose>
2023     </xsl:when>
2024     <xsl:otherwise>
2025      <xsl:value-of select="$incurrent_length + 3 + string-length()"/>
2026     </xsl:otherwise>
2027     </xsl:choose>
2028 </xsl:template>
2029
2030 <xsl:template match="m:ci|m:csymbol" mode="charcount">
2031 <xsl:param name="incurrent_length" select="0"/>
2032 <xsl:param name="nosibling" select="0"/>
2033     <xsl:choose>
2034     <xsl:when test="$framewidth > ($incurrent_length + string-length()) and ($nosibling = 0)">
2035      <xsl:variable name="siblength"><xsl:apply-templates select="following-sibling::*[position()=1]" mode="charcount"><xsl:with-param name="incurrent_length" select="$incurrent_length + string-length()"/></xsl:apply-templates></xsl:variable>
2036      <xsl:choose>
2037      <xsl:when test="string($siblength) = &quot;&quot;">
2038       <xsl:value-of select="$incurrent_length + string-length()"/>
2039      </xsl:when>
2040      <xsl:otherwise>
2041       <xsl:value-of select="number($siblength)"/>
2042      </xsl:otherwise>
2043      </xsl:choose>
2044     </xsl:when>
2045     <xsl:otherwise>
2046      <xsl:value-of select="$incurrent_length + string-length()"/>
2047     </xsl:otherwise>
2048     </xsl:choose>
2049 </xsl:template>
2050
2051 <xsl:template match="*" mode="charcount">
2052 <xsl:param name="incurrent_length" select="0"/>
2053 <xsl:param name="nosibling" select="0"/>
2054  <xsl:choose>
2055   <xsl:when test="count(child::*) = 0">
2056    <xsl:value-of select="$incurrent_length"/>
2057   </xsl:when>
2058   <xsl:otherwise>
2059     <xsl:variable name="childlength"><xsl:apply-templates select="*[position()=1]" mode="charcount"><xsl:with-param name="incurrent_length" select="$incurrent_length"/><xsl:with-param name="nosibling" select="0"/></xsl:apply-templates></xsl:variable>
2060     <xsl:choose>
2061     <xsl:when test="$framewidth > number($childlength) and ($nosibling = 0)">
2062      <xsl:variable name="siblength"><xsl:apply-templates select="following-sibling::*[position()=1]" mode="charcount"><xsl:with-param name="incurrent_length" select="$childlength"/></xsl:apply-templates></xsl:variable>
2063      <xsl:choose>
2064      <xsl:when test="string($siblength) = &quot;&quot;">
2065       <xsl:value-of select="number($childlength)"/>
2066      </xsl:when>
2067      <xsl:otherwise>
2068       <xsl:value-of select="number($siblength)"/>
2069      </xsl:otherwise>
2070      </xsl:choose>
2071     </xsl:when>
2072     <xsl:otherwise>
2073      <xsl:value-of select="number($childlength)"/>
2074     </xsl:otherwise>
2075     </xsl:choose>
2076   </xsl:otherwise>
2077  </xsl:choose>
2078 </xsl:template>
2079
2080 </xsl:stylesheet>