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