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 <!--***********************************************************************-->
  48 <!-- Parameter affecting line-breaking                                     -->
  49 <!--***********************************************************************-->
  50
  51 <xsl:variable name="framewidth" select="35"/>
  52
  53 <!--***********************************************************************-->
  54 <!-- Gli oggetti sono stampati come mtext all'interno di una marca toplevel-->
  55 <!-- math ma al di fuori di semantics. Ora vi sono tanti semantics quanti  -->
  56 <!-- sono i termini: la presentation per un termine e' generata come primo -->
  57 <!-- figlio di un semantics e l'originario content viene inserito nel      -->
  58 <!-- nel secondo figlio di semantics, annotation-xml                       -->
  59 <!--***********************************************************************-->
  60
  61 <!--**********************-->
  62 <!--        OBJECTS       -->
  63 <!--**********************-->
  64
  65 <xsl:param name="type" select="'standalone'"/>
  66
  67 <xsl:template match="/">
  68  <xsl:choose>
  69   <xsl:when test="$type = 'standalone'">
  70    <xsl:apply-templates select="*"/>
  71   </xsl:when>
  72   <xsl:otherwise>
  73    <to_be_embedded>
  74     <xsl:apply-templates select="*"/>
  75    </to_be_embedded>
  76   </xsl:otherwise>
  77  </xsl:choose>
  78 </xsl:template>
  79
  80 <!-- DEFINITION -->
  81
  82 <xsl:template match="Definition">
  83     <m:math>
  84      <m:mtable align="baseline 1" equalrows="false" columnalign="left" helm:xref="{@helm:xref}">
  85       <m:mtr>
  86        <m:mtd>
  87         <m:mrow>
  88          <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>
  89         </m:mrow>
  90        </m:mtd>
  91       </m:mtr>
  92       <m:mtr>
  93        <m:mtd>
  94         <m:mrow>
  95          <m:mphantom><m:mtext>__</m:mtext></m:mphantom>
  96          <xsl:apply-templates select="type/*[1]"/>
  97         </m:mrow>
  98        </m:mtd>
  99       </m:mtr>
 100       <m:mtr>
 101        <m:mtd>
 102         <m:mrow>
 103          <m:mtext>AS</m:mtext>
 104         </m:mrow>
 105        </m:mtd>
 106       </m:mtr>
 107       <m:mtr>
 108        <m:mtd>
 109         <m:mrow>
 110          <m:mphantom><m:mtext>__</m:mtext></m:mphantom>
 111          <xsl:apply-templates select="body/*[1]"/>
 112         </m:mrow>
 113        </m:mtd>
 114       </m:mtr>
 115      </m:mtable>
 116     </m:math>
 117 </xsl:template>
 118
 119 <!-- AXIOM -->
 120
 121 <xsl:template match="Axiom">
 122     <m:math>
 123      <m:mtable align="baseline 1" equalrows="false" columnalign="left" helm:xref="{@helm:xref}">
 124       <m:mtr>
 125        <m:mtd>
 126         <m:mrow>
 127          <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>
 128         </m:mrow>
 129        </m:mtd>
 130       </m:mtr>
 131       <m:mtr>
 132        <m:mtd>
 133         <m:mrow>
 134          <m:mphantom><m:mtext>__</m:mtext></m:mphantom>
 135          <xsl:apply-templates select="type/*[1]"/>
 136         </m:mrow>
 137        </m:mtd>
 138       </m:mtr>
 139      </m:mtable>
 140     </m:math>
 141 </xsl:template>
 142
 143 <!-- UNFINISHED PROOF -->
 144
 145 <xsl:template match="CurrentProof">
 146     <m:math>
 147      <m:mtable align="baseline 1" equalrows="false" columnalign="left" helm:xref="{@helm:xref}">
 148       <m:mtr>
 149        <m:mtd>
 150         <m:mrow>
 151          <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>
 152         </m:mrow>
 153        </m:mtd>
 154       </m:mtr>
 155       <m:mtr>
 156        <m:mtd>
 157         <m:mrow>
 158          <m:mtext>THESIS:</m:mtext>
 159         </m:mrow>
 160        </m:mtd>
 161       </m:mtr>
 162       <m:mtr>
 163        <m:mtd>
 164         <m:mrow>
 165          <m:mphantom><m:mtext>__</m:mtext></m:mphantom>
 166          <xsl:apply-templates select="type/*[1]"/>
 167         </m:mrow>
 168        </m:mtd>
 169       </m:mtr>
 170       <m:mtr>
 171        <m:mtd>
 172         <m:mrow>
 173          <m:mtext>CONJECTURES:</m:mtext>
 174         </m:mrow>
 175        </m:mtd>
 176       </m:mtr>
 177       <xsl:for-each select="Conjecture">
 178       <m:mtr>
 179        <m:mtd>
 180         <m:mrow>
 181          <m:mphantom><m:mtext>__</m:mtext></m:mphantom>
 182          <m:mtext><xsl:value-of select="./@no"/>:</m:mtext>
 183          <xsl:apply-templates select="./*[1]"/>
 184         </m:mrow>
 185        </m:mtd>
 186       </m:mtr>
 187       </xsl:for-each>
 188       <m:mtr>
 189        <m:mtd>
 190         <m:mrow>
 191          <m:mtext>CORRESPONDING PROOF:</m:mtext>
 192         </m:mrow>
 193        </m:mtd>
 194       </m:mtr>
 195       <m:mtr>
 196        <m:mtd>
 197         <m:mrow>
 198          <m:mphantom><m:mtext>__</m:mtext></m:mphantom>
 199          <xsl:apply-templates select="body/*[1]"/>
 200         </m:mrow>
 201        </m:mtd>
 202       </m:mtr>
 203      </m:mtable>
 204     </m:math>
 205 </xsl:template>
 206
 207 <!-- MUTUAL INDUCTIVE DEFINITION -->
 208
 209 <xsl:template match="InductiveDefinition">
 210     <m:math>
 211      <m:mtable align="baseline 1" equalrows="false" columnalign="left" helm:xref="{@helm:xref}">
 212      <xsl:for-each select="InductiveType">
 213       <m:mtr>
 214        <m:mtd>
 215         <m:mrow>
 216          <xsl:choose>
 217          <xsl:when test="position() = 1">
 218           <xsl:choose>
 219           <xsl:when test="string(./@inductive) = &quot;true&quot;">
 220            <m:mtext>INDUCTIVE DEFINITION</m:mtext>
 221           </xsl:when>
 222           <xsl:otherwise>
 223            <m:mtext>COINDUCTIVE DEFINITION</m:mtext>
 224           </xsl:otherwise>
 225           </xsl:choose>
 226          </xsl:when>
 227          <xsl:otherwise>
 228           <m:mtext>AND</m:mtext>
 229          </xsl:otherwise>
 230          </xsl:choose>
 231          <m:mphantom><m:mtext>_</m:mtext></m:mphantom>
 232          <m:mtext><xsl:value-of select="./@name"/>(<xsl:if test="string(../Params) != &quot;&quot;"><xsl:value-of select="../Params"/></xsl:if>)</m:mtext>
 233         </m:mrow>
 234        </m:mtd>
 235       </m:mtr>
 236       <m:mtr>
 237        <m:mtd>
 238         <m:mrow>
 239          <m:mphantom><m:mtext>__</m:mtext></m:mphantom>
 240          <m:mtext>[</m:mtext>
 241          <xsl:choose>
 242          <xsl:when test="string(../Param) != &quot;&quot;">
 243           <m:mtable align="baseline 1" equalrows="false" columnalign="left">
 244            <xsl:for-each select="../Param">
 245             <m:mtr>
 246              <m:mtd>
 247               <m:mrow>
 248                <m:mi><xsl:value-of select="./@name"/></m:mi>
 249                <m:mo>:</m:mo>
 250                <xsl:apply-templates select="*"/>
 251               </m:mrow>
 252              </m:mtd>
 253             </m:mtr>
 254            </xsl:for-each>
 255             <m:mtr>
 256              <m:mtd>
 257               <m:mrow>
 258                <m:mtext>]</m:mtext>
 259               </m:mrow>
 260              </m:mtd>
 261             </m:mtr>
 262           </m:mtable>
 263          </xsl:when>
 264          <xsl:otherwise>
 265           <m:mtext>]</m:mtext>
 266          </xsl:otherwise>
 267          </xsl:choose>
 268         </m:mrow>
 269        </m:mtd>
 270       </m:mtr>
 271       <m:mtr>
 272        <m:mtd>
 273         <m:mrow>
 274          <m:mtext>OF ARITY</m:mtext>
 275         </m:mrow>
 276        </m:mtd>
 277       </m:mtr>
 278       <m:mtr>
 279        <m:mtd>
 280         <m:mrow>
 281          <m:mphantom><m:mtext>__</m:mtext></m:mphantom>
 282          <xsl:apply-templates select="./arity/*[1]"/>
 283         </m:mrow>
 284        </m:mtd>
 285       </m:mtr>
 286       <m:mtr>
 287        <m:mtd>
 288         <m:mrow>
 289          <m:mtext>BUILT FROM</m:mtext>
 290         </m:mrow>
 291        </m:mtd>
 292       </m:mtr>
 293       <xsl:for-each select="./Constructor">
 294       <m:mtr>
 295        <m:mtd>
 296         <m:mrow>
 297          <xsl:choose>
 298          <xsl:when test="position() = 1">
 299           <m:mphantom><m:mtext>__</m:mtext></m:mphantom>
 300          </xsl:when>
 301          <xsl:otherwise>
 302           <m:mtext>|</m:mtext>
 303           <m:mphantom><m:mtext>_</m:mtext></m:mphantom>
 304          </xsl:otherwise>
 305          </xsl:choose>
 306          <m:mtext><xsl:value-of select="./@name"/> OF</m:mtext>
 307          <m:mphantom><m:mtext>_</m:mtext></m:mphantom>
 308          <xsl:apply-templates select="./*[1]"/>
 309         </m:mrow>
 310        </m:mtd>
 311       </m:mtr>
 312       </xsl:for-each>
 313      </xsl:for-each>
 314      </m:mtable>
 315     </m:math>
 316 </xsl:template>
 317
 318 <!-- VARIABLE -->
 319
 320 <xsl:template match="Variable">
 321     <m:math>
 322      <m:mtable align="baseline 1" equalrows="false" columnalign="left" helm:xref="{@helm:xref}">
 323       <m:mtr>
 324        <m:mtd>
 325         <m:mrow>
 326          <m:mtext>VARIABLE <xsl:value-of select="@name"/> OF TYPE</m:mtext>
 327         </m:mrow>
 328        </m:mtd>
 329       </m:mtr>
 330       <m:mtr>
 331        <m:mtd>
 332         <m:mrow>
 333          <m:mphantom><m:mtext>__</m:mtext></m:mphantom>
 334          <xsl:apply-templates select="type/*[1]"/>
 335         </m:mrow>
 336        </m:mtd>
 337       </m:mtr>
 338       <xsl:if test="name(*[1])='body'">
 339        <m:mtr>
 340         <m:mtd>
 341          <m:mrow>
 342           <m:mtext>AS</m:mtext>
 343          </m:mrow>
 344         </m:mtd>
 345        </m:mtr>
 346        <m:mtr>
 347         <m:mtd>
 348          <m:mrow>
 349           <m:mphantom><m:mtext>__</m:mtext></m:mphantom>
 350           <xsl:apply-templates select="body/*[1]"/>
 351          </m:mrow>
 352         </m:mtd>
 353        </m:mtr>
 354       </xsl:if>
 355      </m:mtable>
 356     </m:math>
 357 </xsl:template>
 358
 359 <!--**********************-->
 360 <!--        TERMS         -->
 361 <!--**********************-->
 362
 363 <xsl:template match="m:bvar">
 364  <xsl:choose>
 365   <xsl:when test="m:type">
 366    <xsl:variable name="charlength">
 367     <xsl:apply-templates select="m:ci" mode="charcount"/>
 368    </xsl:variable>
 369    <xsl:choose>
 370     <xsl:when test="$charlength >= $framewidth">
 371      <m:mtable align="baseline 1" equalrows="false" columnalign="left">
 372       <m:mtr>
 373        <m:mtd>
 374         <xsl:apply-templates select="m:ci"/>
 375         <m:mo>:</m:mo>
 376        </m:mtd>
 377       </m:mtr>
 378       <m:mtr>
 379        <m:mtd>
 380          <xsl:apply-templates select="m:type"/>
 381        </m:mtd>
 382       </m:mtr>
 383      </m:mtable>
 384     </xsl:when>
 385     <xsl:otherwise>
 386      <xsl:apply-templates select="m:ci"/>
 387      <m:mo>:</m:mo>
 388      <xsl:apply-templates select="m:type"/>
 389     </xsl:otherwise>
 390    </xsl:choose>
 391   </xsl:when>
 392   <xsl:otherwise>
 393    <xsl:apply-templates select="m:ci"/>
 394   </xsl:otherwise>
 395  </xsl:choose>
 396 </xsl:template>
 397
 398
 399 <!-- CSYMBOL -->
 400
 401 <xsl:template match="m:apply[m:csymbol]">
 402 <xsl:param name="nopar" select="0"/>
 403     <xsl:variable name="name"><xsl:value-of select="m:csymbol"/></xsl:variable>
 404     <xsl:variable name="charlength"><xsl:apply-templates select="m:csymbol" mode="charcount"/></xsl:variable>
 405     <m:mrow>
 406      <xsl:if test="@helm:xref">
 407       <xsl:attribute name="m:xref"><xsl:value-of select="@id"/></xsl:attribute>
 408      </xsl:if>
 409      <xsl:choose>
 410       <!-- FORALL -->
 411       <xsl:when test="$name='forall'">
 412        <xsl:choose>
 413        <xsl:when test="$charlength >= $framewidth">
 414         <m:mtable align="baseline 1" equalrows="false" columnalign="left">
 415          <m:mtr>
 416           <m:mtd>
 417            <m:mrow>
 418             <m:mo mathcolor="Blue"><m:mchar name="ForAll"/></m:mo>
 419             <xsl:apply-templates select="m:bvar"/>
 420            </m:mrow>
 421           </m:mtd>
 422          </m:mtr>
 423          <m:mtr>
 424           <m:mtd>
 425            <m:mrow>
 426             <m:mo>.</m:mo>
 427             <xsl:apply-templates select="*[position()=3]"/>
 428            </m:mrow>
 429           </m:mtd>
 430          </m:mtr>
 431         </m:mtable>
 432        </xsl:when>
 433        <xsl:otherwise>
 434         <m:mo mathcolor="Blue"><m:mchar name="ForAll"/></m:mo>
 435         <xsl:apply-templates select="m:bvar/m:ci"/>
 436         <m:mo>:</m:mo>
 437         <xsl:apply-templates select="m:bvar/m:type"/>
 438         <m:mo>.</m:mo>
 439         <xsl:apply-templates select="*[position()=3]"/>
 440        </xsl:otherwise>
 441        </xsl:choose>
 442       </xsl:when>
 443       <!-- LET-IN -->
 444       <xsl:when test="$name='let_in'">
 445        <xsl:choose>
 446        <xsl:when test="$charlength >= $framewidth">
 447         <m:mtable align="baseline 1" equalrows="false" columnalign="left">
 448          <m:mtr>
 449           <m:mtd>
 450            <m:mrow>
 451             <m:mo>LET</m:mo>
 452             <m:mphantom><m:mtext>_</m:mtext></m:mphantom>
 453             <xsl:apply-templates select="m:bvar"/>
 454            </m:mrow>
 455           </m:mtd>
 456          </m:mtr>
 457          <m:mtr>
 458           <m:mtd>
 459            <m:mrow>
 460             <m:mo>=</m:mo>
 461             <xsl:apply-templates select="*[position()=3]"/>
 462            </m:mrow>
 463           </m:mtd>
 464          </m:mtr>
 465          <m:mtr>
 466           <m:mtd>
 467            <m:mrow>
 468             <m:mo>IN</m:mo>
 469             <m:mphantom><m:mtext>_</m:mtext></m:mphantom>
 470             <xsl:apply-templates select="*[position()=4]"/>
 471            </m:mrow>
 472           </m:mtd>
 473          </m:mtr>
 474         </m:mtable>
 475        </xsl:when>
 476        <xsl:otherwise>
 477         <m:mo>LET</m:mo>
 478         <m:mphantom><m:mtext>_</m:mtext></m:mphantom>
 479         <xsl:apply-templates select="m:bvar/m:ci"/>
 480         <m:mo>=</m:mo>
 481         <xsl:apply-templates select="*[position()=3]"/>
 482         <m:mphantom><m:mtext>_</m:mtext></m:mphantom>
 483         <m:mtext>IN</m:mtext>
 484         <m:mphantom><m:mtext>_</m:mtext></m:mphantom>
 485         <xsl:apply-templates select="*[position()=4]"/>
 486        </xsl:otherwise>
 487        </xsl:choose>
 488       </xsl:when>
 489       <!-- PROD -->
 490       <xsl:when test="$name='prod'">
 491        <xsl:choose>
 492        <xsl:when test="$charlength >= $framewidth">
 493         <m:mtable align="baseline 1" equalrows="false" columnalign="left">
 494          <m:mtr>
 495           <m:mtd>
 496            <m:mrow>
 497             <m:mo mathcolor="Blue">&#x03a0;</m:mo>
 498             <xsl:apply-templates select="m:bvar"/>
 499            </m:mrow>
 500           </m:mtd>
 501          </m:mtr>
 502          <m:mtr>
 503           <m:mtd>
 504            <m:mrow>
 505             <m:mo>.</m:mo>
 506             <xsl:apply-templates select="*[position()=3]"/>
 507            </m:mrow>
 508           </m:mtd>
 509          </m:mtr>
 510         </m:mtable>
 511        </xsl:when>
 512        <xsl:otherwise>
 513         <m:mo mathcolor="Blue">&#x03a0;</m:mo>
 514         <xsl:apply-templates select="m:bvar/m:ci"/>
 515         <m:mo>:</m:mo>
 516         <xsl:apply-templates select="m:bvar/m:type"/>
 517         <m:mo>.</m:mo>
 518         <xsl:apply-templates select="*[position()=3]"/>
 519        </xsl:otherwise>
 520        </xsl:choose>
 521       </xsl:when>
 522       <!-- ARROW -->
 523       <xsl:when test="$name='arrow'">
 524        <xsl:choose>
 525        <xsl:when test="$charlength >= $framewidth">
 526         <m:mtable align="baseline 1" equalrows="false" columnalign="left">
 527          <m:mtr>
 528           <m:mtd>
 529            <m:mrow>
 530             <xsl:if test="$nopar=0">
 531              <m:mo stretchy="false">(</m:mo>
 532             </xsl:if>
 533             <xsl:apply-templates select="*[position()=2]"/>
 534            </m:mrow>
 535           </m:mtd>
 536          </m:mtr>
 537          <m:mtr>
 538           <m:mtd>
 539            <m:mrow>
 540             <m:mo mathmathcolor="Blue">&#x2192;</m:mo>
 541             <xsl:choose>
 542             <xsl:when test="*[position()=3]/m:csymbol">
 543              <xsl:variable name="nextp"><xsl:value-of select="*[position()=3]/m:csymbol"/></xsl:variable>
 544              <xsl:choose>
 545              <xsl:when test="$nextp='arrow'">
 546               <xsl:apply-templates select="*[position()=3]"><xsl:with-param name="nopar" select="1"/></xsl:apply-templates>
 547              </xsl:when>
 548              <xsl:otherwise>
 549               <xsl:apply-templates select="*[position()=3]"/>
 550              </xsl:otherwise>
 551              </xsl:choose>
 552             </xsl:when>
 553             <xsl:otherwise>
 554              <xsl:apply-templates select="*[position()=3]"/>
 555             </xsl:otherwise>
 556             </xsl:choose>
 557            </m:mrow>
 558           </m:mtd>
 559          </m:mtr>
 560          <xsl:if test="$nopar=0">
 561          <m:mtr>
 562           <m:mtd>
 563            <m:mrow>
 564             <m:mo stretchy="false">)</m:mo>
 565            </m:mrow>
 566           </m:mtd>
 567          </m:mtr>
 568          </xsl:if>
 569         </m:mtable>
 570        </xsl:when>
 571        <xsl:otherwise>
 572         <xsl:if test="$nopar=0">
 573          <m:mo stretchy="false">(</m:mo>
 574         </xsl:if>
 575         <xsl:apply-templates select="*[position()=2]"/>
 576         <m:mo mathcolor="Blue">&#x2192;</m:mo>
 577         <xsl:choose>
 578         <xsl:when test="*[position()=3]/m:csymbol">
 579          <xsl:variable name="nextp"><xsl:value-of select="*[position()=3]/m:csymbol"/></xsl:variable>
 580          <xsl:choose>
 581          <xsl:when test="$nextp='arrow'">
 582           <xsl:apply-templates select="*[position()=3]"><xsl:with-param name="nopar" select="1"/></xsl:apply-templates>
 583          </xsl:when>
 584          <xsl:otherwise>
 585           <xsl:apply-templates select="*[position()=3]"/>
 586          </xsl:otherwise>
 587          </xsl:choose>
 588         </xsl:when>
 589         <xsl:otherwise>
 590          <xsl:apply-templates select="*[position()=3]"/>
 591         </xsl:otherwise>
 592         </xsl:choose>
 593         <xsl:if test="$nopar=0">
 594          <m:mo stretchy="false">)</m:mo>
 595         </xsl:if>
 596        </xsl:otherwise>
 597        </xsl:choose>
 598       </xsl:when>
 599       <!-- APP -->
 600       <xsl:when test="$name='app'">
 601        <xsl:choose>
 602        <xsl:when test="$charlength >= $framewidth">
 603         <m:mtable align="baseline 1" equalrows="false" columnalign="left">
 604          <m:mtr>
 605           <m:mtd>
 606            <m:mrow>
 607             <m:mo stretchy="false">(</m:mo>
 608             <xsl:apply-templates select="*[position()=2]"/>
 609            </m:mrow>
 610           </m:mtd>
 611          </m:mtr>
 612          <xsl:for-each select="*[position()>2]">
 613          <m:mtr>
 614           <m:mtd>
 615            <m:mrow>
 616             <m:mphantom><m:mtext>(</m:mtext></m:mphantom>
 617             <xsl:apply-templates select="."/>
 618            </m:mrow>
 619           </m:mtd>
 620          </m:mtr>
 621          </xsl:for-each>
 622          <m:mtr>
 623           <m:mtd>
 624            <m:mrow>
 625             <m:mo stretchy="false">)</m:mo>
 626            </m:mrow>
 627           </m:mtd>
 628          </m:mtr>
 629         </m:mtable>
 630        </xsl:when>
 631        <xsl:otherwise>
 632         <m:mo stretchy="false">(</m:mo>
 633         <xsl:apply-templates select="*[position()=2]"/>
 634         <xsl:for-each select="*[position()>2]">
 635          <m:mphantom><m:mtext>_</m:mtext></m:mphantom>
 636          <xsl:apply-templates select="."/>
 637         </xsl:for-each>
 638         <m:mo stretchy="false">)</m:mo>
 639        </xsl:otherwise>
 640        </xsl:choose>
 641       </xsl:when>
 642       <!-- CAST -->
 643       <xsl:when test="$name='cast'">
 644        <xsl:choose>
 645        <xsl:when test="$charlength >= $framewidth">
 646         <m:mtable align="baseline 1" equalrows="false" columnalign="left">
 647          <m:mtr>
 648           <m:mtd>
 649            <m:mrow>
 650             <m:mo stretchy="false">(</m:mo>
 651             <xsl:apply-templates select="*[position()=2]"/>
 652            </m:mrow>
 653           </m:mtd>
 654          </m:mtr>
 655          <m:mtr>
 656           <m:mtd>
 657            <m:mrow>
 658             <m:mo mathcolor="Maroon">:></m:mo>
 659             <xsl:apply-templates select="*[position()=3]"/>
 660            </m:mrow>
 661           </m:mtd>
 662          </m:mtr>
 663          <m:mtr>
 664           <m:mtd>
 665            <m:mrow>
 666             <m:mo stretchy="false">)</m:mo>
 667            </m:mrow>
 668           </m:mtd>
 669          </m:mtr>
 670         </m:mtable>
 671        </xsl:when>
 672        <xsl:otherwise>
 673         <m:mo stretchy="false">(</m:mo>
 674         <xsl:apply-templates select="*[position()=2]"/>
 675         <m:mo mathcolor="Maroon">:></m:mo>
 676         <xsl:apply-templates select="*[position()=3]"/>
 677         <m:mo stretchy="false">)</m:mo>
 678        </xsl:otherwise>
 679        </xsl:choose>
 680       </xsl:when>
 681       <!-- PROP -->
 682       <xsl:when test="$name='Prop'">
 683        <m:mo>Prop</m:mo>
 684       </xsl:when>
 685       <!-- SET -->
 686       <xsl:when test="$name='Set'">
 687        <m:mo>Set</m:mo>
 688       </xsl:when>
 689       <!-- TYPE -->
 690       <xsl:when test="$name='Type'">
 691        <m:mo>Type</m:mo>
 692       </xsl:when>
 693       <!-- MUTCASE -->
 694       <xsl:when test="$name='mutcase'">
 695        <xsl:choose>
 696        <xsl:when test="$charlength >= $framewidth">
 697         <xsl:variable name="charlength"><xsl:apply-templates select="*[position()=2]" mode="charcount"><xsl:with-param name="nosibling" select="1"/></xsl:apply-templates></xsl:variable>
 698         <m:mtable align="baseline 1" equalrows="false" columnalign="left">
 699          <m:mtr>
 700           <m:mtd>
 701            <m:mrow>
 702             <m:mo>&lt;</m:mo>
 703             <xsl:apply-templates select="*[position()=2]"/>
 704             <xsl:if test="$framewidth > $charlength">
 705              <m:mo>&gt;</m:mo>
 706              <m:mo>CASES</m:mo>
 707              <m:mphantom><m:mtext>_</m:mtext></m:mphantom>
 708              <xsl:apply-templates select="*[position()=3]"/>
 709             </xsl:if>
 710            </m:mrow>
 711           </m:mtd>
 712          </m:mtr>
 713          <xsl:if test="$charlength >= $framewidth">
 714          <m:mtr>
 715           <m:mtd>
 716            <m:mrow>
 717             <m:mo>&gt;</m:mo>
 718             <m:mo>CASES</m:mo>
 719             <m:mphantom><m:mtext>_</m:mtext></m:mphantom>
 720             <xsl:apply-templates select="*[position()=3]"/>
 721            </m:mrow>
 722           </m:mtd>
 723          </m:mtr>
 724          </xsl:if>
 725          <m:mtr>
 726           <m:mtd>
 727            <m:mrow>
 728             <m:mo>OF</m:mo>
 729            </m:mrow>
 730           </m:mtd>
 731          </m:mtr>
 732          <xsl:for-each select="*[position() mod 2 = 0 and position()>3]">
 733          <xsl:variable name="charlength"><xsl:apply-templates select="." mode="charcount"><xsl:with-param name="nosibling" select="1"/></xsl:apply-templates></xsl:variable>
 734          <m:mtr>
 735           <m:mtd>
 736            <m:mrow>
 737             <xsl:choose>
 738             <xsl:when test="position() = 1">
 739               <m:mphantom><m:mtext>|</m:mtext></m:mphantom>
 740             </xsl:when>
 741             <xsl:otherwise>
 742              <m:mo stretchy="false">|</m:mo>
 743             </xsl:otherwise>
 744             </xsl:choose>
 745             <m:mphantom><m:mtext>_</m:mtext></m:mphantom>
 746             <xsl:apply-templates select="."/>
 747             <xsl:if test="$framewidth > $charlength">
 748              <m:mo mathcolor="Green">&#x21d2;</m:mo>
 749              <xsl:apply-templates select="following-sibling::*[position()= 1]"/>
 750             </xsl:if>
 751            </m:mrow>
 752           </m:mtd>
 753          </m:mtr>
 754          <xsl:if test="$charlength >= $framewidth">
 755          <m:mtr>
 756           <m:mtd>
 757            <m:mrow>
 758             <m:mphantom><m:mtext>|_</m:mtext></m:mphantom>
 759             <m:mo mathcolor="Green">&#x21d2;</m:mo>
 760             <xsl:apply-templates select="following-sibling::*[position()= 1]"/>
 761            </m:mrow>
 762           </m:mtd>
 763          </m:mtr>
 764          </xsl:if>
 765         </xsl:for-each>
 766          <m:mtr>
 767           <m:mtd>
 768            <m:mrow>
 769             <m:mo>END</m:mo>
 770            </m:mrow>
 771           </m:mtd>
 772          </m:mtr>
 773         </m:mtable>
 774        </xsl:when>
 775        <xsl:otherwise>
 776         <m:mo>&lt;</m:mo><xsl:apply-templates select="*[position()=2]"/><m:mo>&gt;</m:mo>
 777         <m:mo>CASES</m:mo>
 778         <m:mphantom><m:mtext>_</m:mtext></m:mphantom>
 779         <xsl:apply-templates select="*[position()=3]"/>
 780         <m:mphantom><m:mtext>_</m:mtext></m:mphantom>
 781         <m:mo>OF</m:mo>
 782         <xsl:for-each select="*[position() mod 2 = 0 and position()>3]">
 783          <xsl:choose>
 784          <xsl:when test="position() != 1">
 785           <m:mo stretchy="false">|</m:mo>
 786          </xsl:when>
 787          </xsl:choose>
 788          <xsl:apply-templates select="."/>
 789          <m:mo mathcolor="Green">&#x21d2;</m:mo>
 790          <xsl:apply-templates select="following-sibling::*[position()= 1]"/>
 791         </xsl:for-each>
 792         <m:mphantom><m:mtext>_</m:mtext></m:mphantom>
 793         <m:mo>END</m:mo>
 794        </xsl:otherwise>
 795        </xsl:choose>
 796       </xsl:when>
 797       <!-- FIX -->
 798       <xsl:when test="$name='fix'">
 799        <xsl:choose>
 800        <xsl:when test="$charlength >= $framewidth">
 801         <m:mtable align="baseline 1" equalrows="false" columnalign="left">
 802          <m:mtr>
 803           <m:mtd>
 804            <m:mrow>
 805             <m:mo>FIX</m:mo>
 806             <m:mphantom><m:mtext>_</m:mtext></m:mphantom>
 807             <m:mi><xsl:value-of select="m:ci"/></m:mi>
 808             <m:mo stretchy="false">{</m:mo>
 809            </m:mrow>
 810           </m:mtd>
 811          </m:mtr>
 812          <m:mtr>
 813           <m:mtd>
 814            <m:mrow>
 815             <m:mphantom><m:mtext>__</m:mtext></m:mphantom>
 816             <m:mtable align="baseline 1" equalrows="false" columnalign="left">
 817             <xsl:for-each select="m:bvar">
 818              <xsl:variable name="charlength"><xsl:apply-templates select="m:type" mode="charcount"><xsl:with-param name="nosibling" select="1"/></xsl:apply-templates></xsl:variable>
 819              <m:mtr>
 820               <m:mtd>
 821                <m:mrow>
 822                 <m:mi><xsl:value-of select="m:ci"/></m:mi>
 823                 <m:mo>:</m:mo>
 824                 <xsl:if test="$framewidth > $charlength">
 825                  <xsl:apply-templates select="m:type"/>
 826                 </xsl:if>
 827                </m:mrow>
 828               </m:mtd>
 829              </m:mtr>
 830              <xsl:if test="$charlength >= $framewidth">
 831              <m:mtr>
 832               <m:mtd>
 833                <m:mrow>
 834                 <m:mphantom><m:mtext>:=</m:mtext></m:mphantom>
 835                 <xsl:apply-templates select="m:type"/>
 836                </m:mrow>
 837               </m:mtd>
 838              </m:mtr>
 839              </xsl:if>
 840              <m:mtr>
 841               <m:mtd>
 842                <m:mrow>
 843                 <m:mo>:=</m:mo>
 844                 <xsl:apply-templates select="following-sibling::*[position()=1]"/>
 845                </m:mrow>
 846               </m:mtd>
 847              </m:mtr>
 848             </xsl:for-each>
 849             </m:mtable>
 850            </m:mrow>
 851           </m:mtd>
 852          </m:mtr>
 853          <m:mtr>
 854           <m:mtd>
 855            <m:mrow>
 856             <m:mo stretchy="false">}</m:mo>
 857            </m:mrow>
 858           </m:mtd>
 859          </m:mtr>
 860         </m:mtable>
 861        </xsl:when>
 862        <xsl:otherwise>
 863         <m:mo>FIX</m:mo>
 864         <m:mi><xsl:value-of select="m:ci"/></m:mi>
 865         <m:mo stretchy="false">{</m:mo>
 866         <m:mtable align="baseline 1" equalrows="false" columnalign="left">
 867         <xsl:for-each select="m:bvar">
 868          <m:mtr>
 869           <m:mtd>
 870            <m:mrow>
 871             <m:mi><xsl:value-of select="m:ci"/></m:mi>
 872             <m:mo>:</m:mo>
 873             <xsl:apply-templates select="m:type"/>
 874             <m:mo>:=</m:mo>
 875             <xsl:apply-templates select="following-sibling::*[position() = 1]"/>
 876             <xsl:if test="position()=last()">
 877              <m:mo stretchy="false">}</m:mo>
 878             </xsl:if>
 879            </m:mrow>
 880           </m:mtd>
 881          </m:mtr>
 882          </xsl:for-each>
 883         </m:mtable>
 884        </xsl:otherwise>
 885        </xsl:choose>
 886       </xsl:when>
 887       <!-- COFIX -->
 888       <xsl:when test="$name='cofix'">
 889        <xsl:choose>
 890        <xsl:when test="$charlength >= $framewidth">
 891         <m:mtable align="baseline 1" equalrows="false" columnalign="left">
 892          <m:mtr>
 893           <m:mtd>
 894            <m:mrow>
 895             <m:mo>COFIX</m:mo>
 896             <m:mphantom><m:mtext>_</m:mtext></m:mphantom>
 897             <m:mi><xsl:value-of select="m:ci"/></m:mi>
 898             <m:mo stretchy="false">{</m:mo>
 899            </m:mrow>
 900           </m:mtd>
 901          </m:mtr>
 902          <m:mtr>
 903           <m:mtd>
 904            <m:mrow>
 905             <m:mphantom><m:mtext>__</m:mtext></m:mphantom>
 906             <m:mtable align="baseline 1" equalrows="false" columnalign="left">
 907             <xsl:for-each select="m:bvar">
 908              <xsl:variable name="charlength"><xsl:apply-templates select="m:type" mode="charcount"><xsl:with-param name="nosibling" select="1"/></xsl:apply-templates></xsl:variable>
 909              <m:mtr>
 910               <m:mtd>
 911                <m:mrow>
 912                 <m:mi><xsl:value-of select="m:ci"/></m:mi>
 913                 <m:mo>:</m:mo>
 914                 <xsl:if test="$framewidth > $charlength">
 915                  <xsl:apply-templates select="m:type"/>
 916                 </xsl:if>
 917                </m:mrow>
 918               </m:mtd>
 919              </m:mtr>
 920              <xsl:if test="$charlength >= $framewidth">
 921              <m:mtr>
 922               <m:mtd>
 923                <m:mrow>
 924                 <m:mphantom><m:mtext>:=</m:mtext></m:mphantom>
 925                 <xsl:apply-templates select="m:type"/>
 926                </m:mrow>
 927               </m:mtd>
 928              </m:mtr>
 929              </xsl:if>
 930              <m:mtr>
 931               <m:mtd>
 932                <m:mrow>
 933                 <m:mo>:=</m:mo>
 934                 <xsl:apply-templates select="following-sibling::*[position() = 1]"/>
 935                </m:mrow>
 936               </m:mtd>
 937              </m:mtr>
 938             </xsl:for-each>
 939             </m:mtable>
 940            </m:mrow>
 941           </m:mtd>
 942          </m:mtr>
 943          <m:mtr>
 944           <m:mtd>
 945            <m:mrow>
 946             <m:mo stretchy="false">}</m:mo>
 947            </m:mrow>
 948           </m:mtd>
 949          </m:mtr>
 950         </m:mtable>
 951        </xsl:when>
 952        <xsl:otherwise>
 953         <m:mo>COFIX</m:mo>
 954         <m:mi><xsl:value-of select="m:ci"/></m:mi>
 955         <m:mo stretchy="false">{</m:mo>
 956         <m:mtable align="baseline 1" equalrows="false" columnalign="left">
 957         <xsl:for-each select="m:bvar">
 958          <m:mtr>
 959           <m:mtd>
 960            <m:mrow>
 961             <m:mi><xsl:value-of select="m:ci"/></m:mi>
 962             <m:mo>:</m:mo>
 963             <xsl:apply-templates select="m:type"/>
 964             <m:mo>:=</m:mo>
 965             <xsl:apply-templates select="following-sibling::*[position() = 1]"/>
 966             <xsl:if test="position()=last()">
 967              <m:mo stretchy="false">}</m:mo>
 968             </xsl:if>
 969            </m:mrow>
 970           </m:mtd>
 971          </m:mtr>
 972          </xsl:for-each>
 973         </m:mtable>
 974        </xsl:otherwise>
 975        </xsl:choose>
 976       </xsl:when>
 977       <!-- ***************************************** -->
 978       <!-- *********** PROOF ELEMENTS ************** -->
 979       <!-- ***************************************** -->
 980       <!-- PROOF -->
 981       <xsl:when test="$name='proof'">
 982         <m:mtable align="baseline 1" equalrows="false" columnalign="left">
 983          <m:mtr>
 984           <m:mtd>
 985            <m:mrow>
 986             <xsl:apply-templates select="*[position()=2]"/>
 987            </m:mrow>
 988           </m:mtd>
 989          </m:mtr>
 990          <m:mtr>
 991           <m:mtd>
 992            <m:mrow>
 993             <m:mtext mathcolor="Maroon">we proved </m:mtext>
 994             <m:mphantom><m:mtext>_</m:mtext></m:mphantom>
 995             <xsl:apply-templates select="*[position()=3]"/>
 996            </m:mrow>
 997           </m:mtd>
 998          </m:mtr>
 999         </m:mtable>
1000       </xsl:when>
1001       <!-- LETIN1 -->
1002       <xsl:when test="$name='letin1'">
1003         <m:mtable align="baseline 1" equalrows="false" columnalign="left">
1004          <m:mtr>
1005           <m:mtd>
1006            <m:mrow>
1007             <xsl:apply-templates select="*[2]"/>
1008            </m:mrow>
1009           </m:mtd>
1010          </m:mtr>
1011          <m:mtr>
1012           <m:mtd>
1013            <m:mrow>
1014             <xsl:apply-templates select="*[3]"/>
1015            </m:mrow>
1016           </m:mtd>
1017          </m:mtr>
1018         </m:mtable>
1019       </xsl:when>
1020
1021       <!-- CSC: Il caso che segue e' stato buttato li' giusto per vedere -->
1022       <!-- qualche cosa. Irene, appena puoi, risistemalo.                -->
1023       <xsl:when test="$name='by_induction'">
1024        <m:mtable align="baseline 1" equalrows="false" columnalign="left">
1025         <m:mtr>
1026          <m:mtd>
1027           <m:mrow>
1028            <m:mtext mathcolor="red">We prove </m:mtext>
1029            <m:mphantom><m:mtext>_</m:mtext></m:mphantom>
1030            <xsl:apply-templates select="../*[3]"/>
1031           </m:mrow>
1032          </m:mtd>
1033         </m:mtr>
1034         <m:mtr>
1035          <m:mtd>
1036           <m:mrow>
1037            <m:mtext mathcolor="red">by induction on </m:mtext>
1038            <m:mphantom><m:mtext>_</m:mtext></m:mphantom>
1039            <xsl:apply-templates
1040             select="*[position()=last()]/*[position()=last()]"/>
1041           </m:mrow>
1042          </m:mtd>
1043         </m:mtr>
1044         <m:mtr>
1045          <m:mtd>
1046           <m:mrow>
1047            <m:mphantom><m:mtext>_</m:mtext></m:mphantom>
1048            <m:mtable align="baseline 1" equalrows="false" columnalign="left">
1049             <xsl:for-each select="*[position()>3 and not(position()=last())]">
1050              <m:mtr>
1051               <m:mtd>
1052                <xsl:apply-templates select="."/>
1053               </m:mtd>
1054              </m:mtr>
1055             </xsl:for-each>
1056            </m:mtable>
1057           </m:mrow>
1058          </m:mtd>
1059         </m:mtr>
1060        </m:mtable>
1061       </xsl:when>
1062       <!-- inductive_case -->
1063       <xsl:when test="$name='inductive_case'">
1064        <m:mtable align="baseline 1" equalrows="false" columnalign="left">
1065         <m:mtr>
1066          <m:mtd>
1067           <m:mrow>
1068            <m:mtext mathcolor="red">Case </m:mtext>
1069            <m:mphantom><m:mtext>_</m:mtext></m:mphantom>
1070            <xsl:apply-templates select="*[2]"/>
1071           </m:mrow>
1072          </m:mtd>
1073         </m:mtr>
1074         <m:mtr>
1075          <m:mtd>
1076           <m:mrow>
1077            <m:mphantom><m:mtext>_</m:mtext></m:mphantom>
1078            <m:mtable align="baseline 1" equalrows="false" columnalign="left">
1079             <xsl:if test="*[3]/*[position()>1]">
1080              <m:mtr>
1081               <m:mtd>
1082                <m:mtext mathcolor="red">By induction hypothesis, we have:</m:mtext>
1083               </m:mtd>
1084              </m:mtr>
1085              <m:mtr>
1086               <m:mtd>
1087                <m:mrow>
1088                 <m:mphantom><m:mtext>_</m:mtext></m:mphantom>
1089                 <xsl:for-each select="*[3]/*[position()>1]">
1090                  <m:mo stretchy="false">(</m:mo>
1091                  <xsl:apply-templates select="m:ci"/>
1092                  <m:mo stretchy="false">) </m:mo>
1093                  <m:mphantom><m:mtext>_</m:mtext></m:mphantom>
1094                  <xsl:apply-templates select="m:type"/>
1095                 </xsl:for-each>
1096                </m:mrow>
1097               </m:mtd>
1098              </m:mtr>
1099             </xsl:if>
1100             <m:mtr>
1101              <m:mtd>
1102               <xsl:apply-templates select="*[4]"/>
1103              </m:mtd>
1104             </m:mtr>
1105            </m:mtable>
1106           </m:mrow>
1107          </m:mtd>
1108         </m:mtr>
1109        </m:mtable>
1110       </xsl:when>
1111       <!-- case_lhs  -->
1112       <xsl:when test="$name='case_lhs'">
1113        <m:mrow>
1114         <xsl:choose>
1115          <xsl:when test="count(*)=2">
1116           <xsl:apply-templates select="*[2]"/>
1117          </xsl:when>
1118          <xsl:otherwise>
1119           <m:mo stretchy="false">(</m:mo>
1120           <xsl:apply-templates select="*[2]"/>
1121           <xsl:for-each select="m:bvar">
1122            <m:mphantom><m:mtext>_</m:mtext></m:mphantom>
1123            <xsl:apply-templates select="*[1]"/>
1124            <m:mtext>:</m:mtext>
1125            <xsl:apply-templates select="m:type/*[1]"/>
1126           </xsl:for-each>
1127           <m:mo stretchy="false">)</m:mo>
1128          </xsl:otherwise>
1129         </xsl:choose>
1130        </m:mrow>
1131       </xsl:when>
1132       <xsl:when test="$name='false_ind'">
1133        <m:mtable align="baseline 1" equalrows="false" columnalign="left">
1134         <m:mtr>
1135          <m:mtd>
1136           <m:mrow>
1137            <xsl:apply-templates select="*[3]"/>
1138           </m:mrow>
1139          </m:mtd>
1140         </m:mtr>
1141         <m:mtr>
1142          <m:mtd>
1143           <m:mrow>
1144            <m:mtext mathcolor="Red">Contradiction.</m:mtext>
1145           </m:mrow>
1146          </m:mtd>
1147         </m:mtr>
1148        </m:mtable>
1149       </xsl:when>
1150       <!--CSC fine della parte da risistemare -->
1151
1152       <!-- LET-IN -->
1153       <xsl:when test="$name='letin'">
1154         <m:mtable align="baseline 1" equalrows="false" columnalign="left">
1155          <!-- <xsl:for-each select="APPLY[m:csymbol and (string(m:csymbol)='let')]"> -->
1156          <xsl:for-each select="*[(last() > position()) and (position()>1)]">
1157          <m:mtr>
1158           <m:mtd>
1159            <m:mrow>
1160             <xsl:apply-templates select="."/>
1161            </m:mrow>
1162           </m:mtd>
1163          </m:mtr>
1164          </xsl:for-each>
1165          <m:mtr>
1166           <m:mtd>
1167            <m:mrow>
1168             <xsl:apply-templates select="*[position()=last()]"/>
1169            </m:mrow>
1170           </m:mtd>
1171          </m:mtr>
1172         </m:mtable>
1173       </xsl:when>
1174       <!-- LET -->
1175       <xsl:when test="$name='let'">
1176        <m:mtext>(</m:mtext>
1177        <xsl:apply-templates select="m:ci"/>
1178        <m:mtext>) </m:mtext>
1179        <xsl:apply-templates select="*[3]"/>
1180       </xsl:when>
1181       <!-- RW_STEP -->
1182       <xsl:when test="$name='rw_step'">
1183         <m:mtable align="baseline 1" equalrows="false" columnalign="left">
1184          <m:mtr>
1185           <m:mtd>
1186            <m:mrow>
1187             <xsl:choose>
1188              <xsl:when test="name(*[2])='m:apply'">
1189               <xsl:apply-templates select="*[2]"/>
1190              </xsl:when>
1191              <xsl:otherwise>
1192               <m:mtext>Consider</m:mtext>
1193               <m:mphantom><m:mtext>_</m:mtext></m:mphantom>
1194               <xsl:apply-templates select="*[2]"/>
1195              </xsl:otherwise>
1196             </xsl:choose>
1197            </m:mrow>
1198           </m:mtd>
1199          </m:mtr>
1200          <m:mtr>
1201           <m:mtd>
1202            <m:mrow>
1203             <m:mtext>Rewrite</m:mtext>
1204             <m:mphantom><m:mtext>_</m:mtext></m:mphantom>
1205             <xsl:apply-templates select="*[3]"/>
1206             <m:mphantom><m:mtext>_</m:mtext></m:mphantom>
1207             <m:mtext>with</m:mtext>
1208             <m:mphantom><m:mtext>_</m:mtext></m:mphantom>
1209             <xsl:apply-templates select="*[4]"/>
1210             <m:mphantom><m:mtext>_</m:mtext></m:mphantom>
1211             <m:mtext>by</m:mtext>
1212             <m:mphantom><m:mtext>_</m:mtext></m:mphantom>
1213             <xsl:apply-templates select="*[5]"/>
1214            </m:mrow>
1215           </m:mtd>
1216          </m:mtr>
1217         </m:mtable>
1218       </xsl:when>
1219       <!-- not existing any more
1220       <xsl:when test="$name='thread'">
1221         <m:mtable align="baseline 1" equalrows="false" columnalign="left">
1222          <m:mtr>
1223           <m:mtd>
1224            <m:mrow>
1225             <xsl:choose>
1226              <xsl:when test="name(*[last()])='m:apply'">
1227               <xsl:apply-templates select="*[last()]"/>
1228              </xsl:when>
1229              <xsl:otherwise>
1230               <m:mtext>Consider</m:mtext>
1231               <m:mphantom><m:mtext>_</m:mtext></m:mphantom>
1232               <xsl:apply-templates select="*[last()]"/>
1233              </xsl:otherwise>
1234             </xsl:choose>
1235            </m:mrow>
1236           </m:mtd>
1237          </m:mtr>
1238          <xsl:apply-templates mode="thread" select="*[(last()-2)]"/>
1239         </m:mtable>
1240       </xsl:when>
1241       -->
1242       <!-- REWRITE_AND_APPLY -->
1243       <xsl:when test="$name='rewrite_and_apply'">
1244         <m:mtable align="baseline 1" equalrows="false" columnalign="left">
1245          <m:mtr>
1246           <m:mtd>
1247            <m:mrow>
1248             <xsl:apply-templates select="*[2]"/>
1249            </m:mrow>
1250           </m:mtd>
1251          </m:mtr>
1252          <m:mtr>
1253           <m:mtd>
1254            <m:mrow>
1255             <m:mtext>Then apply it to</m:mtext>
1256             <m:mphantom><m:mtext>_</m:mtext></m:mphantom>
1257             <xsl:apply-templates select="*[position()>2]"/>
1258            </m:mrow>
1259           </m:mtd>
1260          </m:mtr>
1261        </m:mtable>
1262       </xsl:when>
1263       <!-- AND_IND -->
1264       <xsl:when test="$name='and_ind'">
1265         <m:mtable align="baseline 1" equalrows="false" columnalign="left">
1266          <m:mtr>
1267           <m:mtd>
1268            <m:mrow>
1269             <xsl:choose>
1270              <xsl:when test="name(*[2])='m:apply'">
1271               <xsl:apply-templates select="*[2]"/>
1272              </xsl:when>
1273              <xsl:otherwise>
1274               <m:mtext>Consider</m:mtext>
1275               <m:mphantom><m:mtext>_</m:mtext></m:mphantom>
1276               <xsl:apply-templates select="*[2]"/>
1277              </xsl:otherwise>
1278             </xsl:choose>
1279            </m:mrow>
1280           </m:mtd>
1281          </m:mtr>
1282          <m:mtr>
1283           <m:mtd>
1284            <m:mrow>
1285             <m:mtext>In particular, we have</m:mtext>
1286            </m:mrow>
1287           </m:mtd>
1288          </m:mtr>
1289          <m:mtr>
1290           <m:mtd>
1291            <m:mrow>
1292             <m:mtext>(</m:mtext>
1293             <xsl:apply-templates select="*[3]"/>
1294             <m:mtext>)</m:mtext>
1295             <m:mphantom><m:mtext>_</m:mtext></m:mphantom>
1296             <xsl:apply-templates select="*[4]"/>
1297             </m:mrow>
1298           </m:mtd>
1299          </m:mtr>
1300          <m:mtr>
1301           <m:mtd>
1302            <m:mrow>
1303             <m:mtext>(</m:mtext>
1304             <xsl:apply-templates select="*[5]"/>
1305             <m:mtext>)</m:mtext>
1306             <m:mphantom><m:mtext>_</m:mtext></m:mphantom>
1307             <xsl:apply-templates select="*[6]"/>
1308             </m:mrow>
1309           </m:mtd>
1310          </m:mtr>
1311          <m:mtr>
1312           <m:mtd>
1313            <m:mrow>
1314             <xsl:apply-templates select="*[7]"/>
1315            </m:mrow>
1316           </m:mtd>
1317          </m:mtr>
1318         </m:mtable>
1319       </xsl:when>
1320       <!-- CSC: Il caso che segue e' stato buttato li' giusto per vedere -->
1321       <!-- qualche cosa. Irene, appena puoi, risistemalo.                -->
1322       <!-- full_or_ind -->
1323       <xsl:when test="$name='full_or_ind'">
1324         <m:mtable align="baseline 1" equalrows="false" columnalign="left">
1325          <m:mtr>
1326           <m:mtd>
1327            <m:mrow>
1328             <xsl:choose>
1329              <xsl:when test="name(*[2])='m:apply'">
1330               <xsl:apply-templates select="*[2]"/>
1331              </xsl:when>
1332              <xsl:otherwise>
1333               <m:mtext>Consider</m:mtext>
1334               <m:mphantom><m:mtext>_</m:mtext></m:mphantom>
1335               <xsl:apply-templates select="*[2]"/>
1336              </xsl:otherwise>
1337             </xsl:choose>
1338            </m:mrow>
1339           </m:mtd>
1340          </m:mtr>
1341          <m:mtr>
1342           <m:mtd>
1343            <m:mrow>
1344             <m:mtext>We proceed by cases to prove</m:mtext>
1345             <m:mphantom><m:mtext>_</m:mtext></m:mphantom>
1346             <xsl:apply-templates select="*[3]"/>
1347            </m:mrow>
1348           </m:mtd>
1349          </m:mtr>
1350          <m:mtr>
1351           <m:mtd>
1352            <m:mrow>
1353             <m:mtext>Left: suppose</m:mtext>
1354             <m:mphantom><m:mtext>_</m:mtext></m:mphantom>
1355             <m:mo stretchy="false">(</m:mo>
1356             <xsl:apply-templates select="*[4]/m:bvar/m:ci"/>
1357             <m:mo stretchy="false">)</m:mo>
1358             <m:mphantom><m:mtext>_</m:mtext></m:mphantom>
1359             <xsl:apply-templates select="*[4]/m:bvar/m:type/*[1]"/>
1360            </m:mrow>
1361           </m:mtd>
1362          </m:mtr>
1363          <m:mtr>
1364           <m:mtd>
1365            <m:mphantom><m:mtext>_</m:mtext></m:mphantom>
1366            <m:mrow>
1367             <xsl:apply-templates select="*[4]/*[3]"/>
1368            </m:mrow>
1369           </m:mtd>
1370          </m:mtr>
1371          <m:mtr>
1372           <m:mtd>
1373            <m:mrow>
1374             <m:mtext>Right: suppose</m:mtext>
1375             <m:mphantom><m:mtext>_</m:mtext></m:mphantom>
1376             <m:mo stretchy="false">(</m:mo>
1377             <xsl:apply-templates select="*[5]/m:bvar/m:ci"/>
1378             <m:mo stretchy="false">)</m:mo>
1379             <m:mphantom><m:mtext>_</m:mtext></m:mphantom>
1380             <xsl:apply-templates select="*[5]/m:bvar/m:type/*[1]"/>
1381            </m:mrow>
1382           </m:mtd>
1383          </m:mtr>
1384          <m:mtr>
1385           <m:mtd>
1386            <m:mrow>
1387             <xsl:apply-templates select="*[5]/*[3]"/>
1388            </m:mrow>
1389           </m:mtd>
1390          </m:mtr>
1391         </m:mtable>
1392       </xsl:when>
1393       <!--CSC fine della parte da risistemare -->
1394       <!-- OR_IND -->
1395       <xsl:when test="$name='or_ind'">
1396         <m:mtable align="baseline 1" equalrows="false" columnalign="left">
1397          <m:mtr>
1398           <m:mtd>
1399            <m:mrow>
1400             <xsl:choose>
1401              <xsl:when test="name(*[2])='m:apply'">
1402               <xsl:apply-templates select="*[2]"/>
1403              </xsl:when>
1404              <xsl:otherwise>
1405               <m:mtext>Consider</m:mtext>
1406               <m:mphantom><m:mtext>_</m:mtext></m:mphantom>
1407               <xsl:apply-templates select="*[2]"/>
1408              </xsl:otherwise>
1409             </xsl:choose>
1410            </m:mrow>
1411           </m:mtd>
1412          </m:mtr>
1413          <m:mtr>
1414           <m:mtd>
1415            <m:mrow>
1416             <m:mtext>We prove</m:mtext>
1417             <m:mphantom><m:mtext>_</m:mtext></m:mphantom>
1418             <xsl:apply-templates select="*[3]"/>
1419             <m:mphantom><m:mtext>_</m:mtext></m:mphantom>
1420             <m:mtext>by cases:</m:mtext>
1421            </m:mrow>
1422           </m:mtd>
1423          </m:mtr>
1424          <m:mtr>
1425           <m:mtd>
1426            <m:mrow>
1427             <m:mtext>Left</m:mtext>
1428             <xsl:apply-templates select="*[4]"/>
1429            </m:mrow>
1430           </m:mtd>
1431          </m:mtr>
1432          <m:mtr>
1433           <m:mtd>
1434            <m:mrow>
1435             <m:mtext>Right</m:mtext>
1436             <xsl:apply-templates select="*[5]"/>
1437            </m:mrow>
1438           </m:mtd>
1439          </m:mtr>
1440         </m:mtable>
1441       </xsl:when>
1442       <!-- EX_IND -->
1443       <xsl:when test="$name='ex_ind'">
1444         <m:mtable align="baseline 1" equalrows="false" columnalign="left">
1445          <m:mtr>
1446           <m:mtd>
1447            <m:mrow>
1448             <xsl:choose>
1449              <xsl:when test="name(*[2])='m:apply'">
1450               <xsl:apply-templates select="*[2]"/>
1451              </xsl:when>
1452              <xsl:otherwise>
1453               <m:mtext>Consider</m:mtext>
1454               <m:mphantom><m:mtext>_</m:mtext></m:mphantom>
1455               <xsl:apply-templates select="*[2]"/>
1456              </xsl:otherwise>
1457             </xsl:choose>
1458            </m:mrow>
1459           </m:mtd>
1460          </m:mtr>
1461          <m:mtr>
1462           <m:mtd>
1463            <m:mrow>
1464             <m:mtext>Let</m:mtext>
1465             <m:mphantom><m:mtext>_</m:mtext></m:mphantom>
1466             <xsl:apply-templates select="*[3]"/>
1467             <m:mtext>:</m:mtext>
1468             <xsl:apply-templates select="*[4]"/>
1469             <m:mphantom><m:mtext>_</m:mtext></m:mphantom>
1470             <m:mtext>such that</m:mtext>
1471             <m:mphantom><m:mtext>_</m:mtext></m:mphantom>
1472             <m:mtext>(</m:mtext>
1473              <xsl:apply-templates select="*[5]"/>
1474             <m:mtext>)</m:mtext>
1475             <m:mphantom><m:mtext>_</m:mtext></m:mphantom>
1476             <xsl:apply-templates select="*[6]"/>
1477            </m:mrow>
1478           </m:mtd>
1479          </m:mtr>
1480          <m:mtr>
1481           <m:mtd>
1482            <m:mrow>
1483             <xsl:apply-templates select="*[7]"/>
1484            </m:mrow>
1485           </m:mtd>
1486          </m:mtr>
1487         </m:mtable>
1488       </xsl:when>
1489       <!-- ERROR -->
1490       <xsl:otherwise>
1491        <m:mi>ERROR</m:mi>
1492       </xsl:otherwise>
1493      </xsl:choose>
1494     </m:mrow>
1495 </xsl:template>
1496
1497 <!-- Il modo Thread non esiste piu'
1498 <xsl:template match="*" mode="thread">
1499  <xsl:variable name="name"><xsl:value-of select="following-sibling::*[position()=1]/m:csymbol"/></xsl:variable>
1500  <xsl:choose>
1501   <xsl:when test="$name='rw_step'">
1502          <m:mtr>
1503           <m:mtd>
1504            <m:mrow>
1505             <m:mtext>Rewrite</m:mtext>
1506             <m:mphantom><m:mtext>_</m:mtext></m:mphantom>
1507             <xsl:apply-templates select="following-sibling::*[position()=1]/*[2]"/>
1508             <m:mphantom><m:mtext>_</m:mtext></m:mphantom>
1509             <m:mtext>with</m:mtext>
1510             <m:mphantom><m:mtext>_</m:mtext></m:mphantom>
1511             <xsl:apply-templates select="following-sibling::*[position()=1]/*[3]"/>
1512             <m:mphantom><m:mtext>_</m:mtext></m:mphantom>
1513             <m:mtext>by</m:mtext>
1514             <m:mphantom><m:mtext>_</m:mtext></m:mphantom>
1515             <xsl:apply-templates select="following-sibling::*[position()=1]/*[4]"/>
1516            </m:mrow>
1517           </m:mtd>
1518          </m:mtr>
1519          <m:mtr>
1520           <m:mtd>
1521            <m:mrow>
1522             <m:mtext mathcolor="Maroon">we get</m:mtext>
1523             <m:mphantom><m:mtext>_</m:mtext></m:mphantom>
1524             <xsl:apply-templates select="."/>
1525            </m:mrow>
1526           </m:mtd>
1527          </m:mtr>
1528    </xsl:when>
1529    <xsl:otherwise>
1530          <m:mtr>
1531           <m:mtd>
1532            <m:mrow>
1533             <xsl:apply-templates select="following-sibling::*[position()=1]"/>
1534            </m:mrow>
1535           </m:mtd>
1536          </m:mtr>
1537          <m:mtr>
1538           <m:mtd>
1539            <m:mrow>
1540             <m:mtext mathcolor="Maroon">we get</m:mtext>
1541             <m:mphantom><m:mtext>_</m:mtext></m:mphantom>
1542             <xsl:apply-templates select="."/>
1543            </m:mrow>
1544           </m:mtd>
1545          </m:mtr>
1546     </xsl:otherwise>
1547    </xsl:choose>
1548          <xsl:apply-templates mode="thread" select="preceding-sibling::*[position()=2]"/>
1549 </xsl:template>
1550 -->
1551
1552 <!-- LAMBDA -->
1553
1554 <xsl:template match="m:lambda">
1555     <xsl:variable name="charlength"><xsl:apply-templates select="*[position()=1]" mode="charcount"/></xsl:variable>
1556     <m:mrow m:xref="{@id}">
1557      <xsl:choose>
1558      <xsl:when test="$charlength >= $framewidth">
1559       <m:mtable align="baseline 1" equalrows="false" columnalign="left">
1560         <m:mtr>
1561           <m:mtd>
1562            <m:mrow>
1563             <m:mo mathcolor="Red">&#x03bb;</m:mo>
1564             <xsl:apply-templates select="m:bvar"/>
1565            </m:mrow>
1566           </m:mtd>
1567          </m:mtr>
1568        <m:mtr>
1569         <m:mtd>
1570          <m:mrow>
1571           <m:mo>.</m:mo>
1572           <xsl:apply-templates select="*[position()=2]"/>
1573          </m:mrow>
1574         </m:mtd>
1575        </m:mtr>
1576       </m:mtable>
1577      </xsl:when>
1578      <xsl:otherwise>
1579       <m:mo mathcolor="Red">&#x03bb;</m:mo>
1580       <xsl:apply-templates select="m:bvar/m:ci"/>
1581       <m:mo>:</m:mo>
1582       <xsl:apply-templates select="m:bvar/m:type"/>
1583       <m:mo>.</m:mo>
1584       <xsl:apply-templates select="*[position()=2]"/>
1585      </xsl:otherwise>
1586      </xsl:choose>
1587     </m:mrow>
1588 </xsl:template>
1589
1590 <!-- *********************************** -->
1591 <!-- BASE SET OF MATHML CONTENT ELEMENTS -->
1592 <!-- *********************************** -->
1593
1594 <!-- Logic -->
1595
1596 <xsl:template match = "m:apply[m:eq[1]]">
1597  <xsl:variable name="charlength">
1598   <xsl:apply-templates select="*[1]" mode="charcount"/>
1599  </xsl:variable>
1600  <xsl:choose>
1601   <xsl:when test="$charlength >= $framewidth">
1602    <m:mtable align="baseline 1" equalrows="false" columnalign="left">
1603     <xsl:if test="@helm:xref">
1604      <xsl:attribute name="m:xref">
1605       <xsl:value-of select="@id"/>
1606      </xsl:attribute>
1607     </xsl:if>
1608     <m:mtr>
1609      <m:mtd>
1610       <m:mrow>
1611        <m:mo stretchy="false">(</m:mo>
1612        <xsl:apply-templates select="*[position()=2]"/>
1613       </m:mrow>
1614      </m:mtd>
1615     </m:mtr>
1616     <xsl:for-each select = "*[position()>2]">
1617      <m:mtr>
1618       <m:mtd>
1619        <m:mrow>
1620         <m:mphantom><m:mtext>__</m:mtext></m:mphantom>
1621         <m:mo m:xref="{m:in/@id}">=</m:mo>
1622         <xsl:apply-templates select="."/>
1623        </m:mrow>
1624       </m:mtd>
1625      </m:mtr>
1626     </xsl:for-each>
1627     <m:mtr>
1628      <m:mtd>
1629       <m:mrow>
1630        <m:mo stretchy="false">)</m:mo>
1631       </m:mrow>
1632      </m:mtd>
1633     </m:mtr>
1634    </m:mtable>
1635   </xsl:when>
1636   <xsl:otherwise>
1637    <xsl:apply-imports/>
1638   </xsl:otherwise>
1639  </xsl:choose>
1640 </xsl:template>
1641
1642
1643 <xsl:template match = "m:apply[m:and[1]|m:or[1]
1644           |m:geq[1]|m:leq[1]|m:gt[1]|m:lt[1]
1645           |m:in[1]|m:intesect[1]|m:union[1]|m:subset[1]
1646           |m:prsubset|m:setdiff[1]]">
1647  <xsl:variable name="symbol">
1648   <xsl:choose>
1649    <xsl:when test="m:and[1]">
1650     <xsl:value-of select="'wedge'"/>
1651    </xsl:when>
1652    <xsl:when test="m:or[1]">
1653     <xsl:value-of select="'vee'"/>
1654    </xsl:when>
1655    <xsl:when test="m:geq[1]">
1656     <xsl:value-of select="'geq'"/>
1657    </xsl:when>
1658    <xsl:when test="m:leq[1]">
1659     <xsl:value-of select="'leq'"/>
1660    </xsl:when>
1661    <xsl:when test="m:gt[1]">
1662     <xsl:value-of select="'gt'"/>
1663    </xsl:when>
1664    <xsl:when test="m:lt[1]">
1665     <xsl:value-of select="'lt'"/>
1666    </xsl:when>
1667    <xsl:when test="m:eq[1]">
1668     <xsl:value-of select="'Equal'"/>
1669    </xsl:when>
1670    <xsl:when test="m:in[1]">
1671     <xsl:value-of select="'Element'"/>
1672    </xsl:when>
1673    <xsl:when test="m:subset[1]">
1674     <xsl:value-of select="'SubsetEqual'"/>
1675    </xsl:when>
1676    <xsl:when test="m:prsubset[1]">
1677     <xsl:value-of select="'subset'"/>
1678    </xsl:when>
1679    <xsl:when test="m:intersect[1]">
1680     <xsl:value-of select="'Intersection'"/>
1681    </xsl:when>
1682    <xsl:when test="m:union[1]">
1683     <xsl:value-of select="'Union'"/>
1684    </xsl:when>
1685    <xsl:when test="m:setdiff[1]">
1686     <xsl:value-of select="'Backslash'"/>
1687    </xsl:when>
1688   </xsl:choose>
1689  </xsl:variable>
1690  <xsl:variable name="charlength">
1691   <xsl:apply-templates select="*[1]" mode="charcount"/>
1692  </xsl:variable>
1693  <xsl:choose>
1694   <xsl:when test="$charlength >= $framewidth">
1695    <m:mtable align="baseline 1" equalrows="false" columnalign="left">
1696     <xsl:if test="@helm:xref">
1697      <xsl:attribute name="m:xref">
1698       <xsl:value-of select="@id"/>
1699      </xsl:attribute>
1700     </xsl:if>
1701     <m:mtr>
1702      <m:mtd>
1703       <m:mrow>
1704        <m:mo stretchy="false">(</m:mo>
1705        <xsl:apply-templates select="*[position()=2]"/>
1706       </m:mrow>
1707      </m:mtd>
1708     </m:mtr>
1709     <xsl:for-each select = "*[position()>2]">
1710      <m:mtr>
1711       <m:mtd>
1712        <m:mrow>
1713         <m:mphantom><m:mtext>__</m:mtext></m:mphantom>
1714         <m:mo m:xref="{*[1]/@id}">
1715          <m:mchar name="{$symbol}"/>
1716         </m:mo>
1717         <xsl:apply-templates select="."/>
1718        </m:mrow>
1719       </m:mtd>
1720      </m:mtr>
1721     </xsl:for-each>
1722     <m:mtr>
1723      <m:mtd>
1724       <m:mrow>
1725        <m:mo stretchy="false">)</m:mo>
1726       </m:mrow>
1727      </m:mtd>
1728     </m:mtr>
1729    </m:mtable>
1730   </xsl:when>
1731   <xsl:otherwise>
1732    <xsl:apply-imports/>
1733   </xsl:otherwise>
1734  </xsl:choose>
1735 </xsl:template>
1736
1737 <xsl:template match = "m:set">
1738  <xsl:choose>
1739   <xsl:when test="count(child::*) = 0">
1740    <m:mi>
1741     <m:mchar name="emptyset"/>
1742    </m:mi>
1743   </xsl:when>
1744   <xsl:otherwise>
1745    <xsl:variable name="charlength">
1746     <xsl:apply-templates select="*[1]" mode="charcount"/>
1747    </xsl:variable>
1748    <xsl:choose>
1749     <xsl:when test="$charlength >= $framewidth">
1750      <xsl:choose>
1751       <xsl:when test="name(*[1]) = 'm:bvar'">
1752        <m:mtable align="baseline 1" equalrows="false" columnalign="left">
1753         <m:mtr>
1754          <m:mtd>
1755           <m:mrow>
1756            <m:mo stretchy="false">{</m:mo>
1757            <xsl:apply-templates select="*[position()=1]"/>
1758           </m:mrow>
1759          </m:mtd>
1760         </m:mtr>
1761         <m:mtr>
1762          <m:mtd>
1763           <m:mrow>
1764            <m:mphantom><m:mtext>{</m:mtext></m:mphantom>
1765            <m:mo stretchy="false">|</m:mo>
1766            <xsl:apply-templates select="m:condition/*[1]"/>
1767           </m:mrow>
1768          </m:mtd>
1769         </m:mtr>
1770         <m:mtr>
1771          <m:mtd>
1772           <m:mrow>
1773            <m:mo stretchy="false">}</m:mo>
1774           </m:mrow>
1775          </m:mtd>
1776         </m:mtr>
1777        </m:mtable>
1778       </xsl:when>
1779       <xsl:otherwise>
1780        <m:mtable align="baseline 1" equalrows="false" columnalign="left">
1781         <m:mtr>
1782          <m:mtd>
1783           <m:mrow>
1784            <m:mo stretchy="false">{</m:mo>
1785            <xsl:apply-templates select="*[position()=1]"/>
1786            <xsl:if test="position() != last()">
1787             <mo>,</mo>
1788            </xsl:if>
1789           </m:mrow>
1790          </m:mtd>
1791         </m:mtr>
1792         <xsl:for-each select = "*[position()>2]">
1793          <m:mtr>
1794           <m:mtd>
1795            <m:mrow>
1796             <m:mphantom><m:mtext>{</m:mtext></m:mphantom>
1797             <xsl:apply-templates select="."/>
1798             <xsl:if test="position() != last()">
1799              <mo>,</mo>
1800             </xsl:if>
1801            </m:mrow>
1802           </m:mtd>
1803          </m:mtr>
1804         </xsl:for-each>
1805         <m:mtr>
1806          <m:mtd>
1807           <m:mrow>
1808            <m:mo stretchy="false">}</m:mo>
1809           </m:mrow>
1810          </m:mtd>
1811         </m:mtr>
1812        </m:mtable>
1813       </xsl:otherwise>
1814      </xsl:choose>
1815     </xsl:when>
1816     <xsl:otherwise>
1817      <xsl:apply-imports/>
1818     </xsl:otherwise>
1819    </xsl:choose>
1820   </xsl:otherwise>
1821  </xsl:choose>
1822 </xsl:template>
1823
1824 <xsl:template match = "m:apply[m:card[1]]">
1825   <m:mfenced open="|" close="|" stretchy="false">
1826     <xsl:if test="($SEM_SW=$SEM_XREF or $SEM_SW=$SEM_XREF_EXT) and @id">
1827       <xsl:attribute name="m:xref">
1828         <xsl:value-of select="@id"/>
1829       </xsl:attribute>
1830     </xsl:if>
1831   <xsl:apply-templates select="*[2]"/>
1832   </m:mfenced>
1833 </xsl:template>
1834
1835 <!-- *********************************** -->
1836 <!--          PROOF ELEMENTS             -->
1837 <!-- *********************************** -->
1838
1839
1840
1841 <!--**********************-->
1842 <!--       COUNTING       -->
1843 <!--**********************-->
1844
1845 <xsl:template match="m:cn|m:and|m:or|m:not|m:exists|m:eq|m:lt|m:leq|m:gt|m:geq
1846  |m:in|m:notin|m:intersect|m:union|m:subset|m:prsubset|m:card|m:setdiff
1847  |m:plus|m:minus|m:times" mode="charcount">
1848 <xsl:param name="incurrent_length" select="0"/>
1849     <xsl:choose>
1850     <xsl:when test="$framewidth > ($incurrent_length + 3 + string-length())">
1851      <xsl:variable name="siblength">
1852       <xsl:apply-templates select="following-sibling::*[position()=1]" mode="charcount">
1853        <xsl:with-param name="incurrent_length" select="$incurrent_length + string-length()"/>
1854       </xsl:apply-templates>
1855      </xsl:variable>
1856      <xsl:choose>
1857      <xsl:when test="string($siblength) = &quot;&quot;">
1858       <xsl:value-of select="$incurrent_length + 3 + string-length()"/>
1859      </xsl:when>
1860      <xsl:otherwise>
1861       <xsl:value-of select="number($siblength)"/>
1862      </xsl:otherwise>
1863      </xsl:choose>
1864     </xsl:when>
1865     <xsl:otherwise>
1866      <xsl:value-of select="$incurrent_length + 3 + string-length()"/>
1867     </xsl:otherwise>
1868     </xsl:choose>
1869 </xsl:template>
1870
1871 <xsl:template match="m:ci|m:csymbol" mode="charcount">
1872 <xsl:param name="incurrent_length" select="0"/>
1873 <xsl:param name="nosibling" select="0"/>
1874     <xsl:choose>
1875     <xsl:when test="$framewidth > ($incurrent_length + string-length()) and ($nosibling = 0)">
1876      <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>
1877      <xsl:choose>
1878      <xsl:when test="string($siblength) = &quot;&quot;">
1879       <xsl:value-of select="$incurrent_length + string-length()"/>
1880      </xsl:when>
1881      <xsl:otherwise>
1882       <xsl:value-of select="number($siblength)"/>
1883      </xsl:otherwise>
1884      </xsl:choose>
1885     </xsl:when>
1886     <xsl:otherwise>
1887      <xsl:value-of select="$incurrent_length + string-length()"/>
1888     </xsl:otherwise>
1889     </xsl:choose>
1890 </xsl:template>
1891
1892 <xsl:template match="*" mode="charcount">
1893 <xsl:param name="incurrent_length" select="0"/>
1894 <xsl:param name="nosibling" select="0"/>
1895  <xsl:choose>
1896   <xsl:when test="count(child::*) = 0">
1897    <xsl:value-of select="$incurrent_length"/>
1898   </xsl:when>
1899   <xsl:otherwise>
1900     <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>
1901     <xsl:choose>
1902     <xsl:when test="$framewidth > number($childlength) and ($nosibling = 0)">
1903      <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>
1904      <xsl:choose>
1905      <xsl:when test="string($siblength) = &quot;&quot;">
1906       <xsl:value-of select="number($childlength)"/>
1907      </xsl:when>
1908      <xsl:otherwise>
1909       <xsl:value-of select="number($siblength)"/>
1910      </xsl:otherwise>
1911      </xsl:choose>
1912     </xsl:when>
1913     <xsl:otherwise>
1914      <xsl:value-of select="number($childlength)"/>
1915     </xsl:otherwise>
1916     </xsl:choose>
1917   </xsl:otherwise>
1918  </xsl:choose>
1919 </xsl:template>
1920
1921 </xsl:stylesheet>
1922
1923
1924