helm/style/mmlextension.xsl

   1 <?xml version="1.0"?>
   2
   3 <!-- Copyright (C) 2000, HELM Team                                     -->
   4 <!--                                                                   -->
   5 <!-- This file is part of HELM, an Hypertextual, Electronic            -->
   6 <!-- Library of Mathematics, developed at the Computer Science         -->
   7 <!-- Department, University of Bologna, Italy.                         -->
   8 <!--                                                                   -->
   9 <!-- HELM is free software; you can redistribute it and/or             -->
  10 <!-- modify it under the terms of the GNU General Public License       -->
  11 <!-- as published by the Free Software Foundation; either version 2    -->
  12 <!-- of the License, or (at your option) any later version.            -->
  13 <!--                                                                   -->
  14 <!-- HELM is distributed in the hope that it will be useful,           -->
  15 <!-- but WITHOUT ANY WARRANTY; without even the implied warranty of    -->
  16 <!-- MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE.  See the     -->
  17 <!-- GNU General Public License for more details.                      -->
  18 <!--                                                                   -->
  19 <!-- You should have received a copy of the GNU General Public License -->
  20 <!-- along with HELM; if not, write to the Free Software               -->
  21 <!-- Foundation, Inc., 59 Temple Place - Suite 330, Boston,            -->
  22 <!-- MA  02111-1307, USA.                                              -->
  23 <!--                                                                   -->
  24 <!-- For details, see the HELM World-Wide-Web page,                    -->
  25 <!-- http://cs.unibo.it/helm/.                                         -->
  26
  27 <!--***********************************************************************-->
  28 <!-- Extension to the XSLT version 0.07 of MathML content to presentation: -->
  29 <!-- First draft: February 19 2000, Andrea Asperti, Irene Schena           -->
  30 <!-- Revised: March 3 2000, Irene Schena                                   -->
  31 <!-- Revised: March 15 2000, Claudio Sacerdoti Coen, Irene Schena          -->
  32 <!-- Revised: March 21 2000, Irene Schena                                  -->
  33 <!--***********************************************************************-->
  34
  35 <!-- NOTE: the namespace declaration has to be done in the stylesheets
  36 which generates the toplevel element (see for instance xlink) -->
  37 <xsl:stylesheet version="1.0" xmlns:xsl="http://www.w3.org/1999/XSL/Transform"
  38                               xmlns:m="http://www.w3.org/1998/Math/MathML"
  39                               xmlns:helm="http://www.cs.unibo.it/helm"
  40                               xmlns:xlink="http://www.w3.org/1999/xlink">
  41
  42 <!-- OLD: <xsl:import href="mml2mmlv1_0.xsl"/> -->
  43 <xsl:import href="mmlctop.xsl-0.14"/>
  44
  45 <xsl:import href="mmltheoryextension.xsl"/>
  46
  47 <xsl:param name="explodeall" select="false()"/>
  48
  49 <!--***********************************************************************-->
  50 <!-- Parameter affecting line-breaking                                     -->
  51 <!--***********************************************************************-->
  52
  53 <xsl:variable name="framewidth" select="35"/>
  54
  55 <!--***********************************************************************-->
  56 <!-- Gli oggetti sono stampati come mtext all'interno di una marca toplevel-->
  57 <!-- math ma al di fuori di semantics. Ora vi sono tanti semantics quanti  -->
  58 <!-- sono i termini: la presentation per un termine e' generata come primo -->
  59 <!-- figlio di un semantics e l'originario content viene inserito nel      -->
  60 <!-- nel secondo figlio di semantics, annotation-xml                       -->
  61 <!--***********************************************************************-->
  62
  63 <!--**********************-->
  64 <!--        OBJECTS       -->
  65 <!--**********************-->
  66
  67 <xsl:param name="type" select="'standalone'"/>
  68
  69 <xsl:template match="/">
  70  <xsl:choose>
  71   <xsl:when test="$type = 'standalone'">
  72    <xsl:apply-templates select="*"/>
  73   </xsl:when>
  74   <xsl:otherwise>
  75    <to_be_embedded>
  76     <xsl:apply-templates select="*"/>
  77    </to_be_embedded>
  78   </xsl:otherwise>
  79  </xsl:choose>
  80 </xsl:template>
  81
  82 <!-- DEFINITION -->
  83
  84 <xsl:template match="Definition">
  85     <m:math>
  86      <m:mtable align="baseline 1" equalrows="false" columnalign="left" helm:xref="{@helm:xref}">
  87       <m:mtr>
  88        <m:mtd>
  89         <m:mrow>
  90          <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>
  91         </m:mrow>
  92        </m:mtd>
  93       </m:mtr>
  94       <m:mtr>
  95        <m:mtd>
  96         <m:mrow>
  97          <m:mphantom><m:mtext>__</m:mtext></m:mphantom>
  98          <xsl:apply-templates select="type/*[1]"/>
  99         </m:mrow>
 100        </m:mtd>
 101       </m:mtr>
 102       <m:mtr>
 103        <m:mtd>
 104         <m:mrow>
 105          <m:mtext>AS</m:mtext>
 106         </m:mrow>
 107        </m:mtd>
 108       </m:mtr>
 109       <m:mtr>
 110        <m:mtd>
 111         <m:mrow>
 112          <m:mphantom><m:mtext>__</m:mtext></m:mphantom>
 113          <xsl:apply-templates select="body/*[1]"/>
 114         </m:mrow>
 115        </m:mtd>
 116       </m:mtr>
 117      </m:mtable>
 118     </m:math>
 119 </xsl:template>
 120
 121 <!-- AXIOM -->
 122
 123 <xsl:template match="Axiom">
 124     <m:math>
 125      <m:mtable align="baseline 1" equalrows="false" columnalign="left" helm:xref="{@helm:xref}">
 126       <m:mtr>
 127        <m:mtd>
 128         <m:mrow>
 129          <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>
 130         </m:mrow>
 131        </m:mtd>
 132       </m:mtr>
 133       <m:mtr>
 134        <m:mtd>
 135         <m:mrow>
 136          <m:mphantom><m:mtext>__</m:mtext></m:mphantom>
 137          <xsl:apply-templates select="type/*[1]"/>
 138         </m:mrow>
 139        </m:mtd>
 140       </m:mtr>
 141      </m:mtable>
 142     </m:math>
 143 </xsl:template>
 144
 145 <!-- UNFINISHED PROOF -->
 146
 147 <xsl:template match="CurrentProof">
 148     <m:math>
 149      <m:mtable align="baseline 1" equalrows="false" columnalign="left" helm:xref="{@helm:xref}">
 150       <m:mtr>
 151        <m:mtd>
 152         <m:mrow>
 153          <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>
 154         </m:mrow>
 155        </m:mtd>
 156       </m:mtr>
 157       <m:mtr>
 158        <m:mtd>
 159         <m:mrow>
 160          <m:mtext>THESIS:</m:mtext>
 161         </m:mrow>
 162        </m:mtd>
 163       </m:mtr>
 164       <m:mtr>
 165        <m:mtd>
 166         <m:mrow>
 167          <m:mphantom><m:mtext>__</m:mtext></m:mphantom>
 168          <xsl:apply-templates select="type/*[1]"/>
 169         </m:mrow>
 170        </m:mtd>
 171       </m:mtr>
 172       <m:mtr>
 173        <m:mtd>
 174         <m:mrow>
 175          <m:mtext>CONJECTURES:</m:mtext>
 176         </m:mrow>
 177        </m:mtd>
 178       </m:mtr>
 179       <xsl:for-each select="Conjecture">
 180       <m:mtr>
 181        <m:mtd>
 182         <m:mrow>
 183          <m:mphantom><m:mtext>__</m:mtext></m:mphantom>
 184          <m:mtext><xsl:value-of select="./@no"/>:</m:mtext>
 185          <xsl:apply-templates select="./*[1]"/>
 186         </m:mrow>
 187        </m:mtd>
 188       </m:mtr>
 189       </xsl:for-each>
 190       <m:mtr>
 191        <m:mtd>
 192         <m:mrow>
 193          <m:mtext>CORRESPONDING PROOF:</m:mtext>
 194         </m:mrow>
 195        </m:mtd>
 196       </m:mtr>
 197       <m:mtr>
 198        <m:mtd>
 199         <m:mrow>
 200          <m:mphantom><m:mtext>__</m:mtext></m:mphantom>
 201          <xsl:apply-templates select="body/*[1]"/>
 202         </m:mrow>
 203        </m:mtd>
 204       </m:mtr>
 205      </m:mtable>
 206     </m:math>
 207 </xsl:template>
 208
 209 <!-- MUTUAL INDUCTIVE DEFINITION -->
 210
 211 <xsl:template match="InductiveDefinition">
 212     <m:math>
 213      <m:mtable align="baseline 1" equalrows="false" columnalign="left" helm:xref="{@helm:xref}">
 214      <xsl:for-each select="InductiveType">
 215       <m:mtr>
 216        <m:mtd>
 217         <m:mrow>
 218          <xsl:choose>
 219          <xsl:when test="position() = 1">
 220           <xsl:choose>
 221           <xsl:when test="string(./@inductive) = &quot;true&quot;">
 222            <m:mtext>INDUCTIVE DEFINITION</m:mtext>
 223           </xsl:when>
 224           <xsl:otherwise>
 225            <m:mtext>COINDUCTIVE DEFINITION</m:mtext>
 226           </xsl:otherwise>
 227           </xsl:choose>
 228          </xsl:when>
 229          <xsl:otherwise>
 230           <m:mtext>AND</m:mtext>
 231          </xsl:otherwise>
 232          </xsl:choose>
 233          <m:mphantom><m:mtext>_</m:mtext></m:mphantom>
 234          <m:mtext><xsl:value-of select="./@name"/>(<xsl:if test="string(../Params) != &quot;&quot;"><xsl:value-of select="../Params"/></xsl:if>)</m:mtext>
 235         </m:mrow>
 236        </m:mtd>
 237       </m:mtr>
 238       <m:mtr>
 239        <m:mtd>
 240         <m:mrow>
 241          <m:mphantom><m:mtext>__</m:mtext></m:mphantom>
 242          <m:mtext>[</m:mtext>
 243          <xsl:choose>
 244          <xsl:when test="string(../Param) != &quot;&quot;">
 245           <m:mtable align="baseline 1" equalrows="false" columnalign="left">
 246            <xsl:for-each select="../Param">
 247             <m:mtr>
 248              <m:mtd>
 249               <m:mrow>
 250                <m:mi><xsl:value-of select="./@name"/></m:mi>
 251                <m:mo>:</m:mo>
 252                <xsl:apply-templates select="*"/>
 253               </m:mrow>
 254              </m:mtd>
 255             </m:mtr>
 256            </xsl:for-each>
 257             <m:mtr>
 258              <m:mtd>
 259               <m:mrow>
 260                <m:mtext>]</m:mtext>
 261               </m:mrow>
 262              </m:mtd>
 263             </m:mtr>
 264           </m:mtable>
 265          </xsl:when>
 266          <xsl:otherwise>
 267           <m:mtext>]</m:mtext>
 268          </xsl:otherwise>
 269          </xsl:choose>
 270         </m:mrow>
 271        </m:mtd>
 272       </m:mtr>
 273       <m:mtr>
 274        <m:mtd>
 275         <m:mrow>
 276          <m:mtext>OF ARITY</m:mtext>
 277         </m:mrow>
 278        </m:mtd>
 279       </m:mtr>
 280       <m:mtr>
 281        <m:mtd>
 282         <m:mrow>
 283          <m:mphantom><m:mtext>__</m:mtext></m:mphantom>
 284          <xsl:apply-templates select="./arity/*[1]"/>
 285         </m:mrow>
 286        </m:mtd>
 287       </m:mtr>
 288       <m:mtr>
 289        <m:mtd>
 290         <m:mrow>
 291          <m:mtext>BUILT FROM</m:mtext>
 292         </m:mrow>
 293        </m:mtd>
 294       </m:mtr>
 295       <xsl:for-each select="./Constructor">
 296       <m:mtr>
 297        <m:mtd>
 298         <m:mrow>
 299          <xsl:choose>
 300          <xsl:when test="position() = 1">
 301           <m:mphantom><m:mtext>__</m:mtext></m:mphantom>
 302          </xsl:when>
 303          <xsl:otherwise>
 304           <m:mtext>|</m:mtext>
 305           <m:mphantom><m:mtext>_</m:mtext></m:mphantom>
 306          </xsl:otherwise>
 307          </xsl:choose>
 308          <m:mtext><xsl:value-of select="./@name"/> OF</m:mtext>
 309          <m:mphantom><m:mtext>_</m:mtext></m:mphantom>
 310          <xsl:apply-templates select="./*[1]"/>
 311         </m:mrow>
 312        </m:mtd>
 313       </m:mtr>
 314       </xsl:for-each>
 315      </xsl:for-each>
 316      </m:mtable>
 317     </m:math>
 318 </xsl:template>
 319
 320 <!-- VARIABLE -->
 321
 322 <xsl:template match="Variable">
 323     <m:math>
 324      <m:mtable align="baseline 1" equalrows="false" columnalign="left" helm:xref="{@helm:xref}">
 325       <m:mtr>
 326        <m:mtd>
 327         <m:mrow>
 328          <m:mtext>VARIABLE <xsl:value-of select="@name"/> OF TYPE</m:mtext>
 329         </m:mrow>
 330        </m:mtd>
 331       </m:mtr>
 332       <m:mtr>
 333        <m:mtd>
 334         <m:mrow>
 335          <m:mphantom><m:mtext>__</m:mtext></m:mphantom>
 336          <xsl:apply-templates select="type/*[1]"/>
 337         </m:mrow>
 338        </m:mtd>
 339       </m:mtr>
 340       <xsl:if test="name(*[1])='body'">
 341        <m:mtr>
 342         <m:mtd>
 343          <m:mrow>
 344           <m:mtext>AS</m:mtext>
 345          </m:mrow>
 346         </m:mtd>
 347        </m:mtr>
 348        <m:mtr>
 349         <m:mtd>
 350          <m:mrow>
 351           <m:mphantom><m:mtext>__</m:mtext></m:mphantom>
 352           <xsl:apply-templates select="body/*[1]"/>
 353          </m:mrow>
 354         </m:mtd>
 355        </m:mtr>
 356       </xsl:if>
 357      </m:mtable>
 358     </m:math>
 359 </xsl:template>
 360
 361 <!--**********************-->
 362 <!--        TERMS         -->
 363 <!--**********************-->
 364
 365 <xsl:template match="m:bvar">
 366  <xsl:choose>
 367   <xsl:when test="m:type">
 368    <xsl:variable name="charlength">
 369     <xsl:apply-templates select="m:ci" mode="charcount"/>
 370    </xsl:variable>
 371    <xsl:choose>
 372     <xsl:when test="$charlength >= $framewidth">
 373      <m:mtable align="baseline 1" equalrows="false" columnalign="left">
 374       <m:mtr>
 375        <m:mtd>
 376         <m:mrow>
 377          <xsl:apply-templates select="m:ci"/>
 378          <m:mo>:</m:mo>
 379         </m:mrow>
 380        </m:mtd>
 381       </m:mtr>
 382       <m:mtr>
 383        <m:mtd>
 384         <m:mrow>
 385          <xsl:apply-templates select="m:type"/>
 386         </m:mrow>
 387        </m:mtd>
 388       </m:mtr>
 389      </m:mtable>
 390     </xsl:when>
 391     <xsl:otherwise>
 392      <m:mrow>
 393       <xsl:apply-templates select="m:ci"/>
 394       <m:mo>:</m:mo>
 395       <xsl:apply-templates select="m:type"/>
 396      </m:mrow>
 397     </xsl:otherwise>
 398    </xsl:choose>
 399   </xsl:when>
 400   <xsl:otherwise>
 401    <xsl:apply-templates select="m:ci"/>
 402   </xsl:otherwise>
 403  </xsl:choose>
 404 </xsl:template>
 405
 406
 407 <!-- CSYMBOL -->
 408
 409 <xsl:template match="m:apply[m:csymbol]">
 410 <xsl:param name="nopar" select="0"/>
 411     <xsl:variable name="name"><xsl:value-of select="m:csymbol"/></xsl:variable>
 412     <xsl:variable name="charlength"><xsl:apply-templates select="m:csymbol" mode="charcount"/></xsl:variable>
 413     <m:mrow>
 414      <xsl:if test="@helm:xref">
 415       <xsl:attribute name="m:xref"><xsl:value-of select="@id"/></xsl:attribute>
 416      </xsl:if>
 417      <xsl:choose>
 418       <!-- FORALL -->
 419       <xsl:when test="$name='forall'">
 420        <xsl:choose>
 421        <xsl:when test="$charlength >= $framewidth">
 422         <m:mtable align="baseline 1" equalrows="false" columnalign="left">
 423          <m:mtr>
 424           <m:mtd>
 425            <m:mrow>
 426             <m:mo mathcolor="Blue">&#8704;</m:mo>
 427             <xsl:apply-templates select="m:bvar"/>
 428            </m:mrow>
 429           </m:mtd>
 430          </m:mtr>
 431          <m:mtr>
 432           <m:mtd>
 433            <m:mrow>
 434             <m:mo>.</m:mo>
 435             <xsl:apply-templates select="*[position()=3]"/>
 436            </m:mrow>
 437           </m:mtd>
 438          </m:mtr>
 439         </m:mtable>
 440        </xsl:when>
 441        <xsl:otherwise>
 442         <m:mo mathcolor="Blue">&#8704;</m:mo>
 443         <xsl:apply-templates select="m:bvar/m:ci"/>
 444         <m:mo>:</m:mo>
 445         <xsl:apply-templates select="m:bvar/m:type"/>
 446         <m:mo>.</m:mo>
 447         <xsl:apply-templates select="*[position()=3]"/>
 448        </xsl:otherwise>
 449        </xsl:choose>
 450       </xsl:when>
 451       <!-- LET-IN -->
 452       <xsl:when test="$name='let_in'">
 453        <xsl:choose>
 454        <xsl:when test="$charlength >= $framewidth">
 455         <m:mtable align="baseline 1" equalrows="false" columnalign="left">
 456          <m:mtr>
 457           <m:mtd>
 458            <m:mrow>
 459             <m:mo>LET</m:mo>
 460             <m:mphantom><m:mtext>_</m:mtext></m:mphantom>
 461             <xsl:apply-templates select="m:bvar"/>
 462            </m:mrow>
 463           </m:mtd>
 464          </m:mtr>
 465          <m:mtr>
 466           <m:mtd>
 467            <m:mrow>
 468             <m:mo>=</m:mo>
 469             <xsl:apply-templates select="*[position()=3]"/>
 470            </m:mrow>
 471           </m:mtd>
 472          </m:mtr>
 473          <m:mtr>
 474           <m:mtd>
 475            <m:mrow>
 476             <m:mo>IN</m:mo>
 477             <m:mphantom><m:mtext>_</m:mtext></m:mphantom>
 478             <xsl:apply-templates select="*[position()=4]"/>
 479            </m:mrow>
 480           </m:mtd>
 481          </m:mtr>
 482         </m:mtable>
 483        </xsl:when>
 484        <xsl:otherwise>
 485         <m:mo>LET</m:mo>
 486         <m:mphantom><m:mtext>_</m:mtext></m:mphantom>
 487         <xsl:apply-templates select="m:bvar/m:ci"/>
 488         <m:mo>=</m:mo>
 489         <xsl:apply-templates select="*[position()=3]"/>
 490         <m:mphantom><m:mtext>_</m:mtext></m:mphantom>
 491         <m:mtext>IN</m:mtext>
 492         <m:mphantom><m:mtext>_</m:mtext></m:mphantom>
 493         <xsl:apply-templates select="*[position()=4]"/>
 494        </xsl:otherwise>
 495        </xsl:choose>
 496       </xsl:when>
 497       <!-- PROD -->
 498       <xsl:when test="$name='prod'">
 499        <xsl:choose>
 500        <xsl:when test="$charlength >= $framewidth">
 501         <m:mtable align="baseline 1" equalrows="false" columnalign="left">
 502          <m:mtr>
 503           <m:mtd>
 504            <m:mrow>
 505             <m:mo mathcolor="Blue">&#x03a0;</m:mo>
 506             <xsl:apply-templates select="m:bvar"/>
 507            </m:mrow>
 508           </m:mtd>
 509          </m:mtr>
 510          <m:mtr>
 511           <m:mtd>
 512            <m:mrow>
 513             <m:mo>.</m:mo>
 514             <xsl:apply-templates select="*[position()=3]"/>
 515            </m:mrow>
 516           </m:mtd>
 517          </m:mtr>
 518         </m:mtable>
 519        </xsl:when>
 520        <xsl:otherwise>
 521         <m:mo mathcolor="Blue">&#x03a0;</m:mo>
 522         <xsl:apply-templates select="m:bvar/m:ci"/>
 523         <m:mo>:</m:mo>
 524         <xsl:apply-templates select="m:bvar/m:type"/>
 525         <m:mo>.</m:mo>
 526         <xsl:apply-templates select="*[position()=3]"/>
 527        </xsl:otherwise>
 528        </xsl:choose>
 529       </xsl:when>
 530       <!-- ARROW -->
 531       <xsl:when test="$name='arrow'">
 532        <xsl:choose>
 533        <xsl:when test="$charlength >= $framewidth">
 534         <m:mtable align="baseline 1" equalrows="false" columnalign="left">
 535          <m:mtr>
 536           <m:mtd>
 537            <m:mrow>
 538             <xsl:if test="$nopar=0">
 539              <m:mo stretchy="false">(</m:mo>
 540             </xsl:if>
 541             <xsl:apply-templates select="*[position()=2]"/>
 542            </m:mrow>
 543           </m:mtd>
 544          </m:mtr>
 545          <m:mtr>
 546           <m:mtd>
 547            <m:mrow>
 548             <m:mo mathmathcolor="Blue">&#x2192;</m:mo>
 549             <xsl:choose>
 550             <xsl:when test="*[position()=3]/m:csymbol">
 551              <xsl:variable name="nextp"><xsl:value-of select="*[position()=3]/m:csymbol"/></xsl:variable>
 552              <xsl:choose>
 553              <xsl:when test="$nextp='arrow'">
 554               <xsl:apply-templates select="*[position()=3]"><xsl:with-param name="nopar" select="1"/></xsl:apply-templates>
 555              </xsl:when>
 556              <xsl:otherwise>
 557               <xsl:apply-templates select="*[position()=3]"/>
 558              </xsl:otherwise>
 559              </xsl:choose>
 560             </xsl:when>
 561             <xsl:otherwise>
 562              <xsl:apply-templates select="*[position()=3]"/>
 563             </xsl:otherwise>
 564             </xsl:choose>
 565            </m:mrow>
 566           </m:mtd>
 567          </m:mtr>
 568          <xsl:if test="$nopar=0">
 569          <m:mtr>
 570           <m:mtd>
 571            <m:mrow>
 572             <m:mo stretchy="false">)</m:mo>
 573            </m:mrow>
 574           </m:mtd>
 575          </m:mtr>
 576          </xsl:if>
 577         </m:mtable>
 578        </xsl:when>
 579        <xsl:otherwise>
 580         <xsl:if test="$nopar=0">
 581          <m:mo stretchy="false">(</m:mo>
 582         </xsl:if>
 583         <xsl:apply-templates select="*[position()=2]"/>
 584         <m:mo mathcolor="Blue">&#x2192;</m:mo>
 585         <xsl:choose>
 586         <xsl:when test="*[position()=3]/m:csymbol">
 587          <xsl:variable name="nextp"><xsl:value-of select="*[position()=3]/m:csymbol"/></xsl:variable>
 588          <xsl:choose>
 589          <xsl:when test="$nextp='arrow'">
 590           <xsl:apply-templates select="*[position()=3]"><xsl:with-param name="nopar" select="1"/></xsl:apply-templates>
 591          </xsl:when>
 592          <xsl:otherwise>
 593           <xsl:apply-templates select="*[position()=3]"/>
 594          </xsl:otherwise>
 595          </xsl:choose>
 596         </xsl:when>
 597         <xsl:otherwise>
 598          <xsl:apply-templates select="*[position()=3]"/>
 599         </xsl:otherwise>
 600         </xsl:choose>
 601         <xsl:if test="$nopar=0">
 602          <m:mo stretchy="false">)</m:mo>
 603         </xsl:if>
 604        </xsl:otherwise>
 605        </xsl:choose>
 606       </xsl:when>
 607       <!-- APP -->
 608       <xsl:when test="$name='app'">
 609        <xsl:choose>
 610        <xsl:when test="$charlength >= $framewidth">
 611         <m:mtable align="baseline 1" equalrows="false" columnalign="left">
 612          <m:mtr>
 613           <m:mtd>
 614            <m:mrow>
 615             <m:mo stretchy="false">(</m:mo>
 616             <xsl:apply-templates select="*[position()=2]"/>
 617            </m:mrow>
 618           </m:mtd>
 619          </m:mtr>
 620          <xsl:for-each select="*[position()>2]">
 621          <m:mtr>
 622           <m:mtd>
 623            <m:mrow>
 624             <m:mphantom><m:mtext>(</m:mtext></m:mphantom>
 625             <xsl:apply-templates select="."/>
 626            </m:mrow>
 627           </m:mtd>
 628          </m:mtr>
 629          </xsl:for-each>
 630          <m:mtr>
 631           <m:mtd>
 632            <m:mrow>
 633             <m:mo stretchy="false">)</m:mo>
 634            </m:mrow>
 635           </m:mtd>
 636          </m:mtr>
 637         </m:mtable>
 638        </xsl:when>
 639        <xsl:otherwise>
 640         <m:mo stretchy="false">(</m:mo>
 641         <xsl:apply-templates select="*[position()=2]"/>
 642         <xsl:for-each select="*[position()>2]">
 643          <m:mphantom><m:mtext>_</m:mtext></m:mphantom>
 644          <xsl:apply-templates select="."/>
 645         </xsl:for-each>
 646         <m:mo stretchy="false">)</m:mo>
 647        </xsl:otherwise>
 648        </xsl:choose>
 649       </xsl:when>
 650       <!-- CAST -->
 651       <xsl:when test="$name='cast'">
 652        <xsl:choose>
 653        <xsl:when test="$charlength >= $framewidth">
 654         <m:mtable align="baseline 1" equalrows="false" columnalign="left">
 655          <m:mtr>
 656           <m:mtd>
 657            <m:mrow>
 658             <m:mo stretchy="false">(</m:mo>
 659             <xsl:apply-templates select="*[position()=2]"/>
 660            </m:mrow>
 661           </m:mtd>
 662          </m:mtr>
 663          <m:mtr>
 664           <m:mtd>
 665            <m:mrow>
 666             <m:mo mathcolor="Maroon">:></m:mo>
 667             <xsl:apply-templates select="*[position()=3]"/>
 668            </m:mrow>
 669           </m:mtd>
 670          </m:mtr>
 671          <m:mtr>
 672           <m:mtd>
 673            <m:mrow>
 674             <m:mo stretchy="false">)</m:mo>
 675            </m:mrow>
 676           </m:mtd>
 677          </m:mtr>
 678         </m:mtable>
 679        </xsl:when>
 680        <xsl:otherwise>
 681         <m:mo stretchy="false">(</m:mo>
 682         <xsl:apply-templates select="*[position()=2]"/>
 683         <m:mo mathcolor="Maroon">:></m:mo>
 684         <xsl:apply-templates select="*[position()=3]"/>
 685         <m:mo stretchy="false">)</m:mo>
 686        </xsl:otherwise>
 687        </xsl:choose>
 688       </xsl:when>
 689       <!-- PROP -->
 690       <xsl:when test="$name='Prop'">
 691        <m:mo>Prop</m:mo>
 692       </xsl:when>
 693       <!-- SET -->
 694       <xsl:when test="$name='Set'">
 695        <m:mo>Set</m:mo>
 696       </xsl:when>
 697       <!-- TYPE -->
 698       <xsl:when test="$name='Type'">
 699        <m:mo>Type</m:mo>
 700       </xsl:when>
 701       <!-- MUTCASE -->
 702       <xsl:when test="$name='mutcase'">
 703        <xsl:choose>
 704        <xsl:when test="$charlength >= $framewidth">
 705         <xsl:variable name="charlength"><xsl:apply-templates select="*[position()=2]" mode="charcount"><xsl:with-param name="nosibling" select="1"/></xsl:apply-templates></xsl:variable>
 706         <m:mtable align="baseline 1" equalrows="false" columnalign="left">
 707          <m:mtr>
 708           <m:mtd>
 709            <m:mrow>
 710             <m:mo>&lt;</m:mo>
 711             <xsl:apply-templates select="*[position()=2]"/>
 712             <xsl:if test="$framewidth > $charlength">
 713              <m:mo>&gt;</m:mo>
 714              <m:mo>CASES</m:mo>
 715              <m:mphantom><m:mtext>_</m:mtext></m:mphantom>
 716              <xsl:apply-templates select="*[position()=3]"/>
 717             </xsl:if>
 718            </m:mrow>
 719           </m:mtd>
 720          </m:mtr>
 721          <xsl:if test="$charlength >= $framewidth">
 722          <m:mtr>
 723           <m:mtd>
 724            <m:mrow>
 725             <m:mo>&gt;</m:mo>
 726             <m:mo>CASES</m:mo>
 727             <m:mphantom><m:mtext>_</m:mtext></m:mphantom>
 728             <xsl:apply-templates select="*[position()=3]"/>
 729            </m:mrow>
 730           </m:mtd>
 731          </m:mtr>
 732          </xsl:if>
 733          <m:mtr>
 734           <m:mtd>
 735            <m:mrow>
 736             <m:mo>OF</m:mo>
 737            </m:mrow>
 738           </m:mtd>
 739          </m:mtr>
 740          <xsl:for-each select="piecewise/piece">
 741          <xsl:variable name="charlength"><xsl:apply-templates select="./*[2]" mode="charcount"><xsl:with-param name="nosibling" select="1"/></xsl:apply-templates></xsl:variable>
 742          <m:mtr>
 743           <m:mtd>
 744            <m:mrow>
 745             <xsl:choose>
 746             <xsl:when test="position() = 1">
 747               <m:mphantom><m:mtext>|</m:mtext></m:mphantom>
 748             </xsl:when>
 749             <xsl:otherwise>
 750              <m:mo stretchy="false">|</m:mo>
 751             </xsl:otherwise>
 752             </xsl:choose>
 753             <m:mphantom><m:mtext>_</m:mtext></m:mphantom>
 754             <xsl:apply-templates select="./*[2]"/>
 755             <xsl:if test="$framewidth > $charlength">
 756              <m:mo mathcolor="Green">&#x21d2;</m:mo>
 757              <xsl:apply-templates select="./*[1]"/>
 758             </xsl:if>
 759            </m:mrow>
 760           </m:mtd>
 761          </m:mtr>
 762          <xsl:if test="$charlength >= $framewidth">
 763          <m:mtr>
 764           <m:mtd>
 765            <m:mrow>
 766             <m:mphantom><m:mtext>|_</m:mtext></m:mphantom>
 767             <m:mo mathcolor="Green">&#x21d2;</m:mo>
 768             <xsl:apply-templates select="./*[1]"/>
 769            </m:mrow>
 770           </m:mtd>
 771          </m:mtr>
 772          </xsl:if>
 773         </xsl:for-each>
 774          <m:mtr>
 775           <m:mtd>
 776            <m:mrow>
 777             <m:mo>END</m:mo>
 778            </m:mrow>
 779           </m:mtd>
 780          </m:mtr>
 781         </m:mtable>
 782        </xsl:when>
 783        <xsl:otherwise>
 784         <m:mo>&lt;</m:mo><xsl:apply-templates select="*[position()=2]"/><m:mo>&gt;</m:mo>
 785         <m:mo>CASES</m:mo>
 786         <m:mphantom><m:mtext>_</m:mtext></m:mphantom>
 787         <xsl:apply-templates select="*[position()=3]"/>
 788         <m:mphantom><m:mtext>_</m:mtext></m:mphantom>
 789         <m:mo>OF</m:mo>
 790         <xsl:for-each select="piecewise/piece">
 791          <xsl:choose>
 792          <xsl:when test="position() != 1">
 793           <m:mo stretchy="false">|</m:mo>
 794          </xsl:when>
 795          </xsl:choose>
 796          <xsl:apply-templates select="./*[2]"/>
 797          <m:mo mathcolor="Green">&#x21d2;</m:mo>
 798          <xsl:apply-templates select="./*[1]"/>
 799         </xsl:for-each>
 800         <m:mphantom><m:mtext>_</m:mtext></m:mphantom>
 801         <m:mo>END</m:mo>
 802        </xsl:otherwise>
 803        </xsl:choose>
 804       </xsl:when>
 805       <!-- FIX -->
 806       <xsl:when test="$name='fix'">
 807        <xsl:choose>
 808        <xsl:when test="$charlength >= $framewidth">
 809         <m:mtable align="baseline 1" equalrows="false" columnalign="left">
 810          <m:mtr>
 811           <m:mtd>
 812            <m:mrow>
 813             <m:mo>FIX</m:mo>
 814             <m:mphantom><m:mtext>_</m:mtext></m:mphantom>
 815             <m:mi><xsl:value-of select="m:ci"/></m:mi>
 816             <m:mo stretchy="false">{</m:mo>
 817            </m:mrow>
 818           </m:mtd>
 819          </m:mtr>
 820          <m:mtr>
 821           <m:mtd>
 822            <m:mrow>
 823             <m:mphantom><m:mtext>__</m:mtext></m:mphantom>
 824             <m:mtable align="baseline 1" equalrows="false" columnalign="left">
 825             <xsl:for-each select="m:bvar">
 826              <xsl:variable name="charlength"><xsl:apply-templates select="m:type" mode="charcount"><xsl:with-param name="nosibling" select="1"/></xsl:apply-templates></xsl:variable>
 827              <m:mtr>
 828               <m:mtd>
 829                <m:mrow>
 830                 <m:mi><xsl:value-of select="m:ci"/></m:mi>
 831                 <m:mo>:</m:mo>
 832                 <xsl:if test="$framewidth > $charlength">
 833                  <xsl:apply-templates select="m:type"/>
 834                 </xsl:if>
 835                </m:mrow>
 836               </m:mtd>
 837              </m:mtr>
 838              <xsl:if test="$charlength >= $framewidth">
 839              <m:mtr>
 840               <m:mtd>
 841                <m:mrow>
 842                 <m:mphantom><m:mtext>:=</m:mtext></m:mphantom>
 843                 <xsl:apply-templates select="m:type"/>
 844                </m:mrow>
 845               </m:mtd>
 846              </m:mtr>
 847              </xsl:if>
 848              <m:mtr>
 849               <m:mtd>
 850                <m:mrow>
 851                 <m:mo>:=</m:mo>
 852                 <xsl:apply-templates select="following-sibling::*[position()=1]"/>
 853                </m:mrow>
 854               </m:mtd>
 855              </m:mtr>
 856             </xsl:for-each>
 857             </m:mtable>
 858            </m:mrow>
 859           </m:mtd>
 860          </m:mtr>
 861          <m:mtr>
 862           <m:mtd>
 863            <m:mrow>
 864             <m:mo stretchy="false">}</m:mo>
 865            </m:mrow>
 866           </m:mtd>
 867          </m:mtr>
 868         </m:mtable>
 869        </xsl:when>
 870        <xsl:otherwise>
 871         <m:mo>FIX</m:mo>
 872         <m:mi><xsl:value-of select="m:ci"/></m:mi>
 873         <m:mo stretchy="false">{</m:mo>
 874         <m:mtable align="baseline 1" equalrows="false" columnalign="left">
 875         <xsl:for-each select="m:bvar">
 876          <m:mtr>
 877           <m:mtd>
 878            <m:mrow>
 879             <m:mi><xsl:value-of select="m:ci"/></m:mi>
 880             <m:mo>:</m:mo>
 881             <xsl:apply-templates select="m:type"/>
 882             <m:mo>:=</m:mo>
 883             <xsl:apply-templates select="following-sibling::*[position() = 1]"/>
 884             <xsl:if test="position()=last()">
 885              <m:mo stretchy="false">}</m:mo>
 886             </xsl:if>
 887            </m:mrow>
 888           </m:mtd>
 889          </m:mtr>
 890          </xsl:for-each>
 891         </m:mtable>
 892        </xsl:otherwise>
 893        </xsl:choose>
 894       </xsl:when>
 895       <!-- COFIX -->
 896       <xsl:when test="$name='cofix'">
 897        <xsl:choose>
 898        <xsl:when test="$charlength >= $framewidth">
 899         <m:mtable align="baseline 1" equalrows="false" columnalign="left">
 900          <m:mtr>
 901           <m:mtd>
 902            <m:mrow>
 903             <m:mo>COFIX</m:mo>
 904             <m:mphantom><m:mtext>_</m:mtext></m:mphantom>
 905             <m:mi><xsl:value-of select="m:ci"/></m:mi>
 906             <m:mo stretchy="false">{</m:mo>
 907            </m:mrow>
 908           </m:mtd>
 909          </m:mtr>
 910          <m:mtr>
 911           <m:mtd>
 912            <m:mrow>
 913             <m:mphantom><m:mtext>__</m:mtext></m:mphantom>
 914             <m:mtable align="baseline 1" equalrows="false" columnalign="left">
 915             <xsl:for-each select="m:bvar">
 916              <xsl:variable name="charlength"><xsl:apply-templates select="m:type" mode="charcount"><xsl:with-param name="nosibling" select="1"/></xsl:apply-templates></xsl:variable>
 917              <m:mtr>
 918               <m:mtd>
 919                <m:mrow>
 920                 <m:mi><xsl:value-of select="m:ci"/></m:mi>
 921                 <m:mo>:</m:mo>
 922                 <xsl:if test="$framewidth > $charlength">
 923                  <xsl:apply-templates select="m:type"/>
 924                 </xsl:if>
 925                </m:mrow>
 926               </m:mtd>
 927              </m:mtr>
 928              <xsl:if test="$charlength >= $framewidth">
 929              <m:mtr>
 930               <m:mtd>
 931                <m:mrow>
 932                 <m:mphantom><m:mtext>:=</m:mtext></m:mphantom>
 933                 <xsl:apply-templates select="m:type"/>
 934                </m:mrow>
 935               </m:mtd>
 936              </m:mtr>
 937              </xsl:if>
 938              <m:mtr>
 939               <m:mtd>
 940                <m:mrow>
 941                 <m:mo>:=</m:mo>
 942                 <xsl:apply-templates select="following-sibling::*[position() = 1]"/>
 943                </m:mrow>
 944               </m:mtd>
 945              </m:mtr>
 946             </xsl:for-each>
 947             </m:mtable>
 948            </m:mrow>
 949           </m:mtd>
 950          </m:mtr>
 951          <m:mtr>
 952           <m:mtd>
 953            <m:mrow>
 954             <m:mo stretchy="false">}</m:mo>
 955            </m:mrow>
 956           </m:mtd>
 957          </m:mtr>
 958         </m:mtable>
 959        </xsl:when>
 960        <xsl:otherwise>
 961         <m:mo>COFIX</m:mo>
 962         <m:mi><xsl:value-of select="m:ci"/></m:mi>
 963         <m:mo stretchy="false">{</m:mo>
 964         <m:mtable align="baseline 1" equalrows="false" columnalign="left">
 965         <xsl:for-each select="m:bvar">
 966          <m:mtr>
 967           <m:mtd>
 968            <m:mrow>
 969             <m:mi><xsl:value-of select="m:ci"/></m:mi>
 970             <m:mo>:</m:mo>
 971             <xsl:apply-templates select="m:type"/>
 972             <m:mo>:=</m:mo>
 973             <xsl:apply-templates select="following-sibling::*[position() = 1]"/>
 974             <xsl:if test="position()=last()">
 975              <m:mo stretchy="false">}</m:mo>
 976             </xsl:if>
 977            </m:mrow>
 978           </m:mtd>
 979          </m:mtr>
 980          </xsl:for-each>
 981         </m:mtable>
 982        </xsl:otherwise>
 983        </xsl:choose>
 984       </xsl:when>
 985       <!-- ***************************************** -->
 986       <!-- *********** PROOF ELEMENTS ************** -->
 987       <!-- ***************************************** -->
 988       <!-- PROOF -->
 989       <xsl:when test="$name='proof'">
 990        <m:maction actiontype="toggle">
 991         <!-- CSC: next if until the annotationHelper can handle mactions -->
 992         <xsl:if test="not($explodeall)">
 993          <!-- Details hided (default) -->
 994          <m:mtable align="baseline 1" equalrows="false" columnalign="left">
 995           <m:mtr>
 996            <m:mtd>
 997             <m:mrow>
 998              <m:mtext mathcolor="Maroon">We&#x00a0;can&#x00a0;prove</m:mtext>
 999              <m:mphantom><m:mtext>_</m:mtext></m:mphantom>
1000              <xsl:apply-templates select="*[position()=3]"/>
1001              <m:mrow>
1002               <m:mphantom><m:mtext>_</m:mtext></m:mphantom>
1003               <m:mtext mathcolor="Green">(explain)</m:mtext>
1004              </m:mrow>
1005             </m:mrow>
1006            </m:mtd>
1007           </m:mtr>
1008          </m:mtable>
1009         </xsl:if>
1010         <!-- Show details -->
1011         <m:mtable align="baseline 1" equalrows="false" columnalign="left">
1012          <m:mtr>
1013           <m:mtd>
1014            <m:mrow>
1015             <xsl:apply-templates select="*[position()=2]"/>
1016            </m:mrow>
1017           </m:mtd>
1018          </m:mtr>
1019          <m:mtr>
1020           <m:mtd>
1021            <m:mrow>
1022             <m:mtext mathcolor="Maroon">we&#x00a0;proved</m:mtext>
1023             <m:mphantom><m:mtext>_</m:mtext></m:mphantom>
1024             <xsl:apply-templates select="*[position()=3]"/>
1025             <m:mrow>
1026              <m:mphantom>
1027               <m:mtext>_</m:mtext>
1028              </m:mphantom>
1029              <m:mtext mathcolor="Green">(hide&#x00a0;details)</m:mtext>
1030             </m:mrow>
1031            </m:mrow>
1032           </m:mtd>
1033          </m:mtr>
1034         </m:mtable>
1035        </m:maction>
1036       </xsl:when>
1037       <!-- LETIN1 -->
1038       <xsl:when test="$name='letin1'">
1039         <m:mtable align="baseline 1" equalrows="false" columnalign="left">
1040          <m:mtr>
1041           <m:mtd>
1042            <m:mrow>
1043             <xsl:apply-templates select="*[2]"/>
1044            </m:mrow>
1045           </m:mtd>
1046          </m:mtr>
1047          <m:mtr>
1048           <m:mtd>
1049            <m:mrow>
1050             <xsl:apply-templates select="*[3]"/>
1051            </m:mrow>
1052           </m:mtd>
1053          </m:mtr>
1054         </m:mtable>
1055       </xsl:when>
1056       <xsl:when test="$name='by_induction'">
1057        <m:mtable align="baseline 1" equalrows="false" columnalign="left">
1058         <m:mtr>
1059          <m:mtd>
1060           <m:mrow>
1061            <m:mtext mathcolor="red">We&#x00a0;prove</m:mtext>
1062            <m:mphantom><m:mtext>_</m:mtext></m:mphantom>
1063            <xsl:apply-templates select="../*[3]"/>
1064           </m:mrow>
1065          </m:mtd>
1066         </m:mtr>
1067         <m:mtr>
1068          <m:mtd>
1069           <m:mrow>
1070            <m:mtext mathcolor="red">by&#x00a0;induction&#x00a0;on</m:mtext>
1071            <m:mphantom><m:mtext>_</m:mtext></m:mphantom>
1072            <xsl:apply-templates
1073             select="*[position()=last()]/*[position()=last()]"/>
1074           </m:mrow>
1075          </m:mtd>
1076         </m:mtr>
1077         <m:mtr>
1078          <m:mtd>
1079           <m:mrow>
1080            <m:mtable align="baseline 1" equalrows="false" columnalign="left">
1081             <xsl:for-each select="*[position()>3 and not(position()=last())]">
1082              <m:mtr>
1083               <m:mtd>
1084                <m:mrow>
1085                 <xsl:apply-templates select="."/>
1086                </m:mrow>
1087               </m:mtd>
1088              </m:mtr>
1089             </xsl:for-each>
1090            </m:mtable>
1091           </m:mrow>
1092          </m:mtd>
1093         </m:mtr>
1094        </m:mtable>
1095       </xsl:when>
1096       <!-- inductive_case -->
1097       <xsl:when test="$name='inductive_case'">
1098        <m:mtable align="baseline 1" equalrows="false" columnalign="left">
1099         <m:mtr>
1100          <m:mtd>
1101           <m:mrow>
1102            <m:mtext mathcolor="red">Case</m:mtext>
1103            <m:mphantom><m:mtext>_</m:mtext></m:mphantom>
1104            <xsl:apply-templates select="*[2]"/>
1105           </m:mrow>
1106          </m:mtd>
1107         </m:mtr>
1108         <m:mtr>
1109          <m:mtd>
1110           <m:mrow>
1111            <m:mphantom><m:mtext>_</m:mtext></m:mphantom>
1112            <m:mtable align="baseline 1" equalrows="false" columnalign="left">
1113             <xsl:if test="*[3]/*[position()>1]">
1114              <m:mtr>
1115               <m:mtd>
1116                <m:mrow>
1117                 <m:mtext mathcolor="red">By&#x00a0;induction&#x00a0;hypothesis,&#x00a0;we&#x00a0;have:</m:mtext>
1118                </m:mrow>
1119               </m:mtd>
1120              </m:mtr>
1121              <m:mtr>
1122               <m:mtd>
1123                <m:mrow>
1124                 <m:mphantom><m:mtext>_</m:mtext></m:mphantom>
1125                 <xsl:for-each select="*[3]/*[position()>1]">
1126                  <m:mo stretchy="false">(</m:mo>
1127                  <xsl:apply-templates select="m:ci"/>
1128                  <m:mo stretchy="false">) </m:mo>
1129                  <m:mphantom><m:mtext>_</m:mtext></m:mphantom>
1130                  <xsl:apply-templates select="m:type"/>
1131                 </xsl:for-each>
1132                </m:mrow>
1133               </m:mtd>
1134              </m:mtr>
1135             </xsl:if>
1136             <m:mtr>
1137              <m:mtd>
1138               <m:mrow>
1139                <xsl:apply-templates select="*[4]"/>
1140               </m:mrow>
1141              </m:mtd>
1142             </m:mtr>
1143            </m:mtable>
1144           </m:mrow>
1145          </m:mtd>
1146         </m:mtr>
1147        </m:mtable>
1148       </xsl:when>
1149       <!-- case_lhs  -->
1150       <xsl:when test="$name='case_lhs'">
1151        <m:mrow>
1152         <xsl:choose>
1153          <xsl:when test="count(*)=2">
1154           <xsl:apply-templates select="*[2]"/>
1155          </xsl:when>
1156          <xsl:otherwise>
1157           <m:mo stretchy="false">(</m:mo>
1158           <xsl:apply-templates select="*[2]"/>
1159           <xsl:for-each select="m:bvar">
1160            <m:mphantom><m:mtext>_</m:mtext></m:mphantom>
1161            <xsl:apply-templates select="*[1]"/>
1162            <m:mtext>:</m:mtext>
1163            <xsl:apply-templates select="m:type/*[1]"/>
1164           </xsl:for-each>
1165           <m:mo stretchy="false">)</m:mo>
1166          </xsl:otherwise>
1167         </xsl:choose>
1168        </m:mrow>
1169       </xsl:when>
1170       <!-- false_ind  -->
1171       <xsl:when test="$name='false_ind'">
1172        <m:mtable align="baseline 1" equalrows="false" columnalign="left">
1173         <m:mtr>
1174          <m:mtd>
1175           <m:mrow>
1176            <xsl:apply-templates select="*[3]"/>
1177           </m:mrow>
1178          </m:mtd>
1179         </m:mtr>
1180         <m:mtr>
1181          <m:mtd>
1182           <m:mrow>
1183            <m:mtext mathcolor="Red">Contradiction.</m:mtext>
1184           </m:mrow>
1185          </m:mtd>
1186         </m:mtr>
1187        </m:mtable>
1188       </xsl:when>
1189       <!-- LET-IN -->
1190       <xsl:when test="$name='letin'">
1191         <m:mtable align="baseline 1" equalrows="false" columnalign="left">
1192          <!-- <xsl:for-each select="APPLY[m:csymbol and (string(m:csymbol)='let')]"> -->
1193          <xsl:for-each select="*[(last() > position()) and (position()>1)]">
1194          <m:mtr>
1195           <m:mtd>
1196            <m:mrow>
1197             <xsl:apply-templates select="."/>
1198            </m:mrow>
1199           </m:mtd>
1200          </m:mtr>
1201          </xsl:for-each>
1202          <m:mtr>
1203           <m:mtd>
1204            <m:mrow>
1205             <xsl:apply-templates select="*[position()=last()]"/>
1206            </m:mrow>
1207           </m:mtd>
1208          </m:mtr>
1209         </m:mtable>
1210       </xsl:when>
1211       <!-- LET -->
1212       <xsl:when test="$name='let'">
1213        <m:mtext>(</m:mtext>
1214        <xsl:apply-templates select="m:ci"/>
1215        <m:mtext>) </m:mtext>
1216        <xsl:apply-templates select="*[3]"/>
1217       </xsl:when>
1218       <!-- RW_STEP -->
1219       <xsl:when test="$name='rw_step'">
1220         <m:mtable align="baseline 1" equalrows="false" columnalign="left">
1221          <m:mtr>
1222           <m:mtd>
1223            <m:mrow>
1224             <xsl:choose>
1225              <xsl:when test="name(*[2])='m:apply'">
1226               <xsl:apply-templates select="*[2]"/>
1227              </xsl:when>
1228              <xsl:otherwise>
1229               <m:mtext>Consider</m:mtext>
1230               <m:mphantom><m:mtext>_</m:mtext></m:mphantom>
1231               <xsl:apply-templates select="*[2]"/>
1232              </xsl:otherwise>
1233             </xsl:choose>
1234            </m:mrow>
1235           </m:mtd>
1236          </m:mtr>
1237          <m:mtr>
1238           <m:mtd>
1239            <m:mrow>
1240             <m:mtext>Rewrite</m:mtext>
1241             <m:mphantom><m:mtext>_</m:mtext></m:mphantom>
1242             <xsl:apply-templates select="*[3]"/>
1243             <m:mphantom><m:mtext>_</m:mtext></m:mphantom>
1244             <m:mtext>with</m:mtext>
1245             <m:mphantom><m:mtext>_</m:mtext></m:mphantom>
1246             <xsl:apply-templates select="*[4]"/>
1247             <m:mphantom><m:mtext>_</m:mtext></m:mphantom>
1248             <m:mtext>by</m:mtext>
1249             <m:mphantom><m:mtext>_</m:mtext></m:mphantom>
1250             <xsl:apply-templates select="*[5]"/>
1251            </m:mrow>
1252           </m:mtd>
1253          </m:mtr>
1254         </m:mtable>
1255       </xsl:when>
1256       <!-- not existing any more
1257       <xsl:when test="$name='thread'">
1258         <m:mtable align="baseline 1" equalrows="false" columnalign="left">
1259          <m:mtr>
1260           <m:mtd>
1261            <m:mrow>
1262             <xsl:choose>
1263              <xsl:when test="name(*[last()])='m:apply'">
1264               <xsl:apply-templates select="*[last()]"/>
1265              </xsl:when>
1266              <xsl:otherwise>
1267               <m:mtext>Consider</m:mtext>
1268               <m:mphantom><m:mtext>_</m:mtext></m:mphantom>
1269               <xsl:apply-templates select="*[last()]"/>
1270              </xsl:otherwise>
1271             </xsl:choose>
1272            </m:mrow>
1273           </m:mtd>
1274          </m:mtr>
1275          <xsl:apply-templates mode="thread" select="*[(last()-2)]"/>
1276         </m:mtable>
1277       </xsl:when>
1278       -->
1279       <!-- REWRITE_AND_APPLY -->
1280       <xsl:when test="$name='rewrite_and_apply'">
1281         <m:mtable align="baseline 1" equalrows="false" columnalign="left">
1282          <m:mtr>
1283           <m:mtd>
1284            <m:mrow>
1285             <xsl:apply-templates select="*[2]"/>
1286            </m:mrow>
1287           </m:mtd>
1288          </m:mtr>
1289          <m:mtr>
1290           <m:mtd>
1291            <m:mrow>
1292             <m:mtext>Then&#x00a0;apply&#x00a0;it&#x00a0;to</m:mtext>
1293             <m:mphantom><m:mtext>_</m:mtext></m:mphantom>
1294             <xsl:apply-templates select="*[position()>2]"/>
1295            </m:mrow>
1296           </m:mtd>
1297          </m:mtr>
1298        </m:mtable>
1299       </xsl:when>
1300       <!-- AND_IND -->
1301       <xsl:when test="$name='and_ind'">
1302         <m:mtable align="baseline 1" equalrows="false" columnalign="left">
1303          <m:mtr>
1304           <m:mtd>
1305            <m:mrow>
1306             <xsl:choose>
1307              <xsl:when test="name(*[2])='m:apply'">
1308               <xsl:apply-templates select="*[2]"/>
1309              </xsl:when>
1310              <xsl:otherwise>
1311               <m:mtext>Consider</m:mtext>
1312               <m:mphantom><m:mtext>_</m:mtext></m:mphantom>
1313               <xsl:apply-templates select="*[2]"/>
1314              </xsl:otherwise>
1315             </xsl:choose>
1316            </m:mrow>
1317           </m:mtd>
1318          </m:mtr>
1319          <m:mtr>
1320           <m:mtd>
1321            <m:mrow>
1322             <m:mtext>In&#x00a0;particular,&#x00a0;we&#x00a0;have</m:mtext>
1323            </m:mrow>
1324           </m:mtd>
1325          </m:mtr>
1326          <m:mtr>
1327           <m:mtd>
1328            <m:mrow>
1329             <m:mtext>(</m:mtext>
1330             <xsl:apply-templates select="*[3]"/>
1331             <m:mtext>)</m:mtext>
1332             <m:mphantom><m:mtext>_</m:mtext></m:mphantom>
1333             <xsl:apply-templates select="*[4]"/>
1334             </m:mrow>
1335           </m:mtd>
1336          </m:mtr>
1337          <m:mtr>
1338           <m:mtd>
1339            <m:mrow>
1340             <m:mtext>(</m:mtext>
1341             <xsl:apply-templates select="*[5]"/>
1342             <m:mtext>)</m:mtext>
1343             <m:mphantom><m:mtext>_</m:mtext></m:mphantom>
1344             <xsl:apply-templates select="*[6]"/>
1345             </m:mrow>
1346           </m:mtd>
1347          </m:mtr>
1348          <m:mtr>
1349           <m:mtd>
1350            <m:mrow>
1351             <xsl:apply-templates select="*[7]"/>
1352            </m:mrow>
1353           </m:mtd>
1354          </m:mtr>
1355         </m:mtable>
1356       </xsl:when>
1357       <!-- full_or_ind -->
1358       <xsl:when test="$name='full_or_ind'">
1359         <m:mtable align="baseline 1" equalrows="false" columnalign="left">
1360          <m:mtr>
1361           <m:mtd>
1362            <m:mrow>
1363             <xsl:choose>
1364              <xsl:when test="name(*[2])='m:apply'">
1365               <xsl:apply-templates select="*[2]"/>
1366              </xsl:when>
1367              <xsl:otherwise>
1368               <m:mtext>Consider</m:mtext>
1369               <m:mphantom><m:mtext>_</m:mtext></m:mphantom>
1370               <xsl:apply-templates select="*[2]"/>
1371              </xsl:otherwise>
1372             </xsl:choose>
1373            </m:mrow>
1374           </m:mtd>
1375          </m:mtr>
1376          <m:mtr>
1377           <m:mtd>
1378            <m:mrow>
1379             <m:mtext>We&#x00a0;proceed&#x00a0;by&#x00a0;cases&#x00a0;to&#x00a0;prove</m:mtext>
1380             <m:mphantom><m:mtext>_</m:mtext></m:mphantom>
1381             <xsl:apply-templates select="*[3]"/>
1382            </m:mrow>
1383           </m:mtd>
1384          </m:mtr>
1385          <m:mtr>
1386           <m:mtd>
1387            <m:mrow>
1388             <m:mtext>Left:&#x00a0;suppose</m:mtext>
1389             <m:mphantom><m:mtext>_</m:mtext></m:mphantom>
1390             <m:mo stretchy="false">(</m:mo>
1391             <xsl:apply-templates select="*[4]/m:bvar/m:ci"/>
1392             <m:mo stretchy="false">)</m:mo>
1393             <m:mphantom><m:mtext>_</m:mtext></m:mphantom>
1394             <xsl:apply-templates select="*[4]/m:bvar/m:type/*[1]"/>
1395            </m:mrow>
1396           </m:mtd>
1397          </m:mtr>
1398          <m:mtr>
1399           <m:mtd>
1400            <m:mrow>
1401             <m:mphantom><m:mtext>_</m:mtext></m:mphantom>
1402             <xsl:apply-templates select="*[4]/*[3]"/>
1403            </m:mrow>
1404           </m:mtd>
1405          </m:mtr>
1406          <m:mtr>
1407           <m:mtd>
1408            <m:mrow>
1409             <m:mtext>Right:&#x00a0;suppose</m:mtext>
1410             <m:mphantom><m:mtext>_</m:mtext></m:mphantom>
1411             <m:mo stretchy="false">(</m:mo>
1412             <xsl:apply-templates select="*[5]/m:bvar/m:ci"/>
1413             <m:mo stretchy="false">)</m:mo>
1414             <m:mphantom><m:mtext>_</m:mtext></m:mphantom>
1415             <xsl:apply-templates select="*[5]/m:bvar/m:type/*[1]"/>
1416            </m:mrow>
1417           </m:mtd>
1418          </m:mtr>
1419          <m:mtr>
1420           <m:mtd>
1421            <m:mrow>
1422             <xsl:apply-templates select="*[5]/*[3]"/>
1423            </m:mrow>
1424           </m:mtd>
1425          </m:mtr>
1426         </m:mtable>
1427       </xsl:when>
1428       <!-- OR_IND -->
1429       <xsl:when test="$name='or_ind'">
1430         <m:mtable align="baseline 1" equalrows="false" columnalign="left">
1431          <m:mtr>
1432           <m:mtd>
1433            <m:mrow>
1434             <xsl:choose>
1435              <xsl:when test="name(*[2])='m:apply'">
1436               <xsl:apply-templates select="*[2]"/>
1437              </xsl:when>
1438              <xsl:otherwise>
1439               <m:mtext>Consider</m:mtext>
1440               <m:mphantom><m:mtext>_</m:mtext></m:mphantom>
1441               <xsl:apply-templates select="*[2]"/>
1442              </xsl:otherwise>
1443             </xsl:choose>
1444            </m:mrow>
1445           </m:mtd>
1446          </m:mtr>
1447          <m:mtr>
1448           <m:mtd>
1449            <m:mrow>
1450             <m:mtext>We&#x00a0;prove</m:mtext>
1451             <m:mphantom><m:mtext>_</m:mtext></m:mphantom>
1452             <xsl:apply-templates select="*[3]"/>
1453             <m:mphantom><m:mtext>_</m:mtext></m:mphantom>
1454             <m:mtext>by&#x00a0;cases:</m:mtext>
1455            </m:mrow>
1456           </m:mtd>
1457          </m:mtr>
1458          <m:mtr>
1459           <m:mtd>
1460            <m:mrow>
1461             <m:mtext>Left</m:mtext>
1462             <xsl:apply-templates select="*[4]"/>
1463            </m:mrow>
1464           </m:mtd>
1465          </m:mtr>
1466          <m:mtr>
1467           <m:mtd>
1468            <m:mrow>
1469             <m:mtext>Right</m:mtext>
1470             <xsl:apply-templates select="*[5]"/>
1471            </m:mrow>
1472           </m:mtd>
1473          </m:mtr>
1474         </m:mtable>
1475       </xsl:when>
1476       <!-- EX_IND -->
1477       <xsl:when test="$name='ex_ind'">
1478         <m:mtable align="baseline 1" equalrows="false" columnalign="left">
1479          <m:mtr>
1480           <m:mtd>
1481            <m:mrow>
1482             <xsl:choose>
1483              <xsl:when test="name(*[2])='m:apply'">
1484               <xsl:apply-templates select="*[2]"/>
1485              </xsl:when>
1486              <xsl:otherwise>
1487               <m:mtext>Consider</m:mtext>
1488               <m:mphantom><m:mtext>_</m:mtext></m:mphantom>
1489               <xsl:apply-templates select="*[2]"/>
1490              </xsl:otherwise>
1491             </xsl:choose>
1492            </m:mrow>
1493           </m:mtd>
1494          </m:mtr>
1495          <m:mtr>
1496           <m:mtd>
1497            <m:mrow>
1498             <m:mtext>Let</m:mtext>
1499             <m:mphantom><m:mtext>_</m:mtext></m:mphantom>
1500             <xsl:apply-templates select="*[3]"/>
1501             <m:mtext>:</m:mtext>
1502             <xsl:apply-templates select="*[4]"/>
1503             <m:mphantom><m:mtext>_</m:mtext></m:mphantom>
1504             <m:mtext>such&#x00a0;that</m:mtext>
1505             <m:mphantom><m:mtext>_</m:mtext></m:mphantom>
1506             <m:mtext>(</m:mtext>
1507              <xsl:apply-templates select="*[5]"/>
1508             <m:mtext>)</m:mtext>
1509             <m:mphantom><m:mtext>_</m:mtext></m:mphantom>
1510             <xsl:apply-templates select="*[6]"/>
1511            </m:mrow>
1512           </m:mtd>
1513          </m:mtr>
1514          <m:mtr>
1515           <m:mtd>
1516            <m:mrow>
1517             <xsl:apply-templates select="*[7]"/>
1518            </m:mrow>
1519           </m:mtd>
1520          </m:mtr>
1521         </m:mtable>
1522       </xsl:when>
1523       <!-- ERROR -->
1524       <xsl:otherwise>
1525        <m:mi>ERROR</m:mi>
1526       </xsl:otherwise>
1527      </xsl:choose>
1528     </m:mrow>
1529 </xsl:template>
1530
1531 <!-- Il modo Thread non esiste piu'
1532 <xsl:template match="*" mode="thread">
1533  <xsl:variable name="name"><xsl:value-of select="following-sibling::*[position()=1]/m:csymbol"/></xsl:variable>
1534  <xsl:choose>
1535   <xsl:when test="$name='rw_step'">
1536          <m:mtr>
1537           <m:mtd>
1538            <m:mrow>
1539             <m:mtext>Rewrite</m:mtext>
1540             <m:mphantom><m:mtext>_</m:mtext></m:mphantom>
1541             <xsl:apply-templates select="following-sibling::*[position()=1]/*[2]"/>
1542             <m:mphantom><m:mtext>_</m:mtext></m:mphantom>
1543             <m:mtext>with</m:mtext>
1544             <m:mphantom><m:mtext>_</m:mtext></m:mphantom>
1545             <xsl:apply-templates select="following-sibling::*[position()=1]/*[3]"/>
1546             <m:mphantom><m:mtext>_</m:mtext></m:mphantom>
1547             <m:mtext>by</m:mtext>
1548             <m:mphantom><m:mtext>_</m:mtext></m:mphantom>
1549             <xsl:apply-templates select="following-sibling::*[position()=1]/*[4]"/>
1550            </m:mrow>
1551           </m:mtd>
1552          </m:mtr>
1553          <m:mtr>
1554           <m:mtd>
1555            <m:mrow>
1556             <m:mtext mathcolor="Maroon">we&#x00a0;get</m:mtext>
1557             <m:mphantom><m:mtext>_</m:mtext></m:mphantom>
1558             <xsl:apply-templates select="."/>
1559            </m:mrow>
1560           </m:mtd>
1561          </m:mtr>
1562    </xsl:when>
1563    <xsl:otherwise>
1564          <m:mtr>
1565           <m:mtd>
1566            <m:mrow>
1567             <xsl:apply-templates select="following-sibling::*[position()=1]"/>
1568            </m:mrow>
1569           </m:mtd>
1570          </m:mtr>
1571          <m:mtr>
1572           <m:mtd>
1573            <m:mrow>
1574             <m:mtext mathcolor="Maroon">we&#x00a0;get</m:mtext>
1575             <m:mphantom><m:mtext>_</m:mtext></m:mphantom>
1576             <xsl:apply-templates select="."/>
1577            </m:mrow>
1578           </m:mtd>
1579          </m:mtr>
1580     </xsl:otherwise>
1581    </xsl:choose>
1582          <xsl:apply-templates mode="thread" select="preceding-sibling::*[position()=2]"/>
1583 </xsl:template>
1584 -->
1585
1586 <!-- LAMBDA -->
1587
1588 <xsl:template match="m:lambda">
1589     <xsl:variable name="charlength"><xsl:apply-templates select="*[position()=1]" mode="charcount"/></xsl:variable>
1590     <m:mrow m:xref="{@id}">
1591      <xsl:choose>
1592      <xsl:when test="$charlength >= $framewidth">
1593       <m:mtable align="baseline 1" equalrows="false" columnalign="left">
1594         <m:mtr>
1595           <m:mtd>
1596            <m:mrow>
1597             <m:mo mathcolor="Red">&#x03bb;</m:mo>
1598             <xsl:apply-templates select="m:bvar"/>
1599            </m:mrow>
1600           </m:mtd>
1601          </m:mtr>
1602        <m:mtr>
1603         <m:mtd>
1604          <m:mrow>
1605           <m:mo>.</m:mo>
1606           <xsl:apply-templates select="*[position()=2]"/>
1607          </m:mrow>
1608         </m:mtd>
1609        </m:mtr>
1610       </m:mtable>
1611      </xsl:when>
1612      <xsl:otherwise>
1613       <m:mo mathcolor="Red">&#x03bb;</m:mo>
1614       <xsl:apply-templates select="m:bvar/m:ci"/>
1615       <m:mo>:</m:mo>
1616       <xsl:apply-templates select="m:bvar/m:type"/>
1617       <m:mo>.</m:mo>
1618       <xsl:apply-templates select="*[position()=2]"/>
1619      </xsl:otherwise>
1620      </xsl:choose>
1621     </m:mrow>
1622 </xsl:template>
1623
1624 <!-- *********************************** -->
1625 <!-- BASE SET OF MATHML CONTENT ELEMENTS -->
1626 <!-- *********************************** -->
1627
1628 <!-- Logic -->
1629
1630 <xsl:template match = "m:apply[m:eq[1]]">
1631  <xsl:variable name="charlength">
1632   <xsl:apply-templates select="*[1]" mode="charcount"/>
1633  </xsl:variable>
1634  <xsl:choose>
1635   <xsl:when test="$charlength >= $framewidth">
1636    <m:mtable align="baseline 1" equalrows="false" columnalign="left">
1637     <xsl:if test="@helm:xref">
1638      <xsl:attribute name="m:xref">
1639       <xsl:value-of select="@id"/>
1640      </xsl:attribute>
1641     </xsl:if>
1642     <m:mtr>
1643      <m:mtd>
1644       <m:mrow>
1645        <m:mo stretchy="false">(</m:mo>
1646        <xsl:apply-templates select="*[position()=2]"/>
1647       </m:mrow>
1648      </m:mtd>
1649     </m:mtr>
1650     <xsl:for-each select = "*[position()>2]">
1651      <m:mtr>
1652       <m:mtd>
1653        <m:mrow>
1654         <m:mphantom><m:mtext>__</m:mtext></m:mphantom>
1655         <m:mo m:xref="{m:in/@id}">=</m:mo>
1656         <xsl:apply-templates select="."/>
1657        </m:mrow>
1658       </m:mtd>
1659      </m:mtr>
1660     </xsl:for-each>
1661     <m:mtr>
1662      <m:mtd>
1663       <m:mrow>
1664        <m:mo stretchy="false">)</m:mo>
1665       </m:mrow>
1666      </m:mtd>
1667     </m:mtr>
1668    </m:mtable>
1669   </xsl:when>
1670   <xsl:otherwise>
1671    <xsl:apply-imports/>
1672   </xsl:otherwise>
1673  </xsl:choose>
1674 </xsl:template>
1675
1676
1677 <xsl:template match = "m:apply[m:and[1]|m:or[1]
1678           |m:geq[1]|m:leq[1]|m:gt[1]|m:lt[1]
1679           |m:in[1]|m:intesect[1]|m:union[1]|m:subset[1]
1680           |m:prsubset|m:setdiff[1]]">
1681  <xsl:variable name="symbol">
1682   <xsl:choose>
1683    <xsl:when test="m:and[1]">
1684     <xsl:value-of select="'&#8743;'"/>
1685    </xsl:when>
1686    <xsl:when test="m:or[1]">
1687     <xsl:value-of select="'&#8744;'"/>
1688    </xsl:when>
1689    <xsl:when test="m:geq[1]">
1690     <xsl:value-of select="'&#8805;'"/>
1691    </xsl:when>
1692    <xsl:when test="m:leq[1]">
1693     <xsl:value-of select="'&#8804;'"/>
1694    </xsl:when>
1695    <xsl:when test="m:gt[1]">
1696     <xsl:value-of select="'&#62;'"/>
1697    </xsl:when>
1698    <xsl:when test="m:lt[1]">
1699     <xsl:value-of select="'&#60;&#32;'"/>
1700    </xsl:when>
1701    <xsl:when test="m:eq[1]">
1702     <xsl:value-of select="'&#61;'"/>
1703    </xsl:when>
1704    <xsl:when test="m:in[1]">
1705     <xsl:value-of select="'&#x02208;'"/>
1706    </xsl:when>
1707    <xsl:when test="m:subset[1]">
1708     <xsl:value-of select="'&#x02286;'"/>
1709    </xsl:when>
1710    <xsl:when test="m:prsubset[1]">
1711     <xsl:value-of select="'&#x02282;'"/>
1712    </xsl:when>
1713    <xsl:when test="m:intersect[1]">
1714     <xsl:value-of select="'&#x022C2;'"/>
1715    </xsl:when>
1716    <xsl:when test="m:union[1]">
1717     <xsl:value-of select="'&#x022C3;'"/>
1718    </xsl:when>
1719    <xsl:when test="m:setdiff[1]">
1720     <xsl:value-of select="'&#x02216;'"/>
1721    </xsl:when>
1722   </xsl:choose>
1723  </xsl:variable>
1724  <xsl:variable name="charlength">
1725   <xsl:apply-templates select="*[1]" mode="charcount"/>
1726  </xsl:variable>
1727  <xsl:choose>
1728   <xsl:when test="$charlength >= $framewidth">
1729    <m:mtable align="baseline 1" equalrows="false" columnalign="left">
1730     <xsl:if test="@helm:xref">
1731      <xsl:attribute name="m:xref">
1732       <xsl:value-of select="@id"/>
1733      </xsl:attribute>
1734     </xsl:if>
1735     <m:mtr>
1736      <m:mtd>
1737       <m:mrow>
1738        <m:mo stretchy="false">(</m:mo>
1739        <xsl:apply-templates select="*[position()=2]"/>
1740       </m:mrow>
1741      </m:mtd>
1742     </m:mtr>
1743     <xsl:for-each select = "*[position()>2]">
1744      <m:mtr>
1745       <m:mtd>
1746        <m:mrow>
1747         <m:mphantom><m:mtext>__</m:mtext></m:mphantom>
1748         <m:mo m:xref="{*[1]/@id}"><xsl:value-of select="$symbol"/></m:mo>
1749         <xsl:apply-templates select="."/>
1750        </m:mrow>
1751       </m:mtd>
1752      </m:mtr>
1753     </xsl:for-each>
1754     <m:mtr>
1755      <m:mtd>
1756       <m:mrow>
1757        <m:mo stretchy="false">)</m:mo>
1758       </m:mrow>
1759      </m:mtd>
1760     </m:mtr>
1761    </m:mtable>
1762   </xsl:when>
1763   <xsl:otherwise>
1764    <xsl:apply-imports/>
1765   </xsl:otherwise>
1766  </xsl:choose>
1767 </xsl:template>
1768
1769 <xsl:template match = "m:set">
1770  <xsl:choose>
1771   <xsl:when test="count(child::*) = 0">
1772    <m:mi>&#x02205;</m:mi>
1773   </xsl:when>
1774   <xsl:otherwise>
1775    <xsl:variable name="charlength">
1776     <xsl:apply-templates select="*[1]" mode="charcount"/>
1777    </xsl:variable>
1778    <xsl:choose>
1779     <xsl:when test="$charlength >= $framewidth">
1780      <xsl:choose>
1781       <xsl:when test="name(*[1]) = 'm:bvar'">
1782        <m:mtable align="baseline 1" equalrows="false" columnalign="left">
1783         <m:mtr>
1784          <m:mtd>
1785           <m:mrow>
1786            <m:mo stretchy="false">{</m:mo>
1787            <xsl:apply-templates select="*[position()=1]"/>
1788           </m:mrow>
1789          </m:mtd>
1790         </m:mtr>
1791         <m:mtr>
1792          <m:mtd>
1793           <m:mrow>
1794            <m:mphantom><m:mtext>{</m:mtext></m:mphantom>
1795            <m:mo stretchy="false">|</m:mo>
1796            <xsl:apply-templates select="m:condition/*[1]"/>
1797           </m:mrow>
1798          </m:mtd>
1799         </m:mtr>
1800         <m:mtr>
1801          <m:mtd>
1802           <m:mrow>
1803            <m:mo stretchy="false">}</m:mo>
1804           </m:mrow>
1805          </m:mtd>
1806         </m:mtr>
1807        </m:mtable>
1808       </xsl:when>
1809       <xsl:otherwise>
1810        <m:mtable align="baseline 1" equalrows="false" columnalign="left">
1811         <m:mtr>
1812          <m:mtd>
1813           <m:mrow>
1814            <m:mo stretchy="false">{</m:mo>
1815            <xsl:apply-templates select="*[position()=1]"/>
1816            <xsl:if test="position() != last()">
1817             <mo>,</mo>
1818            </xsl:if>
1819           </m:mrow>
1820          </m:mtd>
1821         </m:mtr>
1822         <xsl:for-each select = "*[position()>2]">
1823          <m:mtr>
1824           <m:mtd>
1825            <m:mrow>
1826             <m:mphantom><m:mtext>{</m:mtext></m:mphantom>
1827             <xsl:apply-templates select="."/>
1828             <xsl:if test="position() != last()">
1829              <mo>,</mo>
1830             </xsl:if>
1831            </m:mrow>
1832           </m:mtd>
1833          </m:mtr>
1834         </xsl:for-each>
1835         <m:mtr>
1836          <m:mtd>
1837           <m:mrow>
1838            <m:mo stretchy="false">}</m:mo>
1839           </m:mrow>
1840          </m:mtd>
1841         </m:mtr>
1842        </m:mtable>
1843       </xsl:otherwise>
1844      </xsl:choose>
1845     </xsl:when>
1846     <xsl:otherwise>
1847      <xsl:apply-imports/>
1848     </xsl:otherwise>
1849    </xsl:choose>
1850   </xsl:otherwise>
1851  </xsl:choose>
1852 </xsl:template>
1853
1854 <xsl:template match = "m:apply[m:card[1]]">
1855   <m:mfenced open="|" close="|" stretchy="false">
1856     <xsl:if test="($SEM_SW=$SEM_XREF or $SEM_SW=$SEM_XREF_EXT) and @id">
1857       <xsl:attribute name="m:xref">
1858         <xsl:value-of select="@id"/>
1859       </xsl:attribute>
1860     </xsl:if>
1861   <xsl:apply-templates select="*[2]"/>
1862   </m:mfenced>
1863 </xsl:template>
1864
1865 <!-- *********************************** -->
1866 <!--          PROOF ELEMENTS             -->
1867 <!-- *********************************** -->
1868
1869
1870
1871 <!--**********************-->
1872 <!--       COUNTING       -->
1873 <!--**********************-->
1874
1875 <xsl:template match="m:cn|m:and|m:or|m:not|m:exists|m:eq|m:lt|m:leq|m:gt|m:geq
1876  |m:in|m:notin|m:intersect|m:union|m:subset|m:prsubset|m:card|m:setdiff
1877  |m:plus|m:minus|m:times" mode="charcount">
1878 <xsl:param name="incurrent_length" select="0"/>
1879     <xsl:choose>
1880     <xsl:when test="$framewidth > ($incurrent_length + 3 + string-length())">
1881      <xsl:variable name="siblength">
1882       <xsl:apply-templates select="following-sibling::*[position()=1]" mode="charcount">
1883        <xsl:with-param name="incurrent_length" select="$incurrent_length + string-length()"/>
1884       </xsl:apply-templates>
1885      </xsl:variable>
1886      <xsl:choose>
1887      <xsl:when test="string($siblength) = &quot;&quot;">
1888       <xsl:value-of select="$incurrent_length + 3 + string-length()"/>
1889      </xsl:when>
1890      <xsl:otherwise>
1891       <xsl:value-of select="number($siblength)"/>
1892      </xsl:otherwise>
1893      </xsl:choose>
1894     </xsl:when>
1895     <xsl:otherwise>
1896      <xsl:value-of select="$incurrent_length + 3 + string-length()"/>
1897     </xsl:otherwise>
1898     </xsl:choose>
1899 </xsl:template>
1900
1901 <xsl:template match="m:ci|m:csymbol" mode="charcount">
1902 <xsl:param name="incurrent_length" select="0"/>
1903 <xsl:param name="nosibling" select="0"/>
1904     <xsl:choose>
1905     <xsl:when test="$framewidth > ($incurrent_length + string-length()) and ($nosibling = 0)">
1906      <xsl:variable name="siblength"><xsl:apply-templates select="following-sibling::*[position()=1]" mode="charcount"><xsl:with-param name="incurrent_length" select="$incurrent_length + string-length()"/></xsl:apply-templates></xsl:variable>
1907      <xsl:choose>
1908      <xsl:when test="string($siblength) = &quot;&quot;">
1909       <xsl:value-of select="$incurrent_length + string-length()"/>
1910      </xsl:when>
1911      <xsl:otherwise>
1912       <xsl:value-of select="number($siblength)"/>
1913      </xsl:otherwise>
1914      </xsl:choose>
1915     </xsl:when>
1916     <xsl:otherwise>
1917      <xsl:value-of select="$incurrent_length + string-length()"/>
1918     </xsl:otherwise>
1919     </xsl:choose>
1920 </xsl:template>
1921
1922 <xsl:template match="*" mode="charcount">
1923 <xsl:param name="incurrent_length" select="0"/>
1924 <xsl:param name="nosibling" select="0"/>
1925  <xsl:choose>
1926   <xsl:when test="count(child::*) = 0">
1927    <xsl:value-of select="$incurrent_length"/>
1928   </xsl:when>
1929   <xsl:otherwise>
1930     <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>
1931     <xsl:choose>
1932     <xsl:when test="$framewidth > number($childlength) and ($nosibling = 0)">
1933      <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>
1934      <xsl:choose>
1935      <xsl:when test="string($siblength) = &quot;&quot;">
1936       <xsl:value-of select="number($childlength)"/>
1937      </xsl:when>
1938      <xsl:otherwise>
1939       <xsl:value-of select="number($siblength)"/>
1940      </xsl:otherwise>
1941      </xsl:choose>
1942     </xsl:when>
1943     <xsl:otherwise>
1944      <xsl:value-of select="number($childlength)"/>
1945     </xsl:otherwise>
1946     </xsl:choose>
1947   </xsl:otherwise>
1948  </xsl:choose>
1949 </xsl:template>
1950
1951 </xsl:stylesheet>