helm/style/mmlextension.xsl

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