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