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