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