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       <xsl:when test="$name='forall'">
 411        <xsl:choose>
 412        <xsl:when test="$charlength >= $framewidth">
 413         <m:mtable align="baseline 1" equalrows="false" columnalign="left">
 414          <m:mtr>
 415           <m:mtd>
 416            <m:mrow>
 417             <m:mo mathcolor="Blue"><m:mchar name="ForAll"/></m:mo>
 418             <xsl:apply-templates select="m:bvar"/>
 419            </m:mrow>
 420           </m:mtd>
 421          </m:mtr>
 422          <m:mtr>
 423           <m:mtd>
 424            <m:mrow>
 425             <m:mo>.</m:mo>
 426             <xsl:apply-templates select="*[position()=3]"/>
 427            </m:mrow>
 428           </m:mtd>
 429          </m:mtr>
 430         </m:mtable>
 431        </xsl:when>
 432        <xsl:otherwise>
 433         <m:mo mathcolor="Blue"><m:mchar name="ForAll"/></m:mo>
 434         <xsl:apply-templates select="m:bvar/m:ci"/>
 435         <m:mo>:</m:mo>
 436         <xsl:apply-templates select="m:bvar/m:type"/>
 437         <m:mo>.</m:mo>
 438         <xsl:apply-templates select="*[position()=3]"/>
 439        </xsl:otherwise>
 440        </xsl:choose>
 441       </xsl:when>
 442       <xsl:when test="$name='let_in'">
 443        <xsl:choose>
 444        <xsl:when test="$charlength >= $framewidth">
 445         <m:mtable align="baseline 1" equalrows="false" columnalign="left">
 446          <m:mtr>
 447           <m:mtd>
 448            <m:mrow>
 449             <m:mo>LET</m:mo>
 450             <m:mphantom><m:mtext>_</m:mtext></m:mphantom>
 451             <xsl:apply-templates select="m:bvar"/>
 452            </m:mrow>
 453           </m:mtd>
 454          </m:mtr>
 455          <m:mtr>
 456           <m:mtd>
 457            <m:mrow>
 458             <m:mo>=</m:mo>
 459             <xsl:apply-templates select="*[position()=3]"/>
 460            </m:mrow>
 461           </m:mtd>
 462          </m:mtr>
 463          <m:mtr>
 464           <m:mtd>
 465            <m:mrow>
 466             <m:mo>IN</m:mo>
 467             <m:mphantom><m:mtext>_</m:mtext></m:mphantom>
 468             <xsl:apply-templates select="*[position()=4]"/>
 469            </m:mrow>
 470           </m:mtd>
 471          </m:mtr>
 472         </m:mtable>
 473        </xsl:when>
 474        <xsl:otherwise>
 475         <m:mo>LET</m:mo>
 476         <m:mphantom><m:mtext>_</m:mtext></m:mphantom>
 477         <xsl:apply-templates select="m:bvar/m:ci"/>
 478         <m:mo>=</m:mo>
 479         <xsl:apply-templates select="*[position()=3]"/>
 480         <m:mphantom><m:mtext>_</m:mtext></m:mphantom>
 481         <m:mtext>IN</m:mtext>
 482         <m:mphantom><m:mtext>_</m:mtext></m:mphantom>
 483         <xsl:apply-templates select="*[position()=4]"/>
 484        </xsl:otherwise>
 485        </xsl:choose>
 486       </xsl:when>
 487       <xsl:when test="$name='prod'">
 488        <xsl:choose>
 489        <xsl:when test="$charlength >= $framewidth">
 490         <m:mtable align="baseline 1" equalrows="false" columnalign="left">
 491          <m:mtr>
 492           <m:mtd>
 493            <m:mrow>
 494             <m:mo mathcolor="Blue">&#x03a0;</m:mo>
 495             <xsl:apply-templates select="m:bvar"/>
 496            </m:mrow>
 497           </m:mtd>
 498          </m:mtr>
 499          <m:mtr>
 500           <m:mtd>
 501            <m:mrow>
 502             <m:mo>.</m:mo>
 503             <xsl:apply-templates select="*[position()=3]"/>
 504            </m:mrow>
 505           </m:mtd>
 506          </m:mtr>
 507         </m:mtable>
 508        </xsl:when>
 509        <xsl:otherwise>
 510         <m:mo mathcolor="Blue">&#x03a0;</m:mo>
 511         <xsl:apply-templates select="m:bvar/m:ci"/>
 512         <m:mo>:</m:mo>
 513         <xsl:apply-templates select="m:bvar/m:type"/>
 514         <m:mo>.</m:mo>
 515         <xsl:apply-templates select="*[position()=3]"/>
 516        </xsl:otherwise>
 517        </xsl:choose>
 518       </xsl:when>
 519       <xsl:when test="$name='arrow'">
 520        <xsl:choose>
 521        <xsl:when test="$charlength >= $framewidth">
 522         <m:mtable align="baseline 1" equalrows="false" columnalign="left">
 523          <m:mtr>
 524           <m:mtd>
 525            <m:mrow>
 526             <xsl:if test="$nopar=0">
 527              <m:mo stretchy="false">(</m:mo>
 528             </xsl:if>
 529             <xsl:apply-templates select="*[position()=2]"/>
 530            </m:mrow>
 531           </m:mtd>
 532          </m:mtr>
 533          <m:mtr>
 534           <m:mtd>
 535            <m:mrow>
 536             <m:mo mathmathcolor="Blue">&#x2192;</m:mo>
 537             <xsl:choose>
 538             <xsl:when test="*[position()=3]/m:csymbol">
 539              <xsl:variable name="nextp"><xsl:value-of select="*[position()=3]/m:csymbol"/></xsl:variable>
 540              <xsl:choose>
 541              <xsl:when test="$nextp='arrow'">
 542               <xsl:apply-templates select="*[position()=3]"><xsl:with-param name="nopar" select="1"/></xsl:apply-templates>
 543              </xsl:when>
 544              <xsl:otherwise>
 545               <xsl:apply-templates select="*[position()=3]"/>
 546              </xsl:otherwise>
 547              </xsl:choose>
 548             </xsl:when>
 549             <xsl:otherwise>
 550              <xsl:apply-templates select="*[position()=3]"/>
 551             </xsl:otherwise>
 552             </xsl:choose>
 553            </m:mrow>
 554           </m:mtd>
 555          </m:mtr>
 556          <xsl:if test="$nopar=0">
 557          <m:mtr>
 558           <m:mtd>
 559            <m:mrow>
 560             <m:mo stretchy="false">)</m:mo>
 561            </m:mrow>
 562           </m:mtd>
 563          </m:mtr>
 564          </xsl:if>
 565         </m:mtable>
 566        </xsl:when>
 567        <xsl:otherwise>
 568         <xsl:if test="$nopar=0">
 569          <m:mo stretchy="false">(</m:mo>
 570         </xsl:if>
 571         <xsl:apply-templates select="*[position()=2]"/>
 572         <m:mo mathcolor="Blue">&#x2192;</m:mo>
 573         <xsl:choose>
 574         <xsl:when test="*[position()=3]/m:csymbol">
 575          <xsl:variable name="nextp"><xsl:value-of select="*[position()=3]/m:csymbol"/></xsl:variable>
 576          <xsl:choose>
 577          <xsl:when test="$nextp='arrow'">
 578           <xsl:apply-templates select="*[position()=3]"><xsl:with-param name="nopar" select="1"/></xsl:apply-templates>
 579          </xsl:when>
 580          <xsl:otherwise>
 581           <xsl:apply-templates select="*[position()=3]"/>
 582          </xsl:otherwise>
 583          </xsl:choose>
 584         </xsl:when>
 585         <xsl:otherwise>
 586          <xsl:apply-templates select="*[position()=3]"/>
 587         </xsl:otherwise>
 588         </xsl:choose>
 589         <xsl:if test="$nopar=0">
 590          <m:mo stretchy="false">)</m:mo>
 591         </xsl:if>
 592        </xsl:otherwise>
 593        </xsl:choose>
 594       </xsl:when>
 595       <xsl:when test="$name='app'">
 596        <xsl:choose>
 597        <xsl:when test="$charlength >= $framewidth">
 598         <m:mtable align="baseline 1" equalrows="false" columnalign="left">
 599          <m:mtr>
 600           <m:mtd>
 601            <m:mrow>
 602             <m:mo stretchy="false">(</m:mo>
 603             <xsl:apply-templates select="*[position()=2]"/>
 604            </m:mrow>
 605           </m:mtd>
 606          </m:mtr>
 607          <xsl:for-each select="*[position()>2]">
 608          <m:mtr>
 609           <m:mtd>
 610            <m:mrow>
 611             <m:mphantom><m:mtext>(</m:mtext></m:mphantom>
 612             <xsl:apply-templates select="."/>
 613            </m:mrow>
 614           </m:mtd>
 615          </m:mtr>
 616          </xsl:for-each>
 617          <m:mtr>
 618           <m:mtd>
 619            <m:mrow>
 620             <m:mo stretchy="false">)</m:mo>
 621            </m:mrow>
 622           </m:mtd>
 623          </m:mtr>
 624         </m:mtable>
 625        </xsl:when>
 626        <xsl:otherwise>
 627         <m:mo stretchy="false">(</m:mo>
 628         <xsl:apply-templates select="*[position()=2]"/>
 629         <xsl:for-each select="*[position()>2]">
 630          <m:mphantom><m:mtext>_</m:mtext></m:mphantom>
 631          <xsl:apply-templates select="."/>
 632         </xsl:for-each>
 633         <m:mo stretchy="false">)</m:mo>
 634        </xsl:otherwise>
 635        </xsl:choose>
 636       </xsl:when>
 637       <xsl:when test="$name='cast'">
 638        <xsl:choose>
 639        <xsl:when test="$charlength >= $framewidth">
 640         <m:mtable align="baseline 1" equalrows="false" columnalign="left">
 641          <m:mtr>
 642           <m:mtd>
 643            <m:mrow>
 644             <m:mo stretchy="false">(</m:mo>
 645             <xsl:apply-templates select="*[position()=2]"/>
 646            </m:mrow>
 647           </m:mtd>
 648          </m:mtr>
 649          <m:mtr>
 650           <m:mtd>
 651            <m:mrow>
 652             <m:mo mathcolor="Maroon">:></m:mo>
 653             <xsl:apply-templates select="*[position()=3]"/>
 654            </m:mrow>
 655           </m:mtd>
 656          </m:mtr>
 657          <m:mtr>
 658           <m:mtd>
 659            <m:mrow>
 660             <m:mo stretchy="false">)</m:mo>
 661            </m:mrow>
 662           </m:mtd>
 663          </m:mtr>
 664         </m:mtable>
 665        </xsl:when>
 666        <xsl:otherwise>
 667         <m:mo stretchy="false">(</m:mo>
 668         <xsl:apply-templates select="*[position()=2]"/>
 669         <m:mo mathcolor="Maroon">:></m:mo>
 670         <xsl:apply-templates select="*[position()=3]"/>
 671         <m:mo stretchy="false">)</m:mo>
 672        </xsl:otherwise>
 673        </xsl:choose>
 674       </xsl:when>
 675       <xsl:when test="$name='Prop'">
 676        <m:mo>Prop</m:mo>
 677       </xsl:when>
 678       <xsl:when test="$name='Set'">
 679        <m:mo>Set</m:mo>
 680       </xsl:when>
 681       <xsl:when test="$name='Type'">
 682        <m:mo>Type</m:mo>
 683       </xsl:when>
 684       <xsl:when test="$name='mutcase'">
 685        <xsl:choose>
 686        <xsl:when test="$charlength >= $framewidth">
 687         <xsl:variable name="charlength"><xsl:apply-templates select="*[position()=2]" mode="charcount"><xsl:with-param name="nosibling" select="1"/></xsl:apply-templates></xsl:variable>
 688         <m:mtable align="baseline 1" equalrows="false" columnalign="left">
 689          <m:mtr>
 690           <m:mtd>
 691            <m:mrow>
 692             <m:mo>&lt;</m:mo>
 693             <xsl:apply-templates select="*[position()=2]"/>
 694             <xsl:if test="$framewidth > $charlength">
 695              <m:mo>&gt;</m:mo>
 696              <m:mo>CASES</m:mo>
 697              <m:mphantom><m:mtext>_</m:mtext></m:mphantom>
 698              <xsl:apply-templates select="*[position()=3]"/>
 699             </xsl:if>
 700            </m:mrow>
 701           </m:mtd>
 702          </m:mtr>
 703          <xsl:if test="$charlength >= $framewidth">
 704          <m:mtr>
 705           <m:mtd>
 706            <m:mrow>
 707             <m:mo>&gt;</m:mo>
 708             <m:mo>CASES</m:mo>
 709             <m:mphantom><m:mtext>_</m:mtext></m:mphantom>
 710             <xsl:apply-templates select="*[position()=3]"/>
 711            </m:mrow>
 712           </m:mtd>
 713          </m:mtr>
 714          </xsl:if>
 715          <m:mtr>
 716           <m:mtd>
 717            <m:mrow>
 718             <m:mo>OF</m:mo>
 719            </m:mrow>
 720           </m:mtd>
 721          </m:mtr>
 722          <xsl:for-each select="*[position() mod 2 = 0 and position()>3]">
 723          <xsl:variable name="charlength"><xsl:apply-templates select="." mode="charcount"><xsl:with-param name="nosibling" select="1"/></xsl:apply-templates></xsl:variable>
 724          <m:mtr>
 725           <m:mtd>
 726            <m:mrow>
 727             <xsl:choose>
 728             <xsl:when test="position() = 1">
 729               <m:mphantom><m:mtext>|</m:mtext></m:mphantom>
 730             </xsl:when>
 731             <xsl:otherwise>
 732              <m:mo stretchy="false">|</m:mo>
 733             </xsl:otherwise>
 734             </xsl:choose>
 735             <m:mphantom><m:mtext>_</m:mtext></m:mphantom>
 736             <xsl:apply-templates select="."/>
 737             <xsl:if test="$framewidth > $charlength">
 738              <m:mo mathcolor="Green">&#x21d2;</m:mo>
 739              <xsl:apply-templates select="following-sibling::*[position()= 1]"/>
 740             </xsl:if>
 741            </m:mrow>
 742           </m:mtd>
 743          </m:mtr>
 744          <xsl:if test="$charlength >= $framewidth">
 745          <m:mtr>
 746           <m:mtd>
 747            <m:mrow>
 748             <m:mphantom><m:mtext>|_</m:mtext></m:mphantom>
 749             <m:mo mathcolor="Green">&#x21d2;</m:mo>
 750             <xsl:apply-templates select="following-sibling::*[position()= 1]"/>
 751            </m:mrow>
 752           </m:mtd>
 753          </m:mtr>
 754          </xsl:if>
 755         </xsl:for-each>
 756          <m:mtr>
 757           <m:mtd>
 758            <m:mrow>
 759             <m:mo>END</m:mo>
 760            </m:mrow>
 761           </m:mtd>
 762          </m:mtr>
 763         </m:mtable>
 764        </xsl:when>
 765        <xsl:otherwise>
 766         <m:mo>&lt;</m:mo><xsl:apply-templates select="*[position()=2]"/><m:mo>&gt;</m:mo>
 767         <m:mo>CASES</m:mo>
 768         <m:mphantom><m:mtext>_</m:mtext></m:mphantom>
 769         <xsl:apply-templates select="*[position()=3]"/>
 770         <m:mphantom><m:mtext>_</m:mtext></m:mphantom>
 771         <m:mo>OF</m:mo>
 772         <xsl:for-each select="*[position() mod 2 = 0 and position()>3]">
 773          <xsl:choose>
 774          <xsl:when test="position() != 1">
 775           <m:mo stretchy="false">|</m:mo>
 776          </xsl:when>
 777          </xsl:choose>
 778          <xsl:apply-templates select="."/>
 779          <m:mo mathcolor="Green">&#x21d2;</m:mo>
 780          <xsl:apply-templates select="following-sibling::*[position()= 1]"/>
 781         </xsl:for-each>
 782         <m:mphantom><m:mtext>_</m:mtext></m:mphantom>
 783         <m:mo>END</m:mo>
 784        </xsl:otherwise>
 785        </xsl:choose>
 786       </xsl:when>
 787       <xsl:when test="$name='fix'">
 788        <xsl:choose>
 789        <xsl:when test="$charlength >= $framewidth">
 790         <m:mtable align="baseline 1" equalrows="false" columnalign="left">
 791          <m:mtr>
 792           <m:mtd>
 793            <m:mrow>
 794             <m:mo>FIX</m:mo>
 795             <m:mphantom><m:mtext>_</m:mtext></m:mphantom>
 796             <m:mi><xsl:value-of select="m:ci"/></m:mi>
 797             <m:mo stretchy="false">{</m:mo>
 798            </m:mrow>
 799           </m:mtd>
 800          </m:mtr>
 801          <m:mtr>
 802           <m:mtd>
 803            <m:mrow>
 804             <m:mphantom><m:mtext>__</m:mtext></m:mphantom>
 805             <m:mtable align="baseline 1" equalrows="false" columnalign="left">
 806             <xsl:for-each select="m:bvar">
 807              <xsl:variable name="charlength"><xsl:apply-templates select="m:type" mode="charcount"><xsl:with-param name="nosibling" select="1"/></xsl:apply-templates></xsl:variable>
 808              <m:mtr>
 809               <m:mtd>
 810                <m:mrow>
 811                 <m:mi><xsl:value-of select="m:ci"/></m:mi>
 812                 <m:mo>:</m:mo>
 813                 <xsl:if test="$framewidth > $charlength">
 814                  <xsl:apply-templates select="m:type"/>
 815                 </xsl:if>
 816                </m:mrow>
 817               </m:mtd>
 818              </m:mtr>
 819              <xsl:if test="$charlength >= $framewidth">
 820              <m:mtr>
 821               <m:mtd>
 822                <m:mrow>
 823                 <m:mphantom><m:mtext>:=</m:mtext></m:mphantom>
 824                 <xsl:apply-templates select="m:type"/>
 825                </m:mrow>
 826               </m:mtd>
 827              </m:mtr>
 828              </xsl:if>
 829              <m:mtr>
 830               <m:mtd>
 831                <m:mrow>
 832                 <m:mo>:=</m:mo>
 833                 <xsl:apply-templates select="following-sibling::*[position()=1]"/>
 834                </m:mrow>
 835               </m:mtd>
 836              </m:mtr>
 837             </xsl:for-each>
 838             </m:mtable>
 839            </m:mrow>
 840           </m:mtd>
 841          </m:mtr>
 842          <m:mtr>
 843           <m:mtd>
 844            <m:mrow>
 845             <m:mo stretchy="false">}</m:mo>
 846            </m:mrow>
 847           </m:mtd>
 848          </m:mtr>
 849         </m:mtable>
 850        </xsl:when>
 851        <xsl:otherwise>
 852         <m:mo>FIX</m:mo>
 853         <m:mi><xsl:value-of select="m:ci"/></m:mi>
 854         <m:mo stretchy="false">{</m:mo>
 855         <m:mtable align="baseline 1" equalrows="false" columnalign="left">
 856         <xsl:for-each select="m:bvar">
 857          <m:mtr>
 858           <m:mtd>
 859            <m:mrow>
 860             <m:mi><xsl:value-of select="m:ci"/></m:mi>
 861             <m:mo>:</m:mo>
 862             <xsl:apply-templates select="m:type"/>
 863             <m:mo>:=</m:mo>
 864             <xsl:apply-templates select="following-sibling::*[position() = 1]"/>
 865             <xsl:if test="position()=last()">
 866              <m:mo stretchy="false">}</m:mo>
 867             </xsl:if>
 868            </m:mrow>
 869           </m:mtd>
 870          </m:mtr>
 871          </xsl:for-each>
 872         </m:mtable>
 873        </xsl:otherwise>
 874        </xsl:choose>
 875       </xsl:when>
 876       <xsl:when test="$name='cofix'">
 877        <xsl:choose>
 878        <xsl:when test="$charlength >= $framewidth">
 879         <m:mtable align="baseline 1" equalrows="false" columnalign="left">
 880          <m:mtr>
 881           <m:mtd>
 882            <m:mrow>
 883             <m:mo>COFIX</m:mo>
 884             <m:mphantom><m:mtext>_</m:mtext></m:mphantom>
 885             <m:mi><xsl:value-of select="m:ci"/></m:mi>
 886             <m:mo stretchy="false">{</m:mo>
 887            </m:mrow>
 888           </m:mtd>
 889          </m:mtr>
 890          <m:mtr>
 891           <m:mtd>
 892            <m:mrow>
 893             <m:mphantom><m:mtext>__</m:mtext></m:mphantom>
 894             <m:mtable align="baseline 1" equalrows="false" columnalign="left">
 895             <xsl:for-each select="m:bvar">
 896              <xsl:variable name="charlength"><xsl:apply-templates select="m:type" mode="charcount"><xsl:with-param name="nosibling" select="1"/></xsl:apply-templates></xsl:variable>
 897              <m:mtr>
 898               <m:mtd>
 899                <m:mrow>
 900                 <m:mi><xsl:value-of select="m:ci"/></m:mi>
 901                 <m:mo>:</m:mo>
 902                 <xsl:if test="$framewidth > $charlength">
 903                  <xsl:apply-templates select="m:type"/>
 904                 </xsl:if>
 905                </m:mrow>
 906               </m:mtd>
 907              </m:mtr>
 908              <xsl:if test="$charlength >= $framewidth">
 909              <m:mtr>
 910               <m:mtd>
 911                <m:mrow>
 912                 <m:mphantom><m:mtext>:=</m:mtext></m:mphantom>
 913                 <xsl:apply-templates select="m:type"/>
 914                </m:mrow>
 915               </m:mtd>
 916              </m:mtr>
 917              </xsl:if>
 918              <m:mtr>
 919               <m:mtd>
 920                <m:mrow>
 921                 <m:mo>:=</m:mo>
 922                 <xsl:apply-templates select="following-sibling::*[position() = 1]"/>
 923                </m:mrow>
 924               </m:mtd>
 925              </m:mtr>
 926             </xsl:for-each>
 927             </m:mtable>
 928            </m:mrow>
 929           </m:mtd>
 930          </m:mtr>
 931          <m:mtr>
 932           <m:mtd>
 933            <m:mrow>
 934             <m:mo stretchy="false">}</m:mo>
 935            </m:mrow>
 936           </m:mtd>
 937          </m:mtr>
 938         </m:mtable>
 939        </xsl:when>
 940        <xsl:otherwise>
 941         <m:mo>COFIX</m:mo>
 942         <m:mi><xsl:value-of select="m:ci"/></m:mi>
 943         <m:mo stretchy="false">{</m:mo>
 944         <m:mtable align="baseline 1" equalrows="false" columnalign="left">
 945         <xsl:for-each select="m:bvar">
 946          <m:mtr>
 947           <m:mtd>
 948            <m:mrow>
 949             <m:mi><xsl:value-of select="m:ci"/></m:mi>
 950             <m:mo>:</m:mo>
 951             <xsl:apply-templates select="m:type"/>
 952             <m:mo>:=</m:mo>
 953             <xsl:apply-templates select="following-sibling::*[position() = 1]"/>
 954             <xsl:if test="position()=last()">
 955              <m:mo stretchy="false">}</m:mo>
 956             </xsl:if>
 957            </m:mrow>
 958           </m:mtd>
 959          </m:mtr>
 960          </xsl:for-each>
 961         </m:mtable>
 962        </xsl:otherwise>
 963        </xsl:choose>
 964       </xsl:when>
 965       <!-- ***************************************** -->
 966       <!-- *********** PROOF ELEMENTS ************** -->
 967       <!-- ***************************************** -->
 968       <xsl:when test="$name='proof'">
 969         <m:mtable align="baseline 1" equalrows="false" columnalign="left">
 970          <m:mtr>
 971           <m:mtd>
 972            <m:mrow>
 973             <xsl:apply-templates select="*[position()=2]"/>
 974            </m:mrow>
 975           </m:mtd>
 976          </m:mtr>
 977          <m:mtr>
 978           <m:mtd>
 979            <m:mrow>
 980             <m:mtext mathcolor="Maroon">we proved </m:mtext>
 981             <m:mphantom><m:mtext>_</m:mtext></m:mphantom>
 982             <xsl:apply-templates select="*[position()=3]"/>
 983            </m:mrow>
 984           </m:mtd>
 985          </m:mtr>
 986         </m:mtable>
 987       </xsl:when>
 988       <xsl:when test="$name='letin1'">
 989         <m:mtable align="baseline 1" equalrows="false" columnalign="left">
 990          <m:mtr>
 991           <m:mtd>
 992            <m:mrow>
 993             <xsl:apply-templates select="*[2]"/>
 994            </m:mrow>
 995           </m:mtd>
 996          </m:mtr>
 997          <m:mtr>
 998           <m:mtd>
 999            <m:mrow>
1000             <xsl:apply-templates select="*[3]"/>
1001            </m:mrow>
1002           </m:mtd>
1003          </m:mtr>
1004         </m:mtable>
1005       </xsl:when>
1006       <xsl:when test="$name='letin'">
1007         <m:mtable align="baseline 1" equalrows="false" columnalign="left">
1008          <!-- <xsl:for-each select="APPLY[m:csymbol and (string(m:csymbol)='let')]"> -->
1009          <xsl:for-each select="*[(last() > position()) and (position()>1)]">
1010          <m:mtr>
1011           <m:mtd>
1012            <m:mrow>
1013             <xsl:apply-templates select="."/>
1014            </m:mrow>
1015           </m:mtd>
1016          </m:mtr>
1017          </xsl:for-each>
1018          <m:mtr>
1019           <m:mtd>
1020            <m:mrow>
1021             <xsl:apply-templates select="*[position()=last()]"/>
1022            </m:mrow>
1023           </m:mtd>
1024          </m:mtr>
1025         </m:mtable>
1026       </xsl:when>
1027       <xsl:when test="$name='let'">
1028        <m:mtext>(</m:mtext>
1029        <xsl:apply-templates select="m:ci"/>
1030        <m:mtext>) </m:mtext>
1031        <xsl:apply-templates select="*[3]"/>
1032       </xsl:when>
1033       <xsl:when test="$name='rw_step'">
1034         <m:mtable align="baseline 1" equalrows="false" columnalign="left">
1035          <m:mtr>
1036           <m:mtd>
1037            <m:mrow>
1038             <xsl:choose>
1039              <xsl:when test="name(*[2])='m:apply'">
1040               <xsl:apply-templates select="*[2]"/>
1041              </xsl:when>
1042              <xsl:otherwise>
1043               <m:mtext>Consider</m:mtext>
1044               <m:mphantom><m:mtext>_</m:mtext></m:mphantom>
1045               <xsl:apply-templates select="*[2]"/>
1046              </xsl:otherwise>
1047             </xsl:choose>
1048            </m:mrow>
1049           </m:mtd>
1050          </m:mtr>
1051          <m:mtr>
1052           <m:mtd>
1053            <m:mrow>
1054             <m:mtext>Rewrite</m:mtext>
1055             <m:mphantom><m:mtext>_</m:mtext></m:mphantom>
1056             <xsl:apply-templates select="*[3]"/>
1057             <m:mphantom><m:mtext>_</m:mtext></m:mphantom>
1058             <m:mtext>with</m:mtext>
1059             <m:mphantom><m:mtext>_</m:mtext></m:mphantom>
1060             <xsl:apply-templates select="*[4]"/>
1061             <m:mphantom><m:mtext>_</m:mtext></m:mphantom>
1062             <m:mtext>by</m:mtext>
1063             <m:mphantom><m:mtext>_</m:mtext></m:mphantom>
1064             <xsl:apply-templates select="*[5]"/>
1065            </m:mrow>
1066           </m:mtd>
1067          </m:mtr>
1068         </m:mtable>
1069       </xsl:when>
1070       <!-- not existing any more
1071       <xsl:when test="$name='thread'">
1072         <m:mtable align="baseline 1" equalrows="false" columnalign="left">
1073          <m:mtr>
1074           <m:mtd>
1075            <m:mrow>
1076             <xsl:choose>
1077              <xsl:when test="name(*[last()])='m:apply'">
1078               <xsl:apply-templates select="*[last()]"/>
1079              </xsl:when>
1080              <xsl:otherwise>
1081               <m:mtext>Consider</m:mtext>
1082               <m:mphantom><m:mtext>_</m:mtext></m:mphantom>
1083               <xsl:apply-templates select="*[last()]"/>
1084              </xsl:otherwise>
1085             </xsl:choose>
1086            </m:mrow>
1087           </m:mtd>
1088          </m:mtr>
1089          <xsl:apply-templates mode="thread" select="*[(last()-2)]"/>
1090         </m:mtable>
1091       </xsl:when>
1092       -->
1093       <xsl:when test="$name='rewrite_and_apply'">
1094         <m:mtable align="baseline 1" equalrows="false" columnalign="left">
1095          <m:mtr>
1096           <m:mtd>
1097            <m:mrow>
1098             <xsl:apply-templates select="*[2]"/>
1099            </m:mrow>
1100           </m:mtd>
1101          </m:mtr>
1102          <m:mtr>
1103           <m:mtd>
1104            <m:mrow>
1105             <m:mtext>Then apply it to</m:mtext>
1106             <m:mphantom><m:mtext>_</m:mtext></m:mphantom>
1107             <xsl:apply-templates select="*[position()>2]"/>
1108            </m:mrow>
1109           </m:mtd>
1110          </m:mtr>
1111        </m:mtable>
1112       </xsl:when>
1113       <!-- NAT_IND -->
1114       <xsl:when test="$name='nat_ind'">
1115         <m:mtable align="baseline 1" equalrows="false" columnalign="left">
1116          <m:mtr>
1117           <m:mtd>
1118            <m:mtext>By induction</m:mtext>
1119           </m:mtd>
1120          </m:mtr>
1121          <m:mtr>
1122           <m:mtd>
1123            <m:mrow>
1124             <m:mtext>base case:</m:mtext>
1125             <xsl:apply-templates select="*[2]"/>
1126            </m:mrow>
1127           </m:mtd>
1128          </m:mtr>
1129          <m:mtr>
1130           <m:mtd>
1131            <m:mrow>
1132             <m:mtext>inductive case:</m:mtext>
1133             <xsl:apply-templates select="*[3]"/>
1134            </m:mrow>
1135           </m:mtd>
1136          </m:mtr>
1137         </m:mtable>
1138       </xsl:when>
1139       <!-- AND_IND -->
1140       <xsl:when test="$name='and_ind'">
1141         <m:mtable align="baseline 1" equalrows="false" columnalign="left">
1142          <m:mtr>
1143           <m:mtd>
1144            <m:mrow>
1145             <xsl:choose>
1146              <xsl:when test="name(*[2])='m:apply'">
1147               <xsl:apply-templates select="*[2]"/>
1148              </xsl:when>
1149              <xsl:otherwise>
1150               <m:mtext>Consider</m:mtext>
1151               <m:mphantom><m:mtext>_</m:mtext></m:mphantom>
1152               <xsl:apply-templates select="*[2]"/>
1153              </xsl:otherwise>
1154             </xsl:choose>
1155            </m:mrow>
1156           </m:mtd>
1157          </m:mtr>
1158          <m:mtr>
1159           <m:mtd>
1160            <m:mrow>
1161             <m:mtext>In particular, we have</m:mtext>
1162            </m:mrow>
1163           </m:mtd>
1164          </m:mtr>
1165          <m:mtr>
1166           <m:mtd>
1167            <m:mrow>
1168             <m:mtext>(</m:mtext>
1169             <xsl:apply-templates select="*[3]"/>
1170             <m:mtext>)</m:mtext>
1171             <m:mphantom><m:mtext>_</m:mtext></m:mphantom>
1172             <xsl:apply-templates select="*[4]"/>
1173             </m:mrow>
1174           </m:mtd>
1175          </m:mtr>
1176          <m:mtr>
1177           <m:mtd>
1178            <m:mrow>
1179             <m:mtext>(</m:mtext>
1180             <xsl:apply-templates select="*[5]"/>
1181             <m:mtext>)</m:mtext>
1182             <m:mphantom><m:mtext>_</m:mtext></m:mphantom>
1183             <xsl:apply-templates select="*[6]"/>
1184             </m:mrow>
1185           </m:mtd>
1186          </m:mtr>
1187          <m:mtr>
1188           <m:mtd>
1189            <m:mrow>
1190             <xsl:apply-templates select="*[7]"/>
1191            </m:mrow>
1192           </m:mtd>
1193          </m:mtr>
1194         </m:mtable>
1195       </xsl:when>
1196       <xsl:when test="$name='or_ind'">
1197         <m:mtable align="baseline 1" equalrows="false" columnalign="left">
1198          <m:mtr>
1199           <m:mtd>
1200            <m:mrow>
1201             <xsl:choose>
1202              <xsl:when test="name(*[2])='m:apply'">
1203               <xsl:apply-templates select="*[2]"/>
1204              </xsl:when>
1205              <xsl:otherwise>
1206               <m:mtext>Consider</m:mtext>
1207               <m:mphantom><m:mtext>_</m:mtext></m:mphantom>
1208               <xsl:apply-templates select="*[2]"/>
1209              </xsl:otherwise>
1210             </xsl:choose>
1211            </m:mrow>
1212           </m:mtd>
1213          </m:mtr>
1214          <m:mtr>
1215           <m:mtd>
1216            <m:mrow>
1217             <m:mtext>We prove</m:mtext>
1218             <m:mphantom><m:mtext>_</m:mtext></m:mphantom>
1219             <xsl:apply-templates select="*[3]"/>
1220             <m:mphantom><m:mtext>_</m:mtext></m:mphantom>
1221             <m:mtext>by cases:</m:mtext>
1222            </m:mrow>
1223           </m:mtd>
1224          </m:mtr>
1225          <m:mtr>
1226           <m:mtd>
1227            <m:mrow>
1228             <m:mtext>*</m:mtext>
1229             <xsl:apply-templates select="*[4]"/>
1230            </m:mrow>
1231           </m:mtd>
1232          </m:mtr>
1233          <m:mtr>
1234           <m:mtd>
1235            <m:mrow>
1236             <m:mtext>*</m:mtext>
1237             <xsl:apply-templates select="*[5]"/>
1238            </m:mrow>
1239           </m:mtd>
1240          </m:mtr>
1241         </m:mtable>
1242       </xsl:when>
1243       <xsl:when test="$name='ex_ind'">
1244         <m:mtable align="baseline 1" equalrows="false" columnalign="left">
1245          <m:mtr>
1246           <m:mtd>
1247            <m:mrow>
1248             <xsl:choose>
1249              <xsl:when test="name(*[2])='m:apply'">
1250               <xsl:apply-templates select="*[2]"/>
1251              </xsl:when>
1252              <xsl:otherwise>
1253               <m:mtext>Consider</m:mtext>
1254               <m:mphantom><m:mtext>_</m:mtext></m:mphantom>
1255               <xsl:apply-templates select="*[2]"/>
1256              </xsl:otherwise>
1257             </xsl:choose>
1258            </m:mrow>
1259           </m:mtd>
1260          </m:mtr>
1261          <m:mtr>
1262           <m:mtd>
1263            <m:mrow>
1264             <m:mtext>Let</m:mtext>
1265             <m:mphantom><m:mtext>_</m:mtext></m:mphantom>
1266             <xsl:apply-templates select="*[3]"/>
1267             <m:mtext>:</m:mtext>
1268             <xsl:apply-templates select="*[4]"/>
1269             <m:mphantom><m:mtext>_</m:mtext></m:mphantom>
1270             <m:mtext>such that</m:mtext>
1271             <m:mphantom><m:mtext>_</m:mtext></m:mphantom>
1272             <m:mtext>(</m:mtext>
1273              <xsl:apply-templates select="*[5]"/>
1274             <m:mtext>)</m:mtext>
1275             <m:mphantom><m:mtext>_</m:mtext></m:mphantom>
1276             <xsl:apply-templates select="*[6]"/>
1277            </m:mrow>
1278           </m:mtd>
1279          </m:mtr>
1280          <m:mtr>
1281           <m:mtd>
1282            <m:mrow>
1283             <xsl:apply-templates select="*[7]"/>
1284            </m:mrow>
1285           </m:mtd>
1286          </m:mtr>
1287         </m:mtable>
1288       </xsl:when>
1289       <xsl:otherwise>
1290        <m:ci>ERROR</m:ci>
1291       </xsl:otherwise>
1292      </xsl:choose>
1293     </m:mrow>
1294 </xsl:template>
1295
1296 <!-- Il modo Thread non esiste piu'
1297 <xsl:template match="*" mode="thread">
1298  <xsl:variable name="name"><xsl:value-of select="following-sibling::*[position()=1]/m:csymbol"/></xsl:variable>
1299  <xsl:choose>
1300   <xsl:when test="$name='rw_step'">
1301          <m:mtr>
1302           <m:mtd>
1303            <m:mrow>
1304             <m:mtext>Rewrite</m:mtext>
1305             <m:mphantom><m:mtext>_</m:mtext></m:mphantom>
1306             <xsl:apply-templates select="following-sibling::*[position()=1]/*[2]"/>
1307             <m:mphantom><m:mtext>_</m:mtext></m:mphantom>
1308             <m:mtext>with</m:mtext>
1309             <m:mphantom><m:mtext>_</m:mtext></m:mphantom>
1310             <xsl:apply-templates select="following-sibling::*[position()=1]/*[3]"/>
1311             <m:mphantom><m:mtext>_</m:mtext></m:mphantom>
1312             <m:mtext>by</m:mtext>
1313             <m:mphantom><m:mtext>_</m:mtext></m:mphantom>
1314             <xsl:apply-templates select="following-sibling::*[position()=1]/*[4]"/>
1315            </m:mrow>
1316           </m:mtd>
1317          </m:mtr>
1318          <m:mtr>
1319           <m:mtd>
1320            <m:mrow>
1321             <m:mtext mathcolor="Maroon">we get</m:mtext>
1322             <m:mphantom><m:mtext>_</m:mtext></m:mphantom>
1323             <xsl:apply-templates select="."/>
1324            </m:mrow>
1325           </m:mtd>
1326          </m:mtr>
1327    </xsl:when>
1328    <xsl:otherwise>
1329          <m:mtr>
1330           <m:mtd>
1331            <m:mrow>
1332             <xsl:apply-templates select="following-sibling::*[position()=1]"/>
1333            </m:mrow>
1334           </m:mtd>
1335          </m:mtr>
1336          <m:mtr>
1337           <m:mtd>
1338            <m:mrow>
1339             <m:mtext mathcolor="Maroon">we get</m:mtext>
1340             <m:mphantom><m:mtext>_</m:mtext></m:mphantom>
1341             <xsl:apply-templates select="."/>
1342            </m:mrow>
1343           </m:mtd>
1344          </m:mtr>
1345     </xsl:otherwise>
1346    </xsl:choose>
1347          <xsl:apply-templates mode="thread" select="preceding-sibling::*[position()=2]"/>
1348 </xsl:template>
1349 -->
1350
1351 <!-- LAMBDA -->
1352
1353 <xsl:template match="m:lambda">
1354     <xsl:variable name="charlength"><xsl:apply-templates select="*[position()=1]" mode="charcount"/></xsl:variable>
1355     <m:mrow m:xref="{@id}">
1356      <xsl:choose>
1357      <xsl:when test="$charlength >= $framewidth">
1358       <m:mtable align="baseline 1" equalrows="false" columnalign="left">
1359         <m:mtr>
1360           <m:mtd>
1361            <m:mrow>
1362             <m:mo mathcolor="Red">&#x03bb;</m:mo>
1363             <xsl:apply-templates select="m:bvar"/>
1364            </m:mrow>
1365           </m:mtd>
1366          </m:mtr>
1367        <m:mtr>
1368         <m:mtd>
1369          <m:mrow>
1370           <m:mo>.</m:mo>
1371           <xsl:apply-templates select="*[position()=2]"/>
1372          </m:mrow>
1373         </m:mtd>
1374        </m:mtr>
1375       </m:mtable>
1376      </xsl:when>
1377      <xsl:otherwise>
1378       <m:mo mathcolor="Red">&#x03bb;</m:mo>
1379       <xsl:apply-templates select="m:bvar/m:ci"/>
1380       <m:mo>:</m:mo>
1381       <xsl:apply-templates select="m:bvar/m:type"/>
1382       <m:mo>.</m:mo>
1383       <xsl:apply-templates select="*[position()=2]"/>
1384      </xsl:otherwise>
1385      </xsl:choose>
1386     </m:mrow>
1387 </xsl:template>
1388
1389 <!-- *********************************** -->
1390 <!-- BASE SET OF MATHML CONTENT ELEMENTS -->
1391 <!-- *********************************** -->
1392
1393 <!-- Logic -->
1394
1395 <xsl:template match = "m:apply[m:eq[1]]">
1396  <xsl:variable name="charlength">
1397   <xsl:apply-templates select="*[1]" mode="charcount"/>
1398  </xsl:variable>
1399  <xsl:choose>
1400   <xsl:when test="$charlength >= $framewidth">
1401    <m:mtable align="baseline 1" equalrows="false" columnalign="left">
1402     <xsl:if test="@helm:xref">
1403      <xsl:attribute name="m:xref">
1404       <xsl:value-of select="@id"/>
1405      </xsl:attribute>
1406     </xsl:if>
1407     <m:mtr>
1408      <m:mtd>
1409       <m:mrow>
1410        <m:mo stretchy="false">(</m:mo>
1411        <xsl:apply-templates select="*[position()=2]"/>
1412       </m:mrow>
1413      </m:mtd>
1414     </m:mtr>
1415     <xsl:for-each select = "*[position()>2]">
1416      <m:mtr>
1417       <m:mtd>
1418        <m:mrow>
1419         <m:mphantom><m:mtext>__</m:mtext></m:mphantom>
1420         <m:mo m:xref="{m:in/@id}">=</m:mo>
1421         <xsl:apply-templates select="."/>
1422        </m:mrow>
1423       </m:mtd>
1424      </m:mtr>
1425     </xsl:for-each>
1426     <m:mtr>
1427      <m:mtd>
1428       <m:mrow>
1429        <m:mo stretchy="false">)</m:mo>
1430       </m:mrow>
1431      </m:mtd>
1432     </m:mtr>
1433    </m:mtable>
1434   </xsl:when>
1435   <xsl:otherwise>
1436    <xsl:apply-imports/>
1437   </xsl:otherwise>
1438  </xsl:choose>
1439 </xsl:template>
1440
1441
1442 <xsl:template match = "m:apply[m:and[1]|m:or[1]
1443           |m:geq[1]|m:leq[1]|m:gt[1]|m:lt[1]
1444           |m:in[1]|m:intesect[1]|m:union[1]|m:subset[1]
1445           |m:prsubset|m:setdiff[1]]">
1446  <xsl:variable name="symbol">
1447   <xsl:choose>
1448    <xsl:when test="m:and[1]">
1449     <xsl:value-of select="'wedge'"/>
1450    </xsl:when>
1451    <xsl:when test="m:or[1]">
1452     <xsl:value-of select="'vee'"/>
1453    </xsl:when>
1454    <xsl:when test="m:geq[1]">
1455     <xsl:value-of select="'geq'"/>
1456    </xsl:when>
1457    <xsl:when test="m:leq[1]">
1458     <xsl:value-of select="'leq'"/>
1459    </xsl:when>
1460    <xsl:when test="m:gt[1]">
1461     <xsl:value-of select="'gt'"/>
1462    </xsl:when>
1463    <xsl:when test="m:lt[1]">
1464     <xsl:value-of select="'lt'"/>
1465    </xsl:when>
1466    <xsl:when test="m:eq[1]">
1467     <xsl:value-of select="'Equal'"/>
1468    </xsl:when>
1469    <xsl:when test="m:in[1]">
1470     <xsl:value-of select="'Element'"/>
1471    </xsl:when>
1472    <xsl:when test="m:subset[1]">
1473     <xsl:value-of select="'SubsetEqual'"/>
1474    </xsl:when>
1475    <xsl:when test="m:prsubset[1]">
1476     <xsl:value-of select="'subset'"/>
1477    </xsl:when>
1478    <xsl:when test="m:intersect[1]">
1479     <xsl:value-of select="'Intersection'"/>
1480    </xsl:when>
1481    <xsl:when test="m:union[1]">
1482     <xsl:value-of select="'Union'"/>
1483    </xsl:when>
1484    <xsl:when test="m:setdiff[1]">
1485     <xsl:value-of select="'Backslash'"/>
1486    </xsl:when>
1487   </xsl:choose>
1488  </xsl:variable>
1489  <xsl:variable name="charlength">
1490   <xsl:apply-templates select="*[1]" mode="charcount"/>
1491  </xsl:variable>
1492  <xsl:choose>
1493   <xsl:when test="$charlength >= $framewidth">
1494    <m:mtable align="baseline 1" equalrows="false" columnalign="left">
1495     <xsl:if test="@helm:xref">
1496      <xsl:attribute name="m:xref">
1497       <xsl:value-of select="@id"/>
1498      </xsl:attribute>
1499     </xsl:if>
1500     <m:mtr>
1501      <m:mtd>
1502       <m:mrow>
1503        <m:mo stretchy="false">(</m:mo>
1504        <xsl:apply-templates select="*[position()=2]"/>
1505       </m:mrow>
1506      </m:mtd>
1507     </m:mtr>
1508     <xsl:for-each select = "*[position()>2]">
1509      <m:mtr>
1510       <m:mtd>
1511        <m:mrow>
1512         <m:mphantom><m:mtext>__</m:mtext></m:mphantom>
1513         <m:mo m:xref="{*[1]/@id}">
1514          <m:mchar name="{$symbol}"/>
1515         </m:mo>
1516         <xsl:apply-templates select="."/>
1517        </m:mrow>
1518       </m:mtd>
1519      </m:mtr>
1520     </xsl:for-each>
1521     <m:mtr>
1522      <m:mtd>
1523       <m:mrow>
1524        <m:mo stretchy="false">)</m:mo>
1525       </m:mrow>
1526      </m:mtd>
1527     </m:mtr>
1528    </m:mtable>
1529   </xsl:when>
1530   <xsl:otherwise>
1531    <xsl:apply-imports/>
1532   </xsl:otherwise>
1533  </xsl:choose>
1534 </xsl:template>
1535
1536 <xsl:template match = "m:set">
1537  <xsl:choose>
1538   <xsl:when test="count(child::*) = 0">
1539    <m:mi>
1540     <m:mchar name="emptyset"/>
1541    </m:mi>
1542   </xsl:when>
1543   <xsl:otherwise>
1544    <xsl:variable name="charlength">
1545     <xsl:apply-templates select="*[1]" mode="charcount"/>
1546    </xsl:variable>
1547    <xsl:choose>
1548     <xsl:when test="$charlength >= $framewidth">
1549      <xsl:choose>
1550       <xsl:when test="name(*[1]) = 'm:bvar'">
1551        <m:mtable align="baseline 1" equalrows="false" columnalign="left">
1552         <m:mtr>
1553          <m:mtd>
1554           <m:mrow>
1555            <m:mo stretchy="false">{</m:mo>
1556            <xsl:apply-templates select="*[position()=1]"/>
1557           </m:mrow>
1558          </m:mtd>
1559         </m:mtr>
1560         <m:mtr>
1561          <m:mtd>
1562           <m:mrow>
1563            <m:mphantom><m:mtext>{</m:mtext></m:mphantom>
1564            <m:mo stretchy="false">|</m:mo>
1565            <xsl:apply-templates select="m:condition/*[1]"/>
1566           </m:mrow>
1567          </m:mtd>
1568         </m:mtr>
1569         <m:mtr>
1570          <m:mtd>
1571           <m:mrow>
1572            <m:mo stretchy="false">}</m:mo>
1573           </m:mrow>
1574          </m:mtd>
1575         </m:mtr>
1576        </m:mtable>
1577       </xsl:when>
1578       <xsl:otherwise>
1579        <m:mtable align="baseline 1" equalrows="false" columnalign="left">
1580         <m:mtr>
1581          <m:mtd>
1582           <m:mrow>
1583            <m:mo stretchy="false">{</m:mo>
1584            <xsl:apply-templates select="*[position()=1]"/>
1585            <xsl:if test="position() != last()">
1586             <mo>,</mo>
1587            </xsl:if>
1588           </m:mrow>
1589          </m:mtd>
1590         </m:mtr>
1591         <xsl:for-each select = "*[position()>2]">
1592          <m:mtr>
1593           <m:mtd>
1594            <m:mrow>
1595             <m:mphantom><m:mtext>{</m:mtext></m:mphantom>
1596             <xsl:apply-templates select="."/>
1597             <xsl:if test="position() != last()">
1598              <mo>,</mo>
1599             </xsl:if>
1600            </m:mrow>
1601           </m:mtd>
1602          </m:mtr>
1603         </xsl:for-each>
1604         <m:mtr>
1605          <m:mtd>
1606           <m:mrow>
1607            <m:mo stretchy="false">}</m:mo>
1608           </m:mrow>
1609          </m:mtd>
1610         </m:mtr>
1611        </m:mtable>
1612       </xsl:otherwise>
1613      </xsl:choose>
1614     </xsl:when>
1615     <xsl:otherwise>
1616      <xsl:apply-imports/>
1617     </xsl:otherwise>
1618    </xsl:choose>
1619   </xsl:otherwise>
1620  </xsl:choose>
1621 </xsl:template>
1622
1623 <xsl:template match = "m:apply[m:card[1]]">
1624   <m:mfenced open="|" close="|" stretchy="false">
1625     <xsl:if test="($SEM_SW=$SEM_XREF or $SEM_SW=$SEM_XREF_EXT) and @id">
1626       <xsl:attribute name="m:xref">
1627         <xsl:value-of select="@id"/>
1628       </xsl:attribute>
1629     </xsl:if>
1630   <xsl:apply-templates select="*[2]"/>
1631   </m:mfenced>
1632 </xsl:template>
1633
1634 <!-- *********************************** -->
1635 <!--          PROOF ELEMENTS             -->
1636 <!-- *********************************** -->
1637
1638
1639
1640 <!--**********************-->
1641 <!--       COUNTING       -->
1642 <!--**********************-->
1643
1644 <xsl:template match="m:cn|m:and|m:or|m:not|m:exists|m:eq|m:lt|m:leq|m:gt|m:geq
1645  |m:in|m:notin|m:intersect|m:union|m:subset|m:prsubset|m:card|m:setdiff
1646  |m:plus|m:minus|m:times" mode="charcount">
1647 <xsl:param name="incurrent_length" select="0"/>
1648     <xsl:choose>
1649     <xsl:when test="$framewidth > ($incurrent_length + 3 + string-length())">
1650      <xsl:variable name="siblength">
1651       <xsl:apply-templates select="following-sibling::*[position()=1]" mode="charcount">
1652        <xsl:with-param name="incurrent_length" select="$incurrent_length + string-length()"/>
1653       </xsl:apply-templates>
1654      </xsl:variable>
1655      <xsl:choose>
1656      <xsl:when test="string($siblength) = &quot;&quot;">
1657       <xsl:value-of select="$incurrent_length + 3 + string-length()"/>
1658      </xsl:when>
1659      <xsl:otherwise>
1660       <xsl:value-of select="number($siblength)"/>
1661      </xsl:otherwise>
1662      </xsl:choose>
1663     </xsl:when>
1664     <xsl:otherwise>
1665      <xsl:value-of select="$incurrent_length + 3 + string-length()"/>
1666     </xsl:otherwise>
1667     </xsl:choose>
1668 </xsl:template>
1669
1670 <xsl:template match="m:ci|m:csymbol" mode="charcount">
1671 <xsl:param name="incurrent_length" select="0"/>
1672 <xsl:param name="nosibling" select="0"/>
1673     <xsl:choose>
1674     <xsl:when test="$framewidth > ($incurrent_length + string-length()) and ($nosibling = 0)">
1675      <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>
1676      <xsl:choose>
1677      <xsl:when test="string($siblength) = &quot;&quot;">
1678       <xsl:value-of select="$incurrent_length + string-length()"/>
1679      </xsl:when>
1680      <xsl:otherwise>
1681       <xsl:value-of select="number($siblength)"/>
1682      </xsl:otherwise>
1683      </xsl:choose>
1684     </xsl:when>
1685     <xsl:otherwise>
1686      <xsl:value-of select="$incurrent_length + string-length()"/>
1687     </xsl:otherwise>
1688     </xsl:choose>
1689 </xsl:template>
1690
1691 <xsl:template match="*" mode="charcount">
1692 <xsl:param name="incurrent_length" select="0"/>
1693 <xsl:param name="nosibling" select="0"/>
1694  <xsl:choose>
1695   <xsl:when test="count(child::*) = 0">
1696    <xsl:value-of select="$incurrent_length"/>
1697   </xsl:when>
1698   <xsl:otherwise>
1699     <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>
1700     <xsl:choose>
1701     <xsl:when test="$framewidth > number($childlength) and ($nosibling = 0)">
1702      <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>
1703      <xsl:choose>
1704      <xsl:when test="string($siblength) = &quot;&quot;">
1705       <xsl:value-of select="number($childlength)"/>
1706      </xsl:when>
1707      <xsl:otherwise>
1708       <xsl:value-of select="number($siblength)"/>
1709      </xsl:otherwise>
1710      </xsl:choose>
1711     </xsl:when>
1712     <xsl:otherwise>
1713      <xsl:value-of select="number($childlength)"/>
1714     </xsl:otherwise>
1715     </xsl:choose>
1716   </xsl:otherwise>
1717  </xsl:choose>
1718 </xsl:template>
1719
1720 </xsl:stylesheet>
1721
1722
1723