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