<xsl:include href="html_init.xsl"/>
<xsl:include href="html_set.xsl"/>
<xsl:include href="html_reals.xsl"/>
+<xsl:include href="html_ccorns.xsl"/>
<xsl:variable name="showcast" select="0"/>
<xsl:when test="$UNICODEvsSYMBOL = 'symbol'">
<xsl:variable name="fontsymbol">
<xsl:choose>
+ <xsl:when test="$symbol = 'append'">
+ <xsl:value-of select="'@'"/>
+ </xsl:when>
+ <xsl:when test="$symbol = 'iff'">
+ <xsl:value-of select="'«'"/>
+ </xsl:when>
<xsl:when test="$symbol = 'forall'">
<xsl:value-of select="'"'"/>
</xsl:when>
<xsl:otherwise>
<xsl:variable name="unicodesymbol">
<xsl:choose>
+ <xsl:when test="$symbol = 'append'">
+ <xsl:value-of select="'@'"/>
+ </xsl:when>
+ <xsl:when test="$symbol = 'iff'">
+ <xsl:value-of select="'↔'"/>
+ </xsl:when>
<xsl:when test="$symbol = 'forall'">
<xsl:value-of select="'∀'"/>
</xsl:when>
<xsl:template name="make_indent">
<xsl:param name="current_indent" select="0"/>
+ <!-- non funziona bene con netscape !!!
+ <span>
+ <xsl:attribute name="style">
+ <xsl:value-of select="concat('margin-left:',string($current_indent div 3), 'em')"/>
+ </xsl:attribute>
+ </span> -->
<xsl:if test="$current_indent > 0">
<xsl:text> </xsl:text>
<xsl:call-template name="make_indent">
<xsl:apply-templates mode="inline" select="*[position()=3]"/>
<xsl:text>)</xsl:text>
</xsl:when>
+ <!-- IFF -->
+ <xsl:when test="$name='iff'">
+ <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>
+ <!-- APPEND -->
+ <xsl:when test="$name='append'">
+ <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:when test="$name='cast'">
<xsl:text>(</xsl:text>
<xsl:apply-templates mode="inline" select="*[position()=2]"/>
- <xsl:text>:></xsl:text>
+ <xsl:text>:</xsl:text>
<xsl:apply-templates mode="inline" select="*[position()=3]"/>
<xsl:text>)</xsl:text>
</xsl:when>
<FONT color="red">CASE </FONT>
<xsl:apply-templates mode="inline" select="*[position()=3]"/>
<FONT color="red"> OF </FONT>
-<xsl:for-each select="piecewise/piece">
+ <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: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'"/>
select="./*[1]"/>
</xsl:for-each>
</xsl:when>
+
+ <xsl:when test="$name='inst'">
+ <xsl:apply-templates select="*[2]" mode="inline"/>
+ <FONT color="blue">{</FONT>
+ <xsl:for-each select="*[(position()>2) and (position() mod 2 = 1)]">
+ <xsl:apply-templates select="following-sibling::*[position() = 1]" mode="inline"/>
+ <FONT color="blue">/</FONT>
+ <xsl:if test="name()='m:ci'">
+ <a href="{@definitionURL}">
+ <xsl:apply-templates/>
+ </a>
+ </xsl:if>
+ <!-- <xsl:apply-templates select="." mode="inline"/> -->
+ </xsl:for-each>
+ <FONT color="blue">}</FONT>
+ </xsl:when>
+
<!-- FIX -->
<xsl:when test="$name='fix'">
<FONT color="red">FIX</FONT>
</xsl:choose>
</xsl:for-each>
</xsl:when>
- <!-- proof -->
+ <!-- if then else -->
+ <xsl:when test="$name='ite'">
+ <xsl:text>if </xsl:text>
+ <xsl:apply-templates select="*[2]"/>
+ <xsl:text> then </xsl:text>
+ <xsl:apply-templates select="*[3]"/>
+ <xsl:text> else </xsl:text>
+ <xsl:apply-templates select="*[4]"/>
+ </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>
<!-- <xsl:value-of select="$charlength"/> -->
<xsl:variable name="uri"><xsl:value-of select="*[1]/@definitionURL"/></xsl:variable>
<xsl:choose>
+ <!-- inst -->
+ <xsl:when test="$name='inst'">
+ <xsl:apply-templates select="." mode="inline"/>
+ </xsl:when>
<!-- FORALL -->
<xsl:when test="$name='forall'">
<xsl:choose>
</xsl:otherwise>
</xsl:choose>
</xsl:when>
+ <!-- IFF -->
+ <xsl:when test="$name='iff'">
+ <xsl:choose>
+ <xsl:when test="$charlength > $framewidth">
+ <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:call-template name="make_indent">
+ <xsl:with-param name="current_indent" select="$current_indent + 2"/>
+ </xsl:call-template>
+ <!-- -> -->
+ <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:apply-templates mode="inline" select="."/>
+ </xsl:otherwise>
+ </xsl:choose>
+ </xsl:when>
+ <!-- APPEND -->
+ <xsl:when test="$name='append'">
+ <xsl:choose>
+ <xsl:when test="$charlength > $framewidth">
+ <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:call-template name="make_indent">
+ <xsl:with-param name="current_indent" select="$current_indent + 2"/>
+ </xsl:call-template>
+ <!-- -> -->
+ <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:apply-templates mode="inline" select="."/>
+ </xsl:otherwise>
+ </xsl:choose>
+ </xsl:when>
<!-- APP -->
<xsl:when test="$name='app'">
<xsl:choose>
<xsl:with-param name="current_indent" select="$current_indent + 8"/>
</xsl:apply-templates>
<xsl:text> OF </xsl:text>
- <xsl:for-each select="piecewise/piece">
+ <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+5"/>
</xsl:apply-templates>
</xsl:when>
+ <!-- it then else -->
+ <xsl:when test="$name='ite'">
+ <xsl:text>if </xsl:text>
+ <xsl:apply-templates select="*[2]">
+ <xsl:with-param name="current_indent" select="$current_indent + 5"/>
+ </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> then </xsl:text>
+ <xsl:apply-templates select="*[3]">
+ <xsl:with-param name="current_indent" select="$current_indent + 12"/>
+ </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> else </xsl:text>
+ <xsl:apply-templates select="*[4]">
+ <xsl:with-param name="current_indent" select="$current_indent + 12"/>
+ </xsl:apply-templates>
+ </xsl:when>
<!-- ***************************************** -->
<!-- *********** PROOF ELEMENTS ************** -->
<xsl:with-param name="current_indent" select="$current_indent"/>
</xsl:apply-templates>
 
