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