helm/style/content_to_html.xsl

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