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         <!-- CSC: $explodeall until the annotationHelper can handle mactions -->
 992         <xsl:variable name="test" select="(not($explodeall)) and
 993            (not(preceding-sibling::*[1]/text()='letin1')) and
 994            (not(preceding-sibling::*[1]/text()='rw_step')) and
 995            (not(name(..)='m:lambda'))"/>
 996         <xsl:variable name="hidden_details">
 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         </xsl:variable>
1016         <xsl:variable name="shown_details">
1017          <!-- Show details -->
1018          <m:mtable align="baseline 1" equalrows="false" columnalign="left">
1019           <m:mtr>
1020            <m:mtd>
1021             <m:mrow>
1022              <xsl:apply-templates select="*[position()=2]"/>
1023             </m:mrow>
1024            </m:mtd>
1025           </m:mtr>
1026           <m:mtr>
1027            <m:mtd>
1028             <m:mrow>
1029              <m:mtext mathcolor="Maroon">we&#x00a0;proved</m:mtext>
1030              <m:mphantom><m:mtext>_</m:mtext></m:mphantom>
1031              <xsl:apply-templates select="*[position()=3]"/>
1032              <m:mrow>
1033               <m:mphantom>
1034                <m:mtext>_</m:mtext>
1035               </m:mphantom>
1036               <xsl:if test="$test">
1037                <m:mtext mathcolor="Green">(hide&#x00a0;details)</m:mtext>
1038               </xsl:if>
1039              </m:mrow>
1040             </m:mrow>
1041            </m:mtd>
1042           </m:mtr>
1043          </m:mtable>
1044         </xsl:variable>
1045         <xsl:choose>
1046          <xsl:when test="$test">
1047           <m:maction actiontype="toggle">
1048            <xsl:copy-of select="$hidden_details"/>
1049            <xsl:copy-of select="$shown_details"/>
1050           </m:maction>
1051          </xsl:when>
1052          <xsl:otherwise>
1053           <xsl:copy-of select="$shown_details"/>
1054          </xsl:otherwise>
1055         </xsl:choose>
1056       </xsl:when>
1057       <!-- LETIN1 -->
1058       <xsl:when test="$name='letin1'">
1059         <m:mtable align="baseline 1" equalrows="false" columnalign="left">
1060          <m:mtr>
1061           <m:mtd>
1062            <m:mrow>
1063             <xsl:apply-templates select="*[2]"/>
1064            </m:mrow>
1065           </m:mtd>
1066          </m:mtr>
1067          <m:mtr>
1068           <m:mtd>
1069            <m:mrow>
1070             <xsl:apply-templates select="*[3]"/>
1071            </m:mrow>
1072           </m:mtd>
1073          </m:mtr>
1074         </m:mtable>
1075       </xsl:when>
1076       <xsl:when test="$name='by_induction'">
1077        <m:mtable align="baseline 1" equalrows="false" columnalign="left">
1078         <m:mtr>
1079          <m:mtd>
1080           <m:mrow>
1081            <m:mtext mathcolor="red">We&#x00a0;prove</m:mtext>
1082            <m:mphantom><m:mtext>_</m:mtext></m:mphantom>
1083            <xsl:apply-templates select="../*[3]"/>
1084           </m:mrow>
1085          </m:mtd>
1086         </m:mtr>
1087         <m:mtr>
1088          <m:mtd>
1089           <m:mrow>
1090            <m:mtext mathcolor="red">by&#x00a0;induction&#x00a0;on</m:mtext>
1091            <m:mphantom><m:mtext>_</m:mtext></m:mphantom>
1092            <xsl:apply-templates
1093             select="*[position()=last()]/*[position()=last()]"/>
1094           </m:mrow>
1095          </m:mtd>
1096         </m:mtr>
1097         <m:mtr>
1098          <m:mtd>
1099           <m:mrow>
1100            <m:mtable align="baseline 1" equalrows="false" columnalign="left">
1101             <xsl:for-each select="*[position()>3 and not(position()=last())]">
1102              <m:mtr>
1103               <m:mtd>
1104                <m:mrow>
1105                 <xsl:apply-templates select="."/>
1106                </m:mrow>
1107               </m:mtd>
1108              </m:mtr>
1109             </xsl:for-each>
1110            </m:mtable>
1111           </m:mrow>
1112          </m:mtd>
1113         </m:mtr>
1114        </m:mtable>
1115       </xsl:when>
1116       <!-- inductive_case -->
1117       <xsl:when test="$name='inductive_case'">
1118        <m:mtable align="baseline 1" equalrows="false" columnalign="left">
1119         <m:mtr>
1120          <m:mtd>
1121           <m:mrow>
1122            <m:mtext mathcolor="red">Case</m:mtext>
1123            <m:mphantom><m:mtext>_</m:mtext></m:mphantom>
1124            <xsl:apply-templates select="*[2]"/>
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            <m:mtable align="baseline 1" equalrows="false" columnalign="left">
1133             <xsl:if test="*[3]/*[position()>1]">
1134              <m:mtr>
1135               <m:mtd>
1136                <m:mrow>
1137                 <m:mtext mathcolor="red">By&#x00a0;induction&#x00a0;hypothesis,&#x00a0;we&#x00a0;have:</m:mtext>
1138                </m:mrow>
1139               </m:mtd>
1140              </m:mtr>
1141              <m:mtr>
1142               <m:mtd>
1143                <m:mrow>
1144                 <m:mphantom><m:mtext>_</m:mtext></m:mphantom>
1145                 <xsl:for-each select="*[3]/*[position()>1]">
1146                  <m:mo stretchy="false">(</m:mo>
1147                  <xsl:apply-templates select="m:ci"/>
1148                  <m:mo stretchy="false">) </m:mo>
1149                  <m:mphantom><m:mtext>_</m:mtext></m:mphantom>
1150                  <xsl:apply-templates select="m:type"/>
1151                 </xsl:for-each>
1152                </m:mrow>
1153               </m:mtd>
1154              </m:mtr>
1155             </xsl:if>
1156             <m:mtr>
1157              <m:mtd>
1158               <m:mrow>
1159                <xsl:apply-templates select="*[4]"/>
1160               </m:mrow>
1161              </m:mtd>
1162             </m:mtr>
1163            </m:mtable>
1164           </m:mrow>
1165          </m:mtd>
1166         </m:mtr>
1167        </m:mtable>
1168       </xsl:when>
1169       <!-- case_lhs  -->
1170       <xsl:when test="$name='case_lhs'">
1171        <m:mrow>
1172         <xsl:choose>
1173          <xsl:when test="count(*)=2">
1174           <xsl:apply-templates select="*[2]"/>
1175          </xsl:when>
1176          <xsl:otherwise>
1177           <m:mo stretchy="false">(</m:mo>
1178           <xsl:apply-templates select="*[2]"/>
1179           <xsl:for-each select="m:bvar">
1180            <m:mphantom><m:mtext>_</m:mtext></m:mphantom>
1181            <xsl:apply-templates select="*[1]"/>
1182            <m:mtext>:</m:mtext>
1183            <xsl:apply-templates select="m:type/*[1]"/>
1184           </xsl:for-each>
1185           <m:mo stretchy="false">)</m:mo>
1186          </xsl:otherwise>
1187         </xsl:choose>
1188        </m:mrow>
1189       </xsl:when>
1190       <!-- false_ind  -->
1191       <xsl:when test="$name='false_ind'">
1192        <m:mtable align="baseline 1" equalrows="false" columnalign="left">
1193         <m:mtr>
1194          <m:mtd>
1195           <m:mrow>
1196            <xsl:apply-templates select="*[3]"/>
1197           </m:mrow>
1198          </m:mtd>
1199         </m:mtr>
1200         <m:mtr>
1201          <m:mtd>
1202           <m:mrow>
1203            <m:mtext mathcolor="Red">Contradiction.</m:mtext>
1204           </m:mrow>
1205          </m:mtd>
1206         </m:mtr>
1207        </m:mtable>
1208       </xsl:when>
1209       <!-- LET-IN -->
1210       <xsl:when test="$name='letin'">
1211         <m:mtable align="baseline 1" equalrows="false" columnalign="left">
1212          <!-- <xsl:for-each select="APPLY[m:csymbol and (string(m:csymbol)='let')]"> -->
1213          <xsl:for-each select="*[(last() > position()) and (position()>1)]">
1214          <m:mtr>
1215           <m:mtd>
1216            <m:mrow>
1217             <xsl:apply-templates select="."/>
1218            </m:mrow>
1219           </m:mtd>
1220          </m:mtr>
1221          </xsl:for-each>
1222          <m:mtr>
1223           <m:mtd>
1224            <m:mrow>
1225             <xsl:apply-templates select="*[position()=last()]"/>
1226            </m:mrow>
1227           </m:mtd>
1228          </m:mtr>
1229         </m:mtable>
1230       </xsl:when>
1231       <!-- LET -->
1232       <xsl:when test="$name='let'">
1233        <m:mtext>(</m:mtext>
1234        <xsl:apply-templates select="m:ci"/>
1235        <m:mtext>) </m:mtext>
1236        <xsl:apply-templates select="*[3]"/>
1237       </xsl:when>
1238       <!-- RW_STEP -->
1239       <xsl:when test="$name='rw_step'">
1240         <m:mtable align="baseline 1" equalrows="false" columnalign="left">
1241          <m:mtr>
1242           <m:mtd>
1243            <m:mrow>
1244             <xsl:choose>
1245              <xsl:when test="name(*[2])='m:apply'">
1246               <xsl:apply-templates select="*[2]"/>
1247              </xsl:when>
1248              <xsl:otherwise>
1249               <m:mtext>Consider</m:mtext>
1250               <m:mphantom><m:mtext>_</m:mtext></m:mphantom>
1251               <xsl:apply-templates select="*[2]"/>
1252              </xsl:otherwise>
1253             </xsl:choose>
1254            </m:mrow>
1255           </m:mtd>
1256          </m:mtr>
1257          <m:mtr>
1258           <m:mtd>
1259            <m:mrow>
1260             <m:mtext>Rewrite</m:mtext>
1261             <m:mphantom><m:mtext>_</m:mtext></m:mphantom>
1262             <xsl:apply-templates select="*[3]"/>
1263             <m:mphantom><m:mtext>_</m:mtext></m:mphantom>
1264             <m:mtext>with</m:mtext>
1265             <m:mphantom><m:mtext>_</m:mtext></m:mphantom>
1266             <xsl:apply-templates select="*[4]"/>
1267             <m:mphantom><m:mtext>_</m:mtext></m:mphantom>
1268             <m:mtext>by</m:mtext>
1269             <m:mphantom><m:mtext>_</m:mtext></m:mphantom>
1270             <xsl:apply-templates select="*[5]"/>
1271            </m:mrow>
1272           </m:mtd>
1273          </m:mtr>
1274         </m:mtable>
1275       </xsl:when>
1276       <!-- not existing any more
1277       <xsl:when test="$name='thread'">
1278         <m:mtable align="baseline 1" equalrows="false" columnalign="left">
1279          <m:mtr>
1280           <m:mtd>
1281            <m:mrow>
1282             <xsl:choose>
1283              <xsl:when test="name(*[last()])='m:apply'">
1284               <xsl:apply-templates select="*[last()]"/>
1285              </xsl:when>
1286              <xsl:otherwise>
1287               <m:mtext>Consider</m:mtext>
1288               <m:mphantom><m:mtext>_</m:mtext></m:mphantom>
1289               <xsl:apply-templates select="*[last()]"/>
1290              </xsl:otherwise>
1291             </xsl:choose>
1292            </m:mrow>
1293           </m:mtd>
1294          </m:mtr>
1295          <xsl:apply-templates mode="thread" select="*[(last()-2)]"/>
1296         </m:mtable>
1297       </xsl:when>
1298       -->
1299       <!-- REWRITE_AND_APPLY -->
1300       <xsl:when test="$name='rewrite_and_apply'">
1301         <m:mtable align="baseline 1" equalrows="false" columnalign="left">
1302          <m:mtr>
1303           <m:mtd>
1304            <m:mrow>
1305             <xsl:apply-templates select="*[2]"/>
1306            </m:mrow>
1307           </m:mtd>
1308          </m:mtr>
1309          <m:mtr>
1310           <m:mtd>
1311            <m:mrow>
1312             <m:mtext>Then&#x00a0;apply&#x00a0;it&#x00a0;to</m:mtext>
1313             <m:mphantom><m:mtext>_</m:mtext></m:mphantom>
1314             <xsl:apply-templates select="*[position()>2]"/>
1315            </m:mrow>
1316           </m:mtd>
1317          </m:mtr>
1318        </m:mtable>
1319       </xsl:when>
1320       <!-- AND_IND -->
1321       <xsl:when test="$name='and_ind'">
1322         <m:mtable align="baseline 1" equalrows="false" columnalign="left">
1323          <m:mtr>
1324           <m:mtd>
1325            <m:mrow>
1326             <xsl:choose>
1327              <xsl:when test="name(*[2])='m:apply'">
1328               <xsl:apply-templates select="*[2]"/>
1329              </xsl:when>
1330              <xsl:otherwise>
1331               <m:mtext>Consider</m:mtext>
1332               <m:mphantom><m:mtext>_</m:mtext></m:mphantom>
1333               <xsl:apply-templates select="*[2]"/>
1334              </xsl:otherwise>
1335             </xsl:choose>
1336            </m:mrow>
1337           </m:mtd>
1338          </m:mtr>
1339          <m:mtr>
1340           <m:mtd>
1341            <m:mrow>
1342             <m:mtext>In&#x00a0;particular,&#x00a0;we&#x00a0;have</m:mtext>
1343            </m:mrow>
1344           </m:mtd>
1345          </m:mtr>
1346          <m:mtr>
1347           <m:mtd>
1348            <m:mrow>
1349             <m:mtext>(</m:mtext>
1350             <xsl:apply-templates select="*[3]"/>
1351             <m:mtext>)</m:mtext>
1352             <m:mphantom><m:mtext>_</m:mtext></m:mphantom>
1353             <xsl:apply-templates select="*[4]"/>
1354             </m:mrow>
1355           </m:mtd>
1356          </m:mtr>
1357          <m:mtr>
1358           <m:mtd>
1359            <m:mrow>
1360             <m:mtext>(</m:mtext>
1361             <xsl:apply-templates select="*[5]"/>
1362             <m:mtext>)</m:mtext>
1363             <m:mphantom><m:mtext>_</m:mtext></m:mphantom>
1364             <xsl:apply-templates select="*[6]"/>
1365             </m:mrow>
1366           </m:mtd>
1367          </m:mtr>
1368          <m:mtr>
1369           <m:mtd>
1370            <m:mrow>
1371             <xsl:apply-templates select="*[7]"/>
1372            </m:mrow>
1373           </m:mtd>
1374          </m:mtr>
1375         </m:mtable>
1376       </xsl:when>
1377       <!-- full_or_ind -->
1378       <xsl:when test="$name='full_or_ind'">
1379         <m:mtable align="baseline 1" equalrows="false" columnalign="left">
1380          <m:mtr>
1381           <m:mtd>
1382            <m:mrow>
1383             <xsl:choose>
1384              <xsl:when test="name(*[2])='m:apply'">
1385               <xsl:apply-templates select="*[2]"/>
1386              </xsl:when>
1387              <xsl:otherwise>
1388               <m:mtext>Consider</m:mtext>
1389               <m:mphantom><m:mtext>_</m:mtext></m:mphantom>
1390               <xsl:apply-templates select="*[2]"/>
1391              </xsl:otherwise>
1392             </xsl:choose>
1393            </m:mrow>
1394           </m:mtd>
1395          </m:mtr>
1396          <m:mtr>
1397           <m:mtd>
1398            <m:mrow>
1399             <m:mtext>We&#x00a0;proceed&#x00a0;by&#x00a0;cases&#x00a0;to&#x00a0;prove</m:mtext>
1400             <m:mphantom><m:mtext>_</m:mtext></m:mphantom>
1401             <xsl:apply-templates select="*[3]"/>
1402            </m:mrow>
1403           </m:mtd>
1404          </m:mtr>
1405          <m:mtr>
1406           <m:mtd>
1407            <m:mrow>
1408             <m:mtext>Left:&#x00a0;suppose</m:mtext>
1409             <m:mphantom><m:mtext>_</m:mtext></m:mphantom>
1410             <m:mo stretchy="false">(</m:mo>
1411             <xsl:apply-templates select="*[4]/m:bvar/m:ci"/>
1412             <m:mo stretchy="false">)</m:mo>
1413             <m:mphantom><m:mtext>_</m:mtext></m:mphantom>
1414             <xsl:apply-templates select="*[4]/m:bvar/m:type/*[1]"/>
1415            </m:mrow>
1416           </m:mtd>
1417          </m:mtr>
1418          <m:mtr>
1419           <m:mtd>
1420            <m:mrow>
1421             <m:mphantom><m:mtext>_</m:mtext></m:mphantom>
1422             <xsl:apply-templates select="*[4]/*[3]"/>
1423            </m:mrow>
1424           </m:mtd>
1425          </m:mtr>
1426          <m:mtr>
1427           <m:mtd>
1428            <m:mrow>
1429             <m:mtext>Right:&#x00a0;suppose</m:mtext>
1430             <m:mphantom><m:mtext>_</m:mtext></m:mphantom>
1431             <m:mo stretchy="false">(</m:mo>
1432             <xsl:apply-templates select="*[5]/m:bvar/m:ci"/>
1433             <m:mo stretchy="false">)</m:mo>
1434             <m:mphantom><m:mtext>_</m:mtext></m:mphantom>
1435             <xsl:apply-templates select="*[5]/m:bvar/m:type/*[1]"/>
1436            </m:mrow>
1437           </m:mtd>
1438          </m:mtr>
1439          <m:mtr>
1440           <m:mtd>
1441            <m:mrow>
1442             <xsl:apply-templates select="*[5]/*[3]"/>
1443            </m:mrow>
1444           </m:mtd>
1445          </m:mtr>
1446         </m:mtable>
1447       </xsl:when>
1448       <!-- OR_IND -->
1449       <xsl:when test="$name='or_ind'">
1450         <m:mtable align="baseline 1" equalrows="false" columnalign="left">
1451          <m:mtr>
1452           <m:mtd>
1453            <m:mrow>
1454             <xsl:choose>
1455              <xsl:when test="name(*[2])='m:apply'">
1456               <xsl:apply-templates select="*[2]"/>
1457              </xsl:when>
1458              <xsl:otherwise>
1459               <m:mtext>Consider</m:mtext>
1460               <m:mphantom><m:mtext>_</m:mtext></m:mphantom>
1461               <xsl:apply-templates select="*[2]"/>
1462              </xsl:otherwise>
1463             </xsl:choose>
1464            </m:mrow>
1465           </m:mtd>
1466          </m:mtr>
1467          <m:mtr>
1468           <m:mtd>
1469            <m:mrow>
1470             <m:mtext>We&#x00a0;prove</m:mtext>
1471             <m:mphantom><m:mtext>_</m:mtext></m:mphantom>
1472             <xsl:apply-templates select="*[3]"/>
1473             <m:mphantom><m:mtext>_</m:mtext></m:mphantom>
1474             <m:mtext>by&#x00a0;cases:</m:mtext>
1475            </m:mrow>
1476           </m:mtd>
1477          </m:mtr>
1478          <m:mtr>
1479           <m:mtd>
1480            <m:mrow>
1481             <m:mtext>Left</m:mtext>
1482             <xsl:apply-templates select="*[4]"/>
1483            </m:mrow>
1484           </m:mtd>
1485          </m:mtr>
1486          <m:mtr>
1487           <m:mtd>
1488            <m:mrow>
1489             <m:mtext>Right</m:mtext>
1490             <xsl:apply-templates select="*[5]"/>
1491            </m:mrow>
1492           </m:mtd>
1493          </m:mtr>
1494         </m:mtable>
1495       </xsl:when>
1496       <!-- EX_IND -->
1497       <xsl:when test="$name='ex_ind'">
1498         <m:mtable align="baseline 1" equalrows="false" columnalign="left">
1499          <m:mtr>
1500           <m:mtd>
1501            <m:mrow>
1502             <xsl:choose>
1503              <xsl:when test="name(*[2])='m:apply'">
1504               <xsl:apply-templates select="*[2]"/>
1505              </xsl:when>
1506              <xsl:otherwise>
1507               <m:mtext>Consider</m:mtext>
1508               <m:mphantom><m:mtext>_</m:mtext></m:mphantom>
1509               <xsl:apply-templates select="*[2]"/>
1510              </xsl:otherwise>
1511             </xsl:choose>
1512            </m:mrow>
1513           </m:mtd>
1514          </m:mtr>
1515          <m:mtr>
1516           <m:mtd>
1517            <m:mrow>
1518             <m:mtext>Let</m:mtext>
1519             <m:mphantom><m:mtext>_</m:mtext></m:mphantom>
1520             <xsl:apply-templates select="*[3]"/>
1521             <m:mtext>:</m:mtext>
1522             <xsl:apply-templates select="*[4]"/>
1523             <m:mphantom><m:mtext>_</m:mtext></m:mphantom>
1524             <m:mtext>such&#x00a0;that</m:mtext>
1525             <m:mphantom><m:mtext>_</m:mtext></m:mphantom>
1526             <m:mtext>(</m:mtext>
1527              <xsl:apply-templates select="*[5]"/>
1528             <m:mtext>)</m:mtext>
1529             <m:mphantom><m:mtext>_</m:mtext></m:mphantom>
1530             <xsl:apply-templates select="*[6]"/>
1531            </m:mrow>
1532           </m:mtd>
1533          </m:mtr>
1534          <m:mtr>
1535           <m:mtd>
1536            <m:mrow>
1537             <xsl:apply-templates select="*[7]"/>
1538            </m:mrow>
1539           </m:mtd>
1540          </m:mtr>
1541         </m:mtable>
1542       </xsl:when>
1543       <!-- ***************************************** -->
1544       <!-- *********** NOTATIONS ******************* -->
1545       <!-- ***************************************** -->
1546       <!-- subst -->
1547       <xsl:when test="$name='subst'">
1548         <xsl:apply-templates select="*[3]"/>
1549 <!-- no font for ApplyFunction: <m:mo>&#xe8a0;</m:mo> -->
1550         <m:mo stretchy="false">[</m:mo>
1551         <xsl:apply-templates select="*[4]"/>
1552         <m:mo mathcolor="green">
1553          <xsl:if test="$id != ''">
1554           <xsl:attribute name="m:xref"><xsl:value-of select="$id"/></xsl:attribute>
1555          </xsl:if>&#8592;</m:mo>
1556         <xsl:apply-templates select="*[2]"/>
1557         <m:mo stretchy="false">]</m:mo>
1558       </xsl:when>
1559       <!-- lift -->
1560       <xsl:when test="$name='lift'">
1561         <m:msup>
1562          <m:mo mathcolor="green">
1563           <xsl:if test="$id != ''">
1564            <xsl:attribute name="m:xref"><xsl:value-of select="$id"/></xsl:attribute>
1565           </xsl:if>&#8593;</m:mo>
1566          <xsl:apply-templates select="*[2]"/>
1567         </m:msup>
1568         <m:mrow>
1569          <m:mo stretchy="false">(</m:mo>
1570          <xsl:apply-templates select="*[3]"/>
1571          <m:mo stretchy="false">)</m:mo>
1572         </m:mrow>
1573       </xsl:when>
1574       <!-- lift_with_base -->
1575       <xsl:when test="$name='lift_with_base'">
1576         <m:msubsup>
1577          <m:mo mathcolor="green">
1578           <xsl:if test="$id != ''">
1579            <xsl:attribute name="m:xref"><xsl:value-of select="$id"/></xsl:attribute>
1580           </xsl:if>&#8593;</m:mo>
1581          <xsl:apply-templates select="*[3]"/>
1582          <xsl:apply-templates select="*[4]"/>
1583         </m:msubsup>
1584         <m:mrow>
1585          <m:mo stretchy="false">(</m:mo>
1586          <xsl:apply-templates select="*[2]"/>
1587          <m:mo stretchy="false">)</m:mo>
1588         </m:mrow>
1589       </xsl:when>
1590       <!-- beta_red1 -->
1591       <xsl:when test="$name='beta_red1'">
1592         <xsl:apply-templates select="*[2]"/>
1593         <m:munder>
1594          <m:mo mathcolor="green">
1595           <xsl:if test="$id != ''">
1596            <xsl:attribute name="m:xref"><xsl:value-of select="$id"/></xsl:attribute>
1597           </xsl:if>&#8594;</m:mo>
1598           <m:mi mathcolor="green">&#946;</m:mi>
1599         </m:munder>
1600         <xsl:apply-templates select="*[3]"/>
1601       </xsl:when>
1602       <!-- beta_red -->
1603       <xsl:when test="$name='beta_red'">
1604         <xsl:apply-templates select="*[2]"/>
1605         <m:munderover>
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>&#8594;</m:mo>
1610           <m:mi mathcolor="green">&#946;</m:mi>
1611           <m:mi mathcolor="green">*</m:mi>
1612         </m:munderover>
1613         <xsl:apply-templates select="*[3]"/>
1614       </xsl:when>
1615       <!-- par_beta_red1 -->
1616       <xsl:when test="$name='par_beta_red1'">
1617         <xsl:apply-templates select="*[2]"/>
1618         <m:munder>
1619          <m:mo mathcolor="green">
1620           <xsl:if test="$id != ''">
1621            <xsl:attribute name="m:xref"><xsl:value-of select="$id"/></xsl:attribute>
1622           </xsl:if>&#8658;</m:mo>
1623           <m:mi mathcolor="green">&#946;</m:mi>
1624         </m:munder>
1625         <xsl:apply-templates select="*[3]"/>
1626       </xsl:when>
1627       <!-- par_beta_red -->
1628       <xsl:when test="$name='par_beta_red'">
1629         <xsl:apply-templates select="*[2]"/>
1630         <m:munderover>
1631          <m:mo mathcolor="green">
1632           <xsl:if test="$id != ''">
1633            <xsl:attribute name="m:xref"><xsl:value-of select="$id"/></xsl:attribute>
1634           </xsl:if>&#8658;</m:mo>
1635           <m:mi mathcolor="green">&#946;</m:mi>
1636           <m:mi mathcolor="green">*</m:mi>
1637         </m:munderover>
1638         <xsl:apply-templates select="*[3]"/>
1639       </xsl:when>
1640       <!-- forgetful -->
1641       <xsl:when test="$name='forgetful'">
1642        <m:mfenced open="|" close="|">
1643         <xsl:if test="$id != ''">
1644          <xsl:attribute name="m:xref"><xsl:value-of select="$id"/></xsl:attribute>
1645         </xsl:if>
1646         <xsl:apply-templates select="*[2]"/>
1647        </m:mfenced>
1648       </xsl:when>
1649       <!-- isomorphic -->
1650       <xsl:when test="$name='isomorphic'">
1651         <xsl:apply-templates select="*[2]"/>
1652         <m:mo mathcolor="green">
1653          <xsl:if test="$id != ''">
1654           <xsl:attribute name="m:xref"><xsl:value-of select="$id"/></xsl:attribute>
1655          </xsl:if>&#8773;</m:mo>
1656         <xsl:apply-templates select="*[3]"/>
1657       </xsl:when>
1658       <!-- interp -->
1659       <xsl:when test="$name='forgetful'">
1660        <m:mfenced open="[" close="]">
1661         <xsl:if test="$id != ''">
1662          <xsl:attribute name="m:xref"><xsl:value-of select="$id"/></xsl:attribute>
1663         </xsl:if>
1664         <xsl:apply-templates select="*[2]"/>
1665        </m:mfenced>
1666       </xsl:when>
1667
1668       <!-- ERROR -->
1669       <xsl:otherwise>
1670        <m:mi>ERROR</m:mi>
1671       </xsl:otherwise>
1672      </xsl:choose>
1673     </m:mrow>
1674 </xsl:template>
1675
1676 <!-- Il modo Thread non esiste piu'
1677 <xsl:template match="*" mode="thread">
1678  <xsl:variable name="name"><xsl:value-of select="following-sibling::*[position()=1]/m:csymbol"/></xsl:variable>
1679  <xsl:choose>
1680   <xsl:when test="$name='rw_step'">
1681          <m:mtr>
1682           <m:mtd>
1683            <m:mrow>
1684             <m:mtext>Rewrite</m:mtext>
1685             <m:mphantom><m:mtext>_</m:mtext></m:mphantom>
1686             <xsl:apply-templates select="following-sibling::*[position()=1]/*[2]"/>
1687             <m:mphantom><m:mtext>_</m:mtext></m:mphantom>
1688             <m:mtext>with</m:mtext>
1689             <m:mphantom><m:mtext>_</m:mtext></m:mphantom>
1690             <xsl:apply-templates select="following-sibling::*[position()=1]/*[3]"/>
1691             <m:mphantom><m:mtext>_</m:mtext></m:mphantom>
1692             <m:mtext>by</m:mtext>
1693             <m:mphantom><m:mtext>_</m:mtext></m:mphantom>
1694             <xsl:apply-templates select="following-sibling::*[position()=1]/*[4]"/>
1695            </m:mrow>
1696           </m:mtd>
1697          </m:mtr>
1698          <m:mtr>
1699           <m:mtd>
1700            <m:mrow>
1701             <m:mtext mathcolor="Maroon">we&#x00a0;get</m:mtext>
1702             <m:mphantom><m:mtext>_</m:mtext></m:mphantom>
1703             <xsl:apply-templates select="."/>
1704            </m:mrow>
1705           </m:mtd>
1706          </m:mtr>
1707    </xsl:when>
1708    <xsl:otherwise>
1709          <m:mtr>
1710           <m:mtd>
1711            <m:mrow>
1712             <xsl:apply-templates select="following-sibling::*[position()=1]"/>
1713            </m:mrow>
1714           </m:mtd>
1715          </m:mtr>
1716          <m:mtr>
1717           <m:mtd>
1718            <m:mrow>
1719             <m:mtext mathcolor="Maroon">we&#x00a0;get</m:mtext>
1720             <m:mphantom><m:mtext>_</m:mtext></m:mphantom>
1721             <xsl:apply-templates select="."/>
1722            </m:mrow>
1723           </m:mtd>
1724          </m:mtr>
1725     </xsl:otherwise>
1726    </xsl:choose>
1727          <xsl:apply-templates mode="thread" select="preceding-sibling::*[position()=2]"/>
1728 </xsl:template>
1729 -->
1730
1731 <!-- LAMBDA -->
1732
1733 <xsl:template match="m:lambda">
1734     <xsl:variable name="charlength"><xsl:apply-templates select="*[position()=1]" mode="charcount"/></xsl:variable>
1735     <m:mrow>
1736      <xsl:if test="@id">
1737       <xsl:attribute name="m:xref">
1738        <xsl:value-of select="@id"/>
1739       </xsl:attribute>
1740      </xsl:if>
1741      <xsl:choose>
1742      <xsl:when test="$charlength >= $framewidth">
1743       <m:mtable align="baseline 1" equalrows="false" columnalign="left">
1744         <m:mtr>
1745           <m:mtd>
1746            <m:mrow>
1747             <m:mo mathcolor="Red">&#x03bb;</m:mo>
1748             <xsl:apply-templates select="m:bvar"/>
1749            </m:mrow>
1750           </m:mtd>
1751          </m:mtr>
1752        <m:mtr>
1753         <m:mtd>
1754          <m:mrow>
1755           <m:mo>.</m:mo>
1756           <xsl:apply-templates select="*[position()=2]"/>
1757          </m:mrow>
1758         </m:mtd>
1759        </m:mtr>
1760       </m:mtable>
1761      </xsl:when>
1762      <xsl:otherwise>
1763       <m:mo mathcolor="Red">&#x03bb;</m:mo>
1764       <xsl:apply-templates select="m:bvar/m:ci"/>
1765       <m:mo>:</m:mo>
1766       <xsl:apply-templates select="m:bvar/m:type"/>
1767       <m:mo>.</m:mo>
1768       <xsl:apply-templates select="*[position()=2]"/>
1769      </xsl:otherwise>
1770      </xsl:choose>
1771     </m:mrow>
1772 </xsl:template>
1773
1774 <!-- *********************************** -->
1775 <!-- BASE SET OF MATHML CONTENT ELEMENTS -->
1776 <!-- *********************************** -->
1777
1778 <!-- Logic -->
1779
1780 <xsl:template match = "m:apply[m:eq[1]]">
1781  <xsl:variable name="charlength">
1782   <xsl:apply-templates select="*[1]" mode="charcount"/>
1783  </xsl:variable>
1784  <xsl:choose>
1785   <xsl:when test="$charlength >= $framewidth">
1786    <m:mtable align="baseline 1" equalrows="false" columnalign="left">
1787     <xsl:if test="@id">
1788      <xsl:attribute name="m:xref">
1789       <xsl:value-of select="@id"/>
1790      </xsl:attribute>
1791     </xsl:if>
1792     <m:mtr>
1793      <m:mtd>
1794       <m:mrow>
1795        <m:mo stretchy="false">(</m:mo>
1796        <xsl:apply-templates select="*[position()=2]"/>
1797       </m:mrow>
1798      </m:mtd>
1799     </m:mtr>
1800     <xsl:for-each select = "*[position()>2]">
1801      <m:mtr>
1802       <m:mtd>
1803        <m:mrow>
1804         <m:mphantom><m:mtext>__</m:mtext></m:mphantom>
1805         <m:mo>
1806          <xsl:if test="m:in/@id">
1807           <xsl:attribute name="m:xref">
1808            <xsl:value-of select="m:in/@id"/>
1809           </xsl:attribute>
1810          </xsl:if>=</m:mo>
1811         <xsl:apply-templates select="."/>
1812        </m:mrow>
1813       </m:mtd>
1814      </m:mtr>
1815     </xsl:for-each>
1816     <m:mtr>
1817      <m:mtd>
1818       <m:mrow>
1819        <m:mo stretchy="false">)</m:mo>
1820       </m:mrow>
1821      </m:mtd>
1822     </m:mtr>
1823    </m:mtable>
1824   </xsl:when>
1825   <xsl:otherwise>
1826    <xsl:apply-imports/>
1827   </xsl:otherwise>
1828  </xsl:choose>
1829 </xsl:template>
1830
1831
1832 <xsl:template match = "m:apply[m:and[1]|m:or[1]
1833           |m:geq[1]|m:leq[1]|m:gt[1]|m:lt[1]
1834           |m:in[1]|m:intesect[1]|m:union[1]|m:subset[1]
1835           |m:prsubset|m:setdiff[1]]">
1836  <xsl:variable name="symbol">
1837   <xsl:choose>
1838    <xsl:when test="m:and[1]">
1839     <xsl:value-of select="'&#8743;'"/>
1840    </xsl:when>
1841    <xsl:when test="m:or[1]">
1842     <xsl:value-of select="'&#8744;'"/>
1843    </xsl:when>
1844    <xsl:when test="m:geq[1]">
1845     <xsl:value-of select="'&#8805;'"/>
1846    </xsl:when>
1847    <xsl:when test="m:leq[1]">
1848     <xsl:value-of select="'&#8804;'"/>
1849    </xsl:when>
1850    <xsl:when test="m:gt[1]">
1851     <xsl:value-of select="'&#62;'"/>
1852    </xsl:when>
1853    <xsl:when test="m:lt[1]">
1854     <xsl:value-of select="'&#60;&#32;'"/>
1855    </xsl:when>
1856    <xsl:when test="m:eq[1]">
1857     <xsl:value-of select="'&#61;'"/>
1858    </xsl:when>
1859    <xsl:when test="m:in[1]">
1860     <xsl:value-of select="'&#x02208;'"/>
1861    </xsl:when>
1862    <xsl:when test="m:subset[1]">
1863     <xsl:value-of select="'&#x02286;'"/>
1864    </xsl:when>
1865    <xsl:when test="m:prsubset[1]">
1866     <xsl:value-of select="'&#x02282;'"/>
1867    </xsl:when>
1868    <xsl:when test="m:intersect[1]">
1869     <xsl:value-of select="'&#x022C2;'"/>
1870    </xsl:when>
1871    <xsl:when test="m:union[1]">
1872     <xsl:value-of select="'&#x022C3;'"/>
1873    </xsl:when>
1874    <xsl:when test="m:setdiff[1]">
1875     <xsl:value-of select="'&#x02216;'"/>
1876    </xsl:when>
1877   </xsl:choose>
1878  </xsl:variable>
1879  <xsl:variable name="charlength">
1880   <xsl:apply-templates select="*[1]" mode="charcount"/>
1881  </xsl:variable>
1882  <xsl:choose>
1883   <xsl:when test="$charlength >= $framewidth">
1884    <m:mtable align="baseline 1" equalrows="false" columnalign="left">
1885     <xsl:if test="@id">
1886      <xsl:attribute name="m:xref">
1887       <xsl:value-of select="@id"/>
1888      </xsl:attribute>
1889     </xsl:if>
1890     <m:mtr>
1891      <m:mtd>
1892       <m:mrow>
1893        <m:mo stretchy="false">(</m:mo>
1894        <xsl:apply-templates select="*[position()=2]"/>
1895       </m:mrow>
1896      </m:mtd>
1897     </m:mtr>
1898     <xsl:for-each select = "*[position()>2]">
1899      <m:mtr>
1900       <m:mtd>
1901        <m:mrow>
1902         <m:mphantom><m:mtext>__</m:mtext></m:mphantom>
1903         <m:mo>
1904          <xsl:if test="*[1]/@id">
1905           <xsl:attribute name="m:xref">
1906            <xsl:value-of select="*[1]/@id"/>
1907           </xsl:attribute>
1908          </xsl:if><xsl:value-of select="$symbol"/></m:mo>
1909         <xsl:apply-templates select="."/>
1910        </m:mrow>
1911       </m:mtd>
1912      </m:mtr>
1913     </xsl:for-each>
1914     <m:mtr>
1915      <m:mtd>
1916       <m:mrow>
1917        <m:mo stretchy="false">)</m:mo>
1918       </m:mrow>
1919      </m:mtd>
1920     </m:mtr>
1921    </m:mtable>
1922   </xsl:when>
1923   <xsl:otherwise>
1924    <xsl:apply-imports/>
1925   </xsl:otherwise>
1926  </xsl:choose>
1927 </xsl:template>
1928
1929 <xsl:template match = "m:set">
1930  <xsl:choose>
1931   <xsl:when test="count(child::*) = 0">
1932    <m:mi>
1933     <xsl:if test="@id">
1934      <xsl:attribute name="m:xref">
1935       <xsl:value-of select="@id"/>
1936      </xsl:attribute>
1937     </xsl:if>&#x02205;</m:mi>
1938   </xsl:when>
1939   <xsl:otherwise>
1940    <xsl:variable name="charlength">
1941     <xsl:apply-templates select="*[1]" mode="charcount"/>
1942    </xsl:variable>
1943    <xsl:choose>
1944     <xsl:when test="$charlength >= $framewidth">
1945      <xsl:choose>
1946       <xsl:when test="name(*[1]) = 'm:bvar'">
1947        <m:mtable align="baseline 1" equalrows="false" columnalign="left">
1948         <m:mtr>
1949          <m:mtd>
1950           <m:mrow>
1951            <m:mo stretchy="false">
1952             <xsl:if test="@id">
1953              <xsl:attribute name="m:xref">
1954               <xsl:value-of select="@id"/>
1955              </xsl:attribute>
1956             </xsl:if>{</m:mo>
1957            <xsl:apply-templates select="*[position()=1]"/>
1958           </m:mrow>
1959          </m:mtd>
1960         </m:mtr>
1961         <m:mtr>
1962          <m:mtd>
1963           <m:mrow>
1964            <m:mphantom><m:mtext>{</m:mtext></m:mphantom>
1965            <m:mo stretchy="false">|</m:mo>
1966            <xsl:apply-templates select="m:condition/*[1]"/>
1967           </m:mrow>
1968          </m:mtd>
1969         </m:mtr>
1970         <m:mtr>
1971          <m:mtd>
1972           <m:mrow>
1973            <m:mo stretchy="false">
1974             <xsl:if test="@id">
1975              <xsl:attribute name="m:xref">
1976               <xsl:value-of select="@id"/>
1977              </xsl:attribute>
1978             </xsl:if>}</m:mo>
1979           </m:mrow>
1980          </m:mtd>
1981         </m:mtr>
1982        </m:mtable>
1983       </xsl:when>
1984       <xsl:otherwise>
1985        <m:mtable align="baseline 1" equalrows="false" columnalign="left">
1986         <m:mtr>
1987          <m:mtd>
1988           <m:mrow>
1989            <m:mo stretchy="false">
1990             <xsl:if test="@id">
1991              <xsl:attribute name="m:xref">
1992               <xsl:value-of select="@id"/>
1993              </xsl:attribute>
1994             </xsl:if>{</m:mo>
1995            <xsl:apply-templates select="*[position()=1]"/>
1996            <xsl:if test="position() != last()">
1997             <mo>,</mo>
1998            </xsl:if>
1999           </m:mrow>
2000          </m:mtd>
2001         </m:mtr>
2002         <xsl:for-each select = "*[position()>2]">
2003          <m:mtr>
2004           <m:mtd>
2005            <m:mrow>
2006             <m:mphantom><m:mtext>{</m:mtext></m:mphantom>
2007             <xsl:apply-templates select="."/>
2008             <xsl:if test="position() != last()">
2009              <mo>,</mo>
2010             </xsl:if>
2011            </m:mrow>
2012           </m:mtd>
2013          </m:mtr>
2014         </xsl:for-each>
2015         <m:mtr>
2016          <m:mtd>
2017           <m:mrow>
2018            <m:mo stretchy="false">
2019             <xsl:if test="@id">
2020              <xsl:attribute name="m:xref">
2021               <xsl:value-of select="@id"/>
2022              </xsl:attribute>
2023             </xsl:if>}</m:mo>
2024           </m:mrow>
2025          </m:mtd>
2026         </m:mtr>
2027        </m:mtable>
2028       </xsl:otherwise>
2029      </xsl:choose>
2030     </xsl:when>
2031     <xsl:otherwise>
2032      <xsl:apply-imports/>
2033     </xsl:otherwise>
2034    </xsl:choose>
2035   </xsl:otherwise>
2036  </xsl:choose>
2037 </xsl:template>
2038
2039 <xsl:template match = "m:apply[m:card[1]]">
2040   <m:mfenced open="|" close="|" stretchy="false">
2041     <xsl:if test="($SEM_SW=$SEM_XREF or $SEM_SW=$SEM_XREF_EXT) and @id">
2042       <xsl:attribute name="m:xref">
2043         <xsl:value-of select="@id"/>
2044       </xsl:attribute>
2045     </xsl:if>
2046   <xsl:apply-templates select="*[2]"/>
2047   </m:mfenced>
2048 </xsl:template>
2049
2050
2051 <!--**********************-->
2052 <!--       COUNTING       -->
2053 <!--**********************-->
2054
2055 <xsl:template match="m:cn|m:and|m:or|m:not|m:exists|m:eq|m:lt|m:leq|m:gt|m:geq
2056  |m:in|m:notin|m:intersect|m:union|m:subset|m:prsubset|m:card|m:setdiff
2057  |m:plus|m:minus|m:times" mode="charcount">
2058 <xsl:param name="incurrent_length" select="0"/>
2059     <xsl:choose>
2060     <xsl:when test="$framewidth > ($incurrent_length + 3 + string-length())">
2061      <xsl:variable name="siblength">
2062       <xsl:apply-templates select="following-sibling::*[position()=1]" mode="charcount">
2063        <xsl:with-param name="incurrent_length" select="$incurrent_length + string-length()"/>
2064       </xsl:apply-templates>
2065      </xsl:variable>
2066      <xsl:choose>
2067      <xsl:when test="string($siblength) = &quot;&quot;">
2068       <xsl:value-of select="$incurrent_length + 3 + string-length()"/>
2069      </xsl:when>
2070      <xsl:otherwise>
2071       <xsl:value-of select="number($siblength)"/>
2072      </xsl:otherwise>
2073      </xsl:choose>
2074     </xsl:when>
2075     <xsl:otherwise>
2076      <xsl:value-of select="$incurrent_length + 3 + string-length()"/>
2077     </xsl:otherwise>
2078     </xsl:choose>
2079 </xsl:template>
2080
2081 <xsl:template match="m:ci|m:csymbol" mode="charcount">
2082 <xsl:param name="incurrent_length" select="0"/>
2083 <xsl:param name="nosibling" select="0"/>
2084     <xsl:choose>
2085     <xsl:when test="$framewidth > ($incurrent_length + string-length()) and ($nosibling = 0)">
2086      <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>
2087      <xsl:choose>
2088      <xsl:when test="string($siblength) = &quot;&quot;">
2089       <xsl:value-of select="$incurrent_length + string-length()"/>
2090      </xsl:when>
2091      <xsl:otherwise>
2092       <xsl:value-of select="number($siblength)"/>
2093      </xsl:otherwise>
2094      </xsl:choose>
2095     </xsl:when>
2096     <xsl:otherwise>
2097      <xsl:value-of select="$incurrent_length + string-length()"/>
2098     </xsl:otherwise>
2099     </xsl:choose>
2100 </xsl:template>
2101
2102 <xsl:template match="*" mode="charcount">
2103 <xsl:param name="incurrent_length" select="0"/>
2104 <xsl:param name="nosibling" select="0"/>
2105  <xsl:choose>
2106   <xsl:when test="count(child::*) = 0">
2107    <xsl:value-of select="$incurrent_length"/>
2108   </xsl:when>
2109   <xsl:otherwise>
2110     <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>
2111     <xsl:choose>
2112     <xsl:when test="$framewidth > number($childlength) and ($nosibling = 0)">
2113      <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>
2114      <xsl:choose>
2115      <xsl:when test="string($siblength) = &quot;&quot;">
2116       <xsl:value-of select="number($childlength)"/>
2117      </xsl:when>
2118      <xsl:otherwise>
2119       <xsl:value-of select="number($siblength)"/>
2120      </xsl:otherwise>
2121      </xsl:choose>
2122     </xsl:when>
2123     <xsl:otherwise>
2124      <xsl:value-of select="number($childlength)"/>
2125     </xsl:otherwise>
2126     </xsl:choose>
2127   </xsl:otherwise>
2128  </xsl:choose>
2129 </xsl:template>
2130
2131 </xsl:stylesheet>