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="0"/>
 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]"/>
 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]"/>
 524              </xsl:otherwise>
 525              </xsl:choose>
 526             </xsl:when>
 527             <xsl:otherwise>
 528              <xsl:apply-templates select="*[position()=3]"/>
 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]"/>
 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]"/>
 560          </xsl:otherwise>
 561          </xsl:choose>
 562         </xsl:when>
 563         <xsl:otherwise>
 564          <xsl:apply-templates select="*[position()=3]"/>
 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='letin1'">
 967         <m:mtable align="baseline 1" equalrows="false" columnalign="left">
 968          <m:mtr>
 969           <m:mtd>
 970            <m:mrow>
 971             <xsl:apply-templates select="*[2]"/>
 972            </m:mrow>
 973           </m:mtd>
 974          </m:mtr>
 975          <m:mtr>
 976           <m:mtd>
 977            <m:mrow>
 978             <xsl:apply-templates select="*[3]"/>
 979            </m:mrow>
 980           </m:mtd>
 981          </m:mtr>
 982         </m:mtable>
 983       </xsl:when>
 984       <xsl:when test="$name='letin'">
 985         <m:mtable align="baseline 1" equalrows="false" columnalign="left">
 986          <!-- <xsl:for-each select="APPLY[m:csymbol and (string(m:csymbol)='let')]"> -->
 987          <xsl:for-each select="*[(last() > position()) and (position()>1)]">
 988          <m:mtr>
 989           <m:mtd>
 990            <m:mrow>
 991             <xsl:apply-templates select="."/>
 992            </m:mrow>
 993           </m:mtd>
 994          </m:mtr>
 995          </xsl:for-each>
 996          <m:mtr>
 997           <m:mtd>
 998            <m:mrow>
 999             <xsl:apply-templates select="*[position()=last()]"/>
