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
  44 <xsl:import href="mmlnotation.xsl"/>
  45
  46 <xsl:import href="mmltheoryextension.xsl"/>
  47
  48
  49 <xsl:param name="explodeall" select="false()"/>
  50
  51 <!--***********************************************************************-->
  52 <!-- Parameter affecting line-breaking                                     -->
  53 <!--***********************************************************************-->
  54
  55 <xsl:variable name="framewidth" select="35"/>
  56
  57 <!--***********************************************************************-->
  58 <!-- Gli oggetti sono stampati come mtext all'interno di una marca toplevel-->
  59 <!-- math ma al di fuori di semantics. Ora vi sono tanti semantics quanti  -->
  60 <!-- sono i termini: la presentation per un termine e' generata come primo -->
  61 <!-- figlio di un semantics e l'originario content viene inserito nel      -->
  62 <!-- nel secondo figlio di semantics, annotation-xml                       -->
  63 <!--***********************************************************************-->
  64
  65 <!--**********************-->
  66 <!--        OBJECTS       -->
  67 <!--**********************-->
  68
  69 <xsl:param name="type" select="'standalone'"/>
  70
  71 <xsl:template match="/">
  72  <xsl:choose>
  73   <xsl:when test="$type = 'standalone'">
  74    <xsl:apply-templates select="*"/>
  75   </xsl:when>
  76   <xsl:otherwise>
  77    <to_be_embedded>
  78     <xsl:apply-templates select="*"/>
  79    </to_be_embedded>
  80   </xsl:otherwise>
  81  </xsl:choose>
  82 </xsl:template>
  83
  84 <!-- DEFINITION -->
  85
  86 <xsl:template match="Definition">
  87     <m:math>
  88      <m:mtable align="baseline 1" equalrows="false" columnalign="left" helm:xref="{@helm:xref}">
  89       <m:mtr>
  90        <m:mtd>
  91         <m:mrow>
  92          <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>
  93         </m:mrow>
  94        </m:mtd>
  95       </m:mtr>
  96       <m:mtr>
  97        <m:mtd>
  98         <m:mrow>
  99          <m:mphantom><m:mtext>__</m:mtext></m:mphantom>
 100          <xsl:apply-templates select="type/*[1]"/>
 101         </m:mrow>
 102        </m:mtd>
 103       </m:mtr>
 104       <m:mtr>
 105        <m:mtd>
 106         <m:mrow>
 107          <m:mtext>AS</m:mtext>
 108         </m:mrow>
 109        </m:mtd>
 110       </m:mtr>
 111       <m:mtr>
 112        <m:mtd>
 113         <m:mrow>
 114          <m:mphantom><m:mtext>__</m:mtext></m:mphantom>
 115          <xsl:apply-templates select="body/*[1]"/>
 116         </m:mrow>
 117        </m:mtd>
 118       </m:mtr>
 119      </m:mtable>
 120     </m:math>
 121 </xsl:template>
 122
 123 <!-- AXIOM -->
 124
 125 <xsl:template match="Axiom">
 126     <m:math>
 127      <m:mtable align="baseline 1" equalrows="false" columnalign="left" helm:xref="{@helm:xref}">
 128       <m:mtr>
 129        <m:mtd>
 130         <m:mrow>
 131          <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>
 132         </m:mrow>
 133        </m:mtd>
 134       </m:mtr>
 135       <m:mtr>
 136        <m:mtd>
 137         <m:mrow>
 138          <m:mphantom><m:mtext>__</m:mtext></m:mphantom>
 139          <xsl:apply-templates select="type/*[1]"/>
 140         </m:mrow>
 141        </m:mtd>
 142       </m:mtr>
 143      </m:mtable>
 144     </m:math>
 145 </xsl:template>
 146
 147 <!-- UNFINISHED PROOF -->
 148
 149 <xsl:template match="CurrentProof">
 150     <m:math>
 151      <m:mtable align="baseline 1" equalrows="false" columnalign="left" helm:xref="{@helm:xref}">
 152       <m:mtr>
 153        <m:mtd>
 154         <m:mrow>
 155          <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>
 156         </m:mrow>
 157        </m:mtd>
 158       </m:mtr>
 159       <m:mtr>
 160        <m:mtd>
 161         <m:mrow>
 162          <m:mtext>THESIS:</m:mtext>
 163         </m:mrow>
 164        </m:mtd>
 165       </m:mtr>
 166       <m:mtr>
 167        <m:mtd>
 168         <m:mrow>
 169          <m:mphantom><m:mtext>__</m:mtext></m:mphantom>
 170          <xsl:apply-templates select="type/*[1]"/>
 171         </m:mrow>
 172        </m:mtd>
 173       </m:mtr>
 174       <m:mtr>
 175        <m:mtd>
 176         <m:mrow>
 177          <m:mtext>CONJECTURES:</m:mtext>
 178         </m:mrow>
 179        </m:mtd>
 180       </m:mtr>
 181       <xsl:for-each select="Conjecture">
 182       <m:mtr>
 183        <m:mtd>
 184         <m:mrow>
 185          <m:mphantom><m:mtext>__</m:mtext></m:mphantom>
 186          <m:mtext><xsl:value-of select="./@no"/>:</m:mtext>
 187          <xsl:apply-templates select="./*[1]"/>
 188         </m:mrow>
 189        </m:mtd>
 190       </m:mtr>
 191       </xsl:for-each>
 192       <m:mtr>
 193        <m:mtd>
 194         <m:mrow>
 195          <m:mtext>CORRESPONDING PROOF:</m:mtext>
 196         </m:mrow>
 197        </m:mtd>
 198       </m:mtr>
 199       <m:mtr>
 200        <m:mtd>
 201         <m:mrow>
 202          <m:mphantom><m:mtext>__</m:mtext></m:mphantom>
 203          <xsl:apply-templates select="body/*[1]"/>
 204         </m:mrow>
 205        </m:mtd>
 206       </m:mtr>
 207      </m:mtable>
 208     </m:math>
 209 </xsl:template>
 210
 211 <!-- MUTUAL INDUCTIVE DEFINITION -->
 212
 213 <xsl:template match="InductiveDefinition">
 214     <m:math>
 215      <m:mtable align="baseline 1" equalrows="false" columnalign="left" helm:xref="{@helm:xref}">
 216      <xsl:for-each select="InductiveType">
 217       <m:mtr>
 218        <m:mtd>
 219         <m:mrow>
 220          <xsl:choose>
 221          <xsl:when test="position() = 1">
 222           <xsl:choose>
 223           <xsl:when test="string(./@inductive) = &quot;true&quot;">
 224            <m:mtext>INDUCTIVE DEFINITION</m:mtext>
 225           </xsl:when>
 226           <xsl:otherwise>
 227            <m:mtext>COINDUCTIVE DEFINITION</m:mtext>
 228           </xsl:otherwise>
 229           </xsl:choose>
 230          </xsl:when>
 231          <xsl:otherwise>
 232           <m:mtext>AND</m:mtext>
 233          </xsl:otherwise>
 234          </xsl:choose>
 235          <m:mphantom><m:mtext>_</m:mtext></m:mphantom>
 236          <m:mtext><xsl:value-of select="./@name"/>(<xsl:if test="string(../Params) != &quot;&quot;"><xsl:value-of select="../Params"/></xsl:if>)</m:mtext>
 237         </m:mrow>
 238        </m:mtd>
 239       </m:mtr>
 240       <m:mtr>
 241        <m:mtd>
 242         <m:mrow>
 243          <m:mphantom><m:mtext>__</m:mtext></m:mphantom>
 244          <m:mtext>[</m:mtext>
 245          <xsl:choose>
 246          <xsl:when test="string(../Param) != &quot;&quot;">
 247           <m:mtable align="baseline 1" equalrows="false" columnalign="left">
 248            <xsl:for-each select="../Param">
 249             <m:mtr>
 250              <m:mtd>
 251               <m:mrow>
 252                <m:mi><xsl:value-of select="./@name"/></m:mi>
 253                <m:mo>:</m:mo>
 254                <xsl:apply-templates select="*"/>
 255               </m:mrow>
 256              </m:mtd>
 257             </m:mtr>
 258            </xsl:for-each>
 259             <m:mtr>
 260              <m:mtd>
 261               <m:mrow>
 262                <m:mtext>]</m:mtext>
 263               </m:mrow>
 264              </m:mtd>
 265             </m:mtr>
 266           </m:mtable>
 267          </xsl:when>
 268          <xsl:otherwise>
 269           <m:mtext>]</m:mtext>
 270          </xsl:otherwise>
 271          </xsl:choose>
 272         </m:mrow>
 273        </m:mtd>
 274       </m:mtr>
 275       <m:mtr>
 276        <m:mtd>
 277         <m:mrow>
 278          <m:mtext>OF ARITY</m:mtext>
 279         </m:mrow>
 280        </m:mtd>
 281       </m:mtr>
 282       <m:mtr>
 283        <m:mtd>
 284         <m:mrow>
 285          <m:mphantom><m:mtext>__</m:mtext></m:mphantom>
 286          <xsl:apply-templates select="./arity/*[1]"/>
 287         </m:mrow>
 288        </m:mtd>
 289       </m:mtr>
 290       <m:mtr>
 291        <m:mtd>
 292         <m:mrow>
 293          <m:mtext>BUILT FROM</m:mtext>
 294         </m:mrow>
 295        </m:mtd>
 296       </m:mtr>
 297       <xsl:for-each select="./Constructor">
 298       <m:mtr>
 299        <m:mtd>
 300         <m:mrow>
 301          <xsl:choose>
 302          <xsl:when test="position() = 1">
 303           <m:mphantom><m:mtext>__</m:mtext></m:mphantom>
 304          </xsl:when>
 305          <xsl:otherwise>
 306           <m:mtext>|</m:mtext>
 307           <m:mphantom><m:mtext>_</m:mtext></m:mphantom>
 308          </xsl:otherwise>
 309          </xsl:choose>
 310          <m:mtext><xsl:value-of select="./@name"/> OF</m:mtext>
 311          <m:mphantom><m:mtext>_</m:mtext></m:mphantom>
 312          <xsl:apply-templates select="./*[1]"/>
 313         </m:mrow>
 314        </m:mtd>
 315       </m:mtr>
 316       </xsl:for-each>
 317      </xsl:for-each>
 318      </m:mtable>
 319     </m:math>
 320 </xsl:template>
 321
 322 <!-- VARIABLE -->
 323
 324 <xsl:template match="Variable">
 325     <m:math>
 326      <m:mtable align="baseline 1" equalrows="false" columnalign="left" helm:xref="{@helm:xref}">
 327       <m:mtr>
 328        <m:mtd>
 329         <m:mrow>
 330          <m:mtext>VARIABLE <xsl:value-of select="@name"/> OF TYPE</m:mtext>
 331         </m:mrow>
 332        </m:mtd>
 333       </m:mtr>
 334       <m:mtr>
 335        <m:mtd>
 336         <m:mrow>
 337          <m:mphantom><m:mtext>__</m:mtext></m:mphantom>
 338          <xsl:apply-templates select="type/*[1]"/>
 339         </m:mrow>
 340        </m:mtd>
 341       </m:mtr>
 342       <xsl:if test="name(*[1])='body'">
 343        <m:mtr>
 344         <m:mtd>
 345          <m:mrow>
 346           <m:mtext>AS</m:mtext>
 347          </m:mrow>
 348         </m:mtd>
 349        </m:mtr>
 350        <m:mtr>
 351         <m:mtd>
 352          <m:mrow>
 353           <m:mphantom><m:mtext>__</m:mtext></m:mphantom>
 354           <xsl:apply-templates select="body/*[1]"/>
 355          </m:mrow>
 356         </m:mtd>
 357        </m:mtr>
 358       </xsl:if>
 359      </m:mtable>
 360     </m:math>
 361 </xsl:template>
 362
 363 <!--**********************-->
 364 <!--        TERMS         -->
 365 <!--**********************-->
 366
 367 <xsl:template match="m:bvar">
 368  <xsl:choose>
 369   <xsl:when test="m:type">
 370    <xsl:variable name="charlength">
 371     <xsl:apply-templates select="m:ci" mode="charcount"/>
 372    </xsl:variable>
 373    <xsl:choose>
 374     <xsl:when test="$charlength >= $framewidth">
 375      <m:mtable align="baseline 1" equalrows="false" columnalign="left">
 376       <m:mtr>
 377        <m:mtd>
 378         <m:mrow>
 379          <xsl:apply-templates select="m:ci"/>
 380          <m:mo>:</m:mo>
 381         </m:mrow>
 382        </m:mtd>
 383       </m:mtr>
 384       <m:mtr>
 385        <m:mtd>
 386         <m:mrow>
 387          <xsl:apply-templates select="m:type"/>
 388         </m:mrow>
 389        </m:mtd>
 390       </m:mtr>
 391      </m:mtable>
 392     </xsl:when>
 393     <xsl:otherwise>
 394      <m:mrow>
 395       <xsl:apply-templates select="m:ci"/>
 396       <m:mo>:</m:mo>
 397       <xsl:apply-templates select="m:type"/>
 398      </m:mrow>
 399     </xsl:otherwise>
 400    </xsl:choose>
 401   </xsl:when>
 402   <xsl:otherwise>
 403    <xsl:apply-templates select="m:ci"/>
 404   </xsl:otherwise>
 405  </xsl:choose>
 406 </xsl:template>
 407
 408
 409 <!-- CSYMBOL -->
 410
 411 <xsl:template match="m:apply[m:csymbol]">
 412 <xsl:param name="nopar" select="0"/>
 413     <xsl:variable name="name"><xsl:value-of select="m:csymbol"/></xsl:variable>
 414     <xsl:variable name="charlength"><xsl:apply-templates select="m:csymbol" mode="charcount"/></xsl:variable>
 415     <m:mrow>
 416      <xsl:if test="@id">
 417       <xsl:attribute name="xref"><xsl:value-of select="@id"/></xsl:attribute>
 418      </xsl:if>
 419      <xsl:variable name="id" select="m:csymbol/@id"/>
 420      <xsl:choose>
 421       <!-- FORALL -->
 422       <xsl:when test="$name='forall'">
 423        <xsl:choose>
 424        <xsl:when test="$charlength >= $framewidth">
 425         <m:mtable align="baseline 1" equalrows="false" columnalign="left">
 426          <m:mtr>
 427           <m:mtd>
 428            <m:mrow>
 429             <m:mo mathcolor="Blue">&#8704;</m:mo>
 430             <xsl:apply-templates select="m:bvar"/>
 431            </m:mrow>
 432           </m:mtd>
 433          </m:mtr>
 434          <m:mtr>
 435           <m:mtd>
 436            <m:mrow>
 437             <m:mo>.</m:mo>
 438             <xsl:apply-templates select="*[position()=3]"/>
 439            </m:mrow>
 440           </m:mtd>
 441          </m:mtr>
 442         </m:mtable>
 443        </xsl:when>
 444        <xsl:otherwise>
 445         <m:mo mathcolor="Blue">&#8704;</m:mo>
 446         <xsl:apply-templates select="m:bvar/m:ci"/>
 447         <m:mo>:</m:mo>
 448         <xsl:apply-templates select="m:bvar/m:type"/>
 449         <m:mo>.</m:mo>
 450         <xsl:apply-templates select="*[position()=3]"/>
 451        </xsl:otherwise>
 452        </xsl:choose>
 453       </xsl:when>
 454       <!-- LET-IN -->
 455       <xsl:when test="$name='let_in'">
 456        <xsl:choose>
 457        <xsl:when test="$charlength >= $framewidth">
 458         <m:mtable align="baseline 1" equalrows="false" columnalign="left">
 459          <m:mtr>
 460           <m:mtd>
 461            <m:mrow>
 462             <m:mo>LET</m:mo>
 463             <m:mphantom><m:mtext>_</m:mtext></m:mphantom>
 464             <xsl:apply-templates select="m:bvar"/>
 465            </m:mrow>
 466           </m:mtd>
 467          </m:mtr>
 468          <m:mtr>
 469           <m:mtd>
 470            <m:mrow>
 471             <m:mo>=</m:mo>
 472             <xsl:apply-templates select="*[position()=3]"/>
 473            </m:mrow>
 474           </m:mtd>
 475          </m:mtr>
 476          <m:mtr>
 477           <m:mtd>
 478            <m:mrow>
 479             <m:mo>IN</m:mo>
 480             <m:mphantom><m:mtext>_</m:mtext></m:mphantom>
 481             <xsl:apply-templates select="*[position()=4]"/>
 482            </m:mrow>
 483           </m:mtd>
 484          </m:mtr>
 485         </m:mtable>
 486        </xsl:when>
 487        <xsl:otherwise>
 488         <m:mo>LET</m:mo>
 489         <m:mphantom><m:mtext>_</m:mtext></m:mphantom>
 490         <xsl:apply-templates select="m:bvar/m:ci"/>
 491         <m:mo>=</m:mo>
 492         <xsl:apply-templates select="*[position()=3]"/>
 493         <m:mphantom><m:mtext>_</m:mtext></m:mphantom>
 494         <m:mtext>IN</m:mtext>
 495         <m:mphantom><m:mtext>_</m:mtext></m:mphantom>
 496         <xsl:apply-templates select="*[position()=4]"/>
 497        </xsl:otherwise>
 498        </xsl:choose>
 499       </xsl:when>
 500       <!-- PROD -->
 501       <xsl:when test="$name='prod'">
 502        <xsl:choose>
 503        <xsl:when test="$charlength >= $framewidth">
 504         <m:mtable align="baseline 1" equalrows="false" columnalign="left">
 505          <m:mtr>
 506           <m:mtd>
 507            <m:mrow>
 508             <m:mo mathcolor="Blue">&#x03a0;</m:mo>
 509             <xsl:apply-templates select="m:bvar"/>
 510            </m:mrow>
 511           </m:mtd>
 512          </m:mtr>
 513          <m:mtr>
 514           <m:mtd>
 515            <m:mrow>
 516             <m:mo>.</m:mo>
 517             <xsl:apply-templates select="*[position()=3]"/>
 518            </m:mrow>
 519           </m:mtd>
 520          </m:mtr>
 521         </m:mtable>
 522        </xsl:when>
 523        <xsl:otherwise>
 524         <m:mo mathcolor="Blue">&#x03a0;</m:mo>
 525         <xsl:apply-templates select="m:bvar/m:ci"/>
 526         <m:mo>:</m:mo>
 527         <xsl:apply-templates select="m:bvar/m:type"/>
 528         <m:mo>.</m:mo>
 529         <xsl:apply-templates select="*[position()=3]"/>
 530        </xsl:otherwise>
 531        </xsl:choose>
 532       </xsl:when>
 533       <!-- ARROW -->
 534       <xsl:when test="$name='arrow'">
 535        <xsl:choose>
 536        <xsl:when test="$charlength >= $framewidth">
 537         <m:mtable align="baseline 1" equalrows="false" columnalign="left">
 538          <m:mtr>
 539           <m:mtd>
 540            <m:mrow>
 541             <xsl:if test="$nopar=0">
 542              <m:mo stretchy="false">(</m:mo>
 543             </xsl:if>
 544             <xsl:apply-templates select="*[position()=2]"/>
 545            </m:mrow>
 546           </m:mtd>
 547          </m:mtr>
 548          <m:mtr>
 549           <m:mtd>
 550            <m:mrow>
 551             <m:mo mathmathcolor="Blue">&#x2192;</m:mo>
 552             <xsl:choose>
 553             <xsl:when test="*[position()=3]/m:csymbol">
 554              <xsl:variable name="nextp"><xsl:value-of select="*[position()=3]/m:csymbol"/></xsl:variable>
 555              <xsl:choose>
 556              <xsl:when test="$nextp='arrow'">
 557               <xsl:apply-templates select="*[position()=3]"><xsl:with-param name="nopar" select="1"/></xsl:apply-templates>
 558              </xsl:when>
 559              <xsl:otherwise>
 560               <xsl:apply-templates select="*[position()=3]"/>
 561              </xsl:otherwise>
 562              </xsl:choose>
 563             </xsl:when>
 564             <xsl:otherwise>
 565              <xsl:apply-templates select="*[position()=3]"/>
 566             </xsl:otherwise>
 567             </xsl:choose>
 568            </m:mrow>
 569           </m:mtd>
 570          </m:mtr>
 571          <xsl:if test="$nopar=0">
 572          <m:mtr>
 573           <m:mtd>
 574            <m:mrow>
 575             <m:mo stretchy="false">)</m:mo>
 576            </m:mrow>
 577           </m:mtd>
 578          </m:mtr>
 579          </xsl:if>
 580         </m:mtable>
 581        </xsl:when>
 582        <xsl:otherwise>
 583         <xsl:if test="$nopar=0">
 584          <m:mo stretchy="false">(</m:mo>
 585         </xsl:if>
 586         <xsl:apply-templates select="*[position()=2]"/>
 587         <m:mo mathcolor="Blue">&#x2192;</m:mo>
 588         <xsl:choose>
 589         <xsl:when test="*[position()=3]/m:csymbol">
 590          <xsl:variable name="nextp"><xsl:value-of select="*[position()=3]/m:csymbol"/></xsl:variable>
 591          <xsl:choose>
 592          <xsl:when test="$nextp='arrow'">
 593           <xsl:apply-templates select="*[position()=3]"><xsl:with-param name="nopar" select="1"/></xsl:apply-templates>
 594          </xsl:when>
 595          <xsl:otherwise>
 596           <xsl:apply-templates select="*[position()=3]"/>
 597          </xsl:otherwise>
 598          </xsl:choose>
 599         </xsl:when>
 600         <xsl:otherwise>
 601          <xsl:apply-templates select="*[position()=3]"/>
 602         </xsl:otherwise>
 603         </xsl:choose>
 604         <xsl:if test="$nopar=0">
 605          <m:mo stretchy="false">)</m:mo>
 606         </xsl:if>
 607        </xsl:otherwise>
 608        </xsl:choose>
 609       </xsl:when>
 610       <!-- APP -->
 611       <xsl:when test="$name='app'">
 612        <xsl:choose>
 613        <xsl:when test="$charlength >= $framewidth">
 614         <m:mtable align="baseline 1" equalrows="false" columnalign="left">
 615          <m:mtr>
 616           <m:mtd>
 617            <m:mrow>
 618             <m:mo stretchy="false">(</m:mo>
 619 <!-- added precedence to app = FUNCTION_PREC (99) -->
 620             <xsl:apply-templates select="*[position()=2]">
 621              <xsl:with-param name="IN_PREC" select="$FUNCTION_PREC"/>
 622             </xsl:apply-templates>
 623            </m:mrow>
 624           </m:mtd>
 625          </m:mtr>
 626          <xsl:for-each select="*[position()>2]">
 627          <m:mtr>
 628           <m:mtd>
 629            <m:mrow>
 630             <m:mphantom><m:mtext>(</m:mtext></m:mphantom>
 631 <!-- added precedence to app = FUNCTION_PREC (99) -->
 632             <xsl:apply-templates select=".">
 633              <xsl:with-param name="IN_PREC" select="$FUNCTION_PREC"/>
 634             </xsl:apply-templates>
 635            </m:mrow>
 636           </m:mtd>
 637          </m:mtr>
 638          </xsl:for-each>
 639          <m:mtr>
 640           <m:mtd>
 641            <m:mrow>
 642             <m:mo stretchy="false">)</m:mo>
 643            </m:mrow>
 644           </m:mtd>
 645          </m:mtr>
 646         </m:mtable>
 647        </xsl:when>
 648        <xsl:otherwise>
 649         <m:mo stretchy="false">(</m:mo>
 650 <!-- added precedence to app = FUNCTION_PREC (99) -->
 651         <xsl:apply-templates select="*[position()=2]">
 652          <xsl:with-param name="IN_PREC" select="$FUNCTION_PREC"/>
 653         </xsl:apply-templates>
 654         <xsl:for-each select="*[position()>2]">
 655          <m:mphantom><m:mtext>_</m:mtext></m:mphantom>
 656 <!-- added precedence to app = FUNCTION_PREC (99) -->
 657          <xsl:apply-templates select=".">
 658           <xsl:with-param name="IN_PREC" select="$FUNCTION_PREC"/>
 659          </xsl:apply-templates>
 660         </xsl:for-each>
 661         <m:mo stretchy="false">)</m:mo>
 662        </xsl:otherwise>
 663        </xsl:choose>
 664       </xsl:when>
 665       <!-- CAST -->
 666       <xsl:when test="$name='cast'">
 667        <xsl:choose>
 668        <xsl:when test="$charlength >= $framewidth">
 669         <m:mtable align="baseline 1" equalrows="false" columnalign="left">
 670          <m:mtr>
 671           <m:mtd>
 672            <m:mrow>
 673             <m:mo stretchy="false">(</m:mo>
 674             <xsl:apply-templates select="*[position()=2]"/>
 675            </m:mrow>
 676           </m:mtd>
 677          </m:mtr>
 678          <m:mtr>
 679           <m:mtd>
 680            <m:mrow>
 681             <m:mo mathcolor="Maroon">:></m:mo>
 682             <xsl:apply-templates select="*[position()=3]"/>
 683            </m:mrow>
 684           </m:mtd>
 685          </m:mtr>
 686          <m:mtr>
 687           <m:mtd>
 688            <m:mrow>
 689             <m:mo stretchy="false">)</m:mo>
 690            </m:mrow>
 691           </m:mtd>
 692          </m:mtr>
 693         </m:mtable>
 694        </xsl:when>
 695        <xsl:otherwise>
 696         <m:mo stretchy="false">(</m:mo>
 697         <xsl:apply-templates select="*[position()=2]"/>
 698         <m:mo mathcolor="Maroon">:></m:mo>
 699         <xsl:apply-templates select="*[position()=3]"/>
 700         <m:mo stretchy="false">)</m:mo>
 701        </xsl:otherwise>
 702        </xsl:choose>
 703       </xsl:when>
 704       <!-- PROP -->
 705       <xsl:when test="$name='Prop'">
 706        <m:mo>Prop</m:mo>
 707       </xsl:when>
 708       <!-- SET -->
 709       <xsl:when test="$name='Set'">
 710        <m:mo>Set</m:mo>
 711       </xsl:when>
 712       <!-- TYPE -->
 713       <xsl:when test="$name='Type'">
 714        <m:mo>Type</m:mo>
 715       </xsl:when>
 716       <!-- MUTCASE -->
 717       <xsl:when test="$name='mutcase'">
 718        <xsl:choose>
 719        <xsl:when test="$charlength >= $framewidth">
 720         <xsl:variable name="charlength"><xsl:apply-templates select="*[position()=2]" mode="charcount"><xsl:with-param name="nosibling" select="1"/></xsl:apply-templates></xsl:variable>
 721         <m:mtable align="baseline 1" equalrows="false" columnalign="left">
 722          <m:mtr>
 723           <m:mtd>
 724            <m:mrow>
 725             <m:mo>&lt;</m:mo>
 726             <xsl:apply-templates select="*[position()=2]"/>
 727             <xsl:if test="$framewidth > $charlength">
 728              <m:mo>&gt;</m:mo>
 729              <m:mo>CASES</m:mo>
 730              <m:mphantom><m:mtext>_</m:mtext></m:mphantom>
 731              <xsl:apply-templates select="*[position()=3]"/>
 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:mo>&gt;</m:mo>
 741             <m:mo>CASES</m:mo>
 742             <m:mphantom><m:mtext>_</m:mtext></m:mphantom>
 743             <xsl:apply-templates select="*[position()=3]"/>
 744            </m:mrow>
 745           </m:mtd>
 746          </m:mtr>
 747          </xsl:if>
 748          <m:mtr>
 749           <m:mtd>
 750            <m:mrow>
 751             <m:mo>OF</m:mo>
 752            </m:mrow>
 753           </m:mtd>
 754          </m:mtr>
 755          <xsl:for-each select="piecewise/piece">
 756          <xsl:variable name="charlength"><xsl:apply-templates select="./*[2]" mode="charcount"><xsl:with-param name="nosibling" select="1"/></xsl:apply-templates></xsl:variable>
 757          <m:mtr>
 758           <m:mtd>
 759            <m:mrow>
 760             <xsl:choose>
 761             <xsl:when test="position() = 1">
 762               <m:mphantom><m:mtext>|</m:mtext></m:mphantom>
 763             </xsl:when>
 764             <xsl:otherwise>
 765              <m:mo stretchy="false">|</m:mo>
 766             </xsl:otherwise>
 767             </xsl:choose>
 768             <m:mphantom><m:mtext>_</m:mtext></m:mphantom>
 769             <xsl:apply-templates select="./*[2]"/>
 770             <xsl:if test="$framewidth > $charlength">
 771              <m:mo mathcolor="Green">&#x21d2;</m:mo>
 772              <xsl:apply-templates select="./*[1]"/>
 773             </xsl:if>
 774            </m:mrow>
 775           </m:mtd>
 776          </m:mtr>
 777          <xsl:if test="$charlength >= $framewidth">
 778          <m:mtr>
 779           <m:mtd>
 780            <m:mrow>
 781             <m:mphantom><m:mtext>|_</m:mtext></m:mphantom>
 782             <m:mo mathcolor="Green">&#x21d2;</m:mo>
 783             <xsl:apply-templates select="./*[1]"/>
 784            </m:mrow>
 785           </m:mtd>
 786          </m:mtr>
 787          </xsl:if>
 788         </xsl:for-each>
 789          <m:mtr>
 790           <m:mtd>
 791            <m:mrow>
 792             <m:mo>END</m:mo>
 793            </m:mrow>
 794           </m:mtd>
 795          </m:mtr>
 796         </m:mtable>
 797        </xsl:when>
 798        <xsl:otherwise>
 799         <m:mo>&lt;</m:mo><xsl:apply-templates select="*[position()=2]"/><m:mo>&gt;</m:mo>
 800         <m:mo>CASES</m:mo>
 801         <m:mphantom><m:mtext>_</m:mtext></m:mphantom>
 802         <xsl:apply-templates select="*[position()=3]"/>
 803         <m:mphantom><m:mtext>_</m:mtext></m:mphantom>
 804         <m:mo>OF</m:mo>
 805         <xsl:for-each select="piecewise/piece">
 806          <xsl:choose>
 807          <xsl:when test="position() != 1">
 808           <m:mo stretchy="false">|</m:mo>
 809          </xsl:when>
 810          </xsl:choose>
 811          <xsl:apply-templates select="./*[2]"/>
 812          <m:mo mathcolor="Green">&#x21d2;</m:mo>
 813          <xsl:apply-templates select="./*[1]"/>
 814         </xsl:for-each>
 815         <m:mphantom><m:mtext>_</m:mtext></m:mphantom>
 816         <m:mo>END</m:mo>
 817        </xsl:otherwise>
 818        </xsl:choose>
 819       </xsl:when>
 820       <!-- FIX -->
 821       <xsl:when test="$name='fix'">
 822        <xsl:choose>
 823        <xsl:when test="$charlength >= $framewidth">
 824         <m:mtable align="baseline 1" equalrows="false" columnalign="left">
 825          <m:mtr>
 826           <m:mtd>
 827            <m:mrow>
 828             <m:mo>FIX</m:mo>
 829             <m:mphantom><m:mtext>_</m:mtext></m:mphantom>
 830             <m:mi><xsl:value-of select="m:ci"/></m:mi>
 831             <m:mo stretchy="false">{</m:mo>
 832            </m:mrow>
 833           </m:mtd>
 834          </m:mtr>
 835          <m:mtr>
 836           <m:mtd>
 837            <m:mrow>
 838             <m:mphantom><m:mtext>__</m:mtext></m:mphantom>
 839             <m:mtable align="baseline 1" equalrows="false" columnalign="left">
 840             <xsl:for-each select="m:bvar">
 841              <xsl:variable name="charlength"><xsl:apply-templates select="m:type" mode="charcount"><xsl:with-param name="nosibling" select="1"/></xsl:apply-templates></xsl:variable>
 842              <m:mtr>
 843               <m:mtd>
 844                <m:mrow>
 845                 <m:mi><xsl:value-of select="m:ci"/></m:mi>
 846                 <m:mo>:</m:mo>
 847                 <xsl:if test="$framewidth > $charlength">
 848                  <xsl:apply-templates select="m:type"/>
 849                 </xsl:if>
 850                </m:mrow>
 851               </m:mtd>
 852              </m:mtr>
 853              <xsl:if test="$charlength >= $framewidth">
 854              <m:mtr>
 855               <m:mtd>
 856                <m:mrow>
 857                 <m:mphantom><m:mtext>:=</m:mtext></m:mphantom>
 858                 <xsl:apply-templates select="m:type"/>
 859                </m:mrow>
 860               </m:mtd>
 861              </m:mtr>
 862              </xsl:if>
 863              <m:mtr>
 864               <m:mtd>
 865                <m:mrow>
 866                 <m:mo>:=</m:mo>
 867                 <xsl:apply-templates select="following-sibling::*[position()=1]"/>
 868                </m:mrow>
 869               </m:mtd>
 870              </m:mtr>
 871             </xsl:for-each>
 872             </m:mtable>
 873            </m:mrow>
 874           </m:mtd>
 875          </m:mtr>
 876          <m:mtr>
 877           <m:mtd>
 878            <m:mrow>
 879             <m:mo stretchy="false">}</m:mo>
 880            </m:mrow>
 881           </m:mtd>
 882          </m:mtr>
 883         </m:mtable>
 884        </xsl:when>
 885        <xsl:otherwise>
 886         <m:mo>FIX</m:mo>
 887         <m:mi><xsl:value-of select="m:ci"/></m:mi>
 888         <m:mo stretchy="false">{</m:mo>
 889         <m:mtable align="baseline 1" equalrows="false" columnalign="left">
 890         <xsl:for-each select="m:bvar">
 891          <m:mtr>
 892           <m:mtd>
 893            <m:mrow>
 894             <m:mi><xsl:value-of select="m:ci"/></m:mi>
 895             <m:mo>:</m:mo>
 896             <xsl:apply-templates select="m:type"/>
 897             <m:mo>:=</m:mo>
 898             <xsl:apply-templates select="following-sibling::*[position() = 1]"/>
 899             <xsl:if test="position()=last()">
 900              <m:mo stretchy="false">}</m:mo>
 901             </xsl:if>
 902            </m:mrow>
 903           </m:mtd>
 904          </m:mtr>
 905          </xsl:for-each>
 906         </m:mtable>
 907        </xsl:otherwise>
 908        </xsl:choose>
 909       </xsl:when>
 910       <!-- COFIX -->
 911       <xsl:when test="$name='cofix'">
 912        <xsl:choose>
 913        <xsl:when test="$charlength >= $framewidth">
 914         <m:mtable align="baseline 1" equalrows="false" columnalign="left">
 915          <m:mtr>
 916           <m:mtd>
 917            <m:mrow>
 918             <m:mo>COFIX</m:mo>
 919             <m:mphantom><m:mtext>_</m:mtext></m:mphantom>
 920             <m:mi><xsl:value-of select="m:ci"/></m:mi>
 921             <m:mo stretchy="false">{</m:mo>
 922            </m:mrow>
 923           </m:mtd>
 924          </m:mtr>
 925          <m:mtr>
 926           <m:mtd>
 927            <m:mrow>
 928             <m:mphantom><m:mtext>__</m:mtext></m:mphantom>
 929             <m:mtable align="baseline 1" equalrows="false" columnalign="left">
 930             <xsl:for-each select="m:bvar">
 931              <xsl:variable name="charlength"><xsl:apply-templates select="m:type" mode="charcount"><xsl:with-param name="nosibling" select="1"/></xsl:apply-templates></xsl:variable>
 932              <m:mtr>
 933               <m:mtd>
 934                <m:mrow>
 935                 <m:mi><xsl:value-of select="m:ci"/></m:mi>
 936                 <m:mo>:</m:mo>
 937                 <xsl:if test="$framewidth > $charlength">
 938                  <xsl:apply-templates select="m:type"/>
 939                 </xsl:if>
 940                </m:mrow>
 941               </m:mtd>
 942              </m:mtr>
 943              <xsl:if test="$charlength >= $framewidth">
 944              <m:mtr>
 945               <m:mtd>
 946                <m:mrow>
 947                 <m:mphantom><m:mtext>:=</m:mtext></m:mphantom>
 948                 <xsl:apply-templates select="m:type"/>
 949                </m:mrow>
 950               </m:mtd>
 951              </m:mtr>
 952              </xsl:if>
 953              <m:mtr>
 954               <m:mtd>
 955                <m:mrow>
 956                 <m:mo>:=</m:mo>
 957                 <xsl:apply-templates select="following-sibling::*[position() = 1]"/>
 958                </m:mrow>
 959               </m:mtd>
 960              </m:mtr>
 961             </xsl:for-each>
 962             </m:mtable>
 963            </m:mrow>
 964           </m:mtd>
 965          </m:mtr>
 966          <m:mtr>
 967           <m:mtd>
 968            <m:mrow>
 969             <m:mo stretchy="false">}</m:mo>
 970            </m:mrow>
 971           </m:mtd>
 972          </m:mtr>
 973         </m:mtable>
 974        </xsl:when>
 975        <xsl:otherwise>
 976         <m:mo>COFIX</m:mo>
 977         <m:mi><xsl:value-of select="m:ci"/></m:mi>
 978         <m:mo stretchy="false">{</m:mo>
 979         <m:mtable align="baseline 1" equalrows="false" columnalign="left">
 980         <xsl:for-each select="m:bvar">
 981          <m:mtr>
 982           <m:mtd>
 983            <m:mrow>
 984             <m:mi><xsl:value-of select="m:ci"/></m:mi>
 985             <m:mo>:</m:mo>
 986             <xsl:apply-templates select="m:type"/>
 987             <m:mo>:=</m:mo>
 988             <xsl:apply-templates select="following-sibling::*[position() = 1]"/>
 989             <xsl:if test="position()=last()">
 990              <m:mo stretchy="false">}</m:mo>
 991             </xsl:if>
 992            </m:mrow>
 993           </m:mtd>
 994          </m:mtr>
 995          </xsl:for-each>
 996         </m:mtable>
 997        </xsl:otherwise>
 998        </xsl:choose>
 999       </xsl:when>
1000       <!-- ***************************************** -->
1001       <!-- *********** PROOF ELEMENTS ************** -->
1002       <!-- ***************************************** -->
1003       <!-- PROOF -->
1004       <xsl:when test="$name='proof'">
1005         <!-- CSC: $explodeall until the annotationHelper can handle mactions -->
1006         <xsl:variable name="test" select="(not($explodeall)) and
1007            (not(preceding-sibling::*[1]/text()='letin1')) and
1008            (not(preceding-sibling::*[1]/text()='rw_step')) and
1009            (not(name(..)='m:lambda'))"/>
1010         <xsl:variable name="hidden_details">
1011          <xsl:if test="$test">
1012           <!-- Details hided (default) -->
1013           <m:mtable align="baseline 1" equalrows="false" columnalign="left">
1014            <m:mtr>
1015             <m:mtd>
1016              <m:mrow>
1017               <m:mtext mathcolor="Red">We&#x00a0;can&#x00a0;prove</m:mtext>
1018               <m:mphantom><m:mtext>_</m:mtext></m:mphantom>
1019               <xsl:apply-templates select="*[position()=3]"/>
1020               <m:mrow>
1021                <m:mphantom><m:mtext>_</m:mtext></m:mphantom>
1022                <m:mtext mathcolor="Green">(explain)</m:mtext>
1023               </m:mrow>
1024              </m:mrow>
1025             </m:mtd>
1026            </m:mtr>
1027           </m:mtable>
1028          </xsl:if>
1029         </xsl:variable>
1030         <xsl:variable name="shown_details">
1031          <!-- Show details -->
1032          <m:mtable align="baseline 1" equalrows="false" columnalign="left">
1033           <m:mtr>
1034            <m:mtd>
1035             <m:mrow>
1036              <xsl:apply-templates select="*[position()=2]"/>
1037             </m:mrow>
1038            </m:mtd>
1039           </m:mtr>
1040           <m:mtr>
1041            <m:mtd>
1042             <m:mrow>
1043              <m:mtext mathcolor="Red">we&#x00a0;proved</m:mtext>
1044              <m:mphantom><m:mtext>_</m:mtext></m:mphantom>
1045              <xsl:apply-templates select="*[position()=3]"/>
1046              <m:mrow>
1047               <m:mphantom>
1048                <m:mtext>_</m:mtext>
1049               </m:mphantom>
1050               <xsl:if test="$test">
1051                <m:mtext mathcolor="Green">(hide&#x00a0;details)</m:mtext>
1052               </xsl:if>
1053              </m:mrow>
1054             </m:mrow>
1055            </m:mtd>
1056           </m:mtr>
1057          </m:mtable>
1058         </xsl:variable>
1059         <xsl:choose>
1060          <xsl:when test="$test">
1061           <m:maction actiontype="toggle">
1062            <xsl:copy-of select="$hidden_details"/>
1063            <xsl:copy-of select="$shown_details"/>
1064           </m:maction>
1065          </xsl:when>
1066          <xsl:otherwise>
1067           <xsl:copy-of select="$shown_details"/>
1068          </xsl:otherwise>
1069         </xsl:choose>
1070       </xsl:when>
1071       <!-- SIDE_PROOF -->
1072       <xsl:when test="$name='side_proof'">
1073         <xsl:variable name="test" select="(not($explodeall))"/>
1074         <xsl:variable name="hidden_details">
1075          <xsl:if test="$test">
1076           <!-- Details hided (default) -->
1077           <m:mtable align="baseline 1" equalrows="false" columnalign="left">
1078            <m:mtr>
1079             <m:mtd>
1080              <m:mrow>
1081               <m:mtext mathcolor="Red">We&#x00a0;can&#x00a0;prove</m:mtext>
1082               <m:mphantom><m:mtext>_</m:mtext></m:mphantom>
1083               <xsl:apply-templates select="*[position()=3]"/>
1084               <m:mrow>
1085                <m:mphantom><m:mtext>_</m:mtext></m:mphantom>
1086                <m:mtext mathcolor="Green">(explain)</m:mtext>
1087               </m:mrow>
1088              </m:mrow>
1089             </m:mtd>
1090            </m:mtr>
1091           </m:mtable>
1092          </xsl:if>
1093         </xsl:variable>
1094         <xsl:variable name="shown_details">
1095          <!-- Show details -->
1096          <m:mtable align="baseline 1" equalrows="false" columnalign="left">
1097           <m:mtr>
1098            <m:mtd>
1099             <m:mrow>
1100              <xsl:apply-templates select="*[position()=2]"/>
1101             </m:mrow>
1102            </m:mtd>
1103           </m:mtr>
1104           <m:mtr>
1105            <m:mtd>
1106             <m:mrow>
1107              <m:mtext mathcolor="Red">we&#x00a0;proved</m:mtext>
1108              <m:mphantom><m:mtext>_</m:mtext></m:mphantom>
1109              <xsl:apply-templates select="*[position()=3]"/>
1110              <m:mrow>
1111               <m:mphantom>
1112                <m:mtext>_</m:mtext>
1113               </m:mphantom>
1114               <xsl:if test="$test">
1115                <m:mtext mathcolor="Green">(hide&#x00a0;details)</m:mtext>
1116               </xsl:if>
1117              </m:mrow>
1118             </m:mrow>
1119            </m:mtd>
1120           </m:mtr>
1121          </m:mtable>
1122         </xsl:variable>
1123         <xsl:choose>
1124          <xsl:when test="$test">
1125           <m:maction actiontype="toggle">
1126            <xsl:copy-of select="$hidden_details"/>
1127            <xsl:copy-of select="$shown_details"/>
1128           </m:maction>
1129          </xsl:when>
1130          <xsl:otherwise>
1131           <xsl:copy-of select="$shown_details"/>
1132          </xsl:otherwise>
1133         </xsl:choose>
1134       </xsl:when>
1135       <!-- LETIN1 -->
1136       <xsl:when test="$name='letin1'">
1137         <m:mtable align="baseline 1" equalrows="false" columnalign="left">
1138          <m:mtr>
1139           <m:mtd>
1140            <m:mrow>
1141             <xsl:apply-templates select="*[position()=2]"/>
1142            </m:mrow>
1143           </m:mtd>
1144          </m:mtr>
1145          <m:mtr>
1146           <m:mtd>
1147            <m:mrow>
1148             <xsl:apply-templates select="*[position()=3]"/>
1149            </m:mrow>
1150           </m:mtd>
1151          </m:mtr>
1152         </m:mtable>
1153       </xsl:when>
1154       <xsl:when test="$name='by_induction'">
1155        <m:mtable align="baseline 1" equalrows="false" columnalign="left">
1156         <m:mtr>
1157          <m:mtd>
1158           <m:mrow>
1159            <m:mtext mathcolor="Red">We&#x00a0;prove</m:mtext>
1160            <m:mphantom><m:mtext>_</m:mtext></m:mphantom>
1161            <xsl:apply-templates select="../*[3]"/>
1162           </m:mrow>
1163          </m:mtd>
1164         </m:mtr>
1165         <m:mtr>
1166          <m:mtd>
1167           <m:mrow>
1168            <m:mtext mathcolor="Red">by&#x00a0;induction&#x00a0;on</m:mtext>
1169            <m:mphantom><m:mtext>_</m:mtext></m:mphantom>
1170            <xsl:apply-templates
1171             select="*[position()=last()]/*[position()=last()]"/>
1172           </m:mrow>
1173          </m:mtd>
1174         </m:mtr>
1175         <m:mtr>
1176          <m:mtd>
1177           <m:mrow>
1178            <m:mtable align="baseline 1" equalrows="false" columnalign="left">
1179             <xsl:for-each select="*[position()>3 and not(position()=last())]">
1180              <m:mtr>
1181               <m:mtd>
1182                <m:mrow>
1183                 <xsl:apply-templates select="."/>
1184                </m:mrow>
1185               </m:mtd>
1186              </m:mtr>
1187             </xsl:for-each>
1188            </m:mtable>
1189           </m:mrow>
1190          </m:mtd>
1191         </m:mtr>
1192        </m:mtable>
1193       </xsl:when>
1194       <!-- inductive_case -->
1195       <xsl:when test="$name='inductive_case'">
1196        <m:mtable align="baseline 1" equalrows="false" columnalign="left">
1197         <m:mtr>
1198          <m:mtd>
1199           <m:mrow>
1200            <m:mtext mathcolor="Red">Case</m:mtext>
1201            <m:mphantom><m:mtext>_</m:mtext></m:mphantom>
1202            <xsl:apply-templates select="*[2]"/>
1203           </m:mrow>
1204          </m:mtd>
1205         </m:mtr>
1206         <m:mtr>
1207          <m:mtd>
1208           <m:mrow>
1209            <m:mphantom><m:mtext>_</m:mtext></m:mphantom>
1210            <m:mtable align="baseline 1" equalrows="false" columnalign="left">
1211             <xsl:if test="*[3]/*[position()>1]">
1212              <m:mtr>
1213               <m:mtd>
1214                <m:mrow>
1215                 <m:mtext mathcolor="Red">By&#x00a0;induction&#x00a0;hypothesis,&#x00a0;we&#x00a0;have:</m:mtext>
1216                </m:mrow>
1217               </m:mtd>
1218              </m:mtr>
1219              <m:mtr>
1220               <m:mtd>
1221                <m:mrow>
1222                 <m:mphantom><m:mtext>_</m:mtext></m:mphantom>
1223                 <xsl:for-each select="*[3]/*[position()>1]">
1224                  <m:mo stretchy="false">(</m:mo>
1225                  <xsl:apply-templates select="m:ci"/>
1226                  <m:mo stretchy="false">) </m:mo>
1227                  <m:mphantom><m:mtext>_</m:mtext></m:mphantom>
1228                  <xsl:apply-templates select="m:type"/>
1229                 </xsl:for-each>
1230                </m:mrow>
1231               </m:mtd>
1232              </m:mtr>
1233             </xsl:if>
1234             <m:mtr>
1235              <m:mtd>
1236               <m:mrow>
1237                <xsl:apply-templates select="*[4]"/>
1238               </m:mrow>
1239              </m:mtd>
1240             </m:mtr>
1241            </m:mtable>
1242           </m:mrow>
1243          </m:mtd>
1244         </m:mtr>
1245        </m:mtable>
1246       </xsl:when>
1247       <!-- case_lhs  -->
1248       <xsl:when test="$name='case_lhs'">
1249        <m:mrow>
1250         <xsl:choose>
1251          <xsl:when test="count(*)=2">
1252           <xsl:apply-templates select="*[2]"/>
1253          </xsl:when>
1254          <xsl:otherwise>
1255           <m:mo stretchy="false">(</m:mo>
1256           <xsl:apply-templates select="*[2]"/>
1257           <xsl:for-each select="m:bvar">
1258            <m:mphantom><m:mtext>_</m:mtext></m:mphantom>
1259            <xsl:apply-templates select="*[1]"/>
1260            <m:mtext>:</m:mtext>
1261            <xsl:apply-templates select="m:type/*[1]"/>
1262           </xsl:for-each>
1263           <m:mo stretchy="false">)</m:mo>
1264          </xsl:otherwise>
1265         </xsl:choose>
1266        </m:mrow>
1267       </xsl:when>
1268       <!-- false_ind  -->
1269       <xsl:when test="$name='false_ind'">
1270        <m:mtable align="baseline 1" equalrows="false" columnalign="left">
1271         <m:mtr>
1272          <m:mtd>
1273           <m:mrow>
1274            <xsl:apply-templates select="*[3]"/>
1275           </m:mrow>
1276          </m:mtd>
1277         </m:mtr>
1278         <m:mtr>
1279          <m:mtd>
1280           <m:mrow>
1281            <m:mtext mathcolor="Red">Contradiction.</m:mtext>
1282           </m:mrow>
1283          </m:mtd>
1284         </m:mtr>
1285        </m:mtable>
1286       </xsl:when>
1287       <!-- LET-IN -->
1288       <xsl:when test="$name='letin'">
1289         <m:mtable align="baseline 1" equalrows="false" columnalign="left">
1290          <!-- <xsl:for-each select="APPLY[m:csymbol and (string(m:csymbol)='let')]"> -->
1291          <xsl:for-each select="*[(last() > position()) and (position()>1)]">
1292          <m:mtr>
1293           <m:mtd>
1294            <m:mrow>
1295             <xsl:apply-templates select="."/>
1296            </m:mrow>
1297           </m:mtd>
1298          </m:mtr>
1299          </xsl:for-each>
1300          <m:mtr>
1301           <m:mtd>
1302            <m:mrow>
1303             <xsl:apply-templates select="*[position()=last()]"/>
1304            </m:mrow>
1305           </m:mtd>
1306          </m:mtr>
1307         </m:mtable>
1308       </xsl:when>
1309       <!-- LET -->
1310       <xsl:when test="$name='let'">
1311        <m:mtext>(</m:mtext>
1312        <xsl:apply-templates select="m:ci"/>
1313        <m:mtext>) </m:mtext>
1314        <xsl:apply-templates select="*[3]"/>
1315       </xsl:when>
1316       <!-- RW_STEP -->
1317       <xsl:when test="$name='rw_step'">
1318         <m:mtable align="baseline 1" equalrows="false" columnalign="left">
1319          <m:mtr>
1320           <m:mtd>
1321            <m:mrow>
1322             <xsl:choose>
1323              <xsl:when test="name(*[2])='m:apply'">
1324               <xsl:apply-templates select="*[2]"/>
1325              </xsl:when>
1326              <xsl:otherwise>
1327               <m:mtext>Consider</m:mtext>
1328               <m:mphantom><m:mtext>_</m:mtext></m:mphantom>
1329               <xsl:apply-templates select="*[2]"/>
1330              </xsl:otherwise>
1331             </xsl:choose>
1332            </m:mrow>
1333           </m:mtd>
1334          </m:mtr>
1335          <m:mtr>
1336           <m:mtd>
1337            <m:mrow>
1338             <m:mtext>Rewrite</m:mtext>
1339             <m:mphantom><m:mtext>_</m:mtext></m:mphantom>
1340             <xsl:apply-templates select="*[3]"/>
1341             <m:mphantom><m:mtext>_</m:mtext></m:mphantom>
1342             <m:mtext>with</m:mtext>
1343             <m:mphantom><m:mtext>_</m:mtext></m:mphantom>
1344             <xsl:apply-templates select="*[4]"/>
1345             <m:mphantom><m:mtext>_</m:mtext></m:mphantom>
1346             <m:mtext>by</m:mtext>
1347             <m:mphantom><m:mtext>_</m:mtext></m:mphantom>
1348             <xsl:apply-templates select="*[5]"/>
1349            </m:mrow>
1350           </m:mtd>
1351          </m:mtr>
1352         </m:mtable>
1353       </xsl:when>
1354       <!-- not existing any more
1355       <xsl:when test="$name='thread'">
1356         <m:mtable align="baseline 1" equalrows="false" columnalign="left">
1357          <m:mtr>
1358           <m:mtd>
1359            <m:mrow>
1360             <xsl:choose>
1361              <xsl:when test="name(*[last()])='m:apply'">
1362               <xsl:apply-templates select="*[last()]"/>
1363              </xsl:when>
1364              <xsl:otherwise>
1365               <m:mtext>Consider</m:mtext>
1366               <m:mphantom><m:mtext>_</m:mtext></m:mphantom>
1367               <xsl:apply-templates select="*[last()]"/>
1368              </xsl:otherwise>
1369             </xsl:choose>
1370            </m:mrow>
1371           </m:mtd>
1372          </m:mtr>
1373          <xsl:apply-templates mode="thread" select="*[(last()-2)]"/>
1374         </m:mtable>
1375       </xsl:when>
1376       -->
1377       <!-- REWRITE_AND_APPLY -->
1378       <xsl:when test="$name='rewrite_and_apply'">
1379         <m:mtable align="baseline 1" equalrows="false" columnalign="left">
1380          <m:mtr>
1381           <m:mtd>
1382            <m:mrow>
1383             <xsl:apply-templates select="*[2]"/>
1384            </m:mrow>
1385           </m:mtd>
1386          </m:mtr>
1387          <m:mtr>
1388           <m:mtd>
1389            <m:mrow>
1390             <m:mtext>Then&#x00a0;apply&#x00a0;it&#x00a0;to</m:mtext>
1391             <m:mphantom><m:mtext>_</m:mtext></m:mphantom>
1392             <xsl:apply-templates select="*[position()>2]"/>
1393            </m:mrow>
1394           </m:mtd>
1395          </m:mtr>
1396        </m:mtable>
1397       </xsl:when>
1398       <!-- AND_IND -->
1399       <xsl:when test="$name='and_ind'">
1400         <m:mtable align="baseline 1" equalrows="false" columnalign="left">
1401          <m:mtr>
1402           <m:mtd>
1403            <m:mrow>
1404             <xsl:choose>
1405              <xsl:when test="name(*[2])='m:apply'">
1406               <xsl:apply-templates select="*[2]"/>
1407              </xsl:when>
1408              <xsl:otherwise>
1409               <m:mtext>Consider</m:mtext>
1410               <m:mphantom><m:mtext>_</m:mtext></m:mphantom>
1411               <xsl:apply-templates select="*[2]"/>
1412              </xsl:otherwise>
1413             </xsl:choose>
1414            </m:mrow>
1415           </m:mtd>
1416          </m:mtr>
1417          <m:mtr>
1418           <m:mtd>
1419            <m:mrow>
1420             <m:mtext>In&#x00a0;particular,&#x00a0;we&#x00a0;have</m:mtext>
1421            </m:mrow>
1422           </m:mtd>
1423          </m:mtr>
1424          <m:mtr>
1425           <m:mtd>
1426            <m:mrow>
1427             <m:mtext>(</m:mtext>
1428             <xsl:apply-templates select="*[3]"/>
1429             <m:mtext>)</m:mtext>
1430             <m:mphantom><m:mtext>_</m:mtext></m:mphantom>
1431             <xsl:apply-templates select="*[4]"/>
1432             </m:mrow>
1433           </m:mtd>
1434          </m:mtr>
1435          <m:mtr>
1436           <m:mtd>
1437            <m:mrow>
1438             <m:mtext>(</m:mtext>
1439             <xsl:apply-templates select="*[5]"/>
1440             <m:mtext>)</m:mtext>
1441             <m:mphantom><m:mtext>_</m:mtext></m:mphantom>
1442             <xsl:apply-templates select="*[6]"/>
1443             </m:mrow>
1444           </m:mtd>
1445          </m:mtr>
1446          <m:mtr>
1447           <m:mtd>
1448            <m:mrow>
1449             <xsl:apply-templates select="*[7]"/>
1450            </m:mrow>
1451           </m:mtd>
1452          </m:mtr>
1453         </m:mtable>
1454       </xsl:when>
1455       <!-- full_or_ind -->
1456       <xsl:when test="$name='full_or_ind'">
1457         <m:mtable align="baseline 1" equalrows="false" columnalign="left">
1458          <m:mtr>
1459           <m:mtd>
1460            <m:mrow>
1461             <xsl:choose>
1462              <xsl:when test="name(*[2])='m:apply'">
1463               <xsl:apply-templates select="*[2]"/>
1464              </xsl:when>
1465              <xsl:otherwise>
1466               <m:mtext>Consider</m:mtext>
1467               <m:mphantom><m:mtext>_</m:mtext></m:mphantom>
1468               <xsl:apply-templates select="*[2]"/>
1469              </xsl:otherwise>
1470             </xsl:choose>
1471            </m:mrow>
1472           </m:mtd>
1473          </m:mtr>
1474          <m:mtr>
1475           <m:mtd>
1476            <m:mrow>
1477             <m:mtext>We&#x00a0;proceed&#x00a0;by&#x00a0;cases&#x00a0;to&#x00a0;prove</m:mtext>
1478             <m:mphantom><m:mtext>_</m:mtext></m:mphantom>
1479             <xsl:apply-templates select="*[3]"/>
1480            </m:mrow>
1481           </m:mtd>
1482          </m:mtr>
1483          <m:mtr>
1484           <m:mtd>
1485            <m:mrow>
1486             <m:mtext>Left:&#x00a0;suppose</m:mtext>
1487             <m:mphantom><m:mtext>_</m:mtext></m:mphantom>
1488             <m:mo stretchy="false">(</m:mo>
1489             <xsl:apply-templates select="*[4]/m:bvar/m:ci"/>
1490             <m:mo stretchy="false">)</m:mo>
1491             <m:mphantom><m:mtext>_</m:mtext></m:mphantom>
1492             <xsl:apply-templates select="*[4]/m:bvar/m:type/*[1]"/>
1493            </m:mrow>
1494           </m:mtd>
1495          </m:mtr>
1496          <m:mtr>
1497           <m:mtd>
1498            <m:mrow>
1499             <m:mphantom><m:mtext>_</m:mtext></m:mphantom>
1500             <xsl:apply-templates select="*[4]/*[3]"/>
1501            </m:mrow>
1502           </m:mtd>
1503          </m:mtr>
1504          <m:mtr>
1505           <m:mtd>
1506            <m:mrow>
1507             <m:mtext>Right:&#x00a0;suppose</m:mtext>
1508             <m:mphantom><m:mtext>_</m:mtext></m:mphantom>
1509             <m:mo stretchy="false">(</m:mo>
1510             <xsl:apply-templates select="*[5]/m:bvar/m:ci"/>
1511             <m:mo stretchy="false">)</m:mo>
1512             <m:mphantom><m:mtext>_</m:mtext></m:mphantom>
1513             <xsl:apply-templates select="*[5]/m:bvar/m:type/*[1]"/>
1514            </m:mrow>
1515           </m:mtd>
1516          </m:mtr>
1517          <m:mtr>
1518           <m:mtd>
1519            <m:mrow>
1520             <xsl:apply-templates select="*[5]/*[3]"/>
1521            </m:mrow>
1522           </m:mtd>
1523          </m:mtr>
1524         </m:mtable>
1525       </xsl:when>
1526       <!-- OR_IND -->
1527       <xsl:when test="$name='or_ind'">
1528         <m:mtable align="baseline 1" equalrows="false" columnalign="left">
1529          <m:mtr>
1530           <m:mtd>
1531            <m:mrow>
1532             <xsl:choose>
1533              <xsl:when test="name(*[2])='m:apply'">
1534               <xsl:apply-templates select="*[2]"/>
1535              </xsl:when>
1536              <xsl:otherwise>
1537               <m:mtext>Consider</m:mtext>
1538               <m:mphantom><m:mtext>_</m:mtext></m:mphantom>
1539               <xsl:apply-templates select="*[2]"/>
1540              </xsl:otherwise>
1541             </xsl:choose>
1542            </m:mrow>
1543           </m:mtd>
1544          </m:mtr>
1545          <m:mtr>
1546           <m:mtd>
1547            <m:mrow>
1548             <m:mtext>We&#x00a0;prove</m:mtext>
1549             <m:mphantom><m:mtext>_</m:mtext></m:mphantom>
1550             <xsl:apply-templates select="*[3]"/>
1551             <m:mphantom><m:mtext>_</m:mtext></m:mphantom>
1552             <m:mtext>by&#x00a0;cases:</m:mtext>
1553            </m:mrow>
1554           </m:mtd>
1555          </m:mtr>
1556          <m:mtr>
1557           <m:mtd>
1558            <m:mrow>
1559             <m:mtext>Left</m:mtext>
1560             <xsl:apply-templates select="*[4]"/>
1561            </m:mrow>
1562           </m:mtd>
1563          </m:mtr>
1564          <m:mtr>
1565           <m:mtd>
1566            <m:mrow>
1567             <m:mtext>Right</m:mtext>
1568             <xsl:apply-templates select="*[5]"/>
1569            </m:mrow>
1570           </m:mtd>
1571          </m:mtr>
1572         </m:mtable>
1573       </xsl:when>
1574       <!-- EX_IND -->
1575       <xsl:when test="$name='ex_ind'">
1576         <m:mtable align="baseline 1" equalrows="false" columnalign="left">
1577          <m:mtr>
1578           <m:mtd>
1579            <m:mrow>
1580             <xsl:choose>
1581              <xsl:when test="name(*[2])='m:apply'">
1582               <xsl:apply-templates select="*[2]"/>
1583              </xsl:when>
1584              <xsl:otherwise>
1585               <m:mtext>Consider</m:mtext>
1586               <m:mphantom><m:mtext>_</m:mtext></m:mphantom>
1587               <xsl:apply-templates select="*[2]"/>
1588              </xsl:otherwise>
1589             </xsl:choose>
1590            </m:mrow>
1591           </m:mtd>
1592          </m:mtr>
1593          <m:mtr>
1594           <m:mtd>
1595            <m:mrow>
1596             <m:mtext>Let</m:mtext>
1597             <m:mphantom><m:mtext>_</m:mtext></m:mphantom>
1598             <xsl:apply-templates select="*[3]"/>
1599             <m:mtext>:</m:mtext>
1600             <xsl:apply-templates select="*[4]"/>
1601             <m:mphantom><m:mtext>_</m:mtext></m:mphantom>
1602             <m:mtext>such&#x00a0;that</m:mtext>
1603             <m:mphantom><m:mtext>_</m:mtext></m:mphantom>
1604             <m:mtext>(</m:mtext>
1605              <xsl:apply-templates select="*[5]"/>
1606             <m:mtext>)</m:mtext>
1607             <m:mphantom><m:mtext>_</m:mtext></m:mphantom>
1608             <xsl:apply-templates select="*[6]"/>
1609            </m:mrow>
1610           </m:mtd>
1611          </m:mtr>
1612          <m:mtr>
1613           <m:mtd>
1614            <m:mrow>
1615             <xsl:apply-templates select="*[7]"/>
1616            </m:mrow>
1617           </m:mtd>
1618          </m:mtr>
1619         </m:mtable>
1620       </xsl:when>
1621       <!-- EQ_CHAIN -->
1622       <xsl:when test="$name='eq_chain'">
1623        <m:mtable align="baseline 1" equalrows="false" columnalign="left">
1624         <m:mtr>
1625          <m:mtd>
1626           <m:mrow>
1627            <m:mtext mathcolor="Red">We&#x00a0;have&#x00a0;the&#x00a0;following&#x00a0;equality&#x00a0;chain:</m:mtext>
1628           </m:mrow>
1629          </m:mtd>
1630         </m:mtr>
1631         <xsl:for-each select="*[position() mod 2 = 0]">
1632         <xsl:variable name="pos" select="position()"/>
1633         <m:mtr>
1634          <m:mtd>
1635           <m:mrow>
1636            <xsl:choose>
1637            <xsl:when test="$pos = 1">
1638             <xsl:apply-templates select="."/>
1639             <m:mphantom><m:mtext>_</m:mtext></m:mphantom>
1640             <m:mo>=</m:mo>
1641            </xsl:when>
1642            <xsl:otherwise>
1643             <m:mo>=</m:mo>
1644             <m:mphantom><m:mtext>_</m:mtext></m:mphantom>
1645             <xsl:apply-templates select="."/>
1646            </xsl:otherwise>
1647            </xsl:choose>
1648           </m:mrow>
1649          </m:mtd>
1650         </m:mtr>
1651         <xsl:if test="$pos != last()">
1652         <m:mtr>
1653          <m:mtd>
1654           <m:mrow>
1655            <m:mphantom><m:mtext>__</m:mtext></m:mphantom>
1656            <xsl:apply-templates select="../*[position()=2*$pos +1]"/>
1657           </m:mrow>
1658          </m:mtd>
1659         </m:mtr>
1660         </xsl:if>
1661         </xsl:for-each>
1662        </m:mtable>
1663       </xsl:when>
1664       <!-- DISEQ_CHAIN -->
1665       <xsl:when test="$name='diseq_chain'">
1666        <m:mtable align="baseline 1" equalrows="false" columnalign="left">
1667         <m:mtr>
1668          <m:mtd>
1669           <m:mrow>
1670            <m:mtext mathcolor="Red">We&#x00a0;have&#x00a0;the&#x00a0;following&#x00a0;disequality&#x00a0;chain:</m:mtext>
1671           </m:mrow>
1672          </m:mtd>
1673         </m:mtr>
1674         <xsl:for-each select="*[position() mod 3 = 2]">
1675         <xsl:variable name="pos" select="position()"/>
1676         <m:mtr>
1677          <m:mtd>
1678           <m:mrow>
1679            <xsl:choose>
1680            <xsl:when test="$pos = 1">
1681             <xsl:apply-templates select="."/>
1682             <m:mphantom><m:mtext>_</m:mtext></m:mphantom>
1683             <mo><xsl:apply-templates select="../*[position()=3*$pos]"/></mo>
1684            </xsl:when>
1685            <xsl:otherwise>
1686             <mo><xsl:apply-templates select="../*[position()=3*($pos - 1)]"/></mo>
1687             <m:mphantom><m:mtext>_</m:mtext></m:mphantom>
1688             <xsl:apply-templates select="."/>
1689            </xsl:otherwise>
1690            </xsl:choose>
1691           </m:mrow>
1692          </m:mtd>
1693         </m:mtr>
1694         <xsl:if test="$pos != last()">
1695         <m:mtr>
1696          <m:mtd>
1697           <m:mrow>
1698            <m:mphantom><m:mtext>__</m:mtext></m:mphantom>
1699            <xsl:apply-templates select="../*[position()=3*$pos +1]"/>
1700           </m:mrow>
1701          </m:mtd>
1702         </m:mtr>
1703         </xsl:if>
1704         </xsl:for-each>
1705        </m:mtable>
1706       </xsl:when>
1707       <!-- ***************************************** -->
1708       <!-- *********** NOTATIONS ******************* -->
1709       <!-- ***************************************** -->
1710       <!-- subst -->
1711       <xsl:when test="$name='subst'">
1712         <xsl:apply-templates select="*[3]"/>
1713 <!-- no font for ApplyFunction: <m:mo>&#xe8a0;</m:mo> -->
1714         <m:mo stretchy="false">[</m:mo>
1715         <xsl:apply-templates select="*[4]"/>
1716         <m:mo mathcolor="Green">
1717          <xsl:if test="$id != ''">
1718           <xsl:attribute name="xref"><xsl:value-of select="$id"/></xsl:attribute>
1719          </xsl:if>&#8592;</m:mo>
1720         <xsl:apply-templates select="*[2]"/>
1721         <m:mo stretchy="false">]</m:mo>
1722       </xsl:when>
1723       <!-- lift -->
1724       <xsl:when test="$name='lift'">
1725         <m:msup>
1726          <m:mo mathcolor="Green">
1727           <xsl:if test="$id != ''">
1728            <xsl:attribute name="xref"><xsl:value-of select="$id"/></xsl:attribute>
1729           </xsl:if>&#8593;</m:mo>
1730          <xsl:apply-templates select="*[2]"/>
1731         </m:msup>
1732         <m:mrow>
1733          <m:mo stretchy="false">(</m:mo>
1734          <xsl:apply-templates select="*[3]"/>
1735          <m:mo stretchy="false">)</m:mo>
1736         </m:mrow>
1737       </xsl:when>
1738       <!-- lift_with_base -->
1739       <xsl:when test="$name='lift_with_base'">
1740         <m:msubsup>
1741          <m:mo mathcolor="Green">
1742           <xsl:if test="$id != ''">
1743            <xsl:attribute name="xref"><xsl:value-of select="$id"/></xsl:attribute>
1744           </xsl:if>&#8593;</m:mo>
1745          <xsl:apply-templates select="*[3]"/>
1746          <xsl:apply-templates select="*[4]"/>
1747         </m:msubsup>
1748         <m:mrow>
1749          <m:mo stretchy="false">(</m:mo>
1750          <xsl:apply-templates select="*[2]"/>
1751          <m:mo stretchy="false">)</m:mo>
1752         </m:mrow>
1753       </xsl:when>
1754       <!-- beta_red1 -->
1755       <xsl:when test="$name='beta_red1'">
1756         <xsl:apply-templates select="*[2]"/>
1757         <m:munder>
1758          <m:mo mathcolor="Green">
1759           <xsl:if test="$id != ''">
1760            <xsl:attribute name="xref"><xsl:value-of select="$id"/></xsl:attribute>
1761           </xsl:if>&#8594;</m:mo>
1762           <m:mi mathcolor="Green">&#946;</m:mi>
1763         </m:munder>
1764         <xsl:apply-templates select="*[3]"/>
1765       </xsl:when>
1766       <!-- beta_red -->
1767       <xsl:when test="$name='beta_red'">
1768         <xsl:apply-templates select="*[2]"/>
1769         <m:munderover>
1770          <m:mo mathcolor="Green">
1771           <xsl:if test="$id != ''">
1772            <xsl:attribute name="xref"><xsl:value-of select="$id"/></xsl:attribute>
1773           </xsl:if>&#8594;</m:mo>
1774           <m:mi mathcolor="Green">&#946;</m:mi>
1775           <m:mi mathcolor="Green">*</m:mi>
1776         </m:munderover>
1777         <xsl:apply-templates select="*[3]"/>
1778       </xsl:when>
1779       <!-- par_beta_red1 -->
1780       <xsl:when test="$name='par_beta_red1'">
1781         <xsl:apply-templates select="*[2]"/>
1782         <m:munder>
1783          <m:mo mathcolor="Green">
1784           <xsl:if test="$id != ''">
1785            <xsl:attribute name="xref"><xsl:value-of select="$id"/></xsl:attribute>
1786           </xsl:if>&#8658;</m:mo>
1787           <m:mi mathcolor="Green">&#946;</m:mi>
1788         </m:munder>
1789         <xsl:apply-templates select="*[3]"/>
1790       </xsl:when>
1791       <!-- par_beta_red -->
1792       <xsl:when test="$name='par_beta_red'">
1793         <xsl:apply-templates select="*[2]"/>
1794         <m:munderover>
1795          <m:mo mathcolor="Green">
1796           <xsl:if test="$id != ''">
1797            <xsl:attribute name="xref"><xsl:value-of select="$id"/></xsl:attribute>
1798           </xsl:if>&#8658;</m:mo>
1799           <m:mi mathcolor="Green">&#946;</m:mi>
1800           <m:mi mathcolor="Green">*</m:mi>
1801         </m:munderover>
1802         <xsl:apply-templates select="*[3]"/>
1803       </xsl:when>
1804       <!-- forgetful -->
1805       <xsl:when test="$name='forgetful'">
1806        <m:mfenced open="|" close="|">
1807         <xsl:if test="$id != ''">
1808          <xsl:attribute name="xref"><xsl:value-of select="$id"/></xsl:attribute>
1809         </xsl:if>
1810         <xsl:apply-templates select="*[2]"/>
1811        </m:mfenced>
1812       </xsl:when>
1813       <!-- isomorphic -->
1814       <xsl:when test="$name='isomorphic'">
1815         <xsl:apply-templates select="*[2]"/>
1816         <m:mo mathcolor="Green">
1817          <xsl:if test="$id != ''">
1818           <xsl:attribute name="xref"><xsl:value-of select="$id"/></xsl:attribute>
1819          </xsl:if>&#8773;</m:mo>
1820         <xsl:apply-templates select="*[3]"/>
1821       </xsl:when>
1822       <!-- interp -->
1823       <xsl:when test="$name='forgetful'">
1824        <m:mfenced open="[" close="]">
1825         <xsl:if test="$id != ''">
1826          <xsl:attribute name="xref"><xsl:value-of select="$id"/></xsl:attribute>
1827         </xsl:if>
1828         <xsl:apply-templates select="*[2]"/>
1829        </m:mfenced>
1830       </xsl:when>
1831
1832       <!-- ERROR -->
1833       <xsl:otherwise>
1834        <m:mi>ERROR</m:mi>
1835       </xsl:otherwise>
1836      </xsl:choose>
1837     </m:mrow>
1838 </xsl:template>
1839
1840 <!-- Il modo Thread non esiste piu'
1841 <xsl:template match="*" mode="thread">
1842  <xsl:variable name="name"><xsl:value-of select="following-sibling::*[position()=1]/m:csymbol"/></xsl:variable>
1843  <xsl:choose>
1844   <xsl:when test="$name='rw_step'">
1845          <m:mtr>
1846           <m:mtd>
1847            <m:mrow>
1848             <m:mtext>Rewrite</m:mtext>
1849             <m:mphantom><m:mtext>_</m:mtext></m:mphantom>
1850             <xsl:apply-templates select="following-sibling::*[position()=1]/*[2]"/>
1851             <m:mphantom><m:mtext>_</m:mtext></m:mphantom>
1852             <m:mtext>with</m:mtext>
1853             <m:mphantom><m:mtext>_</m:mtext></m:mphantom>
1854             <xsl:apply-templates select="following-sibling::*[position()=1]/*[3]"/>
1855             <m:mphantom><m:mtext>_</m:mtext></m:mphantom>
1856             <m:mtext>by</m:mtext>
1857             <m:mphantom><m:mtext>_</m:mtext></m:mphantom>
1858             <xsl:apply-templates select="following-sibling::*[position()=1]/*[4]"/>
1859            </m:mrow>
1860           </m:mtd>
1861          </m:mtr>
1862          <m:mtr>
1863           <m:mtd>
1864            <m:mrow>
1865             <m:mtext mathcolor="Red">we&#x00a0;get</m:mtext>
1866             <m:mphantom><m:mtext>_</m:mtext></m:mphantom>
1867             <xsl:apply-templates select="."/>
1868            </m:mrow>
1869           </m:mtd>
1870          </m:mtr>
1871    </xsl:when>
1872    <xsl:otherwise>
1873          <m:mtr>
1874           <m:mtd>
1875            <m:mrow>
1876             <xsl:apply-templates select="following-sibling::*[position()=1]"/>
1877            </m:mrow>
1878           </m:mtd>
1879          </m:mtr>
1880          <m:mtr>
1881           <m:mtd>
1882            <m:mrow>
1883             <m:mtext mathcolor="Red">we&#x00a0;get</m:mtext>
1884             <m:mphantom><m:mtext>_</m:mtext></m:mphantom>
1885             <xsl:apply-templates select="."/>
1886            </m:mrow>
1887           </m:mtd>
1888          </m:mtr>
1889     </xsl:otherwise>
1890    </xsl:choose>
1891          <xsl:apply-templates mode="thread" select="preceding-sibling::*[position()=2]"/>
1892 </xsl:template>
1893 -->
1894
1895 <!-- LAMBDA -->
1896
1897 <xsl:template match="m:lambda">
1898     <xsl:variable name="charlength"><xsl:apply-templates select="*[position()=1]" mode="charcount"/></xsl:variable>
1899     <m:mrow>
1900      <xsl:if test="@id">
1901       <xsl:attribute name="xref">
1902        <xsl:value-of select="@id"/>
1903       </xsl:attribute>
1904      </xsl:if>
1905      <xsl:choose>
1906      <xsl:when test="$charlength >= $framewidth">
1907       <m:mtable align="baseline 1" equalrows="false" columnalign="left">
1908         <m:mtr>
1909           <m:mtd>
1910            <m:mrow>
1911             <m:mo mathcolor="Red">&#x03bb;</m:mo>
1912             <xsl:apply-templates select="m:bvar"/>
1913            </m:mrow>
1914           </m:mtd>
1915          </m:mtr>
1916        <m:mtr>
1917         <m:mtd>
1918          <m:mrow>
1919           <m:mo>.</m:mo>
1920           <xsl:apply-templates select="*[position()=2]"/>
1921          </m:mrow>
1922         </m:mtd>
1923        </m:mtr>
1924       </m:mtable>
1925      </xsl:when>
1926      <xsl:otherwise>
1927       <m:mo mathcolor="Red">&#x03bb;</m:mo>
1928       <xsl:apply-templates select="m:bvar/m:ci"/>
1929       <m:mo>:</m:mo>
1930       <xsl:apply-templates select="m:bvar/m:type"/>
1931       <m:mo>.</m:mo>
1932       <xsl:apply-templates select="*[position()=2]"/>
1933      </xsl:otherwise>
1934      </xsl:choose>
1935     </m:mrow>
1936 </xsl:template>
1937
1938
1939 <!--**********************-->
1940 <!--       COUNTING       -->
1941 <!--**********************-->
1942
1943 <xsl:template match="m:cn|m:and|m:or|m:not|m:exists|m:eq|m:lt|m:leq|m:gt|m:geq
1944  |m:in|m:notin|m:intersect|m:union|m:subset|m:prsubset|m:card|m:setdiff
1945  |m:plus|m:minus|m:times" mode="charcount">
1946 <xsl:param name="incurrent_length" select="0"/>
1947     <xsl:choose>
1948     <xsl:when test="$framewidth > ($incurrent_length + 3 + string-length())">
1949      <xsl:variable name="siblength">
1950       <xsl:apply-templates select="following-sibling::*[position()=1]" mode="charcount">
1951        <xsl:with-param name="incurrent_length" select="$incurrent_length + string-length()"/>
1952       </xsl:apply-templates>
1953      </xsl:variable>
1954      <xsl:choose>
1955      <xsl:when test="string($siblength) = &quot;&quot;">
1956       <xsl:value-of select="$incurrent_length + 3 + string-length()"/>
1957      </xsl:when>
1958      <xsl:otherwise>
1959       <xsl:value-of select="number($siblength)"/>
1960      </xsl:otherwise>
1961      </xsl:choose>
1962     </xsl:when>
1963     <xsl:otherwise>
1964      <xsl:value-of select="$incurrent_length + 3 + string-length()"/>
1965     </xsl:otherwise>
1966     </xsl:choose>
1967 </xsl:template>
1968
1969 <xsl:template match="m:ci|m:csymbol" mode="charcount">
1970 <xsl:param name="incurrent_length" select="0"/>
1971 <xsl:param name="nosibling" select="0"/>
1972     <xsl:choose>
1973     <xsl:when test="$framewidth > ($incurrent_length + string-length()) and ($nosibling = 0)">
1974      <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>
1975      <xsl:choose>
1976      <xsl:when test="string($siblength) = &quot;&quot;">
1977       <xsl:value-of select="$incurrent_length + string-length()"/>
1978      </xsl:when>
1979      <xsl:otherwise>
1980       <xsl:value-of select="number($siblength)"/>
1981      </xsl:otherwise>
1982      </xsl:choose>
1983     </xsl:when>
1984     <xsl:otherwise>
1985      <xsl:value-of select="$incurrent_length + string-length()"/>
1986     </xsl:otherwise>
1987     </xsl:choose>
1988 </xsl:template>
1989
1990 <xsl:template match="*" mode="charcount">
1991 <xsl:param name="incurrent_length" select="0"/>
1992 <xsl:param name="nosibling" select="0"/>
1993  <xsl:choose>
1994   <xsl:when test="count(child::*) = 0">
1995    <xsl:value-of select="$incurrent_length"/>
1996   </xsl:when>
1997   <xsl:otherwise>
1998     <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>
1999     <xsl:choose>
2000     <xsl:when test="$framewidth > number($childlength) and ($nosibling = 0)">
2001      <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>
2002      <xsl:choose>
2003      <xsl:when test="string($siblength) = &quot;&quot;">
2004       <xsl:value-of select="number($childlength)"/>
2005      </xsl:when>
2006      <xsl:otherwise>
2007       <xsl:value-of select="number($siblength)"/>
2008      </xsl:otherwise>
2009      </xsl:choose>
2010     </xsl:when>
2011     <xsl:otherwise>
2012      <xsl:value-of select="number($childlength)"/>
2013     </xsl:otherwise>
2014     </xsl:choose>
2015   </xsl:otherwise>
2016  </xsl:choose>
2017 </xsl:template>
2018
2019 </xsl:stylesheet>
2020