+ <xsl:if test="*[4]">
+ <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:apply-templates select="*[position()=3]">
+ <xsl:with-param name="current_indent" select="$current_indent+16"/>
+ </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">and by delta equivalence</FONT>
+ <xsl:apply-templates select="*[position()=5]">
+ <xsl:with-param name="current_indent" select="$current_indent+16"/>
+ </xsl:apply-templates>
+ </xsl:if>
</span>
<xsl:choose>
<xsl:when test="(preceding-sibling::*[1]/text()='letin1') or
<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>\
+ <a style="text-decoration:underline ; color:red" href="" onClick="Hide(document.getElementById(\'{$freshid1}\')); Show(document.getElementById(\'{$freshid2}\'));Hide(document.getElementById(\'{$freshid3}\'));return (0==1);">we obtain</a>\
</span>\
');
document.to_be_deleted.push('<xsl:value-of select="$freshid1"/>');
</script>
</xsl:otherwise>
</xsl:choose>
- <xsl:apply-templates select="*[position()=3]">
+ <xsl:apply-templates select="*[position()=last()]">
<xsl:with-param name="current_indent" select="$current_indent + 16"/>
</xsl:apply-templates>
</xsl:when>
<xsl:with-param name="current_indent" select="$current_indent"/>
</xsl:apply-templates>
</xsl:when>
- </xsl:choose>
- <xsl:choose>
<xsl:when test="name(.)='Def'">
<xsl:choose>
<xsl:when test="@name">
<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:otherwise>
- <xsl:text> _ :? _ </xsl:text>
- </xsl:otherwise>
</xsl:for-each>
|- <xsl:value-of select="./@no"/> :
<xsl:apply-templates select="./Goal/*[1]">