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       <!-- ***************************************** -->
 737       <!-- *********** PROOF ELEMENTS ************** -->
 738       <!-- ***************************************** -->
 739       <!-- PROOF -->
 740       <xsl:when test="$name='proof'">
 741        <xsl:apply-templates select="*[position()=2]">
 742         <xsl:with-param name="current_indent" select="$current_indent"/>
 743        </xsl:apply-templates>
 744        <br/>
 745        <!-- <xsl:element name="br"/> -->
 746        <xsl:call-template name="make_indent">
 747         <xsl:with-param name="current_indent" select="$current_indent"/>
 748        </xsl:call-template>
 749        <FONT color="red">we proved&#x00a0;</FONT>
 750        <xsl:apply-templates select="*[position()=3]">
 751         <xsl:with-param name="current_indent" select="$current_indent + 16"/>
 752        </xsl:apply-templates>
 753       </xsl:when>
 754       <!-- letin1 -->
 755       <xsl:when test="$name='letin1'">
 756        <xsl:apply-templates select="*[position()=2]">
 757         <xsl:with-param name="current_indent" select="$current_indent"/>
 758        </xsl:apply-templates>
 759        <br/>
 760        <xsl:call-template name="make_indent">
 761         <xsl:with-param name="current_indent" select="$current_indent"/>
 762        </xsl:call-template>
 763        <xsl:apply-templates select="*[position()=3]">
 764         <xsl:with-param name="current_indent" select="$current_indent"/>
 765        </xsl:apply-templates>
 766       </xsl:when>
 767       <!-- letin -->
 768       <xsl:when test="$name='letin'">
 769        <xsl:for-each select="*[position()>1 and last()>position()]">
 770         <xsl:apply-templates select=".">
 771          <xsl:with-param name="current_indent" select="$current_indent"/>
 772         </xsl:apply-templates>
 773         <br/>
 774         <xsl:call-template name="make_indent">
 775          <xsl:with-param name="current_indent" select="$current_indent"/>
 776         </xsl:call-template>
 777        </xsl:for-each>
 778        <xsl:apply-templates select="*[position()=last()]">
 779         <xsl:with-param name="current_indent" select="$current_indent"/>
 780        </xsl:apply-templates>
 781       </xsl:when>
 782       <!-- Let -->
 783       <xsl:when test="$name='let'">
 784        (
 785        <xsl:apply-templates select="m:ci"/>
 786        )
 787        <xsl:apply-templates select="*[3]">
 788         <xsl:with-param name="current_indent" select="$current_indent + 7"/>
 789        </xsl:apply-templates>
 790       </xsl:when>
 791       <!-- rw_step -->
 792       <xsl:when test="$name='rw_step'">
 793        <xsl:choose>
 794         <xsl:when test="name(*[2])='m:apply'">
 795          <xsl:apply-templates select="*[2]">
 796           <xsl:with-param name="current_indent" select="$current_indent"/>
 797          </xsl:apply-templates>
 798         </xsl:when>
 799         <xsl:otherwise>
 800          <FONT color="red">Consider&#x00a0;</FONT>
 801          <xsl:apply-templates select="*[2]"/>
 802         </xsl:otherwise>
 803        </xsl:choose>
 804        <xsl:variable name="charlength_first">
 805         <xsl:apply-templates select="*[3]/*[1]" mode="charcount"/>
 806        </xsl:variable>
 807        <xsl:variable name="charlength_second">
 808         <xsl:apply-templates select="*[4]/*[1]" mode="charcount"/>
 809        </xsl:variable>
 810        <xsl:variable name="charlength_side_proof">
 811         <xsl:apply-templates select="*[5]/*[1]" mode="charcount"/>
 812        </xsl:variable>
 813        <xsl:variable name="split1"
 814           select="$charlength_first + $charlength_second > $framewidth"/>
 815        <xsl:variable name="split2"
 816           select="$charlength_second + $charlength_side_proof > $framewidth"/>
 817      <!-- <xsl:value-of select="$current_indent"/> -->
 818      <!-- <xsl:value-of select="$charlength"/> -->
 819        <br/>
 820        <xsl:call-template name="make_indent">
 821         <xsl:with-param name="current_indent" select="$current_indent"/>
 822        </xsl:call-template>
 823        <FONT color="red">Rewrite&#x00a0;</FONT>
 824        <xsl:apply-templates mode="inline" select="*[3]"/>
 825        <xsl:text>&#x00a0;</xsl:text>
 826        <xsl:if test="$split1">
 827        <br/>
 828        <xsl:call-template name="make_indent">
 829         <xsl:with-param name="current_indent" select="$current_indent + 2"/>
 830        </xsl:call-template>
 831        </xsl:if>
 832        <FONT color="red">with&#x00a0;</FONT>
 833        <xsl:apply-templates mode="inline" select="*[4]"/>
 834        <xsl:text>&#x00a0;</xsl:text>
 835        <xsl:if test="$split2">
 836        <br/>
 837        <xsl:call-template name="make_indent">
 838         <xsl:with-param name="current_indent" select="$current_indent + 2"/>
 839        </xsl:call-template>
 840        </xsl:if>
 841        <FONT color="red">by&#x00a0;</FONT>
 842        <xsl:apply-templates select="*[5]">
 843         <xsl:with-param name="current_indent" select="$current_indent+7"/>
 844        </xsl:apply-templates>
 845       </xsl:when>
 846       <!-- rewrite and apply -->
 847       <xsl:when test="$name='rewrite_and_apply'">
 848        <xsl:apply-templates select="*[2]">
 849         <xsl:with-param name="current_indent" select="$current_indent"/>
 850        </xsl:apply-templates>
 851        <br/>
 852        <xsl:call-template name="make_indent">
 853         <xsl:with-param name="current_indent" select="$current_indent"/>
 854        </xsl:call-template>
 855        <FONT color="red">Then apply it to&#x00a0;</FONT>
 856        <xsl:apply-templates select="*[position()>2]"/>
 857       </xsl:when>
 858       <!-- by_induction -->
 859       <xsl:when test="$name='by_induction'">
 860        <FONT color="red">We prove&#x00a0;</FONT>
 861        <xsl:apply-templates select="../*[3]">
 862         <xsl:with-param name="current_indent" select="$current_indent+18"/>
 863        </xsl:apply-templates>
 864        <br/>
 865        <xsl:call-template name="make_indent">
 866         <xsl:with-param name="current_indent" select="$current_indent"/>
 867        </xsl:call-template>
 868        <FONT color="red">by induction on&#x00a0;</FONT>
 869        <xsl:apply-templates select="*[position()=last()]/*[position()=last()]">
 870         <xsl:with-param name="current_indent" select="$current_indent+30"/>
 871        </xsl:apply-templates>
 872        <!--
 873        <br/>
 874        <xsl:call-template name="make_indent">
 875         <xsl:with-param name="current_indent" select="$current_indent"/>
 876        </xsl:call-template>
 877        <xsl:text>The induction property is</xsl:text>
 878        <br/>
 879        <xsl:call-template name="make_indent">
 880         <xsl:with-param name="current_indent" select="$current_indent"/>
 881        </xsl:call-template>
 882        <xsl:apply-templates select="*[3]">
 883         <xsl:with-param name="current_indent" select="$current_indent"/>
 884        </xsl:apply-templates>
 885        -->
 886        <xsl:apply-templates
 887             select="*[position()>3 and not(position()=last())]">
 888         <xsl:with-param name="current_indent" select="$current_indent+4"/>
 889        </xsl:apply-templates>
 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>End induction</xsl:text> -->
 895       </xsl:when>
 896       <!-- inductive_case -->
 897       <xsl:when test="$name='inductive_case'">
 898        <br/>
 899        <xsl:call-template name="make_indent">
 900         <xsl:with-param name="current_indent" select="$current_indent"/>
 901        </xsl:call-template>
 902        <FONT color="red">Case&#x00a0;</FONT>
 903        <xsl:apply-templates select="*[2]">
 904         <xsl:with-param name="current_indent" select="$current_indent +10"/>
 905        </xsl:apply-templates>
 906        <xsl:if test="*[3]/*[position()>1]">
 907         <br/>
 908         <xsl:call-template name="make_indent">
 909          <xsl:with-param name="current_indent" select="$current_indent+4"/>
 910         </xsl:call-template>
 911         <FONT color="red">By induction hypothesis, we have:</FONT>
 912         <xsl:for-each select="*[3]/*[position()>1]">
 913          <br/>
 914          <xsl:call-template name="make_indent">
 915           <xsl:with-param name="current_indent" select="$current_indent + 4"/>
 916          </xsl:call-template>
 917          <xsl:text>(</xsl:text>
 918          <xsl:apply-templates select="m:ci"/>
 919          <xsl:text>)&#x00a0;</xsl:text>
 920          <xsl:apply-templates select="m:type">
 921           <xsl:with-param name="current_indent" select="$current_indent + 8"/>
 922          </xsl:apply-templates>
 923         </xsl:for-each>
 924        </xsl:if>
 925        <br/>
 926         <xsl:call-template name="make_indent">
 927          <xsl:with-param name="current_indent" select="$current_indent + 4"/>
 928         </xsl:call-template>
 929        <xsl:apply-templates select="*[4]">
 930         <xsl:with-param name="current_indent" select="$current_indent +4"/>
 931        </xsl:apply-templates>
 932        <!-- <br/>
 933        <xsl:call-template name="make_indent">
 934         <xsl:with-param name="current_indent" select="$current_indent"/>
 935        </xsl:call-template>
 936        <xsl:text>End Case</xsl:text> -->
 937       </xsl:when>
 938       <!-- case_lhs  -->
 939       <xsl:when test="$name='case_lhs'">
 940        <xsl:choose>
 941         <xsl:when test="count(*)=2">
 942          <xsl:apply-templates mode="inline" select="*[2]"/>
 943         </xsl:when>
 944         <xsl:otherwise>
 945          <xsl:text>(</xsl:text>
 946          <xsl:apply-templates mode="inline" select="*[2]"/>
 947          <xsl:for-each select="m:bvar">
 948           <xsl:text>&#x00a0;</xsl:text>
 949           <xsl:apply-templates mode="inline" select="*[1]"/>
 950           <xsl:text>:</xsl:text>
 951           <xsl:apply-templates mode="inline" select="m:type/*[1]"/>
 952          </xsl:for-each>
 953          <xsl:text>)</xsl:text>
 954         </xsl:otherwise>
 955        </xsl:choose>
 956       </xsl:when>
 957       <!-- nat_ind -->
 958       <xsl:when test="$name='nat_ind_complete'">
 959        <FONT color="red">By induction on&#x00a0;</FONT>
 960        <xsl:apply-templates select="*[2]"/>:
 961        <br/>
 962        <xsl:call-template name="make_indent">
 963         <xsl:with-param name="current_indent" select="$current_indent"/>
 964        </xsl:call-template>
 965        <xsl:text>0&#x00a0;</xsl:text>
 966        <FONT FACE="Symbol" mathcolor="green">&#222;</FONT>
 967        <xsl:apply-templates select="*[3]">
 968         <xsl:with-param name="current_indent" select="$current_indent + 8"/>
 969        </xsl:apply-templates>
 970        <br/>
 971        <xsl:call-template name="make_indent">
 972         <xsl:with-param name="current_indent" select="$current_indent"/>
 973        </xsl:call-template>
 974        <xsl:text>S(</xsl:text>
 975        <xsl:apply-templates select="*[4]"/>
 976        <xsl:text>)&#x00a0;</xsl:text>
 977        <FONT FACE="Symbol" mathcolor="green">&#222;</FONT>
 978        <FONT color="red">Assume by induction</FONT>
 979        <br/>
 980        <xsl:call-template name="make_indent">
 981         <xsl:with-param name="current_indent" select="$current_indent +10"/>
 982        </xsl:call-template>
 983        <xsl:text>(</xsl:text>
 984        <xsl:apply-templates select="*[5]"/>
 985        <xsl:text>)</xsl:text>
 986        <xsl:apply-templates select="*[6]">
 987         <xsl:with-param name="current_indent" select="$current_indent + 14"/>
 988        </xsl:apply-templates>
 989        <br/>
 990        <xsl:call-template name="make_indent">
 991         <xsl:with-param name="current_indent" select="$current_indent +10"/>
 992        </xsl:call-template>
 993        <xsl:apply-templates select="*[7]">
 994         <xsl:with-param name="current_indent" select="$current_indent + 10"/>
 995        </xsl:apply-templates>
 996       </xsl:when>
 997       <!-- false_ind -->
 998       <xsl:when test="$name='false_ind'">
 999        <xsl:apply-templates select="*[3]">
