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="30"/>
  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             <xsl:apply-templates select="*[position()=3]"/>
 807            </m:mrow>
 808           </m:mtd>
 809          </m:mtr>
 810         </m:mtable>
 811       </xsl:when>
 812       <xsl:when test="$name='letin'">
 813         <m:mtable align="baseline 1" equalrows="false" columnalign="left">
 814          <!-- <xsl:for-each select="APPLY[m:csymbol and (string(m:csymbol)='let')]"> -->
 815          <xsl:for-each select="*[(last() > position()) and (position()>1)]">
 816          <m:mtr>
 817           <m:mtd>
 818            <m:mrow>
 819             <xsl:apply-templates select="."/>
 820            </m:mrow>
 821           </m:mtd>
 822          </m:mtr>
 823          </xsl:for-each>
 824          <m:mtr>
 825           <m:mtd>
 826            <m:mrow>
 827             <xsl:apply-templates select="*[position()=last()]"/>
 828            </m:mrow>
 829           </m:mtd>
 830          </m:mtr>
 831         </m:mtable>
 832       </xsl:when>
 833       <xsl:when test="$name='let'">
 834        <m:mtext>(</m:mtext>
 835        <xsl:apply-templates select="m:ci"/>
 836        <m:mtext>) </m:mtext>
 837        <xsl:apply-templates select="*[3]"/>
 838       </xsl:when>
 839       <xsl:when test="$name='thread'">
 840         <m:mtable align="baseline 1" equalrows="false" columnalign="left">
 841          <m:mtr>
 842           <m:mtd>
 843            <m:mrow>
 844             <xsl:choose>
 845              <xsl:when test="name(*[last()])='m:apply'">
 846               <xsl:apply-templates select="*[last()]"/>
 847              </xsl:when>
 848              <xsl:otherwise>
 849               <m:mtext>Consider </m:mtext>
 850               <xsl:apply-templates select="*[last()]"/>
 851              </xsl:otherwise>
 852             </xsl:choose>
 853            </m:mrow>
 854           </m:mtd>
 855          </m:mtr>
 856          <xsl:apply-templates mode="thread" select="*[(last()-2)]"/>
 857         </m:mtable>
 858       </xsl:when>
 859       <xsl:when test="$name='rewrite_and_apply'">
 860         <m:mtable>
 861          <m:mtr>
 862           <m:mtd>
 863            <m:mrow>
 864             <m:mtext>Rewrite</m:mtext>
 865             <m:mphantom><m:mtext>_</m:mtext></m:mphantom>
 866             <xsl:apply-templates select="*[2]/*[2]"/>
 867             <m:mphantom><m:mtext>_</m:mtext></m:mphantom>
 868             <m:mtext>with</m:mtext>
 869             <m:mphantom><m:mtext>_</m:mtext></m:mphantom>
 870             <xsl:apply-templates select="*[2]/*[3]"/>
 871             <m:mphantom><m:mtext>_</m:mtext></m:mphantom>
 872             <m:mtext>by</m:mtext>
 873             <m:mphantom><m:mtext>_</m:mtext></m:mphantom>
 874             <xsl:apply-templates select="*[2]/*[4]"/>
 875             <m:mphantom><m:mtext>_</m:mtext></m:mphantom>
 876             <m:mtext>in</m:mtext>
 877             <m:mphantom><m:mtext>_</m:mtext></m:mphantom>
 878             <xsl:apply-templates select="*[3]"/>
 879             <m:mphantom><m:mtext>_</m:mtext></m:mphantom>
 880             <m:mtext>and apply</m:mtext>
 881             <m:mphantom><m:mtext>_</m:mtext></m:mphantom>
 882             <xsl:apply-templates select="*[position()>3]"/>
 883            </m:mrow>
 884           </m:mtd>
 885          </m:mtr>
 886        </m:mtable>
 887       </xsl:when>
 888       <xsl:when test="$name='and_ind'">
 889         <m:mtable align="baseline 1" equalrows="false" columnalign="left">
 890          <m:mtr>
 891           <m:mtd>
 892            <m:mrow>
 893             <xsl:choose>
 894              <xsl:when test="name(*[2])='m:apply'">
 895               <xsl:apply-templates select="*[2]"/>
 896              </xsl:when>
 897              <xsl:otherwise>
 898               <m:mtext>Consider </m:mtext>
 899               <xsl:apply-templates select="*[2]"/>
 900              </xsl:otherwise>
 901             </xsl:choose>
 902            </m:mrow>
 903           </m:mtd>
 904          </m:mtr>
 905          <m:mtr>
 906           <m:mtd>
 907            <m:mtext>In particular, we have</m:mtext>
 908           </m:mtd>
 909          </m:mtr>
 910          <m:mtr>
 911           <m:mtd>
 912            <m:mrow>
 913             <m:mtext>(</m:mtext>
 914             <xsl:apply-templates select="*[3]"/>
 915             <m:mtext>)</m:mtext>
 916             <xsl:apply-templates select="*[4]"/>
 917             </m:mrow>
 918           </m:mtd>
 919          </m:mtr>
 920          <m:mtr>
 921           <m:mtd>
 922            <m:mrow>
 923             <m:mtext>(</m:mtext>
 924             <xsl:apply-templates select="*[5]"/>
 925             <m:mtext>)</m:mtext>
 926             <xsl:apply-templates select="*[6]"/>
 927             </m:mrow>
 928           </m:mtd>
 929          </m:mtr>
 930          <m:mtr>
 931           <m:mtd>
 932            <m:mrow>
 933             <xsl:apply-templates select="*[7]"/>
 934            </m:mrow>
 935           </m:mtd>
 936          </m:mtr>
 937         </m:mtable>
 938       </xsl:when>
 939       <xsl:when test="$name='or_ind'">
 940         <m:mtable align="baseline 1" equalrows="false" columnalign="left">
 941          <m:mtr>
 942           <m:mtd>
 943            <m:mrow>
 944             <xsl:choose>
 945              <xsl:when test="name(*[2])='m:apply'">
 946               <xsl:apply-templates select="*[2]"/>
 947              </xsl:when>
 948              <xsl:otherwise>
 949               <m:mtext>Consider</m:mtext>
 950               <m:mphantom><m:mtext>_</m:mtext></m:mphantom>
 951               <xsl:apply-templates select="*[2]"/>
 952              </xsl:otherwise>
 953             </xsl:choose>
 954            </m:mrow>
 955           </m:mtd>
 956          </m:mtr>
 957          <m:mtr>
 958           <m:mtd>
 959            <m:mtext>We prove</m:mtext>
 960            <m:mphantom><m:mtext>_</m:mtext></m:mphantom>
 961            <xsl:apply-templates select="*[3]"/>
 962            <m:mphantom><m:mtext>_</m:mtext></m:mphantom>
 963            <m:mtext>by cases:</m:mtext>
 964           </m:mtd>
 965          </m:mtr>
 966          <m:mtr>
 967           <m:mtd>
 968            <m:mrow>
 969             <m:mtext>*</m:mtext>
 970             <xsl:apply-templates select="*[4]"/>
 971            </m:mrow>
 972           </m:mtd>
 973          </m:mtr>
 974          <m:mtr>
 975           <m:mtd>
 976            <m:mrow>
 977             <m:mtext>*</m:mtext>
 978             <xsl:apply-templates select="*[5]"/>
 979            </m:mrow>
 980           </m:mtd>
 981          </m:mtr>
 982         </m:mtable>
 983       </xsl:when>
 984       <xsl:otherwise>
 985        <m:ci>ERROR</m:ci>
 986       </xsl:otherwise>
 987      </xsl:choose>
 988     </m:mrow>
 989 </xsl:template>
 990
 991 <xsl:template match="*" mode="thread">
 992  <xsl:variable name="name"><xsl:value-of select="following-sibling::*[position()=1]/m:csymbol"/></xsl:variable>
 993  <xsl:choose>
 994   <xsl:when test="$name='rw_step'">
 995          <m:mtr>
 996           <m:mtd>
 997            <m:mrow>
 998             <m:mtext>Rewrite</m:mtext>
 999             <m:mphantom><m:mtext>_</m:mtext></m:mphantom>
