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