helm/style/content_to_html.xsl

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