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