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