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