helm/style/content_to_html.xsl

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