1000         <xsl:with-param name="current_indent" select="$current_indent"/>
1001        </xsl:apply-templates>
1002        <br/>
1003        <xsl:call-template name="make_indent">
1004         <xsl:with-param name="current_indent" select="$current_indent"/>
1005        </xsl:call-template>
1006        <FONT color="red">Contradiction.</FONT>
1007       </xsl:when>
1008       <!-- and_ind -->
1009       <xsl:when test="$name='and_ind'">
1010        <xsl:choose>
1011         <xsl:when test="name(*[2])='m:apply'">
1012          <xsl:apply-templates select="*[2]">
1013           <xsl:with-param name="current_indent" select="$current_indent"/>
1014          </xsl:apply-templates>
1015         </xsl:when>
1016         <xsl:otherwise>
1017          <FONT color="red">Consider&#x00a0;</FONT>
1018          <xsl:apply-templates select="*[2]"/>
1019         </xsl:otherwise>
1020        </xsl:choose>
1021        <br/>
1022        <xsl:call-template name="make_indent">
1023         <xsl:with-param name="current_indent" select="$current_indent"/>
1024        </xsl:call-template>
1025        <FONT color="red">In particular, we have</FONT>
1026        <br/>
1027        <xsl:call-template name="make_indent">
1028         <xsl:with-param name="current_indent" select="$current_indent"/>
1029        </xsl:call-template>
1030        (
1031        <xsl:apply-templates select="*[3]"/>
1032        )&#x00a0;
1033        <xsl:apply-templates select="*[4]">
1034         <xsl:with-param name="current_indent" select="$current_indent + 9"/>
1035        </xsl:apply-templates>
1036        <br/>
1037        <xsl:call-template name="make_indent">
1038         <xsl:with-param name="current_indent" select="$current_indent"/>
1039        </xsl:call-template>
1040        (
1041        <xsl:apply-templates select="*[5]"/>
1042        )&#x00a0;
1043        <xsl:apply-templates select="*[6]">
1044         <xsl:with-param name="current_indent" select="$current_indent + 9"/>
1045        </xsl:apply-templates>
1046        <br/>
1047        <xsl:call-template name="make_indent">
1048         <xsl:with-param name="current_indent" select="$current_indent"/>
1049        </xsl:call-template>
1050        <xsl:apply-templates select="*[7]">
1051         <xsl:with-param name="current_indent" select="$current_indent"/>
1052        </xsl:apply-templates>
1053       </xsl:when>
1054       <!-- full_or_ind -->
1055       <xsl:when test="$name='full_or_ind'">
1056        <xsl:choose>
1057         <xsl:when test="name(*[2])='m:apply'">
1058          <xsl:apply-templates select="*[2]">
1059           <xsl:with-param name="current_indent" select="$current_indent"/>
1060          </xsl:apply-templates>
1061         </xsl:when>
1062         <xsl:otherwise>
1063          <FONT color="red">Consider&#x00a0;</FONT>
1064          <xsl:apply-templates select="*[2]"/>
1065         </xsl:otherwise>
1066        </xsl:choose>
1067        <br/>
1068        <xsl:call-template name="make_indent">
1069         <xsl:with-param name="current_indent" select="$current_indent"/>
1070        </xsl:call-template>
1071        <FONT color="red">We proceed by cases to prove&#x00a0;</FONT>
1072        <xsl:apply-templates select="*[3]"/>
1073        <br/>
1074        <xsl:call-template name="make_indent">
1075         <xsl:with-param name="current_indent" select="$current_indent+4"/>
1076        </xsl:call-template>
1077        <FONT color="red">Left: suppose&#x00a0;</FONT>
1078        <xsl:text>(</xsl:text>
1079        <xsl:value-of select="*[4]/m:bvar/m:ci"/>
1080        <xsl:text>)&#x00a0;</xsl:text>
1081        <xsl:apply-templates
1082             select="*[4]/m:bvar/m:type/*[1]"/>
1083        <br/>
1084        <xsl:call-template name="make_indent">
1085         <xsl:with-param name="current_indent" select="$current_indent+15"/>
1086        </xsl:call-template>
1087        <xsl:apply-templates
1088             select="*[4]/*[3]">
1089         <xsl:with-param name="current_indent" select="$current_indent+15"/>
1090        </xsl:apply-templates>
1091        <br/>
1092        <xsl:call-template name="make_indent">
1093         <xsl:with-param name="current_indent" select="$current_indent+4"/>
1094        </xsl:call-template>
1095        <FONT color="red">Right: suppose&#x00a0;</FONT>
1096        <xsl:text>(</xsl:text>
1097        <xsl:value-of select="*[5]/m:bvar/m:ci"/>
1098        <xsl:text>)&#x00a0;</xsl:text>
1099        <xsl:apply-templates
1100             select="*[5]/m:bvar/m:type/*[1]"/>
1101        <br/>
1102        <xsl:call-template name="make_indent">
1103         <xsl:with-param name="current_indent" select="$current_indent+16"/>
1104        </xsl:call-template>
1105        <xsl:apply-templates
1106             select="*[5]/*[3]">
1107         <xsl:with-param name="current_indent" select="$current_indent+16"/>
1108        </xsl:apply-templates>
1109       </xsl:when>
1110       <!-- or_ind -->
1111       <xsl:when test="$name='or_ind'">
1112        <xsl:choose>
1113         <xsl:when test="name(*[2])='m:apply'">
1114          <xsl:apply-templates select="*[2]">
1115           <xsl:with-param name="current_indent" select="$current_indent"/>
1116          </xsl:apply-templates>
1117         </xsl:when>
1118         <xsl:otherwise>
1119          <FONT color="red">Consider&#x00a0;</FONT>
1120          <xsl:apply-templates select="*[2]"/>
1121         </xsl:otherwise>
1122        </xsl:choose>
1123        <br/>
1124        <xsl:call-template name="make_indent">
1125         <xsl:with-param name="current_indent" select="$current_indent"/>
1126        </xsl:call-template>
1127        <FONT color="red">We prove&#x00a0;</FONT>
1128        <xsl:apply-templates select="*[3]"/>
1129        <FONT color="red">&#x00a0;by cases:</FONT>
1130        <br/>
1131        <xsl:call-template name="make_indent">
1132         <xsl:with-param name="current_indent" select="$current_indent"/>
1133        </xsl:call-template>
1134        *
1135        <xsl:apply-templates select="*[4]">
1136         <xsl:with-param name="current_indent" select="$current_indent"/>
1137        </xsl:apply-templates>
1138        <br/>
1139        <xsl:call-template name="make_indent">
1140         <xsl:with-param name="current_indent" select="$current_indent"/>
1141        </xsl:call-template>
1142        *
1143        <xsl:apply-templates select="*[5]">
1144         <xsl:with-param name="current_indent" select="$current_indent"/>
1145        </xsl:apply-templates>
1146       </xsl:when>
1147       <!-- Ex_ind -->
1148       <xsl:when test="$name='ex_ind'">
1149        <xsl:choose>
1150         <xsl:when test="name(*[2])='m:apply'">
1151          <xsl:apply-templates select="*[2]">
1152           <xsl:with-param name="current_indent" select="$current_indent"/>
1153          </xsl:apply-templates>
1154         </xsl:when>
1155         <xsl:otherwise>
1156          <FONT color="red">Consider&#x00a0;</FONT>
1157          <xsl:apply-templates select="*[2]">
1158           <xsl:with-param name="current_indent" select="$current_indent"/>
1159          </xsl:apply-templates>
1160         </xsl:otherwise>
1161        </xsl:choose>
1162        <br/>
1163        <xsl:call-template name="make_indent">
1164         <xsl:with-param name="current_indent" select="$current_indent"/>
1165        </xsl:call-template>
1166        <FONT color="red">Let&#x00a0;</FONT>
1167        <xsl:apply-templates mode="inline" select="*[3]"/>
1168        :
1169        <xsl:apply-templates mode="inline" select="*[4]"/>
1170        <FONT color="red">&#x00a0;such that</FONT>
1171        <br/>
1172        <xsl:call-template name="make_indent">
1173         <xsl:with-param name="current_indent" select="$current_indent"/>
1174        </xsl:call-template>
1175        (
1176        <xsl:apply-templates mode="inline" select="*[5]"/>
1177        )
1178        <xsl:apply-templates select="*[6]">
1179         <xsl:with-param name="current_indent" select="$current_indent +7"/>
1180        </xsl:apply-templates>
1181        <br/>
1182        <xsl:call-template name="make_indent">
1183         <xsl:with-param name="current_indent" select="$current_indent"/>
1184        </xsl:call-template>
1185        <xsl:apply-templates select="*[7]">
1186         <xsl:with-param name="current_indent" select="$current_indent"/>
1187        </xsl:apply-templates>
1188       </xsl:when>
1189       <!-- ***************************************** -->
1190       <!-- *********** LAMBDA ELEMENTS ************** -->
1191       <!-- ***************************************** -->
1192       <xsl:when test="$name='subst'">
1193        <xsl:apply-templates select="*[2]"/>
1194        <xsl:text>[</xsl:text>
1195        <xsl:apply-templates select="*[4]"/>
1196        <a href="{*[1]/@definitionURL}">
1197        <FONT color="blue" SIZE="+0" FACE="symbol">
1198         <xsl:text>&#x00ac;</xsl:text>
1199        </FONT>
1200        </a>
1201        <xsl:apply-templates select="*[3]"/>
1202        <xsl:text>]</xsl:text>
1203       </xsl:when>
1204
1205       <xsl:when test="$name='lift_with_base'">
1206        <SUB>
1207        <xsl:apply-templates select="*[3]" mode="inline"/>
1208        </SUB>
1209        <a href="{*[1]/@definitionURL}">
1210        <FONT color="green" FACE="symbol">
1211         <xsl:text>&#x00ad;</xsl:text>
1212        </FONT>
1213        </a>
1214        <SUP>
1215        <xsl:apply-templates select="*[4]" mode="inline"/>
1216        </SUP>
1217        <xsl:text>(</xsl:text>
1218        <xsl:apply-templates select="*[2]" mode="inline"/>
1219        <xsl:text>)</xsl:text>
1220       </xsl:when>
1221
1222       <xsl:when test="$name='lift'">
1223        <a href="{*[1]/@definitionURL}">
1224        <FONT color="green" FACE="symbol">
1225         <xsl:text>&#x00ad;</xsl:text>
1226        </FONT>
1227        </a>
1228        <SUP>
1229        <xsl:apply-templates select="*[2]" mode="inline"/>
1230        </SUP>
1231        <xsl:text>(</xsl:text>
1232        <xsl:apply-templates select="*[3]" mode="inline"/>
1233        <xsl:text>)</xsl:text>
1234       </xsl:when>
1235
1236       <!-- reduction -->
1237       <xsl:when test="$name='beta_red1'">
1238        <xsl:apply-templates select="*[2]" mode="inline"/>
1239        <a href="{*[1]/@definitionURL}">
1240        <FONT color="green" FACE="symbol">
1241         <xsl:text>&#x00ae;</xsl:text>
1242        </FONT>
1243        <SUB>
1244         <FONT color="green" FACE="symbol">
1245          <xsl:text>&#x0062;</xsl:text>
1246         </FONT>
1247        </SUB>
1248        </a>
1249        <xsl:apply-templates select="*[3]" mode="inline"/>
1250       </xsl:when>
1251
1252       <xsl:when test="$name='beta_red'">
1253        <xsl:apply-templates select="*[2]" mode="inline"/>
1254        <a href="{*[1]/@definitionURL}">
1255        <FONT color="green" FACE="symbol">
1256         <xsl:text>&#x00ae;</xsl:text>
1257        </FONT>
1258        <SUB>
1259         <FONT color="green" FACE="symbol">
1260          <xsl:text>&#x0062;*</xsl:text>
1261         </FONT>
1262        </SUB>
1263        </a>
1264        <xsl:apply-templates select="*[3]" mode="inline"/>
1265       </xsl:when>
1266
1267       <xsl:when test="$name='par_beta_red1'">
1268        <xsl:apply-templates select="*[2]" mode="inline"/>
1269        <a href="{*[1]/@definitionURL}">
1270        <FONT color="green" FACE="symbol">
1271         <xsl:text>&#x00de;</xsl:text>
1272        </FONT>
1273        <SUB>
1274         <FONT color="green" FACE="symbol">
1275          <xsl:text>&#x0062;</xsl:text>
1276         </FONT>
1277        </SUB>
1278        </a>
1279        <xsl:apply-templates select="*[3]" mode="inline"/>
1280       </xsl:when>
1281
1282       <xsl:when test="$name='par_beta_red'">
1283        <xsl:apply-templates select="*[2]" mode="inline"/>
1284        <a href="{*[1]/@definitionURL}">
1285        <FONT color="green" FACE="symbol">
1286         <xsl:text>&#x00de;</xsl:text>
1287        </FONT>
1288        <SUB>
1289         <FONT color="green" FACE="symbol">
1290          <xsl:text>&#x0062;*</xsl:text>
1291         </FONT>
1292        </SUB>
1293        </a>
1294        <xsl:apply-templates select="*[3]" mode="inline"/>
1295       </xsl:when>
1296
1297       <!-- forgetful -->
1298       <xsl:when test="$name='forgetful'">
1299        <a href="{*[1]/@definitionURL}">|</a>
1300        <xsl:apply-templates select="*[2]" mode="inline"/>
1301        <a href="{*[1]/@definitionURL}">|</a>
1302       </xsl:when>
1303
1304       <!-- boolean algebra of redexes -->
1305
1306       <!-- isomorphic -->
1307       <xsl:when test="$name='isomorphic'">
1308        <xsl:apply-templates select="*[2]" mode="inline"/>
1309        <a href="{*[1]/@definitionURL}">
1310         <FONT color="green" FACE="symbol">
1311         <xsl:text>&#x0040;</xsl:text>
1312        </FONT>
1313        </a>
1314        <xsl:apply-templates select="*[3]" mode="inline"/>
1315       </xsl:when>
1316
1317       <!-- INTERP -->
1318       <xsl:when test="$name='interp'">
1319          <font color="green">[</font>
1320             <xsl:apply-templates select="*[2]"/>
1321          <font color="green">]</font>
1322       </xsl:when>
1323
1324      </xsl:choose>
1325 </xsl:template>
1326
1327 <!-- LAMBDA -->
1328
1329 <xsl:template match="m:lambda">
1330 <xsl:param name="current_indent" select="0"/>
1331     <xsl:variable name="charlength">
1332      <xsl:apply-templates select="*[position()=1]" mode="charcount"/>
1333      <!-- <xsl:apply-templates select="." mode="charcount"/> -->
1334     </xsl:variable>
1335     <!-- <xsl:value-of select="$charlength"/> -->
1336     <!-- <xsl:value-of select="$current_indent"/> -->
1337      <xsl:choose>
1338      <xsl:when test="$charlength > $framewidth">
1339        <!-- &#x03bb; -->
1340        <FONT SIZE="+2" color="red" FACE="symbol">l</FONT>
1341        <xsl:apply-templates select="m:bvar/m:ci"/>
1342        <xsl:text>:</xsl:text>
1343        <xsl:apply-templates select="m:bvar/m:type">
1344         <xsl:with-param name="current_indent"
1345            select="$current_indent + 4 + 2*string-length(m:bvar/m:ci)"/>
1346        </xsl:apply-templates><br/>
1347        <xsl:call-template name="make_indent">
1348         <xsl:with-param name="current_indent" select="$current_indent + 2"/>
1349        </xsl:call-template>
1350        <xsl:text>.</xsl:text>
1351        <xsl:apply-templates select="*[position()=2]">
1352         <xsl:with-param name="current_indent" select="$current_indent + 2"/>
1353        </xsl:apply-templates>
1354      </xsl:when>
1355      <xsl:otherwise>
1356       <xsl:apply-templates mode="inline" select="."/>
1357      </xsl:otherwise>
1358      </xsl:choose>
1359 </xsl:template>
1360
1361 <!-- href -->
1362 <xsl:template match="m:ci">
1363  <xsl:choose>
1364   <xsl:when test="boolean(@definitionURL)">
1365    <a href="{@definitionURL}">
1366    <xsl:apply-templates/>
1367    </a>
1368   </xsl:when>
1369   <xsl:otherwise>
1370    <xsl:value-of select="."/>
1371   </xsl:otherwise>
1372  </xsl:choose>
1373 </xsl:template>
1374
1375 <!-- COUNTING -->
1376
1377 <xsl:template match="m:ci|m:csymbol" mode="charcount">
1378 <xsl:param name="incurrent_length" select="0"/>
1379     <xsl:choose>
1380     <xsl:when test="$framewidth >= ($incurrent_length + string-length())">
1381      <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>
1382      <xsl:choose>
1383      <xsl:when test="string($siblength) = &quot;&quot;">
1384       <xsl:value-of select="$incurrent_length + string-length()"/>
1385      </xsl:when>
1386      <xsl:otherwise>
1387       <xsl:value-of select="number($siblength)"/>
1388      </xsl:otherwise>
1389      </xsl:choose>
1390     </xsl:when>
1391     <xsl:otherwise>
1392      <xsl:value-of select="$incurrent_length + string-length()"/>
1393     </xsl:otherwise>
1394     </xsl:choose>
1395 </xsl:template>
1396
1397 <xsl:template match="*" mode="charcount">
1398  <xsl:param name="incurrent_length" select="0"/>
1399  <xsl:choose>
1400   <xsl:when test="count(child::*) = 0">
1401    <xsl:value-of select="$incurrent_length"/>
1402   </xsl:when>
1403   <xsl:otherwise>
1404     <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>
1405     <xsl:choose>
1406      <xsl:when test="$framewidth >= number($childlength)">
1407       <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>
1408       <xsl:choose>
1409        <xsl:when test="string($siblength) = &quot;&quot;">
1410         <xsl:value-of select="number($childlength)"/>
1411        </xsl:when>
1412        <xsl:otherwise>
1413         <xsl:value-of select="number($siblength)"/>
1414        </xsl:otherwise>
1415       </xsl:choose>
1416      </xsl:when>
1417      <xsl:otherwise>
1418       <xsl:value-of select="number($childlength)"/>
1419      </xsl:otherwise>
1420     </xsl:choose>
1421   </xsl:otherwise>
1422  </xsl:choose>
1423 </xsl:template>
1424
1425
1426 <!--***********************************************************************-->
1427 <!-- OBJECTS                                                               -->
1428 <!--***********************************************************************-->
1429
1430 <!-- DEFINITION -->
1431
1432 <xsl:template match="Definition">
1433 <xsl:param name="current_indent" select="0"/>
1434 <p>
1435 DEFINITION <xsl:value-of select="@name"/>(<xsl:if test="string(./Params) != &quot;&quot;"><xsl:value-of select="Params"/></xsl:if>)<br/>
1436 TYPE =<br/>
1437       <xsl:call-template name="make_indent">
1438        <xsl:with-param name="current_indent" select="$current_indent + 7"/>
1439       </xsl:call-template>
1440        <xsl:apply-templates select="type/*[1]">
1441         <xsl:with-param name="current_indent" select="$current_indent + 7"/>
1442        </xsl:apply-templates><br/>
1443 BODY =<br/>
1444       <xsl:call-template name="make_indent">
1445        <xsl:with-param name="current_indent" select="$current_indent + 7"/>
1446       </xsl:call-template>
1447        <xsl:apply-templates select="body/*[1]">
1448         <xsl:with-param name="current_indent" select="$current_indent + 7"/>
1449        </xsl:apply-templates>
1450 </p>
1451 </xsl:template>
1452
1453 <!-- AXIOM -->
1454
1455 <xsl:template match="Axiom">
1456 <xsl:param name="current_indent" select="0"/>
1457 <p>
1458 AXIOM <xsl:value-of select="@name"/>(<xsl:if test="string(./Params) != &quot;&quot;"><xsl:value-of select="Params"/></xsl:if>)<br/>
1459 TYPE =<br/>
1460       <xsl:call-template name="make_indent">
1461        <xsl:with-param name="current_indent" select="$current_indent + 7"/>
1462       </xsl:call-template>
1463 <xsl:apply-templates select="type/*[1]">
1464           <xsl:with-param name="current_indent" select="$current_indent + 7"/>
1465        </xsl:apply-templates>
1466 </p>
1467 </xsl:template>
1468
1469 <!-- UNFINISHED PROOF -->
1470
1471 <xsl:template match="CurrentProof">
1472 <xsl:param name="current_indent" select="0"/>
1473 <p>
1474 UNFINISHED PROOF <xsl:value-of select="@name"/>(<xsl:if test="string(./Params) != &quot;&quot;"><xsl:value-of select="Params"/></xsl:if>)<br/>
1475 THESIS:  <xsl:apply-templates select="type/*[1]">
1476           <xsl:with-param name="current_indent" select="$current_indent + 8"/>
1477          </xsl:apply-templates><br/>
1478 CONJECTURES:
1479       <xsl:for-each select="Conjecture">
1480       <br/>
1481       <xsl:call-template name="make_indent">
1482        <xsl:with-param name="current_indent" select="$current_indent + 8"/>
1483       </xsl:call-template>
1484       <xsl:value-of select="./@no"/> :
1485       <xsl:apply-templates select="./*[1]">
1486        <xsl:with-param name="current_indent" select="$current_indent + 11"/>
1487       </xsl:apply-templates>
1488       </xsl:for-each>
1489       <br/>
1490 PROOF:
1491       <xsl:apply-templates select="body/*[1]">
1492         <xsl:with-param name="current_indent" select="$current_indent + 8"/>
1493       </xsl:apply-templates>
1494 </p>
1495 </xsl:template>
1496
1497 <!-- MUTUAL INDUCTIVE DEFINITION -->
1498
1499 <xsl:template match="InductiveDefinition">
1500 <xsl:param name="current_indent" select="0"/>
1501 <p>
1502      <xsl:for-each select="InductiveType">
1503          <xsl:choose>
1504          <xsl:when test="position() = 1">
1505           <xsl:choose>
1506           <xsl:when test="string(./@inductive) = &quot;true&quot;">
1507           INDUCTIVE DEFINITION
1508           </xsl:when>
1509           <xsl:otherwise>
1510           COINDUCTIVE DEFINITION
1511           </xsl:otherwise>
1512           </xsl:choose>
1513          </xsl:when>
1514          <xsl:otherwise>
1515           AND
1516          </xsl:otherwise>
1517          </xsl:choose>
1518          <xsl:value-of select="./@name"/>(<xsl:if test="string(../Params) != &quot;&quot;"><xsl:value-of select="../Params"/></xsl:if>)
1519          [
1520           <xsl:if test="string(../Param) != &quot;&quot;">
1521            <xsl:for-each select="../Param">
1522             <xsl:value-of select="./@name"/>
1523             :
1524             <xsl:apply-templates select="*"/>
1525            </xsl:for-each>
1526           </xsl:if>
1527          ] <br/>
1528          OF ARITY
1529          <xsl:apply-templates select="./arity/*[1]">
1530           <xsl:with-param name="current_indent" select="$current_indent + 9"/>
1531          </xsl:apply-templates> <br/>
1532          BUILT FROM:
1533       <xsl:for-each select="./Constructor">
1534       <br/>
1535       <xsl:call-template name="make_indent">
1536        <xsl:with-param name="current_indent" select="$current_indent + 3"/>
1537       </xsl:call-template>
1538          <xsl:choose>
1539          <xsl:when test="position() = 1">
1540          <xsl:text>&#x00A0;&#x00A0;</xsl:text>
1541          </xsl:when>
1542          <xsl:otherwise>
1543          <xsl:text>| </xsl:text>
1544          </xsl:otherwise>
1545          </xsl:choose>
1546          <xsl:value-of select="./@name"/>
1547          <xsl:text>: </xsl:text>
1548          <xsl:apply-templates select="./*[1]">
1549           <xsl:with-param name="current_indent" select="$current_indent + 2*string-length(./@name) + 5"/>
1550          </xsl:apply-templates>
1551       </xsl:for-each>
1552      </xsl:for-each>
1553 </p>
1554 </xsl:template>
1555
1556 <!-- VARIABLE -->
1557
1558 <xsl:template match="Variable">
1559 <xsl:param name="current_indent" select="0"/>
1560 <p>
1561 VARIABLE <xsl:value-of select="@name"/><br/>
1562 TYPE = <xsl:apply-templates select="type/*[1]">
1563           <xsl:with-param name="current_indent" select="$current_indent + 7"/>
1564        </xsl:apply-templates>
1565 </p>
1566 </xsl:template>
1567
1568 <!--***********************************************************************-->
1569 <!-- SECTIONS                                                              -->
1570 <!--***********************************************************************-->
1571
1572 <!-- SECTION -->
1573
1574 <xsl:template match="SECTION">
1575 <xsl:param name="current_indent" select="0"/>
1576  <h1>BEGIN OF SECTION</h1>
1577   <xsl:apply-templates/>
1578  <h1>END OF SECTION</h1>
1579 </xsl:template>
1580
1581 </xsl:stylesheet>