helm/style/content_to_html.xsl

   1 <?xml version="1.0"?>
   2
   3 <!-- Copyright (C) 2000, HELM Team                                     -->
   4 <!--                                                                   -->
   5 <!-- This file is part of HELM, an Hypertextual, Electronic            -->
   6 <!-- Library of Mathematics, developed at the Computer Science         -->
   7 <!-- Department, University of Bologna, Italy.                         -->
   8 <!--                                                                   -->
   9 <!-- HELM is free software; you can redistribute it and/or             -->
  10 <!-- modify it under the terms of the GNU General Public License       -->
  11 <!-- as published by the Free Software Foundation; either version 2    -->
  12 <!-- of the License, or (at your option) any later version.            -->
  13 <!--                                                                   -->
  14 <!-- HELM is distributed in the hope that it will be useful,           -->
  15 <!-- but WITHOUT ANY WARRANTY; without even the implied warranty of    -->
  16 <!-- MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE.  See the     -->
  17 <!-- GNU General Public License for more details.                      -->
  18 <!--                                                                   -->
  19 <!-- You should have received a copy of the GNU General Public License -->
  20 <!-- along with HELM; if not, write to the Free Software               -->
  21 <!-- Foundation, Inc., 59 Temple Place - Suite 330, Boston,            -->
  22 <!-- MA  02111-1307, USA.                                              -->
  23 <!--                                                                   -->
  24 <!-- For details, see the HELM World-Wide-Web page,                    -->
  25 <!-- http://cs.unibo.it/helm/.                                         -->
  26
  27 <xsl:stylesheet version="1.0" xmlns:xsl="http://www.w3.org/1999/XSL/Transform"
  28                               xmlns:m="http://www.w3.org/1998/Math/MathML">
  29
  30 <!--***********************************************************************-->
  31 <!-- From MathML content to HTML                                           -->
  32 <!-- HELM Group: Asperti, Padovani, Sacerdoti, Schena, Guidi               -->
  33 <!--***********************************************************************-->
  34
  35 <xsl:param name="CICURI" select="''"/>
  36 <xsl:param name="type" select="'standalone'"/>
  37 <xsl:param name="UNICODEvsSYMBOL" select="'symbol'"/>
  38
  39 <xsl:include href="html_init.xsl"/>
  40 <xsl:include href="html_set.xsl"/>
  41 <xsl:include href="html_reals.xsl"/>
  42
  43 <xsl:variable name="showcast" select="0"/>
  44
  45 <!--***********************************************************************-->
  46 <!-- HTML Head and Body                                                    -->
  47 <!--***********************************************************************-->
  48
  49 <!-- <xsl:output method="html" encoding="iso-8859-1"/> -->
  50
  51 <!-- document needs method="xml" and searches locally for the dtd if        -->
  52 <!-- doctype-system is specified (the dtd must exist locally for parsing).  -->
  53 <!-- For having output html must be media-type="html" and for having the    -->
  54 <!-- correct <br /> you must specify at least the remote dtd by means of    -->
  55 <!-- doctype-public                                                         -->
  56 <xsl:output
  57         method="xml"
  58         encoding="iso-8859-1"
  59         media-type="text/html"
  60         doctype-public="-//W3C//DTD XHTML 1.0 Transitional//EN" />
  61
  62 <xsl:variable name="framewidth" select="45"/>
  63
  64 <xsl:template name="mksymbol-1">
  65  <xsl:param name="symbol" select="''"/>
  66  <xsl:param name="color" select="''"/>
  67  <xsl:param name="size" select="''"/>
  68   <xsl:choose>
  69    <xsl:when test="$UNICODEvsSYMBOL = 'symbol'">
  70     <xsl:variable name="fontsymbol">
  71      <xsl:choose>
  72       <xsl:when test="$symbol = 'forall'">
  73        <xsl:value-of select="'&#x22;'"/>
  74       </xsl:when>
  75       <xsl:when test="$symbol = 'lambda'">
  76        <xsl:value-of select="'l'"/>
  77       </xsl:when>
  78       <xsl:when test="$symbol = 'prod'">
  79        <xsl:value-of select="'&#x00d5;'"/>
  80       </xsl:when>
  81       <xsl:when test="$symbol = 'arrow'">
  82        <xsl:value-of select="'&#x00ae;'"/>
  83       </xsl:when>
  84       <xsl:when test="$symbol = 'RightArrow'">
  85        <xsl:value-of select="'&#222;'"/>
  86       </xsl:when>
  87       <xsl:when test="$symbol = 'subst'">
  88        <xsl:value-of select="'&#x00ac;'"/>
  89       </xsl:when>
  90       <xsl:when test="$symbol = 'lift' or $symbol = 'lift_with_base'">
  91        <xsl:value-of select="'&#x00ad;'"/>
  92       </xsl:when>
  93       <xsl:when test="$symbol = 'beta_red' or $symbol = 'beta_red1'">
  94        <xsl:value-of select="'&#x00ae;'"/>
  95       </xsl:when>
  96       <xsl:when test="$symbol = 'beta'">
  97        <xsl:value-of select="'&#x0062;'"/>
  98       </xsl:when>
  99       <xsl:when test="$symbol = 'par_beta_red' or $symbol = 'par_beta_red1'">
 100        <xsl:value-of select="'&#x00de;'"/>
 101       </xsl:when>
 102       <xsl:when test="$symbol = 'isomorphic'">
 103        <xsl:value-of select="'&#x0040;'"/>
 104       </xsl:when>
 105       <xsl:otherwise>
 106        <xsl:text>???</xsl:text>
 107       </xsl:otherwise>
 108      </xsl:choose>
 109     </xsl:variable>
 110     <FONT FACE="symbol" SIZE="{$size}" color="{$color}">
 111      <xsl:value-of select="$fontsymbol"/>
 112     </FONT>
 113    </xsl:when>
 114    <xsl:otherwise>
 115     <xsl:variable name="unicodesymbol">
 116      <xsl:choose>
 117       <xsl:when test="$symbol = 'forall'">
 118        <xsl:value-of select="'&#8704;'"/>
 119       </xsl:when>
 120       <xsl:when test="$symbol = 'lambda'">
 121        <xsl:value-of select="'&#955;'"/>
 122       </xsl:when>
 123       <xsl:when test="$symbol = 'prod'">
 124        <xsl:value-of select="'&#928;'"/>
 125       </xsl:when>
 126       <xsl:when test="$symbol = 'arrow'">
 127        <xsl:value-of select="'&#8594;'"/>
 128       </xsl:when>
 129       <xsl:when test="$symbol = 'RightArrow'">
 130        <xsl:value-of select="'&#8658;'"/>
 131       </xsl:when>
 132       <xsl:when test="$symbol = 'subst'">
 133        <xsl:value-of select="'&#8592;'"/>
 134       </xsl:when>
 135       <xsl:when test="$symbol = 'lift' or $symbol = 'lift_with_base'">
 136        <xsl:value-of select="'&#8593;'"/>
 137       </xsl:when>
 138       <xsl:when test="$symbol = 'beta_red' or $symbol = 'beta_red1'">
 139        <xsl:value-of select="'&#8594;'"/>
 140       </xsl:when>
 141       <xsl:when test="$symbol = 'beta'">
 142        <xsl:value-of select="'&#946;'"/>
 143       </xsl:when>
 144       <xsl:when test="$symbol = 'par_beta_red' or $symbol = 'par_beta_red1'">
 145        <xsl:value-of select="'&#8658;'"/>
 146       </xsl:when>
 147       <xsl:when test="$symbol = 'isomorphic'">
 148        <xsl:value-of select="'&#8773;'"/>
 149       </xsl:when>
 150       <xsl:otherwise>
 151        <xsl:text>???</xsl:text>
 152       </xsl:otherwise>
 153      </xsl:choose>
 154     </xsl:variable>
 155     <FONT color="{$color}">
 156      <xsl:value-of select="$unicodesymbol"/>
 157     </FONT>
 158    </xsl:otherwise>
 159   </xsl:choose>
 160 </xsl:template>
 161
 162 <xsl:template match="/">
 163  <xsl:param name="current_indent" select="0"/>
 164  <xsl:choose>
 165   <xsl:when test="$type = 'standalone'">
 166    <html>
 167       <head>
 168          <title> <xsl:value-of select="$CICURI"/> </title> <!-- FG -->
 169          <style> A { text-decoration: none } </style>
 170          <script>
 171           <xsl:text disable-output-escaping="yes">
 172            <![CDATA[
 173             function Hide(which){
 174              if (!document.getElementById)
 175               return
 176              which.style.display="none"
 177             }
 178
 179             function Show(which){
 180              if (!document.getElementById)
 181               return
 182              which.style.display=""
 183             }
 184
 185             document.to_be_deleted = new Array();
 186           ]]>
 187           </xsl:text>
 188          </script>
 189       </head>
 190       <body bgcolor="white">
 191          <xsl:attribute name="onLoad">
 192           if(document.getElementById)
 193            for(var i=0;i&lt;document.to_be_deleted.length;i++)
 194             Hide(document.getElementById(document.to_be_deleted[i]));
 195          </xsl:attribute>
 196          <xsl:apply-templates>
 197             <xsl:with-param name="current_indent" select="0"/>
 198          </xsl:apply-templates>
 199       </body>
 200    </html>
 201   </xsl:when>
 202   <xsl:otherwise>
 203    <to_be_embedded>
 204     <xsl:apply-templates>
 205      <xsl:with-param name="current_indent" select="0"/>
 206     </xsl:apply-templates>
 207    </to_be_embedded>
 208   </xsl:otherwise>
 209  </xsl:choose>
 210 </xsl:template>
 211
 212 <!--***********************************************************************-->
 213 <!-- Indentation                                                           -->
 214 <!--***********************************************************************-->
 215
 216 <xsl:template name="make_indent">
 217  <xsl:param name="current_indent" select="0"/>
 218   <xsl:if test="$current_indent > 0">
 219    <xsl:text>&#x00a0;</xsl:text>
 220    <xsl:call-template name="make_indent">
 221     <xsl:with-param name="current_indent" select="$current_indent - 1"/>
 222    </xsl:call-template>
 223   </xsl:if>
 224 </xsl:template>
 225
 226 <!-- Syntactic Sugar -->
 227 <xsl:template match="m:type">
 228 <xsl:param name="current_indent" select="0"/>
 229 <xsl:apply-templates>
 230  <xsl:with-param name="current_indent"
 231            select="$current_indent"/>
 232 </xsl:apply-templates>
 233 </xsl:template>
 234
 235 <xsl:template match="m:condition">
 236 <xsl:param name="current_indent" select="0"/>
 237 <xsl:apply-templates>
 238  <xsl:with-param name="current_indent"
 239            select="$current_indent"/>
 240 </xsl:apply-templates>
 241 </xsl:template>
 242
 243 <xsl:template match="m:math">
 244 <xsl:param name="current_indent" select="0"/>
 245 <xsl:apply-templates>
 246  <xsl:with-param name="current_indent"
 247            select="$current_indent"/>
 248 </xsl:apply-templates>
 249 </xsl:template>
 250
 251 <!--*********************************************************************-->
 252 <!--                         INLINE MODE                                 -->
 253 <!--*********************************************************************-->
 254
 255 <!-- href -->
 256 <xsl:template mode="inline" match="m:ci">
 257  <xsl:choose>
 258   <xsl:when test="boolean(@definitionURL)">
 259    <a href="{@definitionURL}">
 260    <xsl:apply-templates/>
 261    </a>
 262   </xsl:when>
 263   <xsl:otherwise>
 264    <xsl:value-of select="."/>
 265   </xsl:otherwise>
 266  </xsl:choose>
 267 </xsl:template>
 268
 269 <!-- CSYMBOL -->
 270
 271 <xsl:template match="m:apply[m:csymbol]" mode="inline">
 272    <xsl:variable name="name">
 273     <xsl:value-of select="m:csymbol"/>
 274    </xsl:variable>
 275    <xsl:variable name="uri"><xsl:value-of select="*[1]/@definitionURL"/></xsl:variable>
 276    <xsl:choose>
 277     <!-- FORALL -->
 278     <xsl:when test="$name='forall'">
 279      <xsl:call-template name="mksymbol-1">
 280       <xsl:with-param name="symbol" select="$name"/>
 281       <xsl:with-param name="color" select="'blue'"/>
 282       <xsl:with-param name="size" select="'+2'"/>
 283      </xsl:call-template>
 284      <xsl:apply-templates select="m:bvar/m:ci"/>
 285      <xsl:text>:</xsl:text>
 286      <xsl:apply-templates mode="inline" select="m:bvar/m:type"/>
 287      <xsl:text>.</xsl:text>
 288      <xsl:apply-templates mode="inline" select="*[position()=3]"/>
 289     </xsl:when>
 290     <xsl:when test="$name='prod'">
 291      <xsl:call-template name="mksymbol-1">
 292       <xsl:with-param name="symbol" select="$name"/>
 293       <xsl:with-param name="color" select="'blue'"/>
 294       <xsl:with-param name="size" select="'+2'"/>
 295      </xsl:call-template>
 296      <xsl:apply-templates mode="inline" select="m:bvar/m:ci"/>
 297      <xsl:text>:</xsl:text>
 298      <xsl:apply-templates mode="inline" select="m:bvar/m:type"/>
 299      <xsl:text>.</xsl:text>
 300      <xsl:apply-templates mode="inline" select="*[position()=3]"/>
 301     </xsl:when>
 302     <!-- ARROW -->
 303     <xsl:when test="$name='arrow'">
 304      <xsl:text>(</xsl:text>
 305      <xsl:apply-templates mode="inline" select="*[position()=2]"/>
 306      <xsl:call-template name="mksymbol-1">
 307       <xsl:with-param name="symbol" select="$name"/>
 308       <xsl:with-param name="color" select="'blue'"/>
 309       <xsl:with-param name="size" select="'+0'"/>
 310      </xsl:call-template>
 311      <xsl:apply-templates mode="inline" select="*[position()=3]"/>
 312      <xsl:text>)</xsl:text>
 313     </xsl:when>
 314     <!-- APP -->
 315     <xsl:when test="$name='app'">
 316      <xsl:text>(</xsl:text>
 317      <xsl:apply-templates mode="inline" select="*[position()=2]"/>
 318      <xsl:for-each select="*[position()>2]">
 319       <xsl:text>&#x00A0;</xsl:text>
 320       <xsl:apply-templates mode="inline" select="."/>
 321      </xsl:for-each>
 322      <xsl:text>)</xsl:text>
 323     </xsl:when>
 324     <!-- CAST -->
 325     <xsl:when test="$name='cast'">
 326      <xsl:text>(</xsl:text>
 327      <xsl:apply-templates mode="inline" select="*[position()=2]"/>
 328      <xsl:text>:></xsl:text>
 329      <xsl:apply-templates mode="inline" select="*[position()=3]"/>
 330      <xsl:text>)</xsl:text>
 331     </xsl:when>
 332     <xsl:when test="$name='Prop'">
 333      <FONT color="violet">Prop</FONT>
 334     </xsl:when>
 335     <xsl:when test="$name='Set'">
 336      <FONT color="violet">Set</FONT>
 337     </xsl:when>
 338     <xsl:when test="$name='Type'">
 339      <FONT color="violet">Type</FONT>
 340     </xsl:when>
 341     <!-- MUTCASE -->
 342     <xsl:when test="$name='mutcase'">
 343      <xsl:text>&lt;</xsl:text>
 344      <xsl:apply-templates mode="inline" select="*[position()=2]"/>
 345      <xsl:text>&gt; </xsl:text>
 346      <FONT color="red">CASE </FONT>
 347      <xsl:apply-templates mode="inline" select="*[position()=3]"/>
 348      <FONT color="red"> OF </FONT>
 349 <xsl:for-each select="piecewise/piece">
 350 <!--<xsl:for-each select="*[position() mod 2 = 0 and position()>3]">-->
 351       <xsl:choose>
 352        <xsl:when test="not(position() = 1)">
 353         <xsl:text> | </xsl:text>
 354        </xsl:when>
 355       </xsl:choose>
 356 <xsl:apply-templates mode="inline" select="./*[2]"/>
 357       <xsl:call-template name="mksymbol-1">
 358        <xsl:with-param name="symbol" select="'RightArrow'"/>
 359        <xsl:with-param name="color" select="'green'"/>
 360        <xsl:with-param name="size" select="'+0'"/>
 361       </xsl:call-template>
 362       <xsl:apply-templates mode="inline"
 363            select="./*[1]"/>
 364      </xsl:for-each>
 365     </xsl:when>
 366     <!-- FIX -->
 367     <xsl:when test="$name='fix'">
 368      <FONT color="red">FIX</FONT>
 369      <xsl:value-of select="m:ci"/>
 370      <xsl:text>{</xsl:text>
 371      <xsl:for-each select="m:bvar">
 372       <xsl:value-of select="m:ci"/>
 373       <xsl:text>:</xsl:text>
 374       <xsl:apply-templates mode="inline" select="m:type"/>
 375       <xsl:text>:=</xsl:text>
 376       <xsl:apply-templates mode="inline"
 377              select="following-sibling::*[position() = 1]"/>
 378       <xsl:choose>
 379        <xsl:when test="position()=last()">
 380         <xsl:text>}</xsl:text>
 381        </xsl:when>
 382        <xsl:otherwise>
 383         <xsl:text>;</xsl:text>
 384        </xsl:otherwise>
 385       </xsl:choose>
 386      </xsl:for-each>
 387     </xsl:when>
 388     <!-- COFIX -->
 389     <xsl:when test="$name='cofix'">
 390      <xsl:text>COFIX</xsl:text>
 391      <xsl:value-of select="m:ci"/>
 392      <xsl:text>{</xsl:text>
 393      <xsl:for-each select="m:bvar">
 394       <xsl:value-of select="m:ci"/>
 395       <xsl:text>:</xsl:text>
 396       <xsl:apply-templates mode="inline" select="m:type"/>
 397       <xsl:text>:=</xsl:text>
 398       <xsl:apply-templates mode="inline"
 399           select="following-sibling::*[position() = 1]"/>
 400       <xsl:choose>
 401        <xsl:when test="position()=last()">
 402         <xsl:text>}</xsl:text>
 403        </xsl:when>
 404        <xsl:otherwise>
 405         <xsl:text>;</xsl:text>
 406        </xsl:otherwise>
 407       </xsl:choose>
 408      </xsl:for-each>
 409     </xsl:when>
 410     <!-- proof -->
 411     <xsl:when test="$name='proof'">
 412        <xsl:apply-templates mode="inline" select="*[position()=2]"/>
 413        <FONT color="red">&#x00a0;proves&#x00a0;</FONT>
 414        <xsl:apply-templates mode="inline" select="*[position()=3]"/>
 415     </xsl:when>
 416     <!-- false_ind -->
 417     <xsl:when test="$name='false_ind'">
 418     <xsl:apply-templates mode="inline" select="*[3]"/>
 419     <FONT color="red">Contradiction.</FONT>
 420     </xsl:when>
 421     <!-- and_ind -->
 422     <xsl:when test="$name='and_ind'">
 423      <FONT color="red">From&#x00a0;</FONT>
 424      <xsl:apply-templates select="*[2]"/>
 425      <FONT color="red">&#x00a0;we get</FONT>
 426      (
 427      <xsl:apply-templates select="*[3]"/>
 428      )&#x00a0;
 429      <xsl:apply-templates mode="inline" select="*[4]"/>
 430      <FONT color="red">&#x00a0;and&#x00a0;</FONT>
 431      (
 432      <xsl:apply-templates select="*[5]"/>
 433      )&#x00a0;
 434      <xsl:apply-templates mode="inline" select="*[6]"/>
 435      ;
 436      <FONT color="red">&#x00a0;hence&#x00a0;</FONT>
 437      <xsl:apply-templates mode="inline" select="*[7]"/>
 438     </xsl:when>
 439
 440        <xsl:when test="$name='subst'">
 441        <xsl:apply-templates select="*[3]" mode="inline"/>
 442        <xsl:text>[</xsl:text>
 443        <xsl:apply-templates select="*[4]" mode="inline"/>
 444        <xsl:choose>
 445        <xsl:when test="$uri != ''">
 446         <a href="{$uri}">
 447          <xsl:call-template name="mksymbol-1">
 448           <xsl:with-param name="symbol" select="$name"/>
 449           <xsl:with-param name="color" select="'green'"/>
 450           <xsl:with-param name="size" select="'+0'"/>
 451          </xsl:call-template>
 452         </a>
 453        </xsl:when>
 454        <xsl:otherwise>
 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        </xsl:otherwise>
 461        </xsl:choose>
 462        <xsl:apply-templates select="*[2]" mode="inline"/>
 463        <xsl:text>]</xsl:text>
 464       </xsl:when>
 465
 466       <xsl:when test="$name='lift_with_base'">
 467        <SUB>
 468        <xsl:apply-templates select="*[3]" mode="inline"/>
 469        </SUB>
 470        <xsl:choose>
 471        <xsl:when test="$uri != ''">
 472          <a href="{$uri}">
 473           <xsl:call-template name="mksymbol-1">
 474            <xsl:with-param name="symbol" select="$name"/>
 475            <xsl:with-param name="color" select="'green'"/>
 476            <xsl:with-param name="size" select="'+0'"/>
 477           </xsl:call-template>
 478          </a>
 479        </xsl:when>
 480        <xsl:otherwise>
 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        </xsl:otherwise>
 487        </xsl:choose>
 488        <SUP>
 489        <xsl:apply-templates select="*[4]" mode="inline"/>
 490        </SUP>
 491        <xsl:text>(</xsl:text>
 492        <xsl:apply-templates select="*[2]" mode="inline"/>
 493        <xsl:text>)</xsl:text>
 494       </xsl:when>
 495
 496       <xsl:when test="$name='lift'">
 497        <xsl:choose>
 498        <xsl:when test="$uri != ''">
 499         <a href="{$uri}">
 500          <xsl:call-template name="mksymbol-1">
 501           <xsl:with-param name="symbol" select="$name"/>
 502           <xsl:with-param name="color" select="'green'"/>
 503           <xsl:with-param name="size" select="'+0'"/>
 504          </xsl:call-template>
 505         </a>
 506        </xsl:when>
 507        <xsl:otherwise>
 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        </xsl:otherwise>
 514        </xsl:choose>
 515        <SUP>
 516        <xsl:apply-templates select="*[2]" mode="inline"/>
 517        </SUP>
 518        <xsl:text>(</xsl:text>
 519        <xsl:apply-templates select="*[3]" mode="inline"/>
 520        <xsl:text>)</xsl:text>
 521       </xsl:when>
 522
 523       <!-- reduction -->
 524       <xsl:when test="$name='beta_red1'">
 525        <xsl:apply-templates select="*[2]" mode="inline"/>
 526        <xsl:choose>
 527        <xsl:when test="$uri != ''">
 528         <a href="{$uri}">
 529          <xsl:call-template name="mksymbol-1">
 530           <xsl:with-param name="symbol" select="$name"/>
 531           <xsl:with-param name="color" select="'green'"/>
 532           <xsl:with-param name="size" select="'+0'"/>
 533          </xsl:call-template>
 534          <SUB>
 535          <xsl:call-template name="mksymbol-1">
 536           <xsl:with-param name="symbol" select="'beta'"/>
 537           <xsl:with-param name="color" select="'green'"/>
 538           <xsl:with-param name="size" select="'+0'"/>
 539          </xsl:call-template>
 540          </SUB>
 541         </a>
 542        </xsl:when>
 543        <xsl:otherwise>
 544          <xsl:call-template name="mksymbol-1">
 545           <xsl:with-param name="symbol" select="$name"/>
 546           <xsl:with-param name="color" select="'green'"/>
 547           <xsl:with-param name="size" select="'+0'"/>
 548          </xsl:call-template>
 549          <SUB>
 550          <xsl:call-template name="mksymbol-1">
 551           <xsl:with-param name="symbol" select="'beta'"/>
 552           <xsl:with-param name="color" select="'green'"/>
 553           <xsl:with-param name="size" select="'+0'"/>
 554          </xsl:call-template>
 555          </SUB>
 556        </xsl:otherwise>
 557        </xsl:choose>
 558        <xsl:apply-templates select="*[3]" mode="inline"/>
 559       </xsl:when>
 560
 561       <xsl:when test="$name='beta_red'">
 562        <xsl:apply-templates select="*[2]" mode="inline"/>
 563        <xsl:choose>
 564        <xsl:when test="$uri != ''">
 565         <a href="{$uri}">
 566          <xsl:call-template name="mksymbol-1">
 567           <xsl:with-param name="symbol" select="$name"/>
 568           <xsl:with-param name="color" select="'green'"/>
 569           <xsl:with-param name="size" select="'+0'"/>
 570          </xsl:call-template>
 571          <SUB>
 572          <xsl:call-template name="mksymbol-1">
 573           <xsl:with-param name="symbol" select="'beta'"/>
 574           <xsl:with-param name="color" select="'green'"/>
 575           <xsl:with-param name="size" select="'+0'"/>
 576          </xsl:call-template>
 577          <xsl:text>*</xsl:text>
 578          </SUB>
 579         </a>
 580        </xsl:when>
 581        <xsl:otherwise>
 582          <xsl:call-template name="mksymbol-1">
 583           <xsl:with-param name="symbol" select="$name"/>
 584           <xsl:with-param name="color" select="'green'"/>
 585           <xsl:with-param name="size" select="'+0'"/>
 586          </xsl:call-template>
 587          <SUB>
 588          <xsl:call-template name="mksymbol-1">
 589           <xsl:with-param name="symbol" select="'beta'"/>
 590           <xsl:with-param name="color" select="'green'"/>
 591           <xsl:with-param name="size" select="'+0'"/>
 592          </xsl:call-template>
 593          <xsl:text>*</xsl:text>
 594          </SUB>
 595        </xsl:otherwise>
 596        </xsl:choose>
 597        <xsl:apply-templates select="*[3]" mode="inline"/>
 598       </xsl:when>
 599
 600       <xsl:when test="$name='par_beta_red1'">
 601        <xsl:apply-templates select="*[2]" mode="inline"/>
 602        <xsl:choose>
 603        <xsl:when test="$uri != ''">
 604         <a href="{$uri}">
 605          <xsl:call-template name="mksymbol-1">
 606           <xsl:with-param name="symbol" select="$name"/>
 607           <xsl:with-param name="color" select="'green'"/>
 608           <xsl:with-param name="size" select="'+0'"/>
 609          </xsl:call-template>
 610          <SUB>
 611          <xsl:call-template name="mksymbol-1">
 612           <xsl:with-param name="symbol" select="'beta'"/>
 613           <xsl:with-param name="color" select="'green'"/>
 614           <xsl:with-param name="size" select="'+0'"/>
 615          </xsl:call-template>
 616          </SUB>
 617         </a>
 618        </xsl:when>
 619        <xsl:otherwise>
 620          <xsl:call-template name="mksymbol-1">
 621           <xsl:with-param name="symbol" select="$name"/>
 622           <xsl:with-param name="color" select="'green'"/>
 623           <xsl:with-param name="size" select="'+0'"/>
 624          </xsl:call-template>
 625          <SUB>
 626          <xsl:call-template name="mksymbol-1">
 627           <xsl:with-param name="symbol" select="'beta'"/>
 628           <xsl:with-param name="color" select="'green'"/>
 629           <xsl:with-param name="size" select="'+0'"/>
 630          </xsl:call-template>
 631          </SUB>
 632        </xsl:otherwise>
 633        </xsl:choose>
 634        <xsl:apply-templates select="*[3]" mode="inline"/>
 635       </xsl:when>
 636
 637       <xsl:when test="$name='par_beta_red'">
 638        <xsl:apply-templates select="*[2]" mode="inline"/>
 639        <xsl:choose>
 640        <xsl:when test="$uri != ''">
 641         <a href="{$uri}">
 642          <xsl:call-template name="mksymbol-1">
 643           <xsl:with-param name="symbol" select="$name"/>
 644           <xsl:with-param name="color" select="'green'"/>
 645           <xsl:with-param name="size" select="'+0'"/>
 646          </xsl:call-template>
 647          <SUB>
 648          <xsl:call-template name="mksymbol-1">
 649           <xsl:with-param name="symbol" select="'beta'"/>
 650           <xsl:with-param name="color" select="'green'"/>
 651           <xsl:with-param name="size" select="'+0'"/>
 652          </xsl:call-template>
 653          <xsl:text>*</xsl:text>
 654          </SUB>
 655         </a>
 656        </xsl:when>
 657        <xsl:otherwise>
 658          <xsl:call-template name="mksymbol-1">
 659           <xsl:with-param name="symbol" select="$name"/>
 660           <xsl:with-param name="color" select="'green'"/>
 661           <xsl:with-param name="size" select="'+0'"/>
 662          </xsl:call-template>
 663          <SUB>
 664          <xsl:call-template name="mksymbol-1">
 665           <xsl:with-param name="symbol" select="'beta'"/>
 666           <xsl:with-param name="color" select="'green'"/>
 667           <xsl:with-param name="size" select="'+0'"/>
 668          </xsl:call-template>
 669          <xsl:text>*</xsl:text>
 670          </SUB>
 671        </xsl:otherwise>
 672        </xsl:choose>
 673        <xsl:apply-templates select="*[3]" mode="inline"/>
 674       </xsl:when>
 675
 676       <!-- forgetful -->
 677       <xsl:when test="$name='forgetful'">
 678        <xsl:choose>
 679        <xsl:when test="$uri != ''">
 680         <a href="{$uri}">|</a>
 681        </xsl:when>
 682        <xsl:otherwise>
 683         |
 684        </xsl:otherwise>
 685        </xsl:choose>
 686        <xsl:apply-templates select="*[2]" mode="inline"/>
 687         <xsl:choose>
 688         <xsl:when test="$uri != ''">
 689          <a href="{$uri}">|</a>
 690         </xsl:when>
 691        <xsl:otherwise>
 692         |
 693        </xsl:otherwise>
 694        </xsl:choose>
 695       </xsl:when>
 696
 697       <!-- boolean algebra of redexes -->
 698
 699       <!-- isomorphic -->
 700       <xsl:when test="$name='isomorphic'">
 701        <xsl:apply-templates select="*[2]" mode="inline"/>
 702        <xsl:choose>
 703        <xsl:when test="$uri != ''">
 704         <a href="{$uri}">
 705          <xsl:call-template name="mksymbol-1">
 706           <xsl:with-param name="symbol" select="$name"/>
 707           <xsl:with-param name="color" select="'green'"/>
 708           <xsl:with-param name="size" select="'+0'"/>
 709          </xsl:call-template>
 710         </a>
 711        </xsl:when>
 712        <xsl:otherwise>
 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        </xsl:otherwise>
 719        </xsl:choose>
 720        <xsl:apply-templates select="*[3]" mode="inline"/>
 721       </xsl:when>
 722
 723       <!-- INTERP -->
 724       <xsl:when test="$name='interp'">
 725          <font color="green">[</font>
 726             <xsl:apply-templates select="*[2]"/>
 727          <font color="green">]</font>
 728       </xsl:when>
 729
 730    </xsl:choose>
 731 </xsl:template>
 732
 733 <xsl:template mode="inline" match="m:lambda">
 734       <xsl:call-template name="mksymbol-1">
 735        <xsl:with-param name="symbol" select="'lambda'"/>
 736        <xsl:with-param name="color" select="'red'"/>
 737        <xsl:with-param name="size" select="'+2'"/>
 738       </xsl:call-template>
 739       <xsl:apply-templates select="m:bvar/m:ci"/>
 740       <xsl:text>:</xsl:text>
 741       <xsl:apply-templates mode="inline" select="m:bvar/m:type"/>
 742       <xsl:text>.</xsl:text>
 743       <xsl:apply-templates mode="inline" select="*[position()=2]"/>
 744 </xsl:template>
 745
 746 <!--*********************************************************************-->
 747 <!--                       COUNTING MODE                                 -->
 748 <!--*********************************************************************-->
 749
 750 <xsl:template match="m:apply[m:csymbol]">
 751   <xsl:param name="current_indent" select="0"/>
 752   <xsl:param name="width" select="$framewidth"/>
 753   <xsl:variable name="name">
 754    <xsl:value-of select="m:csymbol"/>
 755   </xsl:variable>
 756   <xsl:variable name="charlength">
 757    <xsl:apply-templates select="m:csymbol" mode="charcount"/>
 758   </xsl:variable>
 759      <!-- <xsl:value-of select="$current_indent"/> -->
 760      <!-- <xsl:value-of select="$charlength"/> -->
 761   <xsl:variable name="uri"><xsl:value-of select="*[1]/@definitionURL"/></xsl:variable>
 762      <xsl:choose>
 763      <!-- FORALL -->
 764       <xsl:when test="$name='forall'">
 765        <xsl:choose>
 766        <xsl:when test="$charlength > $framewidth">
 767          <!-- &#x03a0; -->
 768          <xsl:call-template name="mksymbol-1">
 769           <xsl:with-param name="symbol" select="$name"/>
 770           <xsl:with-param name="color" select="'blue'"/>
 771           <xsl:with-param name="size" select="'+2'"/>
 772          </xsl:call-template>
 773          <xsl:apply-templates select="m:bvar/m:ci"/>
 774          <xsl:text>:</xsl:text>
 775          <xsl:apply-templates select="m:bvar/m:type">
 776           <xsl:with-param name="current_indent"
 777            select="$current_indent + 5 + 2*string-length(m:bvar/m:ci)"/>
 778          </xsl:apply-templates>
 779          <br/>
 780          <xsl:call-template name="make_indent">
 781           <xsl:with-param name="current_indent" select="$current_indent + 2"/>
 782          </xsl:call-template>
 783          <xsl:text>.</xsl:text>
 784          <xsl:apply-templates select="*[position()=3]">
 785           <xsl:with-param name="current_indent" select="$current_indent + 2"/>
 786          </xsl:apply-templates>
 787        </xsl:when>
 788        <xsl:otherwise>
 789         <xsl:apply-templates mode="inline" select="."/>
 790        </xsl:otherwise>
 791        </xsl:choose>
 792       </xsl:when>
 793       <!-- PROD -->
 794       <xsl:when test="$name='prod'">
 795        <xsl:choose>
 796        <xsl:when test="$charlength > $framewidth">
 797          <xsl:call-template name="mksymbol-1">
 798           <xsl:with-param name="symbol" select="$name"/>
 799           <xsl:with-param name="color" select="'blue'"/>
 800           <xsl:with-param name="size" select="'+2'"/>
 801          </xsl:call-template>
 802          <xsl:apply-templates select="m:bvar/m:ci"/>
 803          <xsl:text>:</xsl:text>
 804          <xsl:apply-templates select="m:bvar/m:type">
 805           <xsl:with-param name="current_indent"
 806            select="$current_indent + 5 + 2*string-length(m:bvar/m:ci)"/>
 807          </xsl:apply-templates><br/>
 808          <xsl:call-template name="make_indent">
 809           <xsl:with-param name="current_indent" select="$current_indent + 2"/>
 810          </xsl:call-template>
 811          <xsl:text>.</xsl:text>
 812          <xsl:apply-templates select="*[position()=3]">
 813           <xsl:with-param name="current_indent" select="$current_indent + 2"/>
 814          </xsl:apply-templates>
 815        </xsl:when>
 816        <xsl:otherwise>
 817         <xsl:apply-templates mode="inline" select="."/>
 818        </xsl:otherwise>
 819        </xsl:choose>
 820       </xsl:when>
 821       <!-- ARROW -->
 822       <xsl:when test="$name='arrow'">
 823        <xsl:choose>
 824        <xsl:when test="$charlength > $framewidth">
 825        <xsl:text>(</xsl:text>
 826        <xsl:apply-templates select="*[position()=2]">
 827         <xsl:with-param name="current_indent" select="$current_indent + 2"/>
 828        </xsl:apply-templates>
 829        <br/>
 830        <xsl:call-template name="make_indent">
 831         <xsl:with-param name="current_indent" select="$current_indent + 2"/>
 832        </xsl:call-template>
 833        <!-- -> -->
 834        <xsl:call-template name="mksymbol-1">
 835         <xsl:with-param name="symbol" select="$name"/>
 836         <xsl:with-param name="color" select="'blue'"/>
 837         <xsl:with-param name="size" select="'+0'"/>
 838        </xsl:call-template>
 839        <xsl:apply-templates select="*[position()=3]">
 840         <xsl:with-param name="current_indent" select="$current_indent + 5"/>
 841        </xsl:apply-templates>
 842        <xsl:text>)</xsl:text>
 843        </xsl:when>
 844        <xsl:otherwise>
 845         <xsl:apply-templates mode="inline" select="."/>
 846        </xsl:otherwise>
 847        </xsl:choose>
 848       </xsl:when>
 849       <!-- APP -->
 850       <xsl:when test="$name='app'">
 851        <xsl:choose>
 852        <xsl:when test="$charlength  > $framewidth">
 853         <xsl:text>(</xsl:text>
 854         <xsl:apply-templates select="*[position()=2]">
 855          <xsl:with-param name="current_indent" select="$current_indent + 2"/>
 856         </xsl:apply-templates>
 857          <xsl:for-each select="*[position()>2]">
 858           <br/>
 859            <xsl:call-template name="make_indent">
 860             <xsl:with-param name="current_indent" select="$current_indent + 2"/>
 861            </xsl:call-template>
 862             <xsl:apply-templates select=".">
 863              <xsl:with-param name="current_indent" select="$current_indent + 2"/>
 864             </xsl:apply-templates>
 865          </xsl:for-each>
 866          <xsl:text>)</xsl:text>
 867        </xsl:when>
 868        <xsl:otherwise>
 869         <xsl:apply-templates mode="inline" select="."/>
 870        </xsl:otherwise>
 871        </xsl:choose>
 872       </xsl:when>
 873       <xsl:when test="$name='cast'">
 874        <xsl:choose>
 875         <xsl:when test="$showcast = 1">
 876          <xsl:choose>
 877           <xsl:when test="$charlength > $framewidth">
 878            <xsl:text>(</xsl:text>
 879            <xsl:apply-templates select="*[position()=2]">
 880             <xsl:with-param name="current_indent" select="$current_indent + 2"/>
 881            </xsl:apply-templates><br/>
 882            <xsl:call-template name="make_indent">
 883             <xsl:with-param name="current_indent" select="$current_indent + 2"/>          </xsl:call-template>
 884            <xsl:text>:></xsl:text>
 885            <xsl:apply-templates select="*[position()=3]">
 886             <xsl:with-param name="current_indent" select="$current_indent + 3"/>
 887            </xsl:apply-templates>
 888            <xsl:text>)</xsl:text>
 889           </xsl:when>
 890           <xsl:otherwise>
 891            <xsl:apply-templates mode="inline" select="."/>
 892           </xsl:otherwise>
 893          </xsl:choose>
 894         </xsl:when>
 895         <xsl:otherwise>
 896          <xsl:apply-templates select="*[position()=2]">
 897           <xsl:with-param name="current_indent" select="$current_indent"/>
 898          </xsl:apply-templates>
 899         </xsl:otherwise>
 900        </xsl:choose>
 901       </xsl:when>
 902       <xsl:when test="$name='Prop'">
 903        <xsl:text>Prop</xsl:text>
 904       </xsl:when>
 905       <xsl:when test="$name='Set'">
 906        <xsl:text>Set</xsl:text>
 907       </xsl:when>
 908       <xsl:when test="$name='Type'">
 909        <xsl:text>Type</xsl:text>
 910       </xsl:when>
 911       <xsl:when test="$name='mutcase'">
 912        <xsl:choose>
 913        <xsl:when test="$charlength > $framewidth">
 914          <xsl:text>&lt;</xsl:text>
 915          <xsl:apply-templates select="*[position()=2]">
 916           <xsl:with-param name="current_indent" select="$current_indent + 2"/>
 917          </xsl:apply-templates>
 918          <xsl:text>&gt; </xsl:text>
 919          <br/>
 920          <xsl:call-template name="make_indent">
 921           <xsl:with-param name="current_indent" select="$current_indent + 2"/>           </xsl:call-template>
 922          <xsl:text>CASE </xsl:text>
 923          <xsl:apply-templates select="*[position()=3]">
 924           <xsl:with-param name="current_indent" select="$current_indent + 8"/>
 925          </xsl:apply-templates>
 926          <xsl:text> OF </xsl:text>
 927          <xsl:for-each select="piecewise/piece">
 928     <!--   <xsl:for-each select="*[position() mod 2 = 0 and position()>3]">-->
 929          <br/>
 930          <xsl:call-template name="make_indent">
 931           <xsl:with-param name="current_indent" select="$current_indent + 2"/>
 932          </xsl:call-template>
 933             <xsl:choose>
 934             <xsl:when test="position() = 1">
 935              <xsl:text>&#x00A0;&#x00A0;</xsl:text>
 936             </xsl:when>
 937             <xsl:otherwise>
 938              <xsl:text>| </xsl:text>
 939             </xsl:otherwise>
 940             </xsl:choose>
 941           <xsl:apply-templates select="./*[2]"/>
 942             <xsl:call-template name="mksymbol-1">
 943              <xsl:with-param name="symbol" select="'RightArrow'"/>
 944              <xsl:with-param name="color" select="'green'"/>
 945              <xsl:with-param name="size" select="'+0'"/>
 946             </xsl:call-template>
 947             <xsl:variable name="body_size">
 948   <xsl:apply-templates
 949               select="./*[1]/*[1]" mode="charcount"/>
 950             </xsl:variable>
 951             <xsl:choose>
 952              <xsl:when test="$body_size > $framewidth">
 953               <br/>
 954               <xsl:call-template name="make_indent">
 955                <xsl:with-param name="current_indent"
 956                     select="$current_indent + 8"/>
 957               </xsl:call-template>
 958 <xsl:apply-templates
 959                    select="./*[1]">
 960               <xsl:with-param name="current_indent"
 961                    select="$current_indent + 8"/>
 962              </xsl:apply-templates>
 963             </xsl:when>
 964             <xsl:otherwise>
 965      <xsl:apply-templates select="./*[1]"
 966                    mode="inline" />
 967             </xsl:otherwise>
 968            </xsl:choose>
 969          </xsl:for-each>
 970        </xsl:when>
 971        <xsl:otherwise>
 972         <xsl:apply-templates mode="inline" select="."/>
 973        </xsl:otherwise>
 974        </xsl:choose>
 975       </xsl:when>
 976       <!-- FIX -->
 977       <xsl:when test="$name='fix'">
 978        <xsl:choose>
 979        <xsl:when test="$charlength  > $framewidth">
 980             <xsl:text>FIX</xsl:text>
 981             <xsl:value-of select="m:ci"/>
 982             <xsl:text>{</xsl:text>
 983             <xsl:for-each select="m:bvar">
 984               <br/>
 985               <xsl:call-template name="make_indent">
 986                <xsl:with-param name="current_indent" select="$current_indent + 2"/>
 987               </xsl:call-template>
 988               <xsl:value-of select="m:ci"/>
 989               <xsl:text>:</xsl:text>
 990               <xsl:apply-templates select="m:type">
 991                <xsl:with-param name="current_indent"
 992                     select="$current_indent + 5 + string-length(m:ci)"/>
 993                </xsl:apply-templates>
 994               <br/>
 995               <xsl:call-template name="make_indent">
 996                <xsl:with-param name="current_indent" select="$current_indent + 2"/>
 997               </xsl:call-template>
 998               <xsl:text>:=</xsl:text>
 999               <xsl:apply-templates select="following-sibling::*[position() = 1]">
1000                <xsl:with-param name="current_indent" select="$current_indent +2"/>
1001               </xsl:apply-templates>
1002             </xsl:for-each>
1003              <br/>
1004               <xsl:call-template name="make_indent">
1005                <xsl:with-param name="current_indent" select="$current_indent + 2"/>
1006               </xsl:call-template>
1007            <xsl:text>}</xsl:text>
1008        </xsl:when>
1009        <xsl:otherwise>
1010         <xsl:apply-templates mode="inline" select="."/>
1011        </xsl:otherwise>
1012        </xsl:choose>
1013       </xsl:when>
1014       <!-- COFIX -->
1015       <xsl:when test="$name='cofix'">
1016        <xsl:choose>
1017        <xsl:when test="($charlength + 10) > $framewidth">
1018             <xsl:text>COFIX</xsl:text>
1019             <xsl:value-of select="m:ci"/>
1020             <xsl:text>{</xsl:text>
1021             <br/>
1022             <xsl:call-template name="make_indent">
1023              <xsl:with-param name="current_indent" select="$current_indent + 2"/>
1024             </xsl:call-template>
1025             <xsl:for-each select="m:bvar">
1026                 <xsl:value-of select="m:ci"/>
1027                 <xsl:text>:</xsl:text>
1028                 <xsl:apply-templates select="m:type">
1029                  <xsl:with-param name="current_indent"
1030                     select="$current_indent + 5 + string-length(m:ci)"/>
1031                 </xsl:apply-templates>
1032                 <br/>
1033                 <xsl:call-template name="make_indent">
1034                  <xsl:with-param name="current_indent" select="$current_indent + 2"/>
1035                 </xsl:call-template>
1036                 <xsl:text>:=</xsl:text>
1037                 <xsl:apply-templates select="following-sibling::*[position() = 1]">
1038                  <xsl:with-param name="current_indent" select="$current_indent + 3"/>
1039                 </xsl:apply-templates>
1040
1041             </xsl:for-each>
1042             <br/>
1043               <xsl:call-template name="make_indent">
1044                <xsl:with-param name="current_indent" select="$current_indent + 2"/>
1045               </xsl:call-template>
1046             <xsl:text>}</xsl:text>
1047        </xsl:when>
1048        <xsl:otherwise>
1049         <xsl:apply-templates mode="inline" select="m:type"/>
1050        </xsl:otherwise>
1051        </xsl:choose>
1052       </xsl:when>
1053       <xsl:when test="$name='let_in'">
1054        <xsl:text>let&#x00a0;</xsl:text>
1055        <xsl:apply-templates select="m:bvar/m:ci"/>
1056        <xsl:text>&#x00a0;:=&#x00a0;</xsl:text>
1057        <xsl:apply-templates select="*[3]">
1058         <xsl:with-param name="current_indent" select="$current_indent+14"/>
1059        </xsl:apply-templates>
1060        <br/>
1061        <xsl:call-template name="make_indent">
1062         <xsl:with-param name="current_indent" select="$current_indent"/>
1063        </xsl:call-template>
1064        <xsl:text>in&#x00a0;</xsl:text>
1065        <xsl:apply-templates select="*[4]">
1066         <xsl:with-param name="current_indent" select="$current_indent+5"/>
1067        </xsl:apply-templates>
1068       </xsl:when>
1069
1070       <!-- ***************************************** -->
1071       <!-- *********** PROOF ELEMENTS ************** -->
1072       <!-- ***************************************** -->
1073       <!-- PROOF -->
1074       <xsl:when test="$name='proof'">
1075        <xsl:variable name="nonce" select="generate-id()"/>
1076        <xsl:variable name="freshid1" select="concat('a',$nonce)"/>
1077        <xsl:variable name="freshid2" select="concat('b',$nonce)"/>
1078        <xsl:variable name="freshid3" select="concat('c',$nonce)"/>
1079        <span ID="{$freshid1}">
1080         <xsl:apply-templates select="*[position()=2]">
1081          <xsl:with-param name="current_indent" select="$current_indent"/>
1082         </xsl:apply-templates>
1083         &#x00a0;
1084        </span>
1085        <xsl:choose>
1086         <xsl:when test="(preceding-sibling::*[1]/text()='letin1') or
1087                         (preceding-sibling::*[1]/text()='rw_step')">
1088          <br/>
1089          <xsl:call-template name="make_indent">
1090           <xsl:with-param name="current_indent" select="$current_indent"/>
1091          </xsl:call-template>
1092          <FONT color="red">we proved&#x00a0;</FONT>
1093         </xsl:when>
1094         <xsl:otherwise>
1095          <script>
1096           if(document.getElementById) {
1097            document.write('\
1098             <span ID="{$freshid2}">\
1099              <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>\
1100             </span>\
1101             <span ID="{$freshid3}">\
1102              <br/>\
1103              <xsl:call-template name="make_indent">
1104               <xsl:with-param name="current_indent" select="$current_indent"/>
1105              </xsl:call-template>\
1106              <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>\
1107             </span>\
1108            ');
1109            document.to_be_deleted.push('<xsl:value-of select="$freshid1"/>');
1110            document.to_be_deleted.push('<xsl:value-of select="$freshid3"/>');
1111            document.write('&#x00a0;');
1112           } else {
1113            document.write('\
1114             <br/>\
1115             <xsl:call-template name="make_indent">
1116              <xsl:with-param name="current_indent" select="$current_indent"/>
1117             </xsl:call-template>\
1118             <FONT color="red">we proved&#x00a0;</FONT>\
1119            ');
1120           }
1121          </script>
1122         </xsl:otherwise>
1123        </xsl:choose>
1124        <xsl:apply-templates select="*[position()=3]">
1125         <xsl:with-param name="current_indent" select="$current_indent + 16"/>
1126        </xsl:apply-templates>
1127       </xsl:when>
1128       <!-- letin1 -->
1129       <xsl:when test="$name='letin1'">
1130        <xsl:apply-templates select="*[position()=2]">
1131         <xsl:with-param name="current_indent" select="$current_indent"/>
1132        </xsl:apply-templates>
1133        <br/>
1134        <xsl:call-template name="make_indent">
1135         <xsl:with-param name="current_indent" select="$current_indent"/>
1136        </xsl:call-template>
1137        <xsl:apply-templates select="*[position()=3]">
1138         <xsl:with-param name="current_indent" select="$current_indent"/>
1139        </xsl:apply-templates>
1140       </xsl:when>
1141       <!-- letin -->
1142       <xsl:when test="$name='letin'">
1143        <xsl:for-each select="*[position()>1 and last()>position()]">
1144         <xsl:apply-templates select=".">
1145          <xsl:with-param name="current_indent" select="$current_indent"/>
1146         </xsl:apply-templates>
1147         <br/>
1148         <xsl:call-template name="make_indent">
1149          <xsl:with-param name="current_indent" select="$current_indent"/>
1150         </xsl:call-template>
1151        </xsl:for-each>
1152        <xsl:apply-templates select="*[position()=last()]">
1153         <xsl:with-param name="current_indent" select="$current_indent"/>
1154        </xsl:apply-templates>
1155       </xsl:when>
1156       <!-- Let -->
1157       <xsl:when test="$name='let'">
1158        (
1159        <xsl:apply-templates select="m:ci"/>
1160        )
1161        <xsl:apply-templates select="*[3]">
1162         <xsl:with-param name="current_indent" select="$current_indent + 7"/>
1163        </xsl:apply-templates>
1164       </xsl:when>
1165       <!-- rw_step -->
1166       <xsl:when test="$name='rw_step'">
1167        <xsl:choose>
1168         <xsl:when test="name(*[2])='m:apply'">
1169          <xsl:apply-templates select="*[2]">
1170           <xsl:with-param name="current_indent" select="$current_indent"/>
1171          </xsl:apply-templates>
1172         </xsl:when>
1173         <xsl:otherwise>
1174          <FONT color="red">Consider&#x00a0;</FONT>
1175          <xsl:apply-templates select="*[2]"/>
1176         </xsl:otherwise>
1177        </xsl:choose>
1178        <xsl:variable name="charlength_first">
1179         <xsl:apply-templates select="*[3]" mode="root_charcount"/>
1180        </xsl:variable>
1181        <xsl:variable name="charlength_second">
1182         <xsl:apply-templates select="*[4]" mode="root_charcount"/>
1183        </xsl:variable>
1184        <xsl:variable name="charlength_side_proof">
1185         <xsl:apply-templates select="*[5]" mode="root_charcount"/>
1186        </xsl:variable>
1187        <xsl:variable name="split1"
1188          select="($charlength_first + $charlength_second) > $framewidth"/>
1189        <xsl:variable name="split2"
1190          select="($charlength_second + $charlength_side_proof) > $framewidth"/>
1191      <!-- <xsl:value-of select="$current_indent"/> -->
1192      <!-- <xsl:value-of select="string($charlength_second)"/>  -->
1193      <!-- <xsl:value-of select="$charlength_side_proof"/>  -->
1194      <!-- <xsl:value-of select="$split2"/>  -->
1195        <br/>
1196        <xsl:call-template name="make_indent">
1197         <xsl:with-param name="current_indent" select="$current_indent"/>
1198        </xsl:call-template>
1199        <FONT color="red">Rewrite&#x00a0;</FONT>
1200        <xsl:apply-templates mode="inline" select="*[3]"/>
1201        <xsl:text>&#x00a0;</xsl:text>
1202        <xsl:if test="$split1">
1203        <br/>
1204        <xsl:call-template name="make_indent">
1205         <xsl:with-param name="current_indent" select="$current_indent + 2"/>
1206        </xsl:call-template>
1207        </xsl:if>
1208        <FONT color="red">with&#x00a0;</FONT>
1209        <xsl:apply-templates mode="inline" select="*[4]"/>
1210        <xsl:text>&#x00a0;</xsl:text>
1211        <xsl:if test="$split2">
1212        <br/>
1213        <xsl:call-template name="make_indent">
1214         <xsl:with-param name="current_indent" select="$current_indent + 2"/>
1215        </xsl:call-template>
1216        </xsl:if>
1217        <FONT color="red">by&#x00a0;</FONT>
1218        <xsl:apply-templates select="*[5]">
1219         <xsl:with-param name="current_indent" select="$current_indent+7"/>
1220        </xsl:apply-templates>
1221       </xsl:when>
1222       <!-- rewrite and apply -->
1223       <xsl:when test="$name='rewrite_and_apply'">
1224        <xsl:apply-templates select="*[2]">
1225         <xsl:with-param name="current_indent" select="$current_indent"/>
1226        </xsl:apply-templates>
1227        <br/>
1228        <xsl:call-template name="make_indent">
1229         <xsl:with-param name="current_indent" select="$current_indent"/>
1230        </xsl:call-template>
1231        <FONT color="red">Then apply it to&#x00a0;</FONT>
1232        <xsl:apply-templates select="*[position()>2]"/>
1233       </xsl:when>
1234       <!-- by_induction -->
1235       <xsl:when test="$name='by_induction'">
1236        <FONT color="red">We prove&#x00a0;</FONT>
1237        <xsl:apply-templates select="../*[3]">
1238         <xsl:with-param name="current_indent" select="$current_indent+18"/>
1239        </xsl:apply-templates>
1240        <br/>
1241        <xsl:call-template name="make_indent">
1242         <xsl:with-param name="current_indent" select="$current_indent"/>
1243        </xsl:call-template>
1244        <FONT color="red">by induction on&#x00a0;</FONT>
1245        <xsl:apply-templates select="*[position()=last()]/*[position()=last()]">
1246         <xsl:with-param name="current_indent" select="$current_indent+30"/>
1247        </xsl:apply-templates>
1248        <!--
1249        <br/>
1250        <xsl:call-template name="make_indent">
1251         <xsl:with-param name="current_indent" select="$current_indent"/>
1252        </xsl:call-template>
1253        <xsl:text>The induction property is</xsl:text>
1254        <br/>
1255        <xsl:call-template name="make_indent">
1256         <xsl:with-param name="current_indent" select="$current_indent"/>
1257        </xsl:call-template>
1258        <xsl:apply-templates select="*[3]">
1259         <xsl:with-param name="current_indent" select="$current_indent"/>
1260        </xsl:apply-templates>
1261        -->
1262        <xsl:apply-templates
1263             select="*[position()>3 and not(position()=last())]">
1264         <xsl:with-param name="current_indent" select="$current_indent+4"/>
1265        </xsl:apply-templates>
1266        <!-- <br/>
1267        <xsl:call-template name="make_indent">
1268         <xsl:with-param name="current_indent" select="$current_indent"/>
1269        </xsl:call-template>
1270        <xsl:text>End induction</xsl:text> -->
1271       </xsl:when>
1272       <!-- inductive_case -->
1273       <xsl:when test="$name='inductive_case'">
1274        <br/>
1275        <xsl:call-template name="make_indent">
1276         <xsl:with-param name="current_indent" select="$current_indent"/>
1277        </xsl:call-template>
1278        <FONT color="red">Case&#x00a0;</FONT>
1279        <xsl:apply-templates select="*[2]">
1280         <xsl:with-param name="current_indent" select="$current_indent +10"/>
1281        </xsl:apply-templates>
1282        <xsl:if test="*[3]/*[position()>1]">
1283         <br/>
1284         <xsl:call-template name="make_indent">
1285          <xsl:with-param name="current_indent" select="$current_indent+4"/>
1286         </xsl:call-template>
1287         <FONT color="red">By induction hypothesis, we have:</FONT>
1288         <xsl:for-each select="*[3]/*[position()>1]">
1289          <br/>
1290          <xsl:call-template name="make_indent">
1291           <xsl:with-param name="current_indent" select="$current_indent + 4"/>
1292          </xsl:call-template>
1293          <xsl:text>(</xsl:text>
1294          <xsl:apply-templates select="m:ci"/>
1295          <xsl:text>)&#x00a0;</xsl:text>
1296          <xsl:apply-templates select="m:type">
1297           <xsl:with-param name="current_indent" select="$current_indent + 8"/>
1298          </xsl:apply-templates>
1299         </xsl:for-each>
1300        </xsl:if>
1301        <br/>
1302         <xsl:call-template name="make_indent">
1303          <xsl:with-param name="current_indent" select="$current_indent + 4"/>
1304         </xsl:call-template>
1305        <xsl:apply-templates select="*[4]">
1306         <xsl:with-param name="current_indent" select="$current_indent +4"/>
1307        </xsl:apply-templates>
1308        <!-- <br/>
1309        <xsl:call-template name="make_indent">
1310         <xsl:with-param name="current_indent" select="$current_indent"/>
1311        </xsl:call-template>
1312        <xsl:text>End Case</xsl:text> -->
1313       </xsl:when>
1314       <!-- case_lhs  -->
1315       <xsl:when test="$name='case_lhs'">
1316        <xsl:choose>
1317         <xsl:when test="count(*)=2">
1318          <xsl:apply-templates mode="inline" select="*[2]"/>
1319         </xsl:when>
1320         <xsl:otherwise>
1321          <xsl:text>(</xsl:text>
1322          <xsl:apply-templates mode="inline" select="*[2]"/>
1323          <xsl:for-each select="m:bvar">
1324           <xsl:text>&#x00a0;</xsl:text>
1325           <xsl:apply-templates mode="inline" select="*[1]"/>
1326           <xsl:text>:</xsl:text>
1327           <xsl:apply-templates mode="inline" select="m:type/*[1]"/>
1328          </xsl:for-each>
1329          <xsl:text>)</xsl:text>
1330         </xsl:otherwise>
1331        </xsl:choose>
1332       </xsl:when>
1333       <!-- false_ind -->
1334       <xsl:when test="$name='false_ind'">
1335        <xsl:apply-templates select="*[3]">
1336         <xsl:with-param name="current_indent" select="$current_indent"/>
1337        </xsl:apply-templates>
1338        <br/>
1339        <xsl:call-template name="make_indent">
1340         <xsl:with-param name="current_indent" select="$current_indent"/>
1341        </xsl:call-template>
1342        <FONT color="red">Contradiction.</FONT>
1343       </xsl:when>
1344       <!-- and_ind -->
1345       <xsl:when test="$name='and_ind'">
1346        <xsl:choose>
1347         <xsl:when test="name(*[2])='m:apply'">
1348          <xsl:apply-templates select="*[2]">
1349           <xsl:with-param name="current_indent" select="$current_indent"/>
1350          </xsl:apply-templates>
1351         </xsl:when>
1352         <xsl:otherwise>
1353          <FONT color="red">Consider&#x00a0;</FONT>
1354          <xsl:apply-templates select="*[2]"/>
1355         </xsl:otherwise>
1356        </xsl:choose>
1357        <br/>
1358        <xsl:call-template name="make_indent">
1359         <xsl:with-param name="current_indent" select="$current_indent"/>
1360        </xsl:call-template>
1361        <FONT color="red">In particular, we have</FONT>
1362        <br/>
1363        <xsl:call-template name="make_indent">
1364         <xsl:with-param name="current_indent" select="$current_indent"/>
1365        </xsl:call-template>
1366        (
1367        <xsl:apply-templates select="*[3]"/>
1368        )&#x00a0;
1369        <xsl:apply-templates select="*[4]">
1370         <xsl:with-param name="current_indent" select="$current_indent + 9"/>
1371        </xsl:apply-templates>
1372        <br/>
1373        <xsl:call-template name="make_indent">
1374         <xsl:with-param name="current_indent" select="$current_indent"/>
1375        </xsl:call-template>
1376        (
1377        <xsl:apply-templates select="*[5]"/>
1378        )&#x00a0;
1379        <xsl:apply-templates select="*[6]">
1380         <xsl:with-param name="current_indent" select="$current_indent + 9"/>
1381        </xsl:apply-templates>
1382        <br/>
1383        <xsl:call-template name="make_indent">
1384         <xsl:with-param name="current_indent" select="$current_indent"/>
1385        </xsl:call-template>
1386        <xsl:apply-templates select="*[7]">
1387         <xsl:with-param name="current_indent" select="$current_indent"/>
1388        </xsl:apply-templates>
1389       </xsl:when>
1390       <!-- full_or_ind -->
1391       <xsl:when test="$name='full_or_ind'">
1392        <xsl:choose>
1393         <xsl:when test="name(*[2])='m:apply'">
1394          <xsl:apply-templates select="*[2]">
1395           <xsl:with-param name="current_indent" select="$current_indent"/>
1396          </xsl:apply-templates>
1397         </xsl:when>
1398         <xsl:otherwise>
1399          <FONT color="red">Consider&#x00a0;</FONT>
1400          <xsl:apply-templates select="*[2]"/>
1401         </xsl:otherwise>
1402        </xsl:choose>
1403        <br/>
1404        <xsl:call-template name="make_indent">
1405         <xsl:with-param name="current_indent" select="$current_indent"/>
1406        </xsl:call-template>
1407        <FONT color="red">We proceed by cases to prove&#x00a0;</FONT>
1408        <xsl:apply-templates select="*[3]"/>
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">Left: suppose&#x00a0;</FONT>
1414        <xsl:text>(</xsl:text>
1415        <xsl:value-of select="*[4]/m:bvar/m:ci"/>
1416        <xsl:text>)&#x00a0;</xsl:text>
1417        <xsl:apply-templates
1418             select="*[4]/m:bvar/m:type/*[1]"/>
1419        <br/>
1420        <xsl:call-template name="make_indent">
1421         <xsl:with-param name="current_indent" select="$current_indent+15"/>
1422        </xsl:call-template>
1423        <xsl:apply-templates
1424             select="*[4]/*[3]">
1425         <xsl:with-param name="current_indent" select="$current_indent+15"/>
1426        </xsl:apply-templates>
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        <FONT color="red">Right: suppose&#x00a0;</FONT>
1432        <xsl:text>(</xsl:text>
1433        <xsl:value-of select="*[5]/m:bvar/m:ci"/>
1434        <xsl:text>)&#x00a0;</xsl:text>
1435        <xsl:apply-templates
1436             select="*[5]/m:bvar/m:type/*[1]"/>
1437        <br/>
1438        <xsl:call-template name="make_indent">
1439         <xsl:with-param name="current_indent" select="$current_indent+16"/>
1440        </xsl:call-template>
1441        <xsl:apply-templates
1442             select="*[5]/*[3]">
1443         <xsl:with-param name="current_indent" select="$current_indent+16"/>
1444        </xsl:apply-templates>
1445       </xsl:when>
1446       <!-- or_ind -->
1447       <xsl:when test="$name='or_ind'">
1448        <xsl:choose>
1449         <xsl:when test="name(*[2])='m:apply'">
1450          <xsl:apply-templates select="*[2]">
1451           <xsl:with-param name="current_indent" select="$current_indent"/>
1452          </xsl:apply-templates>
1453         </xsl:when>
1454         <xsl:otherwise>
1455          <FONT color="red">Consider&#x00a0;</FONT>
1456          <xsl:apply-templates select="*[2]"/>
1457         </xsl:otherwise>
1458        </xsl:choose>
1459        <br/>
1460        <xsl:call-template name="make_indent">
1461         <xsl:with-param name="current_indent" select="$current_indent"/>
1462        </xsl:call-template>
1463        <FONT color="red">We prove&#x00a0;</FONT>
1464        <xsl:apply-templates select="*[3]"/>
1465        <FONT color="red">&#x00a0;by cases:</FONT>
1466        <br/>
1467        <xsl:call-template name="make_indent">
1468         <xsl:with-param name="current_indent" select="$current_indent"/>
1469        </xsl:call-template>
1470        Left:&#x00a0;
1471        <xsl:apply-templates select="*[4]">
1472         <xsl:with-param name="current_indent" select="$current_indent"/>
1473        </xsl:apply-templates>
1474        <br/>
1475        <xsl:call-template name="make_indent">
1476         <xsl:with-param name="current_indent" select="$current_indent"/>
1477        </xsl:call-template>
1478        Right:&#x00a0;
1479        <xsl:apply-templates select="*[5]">
1480         <xsl:with-param name="current_indent" select="$current_indent"/>
1481        </xsl:apply-templates>
1482       </xsl:when>
1483       <!-- Ex_ind -->
1484       <xsl:when test="$name='ex_ind'">
1485        <xsl:choose>
1486         <xsl:when test="name(*[2])='m:apply'">
1487          <xsl:apply-templates select="*[2]">
1488           <xsl:with-param name="current_indent" select="$current_indent"/>
1489          </xsl:apply-templates>
1490         </xsl:when>
1491         <xsl:otherwise>
1492          <FONT color="red">Consider&#x00a0;</FONT>
1493          <xsl:apply-templates select="*[2]">
1494           <xsl:with-param name="current_indent" select="$current_indent"/>
1495          </xsl:apply-templates>
1496         </xsl:otherwise>
1497        </xsl:choose>
1498        <br/>
1499        <xsl:call-template name="make_indent">
1500         <xsl:with-param name="current_indent" select="$current_indent"/>
1501        </xsl:call-template>
1502        <FONT color="red">Let&#x00a0;</FONT>
1503        <xsl:apply-templates mode="inline" select="*[3]"/>
1504        :
1505        <xsl:apply-templates mode="inline" select="*[4]"/>
1506        <FONT color="red">&#x00a0;such that</FONT>
1507        <br/>
1508        <xsl:call-template name="make_indent">
1509         <xsl:with-param name="current_indent" select="$current_indent"/>
1510        </xsl:call-template>
1511        (
1512        <xsl:apply-templates mode="inline" select="*[5]"/>
1513        )
1514        <xsl:apply-templates select="*[6]">
1515         <xsl:with-param name="current_indent" select="$current_indent +7"/>
1516        </xsl:apply-templates>
1517        <br/>
1518        <xsl:call-template name="make_indent">
1519         <xsl:with-param name="current_indent" select="$current_indent"/>
1520        </xsl:call-template>
1521        <xsl:apply-templates select="*[7]">
1522         <xsl:with-param name="current_indent" select="$current_indent"/>
1523        </xsl:apply-templates>
1524       </xsl:when>
1525       <!-- ***************************************** -->
1526       <!-- *********** LAMBDA ELEMENTS ************** -->
1527       <!-- ***************************************** -->
1528       <xsl:when test="$name='subst'">
1529        <xsl:apply-templates select="*[3]"/>
1530        <xsl:text>[</xsl:text>
1531        <xsl:apply-templates select="*[4]"/>
1532        <xsl:choose>
1533        <xsl:when test="$uri != ''">
1534         <a href="{$uri}">
1535          <xsl:call-template name="mksymbol-1">
1536           <xsl:with-param name="symbol" select="$name"/>
1537           <xsl:with-param name="color" select="'blue'"/>
1538           <xsl:with-param name="size" select="'+0'"/>
1539          </xsl:call-template>
1540         </a>
1541        </xsl:when>
1542        <xsl:otherwise>
1543          <xsl:call-template name="mksymbol-1">
1544           <xsl:with-param name="symbol" select="$name"/>
1545           <xsl:with-param name="color" select="'blue'"/>
1546           <xsl:with-param name="size" select="'+0'"/>
1547          </xsl:call-template>
1548        </xsl:otherwise>
1549        </xsl:choose>
1550        <xsl:apply-templates select="*[2]"/>
1551        <xsl:text>]</xsl:text>
1552       </xsl:when>
1553
1554       <xsl:when test="$name='lift_with_base'">
1555        <SUB>
1556        <xsl:apply-templates select="*[3]" mode="inline"/>
1557        </SUB>
1558        <xsl:choose>
1559        <xsl:when test="$uri != ''">
1560         <a href="{$uri}">
1561          <xsl:call-template name="mksymbol-1">
1562           <xsl:with-param name="symbol" select="$name"/>
1563           <xsl:with-param name="color" select="'green'"/>
1564           <xsl:with-param name="size" select="'+0'"/>
1565          </xsl:call-template>
1566         </a>
1567        </xsl:when>
1568        <xsl:otherwise>
1569          <xsl:call-template name="mksymbol-1">
1570           <xsl:with-param name="symbol" select="$name"/>
1571           <xsl:with-param name="color" select="'green'"/>
1572           <xsl:with-param name="size" select="'+0'"/>
1573          </xsl:call-template>
1574        </xsl:otherwise>
1575        </xsl:choose>
1576        <SUP>
1577        <xsl:apply-templates select="*[4]" mode="inline"/>
1578        </SUP>
1579        <xsl:text>(</xsl:text>
1580        <xsl:apply-templates select="*[2]" mode="inline"/>
1581        <xsl:text>)</xsl:text>
1582       </xsl:when>
1583
1584       <xsl:when test="$name='lift'">
1585        <xsl:choose>
1586        <xsl:when test="$uri != ''">
1587         <a href="{$uri}">
1588          <xsl:call-template name="mksymbol-1">
1589           <xsl:with-param name="symbol" select="$name"/>
1590           <xsl:with-param name="color" select="'green'"/>
1591           <xsl:with-param name="size" select="'+0'"/>
1592          </xsl:call-template>
1593         </a>
1594        </xsl:when>
1595        <xsl:otherwise>
1596          <xsl:call-template name="mksymbol-1">
1597           <xsl:with-param name="symbol" select="$name"/>
1598           <xsl:with-param name="color" select="'green'"/>
1599           <xsl:with-param name="size" select="'+0'"/>
1600          </xsl:call-template>
1601        </xsl:otherwise>
1602        </xsl:choose>
1603        <SUP>
1604        <xsl:apply-templates select="*[2]" mode="inline"/>
1605        </SUP>
1606        <xsl:text>(</xsl:text>
1607        <xsl:apply-templates select="*[3]" mode="inline"/>
1608        <xsl:text>)</xsl:text>
1609       </xsl:when>
1610
1611       <!-- reduction -->
1612       <xsl:when test="$name='beta_red1'">
1613        <xsl:apply-templates select="*[2]" mode="inline"/>
1614        <xsl:choose>
1615        <xsl:when test="$uri != ''">
1616         <a href="{$uri}">
1617          <xsl:call-template name="mksymbol-1">
1618           <xsl:with-param name="symbol" select="$name"/>
1619           <xsl:with-param name="color" select="'green'"/>
1620           <xsl:with-param name="size" select="'+0'"/>
1621          </xsl:call-template>
1622          <SUB>
1623          <xsl:call-template name="mksymbol-1">
1624           <xsl:with-param name="symbol" select="'beta'"/>
1625           <xsl:with-param name="color" select="'green'"/>
1626           <xsl:with-param name="size" select="'+0'"/>
1627          </xsl:call-template>
1628          </SUB>
1629         </a>
1630        </xsl:when>
1631        <xsl:otherwise>
1632          <xsl:call-template name="mksymbol-1">
1633           <xsl:with-param name="symbol" select="$name"/>
1634           <xsl:with-param name="color" select="'green'"/>
1635           <xsl:with-param name="size" select="'+0'"/>
1636          </xsl:call-template>
1637          <SUB>
1638          <xsl:call-template name="mksymbol-1">
1639           <xsl:with-param name="symbol" select="'beta'"/>
1640           <xsl:with-param name="color" select="'green'"/>
1641           <xsl:with-param name="size" select="'+0'"/>
1642          </xsl:call-template>
1643          </SUB>
1644        </xsl:otherwise>
1645        </xsl:choose>
1646        <xsl:apply-templates select="*[3]" mode="inline"/>
1647       </xsl:when>
1648
1649       <xsl:when test="$name='beta_red'">
1650        <xsl:apply-templates select="*[2]" mode="inline"/>
1651        <xsl:choose>
1652        <xsl:when test="$uri != ''">
1653         <a href="{$uri}">
1654          <xsl:call-template name="mksymbol-1">
1655           <xsl:with-param name="symbol" select="$name"/>
1656           <xsl:with-param name="color" select="'green'"/>
1657           <xsl:with-param name="size" select="'+0'"/>
1658          </xsl:call-template>
1659          <SUB>
1660          <xsl:call-template name="mksymbol-1">
1661           <xsl:with-param name="symbol" select="'beta'"/>
1662           <xsl:with-param name="color" select="'green'"/>
1663           <xsl:with-param name="size" select="'+0'"/>
1664          </xsl:call-template>
1665          <xsl:text>*</xsl:text>
1666          </SUB>
1667         </a>
1668        </xsl:when>
1669        <xsl:otherwise>
1670          <xsl:call-template name="mksymbol-1">
1671           <xsl:with-param name="symbol" select="$name"/>
1672           <xsl:with-param name="color" select="'green'"/>
1673           <xsl:with-param name="size" select="'+0'"/>
1674          </xsl:call-template>
1675          <SUB>
1676          <xsl:call-template name="mksymbol-1">
1677           <xsl:with-param name="symbol" select="'beta'"/>
1678           <xsl:with-param name="color" select="'green'"/>
1679           <xsl:with-param name="size" select="'+0'"/>
1680          </xsl:call-template>
1681          <xsl:text>*</xsl:text>
1682          </SUB>
1683        </xsl:otherwise>
1684        </xsl:choose>
1685        <xsl:apply-templates select="*[3]" mode="inline"/>
1686       </xsl:when>
1687
1688       <xsl:when test="$name='par_beta_red1'">
1689        <xsl:apply-templates select="*[2]" mode="inline"/>
1690        <xsl:choose>
1691        <xsl:when test="$uri != ''">
1692         <a href="{$uri}">
1693          <xsl:call-template name="mksymbol-1">
1694           <xsl:with-param name="symbol" select="$name"/>
1695           <xsl:with-param name="color" select="'green'"/>
1696           <xsl:with-param name="size" select="'+0'"/>
1697          </xsl:call-template>
1698          <SUB>
1699          <xsl:call-template name="mksymbol-1">
1700           <xsl:with-param name="symbol" select="'beta'"/>
1701           <xsl:with-param name="color" select="'green'"/>
1702           <xsl:with-param name="size" select="'+0'"/>
1703          </xsl:call-template>
1704          </SUB>
1705         </a>
1706        </xsl:when>
1707        <xsl:otherwise>
1708          <xsl:call-template name="mksymbol-1">
1709           <xsl:with-param name="symbol" select="$name"/>
1710           <xsl:with-param name="color" select="'green'"/>
1711           <xsl:with-param name="size" select="'+0'"/>
1712          </xsl:call-template>
1713          <SUB>
1714          <xsl:call-template name="mksymbol-1">
1715           <xsl:with-param name="symbol" select="'beta'"/>
1716           <xsl:with-param name="color" select="'green'"/>
1717           <xsl:with-param name="size" select="'+0'"/>
1718          </xsl:call-template>
1719          </SUB>
1720        </xsl:otherwise>
1721        </xsl:choose>
1722        <xsl:apply-templates select="*[3]" mode="inline"/>
1723       </xsl:when>
1724
1725       <xsl:when test="$name='par_beta_red'">
1726        <xsl:apply-templates select="*[2]" mode="inline"/>
1727        <xsl:choose>
1728        <xsl:when test="$uri != ''">
1729         <a href="{$uri}">
1730          <xsl:call-template name="mksymbol-1">
1731           <xsl:with-param name="symbol" select="$name"/>
1732           <xsl:with-param name="color" select="'green'"/>
1733           <xsl:with-param name="size" select="'+0'"/>
1734          </xsl:call-template>
1735          <SUB>
1736          <xsl:call-template name="mksymbol-1">
1737           <xsl:with-param name="symbol" select="'beta'"/>
1738           <xsl:with-param name="color" select="'green'"/>
1739           <xsl:with-param name="size" select="'+0'"/>
1740          </xsl:call-template>
1741          <xsl:text>*</xsl:text>
1742          </SUB>
1743         </a>
1744        </xsl:when>
1745        <xsl:otherwise>
1746          <xsl:call-template name="mksymbol-1">
1747           <xsl:with-param name="symbol" select="$name"/>
1748           <xsl:with-param name="color" select="'green'"/>
1749           <xsl:with-param name="size" select="'+0'"/>
1750          </xsl:call-template>
1751          <SUB>
1752          <xsl:call-template name="mksymbol-1">
1753           <xsl:with-param name="symbol" select="'beta'"/>
1754           <xsl:with-param name="color" select="'green'"/>
1755           <xsl:with-param name="size" select="'+0'"/>
1756          </xsl:call-template>
1757          <xsl:text>*</xsl:text>
1758          </SUB>
1759        </xsl:otherwise>
1760        </xsl:choose>
1761        <xsl:apply-templates select="*[3]" mode="inline"/>
1762       </xsl:when>
1763
1764       <!-- forgetful -->
1765       <xsl:when test="$name='forgetful'">
1766        <xsl:choose>
1767        <xsl:when test="$uri != ''">
1768         <a href="{$uri}">|</a>
1769        </xsl:when>
1770        <xsl:otherwise>
1771         |
1772        </xsl:otherwise>
1773        </xsl:choose>
1774        <xsl:apply-templates select="*[2]" mode="inline"/>
1775        <xsl:choose>
1776        <xsl:when test="$uri != ''">
1777         <a href="{$uri}">|</a>
1778        </xsl:when>
1779        <xsl:otherwise>
1780         |
1781        </xsl:otherwise>
1782        </xsl:choose>
1783       </xsl:when>
1784
1785       <!-- boolean algebra of redexes -->
1786
1787       <!-- isomorphic -->
1788       <xsl:when test="$name='isomorphic'">
1789        <xsl:apply-templates select="*[2]" mode="inline"/>
1790        <xsl:choose>
1791        <xsl:when test="$uri != ''">
1792         <a href="{$uri}">
1793          <xsl:call-template name="mksymbol-1">
1794           <xsl:with-param name="symbol" select="$name"/>
1795           <xsl:with-param name="color" select="'green'"/>
1796           <xsl:with-param name="size" select="'+0'"/>
1797          </xsl:call-template>
1798         </a>
1799        </xsl:when>
1800        <xsl:otherwise>
1801          <xsl:call-template name="mksymbol-1">
1802           <xsl:with-param name="symbol" select="$name"/>
1803           <xsl:with-param name="color" select="'green'"/>
1804           <xsl:with-param name="size" select="'+0'"/>
1805          </xsl:call-template>
1806        </xsl:otherwise>
1807        </xsl:choose>
1808        <xsl:apply-templates select="*[3]" mode="inline"/>
1809       </xsl:when>
1810
1811       <!-- INTERP -->
1812       <xsl:when test="$name='interp'">
1813          <font color="green">[</font>
1814             <xsl:apply-templates select="*[2]"/>
1815          <font color="green">]</font>
1816       </xsl:when>
1817
1818      </xsl:choose>
1819 </xsl:template>
1820
1821 <!-- LAMBDA -->
1822
1823 <xsl:template match="m:lambda">
1824 <xsl:param name="current_indent" select="0"/>
1825     <xsl:variable name="charlength">
1826      <xsl:apply-templates select="*[position()=1]" mode="charcount"/>
1827      <!-- <xsl:apply-templates select="." mode="charcount"/> -->
1828     </xsl:variable>
1829     <!-- <xsl:value-of select="$charlength"/> -->
1830     <!-- <xsl:value-of select="$current_indent"/> -->
1831      <xsl:choose>
1832      <xsl:when test="$charlength > $framewidth">
1833        <!-- &#x03bb; -->
1834        <xsl:call-template name="mksymbol-1">
1835         <xsl:with-param name="symbol" select="'lambda'"/>
1836         <xsl:with-param name="color" select="'red'"/>
1837         <xsl:with-param name="size" select="'+2'"/>
1838        </xsl:call-template>
1839        <xsl:apply-templates select="m:bvar/m:ci"/>
1840        <xsl:text>:</xsl:text>
1841        <xsl:apply-templates select="m:bvar/m:type">
1842         <xsl:with-param name="current_indent"
1843            select="$current_indent + 4 + 2*string-length(m:bvar/m:ci)"/>
1844        </xsl:apply-templates><br/>
1845        <xsl:call-template name="make_indent">
1846         <xsl:with-param name="current_indent" select="$current_indent + 2"/>
1847        </xsl:call-template>
1848        <xsl:text>.</xsl:text>
1849        <xsl:apply-templates select="*[position()=2]">
1850         <xsl:with-param name="current_indent" select="$current_indent + 2"/>
1851        </xsl:apply-templates>
1852      </xsl:when>
1853      <xsl:otherwise>
1854       <xsl:apply-templates mode="inline" select="."/>
1855      </xsl:otherwise>
1856      </xsl:choose>
1857 </xsl:template>
1858
1859 <!-- href -->
1860 <xsl:template match="m:ci">
1861  <xsl:choose>
1862   <xsl:when test="boolean(@definitionURL)">
1863    <a href="{@definitionURL}">
1864    <xsl:apply-templates/>
1865    </a>
1866   </xsl:when>
1867   <xsl:otherwise>
1868    <xsl:value-of select="."/>
1869   </xsl:otherwise>
1870  </xsl:choose>
1871 </xsl:template>
1872
1873 <!-- CHAR COUNTING -->
1874
1875 <!-- enter this counting mode selecting the root -->
1876 <xsl:template match="*" mode="root_charcount">
1877 <xsl:param name="incurrent_length" select="0"/>
1878  <xsl:choose>
1879   <xsl:when test="count(*)=0">
1880    <xsl:value-of select="0"/>
1881   </xsl:when>
1882   <xsl:when test="name()='m:ci'">
1883    <xsl:value-of select="string-length()"/>
1884   </xsl:when>
1885   <xsl:otherwise>
1886    <xsl:apply-templates select="*[1]" mode="charcount">
1887     <xsl:with-param name="incurrent_length" select="$incurrent_length"/>
1888    </xsl:apply-templates>
1889   </xsl:otherwise>
1890  </xsl:choose>
1891 </xsl:template>
1892
1893 <!-- enter this mode selecting the first child -->
1894
1895 <xsl:template match="m:ci|m:csymbol" mode="charcount">
1896 <xsl:param name="incurrent_length" select="0"/>
1897     <xsl:choose>
1898     <xsl:when test="$framewidth >= ($incurrent_length + string-length())">
1899      <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>
1900      <xsl:choose>
1901      <xsl:when test="string($siblength) = &quot;&quot;">
1902       <xsl:value-of select="$incurrent_length + string-length()"/>
1903      </xsl:when>
1904      <xsl:otherwise>
1905       <xsl:value-of select="number($siblength)"/>
1906      </xsl:otherwise>
1907      </xsl:choose>
1908     </xsl:when>
1909     <xsl:otherwise>
1910      <xsl:value-of select="$incurrent_length + string-length()"/>
1911     </xsl:otherwise>
1912     </xsl:choose>
1913 </xsl:template>
1914
1915 <xsl:template match="*" mode="charcount">
1916  <xsl:param name="incurrent_length" select="0"/>
1917  <xsl:choose>
1918   <xsl:when test="count(child::*) = 0">
1919    <xsl:value-of select="$incurrent_length"/>
1920   </xsl:when>
1921   <xsl:otherwise>
1922     <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>
1923     <xsl:choose>
1924      <xsl:when test="$framewidth >= number($childlength)">
1925       <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>
1926       <xsl:choose>
1927        <xsl:when test="string($siblength) = &quot;&quot;">
1928         <xsl:value-of select="number($childlength)"/>
1929        </xsl:when>
1930        <xsl:otherwise>
1931         <xsl:value-of select="number($siblength)"/>
1932        </xsl:otherwise>
1933       </xsl:choose>
1934      </xsl:when>
1935      <xsl:otherwise>
1936       <xsl:value-of select="number($childlength)"/>
1937      </xsl:otherwise>
1938     </xsl:choose>
1939   </xsl:otherwise>
1940  </xsl:choose>
1941 </xsl:template>
1942
1943
1944 <!--***********************************************************************-->
1945 <!-- OBJECTS                                                               -->
1946 <!--***********************************************************************-->
1947
1948 <!-- DEFINITION -->
1949
1950 <xsl:template match="Definition">
1951 <xsl:param name="current_indent" select="0"/>
1952 <p>
1953 DEFINITION <xsl:value-of select="@name"/>(<xsl:if test="string(./Params) != &quot;&quot;"><xsl:value-of select="Params"/></xsl:if>)<br/>
1954 TYPE =<br/>
1955       <xsl:call-template name="make_indent">
1956        <xsl:with-param name="current_indent" select="$current_indent + 7"/>
1957       </xsl:call-template>
1958        <xsl:apply-templates select="type/*[1]">
1959         <xsl:with-param name="current_indent" select="$current_indent + 7"/>
1960        </xsl:apply-templates><br/>
1961 BODY =<br/>
1962       <xsl:call-template name="make_indent">
1963        <xsl:with-param name="current_indent" select="$current_indent + 7"/>
1964       </xsl:call-template>
1965        <xsl:apply-templates select="body/*[1]">
1966         <xsl:with-param name="current_indent" select="$current_indent + 7"/>
1967        </xsl:apply-templates>
1968 </p>
1969 </xsl:template>
1970
1971 <!-- AXIOM -->
1972
1973 <xsl:template match="Axiom">
1974 <xsl:param name="current_indent" select="0"/>
1975 <p>
1976 AXIOM <xsl:value-of select="@name"/>(<xsl:if test="string(./Params) != &quot;&quot;"><xsl:value-of select="Params"/></xsl:if>)<br/>
1977 TYPE =<br/>
1978       <xsl:call-template name="make_indent">
1979        <xsl:with-param name="current_indent" select="$current_indent + 7"/>
1980       </xsl:call-template>
1981 <xsl:apply-templates select="type/*[1]">
1982           <xsl:with-param name="current_indent" select="$current_indent + 7"/>
1983        </xsl:apply-templates>
1984 </p>
1985 </xsl:template>
1986
1987 <!-- UNFINISHED PROOF -->
1988
1989 <xsl:template match="CurrentProof">
1990 <xsl:param name="current_indent" select="0"/>
1991 <p>
1992 UNFINISHED PROOF <xsl:value-of select="@name"/>(<xsl:if test="string(./Params) != &quot;&quot;"><xsl:value-of select="Params"/></xsl:if>)<br/>
1993 THESIS:  <xsl:apply-templates select="type/*[1]">
1994           <xsl:with-param name="current_indent" select="$current_indent + 8"/>
1995          </xsl:apply-templates><br/>
1996 CONJECTURES:
1997       <xsl:for-each select="Conjecture">
1998       <br/>
1999       <xsl:call-template name="make_indent">
2000        <xsl:with-param name="current_indent" select="$current_indent + 8"/>
2001       </xsl:call-template>
2002       <xsl:value-of select="./@no"/> :
2003       <xsl:apply-templates select="./*[1]">
2004        <xsl:with-param name="current_indent" select="$current_indent + 11"/>
2005       </xsl:apply-templates>
2006       </xsl:for-each>
2007       <br/>
2008 PROOF:
2009       <xsl:apply-templates select="body/*[1]">
2010         <xsl:with-param name="current_indent" select="$current_indent + 8"/>
2011       </xsl:apply-templates>
2012 </p>
2013 </xsl:template>
2014
2015 <!-- MUTUAL INDUCTIVE DEFINITION -->
2016
2017 <xsl:template match="InductiveDefinition">
2018 <xsl:param name="current_indent" select="0"/>
2019 <p>
2020      <xsl:for-each select="InductiveType">
2021          <xsl:choose>
2022          <xsl:when test="position() = 1">
2023           <xsl:choose>
2024           <xsl:when test="string(./@inductive) = &quot;true&quot;">
2025           INDUCTIVE DEFINITION
2026           </xsl:when>
2027           <xsl:otherwise>
2028           COINDUCTIVE DEFINITION
2029           </xsl:otherwise>
2030           </xsl:choose>
2031          </xsl:when>
2032          <xsl:otherwise>
2033           AND
2034          </xsl:otherwise>
2035          </xsl:choose>
2036          <xsl:value-of select="./@name"/>(<xsl:if test="string(../Params) != &quot;&quot;"><xsl:value-of select="../Params"/></xsl:if>)
2037          [
2038           <xsl:if test="string(../Param) != &quot;&quot;">
2039            <xsl:for-each select="../Param">
2040             <xsl:value-of select="./@name"/>
2041             :
2042             <xsl:apply-templates select="*"/>
2043            </xsl:for-each>
2044           </xsl:if>
2045          ] <br/>
2046          OF ARITY
2047          <xsl:apply-templates select="./arity/*[1]">
2048           <xsl:with-param name="current_indent" select="$current_indent + 9"/>
2049          </xsl:apply-templates> <br/>
2050          BUILT FROM:
2051       <xsl:for-each select="./Constructor">
2052       <br/>
2053       <xsl:call-template name="make_indent">
2054        <xsl:with-param name="current_indent" select="$current_indent + 3"/>
2055       </xsl:call-template>
2056          <xsl:choose>
2057          <xsl:when test="position() = 1">
2058          <xsl:text>&#x00A0;&#x00A0;</xsl:text>
2059          </xsl:when>
2060          <xsl:otherwise>
2061          <xsl:text>| </xsl:text>
2062          </xsl:otherwise>
2063          </xsl:choose>
2064          <xsl:value-of select="./@name"/>
2065          <xsl:text>: </xsl:text>
2066          <xsl:apply-templates select="./*[1]">
2067           <xsl:with-param name="current_indent" select="$current_indent + 2*string-length(./@name) + 5"/>
2068          </xsl:apply-templates>
2069       </xsl:for-each>
2070      </xsl:for-each>
2071 </p>
2072 </xsl:template>
2073
2074 <!-- VARIABLE -->
2075
2076 <xsl:template match="Variable">
2077 <xsl:param name="current_indent" select="0"/>
2078 <p>
2079 VARIABLE <xsl:value-of select="@name"/><br/>
2080 TYPE = <xsl:apply-templates select="type/*[1]">
2081           <xsl:with-param name="current_indent" select="$current_indent + 7"/>
2082        </xsl:apply-templates>
2083 </p>
2084 </xsl:template>
2085
2086 <!--***********************************************************************-->
2087 <!-- SECTIONS                                                              -->
2088 <!--***********************************************************************-->
2089
2090 <!-- SECTION -->
2091
2092 <xsl:template match="SECTION">
2093 <xsl:param name="current_indent" select="0"/>
2094  <h1>BEGIN OF SECTION</h1>
2095   <xsl:apply-templates/>
2096  <h1>END OF SECTION</h1>
2097 </xsl:template>
2098
2099 </xsl:stylesheet>