helm/style/mmlextension.xsl

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