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