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