1000            </m:mrow>
1001           </m:mtd>
1002          </m:mtr>
1003         </m:mtable>
1004       </xsl:when>
1005       <xsl:when test="$name='let'">
1006        <m:mtext>(</m:mtext>
1007        <xsl:apply-templates select="m:ci"/>
1008        <m:mtext>) </m:mtext>
1009        <xsl:apply-templates select="*[3]"/>
1010       </xsl:when>
1011       <xsl:when test="$name='rw_step'">
1012         <m:mtable align="baseline 1" equalrows="false" columnalign="left">
1013          <m:mtr>
1014           <m:mtd>
1015            <m:mrow>
1016             <xsl:choose>
1017              <xsl:when test="name(*[2])='m:apply'">
1018               <xsl:apply-templates select="*[2]"/>
1019              </xsl:when>
1020              <xsl:otherwise>
1021               <m:mtext>Consider</m:mtext>
1022               <m:mphantom><m:mtext>_</m:mtext></m:mphantom>
1023               <xsl:apply-templates select="*[2]"/>
1024              </xsl:otherwise>
1025             </xsl:choose>
1026            </m:mrow>
1027           </m:mtd>
1028          </m:mtr>
1029          <m:mtr>
1030           <m:mtd>
1031            <m:mrow>
1032             <m:mtext>Rewrite</m:mtext>
1033             <m:mphantom><m:mtext>_</m:mtext></m:mphantom>
1034             <xsl:apply-templates select="*[3]"/>
1035             <m:mphantom><m:mtext>_</m:mtext></m:mphantom>
1036             <m:mtext>with</m:mtext>
1037             <m:mphantom><m:mtext>_</m:mtext></m:mphantom>
1038             <xsl:apply-templates select="*[4]"/>
1039             <m:mphantom><m:mtext>_</m:mtext></m:mphantom>
1040             <m:mtext>by</m:mtext>
1041             <m:mphantom><m:mtext>_</m:mtext></m:mphantom>
1042             <xsl:apply-templates select="*[5]"/>
1043            </m:mrow>
1044           </m:mtd>
1045          </m:mtr>
1046         </m:mtable>
1047       </xsl:when>
1048       <xsl:when test="$name='thread'">
1049         <m:mtable align="baseline 1" equalrows="false" columnalign="left">
1050          <m:mtr>
1051           <m:mtd>
1052            <m:mrow>
1053             <xsl:choose>
1054              <xsl:when test="name(*[last()])='m:apply'">
1055               <xsl:apply-templates select="*[last()]"/>
1056              </xsl:when>
1057              <xsl:otherwise>
1058               <m:mtext>Consider</m:mtext>
1059               <m:mphantom><m:mtext>_</m:mtext></m:mphantom>
1060               <xsl:apply-templates select="*[last()]"/>
1061              </xsl:otherwise>
1062             </xsl:choose>
1063            </m:mrow>
1064           </m:mtd>
1065          </m:mtr>
1066          <xsl:apply-templates mode="thread" select="*[(last()-2)]"/>
1067         </m:mtable>
1068       </xsl:when>
1069       <xsl:when test="$name='rewrite_and_apply'">
1070         <m:mtable align="baseline 1" equalrows="false" columnalign="left">
1071          <m:mtr>
1072           <m:mtd>
1073            <m:mrow>
1074             <xsl:apply-templates select="*[2]"/>
1075            </m:mrow>
1076           </m:mtd>
1077          </m:mtr>
1078          <m:mtr>
1079           <m:mtd>
1080            <m:mrow>
1081             <m:mtext>Then apply it to</m:mtext>
1082             <m:mphantom><m:mtext>_</m:mtext></m:mphantom>
1083             <xsl:apply-templates select="*[position()>2]"/>
1084            </m:mrow>
1085           </m:mtd>
1086          </m:mtr>
1087        </m:mtable>
1088       </xsl:when>
1089       <!-- NAT_IND -->
1090       <xsl:when test="$name='nat_ind'">
1091         <m:mtable align="baseline 1" equalrows="false" columnalign="left">
1092          <m:mtr>
1093           <m:mtd>
1094            <m:mtext>By induction</m:mtext>
1095           </m:mtd>
1096          </m:mtr>
1097          <m:mtr>
1098           <m:mtd>
1099            <m:mrow>
1100             <m:mtext>base case:</m:mtext>
1101             <xsl:apply-templates select="*[2]"/>
1102            </m:mrow>
1103           </m:mtd>
1104          </m:mtr>
1105          <m:mtr>
1106           <m:mtd>
1107            <m:mrow>
1108             <m:mtext>inductive case:</m:mtext>
1109             <xsl:apply-templates select="*[3]"/>
1110            </m:mrow>
1111           </m:mtd>
1112          </m:mtr>
1113         </m:mtable>
1114       </xsl:when>
1115       <!-- AND_IND -->
1116       <xsl:when test="$name='and_ind'">
1117         <m:mtable align="baseline 1" equalrows="false" columnalign="left">
1118          <m:mtr>
1119           <m:mtd>
1120            <m:mrow>
1121             <xsl:choose>
1122              <xsl:when test="name(*[2])='m:apply'">
1123               <xsl:apply-templates select="*[2]"/>
1124              </xsl:when>
1125              <xsl:otherwise>
1126               <m:mtext>Consider</m:mtext>
1127               <m:mphantom><m:mtext>_</m:mtext></m:mphantom>
1128               <xsl:apply-templates select="*[2]"/>
1129              </xsl:otherwise>
1130             </xsl:choose>
1131            </m:mrow>
1132           </m:mtd>
1133          </m:mtr>
1134          <m:mtr>
1135           <m:mtd>
1136            <m:mtext>In particular, we have</m:mtext>
1137           </m:mtd>
1138          </m:mtr>
1139          <m:mtr>
1140           <m:mtd>
1141            <m:mrow>
1142             <m:mtext>(</m:mtext>
1143             <xsl:apply-templates select="*[3]"/>
1144             <m:mtext>)</m:mtext>
1145             <m:mphantom><m:mtext>_</m:mtext></m:mphantom>
1146             <xsl:apply-templates select="*[4]"/>
1147             </m:mrow>
1148           </m:mtd>
1149          </m:mtr>
1150          <m:mtr>
1151           <m:mtd>
1152            <m:mrow>
1153             <m:mtext>(</m:mtext>
1154             <xsl:apply-templates select="*[5]"/>
1155             <m:mtext>)</m:mtext>
1156             <m:mphantom><m:mtext>_</m:mtext></m:mphantom>
1157             <xsl:apply-templates select="*[6]"/>
1158             </m:mrow>
1159           </m:mtd>
1160          </m:mtr>
1161          <m:mtr>
1162           <m:mtd>
1163            <m:mrow>
1164             <xsl:apply-templates select="*[7]"/>
1165            </m:mrow>
1166           </m:mtd>
1167          </m:mtr>
1168         </m:mtable>
1169       </xsl:when>
1170       <xsl:when test="$name='or_ind'">
1171         <m:mtable align="baseline 1" equalrows="false" columnalign="left">
1172          <m:mtr>
1173           <m:mtd>
1174            <m:mrow>
1175             <xsl:choose>
1176              <xsl:when test="name(*[2])='m:apply'">
1177               <xsl:apply-templates select="*[2]"/>
1178              </xsl:when>
1179              <xsl:otherwise>
1180               <m:mtext>Consider</m:mtext>
1181               <m:mphantom><m:mtext>_</m:mtext></m:mphantom>
1182               <xsl:apply-templates select="*[2]"/>
1183              </xsl:otherwise>
1184             </xsl:choose>
1185            </m:mrow>
1186           </m:mtd>
1187          </m:mtr>
1188          <m:mtr>
1189           <m:mtd>
1190            <m:mtext>We prove</m:mtext>
1191            <m:mphantom><m:mtext>_</m:mtext></m:mphantom>
1192            <xsl:apply-templates select="*[3]"/>
1193            <m:mphantom><m:mtext>_</m:mtext></m:mphantom>
1194            <m:mtext>by cases:</m:mtext>
1195           </m:mtd>
1196          </m:mtr>
1197          <m:mtr>
1198           <m:mtd>
1199            <m:mrow>
1200             <m:mtext>*</m:mtext>
1201             <xsl:apply-templates select="*[4]"/>
1202            </m:mrow>
1203           </m:mtd>
1204          </m:mtr>
1205          <m:mtr>
1206           <m:mtd>
1207            <m:mrow>
1208             <m:mtext>*</m:mtext>
1209             <xsl:apply-templates select="*[5]"/>
1210            </m:mrow>
1211           </m:mtd>
1212          </m:mtr>
1213         </m:mtable>
1214       </xsl:when>
1215       <xsl:when test="$name='ex_ind'">
1216         <m:mtable align="baseline 1" equalrows="false" columnalign="left">
1217          <m:mtr>
1218           <m:mtd>
1219            <m:mrow>
1220             <xsl:choose>
1221              <xsl:when test="name(*[2])='m:apply'">
1222               <xsl:apply-templates select="*[2]"/>
1223              </xsl:when>
1224              <xsl:otherwise>
1225               <m:mtext>Consider</m:mtext>
1226               <m:mphantom><m:mtext>_</m:mtext></m:mphantom>
1227               <xsl:apply-templates select="*[2]"/>
1228              </xsl:otherwise>
1229             </xsl:choose>
1230            </m:mrow>
1231           </m:mtd>
1232          </m:mtr>
1233          <m:mtr>
1234           <m:mtd>
1235            <m:mtext>Let</m:mtext>
1236            <m:mphantom><m:mtext>_</m:mtext></m:mphantom>
1237            <xsl:apply-templates select="*[3]"/>
1238            <m:mtext>:</m:mtext>
1239            <xsl:apply-templates select="*[4]"/>
1240            <m:mphantom><m:mtext>_</m:mtext></m:mphantom>
1241            <m:mtext>such that</m:mtext>
1242            <m:mphantom><m:mtext>_</m:mtext></m:mphantom>
1243            <m:mtext>(</m:mtext>
1244             <xsl:apply-templates select="*[5]"/>
1245            <m:mtext>)</m:mtext>
1246            <m:mphantom><m:mtext>_</m:mtext></m:mphantom>
1247            <xsl:apply-templates select="*[6]"/>
1248           </m:mtd>
1249          </m:mtr>
1250          <m:mtr>
1251           <m:mtd>
1252            <m:mrow>
1253             <xsl:apply-templates select="*[7]"/>
1254            </m:mrow>
1255           </m:mtd>
1256          </m:mtr>
1257         </m:mtable>
1258       </xsl:when>
1259       <xsl:otherwise>
1260        <m:ci>ERROR</m:ci>
1261       </xsl:otherwise>
1262      </xsl:choose>
1263     </m:mrow>
1264 </xsl:template>
1265
1266 <!-- Il modo Thread non esiste piu'
1267 <xsl:template match="*" mode="thread">
1268  <xsl:variable name="name"><xsl:value-of select="following-sibling::*[position()=1]/m:csymbol"/></xsl:variable>
1269  <xsl:choose>
1270   <xsl:when test="$name='rw_step'">
1271          <m:mtr>
1272           <m:mtd>
1273            <m:mrow>
1274             <m:mtext>Rewrite</m:mtext>
1275             <m:mphantom><m:mtext>_</m:mtext></m:mphantom>
1276             <xsl:apply-templates select="following-sibling::*[position()=1]/*[2]"/>
1277             <m:mphantom><m:mtext>_</m:mtext></m:mphantom>
1278             <m:mtext>with</m:mtext>
1279             <m:mphantom><m:mtext>_</m:mtext></m:mphantom>
1280             <xsl:apply-templates select="following-sibling::*[position()=1]/*[3]"/>
1281             <m:mphantom><m:mtext>_</m:mtext></m:mphantom>
1282             <m:mtext>by</m:mtext>
1283             <m:mphantom><m:mtext>_</m:mtext></m:mphantom>
1284             <xsl:apply-templates select="following-sibling::*[position()=1]/*[4]"/>
1285            </m:mrow>
1286           </m:mtd>
1287          </m:mtr>
1288          <m:mtr>
1289           <m:mtd>
1290            <m:mrow>
1291             <m:mtext mathcolor="Maroon">we get</m:mtext>
1292             <m:mphantom><m:mtext>_</m:mtext></m:mphantom>
1293             <xsl:apply-templates select="."/>
1294            </m:mrow>
1295           </m:mtd>
1296          </m:mtr>
1297    </xsl:when>
1298    <xsl:otherwise>
1299          <m:mtr>
1300           <m:mtd>
1301            <m:mrow>
1302             <xsl:apply-templates select="following-sibling::*[position()=1]"/>
1303            </m:mrow>
1304           </m:mtd>
1305          </m:mtr>
1306          <m:mtr>
1307           <m:mtd>
1308            <m:mrow>
1309             <m:mtext mathcolor="Maroon">we get</m:mtext>
1310             <m:mphantom><m:mtext>_</m:mtext></m:mphantom>
1311             <xsl:apply-templates select="."/>
1312            </m:mrow>
1313           </m:mtd>
1314          </m:mtr>
1315     </xsl:otherwise>
1316    </xsl:choose>
1317          <xsl:apply-templates mode="thread" select="preceding-sibling::*[position()=2]"/>
1318 </xsl:template>
1319 -->
1320
1321 <!-- LAMBDA -->
1322
1323 <xsl:template match="m:lambda">
1324     <xsl:variable name="charlength"><xsl:apply-templates select="*[position()=1]" mode="charcount"/></xsl:variable>
1325     <m:mrow helm:xref="{@helm:xref}">
1326      <xsl:choose>
1327      <xsl:when test="$charlength >= $framewidth">
1328       <m:mtable align="baseline 1" equalrows="false" columnalign="left">
1329         <m:mtr>
1330           <m:mtd>
1331             <m:mo mathcolor="Red">&#x03bb;</m:mo>
1332             <xsl:apply-templates select="m:bvar"/>
1333           </m:mtd>
1334          </m:mtr>
1335        <m:mtr>
1336         <m:mtd>
1337          <m:mrow>
1338           <m:mo>.</m:mo>
1339           <xsl:apply-templates select="*[position()=2]"/>
1340          </m:mrow>
1341         </m:mtd>
1342        </m:mtr>
1343       </m:mtable>
1344      </xsl:when>
1345      <xsl:otherwise>
1346       <m:mo mathcolor="Red">&#x03bb;</m:mo>
1347       <xsl:apply-templates select="m:bvar/m:ci"/>
1348       <m:mo>:</m:mo>
1349       <xsl:apply-templates select="m:bvar/m:type"/>
1350       <m:mo>.</m:mo>
1351       <xsl:apply-templates select="*[position()=2]"/>
1352      </xsl:otherwise>
1353      </xsl:choose>
1354     </m:mrow>
1355 </xsl:template>
1356
1357 <!-- *********************************** -->
1358 <!-- BASE SET OF MATHML CONTENT ELEMENTS -->
1359 <!-- *********************************** -->
1360
1361 <!-- Logic -->
1362
1363 <xsl:template match = "m:apply[m:eq[1]]">
1364  <xsl:variable name="charlength">
1365   <xsl:apply-templates select="*[1]" mode="charcount"/>
1366  </xsl:variable>
1367  <xsl:choose>
1368   <xsl:when test="$charlength >= $framewidth">
1369    <m:mtable align="baseline 1" equalrows="false" columnalign="left">
1370     <xsl:if test="@helm:xref">
1371      <xsl:attribute name="helm:xref">
1372       <xsl:value-of select="@helm:xref"/>
1373      </xsl:attribute>
1374     </xsl:if>
1375     <m:mtr>
1376      <m:mtd>
1377       <m:mo stretchy="false">(</m:mo>
1378       <xsl:apply-templates select="*[position()=2]"/>
1379      </m:mtd>
1380     </m:mtr>
1381     <xsl:for-each select = "*[position()>2]">
1382      <m:mtr>
1383       <m:mtd>
1384        <m:mphantom><m:mtext>__</m:mtext></m:mphantom>
1385        <m:mo helm:xref="{m:in/@helm:xref}">=</m:mo>
1386        <xsl:apply-templates select="."/>
1387       </m:mtd>
1388      </m:mtr>
1389     </xsl:for-each>
1390     <m:mtr>
1391      <m:mtd>
1392       <m:mo stretchy="false">)</m:mo>
1393      </m:mtd>
1394     </m:mtr>
1395    </m:mtable>
1396   </xsl:when>
1397   <xsl:otherwise>
1398    <xsl:apply-imports/>
1399   </xsl:otherwise>
1400  </xsl:choose>
1401 </xsl:template>
1402
1403
1404 <xsl:template match = "m:apply[m:and[1]|m:or[1]
1405           |m:geq[1]|m:leq[1]|m:gt[1]|m:lt[1]
1406           |m:in[1]|m:intesect[1]|m:union[1]|m:subset[1]
1407           |m:prsubset|m:setdiff[1]]">
1408  <xsl:variable name="symbol">
1409   <xsl:choose>
1410    <xsl:when test="m:and[1]">
1411     <xsl:value-of select="'wedge'"/>
1412    </xsl:when>
1413    <xsl:when test="m:or[1]">
1414     <xsl:value-of select="'vee'"/>
1415    </xsl:when>
1416    <xsl:when test="m:geq[1]">
1417     <xsl:value-of select="'geq'"/>
1418    </xsl:when>
1419    <xsl:when test="m:leq[1]">
1420     <xsl:value-of select="'leq'"/>
1421    </xsl:when>
1422    <xsl:when test="m:gt[1]">
1423     <xsl:value-of select="'gt'"/>
1424    </xsl:when>
1425    <xsl:when test="m:lt[1]">
1426     <xsl:value-of select="'lt'"/>
1427    </xsl:when>
1428    <xsl:when test="m:eq[1]">
1429     <xsl:value-of select="'Equal'"/>
1430    </xsl:when>
1431    <xsl:when test="m:in[1]">
1432     <xsl:value-of select="'Element'"/>
1433    </xsl:when>
1434    <xsl:when test="m:subset[1]">
1435     <xsl:value-of select="'SubsetEqual'"/>
1436    </xsl:when>
1437    <xsl:when test="m:prsubset[1]">
1438     <xsl:value-of select="'subset'"/>
1439    </xsl:when>
1440    <xsl:when test="m:intersect[1]">
1441     <xsl:value-of select="'Intersection'"/>
1442    </xsl:when>
1443    <xsl:when test="m:union[1]">
1444     <xsl:value-of select="'Union'"/>
1445    </xsl:when>
1446    <xsl:when test="m:setdiff[1]">
1447     <xsl:value-of select="'Backslash'"/>
1448    </xsl:when>
1449   </xsl:choose>
1450  </xsl:variable>
1451  <xsl:variable name="charlength">
1452   <xsl:apply-templates select="*[1]" mode="charcount"/>
1453  </xsl:variable>
1454  <xsl:choose>
1455   <xsl:when test="$charlength >= $framewidth">
1456    <m:mtable align="baseline 1" equalrows="false" columnalign="left">
1457     <xsl:if test="@helm:xref">
1458      <xsl:attribute name="helm:xref">
1459       <xsl:value-of select="@helm:xref"/>
1460      </xsl:attribute>
1461     </xsl:if>
1462     <m:mtr>
1463      <m:mtd>
1464       <m:mo stretchy="false">(</m:mo>
1465       <xsl:apply-templates select="*[position()=2]"/>
1466      </m:mtd>
1467     </m:mtr>
1468     <xsl:for-each select = "*[position()>2]">
1469      <m:mtr>
1470       <m:mtd>
1471        <m:mphantom><m:mtext>__</m:mtext></m:mphantom>
1472        <m:mo helm:xref="{*[1]/@helm:xref}">
1473         <m:mchar name="{$symbol}"/>
1474        </m:mo>
1475        <xsl:apply-templates select="."/>
1476       </m:mtd>
1477      </m:mtr>
1478     </xsl:for-each>
1479     <m:mtr>
1480      <m:mtd>
1481       <m:mo stretchy="false">)</m:mo>
1482      </m:mtd>
1483     </m:mtr>
1484    </m:mtable>
1485   </xsl:when>
1486   <xsl:otherwise>
1487    <xsl:apply-imports/>
1488   </xsl:otherwise>
1489  </xsl:choose>
1490 </xsl:template>
1491
1492 <xsl:template match = "m:set">
1493  <xsl:choose>
1494   <xsl:when test="count(child::*) = 0">
1495    <m:mi>
1496     <m:mchar name="emptyset"/>
1497    </m:mi>
1498   </xsl:when>
1499   <xsl:otherwise>
1500    <xsl:variable name="charlength">
1501     <xsl:apply-templates select="*[1]" mode="charcount"/>
1502    </xsl:variable>
1503    <xsl:choose>
1504     <xsl:when test="$charlength >= $framewidth">
1505      <xsl:choose>
1506       <xsl:when test="name(*[1]) = 'm:bvar'">
1507        <m:mtable align="baseline 1" equalrows="false" columnalign="left">
1508         <m:mtr>
1509          <m:mtd>
1510           <m:mo stretchy="false">{</m:mo>
1511           <xsl:apply-templates select="*[position()=1]"/>
1512          </m:mtd>
1513         </m:mtr>
1514         <m:mtr>
1515          <m:mtd>
1516           <m:mphantom><m:mtext>{</m:mtext></m:mphantom>
1517           <m:mo stretchy="false">|</m:mo>
1518           <xsl:apply-templates select="m:condition/*[1]"/>
1519          </m:mtd>
1520         </m:mtr>
1521         <m:mtr>
1522          <m:mtd>
1523           <m:mo stretchy="false">}</m:mo>
1524          </m:mtd>
1525         </m:mtr>
1526        </m:mtable>
1527       </xsl:when>
1528       <xsl:otherwise>
1529        <m:mtable align="baseline 1" equalrows="false" columnalign="left">
1530         <m:mtr>
1531          <m:mtd>
1532           <m:mo stretchy="false">{</m:mo>
1533           <xsl:apply-templates select="*[position()=1]"/>
1534           <xsl:if test="position() != last()">
1535            <mo>,</mo>
1536           </xsl:if>
1537          </m:mtd>
1538         </m:mtr>
1539         <xsl:for-each select = "*[position()>2]">
1540          <m:mtr>
1541           <m:mtd>
1542            <m:mphantom><m:mtext>{</m:mtext></m:mphantom>
1543            <xsl:apply-templates select="."/>
1544            <xsl:if test="position() != last()">
1545             <mo>,</mo>
1546            </xsl:if>
1547           </m:mtd>
1548          </m:mtr>
1549         </xsl:for-each>
1550         <m:mtr>
1551          <m:mtd>
1552           <m:mo stretchy="false">}</m:mo>
1553          </m:mtd>
1554         </m:mtr>
1555        </m:mtable>
1556       </xsl:otherwise>
1557      </xsl:choose>
1558     </xsl:when>
1559     <xsl:otherwise>
1560      <xsl:apply-imports/>
1561     </xsl:otherwise>
1562    </xsl:choose>
1563   </xsl:otherwise>
1564  </xsl:choose>
1565 </xsl:template>
1566
1567 <xsl:template match = "m:apply[m:card[1]]">
1568  <m:mo stretchy="false">|</m:mo>
1569   <xsl:apply-templates select="*[2]"/>
1570  <m:mo stretchy="false">|</m:mo>
1571 </xsl:template>
1572
1573 <!-- *********************************** -->
1574 <!--          PROOF ELEMENTS             -->
1575 <!-- *********************************** -->
1576
1577
1578
1579 <!--**********************-->
1580 <!--       COUNTING       -->
1581 <!--**********************-->
1582
1583 <xsl:template match="m:cn|m:and|m:or|m:not|m:exists|m:eq|m:lt|m:leq|m:gt|m:geq
1584  |m:in|m:notin|m:intersect|m:union|m:subset|m:prsubset|m:card|m:setdiff
1585  |m:plus|m:minus|m:times" mode="charcount">
1586 <xsl:param name="incurrent_length" select="0"/>
1587     <xsl:choose>
1588     <xsl:when test="$framewidth > ($incurrent_length + 3 + string-length())">
1589      <xsl:variable name="siblength">
1590       <xsl:apply-templates select="following-sibling::*[position()=1]" mode="charcount">
1591        <xsl:with-param name="incurrent_length" select="$incurrent_length + string-length()"/>
1592       </xsl:apply-templates>
1593      </xsl:variable>
1594      <xsl:choose>
1595      <xsl:when test="string($siblength) = &quot;&quot;">
1596       <xsl:value-of select="$incurrent_length + 3 + string-length()"/>
1597      </xsl:when>
1598      <xsl:otherwise>
1599       <xsl:value-of select="number($siblength)"/>
1600      </xsl:otherwise>
1601      </xsl:choose>
1602     </xsl:when>
1603     <xsl:otherwise>
1604      <xsl:value-of select="$incurrent_length + 3 + string-length()"/>
1605     </xsl:otherwise>
1606     </xsl:choose>
1607 </xsl:template>
1608
1609 <xsl:template match="m:ci|m:csymbol" mode="charcount">
1610 <xsl:param name="incurrent_length" select="0"/>
1611 <xsl:param name="nosibling" select="0"/>
1612     <xsl:choose>
1613     <xsl:when test="$framewidth > ($incurrent_length + string-length()) and ($nosibling = 0)">
1614      <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>
1615      <xsl:choose>
1616      <xsl:when test="string($siblength) = &quot;&quot;">
1617       <xsl:value-of select="$incurrent_length + string-length()"/>
1618      </xsl:when>
1619      <xsl:otherwise>
1620       <xsl:value-of select="number($siblength)"/>
1621      </xsl:otherwise>
1622      </xsl:choose>
1623     </xsl:when>
1624     <xsl:otherwise>
1625      <xsl:value-of select="$incurrent_length + string-length()"/>
1626     </xsl:otherwise>
1627     </xsl:choose>
1628 </xsl:template>
1629
1630 <xsl:template match="*" mode="charcount">
1631 <xsl:param name="incurrent_length" select="0"/>
1632 <xsl:param name="nosibling" select="0"/>
1633  <xsl:choose>
1634   <xsl:when test="count(child::*) = 0">
1635    <xsl:value-of select="$incurrent_length"/>
1636   </xsl:when>
1637   <xsl:otherwise>
1638     <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>
1639     <xsl:choose>
1640     <xsl:when test="$framewidth > number($childlength) and ($nosibling = 0)">
1641      <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>
1642      <xsl:choose>
1643      <xsl:when test="string($siblength) = &quot;&quot;">
1644       <xsl:value-of select="number($childlength)"/>
1645      </xsl:when>
1646      <xsl:otherwise>
1647       <xsl:value-of select="number($siblength)"/>
1648      </xsl:otherwise>
1649      </xsl:choose>
1650     </xsl:when>
1651     <xsl:otherwise>
1652      <xsl:value-of select="number($childlength)"/>
1653     </xsl:otherwise>
1654     </xsl:choose>
1655   </xsl:otherwise>
1656  </xsl:choose>
1657 </xsl:template>
1658
1659 </xsl:stylesheet>
1660
1661
1662