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