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