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