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="55"/>
  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          <script>
 171           <xsl:text disable-output-escaping="yes">
 172            <![CDATA[
 173             function Hide(which){
 174              if (!document.getElementById)
 175               return
 176              which.style.display="none"
 177             }
 178
 179             function Show(which){
 180              if (!document.getElementById)
 181               return
 182              which.style.display=""
 183             }
 184
 185             document.to_be_deleted = new Array();
 186           ]]>
 187           </xsl:text>
 188          </script>
 189       </head>
 190       <body bgcolor="white">
 191          <xsl:attribute name="onLoad">
 192           if(document.getElementById)
 193            for(var i=0;i&lt;document.to_be_deleted.length;i++)
 194             Hide(document.getElementById(document.to_be_deleted[i]));
 195          </xsl:attribute>
 196          <xsl:apply-templates>
 197             <xsl:with-param name="current_indent" select="0"/>
 198          </xsl:apply-templates>
 199       </body>
 200    </html>
 201   </xsl:when>
 202   <xsl:otherwise>
 203    <to_be_embedded>
 204     <xsl:apply-templates>
 205      <xsl:with-param name="current_indent" select="0"/>
 206     </xsl:apply-templates>
 207    </to_be_embedded>
 208   </xsl:otherwise>
 209  </xsl:choose>
 210 </xsl:template>
 211
 212 <!--***********************************************************************-->
 213 <!-- Indentation                                                           -->
 214 <!--***********************************************************************-->
 215
 216 <xsl:template name="make_indent">
 217  <xsl:param name="current_indent" select="0"/>
 218   <xsl:if test="$current_indent > 0">
 219    <xsl:text>&#x00a0;</xsl:text>
 220    <xsl:call-template name="make_indent">
 221     <xsl:with-param name="current_indent" select="$current_indent - 1"/>
 222    </xsl:call-template>
 223   </xsl:if>
 224 </xsl:template>
 225
 226 <!-- Syntactic Sugar -->
 227 <xsl:template match="m:type">
 228 <xsl:param name="current_indent" select="0"/>
 229 <xsl:apply-templates>
 230  <xsl:with-param name="current_indent"
 231            select="$current_indent"/>
 232 </xsl:apply-templates>
 233 </xsl:template>
 234
 235 <xsl:template match="m:condition">
 236 <xsl:param name="current_indent" select="0"/>
 237 <xsl:apply-templates>
 238  <xsl:with-param name="current_indent"
 239            select="$current_indent"/>
 240 </xsl:apply-templates>
 241 </xsl:template>
 242
 243 <xsl:template match="m:math">
 244 <xsl:param name="current_indent" select="0"/>
 245 <xsl:apply-templates>
 246  <xsl:with-param name="current_indent"
 247            select="$current_indent"/>
 248 </xsl:apply-templates>
 249 </xsl:template>
 250
 251 <!--*********************************************************************-->
 252 <!--                         INLINE MODE                                 -->
 253 <!--*********************************************************************-->
 254
 255 <!-- href -->
 256 <xsl:template mode="inline" match="m:ci">
 257  <xsl:choose>
 258   <xsl:when test="boolean(@definitionURL)">
 259    <a href="{@definitionURL}">
 260    <xsl:apply-templates/>
 261    </a>
 262   </xsl:when>
 263   <xsl:otherwise>
 264    <xsl:value-of select="."/>
 265   </xsl:otherwise>
 266  </xsl:choose>
 267 </xsl:template>
 268
 269 <!-- CSYMBOL -->
 270
 271 <xsl:template match="m:apply[m:csymbol]" mode="inline">
 272    <xsl:variable name="name">
 273     <xsl:value-of select="m:csymbol"/>
 274    </xsl:variable>
 275    <xsl:variable name="uri"><xsl:value-of select="*[1]/@definitionURL"/></xsl:variable>
 276    <xsl:choose>
 277     <!-- FORALL -->
 278     <xsl:when test="$name='forall'">
 279      <xsl:call-template name="mksymbol-1">
 280       <xsl:with-param name="symbol" select="$name"/>
 281       <xsl:with-param name="color" select="'blue'"/>
 282       <xsl:with-param name="size" select="'+2'"/>
 283      </xsl:call-template>
 284      <xsl:apply-templates select="m:bvar/m:ci"/>
 285      <xsl:text>:</xsl:text>
 286      <xsl:apply-templates mode="inline" select="m:bvar/m:type"/>
 287      <xsl:text>.</xsl:text>
 288      <xsl:apply-templates mode="inline" select="*[position()=3]"/>
 289     </xsl:when>
 290     <xsl:when test="$name='prod'">
 291      <xsl:call-template name="mksymbol-1">
 292       <xsl:with-param name="symbol" select="$name"/>
 293       <xsl:with-param name="color" select="'blue'"/>
 294       <xsl:with-param name="size" select="'+2'"/>
 295      </xsl:call-template>
 296      <xsl:apply-templates mode="inline" select="m:bvar/m:ci"/>
 297      <xsl:text>:</xsl:text>
 298      <xsl:apply-templates mode="inline" select="m:bvar/m:type"/>
 299      <xsl:text>.</xsl:text>
 300      <xsl:apply-templates mode="inline" select="*[position()=3]"/>
 301     </xsl:when>
 302     <!-- ARROW -->
 303     <xsl:when test="$name='arrow'">
 304      <xsl:text>(</xsl:text>
 305      <xsl:apply-templates mode="inline" select="*[position()=2]"/>
 306      <xsl:call-template name="mksymbol-1">
 307       <xsl:with-param name="symbol" select="$name"/>
 308       <xsl:with-param name="color" select="'blue'"/>
 309       <xsl:with-param name="size" select="'+0'"/>
 310      </xsl:call-template>
 311      <xsl:apply-templates mode="inline" select="*[position()=3]"/>
 312      <xsl:text>)</xsl:text>
 313     </xsl:when>
 314     <!-- APP -->
 315     <xsl:when test="$name='app'">
 316      <xsl:text>(</xsl:text>
 317      <xsl:apply-templates mode="inline" select="*[position()=2]"/>
 318      <xsl:for-each select="*[position()>2]">
 319       <xsl:text>&#x00A0;</xsl:text>
 320       <xsl:apply-templates mode="inline" select="."/>
 321      </xsl:for-each>
 322      <xsl:text>)</xsl:text>
 323     </xsl:when>
 324     <!-- CAST -->
 325     <xsl:when test="$name='cast'">
 326      <xsl:text>(</xsl:text>
 327      <xsl:apply-templates mode="inline" select="*[position()=2]"/>
 328      <xsl:text>:></xsl:text>
 329      <xsl:apply-templates mode="inline" select="*[position()=3]"/>
 330      <xsl:text>)</xsl:text>
 331     </xsl:when>
 332     <xsl:when test="$name='Prop'">
 333      <FONT color="violet">Prop</FONT>
 334     </xsl:when>
 335     <xsl:when test="$name='Set'">
 336      <FONT color="violet">Set</FONT>
 337     </xsl:when>
 338     <xsl:when test="$name='Type'">
 339      <FONT color="violet">Type</FONT>
 340     </xsl:when>
 341     <!-- MUTCASE -->
 342     <xsl:when test="$name='mutcase'">
 343      <xsl:text>&lt;</xsl:text>
 344      <xsl:apply-templates mode="inline" select="*[position()=2]"/>
 345      <xsl:text>&gt; </xsl:text>
 346      <FONT color="red">CASE </FONT>
 347      <xsl:apply-templates mode="inline" select="*[position()=3]"/>
 348      <FONT color="red"> OF </FONT>
 349 <xsl:for-each select="piecewise/piece">
 350 <!--<xsl:for-each select="*[position() mod 2 = 0 and position()>3]">-->
 351       <xsl:choose>
 352        <xsl:when test="not(position() = 1)">
 353         <xsl:text> | </xsl:text>
 354        </xsl:when>
 355       </xsl:choose>
 356 <xsl:apply-templates mode="inline" select="./*[2]"/>
 357       <xsl:call-template name="mksymbol-1">
 358        <xsl:with-param name="symbol" select="'RightArrow'"/>
 359        <xsl:with-param name="color" select="'green'"/>
 360        <xsl:with-param name="size" select="'+0'"/>
 361       </xsl:call-template>
 362       <xsl:apply-templates mode="inline"
 363            select="./*[1]"/>
 364      </xsl:for-each>
 365     </xsl:when>
 366     <!-- FIX -->
 367     <xsl:when test="$name='fix'">
 368      <FONT color="red">FIX</FONT>
 369      <xsl:value-of select="m:ci"/>
 370      <xsl:text>{</xsl:text>
 371      <xsl:for-each select="m:bvar">
 372       <xsl:value-of select="m:ci"/>
 373       <xsl:text>:</xsl:text>
 374       <xsl:apply-templates mode="inline" select="m:type"/>
 375       <xsl:text>:=</xsl:text>
 376       <xsl:apply-templates mode="inline"
 377              select="following-sibling::*[position() = 1]"/>
 378       <xsl:choose>
 379        <xsl:when test="position()=last()">
 380         <xsl:text>}</xsl:text>
 381        </xsl:when>
 382        <xsl:otherwise>
 383         <xsl:text>;</xsl:text>
 384        </xsl:otherwise>
 385       </xsl:choose>
 386      </xsl:for-each>
 387     </xsl:when>
 388     <!-- COFIX -->
 389     <xsl:when test="$name='cofix'">
 390      <xsl:text>COFIX</xsl:text>
 391      <xsl:value-of select="m:ci"/>
 392      <xsl:text>{</xsl:text>
 393      <xsl:for-each select="m:bvar">
 394       <xsl:value-of select="m:ci"/>
 395       <xsl:text>:</xsl:text>
 396       <xsl:apply-templates mode="inline" select="m:type"/>
 397       <xsl:text>:=</xsl:text>
 398       <xsl:apply-templates mode="inline"
 399           select="following-sibling::*[position() = 1]"/>
 400       <xsl:choose>
 401        <xsl:when test="position()=last()">
 402         <xsl:text>}</xsl:text>
 403        </xsl:when>
 404        <xsl:otherwise>
 405         <xsl:text>;</xsl:text>
 406        </xsl:otherwise>
 407       </xsl:choose>
 408      </xsl:for-each>
 409     </xsl:when>
 410     <!-- proof and side_proof -->
 411     <xsl:when test="$name='proof' or $name='side_proof'">
 412        <xsl:apply-templates mode="inline" select="*[position()=2]"/>
 413        <FONT color="red">&#x00a0;proves&#x00a0;</FONT>
 414        <xsl:apply-templates mode="inline" select="*[position()=3]"/>
 415     </xsl:when>
 416     <!-- letin1 -->
 417     <xsl:when test="$name='letin1'">
 418      <xsl:text>letin1 (inline error)</xsl:text>
 419     </xsl:when>
 420     <!-- false_ind -->
 421     <xsl:when test="$name='false_ind'">
 422     <xsl:apply-templates mode="inline" select="*[3]"/>
 423     <FONT color="red">Contradiction.</FONT>
 424     </xsl:when>
 425     <!-- and_ind -->
 426     <xsl:when test="$name='and_ind'">
 427      <FONT color="red">From&#x00a0;</FONT>
 428      <xsl:apply-templates select="*[2]"/>
 429      <FONT color="red">&#x00a0;we get</FONT>
 430      (
 431      <xsl:apply-templates select="*[3]"/>
 432      )&#x00a0;
 433      <xsl:apply-templates mode="inline" select="*[4]"/>
 434      <FONT color="red">&#x00a0;and&#x00a0;</FONT>
 435      (
 436      <xsl:apply-templates select="*[5]"/>
 437      )&#x00a0;
 438      <xsl:apply-templates mode="inline" select="*[6]"/>
 439      ;
 440      <FONT color="red">&#x00a0;hence&#x00a0;</FONT>
 441      <xsl:apply-templates mode="inline" select="*[7]"/>
 442     </xsl:when>
 443
 444        <xsl:when test="$name='subst'">
 445        <xsl:apply-templates select="*[3]" mode="inline"/>
 446        <xsl:text>[</xsl:text>
 447        <xsl:apply-templates select="*[4]" mode="inline"/>
 448        <xsl:choose>
 449        <xsl:when test="$uri != ''">
 450         <a href="{$uri}">
 451          <xsl:call-template name="mksymbol-1">
 452           <xsl:with-param name="symbol" select="$name"/>
 453           <xsl:with-param name="color" select="'green'"/>
 454           <xsl:with-param name="size" select="'+0'"/>
 455          </xsl:call-template>
 456         </a>
 457        </xsl:when>
 458        <xsl:otherwise>
 459          <xsl:call-template name="mksymbol-1">
 460           <xsl:with-param name="symbol" select="$name"/>
 461           <xsl:with-param name="color" select="'green'"/>
 462           <xsl:with-param name="size" select="'+0'"/>
 463          </xsl:call-template>
 464        </xsl:otherwise>
 465        </xsl:choose>
 466        <xsl:apply-templates select="*[2]" mode="inline"/>
 467        <xsl:text>]</xsl:text>
 468       </xsl:when>
 469
 470       <xsl:when test="$name='lift_with_base'">
 471        <SUB>
 472        <xsl:apply-templates select="*[3]" mode="inline"/>
 473        </SUB>
 474        <xsl:choose>
 475        <xsl:when test="$uri != ''">
 476          <a href="{$uri}">
 477           <xsl:call-template name="mksymbol-1">
 478            <xsl:with-param name="symbol" select="$name"/>
 479            <xsl:with-param name="color" select="'green'"/>
 480            <xsl:with-param name="size" select="'+0'"/>
 481           </xsl:call-template>
 482          </a>
 483        </xsl:when>
 484        <xsl:otherwise>
 485           <xsl:call-template name="mksymbol-1">
 486            <xsl:with-param name="symbol" select="$name"/>
 487            <xsl:with-param name="color" select="'green'"/>
 488            <xsl:with-param name="size" select="'+0'"/>
 489           </xsl:call-template>
 490        </xsl:otherwise>
 491        </xsl:choose>
 492        <SUP>
 493        <xsl:apply-templates select="*[4]" mode="inline"/>
 494        </SUP>
 495        <xsl:text>(</xsl:text>
 496        <xsl:apply-templates select="*[2]" mode="inline"/>
 497        <xsl:text>)</xsl:text>
 498       </xsl:when>
 499
 500       <xsl:when test="$name='lift'">
 501        <xsl:choose>
 502        <xsl:when test="$uri != ''">
 503         <a href="{$uri}">
 504          <xsl:call-template name="mksymbol-1">
 505           <xsl:with-param name="symbol" select="$name"/>
 506           <xsl:with-param name="color" select="'green'"/>
 507           <xsl:with-param name="size" select="'+0'"/>
 508          </xsl:call-template>
 509         </a>
 510        </xsl:when>
 511        <xsl:otherwise>
 512          <xsl:call-template name="mksymbol-1">
 513           <xsl:with-param name="symbol" select="$name"/>
 514           <xsl:with-param name="color" select="'green'"/>
 515           <xsl:with-param name="size" select="'+0'"/>
 516          </xsl:call-template>
 517        </xsl:otherwise>
 518        </xsl:choose>
 519        <SUP>
 520        <xsl:apply-templates select="*[2]" mode="inline"/>
 521        </SUP>
 522        <xsl:text>(</xsl:text>
 523        <xsl:apply-templates select="*[3]" mode="inline"/>
 524        <xsl:text>)</xsl:text>
 525       </xsl:when>
 526
 527       <!-- reduction -->
 528       <xsl:when test="$name='beta_red1'">
 529        <xsl:apply-templates select="*[2]" mode="inline"/>
 530        <xsl:choose>
 531        <xsl:when test="$uri != ''">
 532         <a href="{$uri}">
 533          <xsl:call-template name="mksymbol-1">
 534           <xsl:with-param name="symbol" select="$name"/>
 535           <xsl:with-param name="color" select="'green'"/>
 536           <xsl:with-param name="size" select="'+0'"/>
 537          </xsl:call-template>
 538          <SUB>
 539          <xsl:call-template name="mksymbol-1">
 540           <xsl:with-param name="symbol" select="'beta'"/>
 541           <xsl:with-param name="color" select="'green'"/>
 542           <xsl:with-param name="size" select="'+0'"/>
 543          </xsl:call-template>
 544          </SUB>
 545         </a>
 546        </xsl:when>
 547        <xsl:otherwise>
 548          <xsl:call-template name="mksymbol-1">
 549           <xsl:with-param name="symbol" select="$name"/>
 550           <xsl:with-param name="color" select="'green'"/>
 551           <xsl:with-param name="size" select="'+0'"/>
 552          </xsl:call-template>
 553          <SUB>
 554          <xsl:call-template name="mksymbol-1">
 555           <xsl:with-param name="symbol" select="'beta'"/>
 556           <xsl:with-param name="color" select="'green'"/>
 557           <xsl:with-param name="size" select="'+0'"/>
 558          </xsl:call-template>
 559          </SUB>
 560        </xsl:otherwise>
 561        </xsl:choose>
 562        <xsl:apply-templates select="*[3]" mode="inline"/>
 563       </xsl:when>
 564
 565       <xsl:when test="$name='beta_red'">
 566        <xsl:apply-templates select="*[2]" mode="inline"/>
 567        <xsl:choose>
 568        <xsl:when test="$uri != ''">
 569         <a href="{$uri}">
 570          <xsl:call-template name="mksymbol-1">
 571           <xsl:with-param name="symbol" select="$name"/>
 572           <xsl:with-param name="color" select="'green'"/>
 573           <xsl:with-param name="size" select="'+0'"/>
 574          </xsl:call-template>
 575          <SUB>
 576          <xsl:call-template name="mksymbol-1">
 577           <xsl:with-param name="symbol" select="'beta'"/>
 578           <xsl:with-param name="color" select="'green'"/>
 579           <xsl:with-param name="size" select="'+0'"/>
 580          </xsl:call-template>
 581          <xsl:text>*</xsl:text>
 582          </SUB>
 583         </a>
 584        </xsl:when>
 585        <xsl:otherwise>
 586          <xsl:call-template name="mksymbol-1">
 587           <xsl:with-param name="symbol" select="$name"/>
 588           <xsl:with-param name="color" select="'green'"/>
 589           <xsl:with-param name="size" select="'+0'"/>
 590          </xsl:call-template>
 591          <SUB>
 592          <xsl:call-template name="mksymbol-1">
 593           <xsl:with-param name="symbol" select="'beta'"/>
 594           <xsl:with-param name="color" select="'green'"/>
 595           <xsl:with-param name="size" select="'+0'"/>
 596          </xsl:call-template>
 597          <xsl:text>*</xsl:text>
 598          </SUB>
 599        </xsl:otherwise>
 600        </xsl:choose>
 601        <xsl:apply-templates select="*[3]" mode="inline"/>
 602       </xsl:when>
 603
 604       <xsl:when test="$name='par_beta_red1'">
 605        <xsl:apply-templates select="*[2]" mode="inline"/>
 606        <xsl:choose>
 607        <xsl:when test="$uri != ''">
 608         <a href="{$uri}">
 609          <xsl:call-template name="mksymbol-1">
 610           <xsl:with-param name="symbol" select="$name"/>
 611           <xsl:with-param name="color" select="'green'"/>
 612           <xsl:with-param name="size" select="'+0'"/>
 613          </xsl:call-template>
 614          <SUB>
 615          <xsl:call-template name="mksymbol-1">
 616           <xsl:with-param name="symbol" select="'beta'"/>
 617           <xsl:with-param name="color" select="'green'"/>
 618           <xsl:with-param name="size" select="'+0'"/>
 619          </xsl:call-template>
 620          </SUB>
 621         </a>
 622        </xsl:when>
 623        <xsl:otherwise>
 624          <xsl:call-template name="mksymbol-1">
 625           <xsl:with-param name="symbol" select="$name"/>
 626           <xsl:with-param name="color" select="'green'"/>
 627           <xsl:with-param name="size" select="'+0'"/>
 628          </xsl:call-template>
 629          <SUB>
 630          <xsl:call-template name="mksymbol-1">
 631           <xsl:with-param name="symbol" select="'beta'"/>
 632           <xsl:with-param name="color" select="'green'"/>
 633           <xsl:with-param name="size" select="'+0'"/>
 634          </xsl:call-template>
 635          </SUB>
 636        </xsl:otherwise>
 637        </xsl:choose>
 638        <xsl:apply-templates select="*[3]" mode="inline"/>
 639       </xsl:when>
 640
 641       <xsl:when test="$name='par_beta_red'">
 642        <xsl:apply-templates select="*[2]" mode="inline"/>
 643        <xsl:choose>
 644        <xsl:when test="$uri != ''">
 645         <a href="{$uri}">
 646          <xsl:call-template name="mksymbol-1">
 647           <xsl:with-param name="symbol" select="$name"/>
 648           <xsl:with-param name="color" select="'green'"/>
 649           <xsl:with-param name="size" select="'+0'"/>
 650          </xsl:call-template>
 651          <SUB>
 652          <xsl:call-template name="mksymbol-1">
 653           <xsl:with-param name="symbol" select="'beta'"/>
 654           <xsl:with-param name="color" select="'green'"/>
 655           <xsl:with-param name="size" select="'+0'"/>
 656          </xsl:call-template>
 657          <xsl:text>*</xsl:text>
 658          </SUB>
 659         </a>
 660        </xsl:when>
 661        <xsl:otherwise>
 662          <xsl:call-template name="mksymbol-1">
 663           <xsl:with-param name="symbol" select="$name"/>
 664           <xsl:with-param name="color" select="'green'"/>
 665           <xsl:with-param name="size" select="'+0'"/>
 666          </xsl:call-template>
 667          <SUB>
 668          <xsl:call-template name="mksymbol-1">
 669           <xsl:with-param name="symbol" select="'beta'"/>
 670           <xsl:with-param name="color" select="'green'"/>
 671           <xsl:with-param name="size" select="'+0'"/>
 672          </xsl:call-template>
 673          <xsl:text>*</xsl:text>
 674          </SUB>
 675        </xsl:otherwise>
 676        </xsl:choose>
 677        <xsl:apply-templates select="*[3]" mode="inline"/>
 678       </xsl:when>
 679
 680       <!-- forgetful -->
 681       <xsl:when test="$name='forgetful'">
 682        <xsl:choose>
 683        <xsl:when test="$uri != ''">
 684         <a href="{$uri}">|</a>
 685        </xsl:when>
 686        <xsl:otherwise>
 687         |
 688        </xsl:otherwise>
 689        </xsl:choose>
 690        <xsl:apply-templates select="*[2]" mode="inline"/>
 691         <xsl:choose>
 692         <xsl:when test="$uri != ''">
 693          <a href="{$uri}">|</a>
 694         </xsl:when>
 695        <xsl:otherwise>
 696         |
 697        </xsl:otherwise>
 698        </xsl:choose>
 699       </xsl:when>
 700
 701       <!-- boolean algebra of redexes -->
 702
 703       <!-- isomorphic -->
 704       <xsl:when test="$name='isomorphic'">
 705        <xsl:apply-templates select="*[2]" mode="inline"/>
 706        <xsl:choose>
 707        <xsl:when test="$uri != ''">
 708         <a href="{$uri}">
 709          <xsl:call-template name="mksymbol-1">
 710           <xsl:with-param name="symbol" select="$name"/>
 711           <xsl:with-param name="color" select="'green'"/>
 712           <xsl:with-param name="size" select="'+0'"/>
 713          </xsl:call-template>
 714         </a>
 715        </xsl:when>
 716        <xsl:otherwise>
 717          <xsl:call-template name="mksymbol-1">
 718           <xsl:with-param name="symbol" select="$name"/>
 719           <xsl:with-param name="color" select="'green'"/>
 720           <xsl:with-param name="size" select="'+0'"/>
 721          </xsl:call-template>
 722        </xsl:otherwise>
 723        </xsl:choose>
 724        <xsl:apply-templates select="*[3]" mode="inline"/>
 725       </xsl:when>
 726
 727       <!-- INTERP -->
 728       <xsl:when test="$name='interp'">
 729          <font color="green">[</font>
 730             <xsl:apply-templates select="*[2]"/>
 731          <font color="green">]</font>
 732       </xsl:when>
 733
 734    </xsl:choose>
 735 </xsl:template>
 736
 737 <xsl:template mode="inline" match="m:lambda">
 738       <xsl:call-template name="mksymbol-1">
 739        <xsl:with-param name="symbol" select="'lambda'"/>
 740        <xsl:with-param name="color" select="'red'"/>
 741        <xsl:with-param name="size" select="'+2'"/>
 742       </xsl:call-template>
 743       <xsl:apply-templates select="m:bvar/m:ci"/>
 744       <xsl:text>:</xsl:text>
 745       <xsl:apply-templates mode="inline" select="m:bvar/m:type"/>
 746       <xsl:text>.</xsl:text>
 747       <xsl:apply-templates mode="inline" select="*[position()=2]"/>
 748 </xsl:template>
 749
 750 <!--*********************************************************************-->
 751 <!--                       COUNTING MODE                                 -->
 752 <!--*********************************************************************-->
 753
 754 <xsl:template match="m:apply[m:csymbol]">
 755   <xsl:param name="current_indent" select="0"/>
 756   <xsl:param name="width" select="$framewidth"/>
 757   <xsl:variable name="name">
 758    <xsl:value-of select="m:csymbol"/>
 759   </xsl:variable>
 760   <xsl:variable name="charlength">
 761    <xsl:apply-templates select="m:csymbol" mode="charcount"/>
 762   </xsl:variable>
 763      <!-- <xsl:value-of select="$current_indent"/> -->
 764      <!-- <xsl:value-of select="$charlength"/> -->
 765   <xsl:variable name="uri"><xsl:value-of select="*[1]/@definitionURL"/></xsl:variable>
 766      <xsl:choose>
 767      <!-- FORALL -->
 768       <xsl:when test="$name='forall'">
 769        <xsl:choose>
 770        <xsl:when test="$charlength > $framewidth">
 771          <!-- &#x03a0; -->
 772          <xsl:call-template name="mksymbol-1">
 773           <xsl:with-param name="symbol" select="$name"/>
 774           <xsl:with-param name="color" select="'blue'"/>
 775           <xsl:with-param name="size" select="'+2'"/>
 776          </xsl:call-template>
 777          <xsl:apply-templates select="m:bvar/m:ci"/>
 778          <xsl:text>:</xsl:text>
 779          <xsl:apply-templates select="m:bvar/m:type">
 780           <xsl:with-param name="current_indent"
 781            select="$current_indent + 5 + 2*string-length(m:bvar/m:ci)"/>
 782          </xsl:apply-templates>
 783          <br/>
 784          <xsl:call-template name="make_indent">
 785           <xsl:with-param name="current_indent" select="$current_indent + 2"/>
 786          </xsl:call-template>
 787          <xsl:text>.</xsl:text>
 788          <xsl:apply-templates select="*[position()=3]">
 789           <xsl:with-param name="current_indent" select="$current_indent + 2"/>
 790          </xsl:apply-templates>
 791        </xsl:when>
 792        <xsl:otherwise>
 793         <xsl:apply-templates mode="inline" select="."/>
 794        </xsl:otherwise>
 795        </xsl:choose>
 796       </xsl:when>
 797       <!-- PROD -->
 798       <xsl:when test="$name='prod'">
 799        <xsl:choose>
 800        <xsl:when test="$charlength > $framewidth">
 801          <xsl:call-template name="mksymbol-1">
 802           <xsl:with-param name="symbol" select="$name"/>
 803           <xsl:with-param name="color" select="'blue'"/>
 804           <xsl:with-param name="size" select="'+2'"/>
 805          </xsl:call-template>
 806          <xsl:apply-templates select="m:bvar/m:ci"/>
 807          <xsl:text>:</xsl:text>
 808          <xsl:apply-templates select="m:bvar/m:type">
 809           <xsl:with-param name="current_indent"
 810            select="$current_indent + 5 + 2*string-length(m:bvar/m:ci)"/>
 811          </xsl:apply-templates><br/>
 812          <xsl:call-template name="make_indent">
 813           <xsl:with-param name="current_indent" select="$current_indent + 2"/>
 814          </xsl:call-template>
 815          <xsl:text>.</xsl:text>
 816          <xsl:apply-templates select="*[position()=3]">
 817           <xsl:with-param name="current_indent" select="$current_indent + 2"/>
 818          </xsl:apply-templates>
 819        </xsl:when>
 820        <xsl:otherwise>
 821         <xsl:apply-templates mode="inline" select="."/>
 822        </xsl:otherwise>
 823        </xsl:choose>
 824       </xsl:when>
 825       <!-- ARROW -->
 826       <xsl:when test="$name='arrow'">
 827        <xsl:choose>
 828        <xsl:when test="$charlength > $framewidth">
 829        <xsl:text>(</xsl:text>
 830        <xsl:apply-templates select="*[position()=2]">
 831         <xsl:with-param name="current_indent" select="$current_indent + 2"/>
 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        <!-- -> -->
 838        <xsl:call-template name="mksymbol-1">
 839         <xsl:with-param name="symbol" select="$name"/>
 840         <xsl:with-param name="color" select="'blue'"/>
 841         <xsl:with-param name="size" select="'+0'"/>
 842        </xsl:call-template>
 843        <xsl:apply-templates select="*[position()=3]">
 844         <xsl:with-param name="current_indent" select="$current_indent + 5"/>
 845        </xsl:apply-templates>
 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       <!-- APP -->
 854       <xsl:when test="$name='app'">
 855        <xsl:choose>
 856        <xsl:when test="$charlength  > $framewidth">
 857         <xsl:text>(</xsl:text>
 858         <xsl:apply-templates select="*[position()=2]">
 859          <xsl:with-param name="current_indent" select="$current_indent + 2"/>
 860         </xsl:apply-templates>
 861          <xsl:for-each select="*[position()>2]">
 862           <br/>
 863            <xsl:call-template name="make_indent">
 864             <xsl:with-param name="current_indent" select="$current_indent + 2"/>
 865            </xsl:call-template>
 866             <xsl:apply-templates select=".">
 867              <xsl:with-param name="current_indent" select="$current_indent + 2"/>
 868             </xsl:apply-templates>
 869          </xsl:for-each>
 870          <xsl:text>)</xsl:text>
 871        </xsl:when>
 872        <xsl:otherwise>
 873         <xsl:apply-templates mode="inline" select="."/>
 874        </xsl:otherwise>
 875        </xsl:choose>
 876       </xsl:when>
 877       <xsl:when test="$name='cast'">
 878        <xsl:choose>
 879         <xsl:when test="$showcast = 1">
 880          <xsl:choose>
 881           <xsl:when test="$charlength > $framewidth">
 882            <xsl:text>(</xsl:text>
 883            <xsl:apply-templates select="*[position()=2]">
 884             <xsl:with-param name="current_indent" select="$current_indent + 2"/>
 885            </xsl:apply-templates><br/>
 886            <xsl:call-template name="make_indent">
 887             <xsl:with-param name="current_indent" select="$current_indent + 2"/>          </xsl:call-template>
 888            <xsl:text>:></xsl:text>
 889            <xsl:apply-templates select="*[position()=3]">
 890             <xsl:with-param name="current_indent" select="$current_indent + 3"/>
 891            </xsl:apply-templates>
 892            <xsl:text>)</xsl:text>
 893           </xsl:when>
 894           <xsl:otherwise>
 895            <xsl:apply-templates mode="inline" select="."/>
 896           </xsl:otherwise>
 897          </xsl:choose>
 898         </xsl:when>
 899         <xsl:otherwise>
 900          <xsl:apply-templates select="*[position()=2]">
 901           <xsl:with-param name="current_indent" select="$current_indent"/>
 902          </xsl:apply-templates>
 903         </xsl:otherwise>
 904        </xsl:choose>
 905       </xsl:when>
 906       <xsl:when test="$name='Prop'">
 907        <xsl:text>Prop</xsl:text>
 908       </xsl:when>
 909       <xsl:when test="$name='Set'">
 910        <xsl:text>Set</xsl:text>
 911       </xsl:when>
 912       <xsl:when test="$name='Type'">
 913        <xsl:text>Type</xsl:text>
 914       </xsl:when>
 915       <xsl:when test="$name='mutcase'">
 916        <xsl:choose>
 917        <xsl:when test="$charlength > $framewidth">
 918          <xsl:text>&lt;</xsl:text>
 919          <xsl:apply-templates select="*[position()=2]">
 920           <xsl:with-param name="current_indent" select="$current_indent + 2"/>
 921          </xsl:apply-templates>
 922          <xsl:text>&gt; </xsl:text>
 923          <br/>
 924          <xsl:call-template name="make_indent">
 925           <xsl:with-param name="current_indent" select="$current_indent + 2"/>           </xsl:call-template>
 926          <xsl:text>CASE </xsl:text>
 927          <xsl:apply-templates select="*[position()=3]">
 928           <xsl:with-param name="current_indent" select="$current_indent + 8"/>
 929          </xsl:apply-templates>
 930          <xsl:text> OF </xsl:text>
 931          <xsl:for-each select="piecewise/piece">
 932     <!--   <xsl:for-each select="*[position() mod 2 = 0 and position()>3]">-->
 933          <br/>
 934          <xsl:call-template name="make_indent">
 935           <xsl:with-param name="current_indent" select="$current_indent + 2"/>
 936          </xsl:call-template>
 937             <xsl:choose>
 938             <xsl:when test="position() = 1">
 939              <xsl:text>&#x00A0;&#x00A0;</xsl:text>
 940             </xsl:when>
 941             <xsl:otherwise>
 942              <xsl:text>| </xsl:text>
 943             </xsl:otherwise>
 944             </xsl:choose>
 945           <xsl:apply-templates select="./*[2]"/>
 946             <xsl:call-template name="mksymbol-1">
 947              <xsl:with-param name="symbol" select="'RightArrow'"/>
 948              <xsl:with-param name="color" select="'green'"/>
 949              <xsl:with-param name="size" select="'+0'"/>
 950             </xsl:call-template>
 951             <xsl:variable name="body_size">
 952   <xsl:apply-templates
 953               select="./*[1]/*[1]" mode="charcount"/>
 954             </xsl:variable>
 955             <xsl:choose>
 956              <xsl:when test="$body_size > $framewidth">
 957               <br/>
 958               <xsl:call-template name="make_indent">
 959                <xsl:with-param name="current_indent"
 960                     select="$current_indent + 8"/>
 961               </xsl:call-template>
 962 <xsl:apply-templates
 963                    select="./*[1]">
 964               <xsl:with-param name="current_indent"
 965                    select="$current_indent + 8"/>
 966              </xsl:apply-templates>
 967             </xsl:when>
 968             <xsl:otherwise>
 969      <xsl:apply-templates select="./*[1]"
 970                    mode="inline" />
 971             </xsl:otherwise>
 972            </xsl:choose>
 973          </xsl:for-each>
 974        </xsl:when>
 975        <xsl:otherwise>
 976         <xsl:apply-templates mode="inline" select="."/>
 977        </xsl:otherwise>
 978        </xsl:choose>
 979       </xsl:when>
 980       <!-- FIX -->
 981       <xsl:when test="$name='fix'">
 982        <xsl:choose>
 983        <xsl:when test="$charlength  > $framewidth">
 984             <xsl:text>FIX</xsl:text>
 985             <xsl:value-of select="m:ci"/>
 986             <xsl:text>{</xsl:text>
 987             <xsl:for-each select="m:bvar">
 988               <br/>
 989               <xsl:call-template name="make_indent">
 990                <xsl:with-param name="current_indent" select="$current_indent + 2"/>
 991               </xsl:call-template>
 992               <xsl:value-of select="m:ci"/>
 993               <xsl:text>:</xsl:text>
 994               <xsl:apply-templates select="m:type">
 995                <xsl:with-param name="current_indent"
 996                     select="$current_indent + 5 + string-length(m:ci)"/>
 997                </xsl:apply-templates>
 998               <br/>
 999               <xsl:call-template name="make_indent">
1000                <xsl:with-param name="current_indent" select="$current_indent + 2"/>
1001               </xsl:call-template>
1002               <xsl:text>:=</xsl:text>
1003               <xsl:apply-templates select="following-sibling::*[position() = 1]">
1004                <xsl:with-param name="current_indent" select="$current_indent +2"/>
1005               </xsl:apply-templates>
1006             </xsl:for-each>
1007              <br/>
1008               <xsl:call-template name="make_indent">
1009                <xsl:with-param name="current_indent" select="$current_indent + 2"/>
1010               </xsl:call-template>
1011            <xsl:text>}</xsl:text>
1012        </xsl:when>
1013        <xsl:otherwise>
1014         <xsl:apply-templates mode="inline" select="."/>
1015        </xsl:otherwise>
1016        </xsl:choose>
1017       </xsl:when>
1018       <!-- COFIX -->
1019       <xsl:when test="$name='cofix'">
1020        <xsl:choose>
1021        <xsl:when test="($charlength + 10) > $framewidth">
1022             <xsl:text>COFIX</xsl:text>
1023             <xsl:value-of select="m:ci"/>
1024             <xsl:text>{</xsl:text>
1025             <br/>
1026             <xsl:call-template name="make_indent">
1027              <xsl:with-param name="current_indent" select="$current_indent + 2"/>
1028             </xsl:call-template>
1029             <xsl:for-each select="m:bvar">
1030                 <xsl:value-of select="m:ci"/>
1031                 <xsl:text>:</xsl:text>
1032                 <xsl:apply-templates select="m:type">
1033                  <xsl:with-param name="current_indent"
1034                     select="$current_indent + 5 + string-length(m:ci)"/>
1035                 </xsl:apply-templates>
1036                 <br/>
1037                 <xsl:call-template name="make_indent">
1038                  <xsl:with-param name="current_indent" select="$current_indent + 2"/>
1039                 </xsl:call-template>
1040                 <xsl:text>:=</xsl:text>
1041                 <xsl:apply-templates select="following-sibling::*[position() = 1]">
1042                  <xsl:with-param name="current_indent" select="$current_indent + 3"/>
1043                 </xsl:apply-templates>
1044
1045             </xsl:for-each>
1046             <br/>
1047               <xsl:call-template name="make_indent">
1048                <xsl:with-param name="current_indent" select="$current_indent + 2"/>
1049               </xsl:call-template>
1050             <xsl:text>}</xsl:text>
1051        </xsl:when>
1052        <xsl:otherwise>
1053         <xsl:apply-templates mode="inline" select="m:type"/>
1054        </xsl:otherwise>
1055        </xsl:choose>
1056       </xsl:when>
1057       <xsl:when test="$name='let_in'">
1058        <xsl:text>let&#x00a0;</xsl:text>
1059        <xsl:apply-templates select="m:bvar/m:ci"/>
1060        <xsl:text>&#x00a0;:=&#x00a0;</xsl:text>
1061        <xsl:apply-templates select="*[3]">
1062         <xsl:with-param name="current_indent" select="$current_indent+14"/>
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>in&#x00a0;</xsl:text>
1069        <xsl:apply-templates select="*[4]">
1070         <xsl:with-param name="current_indent" select="$current_indent+5"/>
1071        </xsl:apply-templates>
1072       </xsl:when>
1073
1074       <!-- ***************************************** -->
1075       <!-- *********** PROOF ELEMENTS ************** -->
1076       <!-- ***************************************** -->
1077       <!-- PROOF -->
1078       <xsl:when test="$name='proof'">
1079        <xsl:variable name="nonce" select="generate-id()"/>
1080        <xsl:variable name="freshid1" select="concat('a',$nonce)"/>
1081        <xsl:variable name="freshid2" select="concat('b',$nonce)"/>
1082        <xsl:variable name="freshid3" select="concat('c',$nonce)"/>
1083        <span ID="{$freshid1}">
1084         <xsl:apply-templates select="*[position()=2]">
1085          <xsl:with-param name="current_indent" select="$current_indent"/>
1086         </xsl:apply-templates>
1087         &#x00a0;
1088        </span>
1089        <xsl:choose>
1090         <xsl:when test="(preceding-sibling::*[1]/text()='letin1') or
1091                         (preceding-sibling::*[1]/text()='rw_step') or
1092                         (name(..)='m:lambda')">
1093          <br/>
1094          <xsl:call-template name="make_indent">
1095           <xsl:with-param name="current_indent" select="$current_indent"/>
1096          </xsl:call-template>
1097          <FONT color="red">we proved&#x00a0;</FONT>
1098         </xsl:when>
1099         <xsl:otherwise>
1100          <script>
1101           if(document.getElementById) {
1102            document.write('\
1103             <span ID="{$freshid2}">\
1104              <a style="text-decoration:underline ; color:green" href="" onClick="Show(document.getElementById(\'{$freshid1}\')); Hide(document.getElementById(\'{$freshid2}\'));Show(document.getElementById(\'{$freshid3}\'));return (0==1);">Proof of</a>\
1105             </span>\
1106             <span ID="{$freshid3}">\
1107              <br/>\
1108              <xsl:call-template name="make_indent">
1109               <xsl:with-param name="current_indent" select="$current_indent"/>
1110              </xsl:call-template>\
1111              <a style="text-decoration:underline ; color:red" href="" onClick="Hide(document.getElementById(\'{$freshid1}\')); Show(document.getElementById(\'{$freshid2}\'));Hide(document.getElementById(\'{$freshid3}\'));return (0==1);">we proved</a>\
1112             </span>\
1113            ');
1114            document.to_be_deleted.push('<xsl:value-of select="$freshid1"/>');
1115            document.to_be_deleted.push('<xsl:value-of select="$freshid3"/>');
1116            document.write('&#x00a0;');
1117           } else {
1118            document.write('\
1119             <br/>\
1120             <xsl:call-template name="make_indent">
1121              <xsl:with-param name="current_indent" select="$current_indent"/>
1122             </xsl:call-template>\
1123             <FONT color="red">we proved&#x00a0;</FONT>\
1124            ');
1125           }
1126          </script>
1127         </xsl:otherwise>
1128        </xsl:choose>
1129        <xsl:apply-templates select="*[position()=3]">
1130         <xsl:with-param name="current_indent" select="$current_indent + 16"/>
1131        </xsl:apply-templates>
1132       </xsl:when>
1133       <!-- side_proof -->
1134       <xsl:when test="$name='side_proof'">
1135        <xsl:variable name="nonce" select="generate-id()"/>
1136        <xsl:variable name="freshid1" select="concat('a',$nonce)"/>
1137        <xsl:variable name="freshid2" select="concat('b',$nonce)"/>
1138        <xsl:variable name="freshid3" select="concat('c',$nonce)"/>
1139        <xsl:variable name="freshid4" select="concat('d',$nonce)"/>
1140        <span ID="{$freshid1}">
1141         <xsl:apply-templates select="*[position()=2]">
1142          <xsl:with-param name="current_indent" select="$current_indent"/>
1143         </xsl:apply-templates>
1144         &#x00a0;
1145        </span>
1146          <script>
1147           if(document.getElementById) {
1148            document.write('\
1149             <span ID="{$freshid2}">\
1150              <a style="text-decoration:underline ; color:green" href="" onClick="Show(document.getElementById(\'{$freshid1}\')); Hide(document.getElementById(\'{$freshid2}\'));Show(document.getElementById(\'{$freshid3}\'));Show(document.getElementById(\'{$freshid4}\'));return (0==1);">Justification</a>\
1151             </span>\
1152             <span ID="{$freshid3}">\
1153              <br/>\
1154              <xsl:call-template name="make_indent">
1155               <xsl:with-param name="current_indent" select="$current_indent"/>
1156              </xsl:call-template>\
1157              <a style="text-decoration:underline ; color:red" href="" onClick="Hide(document.getElementById(\'{$freshid1}\')); Show(document.getElementById(\'{$freshid2}\'));Hide(document.getElementById(\'{$freshid3}\'));Hide(document.getElementById(\'{$freshid4}\'));return (0==1);">we proved</a>\
1158             </span>\
1159            ');
1160            document.to_be_deleted.push('<xsl:value-of select="$freshid1"/>');
1161            document.to_be_deleted.push('<xsl:value-of select="$freshid3"/>');
1162            document.to_be_deleted.push('<xsl:value-of select="$freshid4"/>');
1163            document.write('&#x00a0;');
1164           } else {
1165            document.write('\
1166             <br/>\
1167             <xsl:call-template name="make_indent">
1168              <xsl:with-param name="current_indent" select="$current_indent"/>
1169             </xsl:call-template>\
1170             <FONT color="red">we proved&#x00a0;</FONT>\
1171            ');
1172           }
1173          </script>
1174        <span ID="{$freshid4}">
1175         <xsl:apply-templates select="*[position()=3]">
1176          <xsl:with-param name="current_indent" select="$current_indent + 16"/>
1177         </xsl:apply-templates>
1178        </span>
1179       </xsl:when>
1180       <!-- eq_chain -->
1181       <xsl:when test="$name='eq_chain'">
1182        <FONT color="red">We have the following equality chain:</FONT>
1183        <xsl:for-each select="*[position() mod 2 = 0]">
1184         <xsl:variable name="pos" select="position()"/>
1185         <br/>
1186         <xsl:call-template name="make_indent">
1187          <xsl:with-param name="current_indent" select="$current_indent + 5"/>
1188         </xsl:call-template>
1189         <xsl:choose>
1190          <xsl:when test="$pos=1">
1191           <xsl:apply-templates select=".">
1192            <xsl:with-param name="current_indent" select="$current_indent + 5"/>
1193           </xsl:apply-templates>
1194           <xsl:text>&#x00a0;=</xsl:text>
1195          </xsl:when>
1196          <xsl:otherwise>
1197           <xsl:text>=&#x00a0;</xsl:text>
1198           <xsl:apply-templates select=".">
1199            <xsl:with-param name="current_indent" select="$current_indent + 5"/>
1200           </xsl:apply-templates>
1201          </xsl:otherwise>
1202         </xsl:choose>
1203         <xsl:if test="$pos != last()">
1204          <br/>
1205          <xsl:call-template name="make_indent">
1206           <xsl:with-param name="current_indent" select="$current_indent + 15"/>
1207          </xsl:call-template>
1208          <xsl:apply-templates select="../*[position()=2*$pos +1]">
1209           <xsl:with-param name="current_indent" select="$current_indent + 15"/>
1210          </xsl:apply-templates>
1211         </xsl:if>
1212        </xsl:for-each>
1213       </xsl:when>
1214        <!-- diseq_chain -->
1215       <xsl:when test="$name='diseq_chain'">
1216        <FONT color="red">We have the following chain of disequalities:</FONT>
1217        <xsl:for-each select="*[position() mod 3 = 2]">
1218         <xsl:variable name="pos" select="position()"/>
1219         <br/>
1220         <xsl:call-template name="make_indent">
1221          <xsl:with-param name="current_indent" select="$current_indent + 5"/>
1222         </xsl:call-template>
1223         <xsl:choose>
1224          <xsl:when test="$pos=1">
1225           <xsl:apply-templates select=".">
1226            <xsl:with-param name="current_indent" select="$current_indent + 5"/>
1227           </xsl:apply-templates>
1228           <xsl:text>&#x00a0;</xsl:text>
1229           <xsl:apply-templates mode="inline" select="../*[position()=3*$pos]"/>
1230          </xsl:when>
1231          <xsl:otherwise>
1232           <xsl:apply-templates mode="inline" select="../*[position()=3*($pos - 1)]"/>
1233           <xsl:text>&#x00a0;</xsl:text>
1234           <xsl:apply-templates select=".">
1235            <xsl:with-param name="current_indent" select="$current_indent + 5"/>
1236           </xsl:apply-templates>
1237          </xsl:otherwise>
1238         </xsl:choose>
1239         <xsl:if test="$pos != last()">
1240          <br/>
1241          <xsl:call-template name="make_indent">
1242           <xsl:with-param name="current_indent" select="$current_indent + 15"/>
1243          </xsl:call-template>
1244          <xsl:apply-templates select="../*[position()=3*$pos +1]">
1245           <xsl:with-param name="current_indent" select="$current_indent + 15"/>
1246          </xsl:apply-templates>
1247         </xsl:if>
1248        </xsl:for-each>
1249       </xsl:when>
1250       <!-- letin1 -->
1251       <xsl:when test="$name='letin1'">
1252        <xsl:apply-templates select="*[position()=2]">
1253         <xsl:with-param name="current_indent" select="$current_indent"/>
1254        </xsl:apply-templates>
1255        <br/>
1256        <xsl:call-template name="make_indent">
1257         <xsl:with-param name="current_indent" select="$current_indent"/>
1258        </xsl:call-template>
1259        <xsl:apply-templates select="*[position()=3]">
1260         <xsl:with-param name="current_indent" select="$current_indent"/>
1261        </xsl:apply-templates>
1262       </xsl:when>
1263       <!-- letin -->
1264       <xsl:when test="$name='letin'">
1265        <xsl:for-each select="*[position()>1 and last()>position()]">
1266         <xsl:apply-templates select=".">
1267          <xsl:with-param name="current_indent" select="$current_indent"/>
1268         </xsl:apply-templates>
1269         <br/>
1270         <xsl:call-template name="make_indent">
1271          <xsl:with-param name="current_indent" select="$current_indent"/>
1272         </xsl:call-template>
1273        </xsl:for-each>
1274        <xsl:apply-templates select="*[position()=last()]">
1275         <xsl:with-param name="current_indent" select="$current_indent"/>
1276        </xsl:apply-templates>
1277       </xsl:when>
1278       <!-- Let -->
1279       <xsl:when test="$name='let'">
1280        (
1281        <xsl:apply-templates select="m:ci"/>
1282        )
1283        <xsl:apply-templates select="*[3]">
1284         <xsl:with-param name="current_indent" select="$current_indent + 7"/>
1285        </xsl:apply-templates>
1286       </xsl:when>
1287       <!-- rw_step -->
1288       <xsl:when test="$name='rw_step'">
1289        <xsl:choose>
1290         <xsl:when test="name(*[2])='m:apply'">
1291          <xsl:apply-templates select="*[2]">
1292           <xsl:with-param name="current_indent" select="$current_indent"/>
1293          </xsl:apply-templates>
1294         </xsl:when>
1295         <xsl:otherwise>
1296          <FONT color="red">Consider&#x00a0;</FONT>
1297          <xsl:apply-templates select="*[2]"/>
1298         </xsl:otherwise>
1299        </xsl:choose>
1300        <xsl:variable name="charlength_first">
1301         <xsl:apply-templates select="*[3]" mode="root_charcount"/>
1302        </xsl:variable>
1303        <xsl:variable name="charlength_second">
1304         <xsl:apply-templates select="*[4]" mode="root_charcount"/>
1305        </xsl:variable>
1306        <xsl:variable name="charlength_side_proof">
1307         <xsl:apply-templates select="*[5]" mode="root_charcount"/>
1308        </xsl:variable>
1309        <xsl:variable name="split1"
1310          select="($charlength_first + $charlength_second) > $framewidth"/>
1311        <xsl:variable name="split2"
1312          select="($charlength_second + $charlength_side_proof) > $framewidth"/>
1313      <!-- <xsl:value-of select="$current_indent"/> -->
1314      <!-- <xsl:value-of select="string($charlength_second)"/>  -->
1315      <!-- <xsl:value-of select="$charlength_side_proof"/>  -->
1316      <!-- <xsl:value-of select="$split2"/>  -->
1317        <br/>
1318        <xsl:call-template name="make_indent">
1319         <xsl:with-param name="current_indent" select="$current_indent"/>
1320        </xsl:call-template>
1321        <FONT color="red">Rewrite&#x00a0;</FONT>
1322        <xsl:apply-templates mode="inline" select="*[3]"/>
1323        <xsl:text>&#x00a0;</xsl:text>
1324        <xsl:if test="$split1">
1325        <br/>
1326        <xsl:call-template name="make_indent">
1327         <xsl:with-param name="current_indent" select="$current_indent + 2"/>
1328        </xsl:call-template>
1329        </xsl:if>
1330        <FONT color="red">with&#x00a0;</FONT>
1331        <xsl:apply-templates mode="inline" select="*[4]"/>
1332        <xsl:text>&#x00a0;</xsl:text>
1333        <xsl:if test="$split2">
1334        <br/>
1335        <xsl:call-template name="make_indent">
1336         <xsl:with-param name="current_indent" select="$current_indent + 2"/>
1337        </xsl:call-template>
1338        </xsl:if>
1339        <FONT color="red">by&#x00a0;</FONT>
1340        <xsl:apply-templates select="*[5]">
1341         <xsl:with-param name="current_indent" select="$current_indent+7"/>
1342        </xsl:apply-templates>
1343       </xsl:when>
1344       <!-- rewrite and apply -->
1345       <xsl:when test="$name='rewrite_and_apply'">
1346        <xsl:apply-templates select="*[2]">
1347         <xsl:with-param name="current_indent" select="$current_indent"/>
1348        </xsl:apply-templates>
1349        <br/>
1350        <xsl:call-template name="make_indent">
1351         <xsl:with-param name="current_indent" select="$current_indent"/>
1352        </xsl:call-template>
1353        <FONT color="red">Then apply it to&#x00a0;</FONT>
1354        <xsl:apply-templates select="*[position()>2]"/>
1355       </xsl:when>
1356       <!-- by_induction -->
1357       <xsl:when test="$name='by_induction'">
1358        <FONT color="red">We prove&#x00a0;</FONT>
1359        <xsl:apply-templates select="../*[3]">
1360         <xsl:with-param name="current_indent" select="$current_indent+18"/>
1361        </xsl:apply-templates>
1362        <br/>
1363        <xsl:call-template name="make_indent">
1364         <xsl:with-param name="current_indent" select="$current_indent"/>
1365        </xsl:call-template>
1366        <FONT color="red">by induction on&#x00a0;</FONT>
1367        <xsl:apply-templates select="*[position()=last()]/*[position()=last()]">
1368         <xsl:with-param name="current_indent" select="$current_indent+30"/>
1369        </xsl:apply-templates>
1370        <!--
1371        <br/>
1372        <xsl:call-template name="make_indent">
1373         <xsl:with-param name="current_indent" select="$current_indent"/>
1374        </xsl:call-template>
1375        <xsl:text>The induction property is</xsl:text>
1376        <br/>
1377        <xsl:call-template name="make_indent">
1378         <xsl:with-param name="current_indent" select="$current_indent"/>
1379        </xsl:call-template>
1380        <xsl:apply-templates select="*[3]">
1381         <xsl:with-param name="current_indent" select="$current_indent"/>
1382        </xsl:apply-templates>
1383        -->
1384        <xsl:apply-templates
1385             select="*[position()>3 and not(position()=last())]">
1386         <xsl:with-param name="current_indent" select="$current_indent+4"/>
1387        </xsl:apply-templates>
1388        <!-- <br/>
1389        <xsl:call-template name="make_indent">
1390         <xsl:with-param name="current_indent" select="$current_indent"/>
1391        </xsl:call-template>
1392        <xsl:text>End induction</xsl:text> -->
1393       </xsl:when>
1394       <!-- inductive_case -->
1395       <xsl:when test="$name='inductive_case'">
1396        <br/>
1397        <xsl:call-template name="make_indent">
1398         <xsl:with-param name="current_indent" select="$current_indent"/>
1399        </xsl:call-template>
1400        <FONT color="red">Case&#x00a0;</FONT>
1401        <xsl:apply-templates select="*[2]">
1402         <xsl:with-param name="current_indent" select="$current_indent +10"/>
1403        </xsl:apply-templates>
1404        <xsl:if test="*[3]/*[position()>1]">
1405         <br/>
1406         <xsl:call-template name="make_indent">
1407          <xsl:with-param name="current_indent" select="$current_indent+4"/>
1408         </xsl:call-template>
1409         <FONT color="red">By induction hypothesis, we have:</FONT>
1410         <xsl:for-each select="*[3]/*[position()>1]">
1411          <br/>
1412          <xsl:call-template name="make_indent">
1413           <xsl:with-param name="current_indent" select="$current_indent + 4"/>
1414          </xsl:call-template>
1415          <xsl:text>(</xsl:text>
1416          <xsl:apply-templates select="m:ci"/>
1417          <xsl:text>)&#x00a0;</xsl:text>
1418          <xsl:apply-templates select="m:type">
1419           <xsl:with-param name="current_indent" select="$current_indent + 8"/>
1420          </xsl:apply-templates>
1421         </xsl:for-each>
1422        </xsl:if>
1423        <br/>
1424         <xsl:call-template name="make_indent">
1425          <xsl:with-param name="current_indent" select="$current_indent + 4"/>
1426         </xsl:call-template>
1427        <xsl:apply-templates select="*[4]">
1428         <xsl:with-param name="current_indent" select="$current_indent +4"/>
1429        </xsl:apply-templates>
1430        <!-- <br/>
1431        <xsl:call-template name="make_indent">
1432         <xsl:with-param name="current_indent" select="$current_indent"/>
1433        </xsl:call-template>
1434        <xsl:text>End Case</xsl:text> -->
1435       </xsl:when>
1436       <!-- case_lhs  -->
1437       <xsl:when test="$name='case_lhs'">
1438        <xsl:choose>
1439         <xsl:when test="count(*)=2">
1440          <xsl:apply-templates mode="inline" select="*[2]"/>
1441         </xsl:when>
1442         <xsl:otherwise>
1443          <xsl:text>(</xsl:text>
1444          <xsl:apply-templates mode="inline" select="*[2]"/>
1445          <xsl:for-each select="m:bvar">
1446           <xsl:text>&#x00a0;</xsl:text>
1447           <xsl:apply-templates mode="inline" select="*[1]"/>
1448           <xsl:text>:</xsl:text>
1449           <xsl:apply-templates mode="inline" select="m:type/*[1]"/>
1450          </xsl:for-each>
1451          <xsl:text>)</xsl:text>
1452         </xsl:otherwise>
1453        </xsl:choose>
1454       </xsl:when>
1455       <!-- false_ind -->
1456       <xsl:when test="$name='false_ind'">
1457        <xsl:apply-templates select="*[3]">
1458         <xsl:with-param name="current_indent" select="$current_indent"/>
1459        </xsl:apply-templates>
1460        <br/>
1461        <xsl:call-template name="make_indent">
1462         <xsl:with-param name="current_indent" select="$current_indent"/>
1463        </xsl:call-template>
1464        <FONT color="red">Contradiction.</FONT>
1465       </xsl:when>
1466       <!-- and_ind -->
1467       <xsl:when test="$name='and_ind'">
1468        <xsl:choose>
1469         <xsl:when test="name(*[2])='m:apply'">
1470          <xsl:apply-templates select="*[2]">
1471           <xsl:with-param name="current_indent" select="$current_indent"/>
1472          </xsl:apply-templates>
1473         </xsl:when>
1474         <xsl:otherwise>
1475          <FONT color="red">Consider&#x00a0;</FONT>
1476          <xsl:apply-templates select="*[2]"/>
1477         </xsl:otherwise>
1478        </xsl:choose>
1479        <br/>
1480        <xsl:call-template name="make_indent">
1481         <xsl:with-param name="current_indent" select="$current_indent"/>
1482        </xsl:call-template>
1483        <FONT color="red">In particular, we have</FONT>
1484        <br/>
1485        <xsl:call-template name="make_indent">
1486         <xsl:with-param name="current_indent" select="$current_indent"/>
1487        </xsl:call-template>
1488        (
1489        <xsl:apply-templates select="*[3]"/>
1490        )&#x00a0;
1491        <xsl:apply-templates select="*[4]">
1492         <xsl:with-param name="current_indent" select="$current_indent + 9"/>
1493        </xsl:apply-templates>
1494        <br/>
1495        <xsl:call-template name="make_indent">
1496         <xsl:with-param name="current_indent" select="$current_indent"/>
1497        </xsl:call-template>
1498        (
1499        <xsl:apply-templates select="*[5]"/>
1500        )&#x00a0;
1501        <xsl:apply-templates select="*[6]">
1502         <xsl:with-param name="current_indent" select="$current_indent + 9"/>
1503        </xsl:apply-templates>
1504        <br/>
1505        <xsl:call-template name="make_indent">
1506         <xsl:with-param name="current_indent" select="$current_indent"/>
1507        </xsl:call-template>
1508        <xsl:apply-templates select="*[7]">
1509         <xsl:with-param name="current_indent" select="$current_indent"/>
1510        </xsl:apply-templates>
1511       </xsl:when>
1512       <!-- full_or_ind -->
1513       <xsl:when test="$name='full_or_ind'">
1514        <xsl:choose>
1515         <xsl:when test="name(*[2])='m:apply'">
1516          <xsl:apply-templates select="*[2]">
1517           <xsl:with-param name="current_indent" select="$current_indent"/>
1518          </xsl:apply-templates>
1519         </xsl:when>
1520         <xsl:otherwise>
1521          <FONT color="red">Consider&#x00a0;</FONT>
1522          <xsl:apply-templates select="*[2]"/>
1523         </xsl:otherwise>
1524        </xsl:choose>
1525        <br/>
1526        <xsl:call-template name="make_indent">
1527         <xsl:with-param name="current_indent" select="$current_indent"/>
1528        </xsl:call-template>
1529        <FONT color="red">We proceed by cases to prove&#x00a0;</FONT>
1530        <xsl:apply-templates select="*[3]"/>
1531        <br/>
1532        <xsl:call-template name="make_indent">
1533         <xsl:with-param name="current_indent" select="$current_indent+4"/>
1534        </xsl:call-template>
1535        <FONT color="red">Left: suppose&#x00a0;</FONT>
1536        <xsl:text>(</xsl:text>
1537        <xsl:value-of select="*[4]/m:bvar/m:ci"/>
1538        <xsl:text>)&#x00a0;</xsl:text>
1539        <xsl:apply-templates
1540             select="*[4]/m:bvar/m:type/*[1]"/>
1541        <br/>
1542        <xsl:call-template name="make_indent">
1543         <xsl:with-param name="current_indent" select="$current_indent+15"/>
1544        </xsl:call-template>
1545        <xsl:apply-templates
1546             select="*[4]/*[3]">
1547         <xsl:with-param name="current_indent" select="$current_indent+15"/>
1548        </xsl:apply-templates>
1549        <br/>
1550        <xsl:call-template name="make_indent">
1551         <xsl:with-param name="current_indent" select="$current_indent+4"/>
1552        </xsl:call-template>
1553        <FONT color="red">Right: suppose&#x00a0;</FONT>
1554        <xsl:text>(</xsl:text>
1555        <xsl:value-of select="*[5]/m:bvar/m:ci"/>
1556        <xsl:text>)&#x00a0;</xsl:text>
1557        <xsl:apply-templates
1558             select="*[5]/m:bvar/m:type/*[1]"/>
1559        <br/>
1560        <xsl:call-template name="make_indent">
1561         <xsl:with-param name="current_indent" select="$current_indent+16"/>
1562        </xsl:call-template>
1563        <xsl:apply-templates
1564             select="*[5]/*[3]">
1565         <xsl:with-param name="current_indent" select="$current_indent+16"/>
1566        </xsl:apply-templates>
1567       </xsl:when>
1568       <!-- or_ind -->
1569       <xsl:when test="$name='or_ind'">
1570        <xsl:choose>
1571         <xsl:when test="name(*[2])='m:apply'">
1572          <xsl:apply-templates select="*[2]">
1573           <xsl:with-param name="current_indent" select="$current_indent"/>
1574          </xsl:apply-templates>
1575         </xsl:when>
1576         <xsl:otherwise>
1577          <FONT color="red">Consider&#x00a0;</FONT>
1578          <xsl:apply-templates select="*[2]"/>
1579         </xsl:otherwise>
1580        </xsl:choose>
1581        <br/>
1582        <xsl:call-template name="make_indent">
1583         <xsl:with-param name="current_indent" select="$current_indent"/>
1584        </xsl:call-template>
1585        <FONT color="red">We prove&#x00a0;</FONT>
1586        <xsl:apply-templates select="*[3]"/>
1587        <FONT color="red">&#x00a0;by cases:</FONT>
1588        <br/>
1589        <xsl:call-template name="make_indent">
1590         <xsl:with-param name="current_indent" select="$current_indent"/>
1591        </xsl:call-template>
1592        Left:&#x00a0;
1593        <xsl:apply-templates select="*[4]">
1594         <xsl:with-param name="current_indent" select="$current_indent"/>
1595        </xsl:apply-templates>
1596        <br/>
1597        <xsl:call-template name="make_indent">
1598         <xsl:with-param name="current_indent" select="$current_indent"/>
1599        </xsl:call-template>
1600        Right:&#x00a0;
1601        <xsl:apply-templates select="*[5]">
1602         <xsl:with-param name="current_indent" select="$current_indent"/>
1603        </xsl:apply-templates>
1604       </xsl:when>
1605       <!-- Ex_ind -->
1606       <xsl:when test="$name='ex_ind'">
1607        <xsl:choose>
1608         <xsl:when test="name(*[2])='m:apply'">
1609          <xsl:apply-templates select="*[2]">
1610           <xsl:with-param name="current_indent" select="$current_indent"/>
1611          </xsl:apply-templates>
1612         </xsl:when>
1613         <xsl:otherwise>
1614          <FONT color="red">Consider&#x00a0;</FONT>
1615          <xsl:apply-templates select="*[2]">
1616           <xsl:with-param name="current_indent" select="$current_indent"/>
1617          </xsl:apply-templates>
1618         </xsl:otherwise>
1619        </xsl:choose>
1620        <br/>
1621        <xsl:call-template name="make_indent">
1622         <xsl:with-param name="current_indent" select="$current_indent"/>
1623        </xsl:call-template>
1624        <FONT color="red">Let&#x00a0;</FONT>
1625        <xsl:apply-templates mode="inline" select="*[3]"/>
1626        :
1627        <xsl:apply-templates mode="inline" select="*[4]"/>
1628        <FONT color="red">&#x00a0;such that</FONT>
1629        <br/>
1630        <xsl:call-template name="make_indent">
1631         <xsl:with-param name="current_indent" select="$current_indent"/>
1632        </xsl:call-template>
1633        (
1634        <xsl:apply-templates mode="inline" select="*[5]"/>
1635        )
1636        <xsl:apply-templates select="*[6]">
1637         <xsl:with-param name="current_indent" select="$current_indent +7"/>
1638        </xsl:apply-templates>
1639        <br/>
1640        <xsl:call-template name="make_indent">
1641         <xsl:with-param name="current_indent" select="$current_indent"/>
1642        </xsl:call-template>
1643        <xsl:apply-templates select="*[7]">
1644         <xsl:with-param name="current_indent" select="$current_indent"/>
1645        </xsl:apply-templates>
1646       </xsl:when>
1647       <!-- ***************************************** -->
1648       <!-- *********** LAMBDA ELEMENTS ************** -->
1649       <!-- ***************************************** -->
1650       <xsl:when test="$name='subst'">
1651        <xsl:apply-templates select="*[3]"/>
1652        <xsl:text>[</xsl:text>
1653        <xsl:apply-templates select="*[4]"/>
1654        <xsl:choose>
1655        <xsl:when test="$uri != ''">
1656         <a href="{$uri}">
1657          <xsl:call-template name="mksymbol-1">
1658           <xsl:with-param name="symbol" select="$name"/>
1659           <xsl:with-param name="color" select="'blue'"/>
1660           <xsl:with-param name="size" select="'+0'"/>
1661          </xsl:call-template>
1662         </a>
1663        </xsl:when>
1664        <xsl:otherwise>
1665          <xsl:call-template name="mksymbol-1">
1666           <xsl:with-param name="symbol" select="$name"/>
1667           <xsl:with-param name="color" select="'blue'"/>
1668           <xsl:with-param name="size" select="'+0'"/>
1669          </xsl:call-template>
1670        </xsl:otherwise>
1671        </xsl:choose>
1672        <xsl:apply-templates select="*[2]"/>
1673        <xsl:text>]</xsl:text>
1674       </xsl:when>
1675
1676       <xsl:when test="$name='lift_with_base'">
1677        <SUB>
1678        <xsl:apply-templates select="*[3]" mode="inline"/>
1679        </SUB>
1680        <xsl:choose>
1681        <xsl:when test="$uri != ''">
1682         <a href="{$uri}">
1683          <xsl:call-template name="mksymbol-1">
1684           <xsl:with-param name="symbol" select="$name"/>
1685           <xsl:with-param name="color" select="'green'"/>
1686           <xsl:with-param name="size" select="'+0'"/>
1687          </xsl:call-template>
1688         </a>
1689        </xsl:when>
1690        <xsl:otherwise>
1691          <xsl:call-template name="mksymbol-1">
1692           <xsl:with-param name="symbol" select="$name"/>
1693           <xsl:with-param name="color" select="'green'"/>
1694           <xsl:with-param name="size" select="'+0'"/>
1695          </xsl:call-template>
1696        </xsl:otherwise>
1697        </xsl:choose>
1698        <SUP>
1699        <xsl:apply-templates select="*[4]" mode="inline"/>
1700        </SUP>
1701        <xsl:text>(</xsl:text>
1702        <xsl:apply-templates select="*[2]" mode="inline"/>
1703        <xsl:text>)</xsl:text>
1704       </xsl:when>
1705
1706       <xsl:when test="$name='lift'">
1707        <xsl:choose>
1708        <xsl:when test="$uri != ''">
1709         <a href="{$uri}">
1710          <xsl:call-template name="mksymbol-1">
1711           <xsl:with-param name="symbol" select="$name"/>
1712           <xsl:with-param name="color" select="'green'"/>
1713           <xsl:with-param name="size" select="'+0'"/>
1714          </xsl:call-template>
1715         </a>
1716        </xsl:when>
1717        <xsl:otherwise>
1718          <xsl:call-template name="mksymbol-1">
1719           <xsl:with-param name="symbol" select="$name"/>
1720           <xsl:with-param name="color" select="'green'"/>
1721           <xsl:with-param name="size" select="'+0'"/>
1722          </xsl:call-template>
1723        </xsl:otherwise>
1724        </xsl:choose>
1725        <SUP>
1726        <xsl:apply-templates select="*[2]" mode="inline"/>
1727        </SUP>
1728        <xsl:text>(</xsl:text>
1729        <xsl:apply-templates select="*[3]" mode="inline"/>
1730        <xsl:text>)</xsl:text>
1731       </xsl:when>
1732
1733       <!-- reduction -->
1734       <xsl:when test="$name='beta_red1'">
1735        <xsl:apply-templates select="*[2]" mode="inline"/>
1736        <xsl:choose>
1737        <xsl:when test="$uri != ''">
1738         <a href="{$uri}">
1739          <xsl:call-template name="mksymbol-1">
1740           <xsl:with-param name="symbol" select="$name"/>
1741           <xsl:with-param name="color" select="'green'"/>
1742           <xsl:with-param name="size" select="'+0'"/>
1743          </xsl:call-template>
1744          <SUB>
1745          <xsl:call-template name="mksymbol-1">
1746           <xsl:with-param name="symbol" select="'beta'"/>
1747           <xsl:with-param name="color" select="'green'"/>
1748           <xsl:with-param name="size" select="'+0'"/>
1749          </xsl:call-template>
1750          </SUB>
1751         </a>
1752        </xsl:when>
1753        <xsl:otherwise>
1754          <xsl:call-template name="mksymbol-1">
1755           <xsl:with-param name="symbol" select="$name"/>
1756           <xsl:with-param name="color" select="'green'"/>
1757           <xsl:with-param name="size" select="'+0'"/>
1758          </xsl:call-template>
1759          <SUB>
1760          <xsl:call-template name="mksymbol-1">
1761           <xsl:with-param name="symbol" select="'beta'"/>
1762           <xsl:with-param name="color" select="'green'"/>
1763           <xsl:with-param name="size" select="'+0'"/>
1764          </xsl:call-template>
1765          </SUB>
1766        </xsl:otherwise>
1767        </xsl:choose>
1768        <xsl:apply-templates select="*[3]" mode="inline"/>
1769       </xsl:when>
1770
1771       <xsl:when test="$name='beta_red'">
1772        <xsl:apply-templates select="*[2]" mode="inline"/>
1773        <xsl:choose>
1774        <xsl:when test="$uri != ''">
1775         <a href="{$uri}">
1776          <xsl:call-template name="mksymbol-1">
1777           <xsl:with-param name="symbol" select="$name"/>
1778           <xsl:with-param name="color" select="'green'"/>
1779           <xsl:with-param name="size" select="'+0'"/>
1780          </xsl:call-template>
1781          <SUB>
1782          <xsl:call-template name="mksymbol-1">
1783           <xsl:with-param name="symbol" select="'beta'"/>
1784           <xsl:with-param name="color" select="'green'"/>
1785           <xsl:with-param name="size" select="'+0'"/>
1786          </xsl:call-template>
1787          <xsl:text>*</xsl:text>
1788          </SUB>
1789         </a>
1790        </xsl:when>
1791        <xsl:otherwise>
1792          <xsl:call-template name="mksymbol-1">
1793           <xsl:with-param name="symbol" select="$name"/>
1794           <xsl:with-param name="color" select="'green'"/>
1795           <xsl:with-param name="size" select="'+0'"/>
1796          </xsl:call-template>
1797          <SUB>
1798          <xsl:call-template name="mksymbol-1">
1799           <xsl:with-param name="symbol" select="'beta'"/>
1800           <xsl:with-param name="color" select="'green'"/>
1801           <xsl:with-param name="size" select="'+0'"/>
1802          </xsl:call-template>
1803          <xsl:text>*</xsl:text>
1804          </SUB>
1805        </xsl:otherwise>
1806        </xsl:choose>
1807        <xsl:apply-templates select="*[3]" mode="inline"/>
1808       </xsl:when>
1809
1810       <xsl:when test="$name='par_beta_red1'">
1811        <xsl:apply-templates select="*[2]" mode="inline"/>
1812        <xsl:choose>
1813        <xsl:when test="$uri != ''">
1814         <a href="{$uri}">
1815          <xsl:call-template name="mksymbol-1">
1816           <xsl:with-param name="symbol" select="$name"/>
1817           <xsl:with-param name="color" select="'green'"/>
1818           <xsl:with-param name="size" select="'+0'"/>
1819          </xsl:call-template>
1820          <SUB>
1821          <xsl:call-template name="mksymbol-1">
1822           <xsl:with-param name="symbol" select="'beta'"/>
1823           <xsl:with-param name="color" select="'green'"/>
1824           <xsl:with-param name="size" select="'+0'"/>
1825          </xsl:call-template>
1826          </SUB>
1827         </a>
1828        </xsl:when>
1829        <xsl:otherwise>
1830          <xsl:call-template name="mksymbol-1">
1831           <xsl:with-param name="symbol" select="$name"/>
1832           <xsl:with-param name="color" select="'green'"/>
1833           <xsl:with-param name="size" select="'+0'"/>
1834          </xsl:call-template>
1835          <SUB>
1836          <xsl:call-template name="mksymbol-1">
1837           <xsl:with-param name="symbol" select="'beta'"/>
1838           <xsl:with-param name="color" select="'green'"/>
1839           <xsl:with-param name="size" select="'+0'"/>
1840          </xsl:call-template>
1841          </SUB>
1842        </xsl:otherwise>
1843        </xsl:choose>
1844        <xsl:apply-templates select="*[3]" mode="inline"/>
1845       </xsl:when>
1846
1847       <xsl:when test="$name='par_beta_red'">
1848        <xsl:apply-templates select="*[2]" mode="inline"/>
1849        <xsl:choose>
1850        <xsl:when test="$uri != ''">
1851         <a href="{$uri}">
1852          <xsl:call-template name="mksymbol-1">
1853           <xsl:with-param name="symbol" select="$name"/>
1854           <xsl:with-param name="color" select="'green'"/>
1855           <xsl:with-param name="size" select="'+0'"/>
1856          </xsl:call-template>
1857          <SUB>
1858          <xsl:call-template name="mksymbol-1">
1859           <xsl:with-param name="symbol" select="'beta'"/>
1860           <xsl:with-param name="color" select="'green'"/>
1861           <xsl:with-param name="size" select="'+0'"/>
1862          </xsl:call-template>
1863          <xsl:text>*</xsl:text>
1864          </SUB>
1865         </a>
1866        </xsl:when>
1867        <xsl:otherwise>
1868          <xsl:call-template name="mksymbol-1">
1869           <xsl:with-param name="symbol" select="$name"/>
1870           <xsl:with-param name="color" select="'green'"/>
1871           <xsl:with-param name="size" select="'+0'"/>
1872          </xsl:call-template>
1873          <SUB>
1874          <xsl:call-template name="mksymbol-1">
1875           <xsl:with-param name="symbol" select="'beta'"/>
1876           <xsl:with-param name="color" select="'green'"/>
1877           <xsl:with-param name="size" select="'+0'"/>
1878          </xsl:call-template>
1879          <xsl:text>*</xsl:text>
1880          </SUB>
1881        </xsl:otherwise>
1882        </xsl:choose>
1883        <xsl:apply-templates select="*[3]" mode="inline"/>
1884       </xsl:when>
1885
1886       <!-- forgetful -->
1887       <xsl:when test="$name='forgetful'">
1888        <xsl:choose>
1889        <xsl:when test="$uri != ''">
1890         <a href="{$uri}">|</a>
1891        </xsl:when>
1892        <xsl:otherwise>
1893         |
1894        </xsl:otherwise>
1895        </xsl:choose>
1896        <xsl:apply-templates select="*[2]" mode="inline"/>
1897        <xsl:choose>
1898        <xsl:when test="$uri != ''">
1899         <a href="{$uri}">|</a>
1900        </xsl:when>
1901        <xsl:otherwise>
1902         |
1903        </xsl:otherwise>
1904        </xsl:choose>
1905       </xsl:when>
1906
1907       <!-- boolean algebra of redexes -->
1908
1909       <!-- isomorphic -->
1910       <xsl:when test="$name='isomorphic'">
1911        <xsl:apply-templates select="*[2]" mode="inline"/>
1912        <xsl:choose>
1913        <xsl:when test="$uri != ''">
1914         <a href="{$uri}">
1915          <xsl:call-template name="mksymbol-1">
1916           <xsl:with-param name="symbol" select="$name"/>
1917           <xsl:with-param name="color" select="'green'"/>
1918           <xsl:with-param name="size" select="'+0'"/>
1919          </xsl:call-template>
1920         </a>
1921        </xsl:when>
1922        <xsl:otherwise>
1923          <xsl:call-template name="mksymbol-1">
1924           <xsl:with-param name="symbol" select="$name"/>
1925           <xsl:with-param name="color" select="'green'"/>
1926           <xsl:with-param name="size" select="'+0'"/>
1927          </xsl:call-template>
1928        </xsl:otherwise>
1929        </xsl:choose>
1930        <xsl:apply-templates select="*[3]" mode="inline"/>
1931       </xsl:when>
1932
1933       <!-- INTERP -->
1934       <xsl:when test="$name='interp'">
1935          <font color="green">[</font>
1936             <xsl:apply-templates select="*[2]"/>
1937          <font color="green">]</font>
1938       </xsl:when>
1939
1940      </xsl:choose>
1941 </xsl:template>
1942
1943 <!-- LAMBDA -->
1944
1945 <xsl:template match="m:lambda">
1946 <xsl:param name="current_indent" select="0"/>
1947     <xsl:variable name="charlength">
1948      <xsl:apply-templates select="*[position()=1]" mode="charcount"/>
1949      <!-- <xsl:apply-templates select="." mode="charcount"/> -->
1950     </xsl:variable>
1951     <!-- <xsl:value-of select="$charlength"/> -->
1952     <!-- <xsl:value-of select="$current_indent"/> -->
1953      <xsl:choose>
1954      <xsl:when test="$charlength > $framewidth">
1955        <!-- &#x03bb; -->
1956        <xsl:call-template name="mksymbol-1">
1957         <xsl:with-param name="symbol" select="'lambda'"/>
1958         <xsl:with-param name="color" select="'red'"/>
1959         <xsl:with-param name="size" select="'+2'"/>
1960        </xsl:call-template>
1961        <xsl:apply-templates select="m:bvar/m:ci"/>
1962        <xsl:text>:</xsl:text>
1963        <xsl:apply-templates select="m:bvar/m:type">
1964         <xsl:with-param name="current_indent"
1965            select="$current_indent + 4 + 2*string-length(m:bvar/m:ci)"/>
1966        </xsl:apply-templates><br/>
1967        <xsl:call-template name="make_indent">
1968         <xsl:with-param name="current_indent" select="$current_indent + 2"/>
1969        </xsl:call-template>
1970        <xsl:text>.</xsl:text>
1971        <xsl:apply-templates select="*[position()=2]">
1972         <xsl:with-param name="current_indent" select="$current_indent + 2"/>
1973        </xsl:apply-templates>
1974      </xsl:when>
1975      <xsl:otherwise>
1976       <xsl:apply-templates mode="inline" select="."/>
1977      </xsl:otherwise>
1978      </xsl:choose>
1979 </xsl:template>
1980
1981 <!-- href -->
1982 <xsl:template match="m:ci">
1983  <xsl:choose>
1984   <xsl:when test="boolean(@definitionURL)">
1985    <a href="{@definitionURL}">
1986    <xsl:apply-templates/>
1987    </a>
1988   </xsl:when>
1989   <xsl:otherwise>
1990    <xsl:value-of select="."/>
1991   </xsl:otherwise>
1992  </xsl:choose>
1993 </xsl:template>
1994
1995 <!-- CHAR COUNTING -->
1996
1997 <!-- enter this counting mode selecting the root -->
1998 <xsl:template match="*" mode="root_charcount">
1999 <xsl:param name="incurrent_length" select="0"/>
2000  <xsl:choose>
2001   <xsl:when test="count(*)=0">
2002    <xsl:value-of select="0"/>
2003   </xsl:when>
2004   <xsl:when test="name()='m:ci'">
2005    <xsl:value-of select="string-length()"/>
2006   </xsl:when>
2007   <xsl:otherwise>
2008    <xsl:apply-templates select="*[1]" mode="charcount">
2009     <xsl:with-param name="incurrent_length" select="$incurrent_length"/>
2010    </xsl:apply-templates>
2011   </xsl:otherwise>
2012  </xsl:choose>
2013 </xsl:template>
2014
2015 <!-- enter this mode selecting the first child -->
2016
2017 <xsl:template match="m:ci|m:csymbol" mode="charcount">
2018 <xsl:param name="incurrent_length" select="0"/>
2019     <xsl:choose>
2020     <xsl:when test="$framewidth >= ($incurrent_length + string-length())">
2021      <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>
2022      <xsl:choose>
2023      <xsl:when test="string($siblength) = &quot;&quot;">
2024       <xsl:value-of select="$incurrent_length + string-length()"/>
2025      </xsl:when>
2026      <xsl:otherwise>
2027       <xsl:value-of select="number($siblength)"/>
2028      </xsl:otherwise>
2029      </xsl:choose>
2030     </xsl:when>
2031     <xsl:otherwise>
2032      <xsl:value-of select="$incurrent_length + string-length()"/>
2033     </xsl:otherwise>
2034     </xsl:choose>
2035 </xsl:template>
2036
2037 <xsl:template match="*" mode="charcount">
2038  <xsl:param name="incurrent_length" select="0"/>
2039  <xsl:choose>
2040   <xsl:when test="count(child::*) = 0">
2041    <xsl:value-of select="$incurrent_length"/>
2042   </xsl:when>
2043   <xsl:otherwise>
2044     <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>
2045     <xsl:choose>
2046      <xsl:when test="$framewidth >= number($childlength)">
2047       <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>
2048       <xsl:choose>
2049        <xsl:when test="string($siblength) = &quot;&quot;">
2050         <xsl:value-of select="number($childlength)"/>
2051        </xsl:when>
2052        <xsl:otherwise>
2053         <xsl:value-of select="number($siblength)"/>
2054        </xsl:otherwise>
2055       </xsl:choose>
2056      </xsl:when>
2057      <xsl:otherwise>
2058       <xsl:value-of select="number($childlength)"/>
2059      </xsl:otherwise>
2060     </xsl:choose>
2061   </xsl:otherwise>
2062  </xsl:choose>
2063 </xsl:template>
2064
2065
2066 <!--***********************************************************************-->
2067 <!-- OBJECTS                                                               -->
2068 <!--***********************************************************************-->
2069
2070 <!-- DEFINITION -->
2071
2072 <xsl:template match="Definition">
2073 <xsl:param name="current_indent" select="0"/>
2074 <p>
2075 DEFINITION <xsl:value-of select="@name"/>(<xsl:if test="string(./Params) != &quot;&quot;"><xsl:value-of select="Params"/></xsl:if>)<br/>
2076 TYPE =<br/>
2077       <xsl:call-template name="make_indent">
2078        <xsl:with-param name="current_indent" select="$current_indent + 7"/>
2079       </xsl:call-template>
2080        <xsl:apply-templates select="type/*[1]">
2081         <xsl:with-param name="current_indent" select="$current_indent + 7"/>
2082        </xsl:apply-templates><br/>
2083 BODY =<br/>
2084       <xsl:call-template name="make_indent">
2085        <xsl:with-param name="current_indent" select="$current_indent + 7"/>
2086       </xsl:call-template>
2087        <xsl:apply-templates select="body/*[1]">
2088         <xsl:with-param name="current_indent" select="$current_indent + 7"/>
2089        </xsl:apply-templates>
2090 </p>
2091 </xsl:template>
2092
2093 <!-- AXIOM -->
2094
2095 <xsl:template match="Axiom">
2096 <xsl:param name="current_indent" select="0"/>
2097 <p>
2098 AXIOM <xsl:value-of select="@name"/>(<xsl:if test="string(./Params) != &quot;&quot;"><xsl:value-of select="Params"/></xsl:if>)<br/>
2099 TYPE =<br/>
2100       <xsl:call-template name="make_indent">
2101        <xsl:with-param name="current_indent" select="$current_indent + 7"/>
2102       </xsl:call-template>
2103 <xsl:apply-templates select="type/*[1]">
2104           <xsl:with-param name="current_indent" select="$current_indent + 7"/>
2105        </xsl:apply-templates>
2106 </p>
2107 </xsl:template>
2108
2109 <!-- UNFINISHED PROOF -->
2110
2111 <xsl:template match="CurrentProof">
2112 <xsl:param name="current_indent" select="0"/>
2113 <p>
2114 UNFINISHED PROOF <xsl:value-of select="@name"/>(<xsl:if test="string(./Params) != &quot;&quot;"><xsl:value-of select="Params"/></xsl:if>)<br/>
2115 THESIS:  <xsl:apply-templates select="type/*[1]">
2116           <xsl:with-param name="current_indent" select="$current_indent + 8"/>
2117          </xsl:apply-templates><br/>
2118 CONJECTURES:
2119       <xsl:for-each select="Conjecture">
2120       <br/>
2121       <xsl:call-template name="make_indent">
2122        <xsl:with-param name="current_indent" select="$current_indent + 8"/>
2123       </xsl:call-template>
2124       <xsl:for-each select="Decl|Def|Hidden">
2125        <xsl:choose>
2126         <xsl:when test="name(.)='Decl'">
2127          <xsl:choose>
2128           <xsl:when test="@name">
2129            <xsl:value-of select="@name"/>
2130           </xsl:when>
2131           <xsl:otherwise>
2132            <xsl:text>_</xsl:text>
2133           </xsl:otherwise>
2134          </xsl:choose>
2135          <xsl:text> : </xsl:text>
2136          <xsl:apply-templates select="./*[1]">
2137           <xsl:with-param name="current_indent" select="$current_indent"/>
2138          </xsl:apply-templates>
2139         </xsl:when>
2140         <xsl:when test="name(.)='Def'">
2141          <xsl:choose>
2142           <xsl:when test="@name">
2143            <xsl:value-of select="@name"/>
2144           </xsl:when>
2145           <xsl:otherwise>
2146            <xsl:text>_</xsl:text>
2147           </xsl:otherwise>
2148          </xsl:choose>
2149          <xsl:text> := </xsl:text>
2150          <xsl:apply-templates select="./*[1]">
2151           <xsl:with-param name="current_indent" select="$current_indent"/>
2152          </xsl:apply-templates>
2153         </xsl:when>
2154         <xsl:otherwise>
2155          <xsl:text> _ :? _ </xsl:text>
2156         </xsl:otherwise>
2157        </xsl:choose>
2158       </xsl:for-each>
2159       |- <xsl:value-of select="./@no"/> :
2160       <xsl:apply-templates select="./Goal/*[1]">
2161        <xsl:with-param name="current_indent" select="$current_indent + 11"/>
2162       </xsl:apply-templates>
2163       </xsl:for-each>
2164       <br/>
2165 PROOF:
2166       <xsl:apply-templates select="body/*[1]">
2167         <xsl:with-param name="current_indent" select="$current_indent + 8"/>
2168       </xsl:apply-templates>
2169 </p>
2170 </xsl:template>
2171
2172 <!-- MUTUAL INDUCTIVE DEFINITION -->
2173
2174 <xsl:template match="InductiveDefinition">
2175 <xsl:param name="current_indent" select="0"/>
2176 <p>
2177      <xsl:for-each select="InductiveType">
2178          <xsl:choose>
2179          <xsl:when test="position() = 1">
2180           <xsl:choose>
2181           <xsl:when test="string(./@inductive) = &quot;true&quot;">
2182           INDUCTIVE DEFINITION
2183           </xsl:when>
2184           <xsl:otherwise>
2185           COINDUCTIVE DEFINITION
2186           </xsl:otherwise>
2187           </xsl:choose>
2188          </xsl:when>
2189          <xsl:otherwise>
2190           AND
2191          </xsl:otherwise>
2192          </xsl:choose>
2193          <xsl:value-of select="./@name"/>(<xsl:if test="string(../Params) != &quot;&quot;"><xsl:value-of select="../Params"/></xsl:if>)
2194          [
2195           <xsl:if test="string(../Param) != &quot;&quot;">
2196            <xsl:for-each select="../Param">
2197             <xsl:value-of select="./@name"/>
2198             :
2199             <xsl:apply-templates select="*"/>
2200            </xsl:for-each>
2201           </xsl:if>
2202          ] <br/>
2203          OF ARITY
2204          <xsl:apply-templates select="./arity/*[1]">
2205           <xsl:with-param name="current_indent" select="$current_indent + 9"/>
2206          </xsl:apply-templates> <br/>
2207          BUILT FROM:
2208       <xsl:for-each select="./Constructor">
2209       <br/>
2210       <xsl:call-template name="make_indent">
2211        <xsl:with-param name="current_indent" select="$current_indent + 3"/>
2212       </xsl:call-template>
2213          <xsl:choose>
2214          <xsl:when test="position() = 1">
2215          <xsl:text>&#x00A0;&#x00A0;</xsl:text>
2216          </xsl:when>
2217          <xsl:otherwise>
2218          <xsl:text>| </xsl:text>
2219          </xsl:otherwise>
2220          </xsl:choose>
2221          <xsl:value-of select="./@name"/>
2222          <xsl:text>: </xsl:text>
2223          <xsl:apply-templates select="./*[1]">
2224           <xsl:with-param name="current_indent" select="$current_indent + 2*string-length(./@name) + 5"/>
2225          </xsl:apply-templates>
2226       </xsl:for-each>
2227      </xsl:for-each>
2228 </p>
2229 </xsl:template>
2230
2231 <!-- VARIABLE -->
2232
2233 <xsl:template match="Variable">
2234 <xsl:param name="current_indent" select="0"/>
2235 <p>
2236 VARIABLE <xsl:value-of select="@name"/><br/>
2237 TYPE = <xsl:apply-templates select="type/*[1]">
2238           <xsl:with-param name="current_indent" select="$current_indent + 7"/>
2239        </xsl:apply-templates>
2240 <xsl:if test="body">
2241 <br/>
2242 BODY = <xsl:apply-templates select="body/*[1]">
2243           <xsl:with-param name="current_indent" select="$current_indent + 7"/>
2244        </xsl:apply-templates>
2245 </xsl:if>
2246 </p>
2247 </xsl:template>
2248
2249 <!--***********************************************************************-->
2250 <!-- SECTIONS                                                              -->
2251 <!--***********************************************************************-->
2252
2253 <!-- SECTION -->
2254
2255 <xsl:template match="SECTION">
2256 <xsl:param name="current_indent" select="0"/>
2257  <h1>BEGIN OF SECTION</h1>
2258   <xsl:apply-templates/>
2259  <h1>END OF SECTION</h1>
2260 </xsl:template>
2261
2262 </xsl:stylesheet>