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