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