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:otherwise>
1102        <m:ci>ERROR</m:ci>
1103       </xsl:otherwise>
1104      </xsl:choose>
1105     </m:mrow>
1106 </xsl:template>
1107
1108 <xsl:template match="*" mode="thread">
1109  <xsl:variable name="name"><xsl:value-of select="following-sibling::*[position()=1]/m:csymbol"/></xsl:variable>
1110  <xsl:choose>
1111   <xsl:when test="$name='rw_step'">
1112          <m:mtr>
1113           <m:mtd>
1114            <m:mrow>
1115             <m:mtext>Rewrite</m:mtext>
1116             <m:mphantom><m:mtext>_</m:mtext></m:mphantom>
1117             <xsl:apply-templates select="following-sibling::*[position()=1]/*[2]"/>
1118             <m:mphantom><m:mtext>_</m:mtext></m:mphantom>
1119             <m:mtext>with</m:mtext>
1120             <m:mphantom><m:mtext>_</m:mtext></m:mphantom>
1121             <xsl:apply-templates select="following-sibling::*[position()=1]/*[3]"/>
1122             <m:mphantom><m:mtext>_</m:mtext></m:mphantom>
1123             <m:mtext>by</m:mtext>
1124             <m:mphantom><m:mtext>_</m:mtext></m:mphantom>
1125             <xsl:apply-templates select="following-sibling::*[position()=1]/*[4]"/>
1126            </m:mrow>
1127           </m:mtd>
1128          </m:mtr>
1129          <m:mtr>
1130           <m:mtd>
1131            <m:mrow>
1132             <m:mtext mathcolor="Maroon">we get</m:mtext>
1133             <m:mphantom><m:mtext>_</m:mtext></m:mphantom>
1134             <xsl:apply-templates select="."/>
1135            </m:mrow>
1136           </m:mtd>
1137          </m:mtr>
1138    </xsl:when>
1139    <xsl:otherwise>
1140          <m:mtr>
1141           <m:mtd>
1142            <m:mrow>
1143             <xsl:apply-templates select="following-sibling::*[position()=1]"/>
1144            </m:mrow>
1145           </m:mtd>
1146          </m:mtr>
1147          <m:mtr>
1148           <m:mtd>
1149            <m:mrow>
1150             <m:mtext mathcolor="Maroon">we get</m:mtext>
1151             <m:mphantom><m:mtext>_</m:mtext></m:mphantom>
1152             <xsl:apply-templates select="."/>
1153            </m:mrow>
1154           </m:mtd>
1155          </m:mtr>
1156     </xsl:otherwise>
1157    </xsl:choose>
1158          <xsl:apply-templates mode="thread" select="preceding-sibling::*[position()=2]"/>
1159 </xsl:template>
1160
1161
1162 <!-- LAMBDA -->
1163
1164 <xsl:template match="m:lambda">
1165     <xsl:variable name="charlength"><xsl:apply-templates select="*[position()=1]" mode="charcount"/></xsl:variable>
1166     <m:mrow helm:xref="{@helm:xref}">
1167      <xsl:choose>
1168      <xsl:when test="$charlength >= $framewidth">
1169       <m:mtable align="baseline 1" equalrows="false" columnalign="left">
1170         <m:mtr>
1171           <m:mtd>
1172             <m:mo mathcolor="Red">&#x03bb;</m:mo>
1173             <xsl:apply-templates select="m:bvar"/>
1174           </m:mtd>
1175          </m:mtr>
1176        <m:mtr>
1177         <m:mtd>
1178          <m:mrow>
1179           <m:mo>.</m:mo>
1180           <xsl:apply-templates select="*[position()=2]"/>
1181          </m:mrow>
1182         </m:mtd>
1183        </m:mtr>
1184       </m:mtable>
1185      </xsl:when>
1186      <xsl:otherwise>
1187       <m:mo mathcolor="Red">&#x03bb;</m:mo>
1188       <xsl:apply-templates select="m:bvar/m:ci"/>
1189       <m:mo>:</m:mo>
1190       <xsl:apply-templates select="m:bvar/m:type"/>
1191       <m:mo>.</m:mo>
1192       <xsl:apply-templates select="*[position()=2]"/>
1193      </xsl:otherwise>
1194      </xsl:choose>
1195     </m:mrow>
1196 </xsl:template>
1197
1198 <!-- *********************************** -->
1199 <!-- BASE SET OF MATHML CONTENT ELEMENTS -->
1200 <!-- *********************************** -->
1201
1202 <!-- Logic -->
1203
1204 <xsl:template match = "m:apply[m:eq[1]]">
1205  <xsl:variable name="charlength">
1206   <xsl:apply-templates select="*[1]" mode="charcount"/>
1207  </xsl:variable>
1208  <xsl:choose>
1209   <xsl:when test="$charlength >= $framewidth">
1210    <m:mtable align="baseline 1" equalrows="false" columnalign="left">
1211     <xsl:if test="@helm:xref">
1212      <xsl:attribute name="helm:xref">
1213       <xsl:value-of select="@helm:xref"/>
1214      </xsl:attribute>
1215     </xsl:if>
1216     <m:mtr>
1217      <m:mtd>
1218       <m:mo stretchy="false">(</m:mo>
1219       <xsl:apply-templates select="*[position()=2]"/>
1220      </m:mtd>
1221     </m:mtr>
1222     <xsl:for-each select = "*[position()>2]">
1223      <m:mtr>
1224       <m:mtd>
1225        <m:mphantom><m:mtext>__</m:mtext></m:mphantom>
1226        <m:mo helm:xref="m:in/@helm:xref">
1227         =
1228        </m:mo>
1229        <xsl:apply-templates select="."/>
1230       </m:mtd>
1231      </m:mtr>
1232     </xsl:for-each>
1233     <m:mtr>
1234      <m:mtd>
1235       <m:mo stretchy="false">)</m:mo>
1236      </m:mtd>
1237     </m:mtr>
1238    </m:mtable>
1239   </xsl:when>
1240   <xsl:otherwise>
1241    <xsl:apply-imports/>
1242   </xsl:otherwise>
1243  </xsl:choose>
1244 </xsl:template>
1245
1246
1247 <xsl:template match = "m:apply[m:and[1]|m:or[1]
1248           |m:geq[1]|m:leq[1]|m:gt[1]|m:lt[1]
1249           |m:in[1]|m:intesect[1]|m:union[1]|m:subset[1]
1250           |m:prsubset|m:setdiff[1]]">
1251  <xsl:variable name="symbol">
1252   <xsl:choose>
1253    <xsl:when test="m:and[1]">
1254     <xsl:value-of select="'wedge'"/>
1255    </xsl:when>
1256    <xsl:when test="m:or[1]">
1257     <xsl:value-of select="'vee'"/>
1258    </xsl:when>
1259    <xsl:when test="m:geq[1]">
1260     <xsl:value-of select="'geq'"/>
1261    </xsl:when>
1262    <xsl:when test="m:leq[1]">
1263     <xsl:value-of select="'leq'"/>
1264    </xsl:when>
1265    <xsl:when test="m:gt[1]">
1266     <xsl:value-of select="'gt'"/>
1267    </xsl:when>
1268    <xsl:when test="m:lt[1]">
1269     <xsl:value-of select="'lt'"/>
1270    </xsl:when>
1271    <xsl:when test="m:eq[1]">
1272     <xsl:value-of select="'Equal'"/>
1273    </xsl:when>
1274    <xsl:when test="m:in[1]">
1275     <xsl:value-of select="'Element'"/>
1276    </xsl:when>
1277    <xsl:when test="m:subset[1]">
1278     <xsl:value-of select="'SubsetEqual'"/>
1279    </xsl:when>
1280    <xsl:when test="m:prsubset[1]">
1281     <xsl:value-of select="'subset'"/>
1282    </xsl:when>
1283    <xsl:when test="m:intersect[1]">
1284     <xsl:value-of select="'Intersection'"/>
1285    </xsl:when>
1286    <xsl:when test="m:union[1]">
1287     <xsl:value-of select="'Union'"/>
1288    </xsl:when>
1289    <xsl:when test="m:setdiff[1]">
1290     <xsl:value-of select="'Backslash'"/>
1291    </xsl:when>
1292   </xsl:choose>
1293  </xsl:variable>
1294  <xsl:variable name="charlength">
1295   <xsl:apply-templates select="*[1]" mode="charcount"/>
1296  </xsl:variable>
1297  <xsl:choose>
1298   <xsl:when test="$charlength >= $framewidth">
1299    <m:mtable align="baseline 1" equalrows="false" columnalign="left">
1300     <xsl:if test="@helm:xref">
1301      <xsl:attribute name="helm:xref">
1302       <xsl:value-of select="@helm:xref"/>
1303      </xsl:attribute>
1304     </xsl:if>
1305     <m:mtr>
1306      <m:mtd>
1307       <m:mo stretchy="false">(</m:mo>
1308       <xsl:apply-templates select="*[position()=2]"/>
1309      </m:mtd>
1310     </m:mtr>
1311     <xsl:for-each select = "*[position()>2]">
1312      <m:mtr>
1313       <m:mtd>
1314        <m:mphantom><m:mtext>__</m:mtext></m:mphantom>
1315        <m:mo helm:xref="{*[1]/@helm:xref}">
1316         <m:mchar name="{$symbol}"/>
1317        </m:mo>
1318        <xsl:apply-templates select="."/>
1319       </m:mtd>
1320      </m:mtr>
1321     </xsl:for-each>
1322     <m:mtr>
1323      <m:mtd>
1324       <m:mo stretchy="false">)</m:mo>
1325      </m:mtd>
1326     </m:mtr>
1327    </m:mtable>
1328   </xsl:when>
1329   <xsl:otherwise>
1330    <xsl:apply-imports/>
1331   </xsl:otherwise>
1332  </xsl:choose>
1333 </xsl:template>
1334
1335 <xsl:template match = "m:set">
1336  <xsl:choose>
1337   <xsl:when test="count(child::*) = 0">
1338    <m:mi>
1339     <m:mchar name="emptyset"/>
1340    </m:mi>
1341   </xsl:when>
1342   <xsl:otherwise>
1343    <xsl:variable name="charlength">
1344     <xsl:apply-templates select="*[1]" mode="charcount"/>
1345    </xsl:variable>
1346    <xsl:choose>
1347     <xsl:when test="$charlength >= $framewidth">
1348      <xsl:choose>
1349       <xsl:when test="name(*[1]) = 'm:bvar'">
1350        <m:mtable align="baseline 1" equalrows="false" columnalign="left">
1351         <m:mtr>
1352          <m:mtd>
1353           <m:mo stretchy="false">{</m:mo>
1354           <xsl:apply-templates select="*[position()=1]"/>
1355          </m:mtd>
1356         </m:mtr>
1357         <m:mtr>
1358          <m:mtd>
1359           <m:mphantom><m:mtext>{</m:mtext></m:mphantom>
1360           <m:mo stretchy="false">|</m:mo>
1361           <xsl:apply-templates select="m:condition/*[1]"/>
1362          </m:mtd>
1363         </m:mtr>
1364         <m:mtr>
1365          <m:mtd>
1366           <m:mo stretchy="false">}</m:mo>
1367          </m:mtd>
1368         </m:mtr>
1369        </m:mtable>
1370       </xsl:when>
1371       <xsl:otherwise>
1372        <m:mtable align="baseline 1" equalrows="false" columnalign="left">
1373         <m:mtr>
1374          <m:mtd>
1375           <m:mo stretchy="false">{</m:mo>
1376           <xsl:apply-templates select="*[position()=1]"/>
1377           <xsl:if test="position() != last()">
1378            <mo>,</mo>
1379           </xsl:if>
1380          </m:mtd>
1381         </m:mtr>
1382         <xsl:for-each select = "*[position()>2]">
1383          <m:mtr>
1384           <m:mtd>
1385            <m:mphantom><m:mtext>{</m:mtext></m:mphantom>
1386            <xsl:apply-templates select="."/>
1387            <xsl:if test="position() != last()">
1388             <mo>,</mo>
1389            </xsl:if>
1390           </m:mtd>
1391          </m:mtr>
1392         </xsl:for-each>
1393         <m:mtr>
1394          <m:mtd>
1395           <m:mo stretchy="false">}</m:mo>
1396          </m:mtd>
1397         </m:mtr>
1398        </m:mtable>
1399       </xsl:otherwise>
1400      </xsl:choose>
1401     </xsl:when>
1402     <xsl:otherwise>
1403      <xsl:apply-imports/>
1404     </xsl:otherwise>
1405    </xsl:choose>
1406   </xsl:otherwise>
1407  </xsl:choose>
1408 </xsl:template>
1409
1410 <xsl:template match = "m:apply[m:card[1]]">
1411  <m:mo stretchy="false">|</m:mo>
1412   <xsl:apply-templates select="*[2]"/>
1413  <m:mo stretchy="false">|</m:mo>
1414 </xsl:template>
1415
1416 <!-- *********************************** -->
1417 <!--          PROOF ELEMENTS             -->
1418 <!-- *********************************** -->
1419
1420
1421
1422 <!--**********************-->
1423 <!--       COUNTING       -->
1424 <!--**********************-->
1425
1426 <xsl:template match="m:cn|m:and|m:or|m:not|m:exists|m:eq|m:lt|m:leq|m:gt|m:geq
1427  |m:in|m:notin|m:intersect|m:union|m:subset|m:prsubset|m:card|m:setdiff
1428  |m:plus|m:minus|m:times" mode="charcount">
1429 <xsl:param name="incurrent_length" select="0"/>
1430     <xsl:choose>
1431     <xsl:when test="$framewidth > ($incurrent_length + 3 + string-length())">
1432      <xsl:variable name="siblength">
1433       <xsl:apply-templates select="following-sibling::*[position()=1]" mode="charcount">
1434        <xsl:with-param name="incurrent_length" select="$incurrent_length + string-length()"/>
1435       </xsl:apply-templates>
1436      </xsl:variable>
1437      <xsl:choose>
1438      <xsl:when test="string($siblength) = &quot;&quot;">
1439       <xsl:value-of select="$incurrent_length + 3 + string-length()"/>
1440      </xsl:when>
1441      <xsl:otherwise>
1442       <xsl:value-of select="number($siblength)"/>
1443      </xsl:otherwise>
1444      </xsl:choose>
1445     </xsl:when>
1446     <xsl:otherwise>
1447      <xsl:value-of select="$incurrent_length + 3 + string-length()"/>
1448     </xsl:otherwise>
1449     </xsl:choose>
1450 </xsl:template>
1451
1452 <xsl:template match="m:ci|m:csymbol" mode="charcount">
1453 <xsl:param name="incurrent_length" select="0"/>
1454 <xsl:param name="nosibling" select="0"/>
1455     <xsl:choose>
1456     <xsl:when test="$framewidth > ($incurrent_length + string-length()) and ($nosibling = 0)">
1457      <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>
1458      <xsl:choose>
1459      <xsl:when test="string($siblength) = &quot;&quot;">
1460       <xsl:value-of select="$incurrent_length + string-length()"/>
1461      </xsl:when>
1462      <xsl:otherwise>
1463       <xsl:value-of select="number($siblength)"/>
1464      </xsl:otherwise>
1465      </xsl:choose>
1466     </xsl:when>
1467     <xsl:otherwise>
1468      <xsl:value-of select="$incurrent_length + string-length()"/>
1469     </xsl:otherwise>
1470     </xsl:choose>
1471 </xsl:template>
1472
1473 <xsl:template match="*" mode="charcount">
1474 <xsl:param name="incurrent_length" select="0"/>
1475 <xsl:param name="nosibling" select="0"/>
1476  <xsl:choose>
1477   <xsl:when test="count(child::*) = 0">
1478    <xsl:value-of select="$incurrent_length"/>
1479   </xsl:when>
1480   <xsl:otherwise>
1481     <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>
1482     <xsl:choose>
1483     <xsl:when test="$framewidth > number($childlength) and ($nosibling = 0)">
1484      <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>
1485      <xsl:choose>
1486      <xsl:when test="string($siblength) = &quot;&quot;">
1487       <xsl:value-of select="number($childlength)"/>
1488      </xsl:when>
1489      <xsl:otherwise>
1490       <xsl:value-of select="number($siblength)"/>
1491      </xsl:otherwise>
1492      </xsl:choose>>
1493     </xsl:when>
1494     <xsl:otherwise>
1495      <xsl:value-of select="number($childlength)"/>
1496     </xsl:otherwise>
1497     </xsl:choose>
1498   </xsl:otherwise>
1499  </xsl:choose>
1500 </xsl:template>
1501
1502 </xsl:stylesheet>
1503
1504