1000             <xsl:apply-templates select="following-sibling::*[position()=1]/*[2]"/>
1001             <m:mphantom><m:mtext>_</m:mtext></m:mphantom>
1002             <m:mtext>with</m:mtext>
1003             <m:mphantom><m:mtext>_</m:mtext></m:mphantom>
1004             <xsl:apply-templates select="following-sibling::*[position()=1]/*[3]"/>
1005             <m:mphantom><m:mtext>_</m:mtext></m:mphantom>
1006             <m:mtext>by</m:mtext>
1007             <m:mphantom><m:mtext>_</m:mtext></m:mphantom>
1008             <xsl:apply-templates select="following-sibling::*[position()=1]/*[4]"/>
1009            </m:mrow>
1010           </m:mtd>
1011          </m:mtr>
1012          <m:mtr>
1013           <m:mtd>
1014            <m:mrow>
1015             <xsl:apply-templates select="."/>
1016            </m:mrow>
1017           </m:mtd>
1018          </m:mtr>
1019    </xsl:when>
1020    <xsl:otherwise>
1021          <m:mtr>
1022           <m:mtd>
1023            <m:mrow>
1024             <xsl:apply-templates select="following-sibling::*[position()=1]"/>
1025            </m:mrow>
1026           </m:mtd>
1027          </m:mtr>
1028          <m:mtr>
1029           <m:mtd>
1030            <m:mrow>
1031             <xsl:apply-templates select="."/>
1032            </m:mrow>
1033           </m:mtd>
1034          </m:mtr>
1035     </xsl:otherwise>
1036    </xsl:choose>
1037          <xsl:apply-templates mode="thread" select="preceding-sibling::*[position()=2]"/>
1038 </xsl:template>
1039
1040
1041 <!-- LAMBDA -->
1042
1043 <xsl:template match="m:lambda">
1044     <xsl:variable name="charlength"><xsl:apply-templates select="*[position()=1]" mode="charcount"/></xsl:variable>
1045     <m:mrow helm:xref="{@helm:xref}">
1046      <xsl:choose>
1047      <xsl:when test="$charlength >= $framewidth">
1048       <m:mtable align="baseline 1" equalrows="false" columnalign="left">
1049         <m:mtr>
1050           <m:mtd>
1051             <m:mo color="Red">&#x03bb;</m:mo>
1052             <xsl:apply-templates select="m:bvar"/>
1053           </m:mtd>
1054          </m:mtr>
1055        <m:mtr>
1056         <m:mtd>
1057          <m:mrow>
1058           <m:mo>.</m:mo>
1059           <xsl:apply-templates select="*[position()=2]"/>
1060          </m:mrow>
1061         </m:mtd>
1062        </m:mtr>
1063       </m:mtable>
1064      </xsl:when>
1065      <xsl:otherwise>
1066       <m:mo color="Red">&#x03bb;</m:mo>
1067       <xsl:apply-templates select="m:bvar/m:ci"/>
1068       <m:mo>:</m:mo>
1069       <xsl:apply-templates select="m:bvar/m:type"/>
1070       <m:mo>.</m:mo>
1071       <xsl:apply-templates select="*[position()=2]"/>
1072      </xsl:otherwise>
1073      </xsl:choose>
1074     </m:mrow>
1075 </xsl:template>
1076
1077 <!-- *********************************** -->
1078 <!-- BASE SET OF MATHML CONTENT ELEMENTS -->
1079 <!-- *********************************** -->
1080
1081 <!-- Logic -->
1082
1083 <xsl:template match = "m:apply[m:eq[1]]">
1084  <xsl:variable name="charlength">
1085   <xsl:apply-templates select="*[1]" mode="charcount"/>
1086  </xsl:variable>
1087  <xsl:choose>
1088   <xsl:when test="$charlength >= $framewidth">
1089    <m:mtable align="baseline 1" equalrows="false" columnalign="left">
1090     <xsl:if test="@helm:xref">
1091      <xsl:attribute name="helm:xref">
1092       <xsl:value-of select="@helm:xref"/>
1093      </xsl:attribute>
1094     </xsl:if>
1095     <m:mtr>
1096      <m:mtd>
1097       <m:mo stretchy="false">(</m:mo>
1098       <xsl:apply-templates select="*[position()=2]"/>
1099      </m:mtd>
1100     </m:mtr>
1101     <xsl:for-each select = "*[position()>2]">
1102      <m:mtr>
1103       <m:mtd>
1104        <m:mphantom><m:mtext>__</m:mtext></m:mphantom>
1105        <m:mo helm:xref="m:in/@helm:xref">
1106         =
1107        </m:mo>
1108        <xsl:apply-templates select="."/>
1109       </m:mtd>
1110      </m:mtr>
1111     </xsl:for-each>
1112     <m:mtr>
1113      <m:mtd>
1114       <m:mo stretchy="false">)</m:mo>
1115      </m:mtd>
1116     </m:mtr>
1117    </m:mtable>
1118   </xsl:when>
1119   <xsl:otherwise>
1120    <xsl:apply-imports/>
1121   </xsl:otherwise>
1122  </xsl:choose>
1123 </xsl:template>
1124
1125
1126 <xsl:template match = "m:apply[m:and[1]|m:or[1]
1127           |m:geq[1]|m:leq[1]|m:gt[1]|m:lt[1]
1128           |m:in[1]|m:intesect[1]|m:union[1]|m:subset[1]
1129           |m:prsubset|m:setdiff[1]]">
1130  <xsl:variable name="symbol">
1131   <xsl:choose>
1132    <xsl:when test="m:and[1]">
1133     <xsl:value-of select="'wedge'"/>
1134    </xsl:when>
1135    <xsl:when test="m:or[1]">
1136     <xsl:value-of select="'vee'"/>
1137    </xsl:when>
1138    <xsl:when test="m:geq[1]">
1139     <xsl:value-of select="'geq'"/>
1140    </xsl:when>
1141    <xsl:when test="m:leq[1]">
1142     <xsl:value-of select="'leq'"/>
1143    </xsl:when>
1144    <xsl:when test="m:gt[1]">
1145     <xsl:value-of select="'gt'"/>
1146    </xsl:when>
1147    <xsl:when test="m:lt[1]">
1148     <xsl:value-of select="'lt'"/>
1149    </xsl:when>
1150    <xsl:when test="m:eq[1]">
1151     <xsl:value-of select="'Equal'"/>
1152    </xsl:when>
1153    <xsl:when test="m:in[1]">
1154     <xsl:value-of select="'Element'"/>
1155    </xsl:when>
1156    <xsl:when test="m:subset[1]">
1157     <xsl:value-of select="'SubsetEqual'"/>
1158    </xsl:when>
1159    <xsl:when test="m:prsubset[1]">
1160     <xsl:value-of select="'subset'"/>
1161    </xsl:when>
1162    <xsl:when test="m:intersect[1]">
1163     <xsl:value-of select="'Intersection'"/>
1164    </xsl:when>
1165    <xsl:when test="m:union[1]">
1166     <xsl:value-of select="'Union'"/>
1167    </xsl:when>
1168    <xsl:when test="m:setdiff[1]">
1169     <xsl:value-of select="'Backslash'"/>
1170    </xsl:when>
1171   </xsl:choose>
1172  </xsl:variable>
1173  <xsl:variable name="charlength">
1174   <xsl:apply-templates select="*[1]" mode="charcount"/>
1175  </xsl:variable>
1176  <xsl:choose>
1177   <xsl:when test="$charlength >= $framewidth">
1178    <m:mtable align="baseline 1" equalrows="false" columnalign="left">
1179     <xsl:if test="@helm:xref">
1180      <xsl:attribute name="helm:xref">
1181       <xsl:value-of select="@helm:xref"/>
1182      </xsl:attribute>
1183     </xsl:if>
1184     <m:mtr>
1185      <m:mtd>
1186       <m:mo stretchy="false">(</m:mo>
1187       <xsl:apply-templates select="*[position()=2]"/>
1188      </m:mtd>
1189     </m:mtr>
1190     <xsl:for-each select = "*[position()>2]">
1191      <m:mtr>
1192       <m:mtd>
1193        <m:mphantom><m:mtext>__</m:mtext></m:mphantom>
1194        <m:mo helm:xref="{*[1]/@helm:xref}">
1195         <m:mchar name="{$symbol}"/>
1196        </m:mo>
1197        <xsl:apply-templates select="."/>
1198       </m:mtd>
1199      </m:mtr>
1200     </xsl:for-each>
1201     <m:mtr>
1202      <m:mtd>
1203       <m:mo stretchy="false">)</m:mo>
1204      </m:mtd>
1205     </m:mtr>
1206    </m:mtable>
1207   </xsl:when>
1208   <xsl:otherwise>
1209    <xsl:apply-imports/>
1210   </xsl:otherwise>
1211  </xsl:choose>
1212 </xsl:template>
1213
1214 <xsl:template match = "m:set">
1215  <xsl:choose>
1216   <xsl:when test="count(child::*) = 0">
1217    <m:mo>
1218     <m:mchar name="EmptySet"/>
1219    </m:mo>
1220   </xsl:when>
1221   <xsl:otherwise>
1222    <xsl:variable name="charlength">
1223     <xsl:apply-templates select="*[1]" mode="charcount"/>
1224    </xsl:variable>
1225    <xsl:choose>
1226     <xsl:when test="$charlength >= $framewidth">
1227      <xsl:choose>
1228       <xsl:when test="name(*[1]) = 'm:bvar'">
1229        <m:mtable align="baseline 1" equalrows="false" columnalign="left">
1230         <m:mtr>
1231          <m:mtd>
1232           <m:mo stretchy="false">{</m:mo>
1233           <xsl:apply-templates select="*[position()=1]"/>
1234          </m:mtd>
1235         </m:mtr>
1236         <m:mtr>
1237          <m:mtd>
1238           <m:mphantom><m:mtext>{</m:mtext></m:mphantom>
1239           <m:mo stretchy="false">|</m:mo>
1240           <xsl:apply-templates select="m:condition/*[1]"/>
1241          </m:mtd>
1242         </m:mtr>
1243         <m:mtr>
1244          <m:mtd>
1245           <m:mo stretchy="false">}</m:mo>
1246          </m:mtd>
1247         </m:mtr>
1248        </m:mtable>
1249       </xsl:when>
1250       <xsl:otherwise>
1251        <m:mtable align="baseline 1" equalrows="false" columnalign="left">
1252         <m:mtr>
1253          <m:mtd>
1254           <m:mo stretchy="false">{</m:mo>
1255           <xsl:apply-templates select="*[position()=1]"/>
1256           <xsl:if test="position() != last()">
1257            <mo>,</mo>
1258           </xsl:if>
1259          </m:mtd>
1260         </m:mtr>
1261         <xsl:for-each select = "*[position()>2]">
1262          <m:mtr>
1263           <m:mtd>
1264            <m:mphantom><m:mtext>{</m:mtext></m:mphantom>
1265            <xsl:apply-templates select="."/>
1266            <xsl:if test="position() != last()">
1267             <mo>,</mo>
1268            </xsl:if>
1269           </m:mtd>
1270          </m:mtr>
1271         </xsl:for-each>
1272         <m:mtr>
1273          <m:mtd>
1274           <m:mo stretchy="false">}</m:mo>
1275          </m:mtd>
1276         </m:mtr>
1277        </m:mtable>
1278       </xsl:otherwise>
1279      </xsl:choose>
1280     </xsl:when>
1281     <xsl:otherwise>
1282      <xsl:apply-imports/>
1283     </xsl:otherwise>
1284    </xsl:choose>
1285   </xsl:otherwise>
1286  </xsl:choose>
1287 </xsl:template>
1288
1289 <xsl:template match = "m:apply[m:card[1]]">
1290  <m:mo stretchy="false">|</m:mo>
1291   <xsl:apply-templates select="*[2]"/>
1292  <m:mo stretchy="false">|</m:mo>
1293 </xsl:template>
1294
1295 <!-- *********************************** -->
1296 <!--          PROOF ELEMENTS             -->
1297 <!-- *********************************** -->
1298
1299
1300
1301 <!--**********************-->
1302 <!--       COUNTING       -->
1303 <!--**********************-->
1304
1305 <xsl:template match="m:cn|m:and|m:or|m:not|m:exists|m:eq|m:lt|m:leq|m:gt|m:geq
1306  |m:in|m:notin|m:intersect|m:union|m:subset|m:prsubset|m:card|m:setdiff
1307  |m:plus|m:minus|m:times" mode="charcount">
1308 <xsl:param name="incurrent_length" select="0"/>
1309     <xsl:choose>
1310     <xsl:when test="$framewidth > ($incurrent_length + 3 + string-length())">
1311      <xsl:variable name="siblength">
1312       <xsl:apply-templates select="following-sibling::*[position()=1]" mode="charcount">
1313        <xsl:with-param name="incurrent_length" select="$incurrent_length + string-length()"/>
1314       </xsl:apply-templates>
1315      </xsl:variable>
1316      <xsl:choose>
1317      <xsl:when test="string($siblength) = &quot;&quot;">
1318       <xsl:value-of select="$incurrent_length + 3 + string-length()"/>
1319      </xsl:when>
1320      <xsl:otherwise>
1321       <xsl:value-of select="number($siblength)"/>
1322      </xsl:otherwise>
1323      </xsl:choose>
1324     </xsl:when>
1325     <xsl:otherwise>
1326      <xsl:value-of select="$incurrent_length + 3 + string-length()"/>
1327     </xsl:otherwise>
1328     </xsl:choose>
1329 </xsl:template>
1330
1331 <xsl:template match="m:ci|m:csymbol" mode="charcount">
1332 <xsl:param name="incurrent_length" select="0"/>
1333 <xsl:param name="nosibling" select="0"/>
1334     <xsl:choose>
1335     <xsl:when test="$framewidth > ($incurrent_length + string-length()) and ($nosibling = 0)">
1336      <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>
1337      <xsl:choose>
1338      <xsl:when test="string($siblength) = &quot;&quot;">
1339       <xsl:value-of select="$incurrent_length + string-length()"/>
1340      </xsl:when>
1341      <xsl:otherwise>
1342       <xsl:value-of select="number($siblength)"/>
1343      </xsl:otherwise>
1344      </xsl:choose>
1345     </xsl:when>
1346     <xsl:otherwise>
1347      <xsl:value-of select="$incurrent_length + string-length()"/>
1348     </xsl:otherwise>
1349     </xsl:choose>
1350 </xsl:template>
1351
1352 <xsl:template match="*" mode="charcount">
1353 <xsl:param name="incurrent_length" select="0"/>
1354 <xsl:param name="nosibling" select="0"/>
1355  <xsl:choose>
1356   <xsl:when test="count(child::*) = 0">
1357    <xsl:value-of select="$incurrent_length"/>
1358   </xsl:when>
1359   <xsl:otherwise>
1360     <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>
1361     <xsl:choose>
1362     <xsl:when test="$framewidth > number($childlength) and ($nosibling = 0)">
1363      <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>
1364      <xsl:choose>
1365      <xsl:when test="string($siblength) = &quot;&quot;">
1366       <xsl:value-of select="number($childlength)"/>
1367      </xsl:when>
1368      <xsl:otherwise>
1369       <xsl:value-of select="number($siblength)"/>
1370      </xsl:otherwise>
1371      </xsl:choose>>
1372     </xsl:when>
1373     <xsl:otherwise>
1374      <xsl:value-of select="number($childlength)"/>
1375     </xsl:otherwise>
1376     </xsl:choose>
1377   </xsl:otherwise>
1378  </xsl:choose>
1379 </xsl:template>
1380
1381 </xsl:stylesheet>
1382