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