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