helm/nuprl_stylesheets/nuprl_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 <xsl:key name="sequent_number" use="@id" match="Sequent"/>
  49
  50 <xsl:param name="explodeall" select="false()"/>
  51
  52 <!--***********************************************************************-->
  53 <!-- Parameter affecting line-breaking                                     -->
  54 <!--***********************************************************************-->
  55
  56 <xsl:variable name="framewidth" select="35"/>
  57
  58 <!--***********************************************************************-->
  59 <!-- Gli oggetti sono stampati come mtext all'interno di una marca toplevel-->
  60 <!-- math ma al di fuori di semantics. Ora vi sono tanti semantics quanti  -->
  61 <!-- sono i termini: la presentation per un termine e' generata come primo -->
  62 <!-- figlio di un semantics e l'originario content viene inserito nel      -->
  63 <!-- nel secondo figlio di semantics, annotation-xml                       -->
  64 <!--***********************************************************************-->
  65
  66 <!--**********************-->
  67 <!--        OBJECTS       -->
  68 <!--**********************-->
  69
  70
  71 <!--<xsl:key name="variable" use="@name" match="Decl"/> -->
  72
  73 <xsl:param name="type" select="'standalone'"/>
  74
  75 <xsl:template match="/">
  76  <xsl:choose>
  77   <xsl:when test="$type = 'standalone'">
  78    <xsl:apply-templates select="*"/>
  79   </xsl:when>
  80   <xsl:otherwise>
  81    <to_be_embedded>
  82     <xsl:apply-templates select="*"/>
  83    </to_be_embedded>
  84   </xsl:otherwise>
  85  </xsl:choose>
  86 </xsl:template>
  87
  88
  89 <!-- NODE -->
  90
  91  <xsl:template match="Node">
  92      <xsl:choose>
  93       <xsl:when test="count(Node)=0">    <!-- E' una foglia -->
  94        <m:mtable align="baseline 1" equalrows="false" columnalign="left" stretchy="false">
  95         <m:mtr>
  96          <m:mtd>
  97           <m:mrow>
  98            <m:mtext mathcolor="red">Sequent <xsl:apply-templates select="Sequent/@id"/>
  99            </m:mtext>
 100           </m:mrow>
 101          </m:mtd>
 102         </m:mtr>
 103         <m:mtr>
 104         <xsl:if test="*[Decl]">
 105          <m:mtable align="baseline 1" equalrows="false" columnalign="left">
 106           <xsl:for-each select="Sequent/Decl">
 107            <m:mtr columnalign="left">
 108             <m:mtd columnalign="left">
 109              <m:mrow>
 110               <xsl:variable name="num" select="position()"/>
 111               <m:mtext>
 112                <xsl:value-of select="$num"/>)
 113               </m:mtext>
 114               <m:mphantom><m:mtext>__</m:mtext></m:mphantom>
 115               <xsl:if test="@name">
 116                <m:mo mathcolor="green"><xsl:value-of select="@name"/></m:mo>
 117                <m:mo mathcolor="green" stretchy="false">:</m:mo>
 118               </xsl:if>
 119               <xsl:apply-templates select="."/>
 120              </m:mrow>
 121             </m:mtd>
 122            </m:mtr>
 123           </xsl:for-each>
 124          </m:mtable>
 125         </xsl:if>
 126         </m:mtr>
 127         <m:mtr>
 128          <m:mrow>
 129           <m:mtext mathcolor="red" mathvariant="bold">|-</m:mtext>
 130          </m:mrow>
 131         </m:mtr>
 132         <m:mtr>
 133          <m:mtd>
 134           <xsl:apply-templates select="Sequent/Goal"/>
 135          </m:mtd>
 136         </m:mtr>
 137         <m:mtr>
 138          <m:mtd>
 139           <m:mrow>
 140            <m:mo mathcolor="red">Rule: </m:mo>
 141            <xsl:choose>
 142            <xsl:when test="Rule[m:apply]">
 143             <m:mo mathcolor="brown"><xsl:value-of select="Rule/m:apply/m:ci"/></m:mo>
 144            </xsl:when>
 145            <xsl:when test="count(Rule)=0">
 146             <m:mi>NESSUNA REGOLA</m:mi>
 147            </xsl:when>
 148            <xsl:otherwise>
 149             <m:mo mathcolor="brown"><xsl:value-of select="Rule/m:ci"/></m:mo>
 150            </xsl:otherwise>
 151            </xsl:choose>
 152           </m:mrow>
 153          </m:mtd>
 154         </m:mtr>
 155         <m:mspace height="1ex"/>
 156        </m:mtable>
 157       </xsl:when>
 158
 159      <xsl:otherwise>   <!--E' un nodo -->
 160      <m:mtable equalrows="false" columnalign="left">
 161       <m:mtr>
 162        <m:mtable align="baseline 1" equalrows="false" columnalign="left" stretchy="false">
 163         <m:mtr>
 164          <m:mtd>
 165           <m:mrow>
 166            <m:mtext mathcolor="red">Sequent <xsl:apply-templates select="Sequent/@id"/>
 167            </m:mtext>
 168           </m:mrow>
 169          </m:mtd>
 170         </m:mtr>
 171         <m:mtr>
 172         <xsl:if test="*[Decl]">
 173          <m:mtable align="baseline 1" equalrows="false" columnalign="left">
 174           <xsl:for-each select="Sequent/Decl">
 175            <m:mtr columnalign="left">
 176             <m:mtd columnalign="left">
 177              <m:mrow>
 178               <xsl:variable name="num" select="position()"/>
 179               <m:mtext>
 180                <xsl:value-of select="$num"/>)
 181               </m:mtext>
 182               <m:mphantom><m:mtext>__</m:mtext></m:mphantom>
 183               <xsl:if test="@name">
 184                <m:mo mathcolor="green"><xsl:value-of select="@name"/></m:mo>
 185                <m:mo mathcolor="green" stretchy="false">:</m:mo>
 186               </xsl:if>
 187               <xsl:apply-templates select="."/>
 188              </m:mrow>
 189             </m:mtd>
 190            </m:mtr>
 191           </xsl:for-each>
 192          </m:mtable>
 193         </xsl:if>
 194         </m:mtr>
 195         <m:mtr>
 196          <m:mrow>
 197           <m:mtext mathcolor="red" mathvariant="bold">|-</m:mtext>
 198          </m:mrow>
 199         </m:mtr>
 200         <m:mtr>
 201          <m:mtd>
 202           <xsl:apply-templates select="Sequent/Goal"/>
 203          </m:mtd>
 204         </m:mtr>
 205         <m:mtr>
 206          <m:mtd>
 207           <m:mrow>
 208            <m:mo mathcolor="red">Rule: </m:mo>
 209            <xsl:choose>
 210            <xsl:when test="Rule[m:apply]">
 211             <m:mo mathcolor="brown"><xsl:value-of select="Rule/m:apply/m:ci"/></m:mo>
 212            </xsl:when>
 213            <xsl:when test="count(Rule)=0">
 214             <m:mi>NESSUNA REGOLA</m:mi>
 215            </xsl:when>
 216            <xsl:otherwise>
 217             <m:mo mathcolor="brown"><xsl:value-of select="Rule/m:ci"/></m:mo>
 218            </xsl:otherwise>
 219            </xsl:choose>
 220           </m:mrow>
 221          </m:mtd>
 222         </m:mtr>
 223        </m:mtable>
 224       </m:mtr>
 225       <m:mtr>
 226        <m:maction>
 227         <xsl:choose>
 228         <xsl:when test="count(Node)=1">
 229          <m:mi mathcolor="blue" mathvariant="script">Subgoal</m:mi>
 230         </xsl:when>
 231         <xsl:otherwise>
 232          <m:mi mathcolor="blue" mathvariant="script">Subgoals</m:mi>
 233         </xsl:otherwise>
 234         </xsl:choose>
 235         <m:mrow>
 236          <m:mspace width="1em"/>
 237          <m:mtable equalrows="false" columnalign="left">
 238           <xsl:for-each select="Node">
 239            <m:mtr>
 240             <xsl:apply-templates select="."/>
 241            </m:mtr>
 242            <m:mspace height="1ex"/>
 243           </xsl:for-each>
 244          </m:mtable>
 245         </m:mrow>
 246        </m:maction>
 247       </m:mtr>
 248      </m:mtable>
 249      </xsl:otherwise>
 250      </xsl:choose>
 251 </xsl:template>
 252
 253
 254 <!-- NuPRLDefinition -->
 255
 256 <xsl:template match="NuPrlDefinition">
 257  <m:math>
 258   <m:mrow>
 259    <xsl:apply-templates select="*[1]"/>
 260    <m:mo> := </m:mo>
 261    <xsl:apply-templates select="*[2]"/>
 262   </m:mrow>
 263  </m:math>
 264 </xsl:template>
 265
 266 <!-- DEFINITION -->
 267
 268 <xsl:template match="Definition">
 269     <m:math>
 270      <m:mtable align="baseline 1" equalrows="false" columnalign="left" helm:xref="{@helm:xref}">
 271       <m:mtr>
 272        <m:mtd>
 273         <m:mrow>
 274          <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>
 275         </m:mrow>
 276        </m:mtd>
 277       </m:mtr>
 278       <m:mtr>
 279        <m:mtd>
 280         <m:mrow>
 281          <m:mphantom><m:mtext>__</m:mtext></m:mphantom>
 282          <xsl:apply-templates select="type/*[1]"/>
 283         </m:mrow>
 284        </m:mtd>
 285       </m:mtr>
 286       <m:mtr>
 287        <m:mtd>
 288         <m:mrow>
 289          <m:mtext>AS</m:mtext>
 290         </m:mrow>
 291        </m:mtd>
 292       </m:mtr>
 293       <m:mtr>
 294        <m:mtd>
 295         <m:mrow>
 296          <m:mphantom><m:mtext>__</m:mtext></m:mphantom>
 297          <xsl:apply-templates select="body/Node"/>   <!-- body/*[1]"/>-->
 298         </m:mrow>
 299        </m:mtd>
 300       </m:mtr>
 301      </m:mtable>
 302     </m:math>
 303 </xsl:template>
 304
 305 <!-- AXIOM -->
 306
 307 <xsl:template match="Axiom">
 308     <m:math>
 309      <m:mtable align="baseline 1" equalrows="false" columnalign="left" helm:xref="{@helm:xref}">
 310       <m:mtr>
 311        <m:mtd>
 312         <m:mrow>
 313          <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>
 314         </m:mrow>
 315        </m:mtd>
 316       </m:mtr>
 317       <m:mtr>
 318        <m:mtd>
 319         <m:mrow>
 320          <m:mphantom><m:mtext>__</m:mtext></m:mphantom>
 321          <xsl:apply-templates select="type/*[1]"/>
 322         </m:mrow>
 323        </m:mtd>
 324       </m:mtr>
 325      </m:mtable>
 326     </m:math>
 327 </xsl:template>
 328
 329 <!-- UNFINISHED PROOF -->
 330
 331 <xsl:template match="CurrentProof">
 332     <m:math>
 333      <m:mtable align="baseline 1" equalrows="false" columnalign="left" helm:xref="{@helm:xref}">
 334       <m:mtr>
 335        <m:mtd>
 336         <m:mrow>
 337          <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>
 338         </m:mrow>
 339        </m:mtd>
 340       </m:mtr>
 341       <m:mtr>
 342        <m:mtd>
 343         <m:mrow>
 344          <m:mtext>THESIS:</m:mtext>
 345         </m:mrow>
 346        </m:mtd>
 347       </m:mtr>
 348       <m:mtr>
 349        <m:mtd>
 350         <m:mrow>
 351          <m:mphantom><m:mtext>__</m:mtext></m:mphantom>
 352          <xsl:apply-templates select="type/*[1]"/>
 353         </m:mrow>
 354        </m:mtd>
 355       </m:mtr>
 356       <m:mtr>
 357        <m:mtd>
 358         <m:mrow>
 359          <m:mtext>CONJECTURES:</m:mtext>
 360         </m:mrow>
 361        </m:mtd>
 362       </m:mtr>
 363       <xsl:for-each select="Conjecture">
 364       <m:mtr>
 365        <m:mtd>
 366         <m:mrow helm:xref="{@helm:xref}">
 367          <m:mphantom><m:mtext>__</m:mtext></m:mphantom>
 368          <xsl:for-each select="Decl|Def|Hidden">
 369           <xsl:choose>
 370            <xsl:when test="name(.)='Decl'">
 371             <m:mrow helm:xref="{@helm:xref}">
 372              <xsl:choose>
 373               <xsl:when test="@name">
 374                <m:mi><xsl:value-of select="@name"/></m:mi>
 375               </xsl:when>
 376               <xsl:otherwise>
 377                <m:mi>_</m:mi>
 378               </xsl:otherwise>
 379              </xsl:choose>
 380              <m:mo>:</m:mo>
 381              <xsl:apply-templates select="./*[1]"/>
 382             </m:mrow>
 383            </xsl:when>
 384            <xsl:when test="name(.)='Def'">
 385             <m:mrow helm:xref="{@helm:xref}">
 386              <xsl:choose>
 387               <xsl:when test="@name">
 388                <m:mi><xsl:value-of select="@name"/></m:mi>
 389               </xsl:when>
 390               <xsl:otherwise>
 391                <m:mi>_</m:mi>
 392               </xsl:otherwise>
 393              </xsl:choose>
 394              <m:mo>:=</m:mo>
 395              <xsl:apply-templates select="./*[1]"/>
 396             </m:mrow>
 397            </xsl:when>
 398            <xsl:otherwise>
 399             <m:mrow helm:xref="{@helm:xref}">
 400              <m:mi>_</m:mi>
 401              <m:mo>:?</m:mo>
 402              <m:mi>_</m:mi>
 403             </m:mrow>
 404            </xsl:otherwise>
 405           </xsl:choose>
 406           <xsl:if test="not (position() = last())">
 407            <m:mo>;</m:mo>
 408           </xsl:if>
 409          </xsl:for-each>
 410          <m:mo>|-</m:mo>
 411          <m:msub><m:mi>?</m:mi><m:mn><xsl:value-of select="@no"/></m:mn></m:msub>
 412          <m:mo>:</m:mo>
 413          <xsl:apply-templates select="./Goal/*[1]"/>
 414         </m:mrow>
 415        </m:mtd>
 416       </m:mtr>
 417       </xsl:for-each>
 418       <m:mtr>
 419        <m:mtd>
 420         <m:mrow>
 421          <m:mtext>PROOF:</m:mtext>
 422         </m:mrow>
 423        </m:mtd>
 424       </m:mtr>
 425       <m:mtr>
 426        <m:mtd>
 427         <m:mrow>
 428          <m:mphantom><m:mtext>__</m:mtext></m:mphantom>
 429          <xsl:apply-templates select="body/*[1]"/>
 430         </m:mrow>
 431        </m:mtd>
 432       </m:mtr>
 433      </m:mtable>
 434     </m:math>
 435 </xsl:template>
 436
 437 <!-- MUTUAL INDUCTIVE DEFINITION -->
 438
 439 <xsl:template match="InductiveDefinition">
 440     <m:math>
 441      <m:mtable align="baseline 1" equalrows="false" columnalign="left" helm:xref="{@helm:xref}">
 442      <xsl:for-each select="InductiveType">
 443       <m:mtr>
 444        <m:mtd>
 445         <m:mrow>
 446          <xsl:choose>
 447          <xsl:when test="position() = 1">
 448           <xsl:choose>
 449           <xsl:when test="string(./@inductive) = &quot;true&quot;">
 450            <m:mtext>INDUCTIVE DEFINITION</m:mtext>
 451           </xsl:when>
 452           <xsl:otherwise>
 453            <m:mtext>COINDUCTIVE DEFINITION</m:mtext>
 454           </xsl:otherwise>
 455           </xsl:choose>
 456          </xsl:when>
 457          <xsl:otherwise>
 458           <m:mtext>AND</m:mtext>
 459          </xsl:otherwise>
 460          </xsl:choose>
 461          <m:mphantom><m:mtext>_</m:mtext></m:mphantom>
 462          <m:mtext><xsl:value-of select="./@name"/>(<xsl:if test="string(../Params) != &quot;&quot;"><xsl:value-of select="../Params"/></xsl:if>)</m:mtext>
 463         </m:mrow>
 464        </m:mtd>
 465       </m:mtr>
 466       <m:mtr>
 467        <m:mtd>
 468         <m:mrow>
 469          <m:mphantom><m:mtext>__</m:mtext></m:mphantom>
 470          <m:mtext>[</m:mtext>
 471          <xsl:choose>
 472          <xsl:when test="string(../Param) != &quot;&quot;">
 473           <m:mtable align="baseline 1" equalrows="false" columnalign="left">
 474            <xsl:for-each select="../Param">
 475             <m:mtr>
 476              <m:mtd>
 477               <m:mrow>
 478                <m:mi><xsl:value-of select="./@name"/></m:mi>
 479                <m:mo>:</m:mo>
 480                <xsl:apply-templates select="*"/>
 481               </m:mrow>
 482              </m:mtd>
 483             </m:mtr>
 484            </xsl:for-each>
 485             <m:mtr>
 486              <m:mtd>
 487               <m:mrow>
 488                <m:mtext>]</m:mtext>
 489               </m:mrow>
 490              </m:mtd>
 491             </m:mtr>
 492           </m:mtable>
 493          </xsl:when>
 494          <xsl:otherwise>
 495           <m:mtext>]</m:mtext>
 496          </xsl:otherwise>
 497          </xsl:choose>
 498         </m:mrow>
 499        </m:mtd>
 500       </m:mtr>
 501       <m:mtr>
 502        <m:mtd>
 503         <m:mrow>
 504          <m:mtext>OF ARITY</m:mtext>
 505         </m:mrow>
 506        </m:mtd>
 507       </m:mtr>
 508       <m:mtr>
 509        <m:mtd>
 510         <m:mrow>
 511          <m:mphantom><m:mtext>__</m:mtext></m:mphantom>
 512          <xsl:apply-templates select="./arity/*[1]"/>
 513         </m:mrow>
 514        </m:mtd>
 515       </m:mtr>
 516       <m:mtr>
 517        <m:mtd>
 518         <m:mrow>
 519          <m:mtext>BUILT FROM</m:mtext>
 520         </m:mrow>
 521        </m:mtd>
 522       </m:mtr>
 523       <xsl:for-each select="./Constructor">
 524       <m:mtr>
 525        <m:mtd>
 526         <m:mrow>
 527          <xsl:choose>
 528          <xsl:when test="position() = 1">
 529           <m:mphantom><m:mtext>__</m:mtext></m:mphantom>
 530          </xsl:when>
 531          <xsl:otherwise>
 532           <m:mtext>|</m:mtext>
 533           <m:mphantom><m:mtext>_</m:mtext></m:mphantom>
 534          </xsl:otherwise>
 535          </xsl:choose>
 536          <m:mtext><xsl:value-of select="./@name"/> OF</m:mtext>
 537          <m:mphantom><m:mtext>_</m:mtext></m:mphantom>
 538          <xsl:apply-templates select="./*[1]"/>
 539         </m:mrow>
 540        </m:mtd>
 541       </m:mtr>
 542       </xsl:for-each>
 543      </xsl:for-each>
 544      </m:mtable>
 545     </m:math>
 546 </xsl:template>
 547
 548 <!-- VARIABLE -->
 549
 550 <xsl:template match="Variable">
 551     <m:math>
 552      <m:mtable align="baseline 1" equalrows="false" columnalign="left" helm:xref="{@helm:xref}">
 553       <m:mtr>
 554        <m:mtd>
 555         <m:mrow>
 556          <m:mtext>VARIABLE <xsl:value-of select="@name"/> OF TYPE</m:mtext>
 557         </m:mrow>
 558        </m:mtd>
 559       </m:mtr>
 560       <m:mtr>
 561        <m:mtd>
 562         <m:mrow>
 563          <m:mphantom><m:mtext>__</m:mtext></m:mphantom>
 564          <xsl:apply-templates select="type/*[1]"/>
 565         </m:mrow>
 566        </m:mtd>
 567       </m:mtr>
 568       <xsl:if test="name(*[1])='body'">
 569        <m:mtr>
 570         <m:mtd>
 571          <m:mrow>
 572           <m:mtext>AS</m:mtext>
 573          </m:mrow>
 574         </m:mtd>
 575        </m:mtr>
 576        <m:mtr>
 577         <m:mtd>
 578          <m:mrow>
 579           <m:mphantom><m:mtext>__</m:mtext></m:mphantom>
 580           <xsl:apply-templates select="body/*[1]"/>
 581          </m:mrow>
 582         </m:mtd>
 583        </m:mtr>
 584       </xsl:if>
 585      </m:mtable>
 586     </m:math>
 587 </xsl:template>
 588
 589
 590
 591 <!-- SEQUENT -->
 592 <!--
 593 <xsl:template match="Sequent">
 594  <xsl:variable name="rowlines">
 595   <xsl:for-each select="Decl|Def">
 596    <xsl:if test="position() != last()">
 597     <xsl:text>none </xsl:text>
 598    </xsl:if>
 599   </xsl:for-each>
 600   <xsl:text>solid</xsl:text>
 601  </xsl:variable>
 602  <xsl:variable name="no" select="@no"/>
 603     <m:math>
 604      <m:mi><xsl:text>?</xsl:text><xsl:value-of select="$no"/></m:mi>
 605      <m:mo>:</m:mo>
 606      <m:mphantom><m:mtext>_</m:mtext></m:mphantom>
 607      <m:mtable align="baseline 1" equalrows="false" columnalign="left" helm:xref="{@helm:xref}" rowlines="{$rowlines}">
 608       <xsl:for-each select="Decl|Def">
 609        <m:mtr>
 610         <m:mtd>
 611          <m:mrow helm:xref="{@helm:xref}">
 612           <m:mi><xsl:value-of select="@name"/></m:mi>
 613           <xsl:choose>
 614            <xsl:when test="name(.) = 'Decl'">
 615             <m:mo>:</m:mo>
 616            </xsl:when>
 617            <xsl:otherwise>
 618             <m:mo>:=</m:mo>
 619            </xsl:otherwise>
 620           </xsl:choose>
 621           <xsl:apply-templates select="*[1]"/>
 622          </m:mrow>
 623         </m:mtd>
 624        </m:mtr>
 625       </xsl:for-each>
 626       <xsl:if test="not(Decl|Def)">
 627       <m:mtr>
 628        <m:mtd>
 629         <m:mrow>
 630          <m:mphantom><m:mtext>_</m:mtext></m:mphantom>
 631         </m:mrow>
 632        </m:mtd>
 633       </m:mtr>
 634       </xsl:if>
 635       <m:mtr>
 636        <m:mtd>
 637         <m:mrow>
 638          <xsl:apply-templates select="Goal/*[1]"/>
 639         </m:mrow>
 640        </m:mtd>
 641       </m:mtr>
 642      </m:mtable>
 643     </m:math>
 644 </xsl:template>-->
 645
 646 <!--**********************-->
 647 <!--        TERMS         -->
 648 <!--**********************-->
 649
 650 <xsl:template match="m:bvar">
 651  <xsl:choose>
 652   <xsl:when test="m:type">
 653    <xsl:variable name="charlength">
 654     <xsl:apply-templates select="m:ci" mode="charcount"/>
 655    </xsl:variable>
 656    <xsl:choose>
 657     <xsl:when test="$charlength >= $framewidth">
 658      <m:mtable align="baseline 1" equalrows="false" columnalign="left">
 659       <m:mtr>
 660        <m:mtd>
 661         <m:mrow>
 662          <xsl:apply-templates select="m:ci"/>
 663          <m:mo>:</m:mo>
 664         </m:mrow>
 665        </m:mtd>
 666       </m:mtr>
 667       <m:mtr>
 668        <m:mtd>
 669         <m:mrow>
 670          <xsl:apply-templates select="m:type"/>
 671         </m:mrow>
 672        </m:mtd>
 673       </m:mtr>
 674      </m:mtable>
 675     </xsl:when>
 676     <xsl:otherwise>
 677      <m:mrow>
 678       <xsl:apply-templates select="m:ci"/>
 679       <m:mo>:</m:mo>
 680       <xsl:apply-templates select="m:type"/>
 681      </m:mrow>
 682     </xsl:otherwise>
 683    </xsl:choose>
 684   </xsl:when>
 685   <xsl:otherwise>
 686    <xsl:apply-templates select="m:ci"/>
 687   </xsl:otherwise>
 688  </xsl:choose>
 689 </xsl:template>
 690
 691 <xsl:template match="m:apply[m:implies]">
 692     <xsl:variable name="charlength"><xsl:apply-templates select="m:implies" mode="charcount"/></xsl:variable>
 693       <xsl:choose>
 694        <xsl:when test="$charlength >= $framewidth">
 695         <m:mtable align="baseline 1" equalrows="false" columnalign="left">
 696          <m:mtr>
 697           <m:mtd>
 698            <m:mrow>
 699             <xsl:apply-templates select="*[2]"/>
 700            </m:mrow>
 701           </m:mtd>
 702          </m:mtr>
 703          <m:mtr>
 704           <m:mtd>
 705            <m:mrow>
 706             <m:mo>&#8658;</m:mo>
 707             <xsl:apply-templates select="*[position()=3]"/>
 708            </m:mrow>
 709           </m:mtd>
 710          </m:mtr>
 711         </m:mtable>
 712        </xsl:when>
 713        <xsl:otherwise>
 714         <xsl:apply-templates select="*[2]"/>
 715         <m:mo>&#8658;</m:mo>
 716         <xsl:apply-templates select="*[position()=3]"/>
 717        </xsl:otherwise>
 718       </xsl:choose>
 719 </xsl:template>
 720
 721 <!-- CSYMBOL -->
 722
 723 <xsl:template match="m:apply[m:csymbol]">
 724 <xsl:param name="nopar" select="0"/>
 725     <xsl:variable name="name"><xsl:value-of select="m:csymbol"/></xsl:variable>
 726     <xsl:variable name="charlength"><xsl:apply-templates select="m:csymbol" mode="charcount"/></xsl:variable>
 727     <m:mrow>
 728      <xsl:if test="@id">
 729       <xsl:attribute name="xref"><xsl:value-of select="@id"/></xsl:attribute>
 730      </xsl:if>
 731      <xsl:variable name="id" select="m:csymbol/@id"/>
 732      <xsl:choose>
 733       <!-- META -->
 734       <xsl:when test="$name='meta'">
 735        <m:mrow>
 736         <xsl:apply-templates select="*[position()=2]"/>
 737         <m:mfenced open="[" close="]" separators=";">
 738          <xsl:apply-templates select="*[position()>2]"/>
 739         </m:mfenced>
 740        </m:mrow>
 741       </xsl:when>
 742       <!-- FORALL *-->
 743       <xsl:when test="$name='forall'">
 744        <xsl:choose>
 745        <xsl:when test="$charlength >= $framewidth">
 746         <m:mtable align="baseline 1" equalrows="false" columnalign="left">
 747          <m:mtr>
 748           <m:mtd>
 749            <m:mrow>
 750             <m:mo mathcolor="Blue">&#8704;</m:mo>
 751             <xsl:apply-templates select="m:bvar"/>
 752            </m:mrow>
 753           </m:mtd>
 754          </m:mtr>
 755          <m:mtr>
 756           <m:mtd>
 757            <m:mrow>
 758             <m:mo>.</m:mo>
 759             <xsl:apply-templates select="*[position()=3]"/>
 760            </m:mrow>
 761           </m:mtd>
 762          </m:mtr>
 763         </m:mtable>
 764        </xsl:when>
 765        <xsl:otherwise>
 766         <m:mo mathcolor="Blue">&#8704;</m:mo>
 767         <xsl:apply-templates select="m:bvar/m:ci"/>
 768         <m:mo>:</m:mo>
 769         <xsl:apply-templates select="m:bvar/m:type"/>
 770         <m:mo>.</m:mo>
 771         <xsl:apply-templates select="*[position()=3]"/>
 772        </xsl:otherwise>
 773        </xsl:choose>
 774       </xsl:when>
 775       <!-- LET-IN -->
 776       <xsl:when test="$name='let_in'">
 777        <xsl:choose>
 778        <xsl:when test="$charlength >= $framewidth">
 779         <m:mtable align="baseline 1" equalrows="false" columnalign="left">
 780          <m:mtr>
 781           <m:mtd>
 782            <m:mrow>
 783             <m:mo>LET</m:mo>
 784             <m:mphantom><m:mtext>_</m:mtext></m:mphantom>
 785             <xsl:apply-templates select="m:bvar"/>
 786            </m:mrow>
 787           </m:mtd>
 788          </m:mtr>
 789          <m:mtr>
 790           <m:mtd>
 791            <m:mrow>
 792             <m:mo>=</m:mo>
 793             <xsl:apply-templates select="*[position()=3]"/>
 794            </m:mrow>
 795           </m:mtd>
 796          </m:mtr>
 797          <m:mtr>
 798           <m:mtd>
 799            <m:mrow>
 800             <m:mo>IN</m:mo>
 801             <m:mphantom><m:mtext>_</m:mtext></m:mphantom>
 802             <xsl:apply-templates select="*[position()=4]"/>
 803            </m:mrow>
 804           </m:mtd>
 805          </m:mtr>
 806         </m:mtable>
 807        </xsl:when>
 808        <xsl:otherwise>
 809         <m:mo>LET</m:mo>
 810         <m:mphantom><m:mtext>_</m:mtext></m:mphantom>
 811         <xsl:apply-templates select="m:bvar/m:ci"/>
 812         <m:mo>=</m:mo>
 813         <xsl:apply-templates select="*[position()=3]"/>
 814         <m:mphantom><m:mtext>_</m:mtext></m:mphantom>
 815         <m:mtext>IN</m:mtext>
 816         <m:mphantom><m:mtext>_</m:mtext></m:mphantom>
 817         <xsl:apply-templates select="*[position()=4]"/>
 818        </xsl:otherwise>
 819        </xsl:choose>
 820       </xsl:when>
 821       <!-- PROD *-->
 822       <xsl:when test="$name='prod'">
 823        <xsl:choose>
 824        <xsl:when test="$charlength >= $framewidth">
 825         <m:mtable align="baseline 1" equalrows="false" columnalign="left">
 826          <m:mtr>
 827           <m:mtd>
 828            <m:mrow>
 829             <m:mo mathcolor="Blue">&#x03a0;</m:mo>
 830             <xsl:apply-templates select="m:bvar"/>
 831            </m:mrow>
 832           </m:mtd>
 833          </m:mtr>
 834          <m:mtr>
 835           <m:mtd>
 836            <m:mrow>
 837             <m:mo>.</m:mo>
 838             <xsl:apply-templates select="*[position()=3]"/>
 839            </m:mrow>
 840           </m:mtd>
 841          </m:mtr>
 842         </m:mtable>
 843        </xsl:when>
 844        <xsl:otherwise>
 845         <m:mo mathcolor="Blue">&#x03a0;</m:mo>
 846         <xsl:apply-templates select="m:bvar/m:ci"/>
 847         <m:mo>:</m:mo>
 848         <xsl:apply-templates select="m:bvar/m:type"/>
 849         <m:mo>.</m:mo>
 850         <xsl:apply-templates select="*[position()=3]"/>
 851        </xsl:otherwise>
 852        </xsl:choose>
 853       </xsl:when>
 854       <!-- ARROW *-->
 855       <xsl:when test="$name='arrow'">
 856        <xsl:choose>
 857        <xsl:when test="$charlength >= $framewidth">
 858         <m:mtable align="baseline 1" equalrows="false" columnalign="left">
 859          <m:mtr>
 860           <m:mtd>
 861            <m:mrow>
 862             <xsl:if test="$nopar=0">
 863              <m:mo stretchy="false">(</m:mo>
 864             </xsl:if>
 865             <xsl:apply-templates select="*[position()=2]"/>
 866            </m:mrow>
 867           </m:mtd>
 868          </m:mtr>
 869          <m:mtr>
 870           <m:mtd>
 871            <m:mrow>
 872             <m:mo mathmathcolor="Blue">&#x2192;</m:mo>
 873             <xsl:choose>
 874             <xsl:when test="*[position()=3]/m:csymbol">
 875              <xsl:variable name="nextp"><xsl:value-of select="*[position()=3]/m:csymbol"/></xsl:variable>
 876              <xsl:choose>
 877              <xsl:when test="$nextp='arrow'">
 878               <xsl:apply-templates select="*[position()=3]"><xsl:with-param name="nopar" select="1"/></xsl:apply-templates>
 879              </xsl:when>
 880              <xsl:otherwise>
 881               <xsl:apply-templates select="*[position()=3]"/>
 882              </xsl:otherwise>
 883              </xsl:choose>
 884             </xsl:when>
 885             <xsl:otherwise>
 886              <xsl:apply-templates select="*[position()=3]"/>
 887             </xsl:otherwise>
 888             </xsl:choose>
 889            </m:mrow>
 890           </m:mtd>
 891          </m:mtr>
 892          <xsl:if test="$nopar=0">
 893          <m:mtr>
 894           <m:mtd>
 895            <m:mrow>
 896             <m:mo stretchy="false">)</m:mo>
 897            </m:mrow>
 898           </m:mtd>
 899          </m:mtr>
 900          </xsl:if>
 901         </m:mtable>
 902        </xsl:when>
 903        <xsl:otherwise>
 904         <xsl:if test="$nopar=0">
 905          <m:mo stretchy="false">(</m:mo>
 906         </xsl:if>
 907         <xsl:apply-templates select="*[position()=2]"/>
 908         <m:mo mathcolor="Blue">&#x2192;</m:mo>
 909         <xsl:choose>
 910         <xsl:when test="*[position()=3]/m:csymbol">
 911          <xsl:variable name="nextp"><xsl:value-of select="*[position()=3]/m:csymbol"/></xsl:variable>
 912          <xsl:choose>
 913          <xsl:when test="$nextp='arrow'">
 914           <xsl:apply-templates select="*[position()=3]"><xsl:with-param name="nopar" select="1"/></xsl:apply-templates>
 915          </xsl:when>
 916          <xsl:otherwise>
 917           <xsl:apply-templates select="*[position()=3]"/>
 918          </xsl:otherwise>
 919          </xsl:choose>
 920         </xsl:when>
 921         <xsl:otherwise>
 922          <xsl:apply-templates select="*[position()=3]"/>
 923         </xsl:otherwise>
 924         </xsl:choose>
 925         <xsl:if test="$nopar=0">
 926          <m:mo stretchy="false">)</m:mo>
 927         </xsl:if>
 928        </xsl:otherwise>
 929        </xsl:choose>
 930       </xsl:when>
 931       <!-- TYPE_OF -->
 932       <xsl:when test="$name='type_of'">
 933        <xsl:choose>
 934        <xsl:when test="$charlength >= $framewidth">
 935         <m:mtable align="baseline 1" equalrows="false" columnalign="left">
 936          <m:mtr>
 937           <m:mtd>
 938            <m:mrow>
 939             <xsl:value-of select="*[2]"/>
 940             <m:mo>:</m:mo>
 941            </m:mrow>
 942           </m:mtd>
 943          </m:mtr>
 944          <m:mtr>
 945           <m:mtd>
 946            <m:mrow>
 947             <xsl:apply-templates select="*[3]"/>
 948            </m:mrow>
 949           </m:mtd>
 950          </m:mtr>
 951         </m:mtable>
 952        </xsl:when>
 953        <xsl:otherwise>
 954         <m:mrow>
 955          <xsl:apply-templates select="*[2]"/>
 956          <m:mo>:</m:mo>
 957          <xsl:apply-templates select="*[3]"/>
 958         </m:mrow>
 959        </xsl:otherwise>
 960        </xsl:choose>
 961       </xsl:when>
 962       <!--PRODUCT -->
 963       <xsl:when test="$name='product'">
 964        <xsl:choose>
 965        <xsl:when test="$charlength >= $framewidth">
 966         <m:mtable align="baseline 1" equalrows="false" columnalign="left">
 967          <m:mtr>
 968           <m:mtd>
 969            <m:mrow>
 970             <m:mo mathcolor="Blue">&#931;</m:mo>
 971             <xsl:apply-templates select="m:bvar/m:ci"/>
 972             <m:mo>:</m:mo>
 973             <xsl:apply-templates select="m:bvar/m:type"/>
 974            </m:mrow>
 975           </m:mtd>
 976          </m:mtr>
 977          <m:mtr>
 978           <m:mtd>
 979            <m:mrow>
 980             <m:mtext>.</m:mtext>
 981             <xsl:apply-templates select="*[position()=3]"/>
 982            </m:mrow>
 983           </m:mtd>
 984          </m:mtr>
 985         </m:mtable>
 986        </xsl:when>
 987        <xsl:otherwise>
 988         <m:mrow>
 989          <m:mo mathcolor="Blue">&#931;</m:mo>
 990          <xsl:apply-templates select="m:bvar/m:ci"/>
 991          <m:mo>:</m:mo>
 992          <xsl:apply-templates select="m:bvar/m:type"/>
 993          <m:mtext>.</m:mtext>
 994          <xsl:apply-templates select="*[position()=3]"/>
 995         </m:mrow>
 996        </xsl:otherwise>
 997        </xsl:choose>
 998       </xsl:when>
 999       <!-- PROD_IND -->
1000       <xsl:when test="$name='product_ind'">
1001        <xsl:choose>
1002        <xsl:when test="$charlength >= $framewidth">
1003         <m:mtable align="baseline 1" equalrows="false" columnalign="left">
1004          <m:mtr>
1005           <m:mtd>
1006            <m:mrow>
1007             <m:mo stretchy="false">(</m:mo>
1008             <xsl:apply-templates select="m:type"/>
1009            </m:mrow>
1010           </m:mtd>
1011          </m:mtr>
1012          <m:mtr>
1013           <m:mtd>
1014            <m:mrow>
1015             <m:mo mathcolor="Blue">x</m:mo>
1016             <xsl:apply-templates select="*[position()=3]"/>
1017             <m:mo stretchy="false">)</m:mo>
1018            </m:mrow>
1019           </m:mtd>
1020          </m:mtr>
1021         </m:mtable>
1022        </xsl:when>
1023        <xsl:otherwise>
1024         <m:mrow>
1025          <m:mo stretchy="false">(</m:mo>
1026          <xsl:apply-templates select="m:type"/>
1027          <m:mo mathcolor="Blue">x</m:mo>
1028          <xsl:apply-templates select="*[position()=3]"/>
1029          <m:mo stretchy="false">)</m:mo>
1030         </m:mrow>
1031        </xsl:otherwise>
1032        </xsl:choose>
1033       </xsl:when>
1034       <!-- PAIR -->
1035       <xsl:when test="$name='pair'">
1036        <xsl:choose>
1037        <xsl:when test="$charlength >= $framewidth">
1038         <m:mtable align="baseline 1" equalrows="false" columnalign="left">
1039          <m:mtr>
1040           <m:mtd>
1041            <m:mrow>
1042             <m:mo mathcolor="Blue">&lt;</m:mo>
1043             <xsl:apply-templates select="*[2]"/>
1044             <m:mtext>, </m:mtext>
1045            </m:mrow>
1046           </m:mtd>
1047          </m:mtr>
1048          <m:mtr>
1049           <m:mtd>
1050            <m:mrow>
1051             <xsl:apply-templates select="*[3]"/>
1052             <m:mo mathcolor="Blue">&gt;</m:mo>
1053            </m:mrow>
1054           </m:mtd>
1055          </m:mtr>
1056         </m:mtable>
1057        </xsl:when>
1058        <xsl:otherwise>
1059         <m:mrow>
1060          <m:mo mathcolor="Blue">&lt;</m:mo>
1061          <xsl:apply-templates select="*[2]"/>
1062          <m:mtext>, </m:mtext>
1063          <xsl:apply-templates select="*[3]"/>
1064          <m:mo mathcolor="Blue">&gt;</m:mo>
1065         </m:mrow>
1066        </xsl:otherwise>
1067        </xsl:choose>
1068       </xsl:when>
1069       <!-- UNION -->
1070       <xsl:when test="$name='union'">
1071        <xsl:choose>
1072        <xsl:when test="$charlength >= $framewidth">
1073         <m:mtable align="baseline 1" equalrows="false" columnalign="left">
1074          <m:mtr>
1075           <m:mtd>
1076            <xsl:apply-templates select="*[2]"/>
1077           </m:mtd>
1078          </m:mtr>
1079          <m:mtr>
1080           <m:mtd>
1081            <m:mrow>
1082             <m:mo mathcolor="Blue">+</m:mo>
1083             <xsl:apply-templates select="*[3]"/>
1084            </m:mrow>
1085           </m:mtd>
1086          </m:mtr>
1087         </m:mtable>
1088        </xsl:when>
1089        <xsl:otherwise>
1090         <m:mrow>
1091          <xsl:apply-templates select="*[2]"/>
1092          <m:mo mathcolor="Blue">+</m:mo>
1093          <xsl:apply-templates select="*[3]"/>
1094         </m:mrow>
1095        </xsl:otherwise>
1096        </xsl:choose>
1097       </xsl:when>
1098       <!-- INL -->
1099       <xsl:when test="$name='inl'">
1100        <m:mrow>
1101         <m:mo stretchy="false" mathcolor="Blue">inl(</m:mo>
1102         <xsl:apply-templates select="*[position()=2]"/>
1103         <m:mo stretchy="false" mathcolor="Blue">)</m:mo>
1104        </m:mrow>
1105       </xsl:when>
1106       <!-- INR -->
1107       <xsl:when test="$name='inr'">
1108        <m:mrow>
1109         <m:mo stretchy="false" mathcolor="Blue">inr(</m:mo>
1110         <xsl:apply-templates select="*[position()=2]"/>
1111         <m:mo stretchy="false" mathcolor="Blue">)</m:mo>
1112        </m:mrow>
1113       </xsl:when>
1114       <!-- AXIOM -->
1115       <xsl:when test="$name='Ax'">
1116        <m:mo mathcolor="Blue">Ax</m:mo>
1117       </xsl:when>
1118       <!-- VOID -->
1119       <xsl:when test="$name='void'">
1120        <m:mo mathcolor="Blue">Void</m:mo>
1121       </xsl:when>
1122       <!-- ATOM -->
1123       <xsl:when test="$name='atom'">
1124        <m:mo mathcolor="Blue">Atom</m:mo>
1125       </xsl:when>
1126       <!-- UNIVERSE -->
1127       <xsl:when test="$name='universe'">
1128        <m:msub>
1129         <m:mo>U</m:mo>
1130         <xsl:apply-templates select="m:cn"/>
1131        </m:msub>
1132       </xsl:when>
1133       <!-- PROP -->
1134       <xsl:when test="$name='prop'">
1135        <m:msub>
1136         <m:mo>P</m:mo>
1137          <xsl:apply-templates select="m:cn"/>
1138        </m:msub>
1139       </xsl:when>
1140       <!-- EQUAL -->
1141       <xsl:when test="$name='equal'">
1142        <xsl:choose>
1143        <xsl:when test="$charlength >= $framewidth">
1144         <m:mtable align="baseline 1" equalrows="false" columnalign="left">
1145          <m:mtr>
1146           <m:mtd>
1147           <xsl:apply-templates select="*[position()=3]"/>
1148           </m:mtd>
1149          </m:mtr>
1150          <m:mtr>
1151           <m:mtd>
1152            <m:mrow>
1153             <m:mo mathcolor="Blue">=</m:mo>
1154             <xsl:apply-templates select="*[position()=4]"/>
1155            </m:mrow>
1156           </m:mtd>
1157          </m:mtr>
1158          <m:mtr>
1159           <m:mtd>
1160            <m:mrow>
1161             <m:mo mathcolor="Blue">&#x02208;</m:mo>
1162             <xsl:apply-templates select="*[position()=2]"/>
1163            </m:mrow>
1164          </m:mtd>
1165         </m:mtr>
1166        </m:mtable>
1167       </xsl:when>
1168       <xsl:otherwise>
1169        <m:mrow>
1170         <xsl:apply-templates select="*[position()=3]"/>
1171         <m:mo mathcolor="Blue">=</m:mo>
1172         <xsl:apply-templates select="*[position()=4]"/>
1173         <m:mo mathcolor="Blue">&#x02208;</m:mo>
1174         <xsl:apply-templates select="*[position()=2]"/>
1175        </m:mrow>
1176       </xsl:otherwise>
1177      </xsl:choose>
1178     </xsl:when>
1179     <!-- TOKEN  -->
1180     <xsl:when test="$name='token'">
1181      <m:mrow>
1182       <m:mo mathcolor="Blue">"</m:mo>
1183       <xsl:apply-templates select="m:ci"/>
1184       <m:mo mathcolor="Blue">"</m:mo>
1185      </m:mrow>
1186     </xsl:when>
1187     <!-- NIL  -->
1188     <xsl:when test="$name='nil'">
1189      <m:mo mathcolor="Blue">[]</m:mo>
1190     </xsl:when>
1191     <!-- CONS -->
1192     <xsl:when test="$name='cons'">
1193      <xsl:choose>
1194      <xsl:when test="$charlength >= $framewidth">
1195       <m:mtable align="baseline 1" equalrows="false" columnalign="left">
1196        <m:mtr>
1197         <m:mtd>
1198          <xsl:apply-templates select="*[2]"/>
1199         </m:mtd>
1200       </m:mtr>
1201       <m:mtr>
1202        <m:mtd>
1203         <m:mrow>
1204          <m:mo mathcolor="Blue">::</m:mo>
1205          <xsl:apply-templates select="*[3]"/>
1206         </m:mrow>
1207        </m:mtd>
1208       </m:mtr>
1209      </m:mtable>
1210     </xsl:when>
1211     <xsl:otherwise>
1212      <m:mrow>
1213       <xsl:apply-templates select="*[2]"/>
1214       <m:mo mathcolor="Blue">::</m:mo>
1215       <xsl:apply-templates select="*[3]"/>
1216      </m:mrow>
1217     </xsl:otherwise>
1218    </xsl:choose>
1219   </xsl:when>
1220
1221 <!-- REC -->
1222 <xsl:when test="$name='rec'">
1223 <xsl:choose>
1224 <xsl:when test="$charlength >= $framewidth">
1225 <m:mtable align="baseline 1" equalrows="false" columnalign="left">
1226  <m:mtr>
1227   <m:mtd>
1228    <m:mrow>
1229     <m:mo>rectype</m:mo>
1230     <xsl:apply-templates select="*[2]"/>
1231    </m:mrow>
1232   </m:mtd>
1233  </m:mtr>
1234  <m:mtr>
1235   <m:mtd>
1236    <m:mrow>
1237     <m:mo>=</m:mo>
1238     <xsl:apply-templates select="*[3]"/>
1239    </m:mrow>
1240   </m:mtd>
1241  </m:mtr>
1242 </m:mtable>
1243 </xsl:when>
1244 <xsl:otherwise>
1245 <m:mrow>
1246  <m:mo>rectype</m:mo>
1247  <xsl:apply-templates select="*[2]"/>
1248  <m:mo>=</m:mo>
1249  <xsl:apply-templates select="*[3]"/>
1250 </m:mrow>
1251 </xsl:otherwise>
1252 </xsl:choose>
1253 </xsl:when>
1254
1255 <!-- SET  -->
1256 <xsl:when test="$name='t_set'">
1257 <xsl:choose>
1258 <xsl:when test="$charlength >= $framewidth">
1259 <m:mtable align="baseline 1" equalrows="false" columnalign="left">
1260  <m:mtr>
1261   <m:mtd>
1262    <m:mrow>
1263     <m:mo mathcolor="Blue" stretchy="false">{</m:mo>
1264     <xsl:choose>
1265     <xsl:when test="m:bvar/m:ci">
1266      <xsl:apply-templates select="m:bvar/m:ci"/>
1267      <m:mo mathcolor="Blue">:</m:mo>
1268      <xsl:apply-templates select="m:bvar/m:type"/>
1269     </xsl:when>
1270     <xsl:otherwise>
1271      <xsl:apply-templates select="m:bvar/m:type"/>
1272     </xsl:otherwise>
1273     </xsl:choose>
1274    </m:mrow>
1275   </m:mtd>
1276  </m:mtr>
1277  <m:mtr>
1278   <m:mtd>
1279    <m:row>
1280     <m:mo mathcolor="Blue" stretchy="false">|</m:mo>
1281     <xsl:apply-templates select="*[3]"/>
1282     <m:mo mathcolor="Blue" stretchy="false">}</m:mo>
1283    </m:row>
1284   </m:mtd>
1285  </m:mtr>
1286 </m:mtable>
1287 </xsl:when>
1288 <xsl:otherwise>
1289 <m:row>
1290  <m:mo mathcolor="Blue" stretchy="false">{</m:mo>
1291  <xsl:choose>
1292  <xsl:when test="m:bvar/m:ci">
1293   <xsl:apply-templates select="m:bvar/m:ci"/>
1294   <m:mo mathcolor="Blue">:</m:mo>
1295   <xsl:apply-templates select="m:bvar/m:type"/>
1296  </xsl:when>
1297  <xsl:otherwise>
1298   <xsl:apply-templates select="m:bvar/m:type"/>
1299  </xsl:otherwise>
1300  </xsl:choose>
1301  <m:mo mathcolor="Blue" stretchy="false">|</m:mo>
1302  <xsl:apply-templates select="*[3]"/>
1303  <m:mo mathcolor="Blue" stretchy="false">}</m:mo>
1304 </m:row>
1305 </xsl:otherwise>
1306 </xsl:choose>
1307 </xsl:when>
1308
1309 <!-- ISECT -->
1310 <xsl:when test="$name='isect'">
1311 <xsl:choose>
1312 <xsl:when test="$charlength >= $framewidth">
1313 <m:mtable align="baseline 1" equalrows="false" columnalign="left">
1314  <m:mtr>
1315   <m:mtd>
1316    <m:mrow>
1317     <m:mo mathcolor="Blue">&#xc7;</m:mo>
1318     <xsl:apply-templates select="m:bvar/m:ci"/>
1319     <m:mo mathcolor="Blue">:</m:mo>
1320     <xsl:apply-templates select="m:bvar/m:type"/>
1321    </m:mrow>
1322   </m:mtd>
1323  </m:mtr>
1324  <m:mtr>
1325   <m:mtd>
1326    <m:mrow>
1327     <m:mo mathcolor="Blue">.</m:mo>
1328     <xsl:apply-templates select="*[3]"/>
1329    </m:mrow>
1330   </m:mtd>
1331  </m:mtr>
1332 </m:mtable>
1333 </xsl:when>
1334 <xsl:otherwise>
1335 <m:mrow>
1336  <m:mo mathcolor="Blue">&#xc7;</m:mo>
1337  <xsl:apply-templates select="m:bvar/m:ci"/>
1338  <m:mo mathcolor="Blue">:</m:mo>
1339  <xsl:apply-templates select="m:bvar/m:type"/>
1340  <m:mo mathcolor="Blue">.</m:mo>
1341  <xsl:apply-templates select="*[3]"/>
1342 </m:mrow>
1343 </xsl:otherwise>
1344 </xsl:choose>
1345 </xsl:when>
1346 <!-- QUOTIENT -->
1347 <xsl:when test="$name='quotient'">
1348 <xsl:choose>
1349 <xsl:when test="$charlength >= $framewidth">
1350 <m:mtable align="baseline 1" equalrows="false" columnalign="left">
1351  <m:mtr>
1352   <m:mtd>
1353    <m:mrow>
1354     <xsl:apply-templates select="m:bvar[1]"/>
1355     <m:mo mathcolor="Blue">,</m:mo>
1356     <xsl:apply-templates select="m:bvar[2]"/>
1357     <m:mo mathcolor="Blue">:</m:mo>
1358     <xsl:apply-templates select="*[2]"/>
1359    </m:mrow>
1360   </m:mtd>
1361  </m:mtr>
1362  <m:mtr>
1363   <m:mtd>
1364    <m:mrow>
1365     <m:mo mathcolor="Blue">//</m:mo>
1366     <xsl:apply-templates select="*[5]"/>
1367    </m:mrow>
1368   </m:mtd>
1369  </m:mtr>
1370 </m:mtable>
1371 </xsl:when>
1372 <xsl:otherwise>
1373 <m:mrow>
1374  <xsl:apply-templates select="m:bvar[1]"/>
1375  <m:mo mathcolor="Blue">,</m:mo>
1376  <xsl:apply-templates select="m:bvar[2]"/>
1377  <m:mo mathcolor="Blue">:</m:mo>
1378  <xsl:apply-templates select="*[2]"/>
1379  <m:mo mathcolor="Blue">//</m:mo>
1380  <xsl:apply-templates select="*[5]"/>
1381 </m:mrow>
1382 </xsl:otherwise>
1383 </xsl:choose>
1384 </xsl:when>
1385 <!-- IF_THEN_ELSE -->
1386 <xsl:when test="$name='if_then_else'">
1387 <xsl:choose>
1388 <xsl:when test="$charlength >= $framewidth">
1389 <m:mtable align="baseline 1" equalrows="false" columnalign="left">
1390  <m:mtr>
1391   <m:mtd>
1392   <m:mrow>
1393    <xsl:choose>
1394    <xsl:when test="m:where = 'atom_eq'">
1395     <m:mo stretchy="false" mathcolor="Blue">atom_eq (</m:mo>
1396    </xsl:when>
1397    <xsl:when test="m:where = 'int_eq'">
1398     <m:mo stretchy="false" mathcolor="Blue">int_eq (</m:mo>
1399    </xsl:when>
1400    <xsl:when test="m:where = 'less'">
1401     <m:mo stretchy="false" mathcolor="Blue">less (</m:mo>
1402    </xsl:when>
1403    </xsl:choose>
1404    <xsl:apply-templates select="*[3]"/>
1405    <m:mo mathcolor="Blue">;</m:mo>
1406    </m:mrow>
1407   </m:mtd>
1408  </m:mtr>
1409  <m:mtr>
1410   <m:mtd>
1411    <m:mrow>
1412     <xsl:apply-templates select="*[4]"/>
1413     <m:mo mathcolor="Blue">;</m:mo>
1414    </m:mrow>
1415   </m:mtd>
1416  </m:mtr>
1417  <m:mtr>
1418   <m:mtd>
1419    <m:mrow>
1420     <xsl:apply-templates select="*[5]"/>
1421     <m:mo mathcolor="Blue">;</m:mo>
1422    </m:mrow>
1423   </m:mtd>
1424  </m:mtr>
1425  <m:mtr>
1426   <m:mtd>
1427    <m:mrow>
1428     <xsl:apply-templates select="*[6]"/>
1429     <m:mo stretchy="false" mathcolor="Blue">)</m:mo>
1430    </m:mrow>
1431   </m:mtd>
1432  </m:mtr>
1433 </m:mtable>
1434 </xsl:when>
1435 <xsl:otherwise>
1436 <m:mrow>
1437  <xsl:choose>
1438  <xsl:when test="m:where = 'atom_eq'">
1439   <m:mo stretchy="false" mathcolor="Blue">atom_eq (</m:mo>
1440  </xsl:when>
1441  <xsl:when test="m:where = 'int_eq'">
1442   <m:mo stretchy="false" mathcolor="Blue">int_eq (</m:mo>
1443  </xsl:when>
1444  <xsl:when test="m:where = 'less'">
1445   <m:mo stretchy="false" mathcolor="Blue">less (</m:mo>
1446  </xsl:when>
1447  </xsl:choose>
1448  <xsl:apply-templates select="*[3]"/>
1449  <m:mo mathcolor="Blue">;</m:mo>
1450  <xsl:apply-templates select="*[4]"/>
1451  <m:mo mathcolor="Blue">;</m:mo>
1452  <xsl:apply-templates select="*[5]"/>
1453  <m:mo mathcolor="Blue">;</m:mo>
1454  <xsl:apply-templates select="*[6]"/>
1455  <m:mo stretchy="false" mathcolor="Blue">)</m:mo>
1456 </m:mrow>
1457 </xsl:otherwise>
1458 </xsl:choose>
1459 </xsl:when>
1460 <!-- SO_LAMBDA -->
1461 <xsl:when test="$name='so_lambda'">
1462 <xsl:choose>
1463 <xsl:when test="($charlength - 4) >= $framewidth">
1464 <m:mtable align="baseline 1" equalrows="false" columnalign="left">
1465  <m:mtr>
1466   <m:mtd>
1467    <m:mrow>
1468     <m:mo mathcolor="red">&#x03bb;</m:mo>
1469     <xsl:apply-templates select="m:apply[1]/*[2]"/>
1470    </m:mrow>
1471   </m:mtd>
1472  </m:mtr>
1473  <m:mtr>
1474   <m:mtd>
1475    <m:mrow>
1476     <m:mo>.</m:mo>
1477     <xsl:apply-templates select="*[3]"/>
1478    </m:mrow>
1479   </m:mtd>
1480  </m:mtr>
1481 </m:mtable>
1482 </xsl:when>
1483 <xsl:otherwise>
1484 <m:mrow>
1485  <m:mo mathcolor="red">&#x03bb;</m:mo>
1486  <xsl:apply-templates select="m:apply[1]/m:ci[2]"/>
1487  <m:mo>.</m:mo>
1488  <xsl:apply-templates select="*[3]"/>
1489 </m:mrow>
1490 </xsl:otherwise>
1491 </xsl:choose>
1492 </xsl:when>
1493 <!-- SO_APPLY -->
1494 <xsl:when test="$name='so_apply'">
1495 <xsl:choose>
1496 <xsl:when test="($charlength - 4) >= $framewidth">
1497 <m:mtable align="baseline 1" equalrows="false" columnalign="left">
1498  <m:mtr>
1499   <m:mtd>
1500    <m:mrow>
1501     <m:mo stretchy="false">(</m:mo>
1502     <xsl:apply-templates select="*[position()=2]">
1503      <xsl:with-param name="IN_PREC" select="$FUNCTION_PREC"/>
1504     </xsl:apply-templates>
1505    </m:mrow>
1506   </m:mtd>
1507  </m:mtr>
1508  <xsl:for-each select="*[position()>2]">
1509  <m:mtr>
1510   <m:mtd>
1511    <m:mrow>
1512     <m:mphantom stretchy="false"><m:mtext>(</m:mtext></m:mphantom>
1513     <xsl:apply-templates select=".">
1514      <xsl:with-param name="IN_PREC" select="$FUNCTION_PREC"/>
1515     </xsl:apply-templates>
1516    </m:mrow>
1517   </m:mtd>
1518  </m:mtr>
1519  </xsl:for-each>
1520  <m:mtr>
1521   <m:mtd>
1522    <m:mrow>
1523     <m:mo stretchy="false">)</m:mo>
1524    </m:mrow>
1525   </m:mtd>
1526  </m:mtr>
1527 </m:mtable>
1528 </xsl:when>
1529 <xsl:otherwise>
1530 <m:mo stretchy="false">(</m:mo>
1531 <xsl:apply-templates select="*[position()=2]">
1532  <xsl:with-param name="IN_PREC" select="$FUNCTION_PREC"/>
1533 </xsl:apply-templates>
1534 <xsl:for-each select="*[position()>2]">
1535  <m:mphantom><m:mtext>_</m:mtext></m:mphantom>
1536  <xsl:apply-templates select=".">
1537   <xsl:with-param name="IN_PREC" select="$FUNCTION_PREC"/>
1538  </xsl:apply-templates>
1539 </xsl:for-each>
1540 <m:mo stretchy="false">)</m:mo>
1541 </xsl:otherwise>
1542 </xsl:choose>
1543 </xsl:when>
1544 <!-- CAST -->
1545 <xsl:when test="$name='cast'">
1546 <xsl:choose>
1547 <xsl:when test="$charlength >= $framewidth">
1548 <m:mtable align="baseline 1" equalrows="false" columnalign="left">
1549  <m:mtr>
1550   <m:mtd>
1551    <m:mrow>
1552     <m:mo stretchy="false">(</m:mo>
1553     <xsl:apply-templates select="*[position()=2]"/>
1554    </m:mrow>
1555   </m:mtd>
1556  </m:mtr>
1557  <m:mtr>
1558   <m:mtd>
1559    <m:mrow>
1560             <m:mo mathcolor="Maroon">:></m:mo>
1561             <xsl:apply-templates select="*[position()=3]"/>
1562            </m:mrow>
1563           </m:mtd>
1564          </m:mtr>
1565          <m:mtr>
1566           <m:mtd>
1567            <m:mrow>
1568             <m:mo stretchy="false">)</m:mo>
1569            </m:mrow>
1570           </m:mtd>
1571          </m:mtr>
1572         </m:mtable>
1573        </xsl:when>
1574        <xsl:otherwise>
1575         <m:mo stretchy="false">(</m:mo>
1576         <xsl:apply-templates select="*[position()=2]"/>
1577         <m:mo mathcolor="Maroon">:></m:mo>
1578         <xsl:apply-templates select="*[position()=3]"/>
1579         <m:mo stretchy="false">)</m:mo>
1580        </xsl:otherwise>
1581        </xsl:choose>
1582       </xsl:when>
1583       <!-- APP *-->
1584       <xsl:when test="$name='app'">
1585        <xsl:choose>
1586        <xsl:when test="$charlength >= $framewidth">
1587         <m:mtable align="baseline 1" equalrows="false" columnalign="left">
1588          <m:mtr>
1589           <m:mtd>
1590            <m:mrow>
1591             <m:mo stretchy="false">(</m:mo>
1592 <!-- added precedence to app = FUNCTION_PREC (99) -->
1593             <xsl:apply-templates select="*[position()=2]">
1594              <xsl:with-param name="IN_PREC" select="$FUNCTION_PREC"/>
1595             </xsl:apply-templates>
1596            </m:mrow>
1597           </m:mtd>
1598          </m:mtr>
1599          <xsl:for-each select="*[position()>2]">
1600          <m:mtr>
1601           <m:mtd>
1602            <m:mrow>
1603             <m:mphantom><m:mtext>(</m:mtext></m:mphantom>
1604 <!-- added precedence to app = FUNCTION_PREC (99) -->
1605             <xsl:apply-templates select=".">
1606              <xsl:with-param name="IN_PREC" select="$FUNCTION_PREC"/>
1607             </xsl:apply-templates>
1608            </m:mrow>
1609           </m:mtd>
1610          </m:mtr>
1611          </xsl:for-each>
1612          <m:mtr>
1613           <m:mtd>
1614            <m:mrow>
1615             <m:mo stretchy="false">)</m:mo>
1616            </m:mrow>
1617           </m:mtd>
1618          </m:mtr>
1619         </m:mtable>
1620        </xsl:when>
1621        <xsl:otherwise>
1622         <m:mo stretchy="false">(</m:mo>
1623 <!-- added precedence to app = FUNCTION_PREC (99) -->
1624         <xsl:apply-templates select="*[position()=2]">
1625          <xsl:with-param name="IN_PREC" select="$FUNCTION_PREC"/>
1626         </xsl:apply-templates>
1627         <xsl:for-each select="*[position()>2]">
1628          <m:mphantom><m:mtext>_</m:mtext></m:mphantom>
1629 <!-- added precedence to app = FUNCTION_PREC (99) -->
1630          <xsl:apply-templates select=".">
1631           <xsl:with-param name="IN_PREC" select="$FUNCTION_PREC"/>
1632          </xsl:apply-templates>
1633         </xsl:for-each>
1634         <m:mo stretchy="false">)</m:mo>
1635        </xsl:otherwise>
1636        </xsl:choose>
1637       </xsl:when>
1638       <!-- CAST -->
1639       <xsl:when test="$name='cast'">
1640        <xsl:choose>
1641        <xsl:when test="$charlength >= $framewidth">
1642         <m:mtable align="baseline 1" equalrows="false" columnalign="left">
1643          <m:mtr>
1644           <m:mtd>
1645            <m:mrow>
1646             <m:mo stretchy="false">(</m:mo>
1647             <xsl:apply-templates select="*[position()=2]"/>
1648            </m:mrow>
1649           </m:mtd>
1650          </m:mtr>
1651          <m:mtr>
1652           <m:mtd>
1653            <m:mrow>
1654             <m:mo mathcolor="Maroon">:></m:mo>
1655             <xsl:apply-templates select="*[position()=3]"/>
1656            </m:mrow>
1657           </m:mtd>
1658          </m:mtr>
1659          <m:mtr>
1660           <m:mtd>
1661            <m:mrow>
1662             <m:mo stretchy="false">)</m:mo>
1663            </m:mrow>
1664           </m:mtd>
1665          </m:mtr>
1666         </m:mtable>
1667        </xsl:when>
1668        <xsl:otherwise>
1669         <m:mo stretchy="false">(</m:mo>
1670         <xsl:apply-templates select="*[position()=2]"/>
1671         <m:mo mathcolor="Maroon">:></m:mo>
1672         <xsl:apply-templates select="*[position()=3]"/>
1673         <m:mo stretchy="false">)</m:mo>
1674        </xsl:otherwise>
1675        </xsl:choose>
1676       </xsl:when>
1677       <!-- PROP -->
1678       <!--<xsl:when test="$name='Prop'">
1679        <m:mo>Prop</m:mo>
1680       </xsl:when>-->
1681       <!-- SET -->
1682       <!--<xsl:when test="$name='Set'">
1683        <m:mo>Set</m:mo>
1684       </xsl:when>-->
1685       <!-- TYPE -->
1686       <!--<xsl:when test="$name='Type'">
1687        <m:mo>Type</m:mo>
1688       </xsl:when>-->
1689       <!-- MUTCASE -->
1690       <xsl:when test="$name='mutcase'">
1691        <xsl:choose>
1692        <xsl:when test="$charlength >= $framewidth">
1693         <xsl:variable name="charlength"><xsl:apply-templates select="*[position()=2]" mode="charcount"><xsl:with-param name="nosibling" select="1"/></xsl:apply-templates></xsl:variable>
1694         <m:mtable align="baseline 1" equalrows="false" columnalign="left">
1695          <m:mtr>
1696           <m:mtd>
1697            <m:mrow>
1698             <m:mo>&lt;</m:mo>
1699             <xsl:apply-templates select="*[position()=2]"/>
1700             <xsl:if test="$framewidth > $charlength">
1701              <m:mo>&gt;</m:mo>
1702              <m:mo>CASES</m:mo>
1703              <m:mphantom><m:mtext>_</m:mtext></m:mphantom>
1704              <xsl:apply-templates select="*[position()=3]"/>
1705             </xsl:if>
1706            </m:mrow>
1707           </m:mtd>
1708          </m:mtr>
1709          <xsl:if test="$charlength >= $framewidth">
1710          <m:mtr>
1711           <m:mtd>
1712            <m:mrow>
1713             <m:mo>&gt;</m:mo>
1714             <m:mo>CASES</m:mo>
1715             <m:mphantom><m:mtext>_</m:mtext></m:mphantom>
1716             <xsl:apply-templates select="*[position()=3]"/>
1717            </m:mrow>
1718           </m:mtd>
1719          </m:mtr>
1720          </xsl:if>
1721          <m:mtr>
1722           <m:mtd>
1723            <m:mrow>
1724             <m:mo>OF</m:mo>
1725            </m:mrow>
1726           </m:mtd>
1727          </m:mtr>
1728          <xsl:for-each select="m:piecewise/m:piece">
1729          <xsl:variable name="charlength"><xsl:apply-templates select="./*[2]" mode="charcount"><xsl:with-param name="nosibling" select="1"/></xsl:apply-templates></xsl:variable>
1730          <m:mtr>
1731           <m:mtd>
1732            <m:mrow>
1733             <xsl:choose>
1734             <xsl:when test="position() = 1">
1735               <m:mphantom><m:mtext>|</m:mtext></m:mphantom>
1736             </xsl:when>
1737             <xsl:otherwise>
1738              <m:mo stretchy="false">|</m:mo>
1739             </xsl:otherwise>
1740             </xsl:choose>
1741             <m:mphantom><m:mtext>_</m:mtext></m:mphantom>
1742             <xsl:apply-templates select="./*[2]"/>
1743             <xsl:if test="$framewidth > $charlength">
1744              <m:mo mathcolor="Green">&#x21d2;</m:mo>
1745              <xsl:apply-templates select="./*[1]"/>
1746             </xsl:if>
1747            </m:mrow>
1748           </m:mtd>
1749          </m:mtr>
1750          <xsl:if test="$charlength >= $framewidth">
1751          <m:mtr>
1752           <m:mtd>
1753            <m:mrow>
1754             <m:mphantom><m:mtext>|_</m:mtext></m:mphantom>
1755             <m:mo mathcolor="Green">&#x21d2;</m:mo>
1756             <xsl:apply-templates select="./*[1]"/>
1757            </m:mrow>
1758           </m:mtd>
1759          </m:mtr>
1760          </xsl:if>
1761         </xsl:for-each>
1762          <m:mtr>
1763           <m:mtd>
1764            <m:mrow>
1765             <m:mo>END</m:mo>
1766            </m:mrow>
1767           </m:mtd>
1768          </m:mtr>
1769         </m:mtable>
1770        </xsl:when>
1771        <xsl:otherwise>
1772         <m:mo>&lt;</m:mo><xsl:apply-templates select="*[position()=2]"/><m:mo>&gt;</m:mo>
1773         <m:mo>CASES</m:mo>
1774         <m:mphantom><m:mtext>_</m:mtext></m:mphantom>
1775         <xsl:apply-templates select="*[position()=3]"/>
1776         <m:mphantom><m:mtext>_</m:mtext></m:mphantom>
1777         <m:mo>OF</m:mo>
1778         <xsl:for-each select="m:piecewise/m:piece">
1779          <xsl:choose>
1780          <xsl:when test="position() != 1">
1781           <m:mo stretchy="false">|</m:mo>
1782          </xsl:when>
1783          </xsl:choose>
1784          <xsl:apply-templates select="./*[2]"/>
1785          <m:mo mathcolor="Green">&#x21d2;</m:mo>
1786          <xsl:apply-templates select="./*[1]"/>
1787         </xsl:for-each>
1788         <m:mphantom><m:mtext>_</m:mtext></m:mphantom>
1789         <m:mo>END</m:mo>
1790        </xsl:otherwise>
1791        </xsl:choose>
1792       </xsl:when>
1793       <!-- FIX -->
1794       <xsl:when test="$name='fix'">
1795        <xsl:choose>
1796        <xsl:when test="$charlength >= $framewidth">
1797         <m:mtable align="baseline 1" equalrows="false" columnalign="left">
1798          <m:mtr>
1799           <m:mtd>
1800            <m:mrow>
1801             <m:mo>FIX</m:mo>
1802             <m:mphantom><m:mtext>_</m:mtext></m:mphantom>
1803             <m:mi><xsl:value-of select="m:ci"/></m:mi>
1804             <m:mo stretchy="false">{</m:mo>
1805            </m:mrow>
1806           </m:mtd>
1807          </m:mtr>
1808          <m:mtr>
1809           <m:mtd>
1810            <m:mrow>
1811             <m:mphantom><m:mtext>__</m:mtext></m:mphantom>
1812             <m:mtable align="baseline 1" equalrows="false" columnalign="left">
1813             <xsl:for-each select="m:bvar">
1814              <xsl:variable name="charlength"><xsl:apply-templates select="m:type" mode="charcount"><xsl:with-param name="nosibling" select="1"/></xsl:apply-templates></xsl:variable>
1815              <m:mtr>
1816               <m:mtd>
1817                <m:mrow>
1818                 <m:mi><xsl:value-of select="m:ci"/></m:mi>
1819                 <m:mo>:</m:mo>
1820                 <xsl:if test="$framewidth > $charlength">
1821                  <xsl:apply-templates select="m:type"/>
1822                 </xsl:if>
1823                </m:mrow>
1824               </m:mtd>
1825              </m:mtr>
1826              <xsl:if test="$charlength >= $framewidth">
1827              <m:mtr>
1828               <m:mtd>
1829                <m:mrow>
1830                 <m:mphantom><m:mtext>:=</m:mtext></m:mphantom>
1831                 <xsl:apply-templates select="m:type"/>
1832                </m:mrow>
1833               </m:mtd>
1834              </m:mtr>
1835              </xsl:if>
1836              <m:mtr>
1837               <m:mtd>
1838                <m:mrow>
1839                 <m:mo>:=</m:mo>
1840                 <xsl:apply-templates select="following-sibling::*[position()=1]"/>
1841                </m:mrow>
1842               </m:mtd>
1843              </m:mtr>
1844             </xsl:for-each>
1845             </m:mtable>
1846            </m:mrow>
1847           </m:mtd>
1848          </m:mtr>
1849          <m:mtr>
1850           <m:mtd>
1851            <m:mrow>
1852             <m:mo stretchy="false">}</m:mo>
1853            </m:mrow>
1854           </m:mtd>
1855          </m:mtr>
1856         </m:mtable>
1857        </xsl:when>
1858        <xsl:otherwise>
1859         <m:mo>FIX</m:mo>
1860         <m:mi><xsl:value-of select="m:ci"/></m:mi>
1861         <m:mo stretchy="false">{</m:mo>
1862         <m:mtable align="baseline 1" equalrows="false" columnalign="left">
1863         <xsl:for-each select="m:bvar">
1864          <m:mtr>
1865           <m:mtd>
1866            <m:mrow>
1867             <m:mi><xsl:value-of select="m:ci"/></m:mi>
1868             <m:mo>:</m:mo>
1869             <xsl:apply-templates select="m:type"/>
1870             <m:mo>:=</m:mo>
1871             <xsl:apply-templates select="following-sibling::*[position() = 1]"/>
1872             <xsl:if test="position()=last()">
1873              <m:mo stretchy="false">}</m:mo>
1874             </xsl:if>
1875            </m:mrow>
1876           </m:mtd>
1877          </m:mtr>
1878          </xsl:for-each>
1879         </m:mtable>
1880        </xsl:otherwise>
1881        </xsl:choose>
1882       </xsl:when>
1883       <!-- COFIX -->
1884       <xsl:when test="$name='cofix'">
1885        <xsl:choose>
1886        <xsl:when test="$charlength >= $framewidth">
1887         <m:mtable align="baseline 1" equalrows="false" columnalign="left">
1888          <m:mtr>
1889           <m:mtd>
1890            <m:mrow>
1891             <m:mo>COFIX</m:mo>
1892             <m:mphantom><m:mtext>_</m:mtext></m:mphantom>
1893             <m:mi><xsl:value-of select="m:ci"/></m:mi>
1894             <m:mo stretchy="false">{</m:mo>
1895            </m:mrow>
1896           </m:mtd>
1897          </m:mtr>
1898          <m:mtr>
1899           <m:mtd>
1900            <m:mrow>
1901             <m:mphantom><m:mtext>__</m:mtext></m:mphantom>
1902             <m:mtable align="baseline 1" equalrows="false" columnalign="left">
1903             <xsl:for-each select="m:bvar">
1904              <xsl:variable name="charlength"><xsl:apply-templates select="m:type" mode="charcount"><xsl:with-param name="nosibling" select="1"/></xsl:apply-templates></xsl:variable>
1905              <m:mtr>
1906               <m:mtd>
1907                <m:mrow>
1908                 <m:mi><xsl:value-of select="m:ci"/></m:mi>
1909                 <m:mo>:</m:mo>
1910                 <xsl:if test="$framewidth > $charlength">
1911                  <xsl:apply-templates select="m:type"/>
1912                 </xsl:if>
1913                </m:mrow>
1914               </m:mtd>
1915              </m:mtr>
1916              <xsl:if test="$charlength >= $framewidth">
1917              <m:mtr>
1918               <m:mtd>
1919                <m:mrow>
1920                 <m:mphantom><m:mtext>:=</m:mtext></m:mphantom>
1921                 <xsl:apply-templates select="m:type"/>
1922                </m:mrow>
1923               </m:mtd>
1924              </m:mtr>
1925              </xsl:if>
1926              <m:mtr>
1927               <m:mtd>
1928                <m:mrow>
1929                 <m:mo>:=</m:mo>
1930                 <xsl:apply-templates select="following-sibling::*[position() = 1]"/>
1931                </m:mrow>
1932               </m:mtd>
1933              </m:mtr>
1934             </xsl:for-each>
1935             </m:mtable>
1936            </m:mrow>
1937           </m:mtd>
1938          </m:mtr>
1939          <m:mtr>
1940           <m:mtd>
1941            <m:mrow>
1942             <m:mo stretchy="false">}</m:mo>
1943            </m:mrow>
1944           </m:mtd>
1945          </m:mtr>
1946         </m:mtable>
1947        </xsl:when>
1948        <xsl:otherwise>
1949         <m:mo>COFIX</m:mo>
1950         <m:mi><xsl:value-of select="m:ci"/></m:mi>
1951         <m:mo stretchy="false">{</m:mo>
1952         <m:mtable align="baseline 1" equalrows="false" columnalign="left">
1953         <xsl:for-each select="m:bvar">
1954          <m:mtr>
1955           <m:mtd>
1956            <m:mrow>
1957             <m:mi><xsl:value-of select="m:ci"/></m:mi>
1958             <m:mo>:</m:mo>
1959             <xsl:apply-templates select="m:type"/>
1960             <m:mo>:=</m:mo>
1961             <xsl:apply-templates select="following-sibling::*[position() = 1]"/>
1962             <xsl:if test="position()=last()">
1963              <m:mo stretchy="false">}</m:mo>
1964             </xsl:if>
1965            </m:mrow>
1966           </m:mtd>
1967          </m:mtr>
1968          </xsl:for-each>
1969         </m:mtable>
1970        </xsl:otherwise>
1971        </xsl:choose>
1972       </xsl:when>
1973       <!-- ***************************************** -->
1974       <!-- *********** PROOF ELEMENTS ************** -->
1975       <!-- ***************************************** -->
1976       <!-- PROOF -->
1977       <xsl:when test="$name='proof'">
1978         <!-- CSC: $explodeall until the annotationHelper can handle mactions -->
1979         <xsl:variable name="test" select="(not($explodeall)) and
1980            (not(preceding-sibling::*[1]/text()='letin1')) and
1981            (not(preceding-sibling::*[1]/text()='rw_step')) and
1982            (not(name(..)='m:lambda'))"/>
1983         <xsl:variable name="hidden_details">
1984          <xsl:if test="$test">
1985           <!-- Details hided (default) -->
1986           <m:mtable align="baseline 1" equalrows="false" columnalign="left">
1987            <m:mtr>
1988             <m:mtd>
1989              <m:mrow>
1990               <m:mtext mathcolor="Red">We&#x00a0;can&#x00a0;prove</m:mtext>
1991               <m:mphantom><m:mtext>_</m:mtext></m:mphantom>
1992               <!-- the last child is either the expected type, if provided,-->
1993               <!-- or the synthesized type.                                -->
1994               <xsl:apply-templates select="*[position()=last()]"/>
1995               <m:mrow>
1996                <m:mphantom><m:mtext>_</m:mtext></m:mphantom>
1997                <m:mtext mathcolor="Green">(explain)</m:mtext>
1998               </m:mrow>
1999              </m:mrow>
2000             </m:mtd>
2001            </m:mtr>
2002           </m:mtable>
2003          </xsl:if>
2004         </xsl:variable>
2005         <xsl:variable name="shown_details">
2006          <!-- Show details -->
2007          <m:mtable align="baseline 1" equalrows="false" columnalign="left">
2008           <m:mtr>
2009            <m:mtd>
2010             <m:mrow>
2011              <xsl:apply-templates select="*[position()=2]"/>
2012             </m:mrow>
2013            </m:mtd>
2014           </m:mtr>
2015           <xsl:variable name="hidedetails">
2016             <m:mrow>
2017              <m:mphantom>
2018               <m:mtext>_</m:mtext>
2019              </m:mphantom>
2020              <xsl:if test="$test">
2021               <m:mtext mathcolor="Green">(hide&#x00a0;details)</m:mtext>
2022              </xsl:if>
2023             </m:mrow>
2024           </xsl:variable>
2025           <m:mtr>
2026            <m:mtd>
2027             <m:mrow>
2028              <m:mtext mathcolor="Red">we&#x00a0;proved</m:mtext>
2029              <m:mphantom><m:mtext>_</m:mtext></m:mphantom>
2030              <xsl:apply-templates select="*[position()=3]"/>
2031              <xsl:if test="not(*[4])">
2032               <xsl:copy-of select="$hidedetails"/>
2033              </xsl:if>
2034             </m:mrow>
2035            </m:mtd>
2036           </m:mtr>
2037           <xsl:if test="*[4]">
2038            <m:mtr>
2039             <m:mtd>
2040              <m:mrow>
2041               <m:mtext mathcolor="Red">that&#x00a0;is&#x00a0;equivalent&#x00a0;to</m:mtext>
2042               <m:mphantom><m:mtext>_</m:mtext></m:mphantom>
2043               <xsl:apply-templates select="*[position()=4]"/>
2044               <xsl:copy-of select="$hidedetails"/>
2045              </m:mrow>
2046             </m:mtd>
2047            </m:mtr>
2048           </xsl:if>
2049          </m:mtable>
2050         </xsl:variable>
2051         <xsl:choose>
2052          <xsl:when test="$test">
2053           <m:maction actiontype="toggle">
2054            <xsl:copy-of select="$hidden_details"/>
2055            <xsl:copy-of select="$shown_details"/>
2056           </m:maction>
2057          </xsl:when>
2058          <xsl:otherwise>
2059           <xsl:copy-of select="$shown_details"/>
2060          </xsl:otherwise>
2061         </xsl:choose>
2062       </xsl:when>
2063       <!-- SIDE_PROOF -->
2064       <xsl:when test="$name='side_proof'">
2065         <xsl:variable name="test" select="(not($explodeall))"/>
2066         <xsl:variable name="hidden_details">
2067          <xsl:if test="$test">
2068           <!-- Details hided (default) -->
2069           <m:mtable align="baseline 1" equalrows="false" columnalign="left">
2070            <m:mtr>
2071             <m:mtd>
2072              <m:mrow>
2073               <m:mtext mathcolor="Red">We&#x00a0;can&#x00a0;prove</m:mtext>
2074               <m:mphantom><m:mtext>_</m:mtext></m:mphantom>
2075               <!-- the last child is either the expected type, if provided,-->
2076               <!-- or the synthesized type.                                -->
2077               <xsl:apply-templates select="*[position()=last()]"/>
2078               <m:mrow>
2079                <m:mphantom><m:mtext>_</m:mtext></m:mphantom>
2080                <m:mtext mathcolor="Green">(explain)</m:mtext>
2081               </m:mrow>
2082              </m:mrow>
2083             </m:mtd>
2084            </m:mtr>
2085           </m:mtable>
2086          </xsl:if>
2087         </xsl:variable>
2088         <xsl:variable name="shown_details">
2089          <!-- Show details -->
2090          <m:mtable align="baseline 1" equalrows="false" columnalign="left">
2091           <m:mtr>
2092            <m:mtd>
2093             <m:mrow>
2094              <xsl:apply-templates select="*[position()=2]"/>
2095             </m:mrow>
2096            </m:mtd>
2097           </m:mtr>
2098           <xsl:variable name="hidedetails">
2099             <m:mrow>
2100              <m:mphantom>
2101               <m:mtext>_</m:mtext>
2102              </m:mphantom>
2103              <xsl:if test="$test">
2104               <m:mtext mathcolor="Green">(hide&#x00a0;details)</m:mtext>
2105              </xsl:if>
2106             </m:mrow>
2107           </xsl:variable>
2108           <m:mtr>
2109            <m:mtd>
2110             <m:mrow>
2111              <m:mtext mathcolor="Red">we&#x00a0;proved</m:mtext>
2112              <m:mphantom><m:mtext>_</m:mtext></m:mphantom>
2113              <xsl:apply-templates select="*[position()=3]"/>
2114              <xsl:if test="not(*[4])">
2115               <xsl:copy-of select="$hidedetails"/>
2116              </xsl:if>
2117             </m:mrow>
2118            </m:mtd>
2119           </m:mtr>
2120           <xsl:if test="*[4]">
2121            <m:mtr>
2122             <m:mtd>
2123              <m:mrow>
2124               <m:mtext mathcolor="Red">that&#x00a0;is&#x00a0;equivalent&#x00a0;to</m:mtext>
2125               <m:mphantom><m:mtext>_</m:mtext></m:mphantom>
2126               <xsl:apply-templates select="*[position()=4]"/>
2127               <xsl:copy-of select="$hidedetails"/>
2128              </m:mrow>
2129             </m:mtd>
2130            </m:mtr>
2131           </xsl:if>
2132          </m:mtable>
2133         </xsl:variable>
2134         <xsl:choose>
2135          <xsl:when test="$test">
2136           <m:maction actiontype="toggle">
2137            <xsl:copy-of select="$hidden_details"/>
2138            <xsl:copy-of select="$shown_details"/>
2139           </m:maction>
2140          </xsl:when>
2141          <xsl:otherwise>
2142           <xsl:copy-of select="$shown_details"/>
2143          </xsl:otherwise>
2144         </xsl:choose>
2145       </xsl:when>
2146       <!-- LETIN1 -->
2147       <xsl:when test="$name='letin1'">
2148         <m:mtable align="baseline 1" equalrows="false" columnalign="left">
2149          <m:mtr>
2150           <m:mtd>
2151            <m:mrow>
2152             <xsl:apply-templates select="*[position()=2]"/>
2153            </m:mrow>
2154           </m:mtd>
2155          </m:mtr>
2156          <m:mtr>
2157           <m:mtd>
2158            <m:mrow>
2159             <xsl:apply-templates select="*[position()=3]"/>
2160            </m:mrow>
2161           </m:mtd>
2162          </m:mtr>
2163         </m:mtable>
2164       </xsl:when>
2165       <xsl:when test="$name='by_induction'">
2166        <m:mtable align="baseline 1" equalrows="false" columnalign="left">
2167         <m:mtr>
2168          <m:mtd>
2169           <m:mrow>
2170            <m:mtext mathcolor="Red">We&#x00a0;prove</m:mtext>
2171            <m:mphantom><m:mtext>_</m:mtext></m:mphantom>
2172            <xsl:apply-templates select="../*[3]"/>
2173           </m:mrow>
2174          </m:mtd>
2175         </m:mtr>
2176         <m:mtr>
2177          <m:mtd>
2178           <m:mrow>
2179            <m:mtext mathcolor="Red">by&#x00a0;induction&#x00a0;on</m:mtext>
2180            <m:mphantom><m:mtext>_</m:mtext></m:mphantom>
2181            <xsl:apply-templates
2182             select="*[position()=last()]/*[position()=last()]"/>
2183           </m:mrow>
2184          </m:mtd>
2185         </m:mtr>
2186         <m:mtr>
2187          <m:mtd>
2188           <m:mrow>
2189            <m:mtable align="baseline 1" equalrows="false" columnalign="left">
2190             <xsl:for-each select="*[position()>3 and not(position()=last())]">
2191              <m:mtr>
2192               <m:mtd>
2193                <m:mrow>
2194                 <xsl:apply-templates select="."/>
2195                </m:mrow>
2196               </m:mtd>
2197              </m:mtr>
2198             </xsl:for-each>
2199            </m:mtable>
2200           </m:mrow>
2201          </m:mtd>
2202         </m:mtr>
2203        </m:mtable>
2204       </xsl:when>
2205       <!-- inductive_case -->
2206       <xsl:when test="$name='inductive_case'">
2207        <m:mtable align="baseline 1" equalrows="false" columnalign="left">
2208         <m:mtr>
2209          <m:mtd>
2210           <m:mrow>
2211            <m:mtext mathcolor="Red">Case</m:mtext>
2212            <m:mphantom><m:mtext>_</m:mtext></m:mphantom>
2213            <xsl:apply-templates select="*[2]"/>
2214           </m:mrow>
2215          </m:mtd>
2216         </m:mtr>
2217         <m:mtr>
2218          <m:mtd>
2219           <m:mrow>
2220            <m:mphantom><m:mtext>_</m:mtext></m:mphantom>
2221            <m:mtable align="baseline 1" equalrows="false" columnalign="left">
2222             <xsl:if test="*[3]/*[position()>1]">
2223              <m:mtr>
2224               <m:mtd>
2225                <m:mrow>
2226                 <m:mtext mathcolor="Red">By&#x00a0;induction&#x00a0;hypothesis,&#x00a0;we&#x00a0;have:</m:mtext>
2227                </m:mrow>
2228               </m:mtd>
2229              </m:mtr>
2230              <m:mtr>
2231               <m:mtd>
2232                <m:mrow>
2233                 <m:mphantom><m:mtext>_</m:mtext></m:mphantom>
2234                 <xsl:for-each select="*[3]/*[position()>1]">
2235                  <m:mo stretchy="false">(</m:mo>
2236                  <xsl:apply-templates select="m:ci"/>
2237                  <m:mo stretchy="false">) </m:mo>
2238                  <m:mphantom><m:mtext>_</m:mtext></m:mphantom>
2239                  <xsl:apply-templates select="m:type"/>
2240                 </xsl:for-each>
2241                </m:mrow>
2242               </m:mtd>
2243              </m:mtr>
2244             </xsl:if>
2245             <m:mtr>
2246              <m:mtd>
2247               <m:mrow>
2248                <xsl:apply-templates select="*[4]"/>
2249               </m:mrow>
2250              </m:mtd>
2251             </m:mtr>
2252            </m:mtable>
2253           </m:mrow>
2254          </m:mtd>
2255         </m:mtr>
2256        </m:mtable>
2257       </xsl:when>
2258       <!-- case_lhs  -->
2259       <xsl:when test="$name='case_lhs'">
2260        <m:mrow>
2261         <xsl:choose>
2262          <xsl:when test="count(*)=2">
2263           <xsl:apply-templates select="*[2]"/>
2264          </xsl:when>
2265          <xsl:otherwise>
2266           <m:mo stretchy="false">(</m:mo>
2267           <xsl:apply-templates select="*[2]"/>
2268           <xsl:for-each select="m:bvar">
2269            <m:mphantom><m:mtext>_</m:mtext></m:mphantom>
2270            <xsl:apply-templates select="*[1]"/>
2271            <m:mtext>:</m:mtext>
2272            <xsl:apply-templates select="m:type/*[1]"/>
2273           </xsl:for-each>
2274           <m:mo stretchy="false">)</m:mo>
2275          </xsl:otherwise>
2276         </xsl:choose>
2277        </m:mrow>
2278       </xsl:when>
2279       <!-- false_ind  -->
2280       <xsl:when test="$name='false_ind'">
2281        <m:mtable align="baseline 1" equalrows="false" columnalign="left">
2282         <m:mtr>
2283          <m:mtd>
2284           <m:mrow>
2285            <xsl:apply-templates select="*[3]"/>
2286           </m:mrow>
2287          </m:mtd>
2288         </m:mtr>
2289         <m:mtr>
2290          <m:mtd>
2291           <m:mrow>
2292            <m:mtext mathcolor="Red">Contradiction.</m:mtext>
2293           </m:mrow>
2294          </m:mtd>
2295         </m:mtr>
2296        </m:mtable>
2297       </xsl:when>
2298       <!-- LET-IN -->
2299       <xsl:when test="$name='letin'">
2300         <m:mtable align="baseline 1" equalrows="false" columnalign="left">
2301          <!-- <xsl:for-each select="APPLY[m:csymbol and (string(m:csymbol)='let')]"> -->
2302          <xsl:for-each select="*[(last() > position()) and (position()>1)]">
2303          <m:mtr>
2304           <m:mtd>
2305            <m:mrow>
2306             <xsl:apply-templates select="."/>
2307            </m:mrow>
2308           </m:mtd>
2309          </m:mtr>
2310          </xsl:for-each>
2311          <m:mtr>
2312           <m:mtd>
2313            <m:mrow>
2314             <xsl:apply-templates select="*[position()=last()]"/>
2315            </m:mrow>
2316           </m:mtd>
2317          </m:mtr>
2318         </m:mtable>
2319       </xsl:when>
2320       <!-- LET -->
2321       <xsl:when test="$name='let'">
2322        <m:mtext>(</m:mtext>
2323        <xsl:apply-templates select="m:ci"/>
2324        <m:mtext>) </m:mtext>
2325        <xsl:apply-templates select="*[3]"/>
2326       </xsl:when>
2327       <!-- RW_STEP -->
2328       <xsl:when test="$name='rw_step'">
2329         <m:mtable align="baseline 1" equalrows="false" columnalign="left">
2330          <m:mtr>
2331           <m:mtd>
2332            <m:mrow>
2333             <xsl:choose>
2334              <xsl:when test="name(*[2])='m:apply'">
2335               <xsl:apply-templates select="*[2]"/>
2336              </xsl:when>
2337              <xsl:otherwise>
2338               <m:mtext>Consider</m:mtext>
2339               <m:mphantom><m:mtext>_</m:mtext></m:mphantom>
2340               <xsl:apply-templates select="*[2]"/>
2341              </xsl:otherwise>
2342             </xsl:choose>
2343            </m:mrow>
2344           </m:mtd>
2345          </m:mtr>
2346          <m:mtr>
2347           <m:mtd>
2348            <m:mrow>
2349             <m:mtext>Rewrite</m:mtext>
2350             <m:mphantom><m:mtext>_</m:mtext></m:mphantom>
2351             <xsl:apply-templates select="*[3]"/>
2352             <m:mphantom><m:mtext>_</m:mtext></m:mphantom>
2353             <m:mtext>with</m:mtext>
2354             <m:mphantom><m:mtext>_</m:mtext></m:mphantom>
2355             <xsl:apply-templates select="*[4]"/>
2356             <m:mphantom><m:mtext>_</m:mtext></m:mphantom>
2357             <m:mtext>by</m:mtext>
2358             <m:mphantom><m:mtext>_</m:mtext></m:mphantom>
2359             <xsl:apply-templates select="*[5]"/>
2360            </m:mrow>
2361           </m:mtd>
2362          </m:mtr>
2363         </m:mtable>
2364       </xsl:when>
2365       <!-- not existing any more
2366       <xsl:when test="$name='thread'">
2367         <m:mtable align="baseline 1" equalrows="false" columnalign="left">
2368          <m:mtr>
2369           <m:mtd>
2370            <m:mrow>
2371             <xsl:choose>
2372              <xsl:when test="name(*[last()])='m:apply'">
2373               <xsl:apply-templates select="*[last()]"/>
2374              </xsl:when>
2375              <xsl:otherwise>
2376               <m:mtext>Consider</m:mtext>
2377               <m:mphantom><m:mtext>_</m:mtext></m:mphantom>
2378               <xsl:apply-templates select="*[last()]"/>
2379              </xsl:otherwise>
2380             </xsl:choose>
2381            </m:mrow>
2382           </m:mtd>
2383          </m:mtr>
2384          <xsl:apply-templates mode="thread" select="*[(last()-2)]"/>
2385         </m:mtable>
2386       </xsl:when>
2387       -->
2388       <!-- REWRITE_AND_APPLY -->
2389       <xsl:when test="$name='rewrite_and_apply'">
2390         <m:mtable align="baseline 1" equalrows="false" columnalign="left">
2391          <m:mtr>
2392           <m:mtd>
2393            <m:mrow>
2394             <xsl:apply-templates select="*[2]"/>
2395            </m:mrow>
2396           </m:mtd>
2397          </m:mtr>
2398          <m:mtr>
2399           <m:mtd>
2400            <m:mrow>
2401             <m:mtext>Then&#x00a0;apply&#x00a0;it&#x00a0;to</m:mtext>
2402             <m:mphantom><m:mtext>_</m:mtext></m:mphantom>
2403             <xsl:apply-templates select="*[position()>2]"/>
2404            </m:mrow>
2405           </m:mtd>
2406          </m:mtr>
2407        </m:mtable>
2408       </xsl:when>
2409       <!-- AND_IND -->
2410       <xsl:when test="$name='and_ind'">
2411         <m:mtable align="baseline 1" equalrows="false" columnalign="left">
2412          <m:mtr>
2413           <m:mtd>
2414            <m:mrow>
2415             <xsl:choose>
2416              <xsl:when test="name(*[2])='m:apply'">
2417               <xsl:apply-templates select="*[2]"/>
2418              </xsl:when>
2419              <xsl:otherwise>
2420               <m:mtext>Consider</m:mtext>
2421               <m:mphantom><m:mtext>_</m:mtext></m:mphantom>
2422               <xsl:apply-templates select="*[2]"/>
2423              </xsl:otherwise>
2424             </xsl:choose>
2425            </m:mrow>
2426           </m:mtd>
2427          </m:mtr>
2428          <m:mtr>
2429           <m:mtd>
2430            <m:mrow>
2431             <m:mtext>In&#x00a0;particular,&#x00a0;we&#x00a0;have</m:mtext>
2432            </m:mrow>
2433           </m:mtd>
2434          </m:mtr>
2435          <m:mtr>
2436           <m:mtd>
2437            <m:mrow>
2438             <m:mtext>(</m:mtext>
2439             <xsl:apply-templates select="*[3]"/>
2440             <m:mtext>)</m:mtext>
2441             <m:mphantom><m:mtext>_</m:mtext></m:mphantom>
2442             <xsl:apply-templates select="*[4]"/>
2443             </m:mrow>
2444           </m:mtd>
2445          </m:mtr>
2446          <m:mtr>
2447           <m:mtd>
2448            <m:mrow>
2449             <m:mtext>(</m:mtext>
2450             <xsl:apply-templates select="*[5]"/>
2451             <m:mtext>)</m:mtext>
2452             <m:mphantom><m:mtext>_</m:mtext></m:mphantom>
2453             <xsl:apply-templates select="*[6]"/>
2454             </m:mrow>
2455           </m:mtd>
2456          </m:mtr>
2457          <m:mtr>
2458           <m:mtd>
2459            <m:mrow>
2460             <xsl:apply-templates select="*[7]"/>
2461            </m:mrow>
2462           </m:mtd>
2463          </m:mtr>
2464         </m:mtable>
2465       </xsl:when>
2466       <!-- full_or_ind -->
2467       <xsl:when test="$name='full_or_ind'">
2468         <m:mtable align="baseline 1" equalrows="false" columnalign="left">
2469          <m:mtr>
2470           <m:mtd>
2471            <m:mrow>
2472             <xsl:choose>
2473              <xsl:when test="name(*[2])='m:apply'">
2474               <xsl:apply-templates select="*[2]"/>
2475              </xsl:when>
2476              <xsl:otherwise>
2477               <m:mtext>Consider</m:mtext>
2478               <m:mphantom><m:mtext>_</m:mtext></m:mphantom>
2479               <xsl:apply-templates select="*[2]"/>
2480              </xsl:otherwise>
2481             </xsl:choose>
2482            </m:mrow>
2483           </m:mtd>
2484          </m:mtr>
2485          <m:mtr>
2486           <m:mtd>
2487            <m:mrow>
2488             <m:mtext>We&#x00a0;proceed&#x00a0;by&#x00a0;cases&#x00a0;to&#x00a0;prove</m:mtext>
2489             <m:mphantom><m:mtext>_</m:mtext></m:mphantom>
2490             <xsl:apply-templates select="*[3]"/>
2491            </m:mrow>
2492           </m:mtd>
2493          </m:mtr>
2494          <m:mtr>
2495           <m:mtd>
2496            <m:mrow>
2497             <m:mtext>Left:&#x00a0;suppose</m:mtext>
2498             <m:mphantom><m:mtext>_</m:mtext></m:mphantom>
2499             <m:mo stretchy="false">(</m:mo>
2500             <xsl:apply-templates select="*[4]/m:bvar/m:ci"/>
2501             <m:mo stretchy="false">)</m:mo>
2502             <m:mphantom><m:mtext>_</m:mtext></m:mphantom>
2503             <xsl:apply-templates select="*[4]/m:bvar/m:type/*[1]"/>
2504            </m:mrow>
2505           </m:mtd>
2506          </m:mtr>
2507          <m:mtr>
2508           <m:mtd>
2509            <m:mrow>
2510             <m:mphantom><m:mtext>_</m:mtext></m:mphantom>
2511             <xsl:apply-templates select="*[4]/*[3]"/>
2512            </m:mrow>
2513           </m:mtd>
2514          </m:mtr>
2515          <m:mtr>
2516           <m:mtd>
2517            <m:mrow>
2518             <m:mtext>Right:&#x00a0;suppose</m:mtext>
2519             <m:mphantom><m:mtext>_</m:mtext></m:mphantom>
2520             <m:mo stretchy="false">(</m:mo>
2521             <xsl:apply-templates select="*[5]/m:bvar/m:ci"/>
2522             <m:mo stretchy="false">)</m:mo>
2523             <m:mphantom><m:mtext>_</m:mtext></m:mphantom>
2524             <xsl:apply-templates select="*[5]/m:bvar/m:type/*[1]"/>
2525            </m:mrow>
2526           </m:mtd>
2527          </m:mtr>
2528          <m:mtr>
2529           <m:mtd>
2530            <m:mrow>
2531             <xsl:apply-templates select="*[5]/*[3]"/>
2532            </m:mrow>
2533           </m:mtd>
2534          </m:mtr>
2535         </m:mtable>
2536       </xsl:when>
2537       <!-- OR_IND -->
2538       <xsl:when test="$name='or_ind'">
2539         <m:mtable align="baseline 1" equalrows="false" columnalign="left">
2540          <m:mtr>
2541           <m:mtd>
2542            <m:mrow>
2543             <xsl:choose>
2544              <xsl:when test="name(*[2])='m:apply'">
2545               <xsl:apply-templates select="*[2]"/>
2546              </xsl:when>
2547              <xsl:otherwise>
2548               <m:mtext>Consider</m:mtext>
2549               <m:mphantom><m:mtext>_</m:mtext></m:mphantom>
2550               <xsl:apply-templates select="*[2]"/>
2551              </xsl:otherwise>
2552             </xsl:choose>
2553            </m:mrow>
2554           </m:mtd>
2555          </m:mtr>
2556          <m:mtr>
2557           <m:mtd>
2558            <m:mrow>
2559             <m:mtext>We&#x00a0;prove</m:mtext>
2560             <m:mphantom><m:mtext>_</m:mtext></m:mphantom>
2561             <xsl:apply-templates select="*[3]"/>
2562             <m:mphantom><m:mtext>_</m:mtext></m:mphantom>
2563             <m:mtext>by&#x00a0;cases:</m:mtext>
2564            </m:mrow>
2565           </m:mtd>
2566          </m:mtr>
2567          <m:mtr>
2568           <m:mtd>
2569            <m:mrow>
2570             <m:mtext>Left</m:mtext>
2571             <xsl:apply-templates select="*[4]"/>
2572            </m:mrow>
2573           </m:mtd>
2574          </m:mtr>
2575          <m:mtr>
2576           <m:mtd>
2577            <m:mrow>
2578             <m:mtext>Right</m:mtext>
2579             <xsl:apply-templates select="*[5]"/>
2580            </m:mrow>
2581           </m:mtd>
2582          </m:mtr>
2583         </m:mtable>
2584       </xsl:when>
2585       <!-- EX_IND -->
2586       <xsl:when test="$name='ex_ind'">
2587         <m:mtable align="baseline 1" equalrows="false" columnalign="left">
2588          <m:mtr>
2589           <m:mtd>
2590            <m:mrow>
2591             <xsl:choose>
2592              <xsl:when test="name(*[2])='m:apply'">
2593               <xsl:apply-templates select="*[2]"/>
2594              </xsl:when>
2595              <xsl:otherwise>
2596               <m:mtext>Consider</m:mtext>
2597               <m:mphantom><m:mtext>_</m:mtext></m:mphantom>
2598               <xsl:apply-templates select="*[2]"/>
2599              </xsl:otherwise>
2600             </xsl:choose>
2601            </m:mrow>
2602           </m:mtd>
2603          </m:mtr>
2604          <m:mtr>
2605           <m:mtd>
2606            <m:mrow>
2607             <m:mtext>Let</m:mtext>
2608             <m:mphantom><m:mtext>_</m:mtext></m:mphantom>
2609             <xsl:apply-templates select="*[3]"/>
2610             <m:mtext>:</m:mtext>
2611             <xsl:apply-templates select="*[4]"/>
2612             <m:mphantom><m:mtext>_</m:mtext></m:mphantom>
2613             <m:mtext>such&#x00a0;that</m:mtext>
2614             <m:mphantom><m:mtext>_</m:mtext></m:mphantom>
2615             <m:mtext>(</m:mtext>
2616              <xsl:apply-templates select="*[5]"/>
2617             <m:mtext>)</m:mtext>
2618             <m:mphantom><m:mtext>_</m:mtext></m:mphantom>
2619             <xsl:apply-templates select="*[6]"/>
2620            </m:mrow>
2621           </m:mtd>
2622          </m:mtr>
2623          <m:mtr>
2624           <m:mtd>
2625            <m:mrow>
2626             <xsl:apply-templates select="*[7]"/>
2627            </m:mrow>
2628           </m:mtd>
2629          </m:mtr>
2630         </m:mtable>
2631       </xsl:when>
2632       <!-- EQ_CHAIN -->
2633       <xsl:when test="$name='eq_chain'">
2634        <m:mtable align="baseline 1" equalrows="false" columnalign="left">
2635         <m:mtr>
2636          <m:mtd>
2637           <m:mrow>
2638            <m:mtext mathcolor="Red">We&#x00a0;have&#x00a0;the&#x00a0;following&#x00a0;equality&#x00a0;chain:</m:mtext>
2639           </m:mrow>
2640          </m:mtd>
2641         </m:mtr>
2642         <xsl:for-each select="*[position() mod 2 = 0]">
2643         <xsl:variable name="pos" select="position()"/>
2644         <m:mtr>
2645          <m:mtd>
2646           <m:mrow>
2647            <xsl:choose>
2648            <xsl:when test="$pos = 1">
2649             <xsl:apply-templates select="."/>
2650             <m:mphantom><m:mtext>_</m:mtext></m:mphantom>
2651             <m:mo>=</m:mo>
2652            </xsl:when>
2653            <xsl:otherwise>
2654             <m:mo>=</m:mo>
2655             <m:mphantom><m:mtext>_</m:mtext></m:mphantom>
2656             <xsl:apply-templates select="."/>
2657            </xsl:otherwise>
2658            </xsl:choose>
2659           </m:mrow>
2660          </m:mtd>
2661         </m:mtr>
2662         <xsl:if test="$pos != last()">
2663         <m:mtr>
2664          <m:mtd>
2665           <m:mrow>
2666            <m:mphantom><m:mtext>__</m:mtext></m:mphantom>
2667            <xsl:apply-templates select="../*[position()=2*$pos +1]"/>
2668           </m:mrow>
2669          </m:mtd>
2670         </m:mtr>
2671         </xsl:if>
2672         </xsl:for-each>
2673        </m:mtable>
2674       </xsl:when>
2675       <!-- DISEQ_CHAIN -->
2676       <xsl:when test="$name='diseq_chain'">
2677        <m:mtable align="baseline 1" equalrows="false" columnalign="left">
2678         <m:mtr>
2679          <m:mtd>
2680           <m:mrow>
2681            <m:mtext mathcolor="Red">We&#x00a0;have&#x00a0;the&#x00a0;following&#x00a0;disequality&#x00a0;chain:</m:mtext>
2682           </m:mrow>
2683          </m:mtd>
2684         </m:mtr>
2685         <xsl:for-each select="*[position() mod 3 = 2]">
2686         <xsl:variable name="pos" select="position()"/>
2687         <m:mtr>
2688          <m:mtd>
2689           <m:mrow>
2690            <xsl:choose>
2691            <xsl:when test="$pos = 1">
2692             <xsl:apply-templates select="."/>
2693             <m:mphantom><m:mtext>_</m:mtext></m:mphantom>
2694             <mo><xsl:apply-templates select="../*[position()=3*$pos]"/></mo>
2695            </xsl:when>
2696            <xsl:otherwise>
2697             <mo><xsl:apply-templates select="../*[position()=3*($pos - 1)]"/></mo>
2698             <m:mphantom><m:mtext>_</m:mtext></m:mphantom>
2699             <xsl:apply-templates select="."/>
2700            </xsl:otherwise>
2701            </xsl:choose>
2702           </m:mrow>
2703          </m:mtd>
2704         </m:mtr>
2705         <xsl:if test="$pos != last()">
2706         <m:mtr>
2707          <m:mtd>
2708           <m:mrow>
2709            <m:mphantom><m:mtext>__</m:mtext></m:mphantom>
2710            <xsl:apply-templates select="../*[position()=3*$pos +1]"/>
2711           </m:mrow>
2712          </m:mtd>
2713         </m:mtr>
2714         </xsl:if>
2715         </xsl:for-each>
2716        </m:mtable>
2717       </xsl:when>
2718       <!-- ***************************************** -->
2719       <!-- *********** NOTATIONS ******************* -->
2720       <!-- ***************************************** -->
2721       <!-- subst -->
2722       <xsl:when test="$name='subst'">
2723         <xsl:apply-templates select="*[3]"/>
2724 <!-- no font for ApplyFunction: <m:mo>&#xe8a0;</m:mo> -->
2725         <m:mo stretchy="false">[</m:mo>
2726         <xsl:apply-templates select="*[4]"/>
2727         <m:mo mathcolor="Green">
2728          <xsl:if test="$id != ''">
2729           <xsl:attribute name="xref"><xsl:value-of select="$id"/></xsl:attribute>
2730          </xsl:if>&#8592;</m:mo>
2731         <xsl:apply-templates select="*[2]"/>
2732         <m:mo stretchy="false">]</m:mo>
2733       </xsl:when>
2734       <!-- lift -->
2735       <xsl:when test="$name='lift'">
2736         <m:msup>
2737          <m:mo mathcolor="Green">
2738           <xsl:if test="$id != ''">
2739            <xsl:attribute name="xref"><xsl:value-of select="$id"/></xsl:attribute>
2740           </xsl:if>&#8593;</m:mo>
2741          <xsl:apply-templates select="*[2]"/>
2742         </m:msup>
2743         <m:mrow>
2744          <m:mo stretchy="false">(</m:mo>
2745          <xsl:apply-templates select="*[3]"/>
2746          <m:mo stretchy="false">)</m:mo>
2747         </m:mrow>
2748       </xsl:when>
2749       <!-- lift_with_base -->
2750       <xsl:when test="$name='lift_with_base'">
2751         <m:msubsup>
2752          <m:mo mathcolor="Green">
2753           <xsl:if test="$id != ''">
2754            <xsl:attribute name="xref"><xsl:value-of select="$id"/></xsl:attribute>
2755           </xsl:if>&#8593;</m:mo>
2756          <xsl:apply-templates select="*[3]"/>
2757          <xsl:apply-templates select="*[4]"/>
2758         </m:msubsup>
2759         <m:mrow>
2760          <m:mo stretchy="false">(</m:mo>
2761          <xsl:apply-templates select="*[2]"/>
2762          <m:mo stretchy="false">)</m:mo>
2763         </m:mrow>
2764       </xsl:when>
2765       <!-- beta_red1 -->
2766       <xsl:when test="$name='beta_red1'">
2767         <xsl:apply-templates select="*[2]"/>
2768         <m:munder>
2769          <m:mo mathcolor="Green">
2770           <xsl:if test="$id != ''">
2771            <xsl:attribute name="xref"><xsl:value-of select="$id"/></xsl:attribute>
2772           </xsl:if>&#8594;</m:mo>
2773           <m:mi mathcolor="Green">&#946;</m:mi>
2774         </m:munder>
2775         <xsl:apply-templates select="*[3]"/>
2776       </xsl:when>
2777       <!-- beta_red -->
2778       <xsl:when test="$name='beta_red'">
2779         <xsl:apply-templates select="*[2]"/>
2780         <m:munderover>
2781          <m:mo mathcolor="Green">
2782           <xsl:if test="$id != ''">
2783            <xsl:attribute name="xref"><xsl:value-of select="$id"/></xsl:attribute>
2784           </xsl:if>&#8594;</m:mo>
2785           <m:mi mathcolor="Green">&#946;</m:mi>
2786           <m:mi mathcolor="Green">*</m:mi>
2787         </m:munderover>
2788         <xsl:apply-templates select="*[3]"/>
2789       </xsl:when>
2790       <!-- par_beta_red1 -->
2791       <xsl:when test="$name='par_beta_red1'">
2792         <xsl:apply-templates select="*[2]"/>
2793         <m:munder>
2794          <m:mo mathcolor="Green">
2795           <xsl:if test="$id != ''">
2796            <xsl:attribute name="xref"><xsl:value-of select="$id"/></xsl:attribute>
2797           </xsl:if>&#8658;</m:mo>
2798           <m:mi mathcolor="Green">&#946;</m:mi>
2799         </m:munder>
2800         <xsl:apply-templates select="*[3]"/>
2801       </xsl:when>
2802       <!-- par_beta_red -->
2803       <xsl:when test="$name='par_beta_red'">
2804         <xsl:apply-templates select="*[2]"/>
2805         <m:munderover>
2806          <m:mo mathcolor="Green">
2807           <xsl:if test="$id != ''">
2808            <xsl:attribute name="xref"><xsl:value-of select="$id"/></xsl:attribute>
2809           </xsl:if>&#8658;</m:mo>
2810           <m:mi mathcolor="Green">&#946;</m:mi>
2811           <m:mi mathcolor="Green">*</m:mi>
2812         </m:munderover>
2813         <xsl:apply-templates select="*[3]"/>
2814       </xsl:when>
2815       <!-- forgetful -->
2816       <xsl:when test="$name='forgetful'">
2817        <m:mfenced open="|" close="|">
2818         <xsl:if test="$id != ''">
2819          <xsl:attribute name="xref"><xsl:value-of select="$id"/></xsl:attribute>
2820         </xsl:if>
2821         <xsl:apply-templates select="*[2]"/>
2822        </m:mfenced>
2823       </xsl:when>
2824       <!-- isomorphic -->
2825       <xsl:when test="$name='isomorphic'">
2826         <xsl:apply-templates select="*[2]"/>
2827         <m:mo mathcolor="Green">
2828          <xsl:if test="$id != ''">
2829           <xsl:attribute name="xref"><xsl:value-of select="$id"/></xsl:attribute>
2830          </xsl:if>&#8773;</m:mo>
2831         <xsl:apply-templates select="*[3]"/>
2832       </xsl:when>
2833       <!-- interp -->
2834       <xsl:when test="$name='forgetful'">
2835        <m:mfenced open="[" close="]">
2836         <xsl:if test="$id != ''">
2837          <xsl:attribute name="xref"><xsl:value-of select="$id"/></xsl:attribute>
2838         </xsl:if>
2839         <xsl:apply-templates select="*[2]"/>
2840        </m:mfenced>
2841       </xsl:when>
2842
2843       <!-- ERROR -->
2844       <xsl:otherwise>
2845        <m:mi>ERROR</m:mi>
2846       </xsl:otherwise>
2847      </xsl:choose>
2848     </m:mrow>
2849 </xsl:template>
2850
2851 <!-- Il modo Thread non esiste piu'
2852 <xsl:template match="*" mode="thread">
2853  <xsl:variable name="name"><xsl:value-of select="following-sibling::*[position()=1]/m:csymbol"/></xsl:variable>
2854  <xsl:choose>
2855   <xsl:when test="$name='rw_step'">
2856          <m:mtr>
2857           <m:mtd>
2858            <m:mrow>
2859             <m:mtext>Rewrite</m:mtext>
2860             <m:mphantom><m:mtext>_</m:mtext></m:mphantom>
2861             <xsl:apply-templates select="following-sibling::*[position()=1]/*[2]"/>
2862             <m:mphantom><m:mtext>_</m:mtext></m:mphantom>
2863             <m:mtext>with</m:mtext>
2864             <m:mphantom><m:mtext>_</m:mtext></m:mphantom>
2865             <xsl:apply-templates select="following-sibling::*[position()=1]/*[3]"/>
2866             <m:mphantom><m:mtext>_</m:mtext></m:mphantom>
2867             <m:mtext>by</m:mtext>
2868             <m:mphantom><m:mtext>_</m:mtext></m:mphantom>
2869             <xsl:apply-templates select="following-sibling::*[position()=1]/*[4]"/>
2870            </m:mrow>
2871           </m:mtd>
2872          </m:mtr>
2873          <m:mtr>
2874           <m:mtd>
2875            <m:mrow>
2876             <m:mtext mathcolor="Red">we&#x00a0;get</m:mtext>
2877             <m:mphantom><m:mtext>_</m:mtext></m:mphantom>
2878             <xsl:apply-templates select="."/>
2879            </m:mrow>
2880           </m:mtd>
2881          </m:mtr>
2882    </xsl:when>
2883    <xsl:otherwise>
2884          <m:mtr>
2885           <m:mtd>
2886            <m:mrow>
2887             <xsl:apply-templates select="following-sibling::*[position()=1]"/>
2888            </m:mrow>
2889           </m:mtd>
2890          </m:mtr>
2891          <m:mtr>
2892           <m:mtd>
2893            <m:mrow>
2894             <m:mtext mathcolor="Red">we&#x00a0;get</m:mtext>
2895             <m:mphantom><m:mtext>_</m:mtext></m:mphantom>
2896             <xsl:apply-templates select="."/>
2897            </m:mrow>
2898           </m:mtd>
2899          </m:mtr>
2900     </xsl:otherwise>
2901    </xsl:choose>
2902          <xsl:apply-templates mode="thread" select="preceding-sibling::*[position()=2]"/>
2903 </xsl:template>
2904 -->
2905
2906 <!-- LAMBDA -->
2907
2908 <xsl:template match="m:lambda">
2909     <xsl:variable name="charlength"><xsl:apply-templates select="*[position()=1]" mode="charcount"/></xsl:variable>
2910     <m:mrow>
2911      <xsl:if test="@id">
2912       <xsl:attribute name="xref">
2913        <xsl:value-of select="@id"/>
2914       </xsl:attribute>
2915      </xsl:if>
2916      <xsl:choose>
2917      <xsl:when test="$charlength >= $framewidth">
2918       <m:mtable align="baseline 1" equalrows="false" columnalign="left">
2919         <m:mtr>
2920           <m:mtd>
2921            <m:mrow>
2922             <m:mo mathcolor="Red">&#x03bb;</m:mo>
2923             <!--<xsl:apply-templates select="m:bvar"/>-->
2924             <xsl:apply-templates select="m:bvar/m:ci"/>
2925            </m:mrow>
2926           </m:mtd>
2927          </m:mtr>
2928        <m:mtr>
2929         <m:mtd>
2930          <m:mrow>
2931           <m:mo>.</m:mo>
2932           <xsl:apply-templates select="*[position()=2]"/>
2933          </m:mrow>
2934         </m:mtd>
2935        </m:mtr>
2936       </m:mtable>
2937      </xsl:when>
2938      <xsl:otherwise>
2939       <m:mo mathcolor="Red">&#x03bb;</m:mo>
2940       <!--<xsl:apply-templates select="m:bvar/m:ci"/>
2941       <m:mo>:</m:mo>
2942       <xsl:apply-templates select="m:bvar/m:type"/>-->
2943       <xsl:apply-templates select="m:bvar/m:ci"/>
2944       <m:mo>.</m:mo>
2945       <xsl:apply-templates select="*[position()=2]"/>
2946      </xsl:otherwise>
2947      </xsl:choose>
2948     </m:mrow>
2949 </xsl:template>
2950
2951
2952 <!--**********************-->
2953 <!--       COUNTING       -->
2954 <!--**********************-->
2955
2956 <xsl:template match="m:cn|m:and|m:or|m:not|m:exists|m:eq|m:lt|m:leq|m:gt|m:geq
2957  |m:in|m:notin|m:intersect|m:union|m:subset|m:prsubset|m:card|m:setdiff
2958  |m:plus|m:minus|m:times" mode="charcount">
2959 <xsl:param name="incurrent_length" select="0"/>
2960     <xsl:choose>
2961     <xsl:when test="$framewidth > ($incurrent_length + 3 + string-length())">
2962      <xsl:variable name="siblength">
2963       <xsl:apply-templates select="following-sibling::*[position()=1]" mode="charcount">
2964        <xsl:with-param name="incurrent_length" select="$incurrent_length + string-length()"/>
2965       </xsl:apply-templates>
2966      </xsl:variable>
2967      <xsl:choose>
2968      <xsl:when test="string($siblength) = &quot;&quot;">
2969       <xsl:value-of select="$incurrent_length + 3 + string-length()"/>
2970      </xsl:when>
2971      <xsl:otherwise>
2972       <xsl:value-of select="number($siblength)"/>
2973      </xsl:otherwise>
2974      </xsl:choose>
2975     </xsl:when>
2976     <xsl:otherwise>
2977      <xsl:value-of select="$incurrent_length + 3 + string-length()"/>
2978     </xsl:otherwise>
2979     </xsl:choose>
2980 </xsl:template>
2981
2982 <xsl:template match="m:ci|m:csymbol" mode="charcount">
2983 <xsl:param name="incurrent_length" select="0"/>
2984 <xsl:param name="nosibling" select="0"/>
2985     <xsl:choose>
2986     <xsl:when test="$framewidth > ($incurrent_length + string-length()) and ($nosibling = 0)">
2987      <xsl:variable name="siblength">
2988       <xsl:apply-templates select="following-sibling::*[position()=1]" mode="charcount">
2989        <xsl:with-param name="incurrent_length" select="$incurrent_length + string-length()"/>
2990       </xsl:apply-templates>
2991      </xsl:variable>
2992      <xsl:choose>
2993      <xsl:when test="string($siblength) = &quot;&quot;">
2994       <xsl:value-of select="$incurrent_length + string-length()"/>
2995      </xsl:when>
2996      <xsl:otherwise>
2997       <xsl:value-of select="number($siblength)"/>
2998      </xsl:otherwise>
2999      </xsl:choose>
3000     </xsl:when>
3001     <xsl:otherwise>
3002      <xsl:value-of select="$incurrent_length + string-length()"/>
3003     </xsl:otherwise>
3004     </xsl:choose>
3005 </xsl:template>
3006
3007 <xsl:template match="*" mode="charcount">
3008 <xsl:param name="incurrent_length" select="0"/>
3009 <xsl:param name="nosibling" select="0"/>
3010  <xsl:choose>
3011   <xsl:when test="count(child::*) = 0">
3012    <!-- CSC: tremendous bug fixed. An empty element can still have siblings!!! -->
3013    <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>
3014    <xsl:choose>
3015     <xsl:when test="string($siblength) = &quot;&quot;">
3016      <xsl:value-of select="$incurrent_length"/>
3017     </xsl:when>
3018     <xsl:otherwise>
3019       <xsl:value-of select="number($siblength)"/>
3020     </xsl:otherwise>
3021    </xsl:choose>
3022   </xsl:when>
3023   <xsl:otherwise>
3024     <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>
3025     <xsl:choose>
3026     <xsl:when test="$framewidth > number($childlength) and ($nosibling = 0)">
3027      <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>
3028      <xsl:choose>
3029      <xsl:when test="string($siblength) = &quot;&quot;">
3030       <xsl:value-of select="number($childlength)"/>
3031      </xsl:when>
3032      <xsl:otherwise>
3033       <xsl:value-of select="number($siblength)"/>
3034      </xsl:otherwise>
3035      </xsl:choose>
3036     </xsl:when>
3037     <xsl:otherwise>
3038      <xsl:value-of select="number($childlength)"/>
3039     </xsl:otherwise>
3040     </xsl:choose>
3041   </xsl:otherwise>
3042  </xsl:choose>
3043 </xsl:template>
3044
3045 </xsl:stylesheet>
3046