<?xml version="1.0"?>
+<!-- Copyright (C) 2000, HELM Team -->
+<!-- -->
+<!-- This file is part of HELM, an Hypertextual, Electronic -->
+<!-- Library of Mathematics, developed at the Computer Science -->
+<!-- Department, University of Bologna, Italy. -->
+<!-- -->
+<!-- HELM is free software; you can redistribute it and/or -->
+<!-- modify it under the terms of the GNU General Public License -->
+<!-- as published by the Free Software Foundation; either version 2 -->
+<!-- of the License, or (at your option) any later version. -->
+<!-- -->
+<!-- HELM is distributed in the hope that it will be useful, -->
+<!-- but WITHOUT ANY WARRANTY; without even the implied warranty of -->
+<!-- MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE. See the -->
+<!-- GNU General Public License for more details. -->
+<!-- -->
+<!-- You should have received a copy of the GNU General Public License -->
+<!-- along with HELM; if not, write to the Free Software -->
+<!-- Foundation, Inc., 59 Temple Place - Suite 330, Boston, -->
+<!-- MA 02111-1307, USA. -->
+<!-- -->
+<!-- For details, see the HELM World-Wide-Web page, -->
+<!-- http://cs.unibo.it/helm/. -->
+
<xsl:stylesheet version="1.0" xmlns:xsl="http://www.w3.org/1999/XSL/Transform"
xmlns:m="http://www.w3.org/1998/Math/MathML">
<!--***********************************************************************-->
<!-- From MathML content to HTML -->
-<!-- HELM Group: Asperti, Padovani, Sacerdoti, Schena -->
+<!-- HELM Group: Asperti, Padovani, Sacerdoti, Schena, Guidi -->
<!--***********************************************************************-->
+<xsl:param name="CICURI" select="''"/>
+<xsl:param name="type" select="'standalone'"/>
+<xsl:param name="UNICODEvsSYMBOL" select="'symbol'"/>
<xsl:include href="html_init.xsl"/>
<xsl:include href="html_set.xsl"/>
<xsl:include href="html_reals.xsl"/>
-
-<!-- <xsl:variable name="absPath">http://localhost:8081/get?url=</xsl:variable>-->
-<xsl:variable name="header" select="document('http://localhost:8081/conf')/html_link"/>
-
<xsl:variable name="showcast" select="0"/>
-
<!--***********************************************************************-->
<!-- HTML Head and Body -->
<!--***********************************************************************-->
-<xsl:output method="html"/>
+<!-- <xsl:output method="html" encoding="iso-8859-1"/> -->
-<xsl:variable name="framewidth" select="36"/>
+<!-- document needs method="xml" and searches locally for the dtd if -->
+<!-- doctype-system is specified (the dtd must exist locally for parsing). -->
+<!-- For having output html must be media-type="html" and for having the -->
+<!-- correct <br /> you must specify at least the remote dtd by means of -->
+<!-- doctype-public -->
+<xsl:output
+ method="xml"
+ encoding="iso-8859-1"
+ media-type="text/html"
+ doctype-public="-//W3C//DTD XHTML 1.0 Transitional//EN" />
+
+<xsl:variable name="framewidth" select="55"/>
+
+<xsl:template name="mksymbol-1">
+ <xsl:param name="symbol" select="''"/>
+ <xsl:param name="color" select="''"/>
+ <xsl:param name="size" select="''"/>
+ <xsl:choose>
+ <xsl:when test="$UNICODEvsSYMBOL = 'symbol'">
+ <xsl:variable name="fontsymbol">
+ <xsl:choose>
+ <xsl:when test="$symbol = 'forall'">
+ <xsl:value-of select="'"'"/>
+ </xsl:when>
+ <xsl:when test="$symbol = 'lambda'">
+ <xsl:value-of select="'l'"/>
+ </xsl:when>
+ <xsl:when test="$symbol = 'prod'">
+ <xsl:value-of select="'Õ'"/>
+ </xsl:when>
+ <xsl:when test="$symbol = 'arrow'">
+ <xsl:value-of select="'®'"/>
+ </xsl:when>
+ <xsl:when test="$symbol = 'RightArrow'">
+ <xsl:value-of select="'Þ'"/>
+ </xsl:when>
+ <xsl:when test="$symbol = 'subst'">
+ <xsl:value-of select="'¬'"/>
+ </xsl:when>
+ <xsl:when test="$symbol = 'lift' or $symbol = 'lift_with_base'">
+ <xsl:value-of select="'­'"/>
+ </xsl:when>
+ <xsl:when test="$symbol = 'beta_red' or $symbol = 'beta_red1'">
+ <xsl:value-of select="'®'"/>
+ </xsl:when>
+ <xsl:when test="$symbol = 'beta'">
+ <xsl:value-of select="'b'"/>
+ </xsl:when>
+ <xsl:when test="$symbol = 'par_beta_red' or $symbol = 'par_beta_red1'">
+ <xsl:value-of select="'Þ'"/>
+ </xsl:when>
+ <xsl:when test="$symbol = 'isomorphic'">
+ <xsl:value-of select="'@'"/>
+ </xsl:when>
+ <xsl:otherwise>
+ <xsl:text>???</xsl:text>
+ </xsl:otherwise>
+ </xsl:choose>
+ </xsl:variable>
+ <FONT FACE="symbol" SIZE="{$size}" color="{$color}">
+ <xsl:value-of select="$fontsymbol"/>
+ </FONT>
+ </xsl:when>
+ <xsl:otherwise>
+ <xsl:variable name="unicodesymbol">
+ <xsl:choose>
+ <xsl:when test="$symbol = 'forall'">
+ <xsl:value-of select="'∀'"/>
+ </xsl:when>
+ <xsl:when test="$symbol = 'lambda'">
+ <xsl:value-of select="'λ'"/>
+ </xsl:when>
+ <xsl:when test="$symbol = 'prod'">
+ <xsl:value-of select="'Π'"/>
+ </xsl:when>
+ <xsl:when test="$symbol = 'arrow'">
+ <xsl:value-of select="'→'"/>
+ </xsl:when>
+ <xsl:when test="$symbol = 'RightArrow'">
+ <xsl:value-of select="'⇒'"/>
+ </xsl:when>
+ <xsl:when test="$symbol = 'subst'">
+ <xsl:value-of select="'←'"/>
+ </xsl:when>
+ <xsl:when test="$symbol = 'lift' or $symbol = 'lift_with_base'">
+ <xsl:value-of select="'↑'"/>
+ </xsl:when>
+ <xsl:when test="$symbol = 'beta_red' or $symbol = 'beta_red1'">
+ <xsl:value-of select="'→'"/>
+ </xsl:when>
+ <xsl:when test="$symbol = 'beta'">
+ <xsl:value-of select="'β'"/>
+ </xsl:when>
+ <xsl:when test="$symbol = 'par_beta_red' or $symbol = 'par_beta_red1'">
+ <xsl:value-of select="'⇒'"/>
+ </xsl:when>
+ <xsl:when test="$symbol = 'isomorphic'">
+ <xsl:value-of select="'≅'"/>
+ </xsl:when>
+ <xsl:otherwise>
+ <xsl:text>???</xsl:text>
+ </xsl:otherwise>
+ </xsl:choose>
+ </xsl:variable>
+ <FONT color="{$color}">
+ <xsl:value-of select="$unicodesymbol"/>
+ </FONT>
+ </xsl:otherwise>
+ </xsl:choose>
+</xsl:template>
<xsl:template match="/">
<xsl:param name="current_indent" select="0"/>
- <html>
- <head></head>
- <body>
- <xsl:apply-templates>
- <xsl:with-param name="current_indent" select="0"/>
- </xsl:apply-templates>
- </body>
- </html>
+ <xsl:choose>
+ <xsl:when test="$type = 'standalone'">
+ <html>
+ <head>
+ <title> <xsl:value-of select="$CICURI"/> </title> <!-- FG -->
+ <style> A { text-decoration: none } </style>
+ <script>
+ <xsl:text disable-output-escaping="yes">
+ <![CDATA[
+ function Hide(which){
+ if (!document.getElementById)
+ return
+ which.style.display="none"
+ }
+
+ function Show(which){
+ if (!document.getElementById)
+ return
+ which.style.display=""
+ }
+
+ document.to_be_deleted = new Array();
+ ]]>
+ </xsl:text>
+ </script>
+ </head>
+ <body bgcolor="white">
+ <xsl:attribute name="onLoad">
+ if(document.getElementById)
+ for(var i=0;i<document.to_be_deleted.length;i++)
+ Hide(document.getElementById(document.to_be_deleted[i]));
+ </xsl:attribute>
+ <xsl:apply-templates>
+ <xsl:with-param name="current_indent" select="0"/>
+ </xsl:apply-templates>
+ </body>
+ </html>
+ </xsl:when>
+ <xsl:otherwise>
+ <to_be_embedded>
+ <xsl:apply-templates>
+ <xsl:with-param name="current_indent" select="0"/>
+ </xsl:apply-templates>
+ </to_be_embedded>
+ </xsl:otherwise>
+ </xsl:choose>
</xsl:template>
<!--***********************************************************************-->
<xsl:template name="make_indent">
<xsl:param name="current_indent" select="0"/>
<xsl:if test="$current_indent > 0">
- <xsl:text> </xsl:text>
+ <xsl:text> </xsl:text>
<xsl:call-template name="make_indent">
<xsl:with-param name="current_indent" select="$current_indent - 1"/>
</xsl:call-template>
</xsl:template>
<!-- Syntactic Sugar -->
-
<xsl:template match="m:type">
<xsl:param name="current_indent" select="0"/>
<xsl:apply-templates>
</xsl:apply-templates>
</xsl:template>
+<!--*********************************************************************-->
+<!-- INLINE MODE -->
+<!--*********************************************************************-->
+
+<!-- href -->
+<xsl:template mode="inline" match="m:ci">
+ <xsl:choose>
+ <xsl:when test="boolean(@definitionURL)">
+ <a href="{@definitionURL}">
+ <xsl:apply-templates/>
+ </a>
+ </xsl:when>
+ <xsl:otherwise>
+ <xsl:value-of select="."/>
+ </xsl:otherwise>
+ </xsl:choose>
+</xsl:template>
+
<!-- CSYMBOL -->
+<xsl:template match="m:apply[m:csymbol]" mode="inline">
+ <xsl:variable name="name">
+ <xsl:value-of select="m:csymbol"/>
+ </xsl:variable>
+ <xsl:variable name="uri"><xsl:value-of select="*[1]/@definitionURL"/></xsl:variable>
+ <xsl:choose>
+ <!-- FORALL -->
+ <xsl:when test="$name='forall'">
+ <xsl:call-template name="mksymbol-1">
+ <xsl:with-param name="symbol" select="$name"/>
+ <xsl:with-param name="color" select="'blue'"/>
+ <xsl:with-param name="size" select="'+2'"/>
+ </xsl:call-template>
+ <xsl:apply-templates select="m:bvar/m:ci"/>
+ <xsl:text>:</xsl:text>
+ <xsl:apply-templates mode="inline" select="m:bvar/m:type"/>
+ <xsl:text>.</xsl:text>
+ <xsl:apply-templates mode="inline" select="*[position()=3]"/>
+ </xsl:when>
+ <xsl:when test="$name='prod'">
+ <xsl:call-template name="mksymbol-1">
+ <xsl:with-param name="symbol" select="$name"/>
+ <xsl:with-param name="color" select="'blue'"/>
+ <xsl:with-param name="size" select="'+2'"/>
+ </xsl:call-template>
+ <xsl:apply-templates mode="inline" select="m:bvar/m:ci"/>
+ <xsl:text>:</xsl:text>
+ <xsl:apply-templates mode="inline" select="m:bvar/m:type"/>
+ <xsl:text>.</xsl:text>
+ <xsl:apply-templates mode="inline" select="*[position()=3]"/>
+ </xsl:when>
+ <!-- ARROW -->
+ <xsl:when test="$name='arrow'">
+ <xsl:text>(</xsl:text>
+ <xsl:apply-templates mode="inline" select="*[position()=2]"/>
+ <xsl:call-template name="mksymbol-1">
+ <xsl:with-param name="symbol" select="$name"/>
+ <xsl:with-param name="color" select="'blue'"/>
+ <xsl:with-param name="size" select="'+0'"/>
+ </xsl:call-template>
+ <xsl:apply-templates mode="inline" select="*[position()=3]"/>
+ <xsl:text>)</xsl:text>
+ </xsl:when>
+ <!-- APP -->
+ <xsl:when test="$name='app'">
+ <xsl:text>(</xsl:text>
+ <xsl:apply-templates mode="inline" select="*[position()=2]"/>
+ <xsl:for-each select="*[position()>2]">
+ <xsl:text> </xsl:text>
+ <xsl:apply-templates mode="inline" select="."/>
+ </xsl:for-each>
+ <xsl:text>)</xsl:text>
+ </xsl:when>
+ <!-- CAST -->
+ <xsl:when test="$name='cast'">
+ <xsl:text>(</xsl:text>
+ <xsl:apply-templates mode="inline" select="*[position()=2]"/>
+ <xsl:text>:></xsl:text>
+ <xsl:apply-templates mode="inline" select="*[position()=3]"/>
+ <xsl:text>)</xsl:text>
+ </xsl:when>
+ <xsl:when test="$name='Prop'">
+ <FONT color="violet">Prop</FONT>
+ </xsl:when>
+ <xsl:when test="$name='Set'">
+ <FONT color="violet">Set</FONT>
+ </xsl:when>
+ <xsl:when test="$name='Type'">
+ <FONT color="violet">Type</FONT>
+ </xsl:when>
+ <!-- MUTCASE -->
+ <xsl:when test="$name='mutcase'">
+ <xsl:text><</xsl:text>
+ <xsl:apply-templates mode="inline" select="*[position()=2]"/>
+ <xsl:text>> </xsl:text>
+ <FONT color="red">CASE </FONT>
+ <xsl:apply-templates mode="inline" select="*[position()=3]"/>
+ <FONT color="red"> OF </FONT>
+ <xsl:for-each select="m:piecewise/m:piece">
+<!--<xsl:for-each select="*[position() mod 2 = 0 and position()>3]">-->
+ <xsl:choose>
+ <xsl:when test="not(position() = 1)">
+ <xsl:text> | </xsl:text>
+ </xsl:when>
+ </xsl:choose>
+ <xsl:apply-templates mode="inline" select="./*[2]"/>
+ <xsl:call-template name="mksymbol-1">
+ <xsl:with-param name="symbol" select="'RightArrow'"/>
+ <xsl:with-param name="color" select="'green'"/>
+ <xsl:with-param name="size" select="'+0'"/>
+ </xsl:call-template>
+ <xsl:apply-templates mode="inline"
+ select="./*[1]"/>
+ </xsl:for-each>
+ </xsl:when>
+ <!-- FIX -->
+ <xsl:when test="$name='fix'">
+ <FONT color="red">FIX</FONT>
+ <xsl:value-of select="m:ci"/>
+ <xsl:text>{</xsl:text>
+ <xsl:for-each select="m:bvar">
+ <xsl:value-of select="m:ci"/>
+ <xsl:text>:</xsl:text>
+ <xsl:apply-templates mode="inline" select="m:type"/>
+ <xsl:text>:=</xsl:text>
+ <xsl:apply-templates mode="inline"
+ select="following-sibling::*[position() = 1]"/>
+ <xsl:choose>
+ <xsl:when test="position()=last()">
+ <xsl:text>}</xsl:text>
+ </xsl:when>
+ <xsl:otherwise>
+ <xsl:text>;</xsl:text>
+ </xsl:otherwise>
+ </xsl:choose>
+ </xsl:for-each>
+ </xsl:when>
+ <!-- COFIX -->
+ <xsl:when test="$name='cofix'">
+ <xsl:text>COFIX</xsl:text>
+ <xsl:value-of select="m:ci"/>
+ <xsl:text>{</xsl:text>
+ <xsl:for-each select="m:bvar">
+ <xsl:value-of select="m:ci"/>
+ <xsl:text>:</xsl:text>
+ <xsl:apply-templates mode="inline" select="m:type"/>
+ <xsl:text>:=</xsl:text>
+ <xsl:apply-templates mode="inline"
+ select="following-sibling::*[position() = 1]"/>
+ <xsl:choose>
+ <xsl:when test="position()=last()">
+ <xsl:text>}</xsl:text>
+ </xsl:when>
+ <xsl:otherwise>
+ <xsl:text>;</xsl:text>
+ </xsl:otherwise>
+ </xsl:choose>
+ </xsl:for-each>
+ </xsl:when>
+ <!-- proof and side_proof -->
+ <xsl:when test="$name='proof' or $name='side_proof'">
+ <xsl:apply-templates mode="inline" select="*[position()=2]"/>
+ <FONT color="red"> proves </FONT>
+ <xsl:apply-templates mode="inline" select="*[position()=3]"/>
+ <xsl:if test="*[4]">
+ <FONT color="red"> which is equivalent to </FONT>
+ <xsl:apply-templates mode="inline" select="*[position()=4]"/>
+ </xsl:if>
+ </xsl:when>
+ <!-- letin1 -->
+ <xsl:when test="$name='letin1'">
+ <xsl:text>letin1 (inline error)</xsl:text>
+ </xsl:when>
+ <!-- false_ind -->
+ <xsl:when test="$name='false_ind'">
+ <xsl:apply-templates mode="inline" select="*[3]"/>
+ <FONT color="red">Contradiction.</FONT>
+ </xsl:when>
+ <!-- and_ind -->
+ <xsl:when test="$name='and_ind'">
+ <FONT color="red">From </FONT>
+ <xsl:apply-templates select="*[2]"/>
+ <FONT color="red"> we get</FONT>
+ (
+ <xsl:apply-templates select="*[3]"/>
+ ) 
+ <xsl:apply-templates mode="inline" select="*[4]"/>
+ <FONT color="red"> and </FONT>
+ (
+ <xsl:apply-templates select="*[5]"/>
+ ) 
+ <xsl:apply-templates mode="inline" select="*[6]"/>
+ ;
+ <FONT color="red"> hence </FONT>
+ <xsl:apply-templates mode="inline" select="*[7]"/>
+ </xsl:when>
+
+ <xsl:when test="$name='subst'">
+ <xsl:apply-templates select="*[3]" mode="inline"/>
+ <xsl:text>[</xsl:text>
+ <xsl:apply-templates select="*[4]" mode="inline"/>
+ <xsl:choose>
+ <xsl:when test="$uri != ''">
+ <a href="{$uri}">
+ <xsl:call-template name="mksymbol-1">
+ <xsl:with-param name="symbol" select="$name"/>
+ <xsl:with-param name="color" select="'green'"/>
+ <xsl:with-param name="size" select="'+0'"/>
+ </xsl:call-template>
+ </a>
+ </xsl:when>
+ <xsl:otherwise>
+ <xsl:call-template name="mksymbol-1">
+ <xsl:with-param name="symbol" select="$name"/>
+ <xsl:with-param name="color" select="'green'"/>
+ <xsl:with-param name="size" select="'+0'"/>
+ </xsl:call-template>
+ </xsl:otherwise>
+ </xsl:choose>
+ <xsl:apply-templates select="*[2]" mode="inline"/>
+ <xsl:text>]</xsl:text>
+ </xsl:when>
+
+ <xsl:when test="$name='lift_with_base'">
+ <SUB>
+ <xsl:apply-templates select="*[3]" mode="inline"/>
+ </SUB>
+ <xsl:choose>
+ <xsl:when test="$uri != ''">
+ <a href="{$uri}">
+ <xsl:call-template name="mksymbol-1">
+ <xsl:with-param name="symbol" select="$name"/>
+ <xsl:with-param name="color" select="'green'"/>
+ <xsl:with-param name="size" select="'+0'"/>
+ </xsl:call-template>
+ </a>
+ </xsl:when>
+ <xsl:otherwise>
+ <xsl:call-template name="mksymbol-1">
+ <xsl:with-param name="symbol" select="$name"/>
+ <xsl:with-param name="color" select="'green'"/>
+ <xsl:with-param name="size" select="'+0'"/>
+ </xsl:call-template>
+ </xsl:otherwise>
+ </xsl:choose>
+ <SUP>
+ <xsl:apply-templates select="*[4]" mode="inline"/>
+ </SUP>
+ <xsl:text>(</xsl:text>
+ <xsl:apply-templates select="*[2]" mode="inline"/>
+ <xsl:text>)</xsl:text>
+ </xsl:when>
+
+ <xsl:when test="$name='lift'">
+ <xsl:choose>
+ <xsl:when test="$uri != ''">
+ <a href="{$uri}">
+ <xsl:call-template name="mksymbol-1">
+ <xsl:with-param name="symbol" select="$name"/>
+ <xsl:with-param name="color" select="'green'"/>
+ <xsl:with-param name="size" select="'+0'"/>
+ </xsl:call-template>
+ </a>
+ </xsl:when>
+ <xsl:otherwise>
+ <xsl:call-template name="mksymbol-1">
+ <xsl:with-param name="symbol" select="$name"/>
+ <xsl:with-param name="color" select="'green'"/>
+ <xsl:with-param name="size" select="'+0'"/>
+ </xsl:call-template>
+ </xsl:otherwise>
+ </xsl:choose>
+ <SUP>
+ <xsl:apply-templates select="*[2]" mode="inline"/>
+ </SUP>
+ <xsl:text>(</xsl:text>
+ <xsl:apply-templates select="*[3]" mode="inline"/>
+ <xsl:text>)</xsl:text>
+ </xsl:when>
+
+ <!-- reduction -->
+ <xsl:when test="$name='beta_red1'">
+ <xsl:apply-templates select="*[2]" mode="inline"/>
+ <xsl:choose>
+ <xsl:when test="$uri != ''">
+ <a href="{$uri}">
+ <xsl:call-template name="mksymbol-1">
+ <xsl:with-param name="symbol" select="$name"/>
+ <xsl:with-param name="color" select="'green'"/>
+ <xsl:with-param name="size" select="'+0'"/>
+ </xsl:call-template>
+ <SUB>
+ <xsl:call-template name="mksymbol-1">
+ <xsl:with-param name="symbol" select="'beta'"/>
+ <xsl:with-param name="color" select="'green'"/>
+ <xsl:with-param name="size" select="'+0'"/>
+ </xsl:call-template>
+ </SUB>
+ </a>
+ </xsl:when>
+ <xsl:otherwise>
+ <xsl:call-template name="mksymbol-1">
+ <xsl:with-param name="symbol" select="$name"/>
+ <xsl:with-param name="color" select="'green'"/>
+ <xsl:with-param name="size" select="'+0'"/>
+ </xsl:call-template>
+ <SUB>
+ <xsl:call-template name="mksymbol-1">
+ <xsl:with-param name="symbol" select="'beta'"/>
+ <xsl:with-param name="color" select="'green'"/>
+ <xsl:with-param name="size" select="'+0'"/>
+ </xsl:call-template>
+ </SUB>
+ </xsl:otherwise>
+ </xsl:choose>
+ <xsl:apply-templates select="*[3]" mode="inline"/>
+ </xsl:when>
+
+ <xsl:when test="$name='beta_red'">
+ <xsl:apply-templates select="*[2]" mode="inline"/>
+ <xsl:choose>
+ <xsl:when test="$uri != ''">
+ <a href="{$uri}">
+ <xsl:call-template name="mksymbol-1">
+ <xsl:with-param name="symbol" select="$name"/>
+ <xsl:with-param name="color" select="'green'"/>
+ <xsl:with-param name="size" select="'+0'"/>
+ </xsl:call-template>
+ <SUB>
+ <xsl:call-template name="mksymbol-1">
+ <xsl:with-param name="symbol" select="'beta'"/>
+ <xsl:with-param name="color" select="'green'"/>
+ <xsl:with-param name="size" select="'+0'"/>
+ </xsl:call-template>
+ <xsl:text>*</xsl:text>
+ </SUB>
+ </a>
+ </xsl:when>
+ <xsl:otherwise>
+ <xsl:call-template name="mksymbol-1">
+ <xsl:with-param name="symbol" select="$name"/>
+ <xsl:with-param name="color" select="'green'"/>
+ <xsl:with-param name="size" select="'+0'"/>
+ </xsl:call-template>
+ <SUB>
+ <xsl:call-template name="mksymbol-1">
+ <xsl:with-param name="symbol" select="'beta'"/>
+ <xsl:with-param name="color" select="'green'"/>
+ <xsl:with-param name="size" select="'+0'"/>
+ </xsl:call-template>
+ <xsl:text>*</xsl:text>
+ </SUB>
+ </xsl:otherwise>
+ </xsl:choose>
+ <xsl:apply-templates select="*[3]" mode="inline"/>
+ </xsl:when>
+
+ <xsl:when test="$name='par_beta_red1'">
+ <xsl:apply-templates select="*[2]" mode="inline"/>
+ <xsl:choose>
+ <xsl:when test="$uri != ''">
+ <a href="{$uri}">
+ <xsl:call-template name="mksymbol-1">
+ <xsl:with-param name="symbol" select="$name"/>
+ <xsl:with-param name="color" select="'green'"/>
+ <xsl:with-param name="size" select="'+0'"/>
+ </xsl:call-template>
+ <SUB>
+ <xsl:call-template name="mksymbol-1">
+ <xsl:with-param name="symbol" select="'beta'"/>
+ <xsl:with-param name="color" select="'green'"/>
+ <xsl:with-param name="size" select="'+0'"/>
+ </xsl:call-template>
+ </SUB>
+ </a>
+ </xsl:when>
+ <xsl:otherwise>
+ <xsl:call-template name="mksymbol-1">
+ <xsl:with-param name="symbol" select="$name"/>
+ <xsl:with-param name="color" select="'green'"/>
+ <xsl:with-param name="size" select="'+0'"/>
+ </xsl:call-template>
+ <SUB>
+ <xsl:call-template name="mksymbol-1">
+ <xsl:with-param name="symbol" select="'beta'"/>
+ <xsl:with-param name="color" select="'green'"/>
+ <xsl:with-param name="size" select="'+0'"/>
+ </xsl:call-template>
+ </SUB>
+ </xsl:otherwise>
+ </xsl:choose>
+ <xsl:apply-templates select="*[3]" mode="inline"/>
+ </xsl:when>
+
+ <xsl:when test="$name='par_beta_red'">
+ <xsl:apply-templates select="*[2]" mode="inline"/>
+ <xsl:choose>
+ <xsl:when test="$uri != ''">
+ <a href="{$uri}">
+ <xsl:call-template name="mksymbol-1">
+ <xsl:with-param name="symbol" select="$name"/>
+ <xsl:with-param name="color" select="'green'"/>
+ <xsl:with-param name="size" select="'+0'"/>
+ </xsl:call-template>
+ <SUB>
+ <xsl:call-template name="mksymbol-1">
+ <xsl:with-param name="symbol" select="'beta'"/>
+ <xsl:with-param name="color" select="'green'"/>
+ <xsl:with-param name="size" select="'+0'"/>
+ </xsl:call-template>
+ <xsl:text>*</xsl:text>
+ </SUB>
+ </a>
+ </xsl:when>
+ <xsl:otherwise>
+ <xsl:call-template name="mksymbol-1">
+ <xsl:with-param name="symbol" select="$name"/>
+ <xsl:with-param name="color" select="'green'"/>
+ <xsl:with-param name="size" select="'+0'"/>
+ </xsl:call-template>
+ <SUB>
+ <xsl:call-template name="mksymbol-1">
+ <xsl:with-param name="symbol" select="'beta'"/>
+ <xsl:with-param name="color" select="'green'"/>
+ <xsl:with-param name="size" select="'+0'"/>
+ </xsl:call-template>
+ <xsl:text>*</xsl:text>
+ </SUB>
+ </xsl:otherwise>
+ </xsl:choose>
+ <xsl:apply-templates select="*[3]" mode="inline"/>
+ </xsl:when>
+
+ <!-- forgetful -->
+ <xsl:when test="$name='forgetful'">
+ <xsl:choose>
+ <xsl:when test="$uri != ''">
+ <a href="{$uri}">|</a>
+ </xsl:when>
+ <xsl:otherwise>
+ |
+ </xsl:otherwise>
+ </xsl:choose>
+ <xsl:apply-templates select="*[2]" mode="inline"/>
+ <xsl:choose>
+ <xsl:when test="$uri != ''">
+ <a href="{$uri}">|</a>
+ </xsl:when>
+ <xsl:otherwise>
+ |
+ </xsl:otherwise>
+ </xsl:choose>
+ </xsl:when>
+
+ <!-- boolean algebra of redexes -->
+
+ <!-- isomorphic -->
+ <xsl:when test="$name='isomorphic'">
+ <xsl:apply-templates select="*[2]" mode="inline"/>
+ <xsl:choose>
+ <xsl:when test="$uri != ''">
+ <a href="{$uri}">
+ <xsl:call-template name="mksymbol-1">
+ <xsl:with-param name="symbol" select="$name"/>
+ <xsl:with-param name="color" select="'green'"/>
+ <xsl:with-param name="size" select="'+0'"/>
+ </xsl:call-template>
+ </a>
+ </xsl:when>
+ <xsl:otherwise>
+ <xsl:call-template name="mksymbol-1">
+ <xsl:with-param name="symbol" select="$name"/>
+ <xsl:with-param name="color" select="'green'"/>
+ <xsl:with-param name="size" select="'+0'"/>
+ </xsl:call-template>
+ </xsl:otherwise>
+ </xsl:choose>
+ <xsl:apply-templates select="*[3]" mode="inline"/>
+ </xsl:when>
+
+ <!-- INTERP -->
+ <xsl:when test="$name='interp'">
+ <font color="green">[</font>
+ <xsl:apply-templates select="*[2]"/>
+ <font color="green">]</font>
+ </xsl:when>
+
+ </xsl:choose>
+</xsl:template>
+
+<xsl:template mode="inline" match="m:lambda">
+ <xsl:call-template name="mksymbol-1">
+ <xsl:with-param name="symbol" select="'lambda'"/>
+ <xsl:with-param name="color" select="'red'"/>
+ <xsl:with-param name="size" select="'+2'"/>
+ </xsl:call-template>
+ <xsl:apply-templates select="m:bvar/m:ci"/>
+ <xsl:text>:</xsl:text>
+ <xsl:apply-templates mode="inline" select="m:bvar/m:type"/>
+ <xsl:text>.</xsl:text>
+ <xsl:apply-templates mode="inline" select="*[position()=2]"/>
+</xsl:template>
+
+<!--*********************************************************************-->
+<!-- COUNTING MODE -->
+<!--*********************************************************************-->
+
<xsl:template match="m:apply[m:csymbol]">
<xsl:param name="current_indent" select="0"/>
<xsl:param name="width" select="$framewidth"/>
</xsl:variable>
<!-- <xsl:value-of select="$current_indent"/> -->
<!-- <xsl:value-of select="$charlength"/> -->
+ <xsl:variable name="uri"><xsl:value-of select="*[1]/@definitionURL"/></xsl:variable>
<xsl:choose>
- <xsl:when test="$name='prod'">
+ <!-- FORALL -->
+ <xsl:when test="$name='forall'">
<xsl:choose>
<xsl:when test="$charlength > $framewidth">
<!-- Π -->
- <FONT FACE="symbol" SIZE="+2" color="blue">P</FONT>
+ <xsl:call-template name="mksymbol-1">
+ <xsl:with-param name="symbol" select="$name"/>
+ <xsl:with-param name="color" select="'blue'"/>
+ <xsl:with-param name="size" select="'+2'"/>
+ </xsl:call-template>
+ <xsl:apply-templates select="m:bvar/m:ci"/>
+ <xsl:text>:</xsl:text>
+ <xsl:apply-templates select="m:bvar/m:type">
+ <xsl:with-param name="current_indent"
+ select="$current_indent + 5 + 2*string-length(m:bvar/m:ci)"/>
+ </xsl:apply-templates>
+ <br/>
+ <xsl:call-template name="make_indent">
+ <xsl:with-param name="current_indent" select="$current_indent + 2"/>
+ </xsl:call-template>
+ <xsl:text>.</xsl:text>
+ <xsl:apply-templates select="*[position()=3]">
+ <xsl:with-param name="current_indent" select="$current_indent + 2"/>
+ </xsl:apply-templates>
+ </xsl:when>
+ <xsl:otherwise>
+ <xsl:apply-templates mode="inline" select="."/>
+ </xsl:otherwise>
+ </xsl:choose>
+ </xsl:when>
+ <!-- PROD -->
+ <xsl:when test="$name='prod'">
+ <xsl:choose>
+ <xsl:when test="$charlength > $framewidth">
+ <xsl:call-template name="mksymbol-1">
+ <xsl:with-param name="symbol" select="$name"/>
+ <xsl:with-param name="color" select="'blue'"/>
+ <xsl:with-param name="size" select="'+2'"/>
+ </xsl:call-template>
<xsl:apply-templates select="m:bvar/m:ci"/>
<xsl:text>:</xsl:text>
<xsl:apply-templates select="m:bvar/m:type">
<xsl:with-param name="current_indent"
- select="$current_indent + 2 + string-length(m:bvar/m:ci)"/>
- </xsl:apply-templates><BR/>
+ select="$current_indent + 5 + 2*string-length(m:bvar/m:ci)"/>
+ </xsl:apply-templates><br/>
<xsl:call-template name="make_indent">
<xsl:with-param name="current_indent" select="$current_indent + 2"/>
</xsl:call-template>
</xsl:apply-templates>
</xsl:when>
<xsl:otherwise>
- <!-- Π -->
- <FONT FACE="symbol" SIZE="+2" color="blue">P</FONT>
- <xsl:apply-templates select="m:bvar/m:ci"/>
- <xsl:text>:</xsl:text>
- <xsl:apply-templates select="m:bvar/m:type"/>
- <xsl:text>.</xsl:text>
- <xsl:apply-templates select="*[position()=3]"/>
+ <xsl:apply-templates mode="inline" select="."/>
</xsl:otherwise>
</xsl:choose>
</xsl:when>
+ <!-- ARROW -->
<xsl:when test="$name='arrow'">
<xsl:choose>
<xsl:when test="$charlength > $framewidth">
<xsl:apply-templates select="*[position()=2]">
<xsl:with-param name="current_indent" select="$current_indent + 2"/>
</xsl:apply-templates>
- <BR/>
+ <br/>
<xsl:call-template name="make_indent">
<xsl:with-param name="current_indent" select="$current_indent + 2"/>
</xsl:call-template>
<!-- -> -->
- <FONT FACE="symbol" SIZE="+2" color="blue">®</FONT>
+ <xsl:call-template name="mksymbol-1">
+ <xsl:with-param name="symbol" select="$name"/>
+ <xsl:with-param name="color" select="'blue'"/>
+ <xsl:with-param name="size" select="'+0'"/>
+ </xsl:call-template>
<xsl:apply-templates select="*[position()=3]">
<xsl:with-param name="current_indent" select="$current_indent + 5"/>
</xsl:apply-templates>
<xsl:text>)</xsl:text>
</xsl:when>
<xsl:otherwise>
- <xsl:text>(</xsl:text>
- <xsl:apply-templates select="*[position()=2]"/>
- <!-- -> -->
- <FONT FACE="symbol" SIZE="+2" color="blue">®</FONT>
- <xsl:apply-templates select="*[position()=3]"/>
- <xsl:text>)</xsl:text>
+ <xsl:apply-templates mode="inline" select="."/>
</xsl:otherwise>
</xsl:choose>
</xsl:when>
+ <!-- APP -->
<xsl:when test="$name='app'">
<xsl:choose>
<xsl:when test="$charlength > $framewidth">
<xsl:with-param name="current_indent" select="$current_indent + 2"/>
</xsl:apply-templates>
<xsl:for-each select="*[position()>2]">
- <BR/>
+ <br/>
<xsl:call-template name="make_indent">
<xsl:with-param name="current_indent" select="$current_indent + 2"/>
</xsl:call-template>
<xsl:text>)</xsl:text>
</xsl:when>
<xsl:otherwise>
- <xsl:text>(</xsl:text>
- <xsl:apply-templates select="*[position()=2]"/>
- <xsl:for-each select="*[position()>2]">
- <xsl:text> </xsl:text>
- <xsl:apply-templates select="."/>
- </xsl:for-each>
- <xsl:text>)</xsl:text>
+ <xsl:apply-templates mode="inline" select="."/>
</xsl:otherwise>
</xsl:choose>
</xsl:when>
<xsl:text>(</xsl:text>
<xsl:apply-templates select="*[position()=2]">
<xsl:with-param name="current_indent" select="$current_indent + 2"/>
- </xsl:apply-templates><BR/>
+ </xsl:apply-templates><br/>
<xsl:call-template name="make_indent">
<xsl:with-param name="current_indent" select="$current_indent + 2"/> </xsl:call-template>
<xsl:text>:></xsl:text>
<xsl:text>)</xsl:text>
</xsl:when>
<xsl:otherwise>
- <xsl:text>(</xsl:text>
- <xsl:apply-templates select="*[position()=2]"/>
- <xsl:text>:></xsl:text>
- <xsl:apply-templates select="*[position()=3]"/>
- <xsl:text>)</xsl:text>
+ <xsl:apply-templates mode="inline" select="."/>
</xsl:otherwise>
</xsl:choose>
</xsl:when>
<xsl:with-param name="current_indent" select="$current_indent + 2"/>
</xsl:apply-templates>
<xsl:text>> </xsl:text>
+ <br/>
+ <xsl:call-template name="make_indent">
+ <xsl:with-param name="current_indent" select="$current_indent + 2"/> </xsl:call-template>
<xsl:text>CASE </xsl:text>
<xsl:apply-templates select="*[position()=3]">
<xsl:with-param name="current_indent" select="$current_indent + 8"/>
</xsl:apply-templates>
<xsl:text> OF </xsl:text>
- <xsl:for-each select="*[position() mod 2 = 0 and position()>3]">
- <BR/>
+ <xsl:for-each select="m:piecewise/m:piece">
+ <!-- <xsl:for-each select="*[position() mod 2 = 0 and position()>3]">-->
+ <br/>
<xsl:call-template name="make_indent">
- <xsl:with-param name="current_indent" select="$current_indent + 2"/>
+ <xsl:with-param name="current_indent" select="$current_indent + 2"/>
</xsl:call-template>
<xsl:choose>
<xsl:when test="position() = 1">
<xsl:text>| </xsl:text>
</xsl:otherwise>
</xsl:choose>
- <xsl:apply-templates select="."/>
- <FONT FACE="symbol" SIZE="+2" color="green">Þ</FONT>
- <xsl:apply-templates select="following-sibling::*[position()= 1]">
- <xsl:with-param name="current_indent" select="$current_indent + 4 + string-length()"/>
- </xsl:apply-templates>
+ <xsl:apply-templates select="./*[2]"/>
+ <xsl:call-template name="mksymbol-1">
+ <xsl:with-param name="symbol" select="'RightArrow'"/>
+ <xsl:with-param name="color" select="'green'"/>
+ <xsl:with-param name="size" select="'+0'"/>
+ </xsl:call-template>
+ <xsl:variable name="body_size">
+ <xsl:apply-templates
+ select="./*[1]/*[1]" mode="charcount"/>
+ </xsl:variable>
+ <xsl:choose>
+ <xsl:when test="$body_size > $framewidth">
+ <br/>
+ <xsl:call-template name="make_indent">
+ <xsl:with-param name="current_indent"
+ select="$current_indent + 8"/>
+ </xsl:call-template>
+<xsl:apply-templates
+ select="./*[1]">
+ <xsl:with-param name="current_indent"
+ select="$current_indent + 8"/>
+ </xsl:apply-templates>
+ </xsl:when>
+ <xsl:otherwise>
+ <xsl:apply-templates select="./*[1]"
+ mode="inline" />
+ </xsl:otherwise>
+ </xsl:choose>
</xsl:for-each>
</xsl:when>
<xsl:otherwise>
- <xsl:text><</xsl:text>
- <xsl:apply-templates select="*[position()=2]"/>
- <xsl:text>> </xsl:text>
- <xsl:text>CASE </xsl:text>
- <xsl:apply-templates select="*[position()=3]"/>
- <xsl:text> OF </xsl:text>
- <xsl:for-each select="*[position() mod 2 = 0 and position()>3]">
- <xsl:choose>
- <xsl:when test="not(position() = 1)">
- <xsl:text> | </xsl:text>
- </xsl:when>
- </xsl:choose>
- <xsl:apply-templates select="."/>
- <FONT FACE="symbol" SIZE="+2" color="green">Þ</FONT>
- <xsl:apply-templates select="following-sibling::*[position()= 1]">
- <xsl:with-param name="current_indent" select="$current_indent + 2 + string-length()"/>
- </xsl:apply-templates>
- </xsl:for-each>
+ <xsl:apply-templates mode="inline" select="."/>
</xsl:otherwise>
</xsl:choose>
</xsl:when>
+ <!-- FIX -->
<xsl:when test="$name='fix'">
<xsl:choose>
<xsl:when test="$charlength > $framewidth">
<xsl:value-of select="m:ci"/>
<xsl:text>{</xsl:text>
<xsl:for-each select="m:bvar">
- <BR/>
+ <br/>
<xsl:call-template name="make_indent">
<xsl:with-param name="current_indent" select="$current_indent + 2"/>
</xsl:call-template>
<xsl:with-param name="current_indent"
select="$current_indent + 5 + string-length(m:ci)"/>
</xsl:apply-templates>
- <BR/>
+ <br/>
<xsl:call-template name="make_indent">
<xsl:with-param name="current_indent" select="$current_indent + 2"/>
</xsl:call-template>
<xsl:with-param name="current_indent" select="$current_indent +2"/>
</xsl:apply-templates>
</xsl:for-each>
- <BR/>
+ <br/>
<xsl:call-template name="make_indent">
<xsl:with-param name="current_indent" select="$current_indent + 2"/>
</xsl:call-template>
<xsl:text>}</xsl:text>
</xsl:when>
<xsl:otherwise>
- <xsl:text>FIX</xsl:text>
- <xsl:value-of select="m:ci"/>
- <xsl:text>{</xsl:text>
- <xsl:for-each select="m:bvar">
- <xsl:value-of select="m:ci"/>
- <xsl:text>:</xsl:text>
- <xsl:apply-templates select="m:type"/>
- <xsl:text>:=</xsl:text>
- <xsl:apply-templates select="following-sibling::*[position() = 1]"/>
- <xsl:choose>
- <xsl:when test="position()=last()">
- <xsl:text>}</xsl:text>
- </xsl:when>
- <xsl:otherwise>
- <xsl:text>;</xsl:text>
- </xsl:otherwise>
- </xsl:choose>
- </xsl:for-each>
+ <xsl:apply-templates mode="inline" select="."/>
</xsl:otherwise>
</xsl:choose>
</xsl:when>
+ <!-- COFIX -->
<xsl:when test="$name='cofix'">
<xsl:choose>
<xsl:when test="($charlength + 10) > $framewidth">
<xsl:text>COFIX</xsl:text>
<xsl:value-of select="m:ci"/>
<xsl:text>{</xsl:text>
- <BR/>
+ <br/>
<xsl:call-template name="make_indent">
<xsl:with-param name="current_indent" select="$current_indent + 2"/>
</xsl:call-template>
<xsl:with-param name="current_indent"
select="$current_indent + 5 + string-length(m:ci)"/>
</xsl:apply-templates>
- <BR/>
+ <br/>
<xsl:call-template name="make_indent">
<xsl:with-param name="current_indent" select="$current_indent + 2"/>
</xsl:call-template>
</xsl:apply-templates>
</xsl:for-each>
- <BR/>
+ <br/>
<xsl:call-template name="make_indent">
<xsl:with-param name="current_indent" select="$current_indent + 2"/>
</xsl:call-template>
<xsl:text>}</xsl:text>
</xsl:when>
<xsl:otherwise>
- <xsl:text>COFIX</xsl:text>
- <xsl:value-of select="m:ci"/>
- <xsl:text>{</xsl:text>
- <xsl:for-each select="m:bvar">
- <xsl:value-of select="m:ci"/>
- <xsl:text>:</xsl:text>
- <xsl:apply-templates select="m:type"/>
- <xsl:text>:=</xsl:text>
- <xsl:apply-templates select="following-sibling::*[position() = 1]"/>
- <xsl:choose>
- <xsl:when test="position()=last()">
- <xsl:text>}</xsl:text>
- </xsl:when>
- <xsl:otherwise>
- <xsl:text>;</xsl:text>
- </xsl:otherwise>
- </xsl:choose>
- </xsl:for-each>
+ <xsl:apply-templates mode="inline" select="m:type"/>
</xsl:otherwise>
</xsl:choose>
</xsl:when>
- </xsl:choose>
- <!-- </m:mrow> -->
-</xsl:template>
-
-<!-- LAMBDA -->
-
+ <xsl:when test="$name='let_in'">
+ <xsl:text>let </xsl:text>
+ <xsl:apply-templates select="m:bvar/m:ci"/>
+ <xsl:text> := </xsl:text>
+ <xsl:apply-templates select="*[3]">
+ <xsl:with-param name="current_indent" select="$current_indent+14"/>
+ </xsl:apply-templates>
+ <br/>
+ <xsl:call-template name="make_indent">
+ <xsl:with-param name="current_indent" select="$current_indent"/>
+ </xsl:call-template>
+ <xsl:text>in </xsl:text>
+ <xsl:apply-templates select="*[4]">
+ <xsl:with-param name="current_indent" select="$current_indent+5"/>
+ </xsl:apply-templates>
+ </xsl:when>
+
+ <!-- ***************************************** -->
+ <!-- *********** PROOF ELEMENTS ************** -->
+ <!-- ***************************************** -->
+ <!-- PROOF -->
+ <xsl:when test="$name='proof'">
+ <xsl:variable name="nonce" select="generate-id()"/>
+ <xsl:variable name="freshid1" select="concat('a',$nonce)"/>
+ <xsl:variable name="freshid2" select="concat('b',$nonce)"/>
+ <xsl:variable name="freshid3" select="concat('c',$nonce)"/>
+ <span ID="{$freshid1}">
+ <xsl:apply-templates select="*[position()=2]">
+ <xsl:with-param name="current_indent" select="$current_indent"/>
+ </xsl:apply-templates>
+  
+ </span>
+ <xsl:choose>
+ <xsl:when test="(preceding-sibling::*[1]/text()='letin1') or
+ (preceding-sibling::*[1]/text()='rw_step') or
+ (name(..)='m:lambda')">
+ <br/>
+ <xsl:call-template name="make_indent">
+ <xsl:with-param name="current_indent" select="$current_indent"/>
+ </xsl:call-template>
+ <FONT color="red">we proved </FONT>
+ </xsl:when>
+ <xsl:otherwise>
+ <script>
+ if(document.getElementById) {
+ document.write('\
+ <span ID="{$freshid2}">\
+ <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>\
+ </span>\
+ <span ID="{$freshid3}">\
+ <br/>\
+ <xsl:call-template name="make_indent">
+ <xsl:with-param name="current_indent" select="$current_indent"/>
+ </xsl:call-template>\
+ <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>\
+ </span>\
+ ');
+ document.to_be_deleted.push('<xsl:value-of select="$freshid1"/>');
+ document.to_be_deleted.push('<xsl:value-of select="$freshid3"/>');
+ document.write(' ');
+ } else {
+ document.write('\
+ <br/>\
+ <xsl:call-template name="make_indent">
+ <xsl:with-param name="current_indent" select="$current_indent"/>
+ </xsl:call-template>\
+ <FONT color="red">we proved </FONT>\
+ ');
+ }
+ </script>
+ </xsl:otherwise>
+ </xsl:choose>
+ <xsl:apply-templates select="*[position()=3]">
+ <xsl:with-param name="current_indent" select="$current_indent + 16"/>
+ </xsl:apply-templates>
+ </xsl:when>
+ <!-- side_proof -->
+ <xsl:when test="$name='side_proof'">
+ <xsl:variable name="nonce" select="generate-id()"/>
+ <xsl:variable name="freshid1" select="concat('a',$nonce)"/>
+ <xsl:variable name="freshid2" select="concat('b',$nonce)"/>
+ <xsl:variable name="freshid3" select="concat('c',$nonce)"/>
+ <xsl:variable name="freshid4" select="concat('d',$nonce)"/>
+ <span ID="{$freshid1}">
+ <xsl:apply-templates select="*[position()=2]">
+ <xsl:with-param name="current_indent" select="$current_indent"/>
+ </xsl:apply-templates>
+  
+ </span>
+ <script>
+ if(document.getElementById) {
+ document.write('\
+ <span ID="{$freshid2}">\
+ <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>\
+ </span>\
+ <span ID="{$freshid3}">\
+ <br/>\
+ <xsl:call-template name="make_indent">
+ <xsl:with-param name="current_indent" select="$current_indent"/>
+ </xsl:call-template>\
+ <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>\
+ </span>\
+ ');
+ document.to_be_deleted.push('<xsl:value-of select="$freshid1"/>');
+ document.to_be_deleted.push('<xsl:value-of select="$freshid3"/>');
+ document.to_be_deleted.push('<xsl:value-of select="$freshid4"/>');
+ document.write(' ');
+ } else {
+ document.write('\
+ <br/>\
+ <xsl:call-template name="make_indent">
+ <xsl:with-param name="current_indent" select="$current_indent"/>
+ </xsl:call-template>\
+ <FONT color="red">we proved </FONT>\
+ ');
+ }
+ </script>
+ <span ID="{$freshid4}">
+ <xsl:apply-templates select="*[position()=3]">
+ <xsl:with-param name="current_indent" select="$current_indent + 16"/>
+ </xsl:apply-templates>
+ </span>
+ </xsl:when>
+ <!-- eq_chain -->
+ <xsl:when test="$name='eq_chain'">
+ <FONT color="red">We have the following equality chain:</FONT>
+ <xsl:for-each select="*[position() mod 2 = 0]">
+ <xsl:variable name="pos" select="position()"/>
+ <br/>
+ <xsl:call-template name="make_indent">
+ <xsl:with-param name="current_indent" select="$current_indent + 5"/>
+ </xsl:call-template>
+ <xsl:choose>
+ <xsl:when test="$pos=1">
+ <xsl:apply-templates select=".">
+ <xsl:with-param name="current_indent" select="$current_indent + 5"/>
+ </xsl:apply-templates>
+ <xsl:text> =</xsl:text>
+ </xsl:when>
+ <xsl:otherwise>
+ <xsl:text>= </xsl:text>
+ <xsl:apply-templates select=".">
+ <xsl:with-param name="current_indent" select="$current_indent + 5"/>
+ </xsl:apply-templates>
+ </xsl:otherwise>
+ </xsl:choose>
+ <xsl:if test="$pos != last()">
+ <br/>
+ <xsl:call-template name="make_indent">
+ <xsl:with-param name="current_indent" select="$current_indent + 15"/>
+ </xsl:call-template>
+ <xsl:apply-templates select="../*[position()=2*$pos +1]">
+ <xsl:with-param name="current_indent" select="$current_indent + 15"/>
+ </xsl:apply-templates>
+ </xsl:if>
+ </xsl:for-each>
+ </xsl:when>
+ <!-- diseq_chain -->
+ <xsl:when test="$name='diseq_chain'">
+ <FONT color="red">We have the following chain of disequalities:</FONT>
+ <xsl:for-each select="*[position() mod 3 = 2]">
+ <xsl:variable name="pos" select="position()"/>
+ <br/>
+ <xsl:call-template name="make_indent">
+ <xsl:with-param name="current_indent" select="$current_indent + 5"/>
+ </xsl:call-template>
+ <xsl:choose>
+ <xsl:when test="$pos=1">
+ <xsl:apply-templates select=".">
+ <xsl:with-param name="current_indent" select="$current_indent + 5"/>
+ </xsl:apply-templates>
+ <xsl:text> </xsl:text>
+ <xsl:apply-templates mode="inline" select="../*[position()=3*$pos]"/>
+ </xsl:when>
+ <xsl:otherwise>
+ <xsl:apply-templates mode="inline" select="../*[position()=3*($pos - 1)]"/>
+ <xsl:text> </xsl:text>
+ <xsl:apply-templates select=".">
+ <xsl:with-param name="current_indent" select="$current_indent + 5"/>
+ </xsl:apply-templates>
+ </xsl:otherwise>
+ </xsl:choose>
+ <xsl:if test="$pos != last()">
+ <br/>
+ <xsl:call-template name="make_indent">
+ <xsl:with-param name="current_indent" select="$current_indent + 15"/>
+ </xsl:call-template>
+ <xsl:apply-templates select="../*[position()=3*$pos +1]">
+ <xsl:with-param name="current_indent" select="$current_indent + 15"/>
+ </xsl:apply-templates>
+ </xsl:if>
+ </xsl:for-each>
+ </xsl:when>
+ <!-- letin1 -->
+ <xsl:when test="$name='letin1'">
+ <xsl:apply-templates select="*[position()=2]">
+ <xsl:with-param name="current_indent" select="$current_indent"/>
+ </xsl:apply-templates>
+ <br/>
+ <xsl:call-template name="make_indent">
+ <xsl:with-param name="current_indent" select="$current_indent"/>
+ </xsl:call-template>
+ <xsl:apply-templates select="*[position()=3]">
+ <xsl:with-param name="current_indent" select="$current_indent"/>
+ </xsl:apply-templates>
+ </xsl:when>
+ <!-- letin -->
+ <xsl:when test="$name='letin'">
+ <xsl:for-each select="*[position()>1 and last()>position()]">
+ <xsl:apply-templates select=".">
+ <xsl:with-param name="current_indent" select="$current_indent"/>
+ </xsl:apply-templates>
+ <br/>
+ <xsl:call-template name="make_indent">
+ <xsl:with-param name="current_indent" select="$current_indent"/>
+ </xsl:call-template>
+ </xsl:for-each>
+ <xsl:apply-templates select="*[position()=last()]">
+ <xsl:with-param name="current_indent" select="$current_indent"/>
+ </xsl:apply-templates>
+ </xsl:when>
+ <!-- Let -->
+ <xsl:when test="$name='let'">
+ (
+ <xsl:apply-templates select="m:ci"/>
+ )
+ <xsl:apply-templates select="*[3]">
+ <xsl:with-param name="current_indent" select="$current_indent + 7"/>
+ </xsl:apply-templates>
+ </xsl:when>
+ <!-- rw_step -->
+ <xsl:when test="$name='rw_step'">
+ <xsl:choose>
+ <xsl:when test="name(*[2])='m:apply'">
+ <xsl:apply-templates select="*[2]">
+ <xsl:with-param name="current_indent" select="$current_indent"/>
+ </xsl:apply-templates>
+ </xsl:when>
+ <xsl:otherwise>
+ <FONT color="red">Consider </FONT>
+ <xsl:apply-templates select="*[2]"/>
+ </xsl:otherwise>
+ </xsl:choose>
+ <xsl:variable name="charlength_first">
+ <xsl:apply-templates select="*[3]" mode="root_charcount"/>
+ </xsl:variable>
+ <xsl:variable name="charlength_second">
+ <xsl:apply-templates select="*[4]" mode="root_charcount"/>
+ </xsl:variable>
+ <xsl:variable name="charlength_side_proof">
+ <xsl:apply-templates select="*[5]" mode="root_charcount"/>
+ </xsl:variable>
+ <xsl:variable name="split1"
+ select="($charlength_first + $charlength_second) > $framewidth"/>
+ <xsl:variable name="split2"
+ select="($charlength_second + $charlength_side_proof) > $framewidth"/>
+ <!-- <xsl:value-of select="$current_indent"/> -->
+ <!-- <xsl:value-of select="string($charlength_second)"/> -->
+ <!-- <xsl:value-of select="$charlength_side_proof"/> -->
+ <!-- <xsl:value-of select="$split2"/> -->
+ <br/>
+ <xsl:call-template name="make_indent">
+ <xsl:with-param name="current_indent" select="$current_indent"/>
+ </xsl:call-template>
+ <FONT color="red">Rewrite </FONT>
+ <xsl:apply-templates mode="inline" select="*[3]"/>
+ <xsl:text> </xsl:text>
+ <xsl:if test="$split1">
+ <br/>
+ <xsl:call-template name="make_indent">
+ <xsl:with-param name="current_indent" select="$current_indent + 2"/>
+ </xsl:call-template>
+ </xsl:if>
+ <FONT color="red">with </FONT>
+ <xsl:apply-templates mode="inline" select="*[4]"/>
+ <xsl:text> </xsl:text>
+ <xsl:if test="$split2">
+ <br/>
+ <xsl:call-template name="make_indent">
+ <xsl:with-param name="current_indent" select="$current_indent + 2"/>
+ </xsl:call-template>
+ </xsl:if>
+ <FONT color="red">by </FONT>
+ <xsl:apply-templates select="*[5]">
+ <xsl:with-param name="current_indent" select="$current_indent+7"/>
+ </xsl:apply-templates>
+ </xsl:when>
+ <!-- rewrite and apply -->
+ <xsl:when test="$name='rewrite_and_apply'">
+ <xsl:apply-templates select="*[2]">
+ <xsl:with-param name="current_indent" select="$current_indent"/>
+ </xsl:apply-templates>
+ <br/>
+ <xsl:call-template name="make_indent">
+ <xsl:with-param name="current_indent" select="$current_indent"/>
+ </xsl:call-template>
+ <FONT color="red">Then apply it to </FONT>
+ <xsl:apply-templates select="*[position()>2]"/>
+ </xsl:when>
+ <!-- by_induction -->
+ <xsl:when test="$name='by_induction'">
+ <FONT color="red">We prove </FONT>
+ <xsl:apply-templates select="../*[3]">
+ <xsl:with-param name="current_indent" select="$current_indent+18"/>
+ </xsl:apply-templates>
+ <br/>
+ <xsl:call-template name="make_indent">
+ <xsl:with-param name="current_indent" select="$current_indent"/>
+ </xsl:call-template>
+ <FONT color="red">by induction on </FONT>
+ <xsl:apply-templates select="*[position()=last()]/*[position()=last()]">
+ <xsl:with-param name="current_indent" select="$current_indent+30"/>
+ </xsl:apply-templates>
+ <!--
+ <br/>
+ <xsl:call-template name="make_indent">
+ <xsl:with-param name="current_indent" select="$current_indent"/>
+ </xsl:call-template>
+ <xsl:text>The induction property is</xsl:text>
+ <br/>
+ <xsl:call-template name="make_indent">
+ <xsl:with-param name="current_indent" select="$current_indent"/>
+ </xsl:call-template>
+ <xsl:apply-templates select="*[3]">
+ <xsl:with-param name="current_indent" select="$current_indent"/>
+ </xsl:apply-templates>
+ -->
+ <xsl:apply-templates
+ select="*[position()>3 and not(position()=last())]">
+ <xsl:with-param name="current_indent" select="$current_indent+4"/>
+ </xsl:apply-templates>
+ <!-- <br/>
+ <xsl:call-template name="make_indent">
+ <xsl:with-param name="current_indent" select="$current_indent"/>
+ </xsl:call-template>
+ <xsl:text>End induction</xsl:text> -->
+ </xsl:when>
+ <!-- inductive_case -->
+ <xsl:when test="$name='inductive_case'">
+ <br/>
+ <xsl:call-template name="make_indent">
+ <xsl:with-param name="current_indent" select="$current_indent"/>
+ </xsl:call-template>
+ <FONT color="red">Case </FONT>
+ <xsl:apply-templates select="*[2]">
+ <xsl:with-param name="current_indent" select="$current_indent +10"/>
+ </xsl:apply-templates>
+ <xsl:if test="*[3]/*[position()>1]">
+ <br/>
+ <xsl:call-template name="make_indent">
+ <xsl:with-param name="current_indent" select="$current_indent+4"/>
+ </xsl:call-template>
+ <FONT color="red">By induction hypothesis, we have:</FONT>
+ <xsl:for-each select="*[3]/*[position()>1]">
+ <br/>
+ <xsl:call-template name="make_indent">
+ <xsl:with-param name="current_indent" select="$current_indent + 4"/>
+ </xsl:call-template>
+ <xsl:text>(</xsl:text>
+ <xsl:apply-templates select="m:ci"/>
+ <xsl:text>) </xsl:text>
+ <xsl:apply-templates select="m:type">
+ <xsl:with-param name="current_indent" select="$current_indent + 8"/>
+ </xsl:apply-templates>
+ </xsl:for-each>
+ </xsl:if>
+ <br/>
+ <xsl:call-template name="make_indent">
+ <xsl:with-param name="current_indent" select="$current_indent + 4"/>
+ </xsl:call-template>
+ <xsl:apply-templates select="*[4]">
+ <xsl:with-param name="current_indent" select="$current_indent +4"/>
+ </xsl:apply-templates>
+ <!-- <br/>
+ <xsl:call-template name="make_indent">
+ <xsl:with-param name="current_indent" select="$current_indent"/>
+ </xsl:call-template>
+ <xsl:text>End Case</xsl:text> -->
+ </xsl:when>
+ <!-- case_lhs -->
+ <xsl:when test="$name='case_lhs'">
+ <xsl:choose>
+ <xsl:when test="count(*)=2">
+ <xsl:apply-templates mode="inline" select="*[2]"/>
+ </xsl:when>
+ <xsl:otherwise>
+ <xsl:text>(</xsl:text>
+ <xsl:apply-templates mode="inline" select="*[2]"/>
+ <xsl:for-each select="m:bvar">
+ <xsl:text> </xsl:text>
+ <xsl:apply-templates mode="inline" select="*[1]"/>
+ <xsl:text>:</xsl:text>
+ <xsl:apply-templates mode="inline" select="m:type/*[1]"/>
+ </xsl:for-each>
+ <xsl:text>)</xsl:text>
+ </xsl:otherwise>
+ </xsl:choose>
+ </xsl:when>
+ <!-- false_ind -->
+ <xsl:when test="$name='false_ind'">
+ <xsl:apply-templates select="*[3]">
+ <xsl:with-param name="current_indent" select="$current_indent"/>
+ </xsl:apply-templates>
+ <br/>
+ <xsl:call-template name="make_indent">
+ <xsl:with-param name="current_indent" select="$current_indent"/>
+ </xsl:call-template>
+ <FONT color="red">Contradiction.</FONT>
+ </xsl:when>
+ <!-- and_ind -->
+ <xsl:when test="$name='and_ind'">
+ <xsl:choose>
+ <xsl:when test="name(*[2])='m:apply'">
+ <xsl:apply-templates select="*[2]">
+ <xsl:with-param name="current_indent" select="$current_indent"/>
+ </xsl:apply-templates>
+ </xsl:when>
+ <xsl:otherwise>
+ <FONT color="red">Consider </FONT>
+ <xsl:apply-templates select="*[2]"/>
+ </xsl:otherwise>
+ </xsl:choose>
+ <br/>
+ <xsl:call-template name="make_indent">
+ <xsl:with-param name="current_indent" select="$current_indent"/>
+ </xsl:call-template>
+ <FONT color="red">In particular, we have</FONT>
+ <br/>
+ <xsl:call-template name="make_indent">
+ <xsl:with-param name="current_indent" select="$current_indent"/>
+ </xsl:call-template>
+ (
+ <xsl:apply-templates select="*[3]"/>
+ ) 
+ <xsl:apply-templates select="*[4]">
+ <xsl:with-param name="current_indent" select="$current_indent + 9"/>
+ </xsl:apply-templates>
+ <br/>
+ <xsl:call-template name="make_indent">
+ <xsl:with-param name="current_indent" select="$current_indent"/>
+ </xsl:call-template>
+ (
+ <xsl:apply-templates select="*[5]"/>
+ ) 
+ <xsl:apply-templates select="*[6]">
+ <xsl:with-param name="current_indent" select="$current_indent + 9"/>
+ </xsl:apply-templates>
+ <br/>
+ <xsl:call-template name="make_indent">
+ <xsl:with-param name="current_indent" select="$current_indent"/>
+ </xsl:call-template>
+ <xsl:apply-templates select="*[7]">
+ <xsl:with-param name="current_indent" select="$current_indent"/>
+ </xsl:apply-templates>
+ </xsl:when>
+ <!-- full_or_ind -->
+ <xsl:when test="$name='full_or_ind'">
+ <xsl:choose>
+ <xsl:when test="name(*[2])='m:apply'">
+ <xsl:apply-templates select="*[2]">
+ <xsl:with-param name="current_indent" select="$current_indent"/>
+ </xsl:apply-templates>
+ </xsl:when>
+ <xsl:otherwise>
+ <FONT color="red">Consider </FONT>
+ <xsl:apply-templates select="*[2]"/>
+ </xsl:otherwise>
+ </xsl:choose>
+ <br/>
+ <xsl:call-template name="make_indent">
+ <xsl:with-param name="current_indent" select="$current_indent"/>
+ </xsl:call-template>
+ <FONT color="red">We proceed by cases to prove </FONT>
+ <xsl:apply-templates select="*[3]"/>
+ <br/>
+ <xsl:call-template name="make_indent">
+ <xsl:with-param name="current_indent" select="$current_indent+4"/>
+ </xsl:call-template>
+ <FONT color="red">Left: suppose </FONT>
+ <xsl:text>(</xsl:text>
+ <xsl:value-of select="*[4]/m:bvar/m:ci"/>
+ <xsl:text>) </xsl:text>
+ <xsl:apply-templates
+ select="*[4]/m:bvar/m:type/*[1]"/>
+ <br/>
+ <xsl:call-template name="make_indent">
+ <xsl:with-param name="current_indent" select="$current_indent+15"/>
+ </xsl:call-template>
+ <xsl:apply-templates
+ select="*[4]/*[3]">
+ <xsl:with-param name="current_indent" select="$current_indent+15"/>
+ </xsl:apply-templates>
+ <br/>
+ <xsl:call-template name="make_indent">
+ <xsl:with-param name="current_indent" select="$current_indent+4"/>
+ </xsl:call-template>
+ <FONT color="red">Right: suppose </FONT>
+ <xsl:text>(</xsl:text>
+ <xsl:value-of select="*[5]/m:bvar/m:ci"/>
+ <xsl:text>) </xsl:text>
+ <xsl:apply-templates
+ select="*[5]/m:bvar/m:type/*[1]"/>
+ <br/>
+ <xsl:call-template name="make_indent">
+ <xsl:with-param name="current_indent" select="$current_indent+16"/>
+ </xsl:call-template>
+ <xsl:apply-templates
+ select="*[5]/*[3]">
+ <xsl:with-param name="current_indent" select="$current_indent+16"/>
+ </xsl:apply-templates>
+ </xsl:when>
+ <!-- or_ind -->
+ <xsl:when test="$name='or_ind'">
+ <xsl:choose>
+ <xsl:when test="name(*[2])='m:apply'">
+ <xsl:apply-templates select="*[2]">
+ <xsl:with-param name="current_indent" select="$current_indent"/>
+ </xsl:apply-templates>
+ </xsl:when>
+ <xsl:otherwise>
+ <FONT color="red">Consider </FONT>
+ <xsl:apply-templates select="*[2]"/>
+ </xsl:otherwise>
+ </xsl:choose>
+ <br/>
+ <xsl:call-template name="make_indent">
+ <xsl:with-param name="current_indent" select="$current_indent"/>
+ </xsl:call-template>
+ <FONT color="red">We prove </FONT>
+ <xsl:apply-templates select="*[3]"/>
+ <FONT color="red"> by cases:</FONT>
+ <br/>
+ <xsl:call-template name="make_indent">
+ <xsl:with-param name="current_indent" select="$current_indent"/>
+ </xsl:call-template>
+ Left: 
+ <xsl:apply-templates select="*[4]">
+ <xsl:with-param name="current_indent" select="$current_indent"/>
+ </xsl:apply-templates>
+ <br/>
+ <xsl:call-template name="make_indent">
+ <xsl:with-param name="current_indent" select="$current_indent"/>
+ </xsl:call-template>
+ Right: 
+ <xsl:apply-templates select="*[5]">
+ <xsl:with-param name="current_indent" select="$current_indent"/>
+ </xsl:apply-templates>
+ </xsl:when>
+ <!-- Ex_ind -->
+ <xsl:when test="$name='ex_ind'">
+ <xsl:choose>
+ <xsl:when test="name(*[2])='m:apply'">
+ <xsl:apply-templates select="*[2]">
+ <xsl:with-param name="current_indent" select="$current_indent"/>
+ </xsl:apply-templates>
+ </xsl:when>
+ <xsl:otherwise>
+ <FONT color="red">Consider </FONT>
+ <xsl:apply-templates select="*[2]">
+ <xsl:with-param name="current_indent" select="$current_indent"/>
+ </xsl:apply-templates>
+ </xsl:otherwise>
+ </xsl:choose>
+ <br/>
+ <xsl:call-template name="make_indent">
+ <xsl:with-param name="current_indent" select="$current_indent"/>
+ </xsl:call-template>
+ <FONT color="red">Let </FONT>
+ <xsl:apply-templates mode="inline" select="*[3]"/>
+ :
+ <xsl:apply-templates mode="inline" select="*[4]"/>
+ <FONT color="red"> such that</FONT>
+ <br/>
+ <xsl:call-template name="make_indent">
+ <xsl:with-param name="current_indent" select="$current_indent"/>
+ </xsl:call-template>
+ (
+ <xsl:apply-templates mode="inline" select="*[5]"/>
+ )
+ <xsl:apply-templates select="*[6]">
+ <xsl:with-param name="current_indent" select="$current_indent +7"/>
+ </xsl:apply-templates>
+ <br/>
+ <xsl:call-template name="make_indent">
+ <xsl:with-param name="current_indent" select="$current_indent"/>
+ </xsl:call-template>
+ <xsl:apply-templates select="*[7]">
+ <xsl:with-param name="current_indent" select="$current_indent"/>
+ </xsl:apply-templates>
+ </xsl:when>
+ <!-- ***************************************** -->
+ <!-- *********** LAMBDA ELEMENTS ************** -->
+ <!-- ***************************************** -->
+ <xsl:when test="$name='subst'">
+ <xsl:apply-templates select="*[3]"/>
+ <xsl:text>[</xsl:text>
+ <xsl:apply-templates select="*[4]"/>
+ <xsl:choose>
+ <xsl:when test="$uri != ''">
+ <a href="{$uri}">
+ <xsl:call-template name="mksymbol-1">
+ <xsl:with-param name="symbol" select="$name"/>
+ <xsl:with-param name="color" select="'blue'"/>
+ <xsl:with-param name="size" select="'+0'"/>
+ </xsl:call-template>
+ </a>
+ </xsl:when>
+ <xsl:otherwise>
+ <xsl:call-template name="mksymbol-1">
+ <xsl:with-param name="symbol" select="$name"/>
+ <xsl:with-param name="color" select="'blue'"/>
+ <xsl:with-param name="size" select="'+0'"/>
+ </xsl:call-template>
+ </xsl:otherwise>
+ </xsl:choose>
+ <xsl:apply-templates select="*[2]"/>
+ <xsl:text>]</xsl:text>
+ </xsl:when>
+
+ <xsl:when test="$name='lift_with_base'">
+ <SUB>
+ <xsl:apply-templates select="*[3]" mode="inline"/>
+ </SUB>
+ <xsl:choose>
+ <xsl:when test="$uri != ''">
+ <a href="{$uri}">
+ <xsl:call-template name="mksymbol-1">
+ <xsl:with-param name="symbol" select="$name"/>
+ <xsl:with-param name="color" select="'green'"/>
+ <xsl:with-param name="size" select="'+0'"/>
+ </xsl:call-template>
+ </a>
+ </xsl:when>
+ <xsl:otherwise>
+ <xsl:call-template name="mksymbol-1">
+ <xsl:with-param name="symbol" select="$name"/>
+ <xsl:with-param name="color" select="'green'"/>
+ <xsl:with-param name="size" select="'+0'"/>
+ </xsl:call-template>
+ </xsl:otherwise>
+ </xsl:choose>
+ <SUP>
+ <xsl:apply-templates select="*[4]" mode="inline"/>
+ </SUP>
+ <xsl:text>(</xsl:text>
+ <xsl:apply-templates select="*[2]" mode="inline"/>
+ <xsl:text>)</xsl:text>
+ </xsl:when>
+
+ <xsl:when test="$name='lift'">
+ <xsl:choose>
+ <xsl:when test="$uri != ''">
+ <a href="{$uri}">
+ <xsl:call-template name="mksymbol-1">
+ <xsl:with-param name="symbol" select="$name"/>
+ <xsl:with-param name="color" select="'green'"/>
+ <xsl:with-param name="size" select="'+0'"/>
+ </xsl:call-template>
+ </a>
+ </xsl:when>
+ <xsl:otherwise>
+ <xsl:call-template name="mksymbol-1">
+ <xsl:with-param name="symbol" select="$name"/>
+ <xsl:with-param name="color" select="'green'"/>
+ <xsl:with-param name="size" select="'+0'"/>
+ </xsl:call-template>
+ </xsl:otherwise>
+ </xsl:choose>
+ <SUP>
+ <xsl:apply-templates select="*[2]" mode="inline"/>
+ </SUP>
+ <xsl:text>(</xsl:text>
+ <xsl:apply-templates select="*[3]" mode="inline"/>
+ <xsl:text>)</xsl:text>
+ </xsl:when>
+
+ <!-- reduction -->
+ <xsl:when test="$name='beta_red1'">
+ <xsl:apply-templates select="*[2]" mode="inline"/>
+ <xsl:choose>
+ <xsl:when test="$uri != ''">
+ <a href="{$uri}">
+ <xsl:call-template name="mksymbol-1">
+ <xsl:with-param name="symbol" select="$name"/>
+ <xsl:with-param name="color" select="'green'"/>
+ <xsl:with-param name="size" select="'+0'"/>
+ </xsl:call-template>
+ <SUB>
+ <xsl:call-template name="mksymbol-1">
+ <xsl:with-param name="symbol" select="'beta'"/>
+ <xsl:with-param name="color" select="'green'"/>
+ <xsl:with-param name="size" select="'+0'"/>
+ </xsl:call-template>
+ </SUB>
+ </a>
+ </xsl:when>
+ <xsl:otherwise>
+ <xsl:call-template name="mksymbol-1">
+ <xsl:with-param name="symbol" select="$name"/>
+ <xsl:with-param name="color" select="'green'"/>
+ <xsl:with-param name="size" select="'+0'"/>
+ </xsl:call-template>
+ <SUB>
+ <xsl:call-template name="mksymbol-1">
+ <xsl:with-param name="symbol" select="'beta'"/>
+ <xsl:with-param name="color" select="'green'"/>
+ <xsl:with-param name="size" select="'+0'"/>
+ </xsl:call-template>
+ </SUB>
+ </xsl:otherwise>
+ </xsl:choose>
+ <xsl:apply-templates select="*[3]" mode="inline"/>
+ </xsl:when>
+
+ <xsl:when test="$name='beta_red'">
+ <xsl:apply-templates select="*[2]" mode="inline"/>
+ <xsl:choose>
+ <xsl:when test="$uri != ''">
+ <a href="{$uri}">
+ <xsl:call-template name="mksymbol-1">
+ <xsl:with-param name="symbol" select="$name"/>
+ <xsl:with-param name="color" select="'green'"/>
+ <xsl:with-param name="size" select="'+0'"/>
+ </xsl:call-template>
+ <SUB>
+ <xsl:call-template name="mksymbol-1">
+ <xsl:with-param name="symbol" select="'beta'"/>
+ <xsl:with-param name="color" select="'green'"/>
+ <xsl:with-param name="size" select="'+0'"/>
+ </xsl:call-template>
+ <xsl:text>*</xsl:text>
+ </SUB>
+ </a>
+ </xsl:when>
+ <xsl:otherwise>
+ <xsl:call-template name="mksymbol-1">
+ <xsl:with-param name="symbol" select="$name"/>
+ <xsl:with-param name="color" select="'green'"/>
+ <xsl:with-param name="size" select="'+0'"/>
+ </xsl:call-template>
+ <SUB>
+ <xsl:call-template name="mksymbol-1">
+ <xsl:with-param name="symbol" select="'beta'"/>
+ <xsl:with-param name="color" select="'green'"/>
+ <xsl:with-param name="size" select="'+0'"/>
+ </xsl:call-template>
+ <xsl:text>*</xsl:text>
+ </SUB>
+ </xsl:otherwise>
+ </xsl:choose>
+ <xsl:apply-templates select="*[3]" mode="inline"/>
+ </xsl:when>
+
+ <xsl:when test="$name='par_beta_red1'">
+ <xsl:apply-templates select="*[2]" mode="inline"/>
+ <xsl:choose>
+ <xsl:when test="$uri != ''">
+ <a href="{$uri}">
+ <xsl:call-template name="mksymbol-1">
+ <xsl:with-param name="symbol" select="$name"/>
+ <xsl:with-param name="color" select="'green'"/>
+ <xsl:with-param name="size" select="'+0'"/>
+ </xsl:call-template>
+ <SUB>
+ <xsl:call-template name="mksymbol-1">
+ <xsl:with-param name="symbol" select="'beta'"/>
+ <xsl:with-param name="color" select="'green'"/>
+ <xsl:with-param name="size" select="'+0'"/>
+ </xsl:call-template>
+ </SUB>
+ </a>
+ </xsl:when>
+ <xsl:otherwise>
+ <xsl:call-template name="mksymbol-1">
+ <xsl:with-param name="symbol" select="$name"/>
+ <xsl:with-param name="color" select="'green'"/>
+ <xsl:with-param name="size" select="'+0'"/>
+ </xsl:call-template>
+ <SUB>
+ <xsl:call-template name="mksymbol-1">
+ <xsl:with-param name="symbol" select="'beta'"/>
+ <xsl:with-param name="color" select="'green'"/>
+ <xsl:with-param name="size" select="'+0'"/>
+ </xsl:call-template>
+ </SUB>
+ </xsl:otherwise>
+ </xsl:choose>
+ <xsl:apply-templates select="*[3]" mode="inline"/>
+ </xsl:when>
+
+ <xsl:when test="$name='par_beta_red'">
+ <xsl:apply-templates select="*[2]" mode="inline"/>
+ <xsl:choose>
+ <xsl:when test="$uri != ''">
+ <a href="{$uri}">
+ <xsl:call-template name="mksymbol-1">
+ <xsl:with-param name="symbol" select="$name"/>
+ <xsl:with-param name="color" select="'green'"/>
+ <xsl:with-param name="size" select="'+0'"/>
+ </xsl:call-template>
+ <SUB>
+ <xsl:call-template name="mksymbol-1">
+ <xsl:with-param name="symbol" select="'beta'"/>
+ <xsl:with-param name="color" select="'green'"/>
+ <xsl:with-param name="size" select="'+0'"/>
+ </xsl:call-template>
+ <xsl:text>*</xsl:text>
+ </SUB>
+ </a>
+ </xsl:when>
+ <xsl:otherwise>
+ <xsl:call-template name="mksymbol-1">
+ <xsl:with-param name="symbol" select="$name"/>
+ <xsl:with-param name="color" select="'green'"/>
+ <xsl:with-param name="size" select="'+0'"/>
+ </xsl:call-template>
+ <SUB>
+ <xsl:call-template name="mksymbol-1">
+ <xsl:with-param name="symbol" select="'beta'"/>
+ <xsl:with-param name="color" select="'green'"/>
+ <xsl:with-param name="size" select="'+0'"/>
+ </xsl:call-template>
+ <xsl:text>*</xsl:text>
+ </SUB>
+ </xsl:otherwise>
+ </xsl:choose>
+ <xsl:apply-templates select="*[3]" mode="inline"/>
+ </xsl:when>
+
+ <!-- forgetful -->
+ <xsl:when test="$name='forgetful'">
+ <xsl:choose>
+ <xsl:when test="$uri != ''">
+ <a href="{$uri}">|</a>
+ </xsl:when>
+ <xsl:otherwise>
+ |
+ </xsl:otherwise>
+ </xsl:choose>
+ <xsl:apply-templates select="*[2]" mode="inline"/>
+ <xsl:choose>
+ <xsl:when test="$uri != ''">
+ <a href="{$uri}">|</a>
+ </xsl:when>
+ <xsl:otherwise>
+ |
+ </xsl:otherwise>
+ </xsl:choose>
+ </xsl:when>
+
+ <!-- boolean algebra of redexes -->
+
+ <!-- isomorphic -->
+ <xsl:when test="$name='isomorphic'">
+ <xsl:apply-templates select="*[2]" mode="inline"/>
+ <xsl:choose>
+ <xsl:when test="$uri != ''">
+ <a href="{$uri}">
+ <xsl:call-template name="mksymbol-1">
+ <xsl:with-param name="symbol" select="$name"/>
+ <xsl:with-param name="color" select="'green'"/>
+ <xsl:with-param name="size" select="'+0'"/>
+ </xsl:call-template>
+ </a>
+ </xsl:when>
+ <xsl:otherwise>
+ <xsl:call-template name="mksymbol-1">
+ <xsl:with-param name="symbol" select="$name"/>
+ <xsl:with-param name="color" select="'green'"/>
+ <xsl:with-param name="size" select="'+0'"/>
+ </xsl:call-template>
+ </xsl:otherwise>
+ </xsl:choose>
+ <xsl:apply-templates select="*[3]" mode="inline"/>
+ </xsl:when>
+
+ <!-- INTERP -->
+ <xsl:when test="$name='interp'">
+ <font color="green">[</font>
+ <xsl:apply-templates select="*[2]"/>
+ <font color="green">]</font>
+ </xsl:when>
+
+ </xsl:choose>
+</xsl:template>
+
+<!-- LAMBDA -->
+
<xsl:template match="m:lambda">
<xsl:param name="current_indent" select="0"/>
<xsl:variable name="charlength">
<!-- <xsl:apply-templates select="." mode="charcount"/> -->
</xsl:variable>
<!-- <xsl:value-of select="$charlength"/> -->
+ <!-- <xsl:value-of select="$current_indent"/> -->
<xsl:choose>
<xsl:when test="$charlength > $framewidth">
<!-- λ -->
- <FONT FACE="symbol" SIZE="+2" color="red">l</FONT>
+ <xsl:call-template name="mksymbol-1">
+ <xsl:with-param name="symbol" select="'lambda'"/>
+ <xsl:with-param name="color" select="'red'"/>
+ <xsl:with-param name="size" select="'+2'"/>
+ </xsl:call-template>
<xsl:apply-templates select="m:bvar/m:ci"/>
<xsl:text>:</xsl:text>
<xsl:apply-templates select="m:bvar/m:type">
<xsl:with-param name="current_indent"
- select="$current_indent + 2 + string-length(m:bvar/m:ci)"/>
- </xsl:apply-templates><BR/>
+ select="$current_indent + 4 + 2*string-length(m:bvar/m:ci)"/>
+ </xsl:apply-templates><br/>
<xsl:call-template name="make_indent">
<xsl:with-param name="current_indent" select="$current_indent + 2"/>
</xsl:call-template>
</xsl:apply-templates>
</xsl:when>
<xsl:otherwise>
- <!-- λ -->
- <FONT FACE="symbol" SIZE="+2" color="red">l</FONT>
- <xsl:apply-templates select="m:bvar/m:ci"/>
- <xsl:text>:</xsl:text>
- <xsl:apply-templates select="m:bvar/m:type"/>
- <xsl:text>.</xsl:text>
- <xsl:apply-templates select="*[position()=2]"/>
+ <xsl:apply-templates mode="inline" select="."/>
</xsl:otherwise>
</xsl:choose>
</xsl:template>
<xsl:template match="m:ci">
<xsl:choose>
<xsl:when test="boolean(@definitionURL)">
-<!-- CSC: non bisogna piu' utilizzare la url, bensi' la uri -->
-<!-- <xsl:variable name="url">
- <xsl:value-of select="concat(string($absPath),
- @definitionURL)"/>
- </xsl:variable>-->
- <a>
- <xsl:attribute name="href">
- <xsl:value-of select="concat(string($header),string(@definitionURL))"/>
- </xsl:attribute>
+ <a href="{@definitionURL}">
<xsl:apply-templates/>
</a>
</xsl:when>
</xsl:choose>
</xsl:template>
-<!-- COUNTING -->
+<!-- CHAR COUNTING -->
+
+<!-- enter this counting mode selecting the root -->
+<xsl:template match="*" mode="root_charcount">
+<xsl:param name="incurrent_length" select="0"/>
+ <xsl:choose>
+ <xsl:when test="count(*)=0">
+ <xsl:value-of select="0"/>
+ </xsl:when>
+ <xsl:when test="name()='m:ci'">
+ <xsl:value-of select="string-length()"/>
+ </xsl:when>
+ <xsl:otherwise>
+ <xsl:apply-templates select="*[1]" mode="charcount">
+ <xsl:with-param name="incurrent_length" select="$incurrent_length"/>
+ </xsl:apply-templates>
+ </xsl:otherwise>
+ </xsl:choose>
+</xsl:template>
+
+<!-- enter this mode selecting the first child -->
<xsl:template match="m:ci|m:csymbol" mode="charcount">
<xsl:param name="incurrent_length" select="0"/>
<xsl:template match="Definition">
<xsl:param name="current_indent" select="0"/>
<p>
-DEFINITION <xsl:value-of select="@name"/>(<xsl:if test="string(./Params) != """><xsl:value-of select="Params"/></xsl:if>)<BR/>
-TYPE =<BR/>
+DEFINITION <xsl:value-of select="@name"/>(<xsl:if test="string(./Params) != """><xsl:value-of select="Params"/></xsl:if>)<br/>
+TYPE =<br/>
<xsl:call-template name="make_indent">
<xsl:with-param name="current_indent" select="$current_indent + 7"/>
</xsl:call-template>
<xsl:apply-templates select="type/*[1]">
<xsl:with-param name="current_indent" select="$current_indent + 7"/>
- </xsl:apply-templates><BR/>
-BODY =<BR/>
+ </xsl:apply-templates><br/>
+BODY =<br/>
<xsl:call-template name="make_indent">
<xsl:with-param name="current_indent" select="$current_indent + 7"/>
</xsl:call-template>
<xsl:template match="Axiom">
<xsl:param name="current_indent" select="0"/>
<p>
-AXIOM <xsl:value-of select="@name"/>(<xsl:if test="string(./Params) != """><xsl:value-of select="Params"/></xsl:if>)<BR/>
-TYPE = <xsl:apply-templates select="type/*[1]">
+AXIOM <xsl:value-of select="@name"/>(<xsl:if test="string(./Params) != """><xsl:value-of select="Params"/></xsl:if>)<br/>
+TYPE =<br/>
+ <xsl:call-template name="make_indent">
+ <xsl:with-param name="current_indent" select="$current_indent + 7"/>
+ </xsl:call-template>
+<xsl:apply-templates select="type/*[1]">
<xsl:with-param name="current_indent" select="$current_indent + 7"/>
</xsl:apply-templates>
</p>
<xsl:template match="CurrentProof">
<xsl:param name="current_indent" select="0"/>
<p>
-UNFINISHED PROOF <xsl:value-of select="@name"/>(<xsl:if test="string(./Params) != """><xsl:value-of select="Params"/></xsl:if>)<BR/>
+UNFINISHED PROOF <xsl:value-of select="@name"/>(<xsl:if test="string(./Params) != """><xsl:value-of select="Params"/></xsl:if>)<br/>
THESIS: <xsl:apply-templates select="type/*[1]">
<xsl:with-param name="current_indent" select="$current_indent + 8"/>
- </xsl:apply-templates><BR/>
+ </xsl:apply-templates><br/>
CONJECTURES:
<xsl:for-each select="Conjecture">
- <BR/>
+ <br/>
<xsl:call-template name="make_indent">
<xsl:with-param name="current_indent" select="$current_indent + 8"/>
</xsl:call-template>
- <xsl:value-of select="./@no"/> :
- <xsl:apply-templates select="./*[1]">
+ <xsl:for-each select="Decl|Def|Hidden">
+ <xsl:choose>
+ <xsl:when test="name(.)='Decl'">
+ <xsl:choose>
+ <xsl:when test="@name">
+ <xsl:value-of select="@name"/>
+ </xsl:when>
+ <xsl:otherwise>
+ <xsl:text>_</xsl:text>
+ </xsl:otherwise>
+ </xsl:choose>
+ <xsl:text> : </xsl:text>
+ <xsl:apply-templates select="./*[1]">
+ <xsl:with-param name="current_indent" select="$current_indent"/>
+ </xsl:apply-templates>
+ </xsl:when>
+ <xsl:when test="name(.)='Def'">
+ <xsl:choose>
+ <xsl:when test="@name">
+ <xsl:value-of select="@name"/>
+ </xsl:when>
+ <xsl:otherwise>
+ <xsl:text>_</xsl:text>
+ </xsl:otherwise>
+ </xsl:choose>
+ <xsl:text> := </xsl:text>
+ <xsl:apply-templates select="./*[1]">
+ <xsl:with-param name="current_indent" select="$current_indent"/>
+ </xsl:apply-templates>
+ </xsl:when>
+ <xsl:otherwise>
+ <xsl:text> _ :? _ </xsl:text>
+ </xsl:otherwise>
+ </xsl:choose>
+ </xsl:for-each>
+ |- <xsl:value-of select="./@no"/> :
+ <xsl:apply-templates select="./Goal/*[1]">
<xsl:with-param name="current_indent" select="$current_indent + 11"/>
</xsl:apply-templates>
</xsl:for-each>
- <BR/>
+ <br/>
PROOF:
<xsl:apply-templates select="body/*[1]">
<xsl:with-param name="current_indent" select="$current_indent + 8"/>
<xsl:apply-templates select="*"/>
</xsl:for-each>
</xsl:if>
- ] <BR/>
+ ] <br/>
OF ARITY
<xsl:apply-templates select="./arity/*[1]">
<xsl:with-param name="current_indent" select="$current_indent + 9"/>
- </xsl:apply-templates> <BR/>
+ </xsl:apply-templates> <br/>
BUILT FROM:
<xsl:for-each select="./Constructor">
- <BR/>
+ <br/>
<xsl:call-template name="make_indent">
<xsl:with-param name="current_indent" select="$current_indent + 3"/>
</xsl:call-template>
<xsl:text>| </xsl:text>
</xsl:otherwise>
</xsl:choose>
- <xsl:value-of select="./@name"/>
+ <xsl:value-of select="./@name"/>
<xsl:text>: </xsl:text>
<xsl:apply-templates select="./*[1]">
- <xsl:with-param name="current_indent" select="$current_indent + string-length(./@name) + 4"/>
+ <xsl:with-param name="current_indent" select="$current_indent + 2*string-length(./@name) + 5"/>
</xsl:apply-templates>
</xsl:for-each>
</xsl:for-each>
<xsl:template match="Variable">
<xsl:param name="current_indent" select="0"/>
<p>
-VARIABLE <xsl:value-of select="@name"/><BR/>
+VARIABLE <xsl:value-of select="@name"/><br/>
TYPE = <xsl:apply-templates select="type/*[1]">
<xsl:with-param name="current_indent" select="$current_indent + 7"/>
</xsl:apply-templates>
+<xsl:if test="body">
+<br/>
+BODY = <xsl:apply-templates select="body/*[1]">
+ <xsl:with-param name="current_indent" select="$current_indent + 7"/>
+ </xsl:apply-templates>
+</xsl:if>
</p>
</xsl:template>