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='prod'">
 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">&#x03a0;</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">&#x03a0;</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='arrow'">
 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:mrow>
 389             <m:mo stretchy="false">(</m:mo>
 390             <xsl:apply-templates select="*[position()=2]"/>
 391            </m:mrow>
 392           </m:mtd>
 393          </m:mtr>
 394          <m:mtr>
 395           <m:mtd>
 396            <m:mrow>
 397             <m:mo color="Blue">&#x2192;</m:mo>
 398             <xsl:apply-templates select="*[position()=3]"/>
 399            </m:mrow>
 400           </m:mtd>
 401          </m:mtr>
 402          <m:mtr>
 403           <m:mtd>
 404            <m:mrow>
 405             <m:mo stretchy="false">)</m:mo>
 406            </m:mrow>
 407           </m:mtd>
 408          </m:mtr>
 409         </m:mtable>
 410        </xsl:when>
 411        <xsl:otherwise>
 412         <m:mo stretchy="false">(</m:mo>
 413         <xsl:apply-templates select="*[position()=2]"/>
 414         <m:mo color="Blue">&#x2192;</m:mo>
 415         <xsl:apply-templates select="*[position()=3]"/>
 416         <m:mo stretchy="false">)</m:mo>
 417        </xsl:otherwise>
 418        </xsl:choose>
 419       </xsl:when>
 420       <xsl:when test="$name='app'">
 421        <xsl:choose>
 422        <xsl:when test="$charlength >= $framewidth">
 423         <m:mtable align="baseline 1" equalrows="false" columnalign="left">
 424          <m:mtr>
 425           <m:mtd>
 426            <m:mrow>
 427             <m:mo stretchy="false">(</m:mo>
 428             <xsl:apply-templates select="*[position()=2]"/>
 429            </m:mrow>
 430           </m:mtd>
 431          </m:mtr>
 432          <xsl:for-each select="*[position()>2]">
 433          <m:mtr>
 434           <m:mtd>
 435            <m:mrow>
 436             <m:mphantom><m:mtext>(</m:mtext></m:mphantom>
 437             <xsl:apply-templates select="."/>
 438            </m:mrow>
 439           </m:mtd>
 440          </m:mtr>
 441          </xsl:for-each>
 442          <m:mtr>
 443           <m:mtd>
 444            <m:mrow>
 445             <m:mo stretchy="false">)</m:mo>
 446            </m:mrow>
 447           </m:mtd>
 448          </m:mtr>
 449         </m:mtable>
 450        </xsl:when>
 451        <xsl:otherwise>
 452         <m:mo stretchy="false">(</m:mo>
 453         <xsl:apply-templates select="*[position()=2]"/>
 454         <xsl:for-each select="*[position()>2]">
 455          <m:mphantom><m:mtext>_</m:mtext></m:mphantom>
 456          <xsl:apply-templates select="."/>
 457         </xsl:for-each>
 458         <m:mo stretchy="false">)</m:mo>
 459        </xsl:otherwise>
 460        </xsl:choose>
 461       </xsl:when>
 462       <xsl:when test="$name='cast'">
 463        <xsl:choose>
 464        <xsl:when test="$charlength >= $framewidth">
 465         <m:mtable align="baseline 1" equalrows="false" columnalign="left">
 466          <m:mtr>
 467           <m:mtd>
 468            <m:mrow>
 469             <m:mo stretchy="false">(</m:mo>
 470             <xsl:apply-templates select="*[position()=2]"/>
 471            </m:mrow>
 472           </m:mtd>
 473          </m:mtr>
 474          <m:mtr>
 475           <m:mtd>
 476            <m:mrow>
 477             <m:mo color="#b03060">:></m:mo>
 478             <xsl:apply-templates select="*[position()=3]"/>
 479            </m:mrow>
 480           </m:mtd>
 481          </m:mtr>
 482          <m:mtr>
 483           <m:mtd>
 484            <m:mrow>
 485             <m:mo stretchy="false">)</m:mo>
 486            </m:mrow>
 487           </m:mtd>
 488          </m:mtr>
 489         </m:mtable>
 490        </xsl:when>
 491        <xsl:otherwise>
 492         <m:mo stretchy="false">(</m:mo>
 493         <xsl:apply-templates select="*[position()=2]"/>
 494         <m:mo color="#b03060">:></m:mo>
 495         <xsl:apply-templates select="*[position()=3]"/>
 496         <m:mo stretchy="false">)</m:mo>
 497        </xsl:otherwise>
 498        </xsl:choose>
 499       </xsl:when>
 500       <xsl:when test="$name='Prop'">
 501        <m:mo>Prop</m:mo>
 502       </xsl:when>
 503       <xsl:when test="$name='Set'">
 504        <m:mo>Set</m:mo>
 505       </xsl:when>
 506       <xsl:when test="$name='Type'">
 507        <m:mo>Type</m:mo>
 508       </xsl:when>
 509       <xsl:when test="$name='mutcase'">
 510        <xsl:choose>
 511        <xsl:when test="$charlength >= $framewidth">
 512         <xsl:variable name="charlength"><xsl:apply-templates select="*[position()=2]" mode="charcount"><xsl:with-param name="nosibling" select="1"/></xsl:apply-templates></xsl:variable>
 513         <m:mtable align="baseline 1" equalrows="false" columnalign="left">
 514          <m:mtr>
 515           <m:mtd>
 516            <m:mrow>
 517             <m:mo>&lt;</m:mo>
 518             <xsl:apply-templates select="*[position()=2]"/>
 519             <xsl:if test="$framewidth > $charlength">
 520              <m:mo>&gt;</m:mo>
 521              <m:mo>CASES</m:mo>
 522              <m:mphantom><m:mtext>_</m:mtext></m:mphantom>
 523              <xsl:apply-templates select="*[position()=3]"/>
 524             </xsl:if>
 525            </m:mrow>
 526           </m:mtd>
 527          </m:mtr>
 528          <xsl:if test="$charlength >= $framewidth">
 529          <m:mtr>
 530           <m:mtd>
 531            <m:mrow>
 532             <m:mo>&gt;</m:mo>
 533             <m:mo>CASES</m:mo>
 534             <m:mphantom><m:mtext>_</m:mtext></m:mphantom>
 535             <xsl:apply-templates select="*[position()=3]"/>
 536            </m:mrow>
 537           </m:mtd>
 538          </m:mtr>
 539          </xsl:if>
 540          <m:mtr>
 541           <m:mtd>
 542            <m:mrow>
 543             <m:mo>OF</m:mo>
 544            </m:mrow>
 545           </m:mtd>
 546          </m:mtr>
 547          <xsl:for-each select="*[position() mod 2 = 0 and position()>3]">
 548          <xsl:variable name="charlength"><xsl:apply-templates select="." mode="charcount"><xsl:with-param name="nosibling" select="1"/></xsl:apply-templates></xsl:variable>
 549          <m:mtr>
 550           <m:mtd>
 551            <m:mrow>
 552             <xsl:choose>
 553             <xsl:when test="position() = 1">
 554               <m:mphantom><m:mtext>|</m:mtext></m:mphantom>
 555             </xsl:when>
 556             <xsl:otherwise>
 557              <m:mo stretchy="false">|</m:mo>
 558             </xsl:otherwise>
 559             </xsl:choose>
 560             <m:mphantom><m:mtext>_</m:mtext></m:mphantom>
 561             <xsl:apply-templates select="."/>
 562             <xsl:if test="$framewidth > $charlength">
 563              <m:mo color="Green">&#x21d2;</m:mo>
 564              <xsl:apply-templates select="following-sibling::*[position()= 1]"/>
 565             </xsl:if>
 566            </m:mrow>
 567           </m:mtd>
 568          </m:mtr>
 569          <xsl:if test="$charlength >= $framewidth">
 570          <m:mtr>
 571           <m:mtd>
 572            <m:mrow>
 573             <m:mphantom><m:mtext>|_</m:mtext></m:mphantom>
 574             <m:mo color="Green">&#x21d2;</m:mo>
 575             <xsl:apply-templates select="following-sibling::*[position()= 1]"/>
 576            </m:mrow>
 577           </m:mtd>
 578          </m:mtr>
 579          </xsl:if>
 580         </xsl:for-each>
 581          <m:mtr>
 582           <m:mtd>
 583            <m:mrow>
 584             <m:mo>END</m:mo>
 585            </m:mrow>
 586           </m:mtd>
 587          </m:mtr>
 588         </m:mtable>
 589        </xsl:when>
 590        <xsl:otherwise>
 591         <m:mo>&lt;</m:mo><xsl:apply-templates select="*[position()=2]"/><m:mo>&gt;</m:mo>
 592         <m:mo>CASES</m:mo>
 593         <m:mphantom><m:mtext>_</m:mtext></m:mphantom>
 594         <xsl:apply-templates select="*[position()=3]"/>
 595         <m:mphantom><m:mtext>_</m:mtext></m:mphantom>
 596         <m:mo>OF</m:mo>
 597         <xsl:for-each select="*[position() mod 2 = 0 and position()>3]">
 598          <xsl:choose>
 599          <xsl:when test="position() != 1">
 600           <m:mo stretchy="false">|</m:mo>
 601          </xsl:when>
 602          </xsl:choose>
 603          <xsl:apply-templates select="."/>
 604          <m:mo color="Green">&#x21d2;</m:mo>
 605          <xsl:apply-templates select="following-sibling::*[position()= 1]"/>
 606         </xsl:for-each>
 607         <m:mphantom><m:mtext>_</m:mtext></m:mphantom>
 608         <m:mo>END</m:mo>
 609        </xsl:otherwise>
 610        </xsl:choose>
 611       </xsl:when>
 612       <xsl:when test="$name='fix'">
 613        <xsl:choose>
 614        <xsl:when test="$charlength >= $framewidth">
 615         <m:mtable align="baseline 1" equalrows="false" columnalign="left">
 616          <m:mtr>
 617           <m:mtd>
 618            <m:mrow>
 619             <m:mo>FIX</m:mo>
 620             <m:mphantom><m:mtext>_</m:mtext></m:mphantom>
 621             <m:mi><xsl:value-of select="m:ci"/></m:mi>
 622             <m:mo stretchy="false">{</m:mo>
 623            </m:mrow>
 624           </m:mtd>
 625          </m:mtr>
 626          <m:mtr>
 627           <m:mtd>
 628            <m:mrow>
 629             <m:mphantom><m:mtext>__</m:mtext></m:mphantom>
 630             <m:mtable align="baseline 1" equalrows="false" columnalign="left">
 631             <xsl:for-each select="m:bvar">
 632              <xsl:variable name="charlength"><xsl:apply-templates select="m:type" mode="charcount"><xsl:with-param name="nosibling" select="1"/></xsl:apply-templates></xsl:variable>
 633              <m:mtr>
 634               <m:mtd>
 635                <m:mrow>
 636                 <m:mi><xsl:value-of select="m:ci"/></m:mi>
 637                 <m:mo>:</m:mo>
 638                 <xsl:if test="$framewidth > $charlength">
 639                  <xsl:apply-templates select="m:type"/>
 640                 </xsl:if>
 641                </m:mrow>
 642               </m:mtd>
 643              </m:mtr>
 644              <xsl:if test="$charlength >= $framewidth">
 645              <m:mtr>
 646               <m:mtd>
 647                <m:mrow>
 648                 <m:mphantom><m:mtext>:=</m:mtext></m:mphantom>
 649                 <xsl:apply-templates select="m:type"/>
 650                </m:mrow>
 651               </m:mtd>
 652              </m:mtr>
 653              </xsl:if>
 654              <m:mtr>
 655               <m:mtd>
 656                <m:mrow>
 657                 <m:mo>:=</m:mo>
 658                 <xsl:apply-templates select="following-sibling::*[position()=1]"/>
 659                </m:mrow>
 660               </m:mtd>
 661              </m:mtr>
 662             </xsl:for-each>
 663             </m:mtable>
 664            </m:mrow>
 665           </m:mtd>
 666          </m:mtr>
 667          <m:mtr>
 668           <m:mtd>
 669            <m:mrow>
 670             <m:mo stretchy="false">}</m:mo>
 671            </m:mrow>
 672           </m:mtd>
 673          </m:mtr>
 674         </m:mtable>
 675        </xsl:when>
 676        <xsl:otherwise>
 677         <m:mo>FIX</m:mo>
 678         <m:mi><xsl:value-of select="m:ci"/></m:mi>
 679         <m:mo stretchy="false">{</m:mo>
 680         <m:mtable align="baseline 1" equalrows="false" columnalign="left">
 681         <xsl:for-each select="m:bvar">
 682          <m:mtr>
 683           <m:mtd>
 684            <m:mrow>
 685             <m:mi><xsl:value-of select="m:ci"/></m:mi>
 686             <m:mo>:</m:mo>
 687             <xsl:apply-templates select="m:type"/>
 688             <m:mo>:=</m:mo>
 689             <xsl:apply-templates select="following-sibling::*[position() = 1]"/>
 690             <xsl:if test="position()=last()">
 691              <m:mo stretchy="false">}</m:mo>
 692             </xsl:if>
 693            </m:mrow>
 694           </m:mtd>
 695          </m:mtr>
 696          </xsl:for-each>
 697         </m:mtable>
 698        </xsl:otherwise>
 699        </xsl:choose>
 700       </xsl:when>
 701       <xsl:when test="$name='cofix'">
 702        <xsl:choose>
 703        <xsl:when test="$charlength >= $framewidth">
 704         <m:mtable align="baseline 1" equalrows="false" columnalign="left">
 705          <m:mtr>
 706           <m:mtd>
 707            <m:mrow>
 708             <m:mo>COFIX</m:mo>
 709             <m:mphantom><m:mtext>_</m:mtext></m:mphantom>
 710             <m:mi><xsl:value-of select="m:ci"/></m:mi>
 711             <m:mo stretchy="false">{</m:mo>
 712            </m:mrow>
 713           </m:mtd>
 714          </m:mtr>
 715          <m:mtr>
 716           <m:mtd>
 717            <m:mrow>
 718             <m:mphantom><m:mtext>__</m:mtext></m:mphantom>
 719             <m:mtable align="baseline 1" equalrows="false" columnalign="left">
 720             <xsl:for-each select="m:bvar">
 721              <xsl:variable name="charlength"><xsl:apply-templates select="m:type" mode="charcount"><xsl:with-param name="nosibling" select="1"/></xsl:apply-templates></xsl:variable>
 722              <m:mtr>
 723               <m:mtd>
 724                <m:mrow>
 725                 <m:mi><xsl:value-of select="m:ci"/></m:mi>
 726                 <m:mo>:</m:mo>
 727                 <xsl:if test="$framewidth > $charlength">
 728                  <xsl:apply-templates select="m:type"/>
 729                 </xsl:if>
 730                </m:mrow>
 731               </m:mtd>
 732              </m:mtr>
 733              <xsl:if test="$charlength >= $framewidth">
 734              <m:mtr>
 735               <m:mtd>
 736                <m:mrow>
 737                 <m:mphantom><m:mtext>:=</m:mtext></m:mphantom>
 738                 <xsl:apply-templates select="m:type"/>
 739                </m:mrow>
 740               </m:mtd>
 741              </m:mtr>
 742              </xsl:if>
 743              <m:mtr>
 744               <m:mtd>
 745                <m:mrow>
 746                 <m:mo>:=</m:mo>
 747                 <xsl:apply-templates select="following-sibling::*[position() = 1]"/>
 748                </m:mrow>
 749               </m:mtd>
 750              </m:mtr>
 751             </xsl:for-each>
 752             </m:mtable>
 753            </m:mrow>
 754           </m:mtd>
 755          </m:mtr>
 756          <m:mtr>
 757           <m:mtd>
 758            <m:mrow>
 759             <m:mo stretchy="false">}</m:mo>
 760            </m:mrow>
 761           </m:mtd>
 762          </m:mtr>
 763         </m:mtable>
 764        </xsl:when>
 765        <xsl:otherwise>
 766         <m:mo>COFIX</m:mo>
 767         <m:mi><xsl:value-of select="m:ci"/></m:mi>
 768         <m:mo stretchy="false">{</m:mo>
 769         <m:mtable align="baseline 1" equalrows="false" columnalign="left">
 770         <xsl:for-each select="m:bvar">
 771          <m:mtr>
 772           <m:mtd>
 773            <m:mrow>
 774             <m:mi><xsl:value-of select="m:ci"/></m:mi>
 775             <m:mo>:</m:mo>
 776             <xsl:apply-templates select="m:type"/>
 777             <m:mo>:=</m:mo>
 778             <xsl:apply-templates select="following-sibling::*[position() = 1]"/>
 779             <xsl:if test="position()=last()">
 780              <m:mo stretchy="false">}</m:mo>
 781             </xsl:if>
 782            </m:mrow>
 783           </m:mtd>
 784          </m:mtr>
 785          </xsl:for-each>
 786         </m:mtable>
 787        </xsl:otherwise>
 788        </xsl:choose>
 789       </xsl:when>
 790       <!-- ***************************************** -->
 791       <!-- *********** PROOF ELEMENTS ************** -->
 792       <!-- ***************************************** -->
 793       <xsl:when test="$name='proof'">
 794         <m:mtable align="baseline 1" equalrows="false" columnalign="left">
 795          <m:mtr>
 796           <m:mtd>
 797            <m:mrow>
 798             <xsl:apply-templates select="*[position()=2]"/>
 799            </m:mrow>
 800           </m:mtd>
 801          </m:mtr>
 802          <m:mtr>
 803           <m:mtd>
 804            <m:mrow>
 805             <m:mtext color="#b03060">we proved </m:mtext>
 806             <m:mphantom><m:mtext>_</m:mtext></m:mphantom>
 807             <xsl:apply-templates select="*[position()=3]"/>
 808            </m:mrow>
 809           </m:mtd>
 810          </m:mtr>
 811         </m:mtable>
 812       </xsl:when>
 813       <xsl:when test="$name='letin'">
 814         <m:mtable align="baseline 1" equalrows="false" columnalign="left">
 815          <!-- <xsl:for-each select="APPLY[m:csymbol and (string(m:csymbol)='let')]"> -->
 816          <xsl:for-each select="*[(last() > position()) and (position()>1)]">
 817          <m:mtr>
 818           <m:mtd>
 819            <m:mrow>
 820             <xsl:apply-templates select="."/>
 821            </m:mrow>
 822           </m:mtd>
 823          </m:mtr>
 824          </xsl:for-each>
 825          <m:mtr>
 826           <m:mtd>
 827            <m:mrow>
 828             <xsl:apply-templates select="*[position()=last()]"/>
 829            </m:mrow>
 830           </m:mtd>
 831          </m:mtr>
 832         </m:mtable>
 833       </xsl:when>
 834       <xsl:when test="$name='let'">
 835        <m:mtext>(</m:mtext>
 836        <xsl:apply-templates select="m:ci"/>
 837        <m:mtext>) </m:mtext>
 838        <xsl:apply-templates select="*[3]"/>
 839       </xsl:when>
 840       <xsl:when test="$name='thread'">
 841         <m:mtable align="baseline 1" equalrows="false" columnalign="left">
 842          <m:mtr>
 843           <m:mtd>
 844            <m:mrow>
 845             <xsl:choose>
 846              <xsl:when test="name(*[last()])='m:apply'">
 847               <xsl:apply-templates select="*[last()]"/>
 848              </xsl:when>
 849              <xsl:otherwise>
 850               <m:mtext>Consider </m:mtext>
 851               <xsl:apply-templates select="*[last()]"/>
 852              </xsl:otherwise>
 853             </xsl:choose>
 854            </m:mrow>
 855           </m:mtd>
 856          </m:mtr>
 857          <xsl:apply-templates mode="thread" select="*[(last()-2)]"/>
 858         </m:mtable>
 859       </xsl:when>
 860       <xsl:when test="$name='rewrite_and_apply'">
 861         <m:mtable>
 862          <m:mtr>
 863           <m:mtd>
 864            <m:mrow>
 865             <m:mtext>Rewrite</m:mtext>
 866             <m:mphantom><m:mtext>_</m:mtext></m:mphantom>
 867             <xsl:apply-templates select="*[2]/*[2]"/>
 868             <m:mphantom><m:mtext>_</m:mtext></m:mphantom>
 869             <m:mtext>with</m:mtext>
 870             <m:mphantom><m:mtext>_</m:mtext></m:mphantom>
 871             <xsl:apply-templates select="*[2]/*[3]"/>
 872             <m:mphantom><m:mtext>_</m:mtext></m:mphantom>
 873             <m:mtext>by</m:mtext>
 874             <m:mphantom><m:mtext>_</m:mtext></m:mphantom>
 875             <xsl:apply-templates select="*[2]/*[4]"/>
 876             <m:mphantom><m:mtext>_</m:mtext></m:mphantom>
 877             <m:mtext>in</m:mtext>
 878             <m:mphantom><m:mtext>_</m:mtext></m:mphantom>
 879             <xsl:apply-templates select="*[3]"/>
 880             <m:mphantom><m:mtext>_</m:mtext></m:mphantom>
 881             <m:mtext>and apply</m:mtext>
 882             <m:mphantom><m:mtext>_</m:mtext></m:mphantom>
 883             <xsl:apply-templates select="*[position()>3]"/>
 884            </m:mrow>
 885           </m:mtd>
 886          </m:mtr>
 887        </m:mtable>
 888       </xsl:when>
 889       <xsl:when test="$name='and_ind'">
 890         <m:mtable align="baseline 1" equalrows="false" columnalign="left">
 891          <m:mtr>
 892           <m:mtd>
 893            <m:mrow>
 894             <xsl:choose>
 895              <xsl:when test="name(*[2])='m:apply'">
 896               <xsl:apply-templates select="*[2]"/>
 897              </xsl:when>
 898              <xsl:otherwise>
 899               <m:mtext>Consider </m:mtext>
 900               <xsl:apply-templates select="*[2]"/>
 901              </xsl:otherwise>
 902             </xsl:choose>
 903            </m:mrow>
 904           </m:mtd>
 905          </m:mtr>
 906          <m:mtr>
 907           <m:mtd>
 908            <m:mtext>In particular, we have</m:mtext>
 909           </m:mtd>
 910          </m:mtr>
 911          <m:mtr>
 912           <m:mtd>
 913            <m:mrow>
 914             <m:mtext>(</m:mtext>
 915             <xsl:apply-templates select="*[3]"/>
 916             <m:mtext>)</m:mtext>
 917             <m:mphantom><m:mtext>_</m:mtext></m:mphantom>
 918             <xsl:apply-templates select="*[4]"/>
 919             </m:mrow>
 920           </m:mtd>
 921          </m:mtr>
 922          <m:mtr>
 923           <m:mtd>
 924            <m:mrow>
 925             <m:mtext>(</m:mtext>
 926             <xsl:apply-templates select="*[5]"/>
 927             <m:mtext>)</m:mtext>
 928             <m:mphantom><m:mtext>_</m:mtext></m:mphantom>
 929             <xsl:apply-templates select="*[6]"/>
 930             </m:mrow>
 931           </m:mtd>
 932          </m:mtr>
 933          <m:mtr>
 934           <m:mtd>
 935            <m:mrow>
 936             <xsl:apply-templates select="*[7]"/>
 937            </m:mrow>
 938           </m:mtd>
 939          </m:mtr>
 940         </m:mtable>
 941       </xsl:when>
 942       <xsl:when test="$name='or_ind'">
 943         <m:mtable align="baseline 1" equalrows="false" columnalign="left">
 944          <m:mtr>
 945           <m:mtd>
 946            <m:mrow>
 947             <xsl:choose>
 948              <xsl:when test="name(*[2])='m:apply'">
 949               <xsl:apply-templates select="*[2]"/>
 950              </xsl:when>
 951              <xsl:otherwise>
 952               <m:mtext>Consider</m:mtext>
 953               <m:mphantom><m:mtext>_</m:mtext></m:mphantom>
 954               <xsl:apply-templates select="*[2]"/>
 955              </xsl:otherwise>
 956             </xsl:choose>
 957            </m:mrow>
 958           </m:mtd>
 959          </m:mtr>
 960          <m:mtr>
 961           <m:mtd>
 962            <m:mtext>We prove</m:mtext>
 963            <m:mphantom><m:mtext>_</m:mtext></m:mphantom>
 964            <xsl:apply-templates select="*[3]"/>
 965            <m:mphantom><m:mtext>_</m:mtext></m:mphantom>
 966            <m:mtext>by cases:</m:mtext>
 967           </m:mtd>
 968          </m:mtr>
 969          <m:mtr>
 970           <m:mtd>
 971            <m:mrow>
 972             <m:mtext>*</m:mtext>
 973             <xsl:apply-templates select="*[4]"/>
 974            </m:mrow>
 975           </m:mtd>
 976          </m:mtr>
 977          <m:mtr>
 978           <m:mtd>
 979            <m:mrow>
 980             <m:mtext>*</m:mtext>
 981             <xsl:apply-templates select="*[5]"/>
 982            </m:mrow>
 983           </m:mtd>
 984          </m:mtr>
 985         </m:mtable>
 986       </xsl:when>
 987       <xsl:otherwise>
 988        <m:ci>ERROR</m:ci>
 989       </xsl:otherwise>
 990      </xsl:choose>
 991     </m:mrow>
 992 </xsl:template>
 993
 994 <xsl:template match="*" mode="thread">
 995  <xsl:variable name="name"><xsl:value-of select="following-sibling::*[position()=1]/m:csymbol"/></xsl:variable>
 996  <xsl:choose>
 997   <xsl:when test="$name='rw_step'">
 998          <m:mtr>
 999           <m:mtd>
1000            <m:mrow>
1001             <m:mtext>Rewrite</m:mtext>
1002             <m:mphantom><m:mtext>_</m:mtext></m:mphantom>
1003             <xsl:apply-templates select="following-sibling::*[position()=1]/*[2]"/>
1004             <m:mphantom><m:mtext>_</m:mtext></m:mphantom>
1005             <m:mtext>with</m:mtext>
1006             <m:mphantom><m:mtext>_</m:mtext></m:mphantom>
1007             <xsl:apply-templates select="following-sibling::*[position()=1]/*[3]"/>
1008             <m:mphantom><m:mtext>_</m:mtext></m:mphantom>
1009             <m:mtext>by</m:mtext>
1010             <m:mphantom><m:mtext>_</m:mtext></m:mphantom>
1011             <xsl:apply-templates select="following-sibling::*[position()=1]/*[4]"/>
1012            </m:mrow>
1013           </m:mtd>
1014          </m:mtr>
1015          <m:mtr>
1016           <m:mtd>
1017            <m:mrow>
1018             <m:mtext color="#b03060">we get</m:mtext>
1019             <m:mphantom><m:mtext>_</m:mtext></m:mphantom>
1020             <xsl:apply-templates select="."/>
1021            </m:mrow>
1022           </m:mtd>
1023          </m:mtr>
1024    </xsl:when>
1025    <xsl:otherwise>
1026          <m:mtr>
1027           <m:mtd>
1028            <m:mrow>
1029             <xsl:apply-templates select="following-sibling::*[position()=1]"/>
1030            </m:mrow>
1031           </m:mtd>
1032          </m:mtr>
1033          <m:mtr>
1034           <m:mtd>
1035            <m:mrow>
1036             <m:mtext color="#b03060">we get</m:mtext>
1037             <m:mphantom><m:mtext>_</m:mtext></m:mphantom>
1038             <xsl:apply-templates select="."/>
1039            </m:mrow>
1040           </m:mtd>
1041          </m:mtr>
1042     </xsl:otherwise>
1043    </xsl:choose>
1044          <xsl:apply-templates mode="thread" select="preceding-sibling::*[position()=2]"/>
1045 </xsl:template>
1046
1047
1048 <!-- LAMBDA -->
1049
1050 <xsl:template match="m:lambda">
1051     <xsl:variable name="charlength"><xsl:apply-templates select="*[position()=1]" mode="charcount"/></xsl:variable>
1052     <m:mrow helm:xref="{@helm:xref}">
1053      <xsl:choose>
1054      <xsl:when test="$charlength >= $framewidth">
1055       <m:mtable align="baseline 1" equalrows="false" columnalign="left">
1056         <m:mtr>
1057           <m:mtd>
1058             <m:mo color="Red">&#x03bb;</m:mo>
1059             <xsl:apply-templates select="m:bvar"/>
1060           </m:mtd>
1061          </m:mtr>
1062        <m:mtr>
1063         <m:mtd>
1064          <m:mrow>
1065           <m:mo>.</m:mo>
1066           <xsl:apply-templates select="*[position()=2]"/>
1067          </m:mrow>
1068         </m:mtd>
1069        </m:mtr>
1070       </m:mtable>
1071      </xsl:when>
1072      <xsl:otherwise>
1073       <m:mo color="Red">&#x03bb;</m:mo>
1074       <xsl:apply-templates select="m:bvar/m:ci"/>
1075       <m:mo>:</m:mo>
1076       <xsl:apply-templates select="m:bvar/m:type"/>
1077       <m:mo>.</m:mo>
1078       <xsl:apply-templates select="*[position()=2]"/>
1079      </xsl:otherwise>
1080      </xsl:choose>
1081     </m:mrow>
1082 </xsl:template>
1083
1084 <!-- *********************************** -->
1085 <!-- BASE SET OF MATHML CONTENT ELEMENTS -->
1086 <!-- *********************************** -->
1087
1088 <!-- Logic -->
1089
1090 <xsl:template match = "m:apply[m:eq[1]]">
1091  <xsl:variable name="charlength">
1092   <xsl:apply-templates select="*[1]" mode="charcount"/>
1093  </xsl:variable>
1094  <xsl:choose>
1095   <xsl:when test="$charlength >= $framewidth">
1096    <m:mtable align="baseline 1" equalrows="false" columnalign="left">
1097     <xsl:if test="@helm:xref">
1098      <xsl:attribute name="helm:xref">
1099       <xsl:value-of select="@helm:xref"/>
1100      </xsl:attribute>
1101     </xsl:if>
1102     <m:mtr>
1103      <m:mtd>
1104       <m:mo stretchy="false">(</m:mo>
1105       <xsl:apply-templates select="*[position()=2]"/>
1106      </m:mtd>
1107     </m:mtr>
1108     <xsl:for-each select = "*[position()>2]">
1109      <m:mtr>
1110       <m:mtd>
1111        <m:mphantom><m:mtext>__</m:mtext></m:mphantom>
1112        <m:mo helm:xref="m:in/@helm:xref">
1113         =
1114        </m:mo>
1115        <xsl:apply-templates select="."/>
1116       </m:mtd>
1117      </m:mtr>
1118     </xsl:for-each>
1119     <m:mtr>
1120      <m:mtd>
1121       <m:mo stretchy="false">)</m:mo>
1122      </m:mtd>
1123     </m:mtr>
1124    </m:mtable>
1125   </xsl:when>
1126   <xsl:otherwise>
1127    <xsl:apply-imports/>
1128   </xsl:otherwise>
1129  </xsl:choose>
1130 </xsl:template>
1131
1132
1133 <xsl:template match = "m:apply[m:and[1]|m:or[1]
1134           |m:geq[1]|m:leq[1]|m:gt[1]|m:lt[1]
1135           |m:in[1]|m:intesect[1]|m:union[1]|m:subset[1]
1136           |m:prsubset|m:setdiff[1]]">
1137  <xsl:variable name="symbol">
1138   <xsl:choose>
1139    <xsl:when test="m:and[1]">
1140     <xsl:value-of select="'wedge'"/>
1141    </xsl:when>
1142    <xsl:when test="m:or[1]">
1143     <xsl:value-of select="'vee'"/>
1144    </xsl:when>
1145    <xsl:when test="m:geq[1]">
1146     <xsl:value-of select="'geq'"/>
1147    </xsl:when>
1148    <xsl:when test="m:leq[1]">
1149     <xsl:value-of select="'leq'"/>
1150    </xsl:when>
1151    <xsl:when test="m:gt[1]">
1152     <xsl:value-of select="'gt'"/>
1153    </xsl:when>
1154    <xsl:when test="m:lt[1]">
1155     <xsl:value-of select="'lt'"/>
1156    </xsl:when>
1157    <xsl:when test="m:eq[1]">
1158     <xsl:value-of select="'Equal'"/>
1159    </xsl:when>
1160    <xsl:when test="m:in[1]">
1161     <xsl:value-of select="'Element'"/>
1162    </xsl:when>
1163    <xsl:when test="m:subset[1]">
1164     <xsl:value-of select="'SubsetEqual'"/>
1165    </xsl:when>
1166    <xsl:when test="m:prsubset[1]">
1167     <xsl:value-of select="'subset'"/>
1168    </xsl:when>
1169    <xsl:when test="m:intersect[1]">
1170     <xsl:value-of select="'Intersection'"/>
1171    </xsl:when>
1172    <xsl:when test="m:union[1]">
1173     <xsl:value-of select="'Union'"/>
1174    </xsl:when>
1175    <xsl:when test="m:setdiff[1]">
1176     <xsl:value-of select="'Backslash'"/>
1177    </xsl:when>
1178   </xsl:choose>
1179  </xsl:variable>
1180  <xsl:variable name="charlength">
1181   <xsl:apply-templates select="*[1]" mode="charcount"/>
1182  </xsl:variable>
1183  <xsl:choose>
1184   <xsl:when test="$charlength >= $framewidth">
1185    <m:mtable align="baseline 1" equalrows="false" columnalign="left">
1186     <xsl:if test="@helm:xref">
1187      <xsl:attribute name="helm:xref">
1188       <xsl:value-of select="@helm:xref"/>
1189      </xsl:attribute>
1190     </xsl:if>
1191     <m:mtr>
1192      <m:mtd>
1193       <m:mo stretchy="false">(</m:mo>
1194       <xsl:apply-templates select="*[position()=2]"/>
1195      </m:mtd>
1196     </m:mtr>
1197     <xsl:for-each select = "*[position()>2]">
1198      <m:mtr>
1199       <m:mtd>
1200        <m:mphantom><m:mtext>__</m:mtext></m:mphantom>
1201        <m:mo helm:xref="{*[1]/@helm:xref}">
1202         <m:mchar name="{$symbol}"/>
1203        </m:mo>
1204        <xsl:apply-templates select="."/>
1205       </m:mtd>
1206      </m:mtr>
1207     </xsl:for-each>
1208     <m:mtr>
1209      <m:mtd>
1210       <m:mo stretchy="false">)</m:mo>
1211      </m:mtd>
1212     </m:mtr>
1213    </m:mtable>
1214   </xsl:when>
1215   <xsl:otherwise>
1216    <xsl:apply-imports/>
1217   </xsl:otherwise>
1218  </xsl:choose>
1219 </xsl:template>
1220
1221 <xsl:template match = "m:set">
1222  <xsl:choose>
1223   <xsl:when test="count(child::*) = 0">
1224    <m:mi>
1225     <m:mchar name="emptyset"/>
1226    </m:mi>
1227   </xsl:when>
1228   <xsl:otherwise>
1229    <xsl:variable name="charlength">
1230     <xsl:apply-templates select="*[1]" mode="charcount"/>
1231    </xsl:variable>
1232    <xsl:choose>
1233     <xsl:when test="$charlength >= $framewidth">
1234      <xsl:choose>
1235       <xsl:when test="name(*[1]) = 'm:bvar'">
1236        <m:mtable align="baseline 1" equalrows="false" columnalign="left">
1237         <m:mtr>
1238          <m:mtd>
1239           <m:mo stretchy="false">{</m:mo>
1240           <xsl:apply-templates select="*[position()=1]"/>
1241          </m:mtd>
1242         </m:mtr>
1243         <m:mtr>
1244          <m:mtd>
1245           <m:mphantom><m:mtext>{</m:mtext></m:mphantom>
1246           <m:mo stretchy="false">|</m:mo>
1247           <xsl:apply-templates select="m:condition/*[1]"/>
1248          </m:mtd>
1249         </m:mtr>
1250         <m:mtr>
1251          <m:mtd>
1252           <m:mo stretchy="false">}</m:mo>
1253          </m:mtd>
1254         </m:mtr>
1255        </m:mtable>
1256       </xsl:when>
1257       <xsl:otherwise>
1258        <m:mtable align="baseline 1" equalrows="false" columnalign="left">
1259         <m:mtr>
1260          <m:mtd>
1261           <m:mo stretchy="false">{</m:mo>
1262           <xsl:apply-templates select="*[position()=1]"/>
1263           <xsl:if test="position() != last()">
1264            <mo>,</mo>
1265           </xsl:if>
1266          </m:mtd>
1267         </m:mtr>
1268         <xsl:for-each select = "*[position()>2]">
1269          <m:mtr>
1270           <m:mtd>
1271            <m:mphantom><m:mtext>{</m:mtext></m:mphantom>
1272            <xsl:apply-templates select="."/>
1273            <xsl:if test="position() != last()">
1274             <mo>,</mo>
1275            </xsl:if>
1276           </m:mtd>
1277          </m:mtr>
1278         </xsl:for-each>
1279         <m:mtr>
1280          <m:mtd>
1281           <m:mo stretchy="false">}</m:mo>
1282          </m:mtd>
1283         </m:mtr>
1284        </m:mtable>
1285       </xsl:otherwise>
1286      </xsl:choose>
1287     </xsl:when>
1288     <xsl:otherwise>
1289      <xsl:apply-imports/>
1290     </xsl:otherwise>
1291    </xsl:choose>
1292   </xsl:otherwise>
1293  </xsl:choose>
1294 </xsl:template>
1295
1296 <xsl:template match = "m:apply[m:card[1]]">
1297  <m:mo stretchy="false">|</m:mo>
1298   <xsl:apply-templates select="*[2]"/>
1299  <m:mo stretchy="false">|</m:mo>
1300 </xsl:template>
1301
1302 <!-- *********************************** -->
1303 <!--          PROOF ELEMENTS             -->
1304 <!-- *********************************** -->
1305
1306
1307
1308 <!--**********************-->
1309 <!--       COUNTING       -->
1310 <!--**********************-->
1311
1312 <xsl:template match="m:cn|m:and|m:or|m:not|m:exists|m:eq|m:lt|m:leq|m:gt|m:geq
1313  |m:in|m:notin|m:intersect|m:union|m:subset|m:prsubset|m:card|m:setdiff
1314  |m:plus|m:minus|m:times" mode="charcount">
1315 <xsl:param name="incurrent_length" select="0"/>
1316     <xsl:choose>
1317     <xsl:when test="$framewidth > ($incurrent_length + 3 + string-length())">
1318      <xsl:variable name="siblength">
1319       <xsl:apply-templates select="following-sibling::*[position()=1]" mode="charcount">
1320        <xsl:with-param name="incurrent_length" select="$incurrent_length + string-length()"/>
1321       </xsl:apply-templates>
1322      </xsl:variable>
1323      <xsl:choose>
1324      <xsl:when test="string($siblength) = &quot;&quot;">
1325       <xsl:value-of select="$incurrent_length + 3 + string-length()"/>
1326      </xsl:when>
1327      <xsl:otherwise>
1328       <xsl:value-of select="number($siblength)"/>
1329      </xsl:otherwise>
1330      </xsl:choose>
1331     </xsl:when>
1332     <xsl:otherwise>
1333      <xsl:value-of select="$incurrent_length + 3 + string-length()"/>
1334     </xsl:otherwise>
1335     </xsl:choose>
1336 </xsl:template>
1337
1338 <xsl:template match="m:ci|m:csymbol" mode="charcount">
1339 <xsl:param name="incurrent_length" select="0"/>
1340 <xsl:param name="nosibling" select="0"/>
1341     <xsl:choose>
1342     <xsl:when test="$framewidth > ($incurrent_length + string-length()) and ($nosibling = 0)">
1343      <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>
1344      <xsl:choose>
1345      <xsl:when test="string($siblength) = &quot;&quot;">
1346       <xsl:value-of select="$incurrent_length + string-length()"/>
1347      </xsl:when>
1348      <xsl:otherwise>
1349       <xsl:value-of select="number($siblength)"/>
1350      </xsl:otherwise>
1351      </xsl:choose>
1352     </xsl:when>
1353     <xsl:otherwise>
1354      <xsl:value-of select="$incurrent_length + string-length()"/>
1355     </xsl:otherwise>
1356     </xsl:choose>
1357 </xsl:template>
1358
1359 <xsl:template match="*" mode="charcount">
1360 <xsl:param name="incurrent_length" select="0"/>
1361 <xsl:param name="nosibling" select="0"/>
1362  <xsl:choose>
1363   <xsl:when test="count(child::*) = 0">
1364    <xsl:value-of select="$incurrent_length"/>
1365   </xsl:when>
1366   <xsl:otherwise>
1367     <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>
1368     <xsl:choose>
1369     <xsl:when test="$framewidth > number($childlength) and ($nosibling = 0)">
1370      <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>
1371      <xsl:choose>
1372      <xsl:when test="string($siblength) = &quot;&quot;">
1373       <xsl:value-of select="number($childlength)"/>
1374      </xsl:when>
1375      <xsl:otherwise>
1376       <xsl:value-of select="number($siblength)"/>
1377      </xsl:otherwise>
1378      </xsl:choose>>
1379     </xsl:when>
1380     <xsl:otherwise>
1381      <xsl:value-of select="number($childlength)"/>
1382     </xsl:otherwise>
1383     </xsl:choose>
1384   </xsl:otherwise>
1385  </xsl:choose>
1386 </xsl:template>
1387
1388 </xsl:stylesheet>
1389