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  <!--
  61  <xsl:processing-instruction name="cocoon-format">type="text/xhtml"</xsl:processing-instruction>
  62  -->
  63  <xsl:apply-templates select="*"/>
  64 </xsl:template>
  65
  66 <!-- DEFINITION -->
  67
  68 <xsl:template match="Definition">
  69     <m:math>
  70      <m:mtable align="baseline 1" equalrows="false" columnalign="left" helm:xref="{@helm:xref}">
  71       <m:mtr>
  72        <m:mtd>
  73         <m:mrow>
  74          <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>
  75         </m:mrow>
  76        </m:mtd>
  77       </m:mtr>
  78       <m:mtr>
  79        <m:mtd>
  80         <m:mrow>
  81          <m:mphantom><m:mtext>__</m:mtext></m:mphantom>
  82          <xsl:apply-templates select="type/*[1]"/>
  83         </m:mrow>
  84        </m:mtd>
  85       </m:mtr>
  86       <m:mtr>
  87        <m:mtd>
  88         <m:mrow>
  89          <m:mtext>AS</m:mtext>
  90         </m:mrow>
  91        </m:mtd>
  92       </m:mtr>
  93       <m:mtr>
  94        <m:mtd>
  95         <m:mrow>
  96          <m:mphantom><m:mtext>__</m:mtext></m:mphantom>
  97          <xsl:apply-templates select="body/*[1]"/>
  98         </m:mrow>
  99        </m:mtd>
 100       </m:mtr>
 101      </m:mtable>
 102     </m:math>
 103 </xsl:template>
 104
 105 <!-- AXIOM -->
 106
 107 <xsl:template match="Axiom">
 108     <m:math>
 109      <m:mtable align="baseline 1" equalrows="false" columnalign="left" helm:xref="{@helm:xref}">
 110       <m:mtr>
 111        <m:mtd>
 112         <m:mrow>
 113          <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>
 114         </m:mrow>
 115        </m:mtd>
 116       </m:mtr>
 117       <m:mtr>
 118        <m:mtd>
 119         <m:mrow>
 120          <m:mphantom><m:mtext>__</m:mtext></m:mphantom>
 121          <xsl:apply-templates select="type/*[1]"/>
 122         </m:mrow>
 123        </m:mtd>
 124       </m:mtr>
 125      </m:mtable>
 126     </m:math>
 127 </xsl:template>
 128
 129 <!-- UNFINISHED PROOF -->
 130
 131 <xsl:template match="CurrentProof">
 132     <m:math>
 133      <m:mtable align="baseline 1" equalrows="false" columnalign="left" helm:xref="{@helm:xref}">
 134       <m:mtr>
 135        <m:mtd>
 136         <m:mrow>
 137          <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>
 138         </m:mrow>
 139        </m:mtd>
 140       </m:mtr>
 141       <m:mtr>
 142        <m:mtd>
 143         <m:mrow>
 144          <m:mtext>THESIS:</m:mtext>
 145         </m:mrow>
 146        </m:mtd>
 147       </m:mtr>
 148       <m:mtr>
 149        <m:mtd>
 150         <m:mrow>
 151          <m:mphantom><m:mtext>__</m:mtext></m:mphantom>
 152          <xsl:apply-templates select="type/*[1]"/>
 153         </m:mrow>
 154        </m:mtd>
 155       </m:mtr>
 156       <m:mtr>
 157        <m:mtd>
 158         <m:mrow>
 159          <m:mtext>CONJECTURES:</m:mtext>
 160         </m:mrow>
 161        </m:mtd>
 162       </m:mtr>
 163       <xsl:for-each select="Conjecture">
 164       <m:mtr>
 165        <m:mtd>
 166         <m:mrow>
 167          <m:mphantom><m:mtext>__</m:mtext></m:mphantom>
 168          <m:mtext><xsl:value-of select="./@no"/>:</m:mtext>
 169          <xsl:apply-templates select="./*[1]"/>
 170         </m:mrow>
 171        </m:mtd>
 172       </m:mtr>
 173       </xsl:for-each>
 174       <m:mtr>
 175        <m:mtd>
 176         <m:mrow>
 177          <m:mtext>CORRESPONDING PROOF:</m:mtext>
 178         </m:mrow>
 179        </m:mtd>
 180       </m:mtr>
 181       <m:mtr>
 182        <m:mtd>
 183         <m:mrow>
 184          <m:mphantom><m:mtext>__</m:mtext></m:mphantom>
 185          <xsl:apply-templates select="body/*[1]"/>
 186         </m:mrow>
 187        </m:mtd>
 188       </m:mtr>
 189      </m:mtable>
 190     </m:math>
 191 </xsl:template>
 192
 193 <!-- MUTUAL INDUCTIVE DEFINITION -->
 194
 195 <xsl:template match="InductiveDefinition">
 196     <m:math>
 197      <m:mtable align="baseline 1" equalrows="false" columnalign="left" helm:xref="{@helm:xref}">
 198      <xsl:for-each select="InductiveType">
 199       <m:mtr>
 200        <m:mtd>
 201         <m:mrow>
 202          <xsl:choose>
 203          <xsl:when test="position() = 1">
 204           <xsl:choose>
 205           <xsl:when test="string(./@inductive) = &quot;true&quot;">
 206            <m:mtext>INDUCTIVE DEFINITION</m:mtext>
 207           </xsl:when>
 208           <xsl:otherwise>
 209            <m:mtext>COINDUCTIVE DEFINITION</m:mtext>
 210           </xsl:otherwise>
 211           </xsl:choose>
 212          </xsl:when>
 213          <xsl:otherwise>
 214           <m:mtext>AND</m:mtext>
 215          </xsl:otherwise>
 216          </xsl:choose>
 217          <m:mphantom><m:mtext>_</m:mtext></m:mphantom>
 218          <m:mtext><xsl:value-of select="./@name"/>(<xsl:if test="string(../Params) != &quot;&quot;"><xsl:value-of select="../Params"/></xsl:if>)</m:mtext>
 219         </m:mrow>
 220        </m:mtd>
 221       </m:mtr>
 222       <m:mtr>
 223        <m:mtd>
 224         <m:mrow>
 225          <m:mphantom><m:mtext>__</m:mtext></m:mphantom>
 226          <m:mtext>[</m:mtext>
 227          <xsl:choose>
 228          <xsl:when test="string(../Param) != &quot;&quot;">
 229           <m:mtable align="baseline 1" equalrows="false" columnalign="left">
 230            <xsl:for-each select="../Param">
 231             <m:mtr>
 232              <m:mtd>
 233               <m:mrow>
 234                <m:mi><xsl:value-of select="./@name"/></m:mi>
 235                <m:mo>:</m:mo>
 236                <xsl:apply-templates select="*"/>
 237               </m:mrow>
 238              </m:mtd>
 239             </m:mtr>
 240            </xsl:for-each>
 241             <m:mtr>
 242              <m:mtd>
 243               <m:mrow>
 244                <m:mtext>]</m:mtext>
 245               </m:mrow>
 246              </m:mtd>
 247             </m:mtr>
 248           </m:mtable>
 249          </xsl:when>
 250          <xsl:otherwise>
 251           <m:mtext>]</m:mtext>
 252          </xsl:otherwise>
 253          </xsl:choose>
 254         </m:mrow>
 255        </m:mtd>
 256       </m:mtr>
 257       <m:mtr>
 258        <m:mtd>
 259         <m:mrow>
 260          <m:mtext>OF ARITY</m:mtext>
 261         </m:mrow>
 262        </m:mtd>
 263       </m:mtr>
 264       <m:mtr>
 265        <m:mtd>
 266         <m:mrow>
 267          <m:mphantom><m:mtext>__</m:mtext></m:mphantom>
 268          <xsl:apply-templates select="./arity/*[1]"/>
 269         </m:mrow>
 270        </m:mtd>
 271       </m:mtr>
 272       <m:mtr>
 273        <m:mtd>
 274         <m:mrow>
 275          <m:mtext>BUILT FROM</m:mtext>
 276         </m:mrow>
 277        </m:mtd>
 278       </m:mtr>
 279       <xsl:for-each select="./Constructor">
 280       <m:mtr>
 281        <m:mtd>
 282         <m:mrow>
 283          <xsl:choose>
 284          <xsl:when test="position() = 1">
 285           <m:mphantom><m:mtext>__</m:mtext></m:mphantom>
 286          </xsl:when>
 287          <xsl:otherwise>
 288           <m:mtext>|</m:mtext>
 289           <m:mphantom><m:mtext>_</m:mtext></m:mphantom>
 290          </xsl:otherwise>
 291          </xsl:choose>
 292          <m:mtext><xsl:value-of select="./@name"/> OF</m:mtext>
 293          <m:mphantom><m:mtext>_</m:mtext></m:mphantom>
 294          <xsl:apply-templates select="./*[1]"/>
 295         </m:mrow>
 296        </m:mtd>
 297       </m:mtr>
 298       </xsl:for-each>
 299      </xsl:for-each>
 300      </m:mtable>
 301     </m:math>
 302 </xsl:template>
 303
 304 <!-- VARIABLE -->
 305
 306 <xsl:template match="Variable">
 307     <m:math>
 308      <m:mtable align="baseline 1" equalrows="false" columnalign="left" helm:xref="{@helm:xref}">
 309       <m:mtr>
 310        <m:mtd>
 311         <m:mrow>
 312          <m:mtext>VARIABLE <xsl:value-of select="@name"/> OF TYPE</m:mtext>
 313         </m:mrow>
 314        </m:mtd>
 315       </m:mtr>
 316       <m:mtr>
 317        <m:mtd>
 318         <m:mrow>
 319          <m:mphantom><m:mtext>__</m:mtext></m:mphantom>
 320          <xsl:apply-templates select="type/*[1]"/>
 321         </m:mrow>
 322        </m:mtd>
 323       </m:mtr>
 324       <xsl:if test="name(*[1])='body'">
 325        <m:mtr>
 326         <m:mtd>
 327          <m:mrow>
 328           <m:mtext>AS</m:mtext>
 329          </m:mrow>
 330         </m:mtd>
 331        </m:mtr>
 332        <m:mtr>
 333         <m:mtd>
 334          <m:mrow>
 335           <m:mphantom><m:mtext>__</m:mtext></m:mphantom>
 336           <xsl:apply-templates select="body/*[1]"/>
 337          </m:mrow>
 338         </m:mtd>
 339        </m:mtr>
 340       </xsl:if>
 341      </m:mtable>
 342     </m:math>
 343 </xsl:template>
 344
 345 <!--**********************-->
 346 <!--        TERMS         -->
 347 <!--**********************-->
 348
 349 <xsl:template match="m:bvar">
 350  <xsl:choose>
 351   <xsl:when test="m:type">
 352    <xsl:variable name="charlength">
 353     <xsl:apply-templates select="m:ci" mode="charcount"/>
 354    </xsl:variable>
 355    <xsl:choose>
 356     <xsl:when test="$charlength >= $framewidth">
 357      <m:mtable align="baseline 1" equalrows="false" columnalign="left">
 358       <m:mtr>
 359        <m:mtd>
 360         <xsl:apply-templates select="m:ci"/>
 361         <m:mo>:</m:mo>
 362        </m:mtd>
 363       </m:mtr>
 364       <m:mtr>
 365        <m:mtd>
 366          <xsl:apply-templates select="m:type"/>
 367        </m:mtd>
 368       </m:mtr>
 369      </m:mtable>
 370     </xsl:when>
 371     <xsl:otherwise>
 372      <xsl:apply-templates select="m:ci"/>
 373      <m:mo>:</m:mo>
 374      <xsl:apply-templates select="m:type"/>
 375     </xsl:otherwise>
 376    </xsl:choose>
 377   </xsl:when>
 378   <xsl:otherwise>
 379    <xsl:apply-templates select="m:ci"/>
 380   </xsl:otherwise>
 381  </xsl:choose>
 382 </xsl:template>
 383
 384
 385 <!-- CSYMBOL -->
 386
 387 <xsl:template match="m:apply[m:csymbol]">
 388 <xsl:param name="nopar" select="0"/>
 389     <xsl:variable name="name"><xsl:value-of select="m:csymbol"/></xsl:variable>
 390     <xsl:variable name="charlength"><xsl:apply-templates select="m:csymbol" mode="charcount"/></xsl:variable>
 391     <m:mrow>
 392      <xsl:if test="@helm:xref">
 393       <xsl:attribute name="helm:xref"><xsl:value-of select="@helm:xref"/></xsl:attribute>
 394      </xsl:if>
 395      <xsl:choose>
 396       <xsl:when test="$name='forall'">
 397        <xsl:choose>
 398        <xsl:when test="$charlength >= $framewidth">
 399         <m:mtable align="baseline 1" equalrows="false" columnalign="left">
 400          <m:mtr>
 401           <m:mtd>
 402             <m:mo mathcolor="Blue"><m:mchar name="ForAll"/></m:mo>
 403             <xsl:apply-templates select="m:bvar"/>
 404           </m:mtd>
 405          </m:mtr>
 406          <m:mtr>
 407           <m:mtd>
 408            <m:mrow>
 409             <m:mo>.</m:mo>
 410             <xsl:apply-templates select="*[position()=3]"/>
 411            </m:mrow>
 412           </m:mtd>
 413          </m:mtr>
 414         </m:mtable>
 415        </xsl:when>
 416        <xsl:otherwise>
 417         <m:mo mathcolor="Blue"><m:mchar name="ForAll"/></m:mo>
 418         <xsl:apply-templates select="m:bvar/m:ci"/>
 419         <m:mo>:</m:mo>
 420         <xsl:apply-templates select="m:bvar/m:type"/>
 421         <m:mo>.</m:mo>
 422         <xsl:apply-templates select="*[position()=3]"/>
 423        </xsl:otherwise>
 424        </xsl:choose>
 425       </xsl:when>
 426       <xsl:when test="$name='let_in'">
 427        <xsl:choose>
 428        <xsl:when test="$charlength >= $framewidth">
 429         <m:mtable align="baseline 1" equalrows="false" columnalign="left">
 430          <m:mtr>
 431           <m:mtd>
 432             <m:mo>LET</m:mo>
 433             <m:mphantom><m:mtext>_</m:mtext></m:mphantom>
 434             <xsl:apply-templates select="m:bvar"/>
 435           </m:mtd>
 436          </m:mtr>
 437          <m:mtr>
 438           <m:mtd>
 439            <m:mrow>
 440             <m:mo>=</m:mo>
 441             <xsl:apply-templates select="*[position()=3]"/>
 442            </m:mrow>
 443           </m:mtd>
 444          </m:mtr>
 445          <m:mtr>
 446           <m:mtd>
 447            <m:mrow>
 448             <m:mo>IN</m:mo>
 449             <m:mphantom><m:mtext>_</m:mtext></m:mphantom>
 450             <xsl:apply-templates select="*[position()=4]"/>
 451            </m:mrow>
 452           </m:mtd>
 453          </m:mtr>
 454         </m:mtable>
 455        </xsl:when>
 456        <xsl:otherwise>
 457         <m:mo>LET</m:mo>
 458         <m:mphantom><m:mtext>_</m:mtext></m:mphantom>
 459         <xsl:apply-templates select="m:bvar/m:ci"/>
 460         <m:mo>=</m:mo>
 461         <xsl:apply-templates select="*[position()=3]"/>
 462         <m:mphantom><m:mtext>_</m:mtext></m:mphantom>
 463         <m:mtext>IN</m:mtext>
 464         <m:mphantom><m:mtext>_</m:mtext></m:mphantom>
 465         <xsl:apply-templates select="*[position()=4]"/>
 466        </xsl:otherwise>
 467        </xsl:choose>
 468       </xsl:when>
 469       <xsl:when test="$name='prod'">
 470        <xsl:choose>
 471        <xsl:when test="$charlength >= $framewidth">
 472         <m:mtable align="baseline 1" equalrows="false" columnalign="left">
 473          <m:mtr>
 474           <m:mtd>
 475             <m:mo mathcolor="Blue">&#x03a0;</m:mo>
 476             <xsl:apply-templates select="m:bvar"/>
 477           </m:mtd>
 478          </m:mtr>
 479          <m:mtr>
 480           <m:mtd>
 481            <m:mrow>
 482             <m:mo>.</m:mo>
 483             <xsl:apply-templates select="*[position()=3]"/>
 484            </m:mrow>
 485           </m:mtd>
 486          </m:mtr>
 487         </m:mtable>
 488        </xsl:when>
 489        <xsl:otherwise>
 490         <m:mo mathcolor="Blue">&#x03a0;</m:mo>
 491         <xsl:apply-templates select="m:bvar/m:ci"/>
 492         <m:mo>:</m:mo>
 493         <xsl:apply-templates select="m:bvar/m:type"/>
 494         <m:mo>.</m:mo>
 495         <xsl:apply-templates select="*[position()=3]"/>
 496        </xsl:otherwise>
 497        </xsl:choose>
 498       </xsl:when>
 499       <xsl:when test="$name='arrow'">
 500        <xsl:choose>
 501        <xsl:when test="$charlength >= $framewidth">
 502         <m:mtable align="baseline 1" equalrows="false" columnalign="left">
 503          <m:mtr>
 504           <m:mtd>
 505            <m:mrow>
 506             <xsl:if test="$nopar=0">
 507              <m:mo stretchy="false">(</m:mo>
 508             </xsl:if>
 509             <xsl:apply-templates select="*[position()=2]"/>
 510            </m:mrow>
 511           </m:mtd>
 512          </m:mtr>
 513          <m:mtr>
 514           <m:mtd>
 515            <m:mrow>
 516             <m:mo mathmathcolor="Blue">&#x2192;</m:mo>
 517             <xsl:choose>
 518             <xsl:when test="*[position()=3]/m:csymbol">
 519              <xsl:variable name="nextp"><xsl:value-of select="*[position()=3]/m:csymbol"/></xsl:variable>
 520              <xsl:choose>
 521              <xsl:when test="$nextp='arrow'">
 522               <xsl:apply-templates select="*[position()=3]"><xsl:with-param name="nopar" select="1"/></xsl:apply-templates>
 523              </xsl:when>
 524              <xsl:otherwise>
 525               <xsl:apply-templates select="*[position()=3]"/>
 526              </xsl:otherwise>
 527              </xsl:choose>
 528             </xsl:when>
 529             <xsl:otherwise>
 530              <xsl:apply-templates select="*[position()=3]"/>
 531             </xsl:otherwise>
 532             </xsl:choose>
 533            </m:mrow>
 534           </m:mtd>
 535          </m:mtr>
 536          <xsl:if test="$nopar=0">
 537          <m:mtr>
 538           <m:mtd>
 539            <m:mrow>
 540             <m:mo stretchy="false">)</m:mo>
 541            </m:mrow>
 542           </m:mtd>
 543          </m:mtr>
 544          </xsl:if>
 545         </m:mtable>
 546        </xsl:when>
 547        <xsl:otherwise>
 548         <xsl:if test="$nopar=0">
 549          <m:mo stretchy="false">(</m:mo>
 550         </xsl:if>
 551         <xsl:apply-templates select="*[position()=2]"/>
 552         <m:mo mathcolor="Blue">&#x2192;</m:mo>
 553         <xsl:choose>
 554         <xsl:when test="*[position()=3]/m:csymbol">
 555          <xsl:variable name="nextp"><xsl:value-of select="*[position()=3]/m:csymbol"/></xsl:variable>
 556          <xsl:choose>
 557          <xsl:when test="$nextp='arrow'">
 558           <xsl:apply-templates select="*[position()=3]"><xsl:with-param name="nopar" select="1"/></xsl:apply-templates>
 559          </xsl:when>
 560          <xsl:otherwise>
 561           <xsl:apply-templates select="*[position()=3]"/>
 562          </xsl:otherwise>
 563          </xsl:choose>
 564         </xsl:when>
 565         <xsl:otherwise>
 566          <xsl:apply-templates select="*[position()=3]"/>
 567         </xsl:otherwise>
 568         </xsl:choose>
 569         <xsl:if test="$nopar=0">
 570          <m:mo stretchy="false">)</m:mo>
 571         </xsl:if>
 572        </xsl:otherwise>
 573        </xsl:choose>
 574       </xsl:when>
 575       <xsl:when test="$name='app'">
 576        <xsl:choose>
 577        <xsl:when test="$charlength >= $framewidth">
 578         <m:mtable align="baseline 1" equalrows="false" columnalign="left">
 579          <m:mtr>
 580           <m:mtd>
 581            <m:mrow>
 582             <m:mo stretchy="false">(</m:mo>
 583             <xsl:apply-templates select="*[position()=2]"/>
 584            </m:mrow>
 585           </m:mtd>
 586          </m:mtr>
 587          <xsl:for-each select="*[position()>2]">
 588          <m:mtr>
 589           <m:mtd>
 590            <m:mrow>
 591             <m:mphantom><m:mtext>(</m:mtext></m:mphantom>
 592             <xsl:apply-templates select="."/>
 593            </m:mrow>
 594           </m:mtd>
 595          </m:mtr>
 596          </xsl:for-each>
 597          <m:mtr>
 598           <m:mtd>
 599            <m:mrow>
 600             <m:mo stretchy="false">)</m:mo>
 601            </m:mrow>
 602           </m:mtd>
 603          </m:mtr>
 604         </m:mtable>
 605        </xsl:when>
 606        <xsl:otherwise>
 607         <m:mo stretchy="false">(</m:mo>
 608         <xsl:apply-templates select="*[position()=2]"/>
 609         <xsl:for-each select="*[position()>2]">
 610          <m:mphantom><m:mtext>_</m:mtext></m:mphantom>
 611          <xsl:apply-templates select="."/>
 612         </xsl:for-each>
 613         <m:mo stretchy="false">)</m:mo>
 614        </xsl:otherwise>
 615        </xsl:choose>
 616       </xsl:when>
 617       <xsl:when test="$name='cast'">
 618        <xsl:choose>
 619        <xsl:when test="$charlength >= $framewidth">
 620         <m:mtable align="baseline 1" equalrows="false" columnalign="left">
 621          <m:mtr>
 622           <m:mtd>
 623            <m:mrow>
 624             <m:mo stretchy="false">(</m:mo>
 625             <xsl:apply-templates select="*[position()=2]"/>
 626            </m:mrow>
 627           </m:mtd>
 628          </m:mtr>
 629          <m:mtr>
 630           <m:mtd>
 631            <m:mrow>
 632             <m:mo mathcolor="Maroon">:></m:mo>
 633             <xsl:apply-templates select="*[position()=3]"/>
 634            </m:mrow>
 635           </m:mtd>
 636          </m:mtr>
 637          <m:mtr>
 638           <m:mtd>
 639            <m:mrow>
 640             <m:mo stretchy="false">)</m:mo>
 641            </m:mrow>
 642           </m:mtd>
 643          </m:mtr>
 644         </m:mtable>
 645        </xsl:when>
 646        <xsl:otherwise>
 647         <m:mo stretchy="false">(</m:mo>
 648         <xsl:apply-templates select="*[position()=2]"/>
 649         <m:mo mathcolor="Maroon">:></m:mo>
 650         <xsl:apply-templates select="*[position()=3]"/>
 651         <m:mo stretchy="false">)</m:mo>
 652        </xsl:otherwise>
 653        </xsl:choose>
 654       </xsl:when>
 655       <xsl:when test="$name='Prop'">
 656        <m:mo>Prop</m:mo>
 657       </xsl:when>
 658       <xsl:when test="$name='Set'">
 659        <m:mo>Set</m:mo>
 660       </xsl:when>
 661       <xsl:when test="$name='Type'">
 662        <m:mo>Type</m:mo>
 663       </xsl:when>
 664       <xsl:when test="$name='mutcase'">
 665        <xsl:choose>
 666        <xsl:when test="$charlength >= $framewidth">
 667         <xsl:variable name="charlength"><xsl:apply-templates select="*[position()=2]" mode="charcount"><xsl:with-param name="nosibling" select="1"/></xsl:apply-templates></xsl:variable>
 668         <m:mtable align="baseline 1" equalrows="false" columnalign="left">
 669          <m:mtr>
 670           <m:mtd>
 671            <m:mrow>
 672             <m:mo>&lt;</m:mo>
 673             <xsl:apply-templates select="*[position()=2]"/>
 674             <xsl:if test="$framewidth > $charlength">
 675              <m:mo>&gt;</m:mo>
 676              <m:mo>CASES</m:mo>
 677              <m:mphantom><m:mtext>_</m:mtext></m:mphantom>
 678              <xsl:apply-templates select="*[position()=3]"/>
 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:mo>&gt;</m:mo>
 688             <m:mo>CASES</m:mo>
 689             <m:mphantom><m:mtext>_</m:mtext></m:mphantom>
 690             <xsl:apply-templates select="*[position()=3]"/>
 691            </m:mrow>
 692           </m:mtd>
 693          </m:mtr>
 694          </xsl:if>
 695          <m:mtr>
 696           <m:mtd>
 697            <m:mrow>
 698             <m:mo>OF</m:mo>
 699            </m:mrow>
 700           </m:mtd>
 701          </m:mtr>
 702          <xsl:for-each select="*[position() mod 2 = 0 and position()>3]">
 703          <xsl:variable name="charlength"><xsl:apply-templates select="." mode="charcount"><xsl:with-param name="nosibling" select="1"/></xsl:apply-templates></xsl:variable>
 704          <m:mtr>
 705           <m:mtd>
 706            <m:mrow>
 707             <xsl:choose>
 708             <xsl:when test="position() = 1">
 709               <m:mphantom><m:mtext>|</m:mtext></m:mphantom>
 710             </xsl:when>
 711             <xsl:otherwise>
 712              <m:mo stretchy="false">|</m:mo>
 713             </xsl:otherwise>
 714             </xsl:choose>
 715             <m:mphantom><m:mtext>_</m:mtext></m:mphantom>
 716             <xsl:apply-templates select="."/>
 717             <xsl:if test="$framewidth > $charlength">
 718              <m:mo mathcolor="Green">&#x21d2;</m:mo>
 719              <xsl:apply-templates select="following-sibling::*[position()= 1]"/>
 720             </xsl:if>
 721            </m:mrow>
 722           </m:mtd>
 723          </m:mtr>
 724          <xsl:if test="$charlength >= $framewidth">
 725          <m:mtr>
 726           <m:mtd>
 727            <m:mrow>
 728             <m:mphantom><m:mtext>|_</m:mtext></m:mphantom>
 729             <m:mo mathcolor="Green">&#x21d2;</m:mo>
 730             <xsl:apply-templates select="following-sibling::*[position()= 1]"/>
 731            </m:mrow>
 732           </m:mtd>
 733          </m:mtr>
 734          </xsl:if>
 735         </xsl:for-each>
 736          <m:mtr>
 737           <m:mtd>
 738            <m:mrow>
 739             <m:mo>END</m:mo>
 740            </m:mrow>
 741           </m:mtd>
 742          </m:mtr>
 743         </m:mtable>
 744        </xsl:when>
 745        <xsl:otherwise>
 746         <m:mo>&lt;</m:mo><xsl:apply-templates select="*[position()=2]"/><m:mo>&gt;</m:mo>
 747         <m:mo>CASES</m:mo>
 748         <m:mphantom><m:mtext>_</m:mtext></m:mphantom>
 749         <xsl:apply-templates select="*[position()=3]"/>
 750         <m:mphantom><m:mtext>_</m:mtext></m:mphantom>
 751         <m:mo>OF</m:mo>
 752         <xsl:for-each select="*[position() mod 2 = 0 and position()>3]">
 753          <xsl:choose>
 754          <xsl:when test="position() != 1">
 755           <m:mo stretchy="false">|</m:mo>
 756          </xsl:when>
 757          </xsl:choose>
 758          <xsl:apply-templates select="."/>
 759          <m:mo mathcolor="Green">&#x21d2;</m:mo>
 760          <xsl:apply-templates select="following-sibling::*[position()= 1]"/>
 761         </xsl:for-each>
 762         <m:mphantom><m:mtext>_</m:mtext></m:mphantom>
 763         <m:mo>END</m:mo>
 764        </xsl:otherwise>
 765        </xsl:choose>
 766       </xsl:when>
 767       <xsl:when test="$name='fix'">
 768        <xsl:choose>
 769        <xsl:when test="$charlength >= $framewidth">
 770         <m:mtable align="baseline 1" equalrows="false" columnalign="left">
 771          <m:mtr>
 772           <m:mtd>
 773            <m:mrow>
 774             <m:mo>FIX</m:mo>
 775             <m:mphantom><m:mtext>_</m:mtext></m:mphantom>
 776             <m:mi><xsl:value-of select="m:ci"/></m:mi>
 777             <m:mo stretchy="false">{</m:mo>
 778            </m:mrow>
 779           </m:mtd>
 780          </m:mtr>
 781          <m:mtr>
 782           <m:mtd>
 783            <m:mrow>
 784             <m:mphantom><m:mtext>__</m:mtext></m:mphantom>
 785             <m:mtable align="baseline 1" equalrows="false" columnalign="left">
 786             <xsl:for-each select="m:bvar">
 787              <xsl:variable name="charlength"><xsl:apply-templates select="m:type" mode="charcount"><xsl:with-param name="nosibling" select="1"/></xsl:apply-templates></xsl:variable>
 788              <m:mtr>
 789               <m:mtd>
 790                <m:mrow>
 791                 <m:mi><xsl:value-of select="m:ci"/></m:mi>
 792                 <m:mo>:</m:mo>
 793                 <xsl:if test="$framewidth > $charlength">
 794                  <xsl:apply-templates select="m:type"/>
 795                 </xsl:if>
 796                </m:mrow>
 797               </m:mtd>
 798              </m:mtr>
 799              <xsl:if test="$charlength >= $framewidth">
 800              <m:mtr>
 801               <m:mtd>
 802                <m:mrow>
 803                 <m:mphantom><m:mtext>:=</m:mtext></m:mphantom>
 804                 <xsl:apply-templates select="m:type"/>
 805                </m:mrow>
 806               </m:mtd>
 807              </m:mtr>
 808              </xsl:if>
 809              <m:mtr>
 810               <m:mtd>
 811                <m:mrow>
 812                 <m:mo>:=</m:mo>
 813                 <xsl:apply-templates select="following-sibling::*[position()=1]"/>
 814                </m:mrow>
 815               </m:mtd>
 816              </m:mtr>
 817             </xsl:for-each>
 818             </m:mtable>
 819            </m:mrow>
 820           </m:mtd>
 821          </m:mtr>
 822          <m:mtr>
 823           <m:mtd>
 824            <m:mrow>
 825             <m:mo stretchy="false">}</m:mo>
 826            </m:mrow>
 827           </m:mtd>
 828          </m:mtr>
 829         </m:mtable>
 830        </xsl:when>
 831        <xsl:otherwise>
 832         <m:mo>FIX</m:mo>
 833         <m:mi><xsl:value-of select="m:ci"/></m:mi>
 834         <m:mo stretchy="false">{</m:mo>
 835         <m:mtable align="baseline 1" equalrows="false" columnalign="left">
 836         <xsl:for-each select="m:bvar">
 837          <m:mtr>
 838           <m:mtd>
 839            <m:mrow>
 840             <m:mi><xsl:value-of select="m:ci"/></m:mi>
 841             <m:mo>:</m:mo>
 842             <xsl:apply-templates select="m:type"/>
 843             <m:mo>:=</m:mo>
 844             <xsl:apply-templates select="following-sibling::*[position() = 1]"/>
 845             <xsl:if test="position()=last()">
 846              <m:mo stretchy="false">}</m:mo>
 847             </xsl:if>
 848            </m:mrow>
 849           </m:mtd>
 850          </m:mtr>
 851          </xsl:for-each>
 852         </m:mtable>
 853        </xsl:otherwise>
 854        </xsl:choose>
 855       </xsl:when>
 856       <xsl:when test="$name='cofix'">
 857        <xsl:choose>
 858        <xsl:when test="$charlength >= $framewidth">
 859         <m:mtable align="baseline 1" equalrows="false" columnalign="left">
 860          <m:mtr>
 861           <m:mtd>
 862            <m:mrow>
 863             <m:mo>COFIX</m:mo>
 864             <m:mphantom><m:mtext>_</m:mtext></m:mphantom>
 865             <m:mi><xsl:value-of select="m:ci"/></m:mi>
 866             <m:mo stretchy="false">{</m:mo>
 867            </m:mrow>
 868           </m:mtd>
 869          </m:mtr>
 870          <m:mtr>
 871           <m:mtd>
 872            <m:mrow>
 873             <m:mphantom><m:mtext>__</m:mtext></m:mphantom>
 874             <m:mtable align="baseline 1" equalrows="false" columnalign="left">
 875             <xsl:for-each select="m:bvar">
 876              <xsl:variable name="charlength"><xsl:apply-templates select="m:type" mode="charcount"><xsl:with-param name="nosibling" select="1"/></xsl:apply-templates></xsl:variable>
 877              <m:mtr>
 878               <m:mtd>
 879                <m:mrow>
 880                 <m:mi><xsl:value-of select="m:ci"/></m:mi>
 881                 <m:mo>:</m:mo>
 882                 <xsl:if test="$framewidth > $charlength">
 883                  <xsl:apply-templates select="m:type"/>
 884                 </xsl:if>
 885                </m:mrow>
 886               </m:mtd>
 887              </m:mtr>
 888              <xsl:if test="$charlength >= $framewidth">
 889              <m:mtr>
 890               <m:mtd>
 891                <m:mrow>
 892                 <m:mphantom><m:mtext>:=</m:mtext></m:mphantom>
 893                 <xsl:apply-templates select="m:type"/>
 894                </m:mrow>
 895               </m:mtd>
 896              </m:mtr>
 897              </xsl:if>
 898              <m:mtr>
 899               <m:mtd>
 900                <m:mrow>
 901                 <m:mo>:=</m:mo>
 902                 <xsl:apply-templates select="following-sibling::*[position() = 1]"/>
 903                </m:mrow>
 904               </m:mtd>
 905              </m:mtr>
 906             </xsl:for-each>
 907             </m:mtable>
 908            </m:mrow>
 909           </m:mtd>
 910          </m:mtr>
 911          <m:mtr>
 912           <m:mtd>
 913            <m:mrow>
 914             <m:mo stretchy="false">}</m:mo>
 915            </m:mrow>
 916           </m:mtd>
 917          </m:mtr>
 918         </m:mtable>
 919        </xsl:when>
 920        <xsl:otherwise>
 921         <m:mo>COFIX</m:mo>
 922         <m:mi><xsl:value-of select="m:ci"/></m:mi>
 923         <m:mo stretchy="false">{</m:mo>
 924         <m:mtable align="baseline 1" equalrows="false" columnalign="left">
 925         <xsl:for-each select="m:bvar">
 926          <m:mtr>
 927           <m:mtd>
 928            <m:mrow>
 929             <m:mi><xsl:value-of select="m:ci"/></m:mi>
 930             <m:mo>:</m:mo>
 931             <xsl:apply-templates select="m:type"/>
 932             <m:mo>:=</m:mo>
 933             <xsl:apply-templates select="following-sibling::*[position() = 1]"/>
 934             <xsl:if test="position()=last()">
 935              <m:mo stretchy="false">}</m:mo>
 936             </xsl:if>
 937            </m:mrow>
 938           </m:mtd>
 939          </m:mtr>
 940          </xsl:for-each>
 941         </m:mtable>
 942        </xsl:otherwise>
 943        </xsl:choose>
 944       </xsl:when>
 945       <!-- ***************************************** -->
 946       <!-- *********** PROOF ELEMENTS ************** -->
 947       <!-- ***************************************** -->
 948       <xsl:when test="$name='proof'">
 949         <m:mtable align="baseline 1" equalrows="false" columnalign="left">
 950          <m:mtr>
 951           <m:mtd>
 952            <m:mrow>
 953             <xsl:apply-templates select="*[position()=2]"/>
 954            </m:mrow>
 955           </m:mtd>
 956          </m:mtr>
 957          <m:mtr>
 958           <m:mtd>
 959            <m:mrow>
 960             <m:mtext mathcolor="Maroon">we proved </m:mtext>
 961             <m:mphantom><m:mtext>_</m:mtext></m:mphantom>
 962             <xsl:apply-templates select="*[position()=3]"/>
 963            </m:mrow>
 964           </m:mtd>
 965          </m:mtr>
 966         </m:mtable>
 967       </xsl:when>
 968       <xsl:when test="$name='letin1'">
 969         <m:mtable align="baseline 1" equalrows="false" columnalign="left">
 970          <m:mtr>
 971           <m:mtd>
 972            <m:mrow>
 973             <xsl:apply-templates select="*[2]"/>
 974            </m:mrow>
 975           </m:mtd>
 976          </m:mtr>
 977          <m:mtr>
 978           <m:mtd>
 979            <m:mrow>
 980             <xsl:apply-templates select="*[3]"/>
 981            </m:mrow>
 982           </m:mtd>
 983          </m:mtr>
 984         </m:mtable>
 985       </xsl:when>
 986       <xsl:when test="$name='letin'">
 987         <m:mtable align="baseline 1" equalrows="false" columnalign="left">
 988          <!-- <xsl:for-each select="APPLY[m:csymbol and (string(m:csymbol)='let')]"> -->
 989          <xsl:for-each select="*[(last() > position()) and (position()>1)]">
 990          <m:mtr>
 991           <m:mtd>
 992            <m:mrow>
 993             <xsl:apply-templates select="."/>
 994            </m:mrow>
 995           </m:mtd>
 996          </m:mtr>
 997          </xsl:for-each>
 998          <m:mtr>
 999           <m:mtd>
1000            <m:mrow>
1001             <xsl:apply-templates select="*[position()=last()]"/>
1002            </m:mrow>
1003           </m:mtd>
1004          </m:mtr>
1005         </m:mtable>
1006       </xsl:when>
1007       <xsl:when test="$name='let'">
1008        <m:mtext>(</m:mtext>
1009        <xsl:apply-templates select="m:ci"/>
1010        <m:mtext>) </m:mtext>
1011        <xsl:apply-templates select="*[3]"/>
1012       </xsl:when>
1013       <xsl:when test="$name='rw_step'">
1014         <m:mtable align="baseline 1" equalrows="false" columnalign="left">
1015          <m:mtr>
1016           <m:mtd>
1017            <m:mrow>
1018             <xsl:choose>
1019              <xsl:when test="name(*[2])='m:apply'">
1020               <xsl:apply-templates select="*[2]"/>
1021              </xsl:when>
1022              <xsl:otherwise>
1023               <m:mtext>Consider</m:mtext>
1024               <m:mphantom><m:mtext>_</m:mtext></m:mphantom>
1025               <xsl:apply-templates select="*[2]"/>
1026              </xsl:otherwise>
1027             </xsl:choose>
1028            </m:mrow>
1029           </m:mtd>
1030          </m:mtr>
1031          <m:mtr>
1032           <m:mtd>
1033            <m:mrow>
1034             <m:mtext>Rewrite</m:mtext>
1035             <m:mphantom><m:mtext>_</m:mtext></m:mphantom>
1036             <xsl:apply-templates select="*[3]"/>
1037             <m:mphantom><m:mtext>_</m:mtext></m:mphantom>
1038             <m:mtext>with</m:mtext>
1039             <m:mphantom><m:mtext>_</m:mtext></m:mphantom>
1040             <xsl:apply-templates select="*[4]"/>
1041             <m:mphantom><m:mtext>_</m:mtext></m:mphantom>
1042             <m:mtext>by</m:mtext>
1043             <m:mphantom><m:mtext>_</m:mtext></m:mphantom>
1044             <xsl:apply-templates select="*[5]"/>
1045            </m:mrow>
1046           </m:mtd>
1047          </m:mtr>
1048         </m:mtable>
1049       </xsl:when>
1050       <!-- not existing any more
1051       <xsl:when test="$name='thread'">
1052         <m:mtable align="baseline 1" equalrows="false" columnalign="left">
1053          <m:mtr>
1054           <m:mtd>
1055            <m:mrow>
1056             <xsl:choose>
1057              <xsl:when test="name(*[last()])='m:apply'">
1058               <xsl:apply-templates select="*[last()]"/>
1059              </xsl:when>
1060              <xsl:otherwise>
1061               <m:mtext>Consider</m:mtext>
1062               <m:mphantom><m:mtext>_</m:mtext></m:mphantom>
1063               <xsl:apply-templates select="*[last()]"/>
1064              </xsl:otherwise>
1065             </xsl:choose>
1066            </m:mrow>
1067           </m:mtd>
1068          </m:mtr>
1069          <xsl:apply-templates mode="thread" select="*[(last()-2)]"/>
1070         </m:mtable>
1071       </xsl:when>
1072       -->
1073       <xsl:when test="$name='rewrite_and_apply'">
1074         <m:mtable align="baseline 1" equalrows="false" columnalign="left">
1075          <m:mtr>
1076           <m:mtd>
1077            <m:mrow>
1078             <xsl:apply-templates select="*[2]"/>
1079            </m:mrow>
1080           </m:mtd>
1081          </m:mtr>
1082          <m:mtr>
1083           <m:mtd>
1084            <m:mrow>
1085             <m:mtext>Then apply it to</m:mtext>
1086             <m:mphantom><m:mtext>_</m:mtext></m:mphantom>
1087             <xsl:apply-templates select="*[position()>2]"/>
1088            </m:mrow>
1089           </m:mtd>
1090          </m:mtr>
1091        </m:mtable>
1092       </xsl:when>
1093       <!-- NAT_IND -->
1094       <xsl:when test="$name='nat_ind'">
1095         <m:mtable align="baseline 1" equalrows="false" columnalign="left">
1096          <m:mtr>
1097           <m:mtd>
1098            <m:mtext>By induction</m:mtext>
1099           </m:mtd>
1100          </m:mtr>
1101          <m:mtr>
1102           <m:mtd>
1103            <m:mrow>
1104             <m:mtext>base case:</m:mtext>
1105             <xsl:apply-templates select="*[2]"/>
1106            </m:mrow>
1107           </m:mtd>
1108          </m:mtr>
1109          <m:mtr>
1110           <m:mtd>
1111            <m:mrow>
1112             <m:mtext>inductive case:</m:mtext>
1113             <xsl:apply-templates select="*[3]"/>
1114            </m:mrow>
1115           </m:mtd>
1116          </m:mtr>
1117         </m:mtable>
1118       </xsl:when>
1119       <!-- AND_IND -->
1120       <xsl:when test="$name='and_ind'">
1121         <m:mtable align="baseline 1" equalrows="false" columnalign="left">
1122          <m:mtr>
1123           <m:mtd>
1124            <m:mrow>
1125             <xsl:choose>
1126              <xsl:when test="name(*[2])='m:apply'">
1127               <xsl:apply-templates select="*[2]"/>
1128              </xsl:when>
1129              <xsl:otherwise>
1130               <m:mtext>Consider</m:mtext>
1131               <m:mphantom><m:mtext>_</m:mtext></m:mphantom>
1132               <xsl:apply-templates select="*[2]"/>
1133              </xsl:otherwise>
1134             </xsl:choose>
1135            </m:mrow>
1136           </m:mtd>
1137          </m:mtr>
1138          <m:mtr>
1139           <m:mtd>
1140            <m:mtext>In particular, we have</m:mtext>
1141           </m:mtd>
1142          </m:mtr>
1143          <m:mtr>
1144           <m:mtd>
1145            <m:mrow>
1146             <m:mtext>(</m:mtext>
1147             <xsl:apply-templates select="*[3]"/>
1148             <m:mtext>)</m:mtext>
1149             <m:mphantom><m:mtext>_</m:mtext></m:mphantom>
1150             <xsl:apply-templates select="*[4]"/>
1151             </m:mrow>
1152           </m:mtd>
1153          </m:mtr>
1154          <m:mtr>
1155           <m:mtd>
1156            <m:mrow>
1157             <m:mtext>(</m:mtext>
1158             <xsl:apply-templates select="*[5]"/>
1159             <m:mtext>)</m:mtext>
1160             <m:mphantom><m:mtext>_</m:mtext></m:mphantom>
1161             <xsl:apply-templates select="*[6]"/>
1162             </m:mrow>
1163           </m:mtd>
1164          </m:mtr>
1165          <m:mtr>
1166           <m:mtd>
1167            <m:mrow>
1168             <xsl:apply-templates select="*[7]"/>
1169            </m:mrow>
1170           </m:mtd>
1171          </m:mtr>
1172         </m:mtable>
1173       </xsl:when>
1174       <xsl:when test="$name='or_ind'">
1175         <m:mtable align="baseline 1" equalrows="false" columnalign="left">
1176          <m:mtr>
1177           <m:mtd>
1178            <m:mrow>
1179             <xsl:choose>
1180              <xsl:when test="name(*[2])='m:apply'">
1181               <xsl:apply-templates select="*[2]"/>
1182              </xsl:when>
1183              <xsl:otherwise>
1184               <m:mtext>Consider</m:mtext>
1185               <m:mphantom><m:mtext>_</m:mtext></m:mphantom>
1186               <xsl:apply-templates select="*[2]"/>
1187              </xsl:otherwise>
1188             </xsl:choose>
1189            </m:mrow>
1190           </m:mtd>
1191          </m:mtr>
1192          <m:mtr>
1193           <m:mtd>
1194            <m:mtext>We prove</m:mtext>
1195            <m:mphantom><m:mtext>_</m:mtext></m:mphantom>
1196            <xsl:apply-templates select="*[3]"/>
1197            <m:mphantom><m:mtext>_</m:mtext></m:mphantom>
1198            <m:mtext>by cases:</m:mtext>
1199           </m:mtd>
1200          </m:mtr>
1201          <m:mtr>
1202           <m:mtd>
1203            <m:mrow>
1204             <m:mtext>*</m:mtext>
1205             <xsl:apply-templates select="*[4]"/>
1206            </m:mrow>
1207           </m:mtd>
1208          </m:mtr>
1209          <m:mtr>
1210           <m:mtd>
1211            <m:mrow>
1212             <m:mtext>*</m:mtext>
1213             <xsl:apply-templates select="*[5]"/>
1214            </m:mrow>
1215           </m:mtd>
1216          </m:mtr>
1217         </m:mtable>
1218       </xsl:when>
1219       <xsl:when test="$name='ex_ind'">
1220         <m:mtable align="baseline 1" equalrows="false" columnalign="left">
1221          <m:mtr>
1222           <m:mtd>
1223            <m:mrow>
1224             <xsl:choose>
1225              <xsl:when test="name(*[2])='m:apply'">
1226               <xsl:apply-templates select="*[2]"/>
1227              </xsl:when>
1228              <xsl:otherwise>
1229               <m:mtext>Consider</m:mtext>
1230               <m:mphantom><m:mtext>_</m:mtext></m:mphantom>
1231               <xsl:apply-templates select="*[2]"/>
1232              </xsl:otherwise>
1233             </xsl:choose>
1234            </m:mrow>
1235           </m:mtd>
1236          </m:mtr>
1237          <m:mtr>
1238           <m:mtd>
1239            <m:mtext>Let</m:mtext>
1240            <m:mphantom><m:mtext>_</m:mtext></m:mphantom>
1241            <xsl:apply-templates select="*[3]"/>
1242            <m:mtext>:</m:mtext>
1243            <xsl:apply-templates select="*[4]"/>
1244            <m:mphantom><m:mtext>_</m:mtext></m:mphantom>
1245            <m:mtext>such that</m:mtext>
1246            <m:mphantom><m:mtext>_</m:mtext></m:mphantom>
1247            <m:mtext>(</m:mtext>
1248             <xsl:apply-templates select="*[5]"/>
1249            <m:mtext>)</m:mtext>
1250            <m:mphantom><m:mtext>_</m:mtext></m:mphantom>
1251            <xsl:apply-templates select="*[6]"/>
1252           </m:mtd>
1253          </m:mtr>
1254          <m:mtr>
1255           <m:mtd>
1256            <m:mrow>
1257             <xsl:apply-templates select="*[7]"/>
1258            </m:mrow>
1259           </m:mtd>
1260          </m:mtr>
1261         </m:mtable>
1262       </xsl:when>
1263       <xsl:otherwise>
1264        <m:ci>ERROR</m:ci>
1265       </xsl:otherwise>
1266      </xsl:choose>
1267     </m:mrow>
1268 </xsl:template>
1269
1270 <!-- Il modo Thread non esiste piu'
1271 <xsl:template match="*" mode="thread">
1272  <xsl:variable name="name"><xsl:value-of select="following-sibling::*[position()=1]/m:csymbol"/></xsl:variable>
1273  <xsl:choose>
1274   <xsl:when test="$name='rw_step'">
1275          <m:mtr>
1276           <m:mtd>
1277            <m:mrow>
1278             <m:mtext>Rewrite</m:mtext>
1279             <m:mphantom><m:mtext>_</m:mtext></m:mphantom>
1280             <xsl:apply-templates select="following-sibling::*[position()=1]/*[2]"/>
1281             <m:mphantom><m:mtext>_</m:mtext></m:mphantom>
1282             <m:mtext>with</m:mtext>
1283             <m:mphantom><m:mtext>_</m:mtext></m:mphantom>
1284             <xsl:apply-templates select="following-sibling::*[position()=1]/*[3]"/>
1285             <m:mphantom><m:mtext>_</m:mtext></m:mphantom>
1286             <m:mtext>by</m:mtext>
1287             <m:mphantom><m:mtext>_</m:mtext></m:mphantom>
1288             <xsl:apply-templates select="following-sibling::*[position()=1]/*[4]"/>
1289            </m:mrow>
1290           </m:mtd>
1291          </m:mtr>
1292          <m:mtr>
1293           <m:mtd>
1294            <m:mrow>
1295             <m:mtext mathcolor="Maroon">we get</m:mtext>
1296             <m:mphantom><m:mtext>_</m:mtext></m:mphantom>
1297             <xsl:apply-templates select="."/>
1298            </m:mrow>
1299           </m:mtd>
1300          </m:mtr>
1301    </xsl:when>
1302    <xsl:otherwise>
1303          <m:mtr>
1304           <m:mtd>
1305            <m:mrow>
1306             <xsl:apply-templates select="following-sibling::*[position()=1]"/>
1307            </m:mrow>
1308           </m:mtd>
1309          </m:mtr>
1310          <m:mtr>
1311           <m:mtd>
1312            <m:mrow>
1313             <m:mtext mathcolor="Maroon">we get</m:mtext>
1314             <m:mphantom><m:mtext>_</m:mtext></m:mphantom>
1315             <xsl:apply-templates select="."/>
1316            </m:mrow>
1317           </m:mtd>
1318          </m:mtr>
1319     </xsl:otherwise>
1320    </xsl:choose>
1321          <xsl:apply-templates mode="thread" select="preceding-sibling::*[position()=2]"/>
1322 </xsl:template>
1323 -->
1324
1325 <!-- LAMBDA -->
1326
1327 <xsl:template match="m:lambda">
1328     <xsl:variable name="charlength"><xsl:apply-templates select="*[position()=1]" mode="charcount"/></xsl:variable>
1329     <m:mrow helm:xref="{@helm:xref}">
1330      <xsl:choose>
1331      <xsl:when test="$charlength >= $framewidth">
1332       <m:mtable align="baseline 1" equalrows="false" columnalign="left">
1333         <m:mtr>
1334           <m:mtd>
1335             <m:mo mathcolor="Red">&#x03bb;</m:mo>
1336             <xsl:apply-templates select="m:bvar"/>
1337           </m:mtd>
1338          </m:mtr>
1339        <m:mtr>
1340         <m:mtd>
1341          <m:mrow>
1342           <m:mo>.</m:mo>
1343           <xsl:apply-templates select="*[position()=2]"/>
1344          </m:mrow>
1345         </m:mtd>
1346        </m:mtr>
1347       </m:mtable>
1348      </xsl:when>
1349      <xsl:otherwise>
1350       <m:mo mathcolor="Red">&#x03bb;</m:mo>
1351       <xsl:apply-templates select="m:bvar/m:ci"/>
1352       <m:mo>:</m:mo>
1353       <xsl:apply-templates select="m:bvar/m:type"/>
1354       <m:mo>.</m:mo>
1355       <xsl:apply-templates select="*[position()=2]"/>
1356      </xsl:otherwise>
1357      </xsl:choose>
1358     </m:mrow>
1359 </xsl:template>
1360
1361 <!-- *********************************** -->
1362 <!-- BASE SET OF MATHML CONTENT ELEMENTS -->
1363 <!-- *********************************** -->
1364
1365 <!-- Logic -->
1366
1367 <xsl:template match = "m:apply[m:eq[1]]">
1368  <xsl:variable name="charlength">
1369   <xsl:apply-templates select="*[1]" mode="charcount"/>
1370  </xsl:variable>
1371  <xsl:choose>
1372   <xsl:when test="$charlength >= $framewidth">
1373    <m:mtable align="baseline 1" equalrows="false" columnalign="left">
1374     <xsl:if test="@helm:xref">
1375      <xsl:attribute name="helm:xref">
1376       <xsl:value-of select="@helm:xref"/>
1377      </xsl:attribute>
1378     </xsl:if>
1379     <m:mtr>
1380      <m:mtd>
1381       <m:mo stretchy="false">(</m:mo>
1382       <xsl:apply-templates select="*[position()=2]"/>
1383      </m:mtd>
1384     </m:mtr>
1385     <xsl:for-each select = "*[position()>2]">
1386      <m:mtr>
1387       <m:mtd>
1388        <m:mphantom><m:mtext>__</m:mtext></m:mphantom>
1389        <m:mo helm:xref="{m:in/@helm:xref}">=</m:mo>
1390        <xsl:apply-templates select="."/>
1391       </m:mtd>
1392      </m:mtr>
1393     </xsl:for-each>
1394     <m:mtr>
1395      <m:mtd>
1396       <m:mo stretchy="false">)</m:mo>
1397      </m:mtd>
1398     </m:mtr>
1399    </m:mtable>
1400   </xsl:when>
1401   <xsl:otherwise>
1402    <xsl:apply-imports/>
1403   </xsl:otherwise>
1404  </xsl:choose>
1405 </xsl:template>
1406
1407
1408 <xsl:template match = "m:apply[m:and[1]|m:or[1]
1409           |m:geq[1]|m:leq[1]|m:gt[1]|m:lt[1]
1410           |m:in[1]|m:intesect[1]|m:union[1]|m:subset[1]
1411           |m:prsubset|m:setdiff[1]]">
1412  <xsl:variable name="symbol">
1413   <xsl:choose>
1414    <xsl:when test="m:and[1]">
1415     <xsl:value-of select="'wedge'"/>
1416    </xsl:when>
1417    <xsl:when test="m:or[1]">
1418     <xsl:value-of select="'vee'"/>
1419    </xsl:when>
1420    <xsl:when test="m:geq[1]">
1421     <xsl:value-of select="'geq'"/>
1422    </xsl:when>
1423    <xsl:when test="m:leq[1]">
1424     <xsl:value-of select="'leq'"/>
1425    </xsl:when>
1426    <xsl:when test="m:gt[1]">
1427     <xsl:value-of select="'gt'"/>
1428    </xsl:when>
1429    <xsl:when test="m:lt[1]">
1430     <xsl:value-of select="'lt'"/>
1431    </xsl:when>
1432    <xsl:when test="m:eq[1]">
1433     <xsl:value-of select="'Equal'"/>
1434    </xsl:when>
1435    <xsl:when test="m:in[1]">
1436     <xsl:value-of select="'Element'"/>
1437    </xsl:when>
1438    <xsl:when test="m:subset[1]">
1439     <xsl:value-of select="'SubsetEqual'"/>
1440    </xsl:when>
1441    <xsl:when test="m:prsubset[1]">
1442     <xsl:value-of select="'subset'"/>
1443    </xsl:when>
1444    <xsl:when test="m:intersect[1]">
1445     <xsl:value-of select="'Intersection'"/>
1446    </xsl:when>
1447    <xsl:when test="m:union[1]">
1448     <xsl:value-of select="'Union'"/>
1449    </xsl:when>
1450    <xsl:when test="m:setdiff[1]">
1451     <xsl:value-of select="'Backslash'"/>
1452    </xsl:when>
1453   </xsl:choose>
1454  </xsl:variable>
1455  <xsl:variable name="charlength">
1456   <xsl:apply-templates select="*[1]" mode="charcount"/>
1457  </xsl:variable>
1458  <xsl:choose>
1459   <xsl:when test="$charlength >= $framewidth">
1460    <m:mtable align="baseline 1" equalrows="false" columnalign="left">
1461     <xsl:if test="@helm:xref">
1462      <xsl:attribute name="helm:xref">
1463       <xsl:value-of select="@helm:xref"/>
1464      </xsl:attribute>
1465     </xsl:if>
1466     <m:mtr>
1467      <m:mtd>
1468       <m:mo stretchy="false">(</m:mo>
1469       <xsl:apply-templates select="*[position()=2]"/>
1470      </m:mtd>
1471     </m:mtr>
1472     <xsl:for-each select = "*[position()>2]">
1473      <m:mtr>
1474       <m:mtd>
1475        <m:mphantom><m:mtext>__</m:mtext></m:mphantom>
1476        <m:mo helm:xref="{*[1]/@helm:xref}">
1477         <m:mchar name="{$symbol}"/>
1478        </m:mo>
1479        <xsl:apply-templates select="."/>
1480       </m:mtd>
1481      </m:mtr>
1482     </xsl:for-each>
1483     <m:mtr>
1484      <m:mtd>
1485       <m:mo stretchy="false">)</m:mo>
1486      </m:mtd>
1487     </m:mtr>
1488    </m:mtable>
1489   </xsl:when>
1490   <xsl:otherwise>
1491    <xsl:apply-imports/>
1492   </xsl:otherwise>
1493  </xsl:choose>
1494 </xsl:template>
1495
1496 <xsl:template match = "m:set">
1497  <xsl:choose>
1498   <xsl:when test="count(child::*) = 0">
1499    <m:mi>
1500     <m:mchar name="emptyset"/>
1501    </m:mi>
1502   </xsl:when>
1503   <xsl:otherwise>
1504    <xsl:variable name="charlength">
1505     <xsl:apply-templates select="*[1]" mode="charcount"/>
1506    </xsl:variable>
1507    <xsl:choose>
1508     <xsl:when test="$charlength >= $framewidth">
1509      <xsl:choose>
1510       <xsl:when test="name(*[1]) = 'm:bvar'">
1511        <m:mtable align="baseline 1" equalrows="false" columnalign="left">
1512         <m:mtr>
1513          <m:mtd>
1514           <m:mo stretchy="false">{</m:mo>
1515           <xsl:apply-templates select="*[position()=1]"/>
1516          </m:mtd>
1517         </m:mtr>
1518         <m:mtr>
1519          <m:mtd>
1520           <m:mphantom><m:mtext>{</m:mtext></m:mphantom>
1521           <m:mo stretchy="false">|</m:mo>
1522           <xsl:apply-templates select="m:condition/*[1]"/>
1523          </m:mtd>
1524         </m:mtr>
1525         <m:mtr>
1526          <m:mtd>
1527           <m:mo stretchy="false">}</m:mo>
1528          </m:mtd>
1529         </m:mtr>
1530        </m:mtable>
1531       </xsl:when>
1532       <xsl:otherwise>
1533        <m:mtable align="baseline 1" equalrows="false" columnalign="left">
1534         <m:mtr>
1535          <m:mtd>
1536           <m:mo stretchy="false">{</m:mo>
1537           <xsl:apply-templates select="*[position()=1]"/>
1538           <xsl:if test="position() != last()">
1539            <mo>,</mo>
1540           </xsl:if>
1541          </m:mtd>
1542         </m:mtr>
1543         <xsl:for-each select = "*[position()>2]">
1544          <m:mtr>
1545           <m:mtd>
1546            <m:mphantom><m:mtext>{</m:mtext></m:mphantom>
1547            <xsl:apply-templates select="."/>
1548            <xsl:if test="position() != last()">
1549             <mo>,</mo>
1550            </xsl:if>
1551           </m:mtd>
1552          </m:mtr>
1553         </xsl:for-each>
1554         <m:mtr>
1555          <m:mtd>
1556           <m:mo stretchy="false">}</m:mo>
1557          </m:mtd>
1558         </m:mtr>
1559        </m:mtable>
1560       </xsl:otherwise>
1561      </xsl:choose>
1562     </xsl:when>
1563     <xsl:otherwise>
1564      <xsl:apply-imports/>
1565     </xsl:otherwise>
1566    </xsl:choose>
1567   </xsl:otherwise>
1568  </xsl:choose>
1569 </xsl:template>
1570
1571 <xsl:template match = "m:apply[m:card[1]]">
1572  <m:mo stretchy="false">|</m:mo>
1573   <xsl:apply-templates select="*[2]"/>
1574  <m:mo stretchy="false">|</m:mo>
1575 </xsl:template>
1576
1577 <!-- *********************************** -->
1578 <!--          PROOF ELEMENTS             -->
1579 <!-- *********************************** -->
1580
1581
1582
1583 <!--**********************-->
1584 <!--       COUNTING       -->
1585 <!--**********************-->
1586
1587 <xsl:template match="m:cn|m:and|m:or|m:not|m:exists|m:eq|m:lt|m:leq|m:gt|m:geq
1588  |m:in|m:notin|m:intersect|m:union|m:subset|m:prsubset|m:card|m:setdiff
1589  |m:plus|m:minus|m:times" mode="charcount">
1590 <xsl:param name="incurrent_length" select="0"/>
1591     <xsl:choose>
1592     <xsl:when test="$framewidth > ($incurrent_length + 3 + string-length())">
1593      <xsl:variable name="siblength">
1594       <xsl:apply-templates select="following-sibling::*[position()=1]" mode="charcount">
1595        <xsl:with-param name="incurrent_length" select="$incurrent_length + string-length()"/>
1596       </xsl:apply-templates>
1597      </xsl:variable>
1598      <xsl:choose>
1599      <xsl:when test="string($siblength) = &quot;&quot;">
1600       <xsl:value-of select="$incurrent_length + 3 + string-length()"/>
1601      </xsl:when>
1602      <xsl:otherwise>
1603       <xsl:value-of select="number($siblength)"/>
1604      </xsl:otherwise>
1605      </xsl:choose>
1606     </xsl:when>
1607     <xsl:otherwise>
1608      <xsl:value-of select="$incurrent_length + 3 + string-length()"/>
1609     </xsl:otherwise>
1610     </xsl:choose>
1611 </xsl:template>
1612
1613 <xsl:template match="m:ci|m:csymbol" mode="charcount">
1614 <xsl:param name="incurrent_length" select="0"/>
1615 <xsl:param name="nosibling" select="0"/>
1616     <xsl:choose>
1617     <xsl:when test="$framewidth > ($incurrent_length + string-length()) and ($nosibling = 0)">
1618      <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>
1619      <xsl:choose>
1620      <xsl:when test="string($siblength) = &quot;&quot;">
1621       <xsl:value-of select="$incurrent_length + string-length()"/>
1622      </xsl:when>
1623      <xsl:otherwise>
1624       <xsl:value-of select="number($siblength)"/>
1625      </xsl:otherwise>
1626      </xsl:choose>
1627     </xsl:when>
1628     <xsl:otherwise>
1629      <xsl:value-of select="$incurrent_length + string-length()"/>
1630     </xsl:otherwise>
1631     </xsl:choose>
1632 </xsl:template>
1633
1634 <xsl:template match="*" mode="charcount">
1635 <xsl:param name="incurrent_length" select="0"/>
1636 <xsl:param name="nosibling" select="0"/>
1637  <xsl:choose>
1638   <xsl:when test="count(child::*) = 0">
1639    <xsl:value-of select="$incurrent_length"/>
1640   </xsl:when>
1641   <xsl:otherwise>
1642     <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>
1643     <xsl:choose>
1644     <xsl:when test="$framewidth > number($childlength) and ($nosibling = 0)">
1645      <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>
1646      <xsl:choose>
1647      <xsl:when test="string($siblength) = &quot;&quot;">
1648       <xsl:value-of select="number($childlength)"/>
1649      </xsl:when>
1650      <xsl:otherwise>
1651       <xsl:value-of select="number($siblength)"/>
1652      </xsl:otherwise>
1653      </xsl:choose>
1654     </xsl:when>
1655     <xsl:otherwise>
1656      <xsl:value-of select="number($childlength)"/>
1657     </xsl:otherwise>
1658     </xsl:choose>
1659   </xsl:otherwise>
1660  </xsl:choose>
1661 </xsl:template>
1662
1663 </xsl:stylesheet>
1664
1665
1666