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       <!-- nat_ind -->
1132       <xsl:when test="$name='nat_ind_complete'">
1133        <FONT color="red">By induction on&#x00a0;</FONT>
1134        <xsl:apply-templates select="*[2]"/>:
1135        <br/>
1136        <xsl:call-template name="make_indent">
1137         <xsl:with-param name="current_indent" select="$current_indent"/>
1138        </xsl:call-template>
1139        <xsl:text>0&#x00a0;</xsl:text>
1140        <xsl:call-template name="mksymbol-1">
1141         <xsl:with-param name="symbol" select="'RightArrow'"/>
1142         <xsl:with-param name="color" select="'green'"/>
1143         <xsl:with-param name="size" select="'+0'"/>
1144        </xsl:call-template>
1145        <xsl:apply-templates select="*[3]">
1146         <xsl:with-param name="current_indent" select="$current_indent + 8"/>
1147        </xsl:apply-templates>
1148        <br/>
1149        <xsl:call-template name="make_indent">
1150         <xsl:with-param name="current_indent" select="$current_indent"/>
1151        </xsl:call-template>
1152        <xsl:text>S(</xsl:text>
1153        <xsl:apply-templates select="*[4]"/>
1154        <xsl:text>)&#x00a0;</xsl:text>
1155        <xsl:call-template name="mksymbol-1">
1156         <xsl:with-param name="symbol" select="'RightArrow'"/>
1157         <xsl:with-param name="color" select="'green'"/>
1158         <xsl:with-param name="size" select="'+0'"/>
1159        </xsl:call-template>
1160        <FONT color="red">Assume by induction</FONT>
1161        <br/>
1162        <xsl:call-template name="make_indent">
1163         <xsl:with-param name="current_indent" select="$current_indent +10"/>
1164        </xsl:call-template>
1165        <xsl:text>(</xsl:text>
1166        <xsl:apply-templates select="*[5]"/>
1167        <xsl:text>)</xsl:text>
1168        <xsl:apply-templates select="*[6]">
1169         <xsl:with-param name="current_indent" select="$current_indent + 14"/>
1170        </xsl:apply-templates>
1171        <br/>
1172        <xsl:call-template name="make_indent">
1173         <xsl:with-param name="current_indent" select="$current_indent +10"/>
1174        </xsl:call-template>
1175        <xsl:apply-templates select="*[7]">
1176         <xsl:with-param name="current_indent" select="$current_indent + 10"/>
1177        </xsl:apply-templates>
1178       </xsl:when>
1179       <!-- false_ind -->
1180       <xsl:when test="$name='false_ind'">
1181        <xsl:apply-templates select="*[3]">
1182         <xsl:with-param name="current_indent" select="$current_indent"/>
1183        </xsl:apply-templates>
1184        <br/>
1185        <xsl:call-template name="make_indent">
1186         <xsl:with-param name="current_indent" select="$current_indent"/>
1187        </xsl:call-template>
1188        <FONT color="red">Contradiction.</FONT>
1189       </xsl:when>
1190       <!-- and_ind -->
1191       <xsl:when test="$name='and_ind'">
1192        <xsl:choose>
1193         <xsl:when test="name(*[2])='m:apply'">
1194          <xsl:apply-templates select="*[2]">
1195           <xsl:with-param name="current_indent" select="$current_indent"/>
1196          </xsl:apply-templates>
1197         </xsl:when>
1198         <xsl:otherwise>
1199          <FONT color="red">Consider&#x00a0;</FONT>
1200          <xsl:apply-templates select="*[2]"/>
1201         </xsl:otherwise>
1202        </xsl:choose>
1203        <br/>
1204        <xsl:call-template name="make_indent">
1205         <xsl:with-param name="current_indent" select="$current_indent"/>
1206        </xsl:call-template>
1207        <FONT color="red">In particular, we have</FONT>
1208        <br/>
1209        <xsl:call-template name="make_indent">
1210         <xsl:with-param name="current_indent" select="$current_indent"/>
1211        </xsl:call-template>
1212        (
1213        <xsl:apply-templates select="*[3]"/>
1214        )&#x00a0;
1215        <xsl:apply-templates select="*[4]">
1216         <xsl:with-param name="current_indent" select="$current_indent + 9"/>
1217        </xsl:apply-templates>
1218        <br/>
1219        <xsl:call-template name="make_indent">
1220         <xsl:with-param name="current_indent" select="$current_indent"/>
1221        </xsl:call-template>
1222        (
1223        <xsl:apply-templates select="*[5]"/>
1224        )&#x00a0;
1225        <xsl:apply-templates select="*[6]">
1226         <xsl:with-param name="current_indent" select="$current_indent + 9"/>
1227        </xsl:apply-templates>
1228        <br/>
1229        <xsl:call-template name="make_indent">
1230         <xsl:with-param name="current_indent" select="$current_indent"/>
1231        </xsl:call-template>
1232        <xsl:apply-templates select="*[7]">
1233         <xsl:with-param name="current_indent" select="$current_indent"/>
1234        </xsl:apply-templates>
1235       </xsl:when>
1236       <!-- full_or_ind -->
1237       <xsl:when test="$name='full_or_ind'">
1238        <xsl:choose>
1239         <xsl:when test="name(*[2])='m:apply'">
1240          <xsl:apply-templates select="*[2]">
1241           <xsl:with-param name="current_indent" select="$current_indent"/>
1242          </xsl:apply-templates>
1243         </xsl:when>
1244         <xsl:otherwise>
1245          <FONT color="red">Consider&#x00a0;</FONT>
1246          <xsl:apply-templates select="*[2]"/>
1247         </xsl:otherwise>
1248        </xsl:choose>
1249        <br/>
1250        <xsl:call-template name="make_indent">
1251         <xsl:with-param name="current_indent" select="$current_indent"/>
1252        </xsl:call-template>
1253        <FONT color="red">We proceed by cases to prove&#x00a0;</FONT>
1254        <xsl:apply-templates select="*[3]"/>
1255        <br/>
1256        <xsl:call-template name="make_indent">
1257         <xsl:with-param name="current_indent" select="$current_indent+4"/>
1258        </xsl:call-template>
1259        <FONT color="red">Left: suppose&#x00a0;</FONT>
1260        <xsl:text>(</xsl:text>
1261        <xsl:value-of select="*[4]/m:bvar/m:ci"/>
1262        <xsl:text>)&#x00a0;</xsl:text>
1263        <xsl:apply-templates
1264             select="*[4]/m:bvar/m:type/*[1]"/>
1265        <br/>
1266        <xsl:call-template name="make_indent">
1267         <xsl:with-param name="current_indent" select="$current_indent+15"/>
1268        </xsl:call-template>
1269        <xsl:apply-templates
1270             select="*[4]/*[3]">
1271         <xsl:with-param name="current_indent" select="$current_indent+15"/>
1272        </xsl:apply-templates>
1273        <br/>
1274        <xsl:call-template name="make_indent">
1275         <xsl:with-param name="current_indent" select="$current_indent+4"/>
1276        </xsl:call-template>
1277        <FONT color="red">Right: suppose&#x00a0;</FONT>
1278        <xsl:text>(</xsl:text>
1279        <xsl:value-of select="*[5]/m:bvar/m:ci"/>
1280        <xsl:text>)&#x00a0;</xsl:text>
1281        <xsl:apply-templates
1282             select="*[5]/m:bvar/m:type/*[1]"/>
1283        <br/>
1284        <xsl:call-template name="make_indent">
1285         <xsl:with-param name="current_indent" select="$current_indent+16"/>
1286        </xsl:call-template>
1287        <xsl:apply-templates
1288             select="*[5]/*[3]">
1289         <xsl:with-param name="current_indent" select="$current_indent+16"/>
1290        </xsl:apply-templates>
1291       </xsl:when>
1292       <!-- or_ind -->
1293       <xsl:when test="$name='or_ind'">
1294        <xsl:choose>
1295         <xsl:when test="name(*[2])='m:apply'">
1296          <xsl:apply-templates select="*[2]">
1297           <xsl:with-param name="current_indent" select="$current_indent"/>
1298          </xsl:apply-templates>
1299         </xsl:when>
1300         <xsl:otherwise>
1301          <FONT color="red">Consider&#x00a0;</FONT>
1302          <xsl:apply-templates select="*[2]"/>
1303         </xsl:otherwise>
1304        </xsl:choose>
1305        <br/>
1306        <xsl:call-template name="make_indent">
1307         <xsl:with-param name="current_indent" select="$current_indent"/>
1308        </xsl:call-template>
1309        <FONT color="red">We prove&#x00a0;</FONT>
1310        <xsl:apply-templates select="*[3]"/>
1311        <FONT color="red">&#x00a0;by cases:</FONT>
1312        <br/>
1313        <xsl:call-template name="make_indent">
1314         <xsl:with-param name="current_indent" select="$current_indent"/>
1315        </xsl:call-template>
1316        *
1317        <xsl:apply-templates select="*[4]">
1318         <xsl:with-param name="current_indent" select="$current_indent"/>
1319        </xsl:apply-templates>
1320        <br/>
1321        <xsl:call-template name="make_indent">
1322         <xsl:with-param name="current_indent" select="$current_indent"/>
1323        </xsl:call-template>
1324        *
1325        <xsl:apply-templates select="*[5]">
1326         <xsl:with-param name="current_indent" select="$current_indent"/>
1327        </xsl:apply-templates>
1328       </xsl:when>
1329       <!-- Ex_ind -->
1330       <xsl:when test="$name='ex_ind'">
1331        <xsl:choose>
1332         <xsl:when test="name(*[2])='m:apply'">
1333          <xsl:apply-templates select="*[2]">
1334           <xsl:with-param name="current_indent" select="$current_indent"/>
1335          </xsl:apply-templates>
1336         </xsl:when>
1337         <xsl:otherwise>
1338          <FONT color="red">Consider&#x00a0;</FONT>
1339          <xsl:apply-templates select="*[2]">
1340           <xsl:with-param name="current_indent" select="$current_indent"/>
1341          </xsl:apply-templates>
1342         </xsl:otherwise>
1343        </xsl:choose>
1344        <br/>
1345        <xsl:call-template name="make_indent">
1346         <xsl:with-param name="current_indent" select="$current_indent"/>
1347        </xsl:call-template>
1348        <FONT color="red">Let&#x00a0;</FONT>
1349        <xsl:apply-templates mode="inline" select="*[3]"/>
1350        :
1351        <xsl:apply-templates mode="inline" select="*[4]"/>
1352        <FONT color="red">&#x00a0;such that</FONT>
1353        <br/>
1354        <xsl:call-template name="make_indent">
1355         <xsl:with-param name="current_indent" select="$current_indent"/>
1356        </xsl:call-template>
1357        (
1358        <xsl:apply-templates mode="inline" select="*[5]"/>
1359        )
1360        <xsl:apply-templates select="*[6]">
1361         <xsl:with-param name="current_indent" select="$current_indent +7"/>
1362        </xsl:apply-templates>
1363        <br/>
1364        <xsl:call-template name="make_indent">
1365         <xsl:with-param name="current_indent" select="$current_indent"/>
1366        </xsl:call-template>
1367        <xsl:apply-templates select="*[7]">
1368         <xsl:with-param name="current_indent" select="$current_indent"/>
1369        </xsl:apply-templates>
1370       </xsl:when>
1371       <!-- ***************************************** -->
1372       <!-- *********** LAMBDA ELEMENTS ************** -->
1373       <!-- ***************************************** -->
1374       <xsl:when test="$name='subst'">
1375        <xsl:apply-templates select="*[3]"/>
1376        <xsl:text>[</xsl:text>
1377        <xsl:apply-templates select="*[4]"/>
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="'blue'"/>
1382          <xsl:with-param name="size" select="'+0'"/>
1383         </xsl:call-template>
1384        </a>
1385        <xsl:apply-templates select="*[2]"/>
1386        <xsl:text>]</xsl:text>
1387       </xsl:when>
1388
1389       <xsl:when test="$name='lift_with_base'">
1390        <SUB>
1391        <xsl:apply-templates select="*[3]" mode="inline"/>
1392        </SUB>
1393        <a href="{*[1]/@definitionURL}">
1394         <xsl:call-template name="mksymbol-1">
1395          <xsl:with-param name="symbol" select="$name"/>
1396          <xsl:with-param name="color" select="'green'"/>
1397          <xsl:with-param name="size" select="'+0'"/>
1398         </xsl:call-template>
1399        </a>
1400        <SUP>
1401        <xsl:apply-templates select="*[4]" mode="inline"/>
1402        </SUP>
1403        <xsl:text>(</xsl:text>
1404        <xsl:apply-templates select="*[2]" mode="inline"/>
1405        <xsl:text>)</xsl:text>
1406       </xsl:when>
1407
1408       <xsl:when test="$name='lift'">
1409        <a href="{*[1]/@definitionURL}">
1410         <xsl:call-template name="mksymbol-1">
1411          <xsl:with-param name="symbol" select="$name"/>
1412          <xsl:with-param name="color" select="'green'"/>
1413          <xsl:with-param name="size" select="'+0'"/>
1414         </xsl:call-template>
1415        </a>
1416        <SUP>
1417        <xsl:apply-templates select="*[2]" mode="inline"/>
1418        </SUP>
1419        <xsl:text>(</xsl:text>
1420        <xsl:apply-templates select="*[3]" mode="inline"/>
1421        <xsl:text>)</xsl:text>
1422       </xsl:when>
1423
1424       <!-- reduction -->
1425       <xsl:when test="$name='beta_red1'">
1426        <xsl:apply-templates select="*[2]" mode="inline"/>
1427        <a href="{*[1]/@definitionURL}">
1428         <xsl:call-template name="mksymbol-1">
1429          <xsl:with-param name="symbol" select="$name"/>
1430          <xsl:with-param name="color" select="'green'"/>
1431          <xsl:with-param name="size" select="'+0'"/>
1432         </xsl:call-template>
1433        <SUB>
1434         <xsl:call-template name="mksymbol-1">
1435          <xsl:with-param name="symbol" select="'beta'"/>
1436          <xsl:with-param name="color" select="'green'"/>
1437          <xsl:with-param name="size" select="'+0'"/>
1438         </xsl:call-template>
1439        </SUB>
1440        </a>
1441        <xsl:apply-templates select="*[3]" mode="inline"/>
1442       </xsl:when>
1443
1444       <xsl:when test="$name='beta_red'">
1445        <xsl:apply-templates select="*[2]" mode="inline"/>
1446        <a href="{*[1]/@definitionURL}">
1447         <xsl:call-template name="mksymbol-1">
1448          <xsl:with-param name="symbol" select="$name"/>
1449          <xsl:with-param name="color" select="'green'"/>
1450          <xsl:with-param name="size" select="'+0'"/>
1451         </xsl:call-template>
1452        <SUB>
1453         <xsl:call-template name="mksymbol-1">
1454          <xsl:with-param name="symbol" select="'beta'"/>
1455          <xsl:with-param name="color" select="'green'"/>
1456          <xsl:with-param name="size" select="'+0'"/>
1457         </xsl:call-template>
1458         <xsl:text>*</xsl:text>
1459        </SUB>
1460        </a>
1461        <xsl:apply-templates select="*[3]" mode="inline"/>
1462       </xsl:when>
1463
1464       <xsl:when test="$name='par_beta_red1'">
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        <SUB>
1473         <xsl:call-template name="mksymbol-1">
1474          <xsl:with-param name="symbol" select="'beta'"/>
1475          <xsl:with-param name="color" select="'green'"/>
1476          <xsl:with-param name="size" select="'+0'"/>
1477         </xsl:call-template>
1478        </SUB>
1479        </a>
1480        <xsl:apply-templates select="*[3]" mode="inline"/>
1481       </xsl:when>
1482
1483       <xsl:when test="$name='par_beta_red'">
1484        <xsl:apply-templates select="*[2]" mode="inline"/>
1485        <a href="{*[1]/@definitionURL}">
1486         <xsl:call-template name="mksymbol-1">
1487          <xsl:with-param name="symbol" select="$name"/>
1488          <xsl:with-param name="color" select="'green'"/>
1489          <xsl:with-param name="size" select="'+0'"/>
1490         </xsl:call-template>
1491        <SUB>
1492         <xsl:call-template name="mksymbol-1">
1493          <xsl:with-param name="symbol" select="'beta'"/>
1494          <xsl:with-param name="color" select="'green'"/>
1495          <xsl:with-param name="size" select="'+0'"/>
1496         </xsl:call-template>
1497         <xsl:text>*</xsl:text>
1498        </SUB>
1499        </a>
1500        <xsl:apply-templates select="*[3]" mode="inline"/>
1501       </xsl:when>
1502
1503       <!-- forgetful -->
1504       <xsl:when test="$name='forgetful'">
1505        <a href="{*[1]/@definitionURL}">|</a>
1506        <xsl:apply-templates select="*[2]" mode="inline"/>
1507        <a href="{*[1]/@definitionURL}">|</a>
1508       </xsl:when>
1509
1510       <!-- boolean algebra of redexes -->
1511
1512       <!-- isomorphic -->
1513       <xsl:when test="$name='isomorphic'">
1514        <xsl:apply-templates select="*[2]" mode="inline"/>
1515        <a href="{*[1]/@definitionURL}">
1516         <xsl:call-template name="mksymbol-1">
1517          <xsl:with-param name="symbol" select="$name"/>
1518          <xsl:with-param name="color" select="'green'"/>
1519          <xsl:with-param name="size" select="'+0'"/>
1520         </xsl:call-template>
1521        </a>
1522        <xsl:apply-templates select="*[3]" mode="inline"/>
1523       </xsl:when>
1524
1525       <!-- INTERP -->
1526       <xsl:when test="$name='interp'">
1527          <font color="green">[</font>
1528             <xsl:apply-templates select="*[2]"/>
1529          <font color="green">]</font>
1530       </xsl:when>
1531
1532      </xsl:choose>
1533 </xsl:template>
1534
1535 <!-- LAMBDA -->
1536
1537 <xsl:template match="m:lambda">
1538 <xsl:param name="current_indent" select="0"/>
1539     <xsl:variable name="charlength">
1540      <xsl:apply-templates select="*[position()=1]" mode="charcount"/>
1541      <!-- <xsl:apply-templates select="." mode="charcount"/> -->
1542     </xsl:variable>
1543     <!-- <xsl:value-of select="$charlength"/> -->
1544     <!-- <xsl:value-of select="$current_indent"/> -->
1545      <xsl:choose>
1546      <xsl:when test="$charlength > $framewidth">
1547        <!-- &#x03bb; -->
1548        <xsl:call-template name="mksymbol-1">
1549         <xsl:with-param name="symbol" select="'lambda'"/>
1550         <xsl:with-param name="color" select="'red'"/>
1551         <xsl:with-param name="size" select="'+2'"/>
1552        </xsl:call-template>
1553        <xsl:apply-templates select="m:bvar/m:ci"/>
1554        <xsl:text>:</xsl:text>
1555        <xsl:apply-templates select="m:bvar/m:type">
1556         <xsl:with-param name="current_indent"
1557            select="$current_indent + 4 + 2*string-length(m:bvar/m:ci)"/>
1558        </xsl:apply-templates><br/>
1559        <xsl:call-template name="make_indent">
1560         <xsl:with-param name="current_indent" select="$current_indent + 2"/>
1561        </xsl:call-template>
1562        <xsl:text>.</xsl:text>
1563        <xsl:apply-templates select="*[position()=2]">
1564         <xsl:with-param name="current_indent" select="$current_indent + 2"/>
1565        </xsl:apply-templates>
1566      </xsl:when>
1567      <xsl:otherwise>
1568       <xsl:apply-templates mode="inline" select="."/>
1569      </xsl:otherwise>
1570      </xsl:choose>
1571 </xsl:template>
1572
1573 <!-- href -->
1574 <xsl:template match="m:ci">
1575  <xsl:choose>
1576   <xsl:when test="boolean(@definitionURL)">
1577    <a href="{@definitionURL}">
1578    <xsl:apply-templates/>
1579    </a>
1580   </xsl:when>
1581   <xsl:otherwise>
1582    <xsl:value-of select="."/>
1583   </xsl:otherwise>
1584  </xsl:choose>
1585 </xsl:template>
1586
1587 <!-- COUNTING -->
1588
1589 <xsl:template match="m:ci|m:csymbol" mode="charcount">
1590 <xsl:param name="incurrent_length" select="0"/>
1591     <xsl:choose>
1592     <xsl:when test="$framewidth >= ($incurrent_length + string-length())">
1593      <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>
1594      <xsl:choose>
1595      <xsl:when test="string($siblength) = &quot;&quot;">
1596       <xsl:value-of select="$incurrent_length + string-length()"/>
1597      </xsl:when>
1598      <xsl:otherwise>
1599       <xsl:value-of select="number($siblength)"/>
1600      </xsl:otherwise>
1601      </xsl:choose>
1602     </xsl:when>
1603     <xsl:otherwise>
1604      <xsl:value-of select="$incurrent_length + string-length()"/>
1605     </xsl:otherwise>
1606     </xsl:choose>
1607 </xsl:template>
1608
1609 <xsl:template match="*" mode="charcount">
1610  <xsl:param name="incurrent_length" select="0"/>
1611  <xsl:choose>
1612   <xsl:when test="count(child::*) = 0">
1613    <xsl:value-of select="$incurrent_length"/>
1614   </xsl:when>
1615   <xsl:otherwise>
1616     <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>
1617     <xsl:choose>
1618      <xsl:when test="$framewidth >= number($childlength)">
1619       <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>
1620       <xsl:choose>
1621        <xsl:when test="string($siblength) = &quot;&quot;">
1622         <xsl:value-of select="number($childlength)"/>
1623        </xsl:when>
1624        <xsl:otherwise>
1625         <xsl:value-of select="number($siblength)"/>
1626        </xsl:otherwise>
1627       </xsl:choose>
1628      </xsl:when>
1629      <xsl:otherwise>
1630       <xsl:value-of select="number($childlength)"/>
1631      </xsl:otherwise>
1632     </xsl:choose>
1633   </xsl:otherwise>
1634  </xsl:choose>
1635 </xsl:template>
1636
1637
1638 <!--***********************************************************************-->
1639 <!-- OBJECTS                                                               -->
1640 <!--***********************************************************************-->
1641
1642 <!-- DEFINITION -->
1643
1644 <xsl:template match="Definition">
1645 <xsl:param name="current_indent" select="0"/>
1646 <p>
1647 DEFINITION <xsl:value-of select="@name"/>(<xsl:if test="string(./Params) != &quot;&quot;"><xsl:value-of select="Params"/></xsl:if>)<br/>
1648 TYPE =<br/>
1649       <xsl:call-template name="make_indent">
1650        <xsl:with-param name="current_indent" select="$current_indent + 7"/>
1651       </xsl:call-template>
1652        <xsl:apply-templates select="type/*[1]">
1653         <xsl:with-param name="current_indent" select="$current_indent + 7"/>
1654        </xsl:apply-templates><br/>
1655 BODY =<br/>
1656       <xsl:call-template name="make_indent">
1657        <xsl:with-param name="current_indent" select="$current_indent + 7"/>
1658       </xsl:call-template>
1659        <xsl:apply-templates select="body/*[1]">
1660         <xsl:with-param name="current_indent" select="$current_indent + 7"/>
1661        </xsl:apply-templates>
1662 </p>
1663 </xsl:template>
1664
1665 <!-- AXIOM -->
1666
1667 <xsl:template match="Axiom">
1668 <xsl:param name="current_indent" select="0"/>
1669 <p>
1670 AXIOM <xsl:value-of select="@name"/>(<xsl:if test="string(./Params) != &quot;&quot;"><xsl:value-of select="Params"/></xsl:if>)<br/>
1671 TYPE =<br/>
1672       <xsl:call-template name="make_indent">
1673        <xsl:with-param name="current_indent" select="$current_indent + 7"/>
1674       </xsl:call-template>
1675 <xsl:apply-templates select="type/*[1]">
1676           <xsl:with-param name="current_indent" select="$current_indent + 7"/>
1677        </xsl:apply-templates>
1678 </p>
1679 </xsl:template>
1680
1681 <!-- UNFINISHED PROOF -->
1682
1683 <xsl:template match="CurrentProof">
1684 <xsl:param name="current_indent" select="0"/>
1685 <p>
1686 UNFINISHED PROOF <xsl:value-of select="@name"/>(<xsl:if test="string(./Params) != &quot;&quot;"><xsl:value-of select="Params"/></xsl:if>)<br/>
1687 THESIS:  <xsl:apply-templates select="type/*[1]">
1688           <xsl:with-param name="current_indent" select="$current_indent + 8"/>
1689          </xsl:apply-templates><br/>
1690 CONJECTURES:
1691       <xsl:for-each select="Conjecture">
1692       <br/>
1693       <xsl:call-template name="make_indent">
1694        <xsl:with-param name="current_indent" select="$current_indent + 8"/>
1695       </xsl:call-template>
1696       <xsl:value-of select="./@no"/> :
1697       <xsl:apply-templates select="./*[1]">
1698        <xsl:with-param name="current_indent" select="$current_indent + 11"/>
1699       </xsl:apply-templates>
1700       </xsl:for-each>
1701       <br/>
1702 PROOF:
1703       <xsl:apply-templates select="body/*[1]">
1704         <xsl:with-param name="current_indent" select="$current_indent + 8"/>
1705       </xsl:apply-templates>
1706 </p>
1707 </xsl:template>
1708
1709 <!-- MUTUAL INDUCTIVE DEFINITION -->
1710
1711 <xsl:template match="InductiveDefinition">
1712 <xsl:param name="current_indent" select="0"/>
1713 <p>
1714      <xsl:for-each select="InductiveType">
1715          <xsl:choose>
1716          <xsl:when test="position() = 1">
1717           <xsl:choose>
1718           <xsl:when test="string(./@inductive) = &quot;true&quot;">
1719           INDUCTIVE DEFINITION
1720           </xsl:when>
1721           <xsl:otherwise>
1722           COINDUCTIVE DEFINITION
1723           </xsl:otherwise>
1724           </xsl:choose>
1725          </xsl:when>
1726          <xsl:otherwise>
1727           AND
1728          </xsl:otherwise>
1729          </xsl:choose>
1730          <xsl:value-of select="./@name"/>(<xsl:if test="string(../Params) != &quot;&quot;"><xsl:value-of select="../Params"/></xsl:if>)
1731          [
1732           <xsl:if test="string(../Param) != &quot;&quot;">
1733            <xsl:for-each select="../Param">
1734             <xsl:value-of select="./@name"/>
1735             :
1736             <xsl:apply-templates select="*"/>
1737            </xsl:for-each>
1738           </xsl:if>
1739          ] <br/>
1740          OF ARITY
1741          <xsl:apply-templates select="./arity/*[1]">
1742           <xsl:with-param name="current_indent" select="$current_indent + 9"/>
1743          </xsl:apply-templates> <br/>
1744          BUILT FROM:
1745       <xsl:for-each select="./Constructor">
1746       <br/>
1747       <xsl:call-template name="make_indent">
1748        <xsl:with-param name="current_indent" select="$current_indent + 3"/>
1749       </xsl:call-template>
1750          <xsl:choose>
1751          <xsl:when test="position() = 1">
1752          <xsl:text>&#x00A0;&#x00A0;</xsl:text>
1753          </xsl:when>
1754          <xsl:otherwise>
1755          <xsl:text>| </xsl:text>
1756          </xsl:otherwise>
1757          </xsl:choose>
1758          <xsl:value-of select="./@name"/>
1759          <xsl:text>: </xsl:text>
1760          <xsl:apply-templates select="./*[1]">
1761           <xsl:with-param name="current_indent" select="$current_indent + 2*string-length(./@name) + 5"/>
1762          </xsl:apply-templates>
1763       </xsl:for-each>
1764      </xsl:for-each>
1765 </p>
1766 </xsl:template>
1767
1768 <!-- VARIABLE -->
1769
1770 <xsl:template match="Variable">
1771 <xsl:param name="current_indent" select="0"/>
1772 <p>
1773 VARIABLE <xsl:value-of select="@name"/><br/>
1774 TYPE = <xsl:apply-templates select="type/*[1]">
1775           <xsl:with-param name="current_indent" select="$current_indent + 7"/>
1776        </xsl:apply-templates>
1777 </p>
1778 </xsl:template>
1779
1780 <!--***********************************************************************-->
1781 <!-- SECTIONS                                                              -->
1782 <!--***********************************************************************-->
1783
1784 <!-- SECTION -->
1785
1786 <xsl:template match="SECTION">
1787 <xsl:param name="current_indent" select="0"/>
1788  <h1>BEGIN OF SECTION</h1>
1789   <xsl:apply-templates/>
1790  <h1>END OF SECTION</h1>
1791 </xsl:template>
1792
1793 </xsl:stylesheet>