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