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