helm/style/mmlextension.xsl

   1 <?xml version="1.0"?>
   2
   3 <!--***********************************************************************-->
   4 <!-- Extension to the XSLT version 0.07 of MathML content to presentation: -->
   5 <!-- First draft: February 19 2000, Andrea Asperti, Irene Schena           -->
   6 <!-- Revised: March 3 2000, Irene Schena                                   -->
   7 <!-- Revised: March 15 2000, Claudio Sacerdoti Coen, Irene Schena          -->
   8 <!-- Revised: March 21 2000, Irene Schena                                  -->
   9 <!--***********************************************************************-->
  10
  11 <xsl:stylesheet version="1.0" xmlns:xsl="http://www.w3.org/1999/XSL/Transform"
  12                               xmlns:m="http://www.w3.org/1998/Math/MathML"
  13                               xmlns:helm="http://www.cs.unibo.it/helm">
  14
  15 <xsl:import href="mml2mmlv1_0.xsl"/>
  16
  17 <!--***********************************************************************-->
  18 <!-- Parameter affecting line-breaking                                     -->
  19 <!--***********************************************************************-->
  20
  21 <xsl:variable name="framewidth" select="35"/>
  22
  23 <!--***********************************************************************-->
  24 <!-- Gli oggetti sono stampati come mtext all'interno di una marca toplevel-->
  25 <!-- math ma al di fuori di semantics. Ora vi sono tanti semantics quanti  -->
  26 <!-- sono i termini: la presentation per un termine e' generata come primo -->
  27 <!-- figlio di un semantics e l'originario content viene inserito nel      -->
  28 <!-- nel secondo figlio di semantics, annotation-xml                       -->
  29 <!--***********************************************************************-->
  30
  31 <!--**********************-->
  32 <!--        OBJECTS       -->
  33 <!--**********************-->
  34
  35 <xsl:template match="/">
  36  <xsl:processing-instruction name="cocoon-format">type="text/xhtml"</xsl:processing-instruction>
  37  <xsl:apply-templates select="*"/>
  38 </xsl:template>
  39
  40 <!-- DEFINITION -->
  41
  42 <xsl:template match="Definition">
  43     <m:math>
  44      <m:mtable align="baseline 1" equalrows="false" columnalign="left" helm:xref="{@helm:xref}">
  45       <m:mtr>
  46        <m:mtd>
  47         <m:mrow>
  48          <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>
  49         </m:mrow>
  50        </m:mtd>
  51       </m:mtr>
  52       <m:mtr>
  53        <m:mtd>
  54         <m:mrow>
  55          <m:mphantom><m:mtext>__</m:mtext></m:mphantom>
  56          <xsl:apply-templates select="type/*[1]"/>
  57         </m:mrow>
  58        </m:mtd>
  59       </m:mtr>
  60       <m:mtr>
  61        <m:mtd>
  62         <m:mrow>
  63          <m:mtext>AS</m:mtext>
  64         </m:mrow>
  65        </m:mtd>
  66       </m:mtr>
  67       <m:mtr>
  68        <m:mtd>
  69         <m:mrow>
  70          <m:mphantom><m:mtext>__</m:mtext></m:mphantom>
  71          <xsl:apply-templates select="body/*[1]"/>
  72         </m:mrow>
  73        </m:mtd>
  74       </m:mtr>
  75      </m:mtable>
  76     </m:math>
  77 </xsl:template>
  78
  79 <!-- AXIOM -->
  80
  81 <xsl:template match="Axiom">
  82     <m:math>
  83      <m:mtable align="baseline 1" equalrows="false" columnalign="left" helm:xref="{@helm:xref}">
  84       <m:mtr>
  85        <m:mtd>
  86         <m:mrow>
  87          <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>
  88         </m:mrow>
  89        </m:mtd>
  90       </m:mtr>
  91       <m:mtr>
  92        <m:mtd>
  93         <m:mrow>
  94          <m:mphantom><m:mtext>__</m:mtext></m:mphantom>
  95          <xsl:apply-templates select="type/*[1]"/>
  96         </m:mrow>
  97        </m:mtd>
  98       </m:mtr>
  99      </m:mtable>
 100     </m:math>
 101 </xsl:template>
 102
 103 <!-- UNFINISHED PROOF -->
 104
 105 <xsl:template match="CurrentProof">
 106     <m:math>
 107      <m:mtable align="baseline 1" equalrows="false" columnalign="left" helm:xref="{@helm:xref}">
 108       <m:mtr>
 109        <m:mtd>
 110         <m:mrow>
 111          <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>
 112         </m:mrow>
 113        </m:mtd>
 114       </m:mtr>
 115       <m:mtr>
 116        <m:mtd>
 117         <m:mrow>
 118          <m:mtext>THESIS:</m:mtext>
 119         </m:mrow>
 120        </m:mtd>
 121       </m:mtr>
 122       <m:mtr>
 123        <m:mtd>
 124         <m:mrow>
 125          <m:mphantom><m:mtext>__</m:mtext></m:mphantom>
 126          <xsl:apply-templates select="type/*[1]"/>
 127         </m:mrow>
 128        </m:mtd>
 129       </m:mtr>
 130       <m:mtr>
 131        <m:mtd>
 132         <m:mrow>
 133          <m:mtext>CONJECTURES:</m:mtext>
 134         </m:mrow>
 135        </m:mtd>
 136       </m:mtr>
 137       <xsl:for-each select="Conjecture">
 138       <m:mtr>
 139        <m:mtd>
 140         <m:mrow>
 141          <m:mphantom><m:mtext>__</m:mtext></m:mphantom>
 142          <m:mtext><xsl:value-of select="./@no"/>:</m:mtext>
 143          <xsl:apply-templates select="./*[1]"/>
 144         </m:mrow>
 145        </m:mtd>
 146       </m:mtr>
 147       </xsl:for-each>
 148       <m:mtr>
 149        <m:mtd>
 150         <m:mrow>
 151          <m:mtext>CORRESPONDING PROOF:</m:mtext>
 152         </m:mrow>
 153        </m:mtd>
 154       </m:mtr>
 155       <m:mtr>
 156        <m:mtd>
 157         <m:mrow>
 158          <m:mphantom><m:mtext>__</m:mtext></m:mphantom>
 159          <xsl:apply-templates select="body/*[1]"/>
 160         </m:mrow>
 161        </m:mtd>
 162       </m:mtr>
 163      </m:mtable>
 164     </m:math>
 165 </xsl:template>
 166
 167 <!-- MUTUAL INDUCTIVE DEFINITION -->
 168
 169 <xsl:template match="InductiveDefinition">
 170     <m:math>
 171      <m:mtable align="baseline 1" equalrows="false" columnalign="left" helm:xref="{@helm:xref}">
 172      <xsl:for-each select="InductiveType">
 173       <m:mtr>
 174        <m:mtd>
 175         <m:mrow>
 176          <xsl:choose>
 177          <xsl:when test="position() = 1">
 178           <xsl:choose>
 179           <xsl:when test="string(./@inductive) = &quot;true&quot;">
 180            <m:mtext>INDUCTIVE DEFINITION</m:mtext>
 181           </xsl:when>
 182           <xsl:otherwise>
 183            <m:mtext>COINDUCTIVE DEFINITION</m:mtext>
 184           </xsl:otherwise>
 185           </xsl:choose>
 186          </xsl:when>
 187          <xsl:otherwise>
 188           <m:mtext>AND</m:mtext>
 189          </xsl:otherwise>
 190          </xsl:choose>
 191          <m:mphantom><m:mtext>_</m:mtext></m:mphantom>
 192          <m:mtext><xsl:value-of select="./@name"/>(<xsl:if test="string(../Params) != &quot;&quot;"><xsl:value-of select="../Params"/></xsl:if>)</m:mtext>
 193         </m:mrow>
 194        </m:mtd>
 195       </m:mtr>
 196       <m:mtr>
 197        <m:mtd>
 198         <m:mrow>
 199          <m:mphantom><m:mtext>__</m:mtext></m:mphantom>
 200          <m:mtext>[</m:mtext>
 201          <xsl:choose>
 202          <xsl:when test="string(../Param) != &quot;&quot;">
 203           <m:mtable align="baseline 1" equalrows="false" columnalign="left">
 204            <xsl:for-each select="../Param">
 205             <m:mtr>
 206              <m:mtd>
 207               <m:mrow>
 208                <m:mi><xsl:value-of select="./@name"/></m:mi>
 209                <m:mo>:</m:mo>
 210                <xsl:apply-templates select="*"/>
 211               </m:mrow>
 212              </m:mtd>
 213             </m:mtr>
 214            </xsl:for-each>
 215             <m:mtr>
 216              <m:mtd>
 217               <m:mrow>
 218                <m:mtext>]</m:mtext>
 219               </m:mrow>
 220              </m:mtd>
 221             </m:mtr>
 222           </m:mtable>
 223          </xsl:when>
 224          <xsl:otherwise>
 225           <m:mtext>]</m:mtext>
 226          </xsl:otherwise>
 227          </xsl:choose>
 228         </m:mrow>
 229        </m:mtd>
 230       </m:mtr>
 231       <m:mtr>
 232        <m:mtd>
 233         <m:mrow>
 234          <m:mtext>OF ARITY</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          <xsl:apply-templates select="./arity/*[1]"/>
 243         </m:mrow>
 244        </m:mtd>
 245       </m:mtr>
 246       <m:mtr>
 247        <m:mtd>
 248         <m:mrow>
 249          <m:mtext>BUILT FROM</m:mtext>
 250         </m:mrow>
 251        </m:mtd>
 252       </m:mtr>
 253       <xsl:for-each select="./Constructor">
 254       <m:mtr>
 255        <m:mtd>
 256         <m:mrow>
 257          <xsl:choose>
 258          <xsl:when test="position() = 1">
 259           <m:mphantom><m:mtext>__</m:mtext></m:mphantom>
 260          </xsl:when>
 261          <xsl:otherwise>
 262           <m:mtext>|</m:mtext>
 263           <m:mphantom><m:mtext>_</m:mtext></m:mphantom>
 264          </xsl:otherwise>
 265          </xsl:choose>
 266          <m:mtext><xsl:value-of select="./@name"/> OF</m:mtext>
 267          <m:mphantom><m:mtext>_</m:mtext></m:mphantom>
 268          <xsl:apply-templates select="./*[1]"/>
 269         </m:mrow>
 270        </m:mtd>
 271       </m:mtr>
 272       </xsl:for-each>
 273      </xsl:for-each>
 274      </m:mtable>
 275     </m:math>
 276 </xsl:template>
 277
 278 <!-- VARIABLE -->
 279
 280 <xsl:template match="Variable">
 281     <m:math>
 282      <m:mtable align="baseline 1" equalrows="false" columnalign="left" helm:xref="{@helm:xref}">
 283       <m:mtr>
 284        <m:mtd>
 285         <m:mrow>
 286          <m:mtext>VARIABLE <xsl:value-of select="@name"/> OF TYPE</m:mtext>
 287         </m:mrow>
 288        </m:mtd>
 289       </m:mtr>
 290       <m:mtr>
 291        <m:mtd>
 292         <m:mrow>
 293          <m:mphantom><m:mtext>__</m:mtext></m:mphantom>
 294          <xsl:apply-templates select="type/*[1]"/>
 295         </m:mrow>
 296        </m:mtd>
 297       </m:mtr>
 298      </m:mtable>
 299     </m:math>
 300 </xsl:template>
 301
 302 <!--**********************-->
 303 <!--        TERMS         -->
 304 <!--**********************-->
 305
 306 <xsl:template match="m:bvar">
 307  <xsl:choose>
 308   <xsl:when test="m:type">
 309    <xsl:variable name="charlength">
 310     <xsl:apply-templates select="m:ci" mode="charcount"/>
 311    </xsl:variable>
 312    <xsl:choose>
 313     <xsl:when test="$charlength >= $framewidth">
 314      <m:mtable align="baseline 1" equalrows="false" columnalign="left">
 315       <m:mtr>
 316        <m:mtd>
 317         <xsl:apply-templates select="m:ci"/>
 318         <m:mo>:</m:mo>
 319        </m:mtd>
 320       </m:mtr>
 321       <m:mtr>
 322        <m:mtd>
 323          <xsl:apply-templates select="m:type"/>
 324        </m:mtd>
 325       </m:mtr>
 326      </m:mtable>
 327     </xsl:when>
 328     <xsl:otherwise>
 329      <xsl:apply-templates select="m:ci"/>
 330      <m:mo>:</m:mo>
 331      <xsl:apply-templates select="m:type"/>
 332     </xsl:otherwise>
 333    </xsl:choose>
 334   </xsl:when>
 335   <xsl:otherwise>
 336    <xsl:apply-templates select="m:ci"/>
 337   </xsl:otherwise>
 338  </xsl:choose>
 339 </xsl:template>
 340
 341
 342 <!-- CSYMBOL -->
 343
 344 <xsl:template match="m:apply[m:csymbol]">
 345     <xsl:variable name="name"><xsl:value-of select="m:csymbol"/></xsl:variable>
 346     <xsl:variable name="charlength"><xsl:apply-templates select="m:csymbol" mode="charcount"/></xsl:variable>
 347     <m:mrow>
 348      <xsl:if test="@helm:xref">
 349       <xsl:attribute name="helm:xref"><xsl:value-of select="@helm:xref"/></xsl:attribute>
 350      </xsl:if>
 351      <xsl:choose>
 352       <xsl:when test="$name='forall'">
 353        <xsl:choose>
 354        <xsl:when test="$charlength >= $framewidth">
 355         <m:mtable align="baseline 1" equalrows="false" columnalign="left">
 356          <m:mtr>
 357           <m:mtd>
 358             <m:mo color="Blue"><m:mchar name="ForAll"/></m:mo>
 359             <xsl:apply-templates select="m:bvar"/>
 360           </m:mtd>
 361          </m:mtr>
 362          <m:mtr>
 363           <m:mtd>
 364            <m:mrow>
 365             <m:mo>.</m:mo>
 366             <xsl:apply-templates select="*[position()=3]"/>
 367            </m:mrow>
 368           </m:mtd>
 369          </m:mtr>
 370         </m:mtable>
 371        </xsl:when>
 372        <xsl:otherwise>
 373         <m:mo color="Blue"><m:mchar name="ForAll"/></m:mo>
 374         <xsl:apply-templates select="m:bvar/m:ci"/>
 375         <m:mo>:</m:mo>
 376         <xsl:apply-templates select="m:bvar/m:type"/>
 377         <m:mo>.</m:mo>
 378         <xsl:apply-templates select="*[position()=3]"/>
 379        </xsl:otherwise>
 380        </xsl:choose>
 381       </xsl:when>
 382       <xsl:when test="$name='prod'">
 383        <xsl:choose>
 384        <xsl:when test="$charlength >= $framewidth">
 385         <m:mtable align="baseline 1" equalrows="false" columnalign="left">
 386          <m:mtr>
 387           <m:mtd>
 388             <m:mo color="Blue">&#x03a0;</m:mo>
 389             <xsl:apply-templates select="m:bvar"/>
 390           </m:mtd>
 391          </m:mtr>
 392          <m:mtr>
 393           <m:mtd>
 394            <m:mrow>
 395             <m:mo>.</m:mo>
 396             <xsl:apply-templates select="*[position()=3]"/>
 397            </m:mrow>
 398           </m:mtd>
 399          </m:mtr>
 400         </m:mtable>
 401        </xsl:when>
 402        <xsl:otherwise>
 403         <m:mo color="Blue">&#x03a0;</m:mo>
 404         <xsl:apply-templates select="m:bvar/m:ci"/>
 405         <m:mo>:</m:mo>
 406         <xsl:apply-templates select="m:bvar/m:type"/>
 407         <m:mo>.</m:mo>
 408         <xsl:apply-templates select="*[position()=3]"/>
 409        </xsl:otherwise>
 410        </xsl:choose>
 411       </xsl:when>
 412       <xsl:when test="$name='arrow'">
 413        <xsl:choose>
 414        <xsl:when test="$charlength >= $framewidth">
 415         <m:mtable align="baseline 1" equalrows="false" columnalign="left">
 416          <m:mtr>
 417           <m:mtd>
 418            <m:mrow>
 419             <m:mo stretchy="false">(</m:mo>
 420             <xsl:apply-templates select="*[position()=2]"/>
 421            </m:mrow>
 422           </m:mtd>
 423          </m:mtr>
 424          <m:mtr>
 425           <m:mtd>
 426            <m:mrow>
 427             <m:mo color="Blue">&#x2192;</m:mo>
 428             <xsl:apply-templates select="*[position()=3]"/>
 429            </m:mrow>
 430           </m:mtd>
 431          </m:mtr>
 432          <m:mtr>
 433           <m:mtd>
 434            <m:mrow>
 435             <m:mo stretchy="false">)</m:mo>
 436            </m:mrow>
 437           </m:mtd>
 438          </m:mtr>
 439         </m:mtable>
 440        </xsl:when>
 441        <xsl:otherwise>
 442         <m:mo stretchy="false">(</m:mo>
 443         <xsl:apply-templates select="*[position()=2]"/>
 444         <m:mo color="Blue">&#x2192;</m:mo>
 445         <xsl:apply-templates select="*[position()=3]"/>
 446         <m:mo stretchy="false">)</m:mo>
 447        </xsl:otherwise>
 448        </xsl:choose>
 449       </xsl:when>
 450       <xsl:when test="$name='app'">
 451        <xsl:choose>
 452        <xsl:when test="$charlength >= $framewidth">
 453         <m:mtable align="baseline 1" equalrows="false" columnalign="left">
 454          <m:mtr>
 455           <m:mtd>
 456            <m:mrow>
 457             <m:mo stretchy="false">(</m:mo>
 458             <xsl:apply-templates select="*[position()=2]"/>
 459            </m:mrow>
 460           </m:mtd>
 461          </m:mtr>
 462          <xsl:for-each select="*[position()>2]">
 463          <m:mtr>
 464           <m:mtd>
 465            <m:mrow>
 466             <m:mphantom><m:mtext>(</m:mtext></m:mphantom>
 467             <xsl:apply-templates select="."/>
 468            </m:mrow>
 469           </m:mtd>
 470          </m:mtr>
 471          </xsl:for-each>
 472          <m:mtr>
 473           <m:mtd>
 474            <m:mrow>
 475             <m:mo stretchy="false">)</m:mo>
 476            </m:mrow>
 477           </m:mtd>
 478          </m:mtr>
 479         </m:mtable>
 480        </xsl:when>
 481        <xsl:otherwise>
 482         <m:mo stretchy="false">(</m:mo>
 483         <xsl:apply-templates select="*[position()=2]"/>
 484         <xsl:for-each select="*[position()>2]">
 485          <m:mphantom><m:mtext>_</m:mtext></m:mphantom>
 486          <xsl:apply-templates select="."/>
 487         </xsl:for-each>
 488         <m:mo stretchy="false">)</m:mo>
 489        </xsl:otherwise>
 490        </xsl:choose>
 491       </xsl:when>
 492       <xsl:when test="$name='cast'">
 493        <xsl:choose>
 494        <xsl:when test="$charlength >= $framewidth">
 495         <m:mtable align="baseline 1" equalrows="false" columnalign="left">
 496          <m:mtr>
 497           <m:mtd>
 498            <m:mrow>
 499             <m:mo stretchy="false">(</m:mo>
 500             <xsl:apply-templates select="*[position()=2]"/>
 501            </m:mrow>
 502           </m:mtd>
 503          </m:mtr>
 504          <m:mtr>
 505           <m:mtd>
 506            <m:mrow>
 507             <m:mo color="Maroon">:></m:mo>
 508             <xsl:apply-templates select="*[position()=3]"/>
 509            </m:mrow>
 510           </m:mtd>
 511          </m:mtr>
 512          <m:mtr>
 513           <m:mtd>
 514            <m:mrow>
 515             <m:mo stretchy="false">)</m:mo>
 516            </m:mrow>
 517           </m:mtd>
 518          </m:mtr>
 519         </m:mtable>
 520        </xsl:when>
 521        <xsl:otherwise>
 522         <m:mo stretchy="false">(</m:mo>
 523         <xsl:apply-templates select="*[position()=2]"/>
 524         <m:mo color="Maroon">:></m:mo>
 525         <xsl:apply-templates select="*[position()=3]"/>
 526         <m:mo stretchy="false">)</m:mo>
 527        </xsl:otherwise>
 528        </xsl:choose>
 529       </xsl:when>
 530       <xsl:when test="$name='Prop'">
 531        <m:mo>Prop</m:mo>
 532       </xsl:when>
 533       <xsl:when test="$name='Set'">
 534        <m:mo>Set</m:mo>
 535       </xsl:when>
 536       <xsl:when test="$name='Type'">
 537        <m:mo>Type</m:mo>
 538       </xsl:when>
 539       <xsl:when test="$name='mutcase'">
 540        <xsl:choose>
 541        <xsl:when test="$charlength >= $framewidth">
 542         <xsl:variable name="charlength"><xsl:apply-templates select="*[position()=2]" mode="charcount"><xsl:with-param name="nosibling" select="1"/></xsl:apply-templates></xsl:variable>
 543         <m:mtable align="baseline 1" equalrows="false" columnalign="left">
 544          <m:mtr>
 545           <m:mtd>
 546            <m:mrow>
 547             <m:mo>&lt;</m:mo>
 548             <xsl:apply-templates select="*[position()=2]"/>
 549             <xsl:if test="$framewidth > $charlength">
 550              <m:mo>&gt;</m:mo>
 551              <m:mo>CASES</m:mo>
 552              <m:mphantom><m:mtext>_</m:mtext></m:mphantom>
 553              <xsl:apply-templates select="*[position()=3]"/>
 554             </xsl:if>
 555            </m:mrow>
 556           </m:mtd>
 557          </m:mtr>
 558          <xsl:if test="$charlength >= $framewidth">
 559          <m:mtr>
 560           <m:mtd>
 561            <m:mrow>
 562             <m:mo>&gt;</m:mo>
 563             <m:mo>CASES</m:mo>
 564             <m:mphantom><m:mtext>_</m:mtext></m:mphantom>
 565             <xsl:apply-templates select="*[position()=3]"/>
 566            </m:mrow>
 567           </m:mtd>
 568          </m:mtr>
 569          </xsl:if>
 570          <m:mtr>
 571           <m:mtd>
 572            <m:mrow>
 573             <m:mo>OF</m:mo>
 574            </m:mrow>
 575           </m:mtd>
 576          </m:mtr>
 577          <xsl:for-each select="*[position() mod 2 = 0 and position()>3]">
 578          <xsl:variable name="charlength"><xsl:apply-templates select="." mode="charcount"><xsl:with-param name="nosibling" select="1"/></xsl:apply-templates></xsl:variable>
 579          <m:mtr>
 580           <m:mtd>
 581            <m:mrow>
 582             <xsl:choose>
 583             <xsl:when test="position() = 1">
 584               <m:mphantom><m:mtext>|</m:mtext></m:mphantom>
 585             </xsl:when>
 586             <xsl:otherwise>
 587              <m:mo stretchy="false">|</m:mo>
 588             </xsl:otherwise>
 589             </xsl:choose>
 590             <m:mphantom><m:mtext>_</m:mtext></m:mphantom>
 591             <xsl:apply-templates select="."/>
 592             <xsl:if test="$framewidth > $charlength">
 593              <m:mo color="Green">&#x21d2;</m:mo>
 594              <xsl:apply-templates select="following-sibling::*[position()= 1]"/>
 595             </xsl:if>
 596            </m:mrow>
 597           </m:mtd>
 598          </m:mtr>
 599          <xsl:if test="$charlength >= $framewidth">
 600          <m:mtr>
 601           <m:mtd>
 602            <m:mrow>
 603             <m:mphantom><m:mtext>|_</m:mtext></m:mphantom>
 604             <m:mo color="Green">&#x21d2;</m:mo>
 605             <xsl:apply-templates select="following-sibling::*[position()= 1]"/>
 606            </m:mrow>
 607           </m:mtd>
 608          </m:mtr>
 609          </xsl:if>
 610         </xsl:for-each>
 611          <m:mtr>
 612           <m:mtd>
 613            <m:mrow>
 614             <m:mo>END</m:mo>
 615            </m:mrow>
 616           </m:mtd>
 617          </m:mtr>
 618         </m:mtable>
 619        </xsl:when>
 620        <xsl:otherwise>
 621         <m:mo>&lt;</m:mo><xsl:apply-templates select="*[position()=2]"/><m:mo>&gt;</m:mo>
 622         <m:mo>CASES</m:mo>
 623         <m:mphantom><m:mtext>_</m:mtext></m:mphantom>
 624         <xsl:apply-templates select="*[position()=3]"/>
 625         <m:mphantom><m:mtext>_</m:mtext></m:mphantom>
 626         <m:mo>OF</m:mo>
 627         <xsl:for-each select="*[position() mod 2 = 0 and position()>3]">
 628          <xsl:choose>
 629          <xsl:when test="position() != 1">
 630           <m:mo stretchy="false">|</m:mo>
 631          </xsl:when>
 632          </xsl:choose>
 633          <xsl:apply-templates select="."/>
 634          <m:mo color="Green">&#x21d2;</m:mo>
 635          <xsl:apply-templates select="following-sibling::*[position()= 1]"/>
 636         </xsl:for-each>
 637         <m:mphantom><m:mtext>_</m:mtext></m:mphantom>
 638         <m:mo>END</m:mo>
 639        </xsl:otherwise>
 640        </xsl:choose>
 641       </xsl:when>
 642       <xsl:when test="$name='fix'">
 643        <xsl:choose>
 644        <xsl:when test="$charlength >= $framewidth">
 645         <m:mtable align="baseline 1" equalrows="false" columnalign="left">
 646          <m:mtr>
 647           <m:mtd>
 648            <m:mrow>
 649             <m:mo>FIX</m:mo>
 650             <m:mphantom><m:mtext>_</m:mtext></m:mphantom>
 651             <m:mi><xsl:value-of select="m:ci"/></m:mi>
 652             <m:mo stretchy="false">{</m:mo>
 653            </m:mrow>
 654           </m:mtd>
 655          </m:mtr>
 656          <m:mtr>
 657           <m:mtd>
 658            <m:mrow>
 659             <m:mphantom><m:mtext>__</m:mtext></m:mphantom>
 660             <m:mtable align="baseline 1" equalrows="false" columnalign="left">
 661             <xsl:for-each select="m:bvar">
 662              <xsl:variable name="charlength"><xsl:apply-templates select="m:type" mode="charcount"><xsl:with-param name="nosibling" select="1"/></xsl:apply-templates></xsl:variable>
 663              <m:mtr>
 664               <m:mtd>
 665                <m:mrow>
 666                 <m:mi><xsl:value-of select="m:ci"/></m:mi>
 667                 <m:mo>:</m:mo>
 668                 <xsl:if test="$framewidth > $charlength">
 669                  <xsl:apply-templates select="m:type"/>
 670                 </xsl:if>
 671                </m:mrow>
 672               </m:mtd>
 673              </m:mtr>
 674              <xsl:if test="$charlength >= $framewidth">
 675              <m:mtr>
 676               <m:mtd>
 677                <m:mrow>
 678                 <m:mphantom><m:mtext>:=</m:mtext></m:mphantom>
 679                 <xsl:apply-templates select="m:type"/>
 680                </m:mrow>
 681               </m:mtd>
 682              </m:mtr>
 683              </xsl:if>
 684              <m:mtr>
 685               <m:mtd>
 686                <m:mrow>
 687                 <m:mo>:=</m:mo>
 688                 <xsl:apply-templates select="following-sibling::*[position()=1]"/>
 689                </m:mrow>
 690               </m:mtd>
 691              </m:mtr>
 692             </xsl:for-each>
 693             </m:mtable>
 694            </m:mrow>
 695           </m:mtd>
 696          </m:mtr>
 697          <m:mtr>
 698           <m:mtd>
 699            <m:mrow>
 700             <m:mo stretchy="false">}</m:mo>
 701            </m:mrow>
 702           </m:mtd>
 703          </m:mtr>
 704         </m:mtable>
 705        </xsl:when>
 706        <xsl:otherwise>
 707         <m:mo>FIX</m:mo>
 708         <m:mi><xsl:value-of select="m:ci"/></m:mi>
 709         <m:mo stretchy="false">{</m:mo>
 710         <m:mtable align="baseline 1" equalrows="false" columnalign="left">
 711         <xsl:for-each select="m:bvar">
 712          <m:mtr>
 713           <m:mtd>
 714            <m:mrow>
 715             <m:mi><xsl:value-of select="m:ci"/></m:mi>
 716             <m:mo>:</m:mo>
 717             <xsl:apply-templates select="m:type"/>
 718             <m:mo>:=</m:mo>
 719             <xsl:apply-templates select="following-sibling::*[position() = 1]"/>
 720             <xsl:if test="position()=last()">
 721              <m:mo stretchy="false">}</m:mo>
 722             </xsl:if>
 723            </m:mrow>
 724           </m:mtd>
 725          </m:mtr>
 726          </xsl:for-each>
 727         </m:mtable>
 728        </xsl:otherwise>
 729        </xsl:choose>
 730       </xsl:when>
 731       <xsl:when test="$name='cofix'">
 732        <xsl:choose>
 733        <xsl:when test="$charlength >= $framewidth">
 734         <m:mtable align="baseline 1" equalrows="false" columnalign="left">
 735          <m:mtr>
 736           <m:mtd>
 737            <m:mrow>
 738             <m:mo>COFIX</m:mo>
 739             <m:mphantom><m:mtext>_</m:mtext></m:mphantom>
 740             <m:mi><xsl:value-of select="m:ci"/></m:mi>
 741             <m:mo stretchy="false">{</m:mo>
 742            </m:mrow>
 743           </m:mtd>
 744          </m:mtr>
 745          <m:mtr>
 746           <m:mtd>
 747            <m:mrow>
 748             <m:mphantom><m:mtext>__</m:mtext></m:mphantom>
 749             <m:mtable align="baseline 1" equalrows="false" columnalign="left">
 750             <xsl:for-each select="m:bvar">
 751              <xsl:variable name="charlength"><xsl:apply-templates select="m:type" mode="charcount"><xsl:with-param name="nosibling" select="1"/></xsl:apply-templates></xsl:variable>
 752              <m:mtr>
 753               <m:mtd>
 754                <m:mrow>
 755                 <m:mi><xsl:value-of select="m:ci"/></m:mi>
 756                 <m:mo>:</m:mo>
 757                 <xsl:if test="$framewidth > $charlength">
 758                  <xsl:apply-templates select="m:type"/>
 759                 </xsl:if>
 760                </m:mrow>
 761               </m:mtd>
 762              </m:mtr>
 763              <xsl:if test="$charlength >= $framewidth">
 764              <m:mtr>
 765               <m:mtd>
 766                <m:mrow>
 767                 <m:mphantom><m:mtext>:=</m:mtext></m:mphantom>
 768                 <xsl:apply-templates select="m:type"/>
 769                </m:mrow>
 770               </m:mtd>
 771              </m:mtr>
 772              </xsl:if>
 773              <m:mtr>
 774               <m:mtd>
 775                <m:mrow>
 776                 <m:mo>:=</m:mo>
 777                 <xsl:apply-templates select="following-sibling::*[position() = 1]"/>
 778                </m:mrow>
 779               </m:mtd>
 780              </m:mtr>
 781             </xsl:for-each>
 782             </m:mtable>
 783            </m:mrow>
 784           </m:mtd>
 785          </m:mtr>
 786          <m:mtr>
 787           <m:mtd>
 788            <m:mrow>
 789             <m:mo stretchy="false">}</m:mo>
 790            </m:mrow>
 791           </m:mtd>
 792          </m:mtr>
 793         </m:mtable>
 794        </xsl:when>
 795        <xsl:otherwise>
 796         <m:mo>COFIX</m:mo>
 797         <m:mi><xsl:value-of select="m:ci"/></m:mi>
 798         <m:mo stretchy="false">{</m:mo>
 799         <m:mtable align="baseline 1" equalrows="false" columnalign="left">
 800         <xsl:for-each select="m:bvar">
 801          <m:mtr>
 802           <m:mtd>
 803            <m:mrow>
 804             <m:mi><xsl:value-of select="m:ci"/></m:mi>
 805             <m:mo>:</m:mo>
 806             <xsl:apply-templates select="m:type"/>
 807             <m:mo>:=</m:mo>
 808             <xsl:apply-templates select="following-sibling::*[position() = 1]"/>
 809             <xsl:if test="position()=last()">
 810              <m:mo stretchy="false">}</m:mo>
 811             </xsl:if>
 812            </m:mrow>
 813           </m:mtd>
 814          </m:mtr>
 815          </xsl:for-each>
 816         </m:mtable>
 817        </xsl:otherwise>
 818        </xsl:choose>
 819       </xsl:when>
 820       <!-- ***************************************** -->
 821       <!-- *********** PROOF ELEMENTS ************** -->
 822       <!-- ***************************************** -->
 823       <xsl:when test="$name='proof'">
 824         <m:mtable align="baseline 1" equalrows="false" columnalign="left">
 825          <m:mtr>
 826           <m:mtd>
 827            <m:mrow>
 828             <xsl:apply-templates select="*[position()=2]"/>
 829            </m:mrow>
 830           </m:mtd>
 831          </m:mtr>
 832          <m:mtr>
 833           <m:mtd>
 834            <m:mrow>
 835             <m:mtext color="Maroon">we proved </m:mtext>
 836             <m:mphantom><m:mtext>_</m:mtext></m:mphantom>
 837             <xsl:apply-templates select="*[position()=3]"/>
 838            </m:mrow>
 839           </m:mtd>
 840          </m:mtr>
 841         </m:mtable>
 842       </xsl:when>
 843       <xsl:when test="$name='letin'">
 844         <m:mtable align="baseline 1" equalrows="false" columnalign="left">
 845          <!-- <xsl:for-each select="APPLY[m:csymbol and (string(m:csymbol)='let')]"> -->
 846          <xsl:for-each select="*[(last() > position()) and (position()>1)]">
 847          <m:mtr>
 848           <m:mtd>
 849            <m:mrow>
 850             <xsl:apply-templates select="."/>
 851            </m:mrow>
 852           </m:mtd>
 853          </m:mtr>
 854          </xsl:for-each>
 855          <m:mtr>
 856           <m:mtd>
 857            <m:mrow>
 858             <xsl:apply-templates select="*[position()=last()]"/>
 859            </m:mrow>
 860           </m:mtd>
 861          </m:mtr>
 862         </m:mtable>
 863       </xsl:when>
 864       <xsl:when test="$name='let'">
 865        <m:mtext>(</m:mtext>
 866        <xsl:apply-templates select="m:ci"/>
 867        <m:mtext>) </m:mtext>
 868        <xsl:apply-templates select="*[3]"/>
 869       </xsl:when>
 870       <xsl:when test="$name='thread'">
 871         <m:mtable align="baseline 1" equalrows="false" columnalign="left">
 872          <m:mtr>
 873           <m:mtd>
 874            <m:mrow>
 875             <xsl:choose>
 876              <xsl:when test="name(*[last()])='m:apply'">
 877               <xsl:apply-templates select="*[last()]"/>
 878              </xsl:when>
 879              <xsl:otherwise>
 880               <m:mtext>Consider </m:mtext>
 881               <xsl:apply-templates select="*[last()]"/>
 882              </xsl:otherwise>
 883             </xsl:choose>
 884            </m:mrow>
 885           </m:mtd>
 886          </m:mtr>
 887          <xsl:apply-templates mode="thread" select="*[(last()-2)]"/>
 888         </m:mtable>
 889       </xsl:when>
 890       <xsl:when test="$name='rewrite_and_apply'">
 891         <m:mtable>
 892          <m:mtr>
 893           <m:mtd>
 894            <m:mrow>
 895             <m:mtext>Rewrite</m:mtext>
 896             <m:mphantom><m:mtext>_</m:mtext></m:mphantom>
 897             <xsl:apply-templates select="*[2]/*[2]"/>
 898             <m:mphantom><m:mtext>_</m:mtext></m:mphantom>
 899             <m:mtext>with</m:mtext>
 900             <m:mphantom><m:mtext>_</m:mtext></m:mphantom>
 901             <xsl:apply-templates select="*[2]/*[3]"/>
 902             <m:mphantom><m:mtext>_</m:mtext></m:mphantom>
 903             <m:mtext>by</m:mtext>
 904             <m:mphantom><m:mtext>_</m:mtext></m:mphantom>
 905             <xsl:apply-templates select="*[2]/*[4]"/>
 906             <m:mphantom><m:mtext>_</m:mtext></m:mphantom>
 907             <m:mtext>in</m:mtext>
 908             <m:mphantom><m:mtext>_</m:mtext></m:mphantom>
 909             <xsl:apply-templates select="*[3]"/>
 910             <m:mphantom><m:mtext>_</m:mtext></m:mphantom>
 911             <m:mtext>and apply to</m:mtext>
 912             <m:mphantom><m:mtext>_</m:mtext></m:mphantom>
 913             <xsl:apply-templates select="*[position()>3]"/>
 914            </m:mrow>
 915           </m:mtd>
 916          </m:mtr>
 917        </m:mtable>
 918       </xsl:when>
 919       <xsl:when test="$name='and_ind'">
 920         <m:mtable align="baseline 1" equalrows="false" columnalign="left">
 921          <m:mtr>
 922           <m:mtd>
 923            <m:mrow>
 924             <xsl:choose>
 925              <xsl:when test="name(*[2])='m:apply'">
 926               <xsl:apply-templates select="*[2]"/>
 927              </xsl:when>
 928              <xsl:otherwise>
 929               <m:mtext>Consider </m:mtext>
 930               <xsl:apply-templates select="*[2]"/>
 931              </xsl:otherwise>
 932             </xsl:choose>
 933            </m:mrow>
 934           </m:mtd>
 935          </m:mtr>
 936          <m:mtr>
 937           <m:mtd>
 938            <m:mtext>In particular, we have</m:mtext>
 939           </m:mtd>
 940          </m:mtr>
 941          <m:mtr>
 942           <m:mtd>
 943            <m:mrow>
 944             <m:mtext>(</m:mtext>
 945             <xsl:apply-templates select="*[3]"/>
 946             <m:mtext>)</m:mtext>
 947             <m:mphantom><m:mtext>_</m:mtext></m:mphantom>
 948             <xsl:apply-templates select="*[4]"/>
 949             </m:mrow>
 950           </m:mtd>
 951          </m:mtr>
 952          <m:mtr>
 953           <m:mtd>
 954            <m:mrow>
 955             <m:mtext>(</m:mtext>
 956             <xsl:apply-templates select="*[5]"/>
 957             <m:mtext>)</m:mtext>
 958             <m:mphantom><m:mtext>_</m:mtext></m:mphantom>
 959             <xsl:apply-templates select="*[6]"/>
 960             </m:mrow>
 961           </m:mtd>
 962          </m:mtr>
 963          <m:mtr>
 964           <m:mtd>
 965            <m:mrow>
 966             <xsl:apply-templates select="*[7]"/>
 967            </m:mrow>
 968           </m:mtd>
 969          </m:mtr>
 970         </m:mtable>
 971       </xsl:when>
 972       <xsl:when test="$name='or_ind'">
 973         <m:mtable align="baseline 1" equalrows="false" columnalign="left">
 974          <m:mtr>
 975           <m:mtd>
 976            <m:mrow>
 977             <xsl:choose>
 978              <xsl:when test="name(*[2])='m:apply'">
 979               <xsl:apply-templates select="*[2]"/>
 980              </xsl:when>
 981              <xsl:otherwise>
 982               <m:mtext>Consider</m:mtext>
 983               <m:mphantom><m:mtext>_</m:mtext></m:mphantom>
 984               <xsl:apply-templates select="*[2]"/>
 985              </xsl:otherwise>
 986             </xsl:choose>
 987            </m:mrow>
 988           </m:mtd>
 989          </m:mtr>
 990          <m:mtr>
 991           <m:mtd>
 992            <m:mtext>We prove</m:mtext>
 993            <m:mphantom><m:mtext>_</m:mtext></m:mphantom>
 994            <xsl:apply-templates select="*[3]"/>
 995            <m:mphantom><m:mtext>_</m:mtext></m:mphantom>
 996            <m:mtext>by cases:</m:mtext>
 997           </m:mtd>
 998          </m:mtr>
 999          <m:mtr>
1000           <m:mtd>
1001            <m:mrow>
1002             <m:mtext>*</m:mtext>
1003             <xsl:apply-templates select="*[4]"/>
1004            </m:mrow>
1005           </m:mtd>
1006          </m:mtr>
1007          <m:mtr>
1008           <m:mtd>
1009            <m:mrow>
1010             <m:mtext>*</m:mtext>
1011             <xsl:apply-templates select="*[5]"/>
1012            </m:mrow>
1013           </m:mtd>
1014          </m:mtr>
1015         </m:mtable>
1016       </xsl:when>
1017       <xsl:otherwise>
1018        <m:ci>ERROR</m:ci>
1019       </xsl:otherwise>
1020      </xsl:choose>
1021     </m:mrow>
1022 </xsl:template>
1023
1024 <xsl:template match="*" mode="thread">
1025  <xsl:variable name="name"><xsl:value-of select="following-sibling::*[position()=1]/m:csymbol"/></xsl:variable>
1026  <xsl:choose>
1027   <xsl:when test="$name='rw_step'">
1028          <m:mtr>
1029           <m:mtd>
1030            <m:mrow>
1031             <m:mtext>Rewrite</m:mtext>
1032             <m:mphantom><m:mtext>_</m:mtext></m:mphantom>
1033             <xsl:apply-templates select="following-sibling::*[position()=1]/*[2]"/>
1034             <m:mphantom><m:mtext>_</m:mtext></m:mphantom>
1035             <m:mtext>with</m:mtext>
1036             <m:mphantom><m:mtext>_</m:mtext></m:mphantom>
1037             <xsl:apply-templates select="following-sibling::*[position()=1]/*[3]"/>
1038             <m:mphantom><m:mtext>_</m:mtext></m:mphantom>
1039             <m:mtext>by</m:mtext>
1040             <m:mphantom><m:mtext>_</m:mtext></m:mphantom>
1041             <xsl:apply-templates select="following-sibling::*[position()=1]/*[4]"/>
1042            </m:mrow>
1043           </m:mtd>
1044          </m:mtr>
1045          <m:mtr>
1046           <m:mtd>
1047            <m:mrow>
1048             <m:mtext color="Maroon">we get</m:mtext>
1049             <m:mphantom><m:mtext>_</m:mtext></m:mphantom>
1050             <xsl:apply-templates select="."/>
1051            </m:mrow>
1052           </m:mtd>
1053          </m:mtr>
1054    </xsl:when>
1055    <xsl:otherwise>
1056          <m:mtr>
1057           <m:mtd>
1058            <m:mrow>
1059             <xsl:apply-templates select="following-sibling::*[position()=1]"/>
1060            </m:mrow>
1061           </m:mtd>
1062          </m:mtr>
1063          <m:mtr>
1064           <m:mtd>
1065            <m:mrow>
1066             <m:mtext color="Maroon">we get</m:mtext>
1067             <m:mphantom><m:mtext>_</m:mtext></m:mphantom>
1068             <xsl:apply-templates select="."/>
1069            </m:mrow>
1070           </m:mtd>
1071          </m:mtr>
1072     </xsl:otherwise>
1073    </xsl:choose>
1074          <xsl:apply-templates mode="thread" select="preceding-sibling::*[position()=2]"/>
1075 </xsl:template>
1076
1077
1078 <!-- LAMBDA -->
1079
1080 <xsl:template match="m:lambda">
1081     <xsl:variable name="charlength"><xsl:apply-templates select="*[position()=1]" mode="charcount"/></xsl:variable>
1082     <m:mrow helm:xref="{@helm:xref}">
1083      <xsl:choose>
1084      <xsl:when test="$charlength >= $framewidth">
1085       <m:mtable align="baseline 1" equalrows="false" columnalign="left">
1086         <m:mtr>
1087           <m:mtd>
1088             <m:mo color="Red">&#x03bb;</m:mo>
1089             <xsl:apply-templates select="m:bvar"/>
1090           </m:mtd>
1091          </m:mtr>
1092        <m:mtr>
1093         <m:mtd>
1094          <m:mrow>
1095           <m:mo>.</m:mo>
1096           <xsl:apply-templates select="*[position()=2]"/>
1097          </m:mrow>
1098         </m:mtd>
1099        </m:mtr>
1100       </m:mtable>
1101      </xsl:when>
1102      <xsl:otherwise>
1103       <m:mo color="Red">&#x03bb;</m:mo>
1104       <xsl:apply-templates select="m:bvar/m:ci"/>
1105       <m:mo>:</m:mo>
1106       <xsl:apply-templates select="m:bvar/m:type"/>
1107       <m:mo>.</m:mo>
1108       <xsl:apply-templates select="*[position()=2]"/>
1109      </xsl:otherwise>
1110      </xsl:choose>
1111     </m:mrow>
1112 </xsl:template>
1113
1114 <!-- *********************************** -->
1115 <!-- BASE SET OF MATHML CONTENT ELEMENTS -->
1116 <!-- *********************************** -->
1117
1118 <!-- Logic -->
1119
1120 <xsl:template match = "m:apply[m:eq[1]]">
1121  <xsl:variable name="charlength">
1122   <xsl:apply-templates select="*[1]" mode="charcount"/>
1123  </xsl:variable>
1124  <xsl:choose>
1125   <xsl:when test="$charlength >= $framewidth">
1126    <m:mtable align="baseline 1" equalrows="false" columnalign="left">
1127     <xsl:if test="@helm:xref">
1128      <xsl:attribute name="helm:xref">
1129       <xsl:value-of select="@helm:xref"/>
1130      </xsl:attribute>
1131     </xsl:if>
1132     <m:mtr>
1133      <m:mtd>
1134       <m:mo stretchy="false">(</m:mo>
1135       <xsl:apply-templates select="*[position()=2]"/>
1136      </m:mtd>
1137     </m:mtr>
1138     <xsl:for-each select = "*[position()>2]">
1139      <m:mtr>
1140       <m:mtd>
1141        <m:mphantom><m:mtext>__</m:mtext></m:mphantom>
1142        <m:mo helm:xref="m:in/@helm:xref">
1143         =
1144        </m:mo>
1145        <xsl:apply-templates select="."/>
1146       </m:mtd>
1147      </m:mtr>
1148     </xsl:for-each>
1149     <m:mtr>
1150      <m:mtd>
1151       <m:mo stretchy="false">)</m:mo>
1152      </m:mtd>
1153     </m:mtr>
1154    </m:mtable>
1155   </xsl:when>
1156   <xsl:otherwise>
1157    <xsl:apply-imports/>
1158   </xsl:otherwise>
1159  </xsl:choose>
1160 </xsl:template>
1161
1162
1163 <xsl:template match = "m:apply[m:and[1]|m:or[1]
1164           |m:geq[1]|m:leq[1]|m:gt[1]|m:lt[1]
1165           |m:in[1]|m:intesect[1]|m:union[1]|m:subset[1]
1166           |m:prsubset|m:setdiff[1]]">
1167  <xsl:variable name="symbol">
1168   <xsl:choose>
1169    <xsl:when test="m:and[1]">
1170     <xsl:value-of select="'wedge'"/>
1171    </xsl:when>
1172    <xsl:when test="m:or[1]">
1173     <xsl:value-of select="'vee'"/>
1174    </xsl:when>
1175    <xsl:when test="m:geq[1]">
1176     <xsl:value-of select="'geq'"/>
1177    </xsl:when>
1178    <xsl:when test="m:leq[1]">
1179     <xsl:value-of select="'leq'"/>
1180    </xsl:when>
1181    <xsl:when test="m:gt[1]">
1182     <xsl:value-of select="'gt'"/>
1183    </xsl:when>
1184    <xsl:when test="m:lt[1]">
1185     <xsl:value-of select="'lt'"/>
1186    </xsl:when>
1187    <xsl:when test="m:eq[1]">
1188     <xsl:value-of select="'Equal'"/>
1189    </xsl:when>
1190    <xsl:when test="m:in[1]">
1191     <xsl:value-of select="'Element'"/>
1192    </xsl:when>
1193    <xsl:when test="m:subset[1]">
1194     <xsl:value-of select="'SubsetEqual'"/>
1195    </xsl:when>
1196    <xsl:when test="m:prsubset[1]">
1197     <xsl:value-of select="'subset'"/>
1198    </xsl:when>
1199    <xsl:when test="m:intersect[1]">
1200     <xsl:value-of select="'Intersection'"/>
1201    </xsl:when>
1202    <xsl:when test="m:union[1]">
1203     <xsl:value-of select="'Union'"/>
1204    </xsl:when>
1205    <xsl:when test="m:setdiff[1]">
1206     <xsl:value-of select="'Backslash'"/>
1207    </xsl:when>
1208   </xsl:choose>
1209  </xsl:variable>
1210  <xsl:variable name="charlength">
1211   <xsl:apply-templates select="*[1]" mode="charcount"/>
1212  </xsl:variable>
1213  <xsl:choose>
1214   <xsl:when test="$charlength >= $framewidth">
1215    <m:mtable align="baseline 1" equalrows="false" columnalign="left">
1216     <xsl:if test="@helm:xref">
1217      <xsl:attribute name="helm:xref">
1218       <xsl:value-of select="@helm:xref"/>
1219      </xsl:attribute>
1220     </xsl:if>
1221     <m:mtr>
1222      <m:mtd>
1223       <m:mo stretchy="false">(</m:mo>
1224       <xsl:apply-templates select="*[position()=2]"/>
1225      </m:mtd>
1226     </m:mtr>
1227     <xsl:for-each select = "*[position()>2]">
1228      <m:mtr>
1229       <m:mtd>
1230        <m:mphantom><m:mtext>__</m:mtext></m:mphantom>
1231        <m:mo helm:xref="{*[1]/@helm:xref}">
1232         <m:mchar name="{$symbol}"/>
1233        </m:mo>
1234        <xsl:apply-templates select="."/>
1235       </m:mtd>
1236      </m:mtr>
1237     </xsl:for-each>
1238     <m:mtr>
1239      <m:mtd>
1240       <m:mo stretchy="false">)</m:mo>
1241      </m:mtd>
1242     </m:mtr>
1243    </m:mtable>
1244   </xsl:when>
1245   <xsl:otherwise>
1246    <xsl:apply-imports/>
1247   </xsl:otherwise>
1248  </xsl:choose>
1249 </xsl:template>
1250
1251 <xsl:template match = "m:set">
1252  <xsl:choose>
1253   <xsl:when test="count(child::*) = 0">
1254    <m:mi>
1255     <m:mchar name="emptyset"/>
1256    </m:mi>
1257   </xsl:when>
1258   <xsl:otherwise>
1259    <xsl:variable name="charlength">
1260     <xsl:apply-templates select="*[1]" mode="charcount"/>
1261    </xsl:variable>
1262    <xsl:choose>
1263     <xsl:when test="$charlength >= $framewidth">
1264      <xsl:choose>
1265       <xsl:when test="name(*[1]) = 'm:bvar'">
1266        <m:mtable align="baseline 1" equalrows="false" columnalign="left">
1267         <m:mtr>
1268          <m:mtd>
1269           <m:mo stretchy="false">{</m:mo>
1270           <xsl:apply-templates select="*[position()=1]"/>
1271          </m:mtd>
1272         </m:mtr>
1273         <m:mtr>
1274          <m:mtd>
1275           <m:mphantom><m:mtext>{</m:mtext></m:mphantom>
1276           <m:mo stretchy="false">|</m:mo>
1277           <xsl:apply-templates select="m:condition/*[1]"/>
1278          </m:mtd>
1279         </m:mtr>
1280         <m:mtr>
1281          <m:mtd>
1282           <m:mo stretchy="false">}</m:mo>
1283          </m:mtd>
1284         </m:mtr>
1285        </m:mtable>
1286       </xsl:when>
1287       <xsl:otherwise>
1288        <m:mtable align="baseline 1" equalrows="false" columnalign="left">
1289         <m:mtr>
1290          <m:mtd>
1291           <m:mo stretchy="false">{</m:mo>
1292           <xsl:apply-templates select="*[position()=1]"/>
1293           <xsl:if test="position() != last()">
1294            <mo>,</mo>
1295           </xsl:if>
1296          </m:mtd>
1297         </m:mtr>
1298         <xsl:for-each select = "*[position()>2]">
1299          <m:mtr>
1300           <m:mtd>
1301            <m:mphantom><m:mtext>{</m:mtext></m:mphantom>
1302            <xsl:apply-templates select="."/>
1303            <xsl:if test="position() != last()">
1304             <mo>,</mo>
1305            </xsl:if>
1306           </m:mtd>
1307          </m:mtr>
1308         </xsl:for-each>
1309         <m:mtr>
1310          <m:mtd>
1311           <m:mo stretchy="false">}</m:mo>
1312          </m:mtd>
1313         </m:mtr>
1314        </m:mtable>
1315       </xsl:otherwise>
1316      </xsl:choose>
1317     </xsl:when>
1318     <xsl:otherwise>
1319      <xsl:apply-imports/>
1320     </xsl:otherwise>
1321    </xsl:choose>
1322   </xsl:otherwise>
1323  </xsl:choose>
1324 </xsl:template>
1325
1326 <xsl:template match = "m:apply[m:card[1]]">
1327  <m:mo stretchy="false">|</m:mo>
1328   <xsl:apply-templates select="*[2]"/>
1329  <m:mo stretchy="false">|</m:mo>
1330 </xsl:template>
1331
1332 <!-- *********************************** -->
1333 <!--          PROOF ELEMENTS             -->
1334 <!-- *********************************** -->
1335
1336
1337
1338 <!--**********************-->
1339 <!--       COUNTING       -->
1340 <!--**********************-->
1341
1342 <xsl:template match="m:cn|m:and|m:or|m:not|m:exists|m:eq|m:lt|m:leq|m:gt|m:geq
1343  |m:in|m:notin|m:intersect|m:union|m:subset|m:prsubset|m:card|m:setdiff
1344  |m:plus|m:minus|m:times" mode="charcount">
1345 <xsl:param name="incurrent_length" select="0"/>
1346     <xsl:choose>
1347     <xsl:when test="$framewidth > ($incurrent_length + 3 + string-length())">
1348      <xsl:variable name="siblength">
1349       <xsl:apply-templates select="following-sibling::*[position()=1]" mode="charcount">
1350        <xsl:with-param name="incurrent_length" select="$incurrent_length + string-length()"/>
1351       </xsl:apply-templates>
1352      </xsl:variable>
1353      <xsl:choose>
1354      <xsl:when test="string($siblength) = &quot;&quot;">
1355       <xsl:value-of select="$incurrent_length + 3 + string-length()"/>
1356      </xsl:when>
1357      <xsl:otherwise>
1358       <xsl:value-of select="number($siblength)"/>
1359      </xsl:otherwise>
1360      </xsl:choose>
1361     </xsl:when>
1362     <xsl:otherwise>
1363      <xsl:value-of select="$incurrent_length + 3 + string-length()"/>
1364     </xsl:otherwise>
1365     </xsl:choose>
1366 </xsl:template>
1367
1368 <xsl:template match="m:ci|m:csymbol" mode="charcount">
1369 <xsl:param name="incurrent_length" select="0"/>
1370 <xsl:param name="nosibling" select="0"/>
1371     <xsl:choose>
1372     <xsl:when test="$framewidth > ($incurrent_length + string-length()) and ($nosibling = 0)">
1373      <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>
1374      <xsl:choose>
1375      <xsl:when test="string($siblength) = &quot;&quot;">
1376       <xsl:value-of select="$incurrent_length + string-length()"/>
1377      </xsl:when>
1378      <xsl:otherwise>
1379       <xsl:value-of select="number($siblength)"/>
1380      </xsl:otherwise>
1381      </xsl:choose>
1382     </xsl:when>
1383     <xsl:otherwise>
1384      <xsl:value-of select="$incurrent_length + string-length()"/>
1385     </xsl:otherwise>
1386     </xsl:choose>
1387 </xsl:template>
1388
1389 <xsl:template match="*" mode="charcount">
1390 <xsl:param name="incurrent_length" select="0"/>
1391 <xsl:param name="nosibling" select="0"/>
1392  <xsl:choose>
1393   <xsl:when test="count(child::*) = 0">
1394    <xsl:value-of select="$incurrent_length"/>
1395   </xsl:when>
1396   <xsl:otherwise>
1397     <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>
1398     <xsl:choose>
1399     <xsl:when test="$framewidth > number($childlength) and ($nosibling = 0)">
1400      <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>
1401      <xsl:choose>
1402      <xsl:when test="string($siblength) = &quot;&quot;">
1403       <xsl:value-of select="number($childlength)"/>
1404      </xsl:when>
1405      <xsl:otherwise>
1406       <xsl:value-of select="number($siblength)"/>
1407      </xsl:otherwise>
1408      </xsl:choose>>
1409     </xsl:when>
1410     <xsl:otherwise>
1411      <xsl:value-of select="number($childlength)"/>
1412     </xsl:otherwise>
1413     </xsl:choose>
1414   </xsl:otherwise>
1415  </xsl:choose>
1416 </xsl:template>
1417
1418 </xsl:stylesheet>
1419