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