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