<xsl:variable name="name"><xsl:value-of select="m:csymbol"/></xsl:variable>
<xsl:variable name="charlength"><xsl:apply-templates select="m:csymbol" mode="charcount"/></xsl:variable>
<m:mrow>
- <xsl:if test="@helm:xref">
+ <xsl:if test="@id">
<xsl:attribute name="m:xref"><xsl:value-of select="@id"/></xsl:attribute>
</xsl:if>
+ <xsl:variable name="id" select="m:csymbol/@id"/>
<xsl:choose>
<!-- FORALL -->
<xsl:when test="$name='forall'">
</m:mrow>
</m:mtd>
</m:mtr>
- <xsl:for-each select="*[position() mod 2 = 0 and position()>3]">
- <xsl:variable name="charlength"><xsl:apply-templates select="." mode="charcount"><xsl:with-param name="nosibling" select="1"/></xsl:apply-templates></xsl:variable>
+ <xsl:for-each select="piecewise/piece">
+ <xsl:variable name="charlength"><xsl:apply-templates select="./*[2]" mode="charcount"><xsl:with-param name="nosibling" select="1"/></xsl:apply-templates></xsl:variable>
<m:mtr>
<m:mtd>
<m:mrow>
</xsl:otherwise>
</xsl:choose>
<m:mphantom><m:mtext>_</m:mtext></m:mphantom>
- <xsl:apply-templates select="."/>
+ <xsl:apply-templates select="./*[2]"/>
<xsl:if test="$framewidth > $charlength">
<m:mo mathcolor="Green">⇒</m:mo>
- <xsl:apply-templates select="following-sibling::*[position()= 1]"/>
+ <xsl:apply-templates select="./*[1]"/>
</xsl:if>
</m:mrow>
</m:mtd>
<m:mrow>
<m:mphantom><m:mtext>|_</m:mtext></m:mphantom>
<m:mo mathcolor="Green">⇒</m:mo>
- <xsl:apply-templates select="following-sibling::*[position()= 1]"/>
+ <xsl:apply-templates select="./*[1]"/>
</m:mrow>
</m:mtd>
</m:mtr>
<xsl:apply-templates select="*[position()=3]"/>
<m:mphantom><m:mtext>_</m:mtext></m:mphantom>
<m:mo>OF</m:mo>
- <xsl:for-each select="*[position() mod 2 = 0 and position()>3]">
+ <xsl:for-each select="piecewise/piece">
<xsl:choose>
<xsl:when test="position() != 1">
<m:mo stretchy="false">|</m:mo>
</xsl:when>
</xsl:choose>
- <xsl:apply-templates select="."/>
+ <xsl:apply-templates select="./*[2]"/>
<m:mo mathcolor="Green">⇒</m:mo>
- <xsl:apply-templates select="following-sibling::*[position()= 1]"/>
+ <xsl:apply-templates select="./*[1]"/>
</xsl:for-each>
<m:mphantom><m:mtext>_</m:mtext></m:mphantom>
<m:mo>END</m:mo>
<!-- ***************************************** -->
<!-- PROOF -->
<xsl:when test="$name='proof'">
- <m:maction actiontype="toggle">
- <!-- CSC: next if until the annotationHelper can handle mactions -->
- <xsl:if test="not($explodeall)">
- <!-- Details hided (default) -->
+ <!-- CSC: $explodeall until the annotationHelper can handle mactions -->
+ <xsl:variable name="test" select="(not($explodeall)) and
+ (not(preceding-sibling::*[1]/text()='letin1')) and
+ (not(preceding-sibling::*[1]/text()='rw_step')) and
+ (not(name(..)='m:lambda'))"/>
+ <xsl:variable name="hidden_details">
+ <xsl:if test="$test">
+ <!-- Details hided (default) -->
+ <m:mtable align="baseline 1" equalrows="false" columnalign="left">
+ <m:mtr>
+ <m:mtd>
+ <m:mrow>
+ <m:mtext mathcolor="Maroon">We can prove</m:mtext>
+ <m:mphantom><m:mtext>_</m:mtext></m:mphantom>
+ <xsl:apply-templates select="*[position()=3]"/>
+ <m:mrow>
+ <m:mphantom><m:mtext>_</m:mtext></m:mphantom>
+ <m:mtext mathcolor="Green">(explain)</m:mtext>
+ </m:mrow>
+ </m:mrow>
+ </m:mtd>
+ </m:mtr>
+ </m:mtable>
+ </xsl:if>
+ </xsl:variable>
+ <xsl:variable name="shown_details">
+ <!-- Show details -->
<m:mtable align="baseline 1" equalrows="false" columnalign="left">
<m:mtr>
<m:mtd>
<m:mrow>
- <m:mtext mathcolor="Maroon">We can prove</m:mtext>
+ <xsl:apply-templates select="*[position()=2]"/>
+ </m:mrow>
+ </m:mtd>
+ </m:mtr>
+ <m:mtr>
+ <m:mtd>
+ <m:mrow>
+ <m:mtext mathcolor="Maroon">we proved</m:mtext>
<m:mphantom><m:mtext>_</m:mtext></m:mphantom>
<xsl:apply-templates select="*[position()=3]"/>
<m:mrow>
- <m:mphantom><m:mtext>_</m:mtext></m:mphantom>
- <m:mtext mathcolor="Green">(explain)</m:mtext>
+ <m:mphantom>
+ <m:mtext>_</m:mtext>
+ </m:mphantom>
+ <xsl:if test="$test">
+ <m:mtext mathcolor="Green">(hide details)</m:mtext>
+ </xsl:if>
</m:mrow>
</m:mrow>
</m:mtd>
</m:mtr>
</m:mtable>
- </xsl:if>
- <!-- Show details -->
- <m:mtable align="baseline 1" equalrows="false" columnalign="left">
- <m:mtr>
- <m:mtd>
- <m:mrow>
- <xsl:apply-templates select="*[position()=2]"/>
- </m:mrow>
- </m:mtd>
- </m:mtr>
- <m:mtr>
- <m:mtd>
- <m:mrow>
- <m:mtext mathcolor="Maroon">we proved</m:mtext>
- <m:mphantom><m:mtext>_</m:mtext></m:mphantom>
- <xsl:apply-templates select="*[position()=3]"/>
- <m:mrow>
- <m:mphantom>
- <m:mtext>_</m:mtext>
- </m:mphantom>
- <m:mtext mathcolor="Green">(hide details)</m:mtext>
- </m:mrow>
- </m:mrow>
- </m:mtd>
- </m:mtr>
- </m:mtable>
- </m:maction>
+ </xsl:variable>
+ <xsl:choose>
+ <xsl:when test="$test">
+ <m:maction actiontype="toggle">
+ <xsl:copy-of select="$hidden_details"/>
+ <xsl:copy-of select="$shown_details"/>
+ </m:maction>
+ </xsl:when>
+ <xsl:otherwise>
+ <xsl:copy-of select="$shown_details"/>
+ </xsl:otherwise>
+ </xsl:choose>
</xsl:when>
<!-- LETIN1 -->
<xsl:when test="$name='letin1'">
</m:mtr>
</m:mtable>
</xsl:when>
+ <!-- ***************************************** -->
+ <!-- *********** NOTATIONS ******************* -->
+ <!-- ***************************************** -->
+ <!-- subst -->
+ <xsl:when test="$name='subst'">
+ <xsl:apply-templates select="*[3]"/>
+<!-- no font for ApplyFunction: <m:mo></m:mo> -->
+ <m:mo stretchy="false">[</m:mo>
+ <xsl:apply-templates select="*[4]"/>
+ <m:mo mathcolor="green">
+ <xsl:if test="$id != ''">
+ <xsl:attribute name="m:xref"><xsl:value-of select="$id"/></xsl:attribute>
+ </xsl:if>←</m:mo>
+ <xsl:apply-templates select="*[2]"/>
+ <m:mo stretchy="false">]</m:mo>
+ </xsl:when>
+ <!-- lift -->
+ <xsl:when test="$name='lift'">
+ <m:msup>
+ <m:mo mathcolor="green">
+ <xsl:if test="$id != ''">
+ <xsl:attribute name="m:xref"><xsl:value-of select="$id"/></xsl:attribute>
+ </xsl:if>↑</m:mo>
+ <xsl:apply-templates select="*[2]"/>
+ </m:msup>
+ <m:mrow>
+ <m:mo stretchy="false">(</m:mo>
+ <xsl:apply-templates select="*[3]"/>
+ <m:mo stretchy="false">)</m:mo>
+ </m:mrow>
+ </xsl:when>
+ <!-- lift_with_base -->
+ <xsl:when test="$name='lift_with_base'">
+ <m:msubsup>
+ <m:mo mathcolor="green">
+ <xsl:if test="$id != ''">
+ <xsl:attribute name="m:xref"><xsl:value-of select="$id"/></xsl:attribute>
+ </xsl:if>↑</m:mo>
+ <xsl:apply-templates select="*[3]"/>
+ <xsl:apply-templates select="*[4]"/>
+ </m:msubsup>
+ <m:mrow>
+ <m:mo stretchy="false">(</m:mo>
+ <xsl:apply-templates select="*[2]"/>
+ <m:mo stretchy="false">)</m:mo>
+ </m:mrow>
+ </xsl:when>
+ <!-- beta_red1 -->
+ <xsl:when test="$name='beta_red1'">
+ <xsl:apply-templates select="*[2]"/>
+ <m:munder>
+ <m:mo mathcolor="green">
+ <xsl:if test="$id != ''">
+ <xsl:attribute name="m:xref"><xsl:value-of select="$id"/></xsl:attribute>
+ </xsl:if>→</m:mo>
+ <m:mi mathcolor="green">β</m:mi>
+ </m:munder>
+ <xsl:apply-templates select="*[3]"/>
+ </xsl:when>
+ <!-- beta_red -->
+ <xsl:when test="$name='beta_red'">
+ <xsl:apply-templates select="*[2]"/>
+ <m:munderover>
+ <m:mo mathcolor="green">
+ <xsl:if test="$id != ''">
+ <xsl:attribute name="m:xref"><xsl:value-of select="$id"/></xsl:attribute>
+ </xsl:if>→</m:mo>
+ <m:mi mathcolor="green">β</m:mi>
+ <m:mi mathcolor="green">*</m:mi>
+ </m:munderover>
+ <xsl:apply-templates select="*[3]"/>
+ </xsl:when>
+ <!-- par_beta_red1 -->
+ <xsl:when test="$name='par_beta_red1'">
+ <xsl:apply-templates select="*[2]"/>
+ <m:munder>
+ <m:mo mathcolor="green">
+ <xsl:if test="$id != ''">
+ <xsl:attribute name="m:xref"><xsl:value-of select="$id"/></xsl:attribute>
+ </xsl:if>⇒</m:mo>
+ <m:mi mathcolor="green">β</m:mi>
+ </m:munder>
+ <xsl:apply-templates select="*[3]"/>
+ </xsl:when>
+ <!-- par_beta_red -->
+ <xsl:when test="$name='par_beta_red'">
+ <xsl:apply-templates select="*[2]"/>
+ <m:munderover>
+ <m:mo mathcolor="green">
+ <xsl:if test="$id != ''">
+ <xsl:attribute name="m:xref"><xsl:value-of select="$id"/></xsl:attribute>
+ </xsl:if>⇒</m:mo>
+ <m:mi mathcolor="green">β</m:mi>
+ <m:mi mathcolor="green">*</m:mi>
+ </m:munderover>
+ <xsl:apply-templates select="*[3]"/>
+ </xsl:when>
+ <!-- forgetful -->
+ <xsl:when test="$name='forgetful'">
+ <m:mfenced open="|" close="|">
+ <xsl:if test="$id != ''">
+ <xsl:attribute name="m:xref"><xsl:value-of select="$id"/></xsl:attribute>
+ </xsl:if>
+ <xsl:apply-templates select="*[2]"/>
+ </m:mfenced>
+ </xsl:when>
+ <!-- isomorphic -->
+ <xsl:when test="$name='isomorphic'">
+ <xsl:apply-templates select="*[2]"/>
+ <m:mo mathcolor="green">
+ <xsl:if test="$id != ''">
+ <xsl:attribute name="m:xref"><xsl:value-of select="$id"/></xsl:attribute>
+ </xsl:if>≅</m:mo>
+ <xsl:apply-templates select="*[3]"/>
+ </xsl:when>
+ <!-- interp -->
+ <xsl:when test="$name='forgetful'">
+ <m:mfenced open="[" close="]">
+ <xsl:if test="$id != ''">
+ <xsl:attribute name="m:xref"><xsl:value-of select="$id"/></xsl:attribute>
+ </xsl:if>
+ <xsl:apply-templates select="*[2]"/>
+ </m:mfenced>
+ </xsl:when>
+
<!-- ERROR -->
<xsl:otherwise>
<m:mi>ERROR</m:mi>
<xsl:template match="m:lambda">
<xsl:variable name="charlength"><xsl:apply-templates select="*[position()=1]" mode="charcount"/></xsl:variable>
- <m:mrow m:xref="{@id}">
+ <m:mrow>
+ <xsl:if test="@id">
+ <xsl:attribute name="m:xref">
+ <xsl:value-of select="@id"/>
+ </xsl:attribute>
+ </xsl:if>
<xsl:choose>
<xsl:when test="$charlength >= $framewidth">
<m:mtable align="baseline 1" equalrows="false" columnalign="left">
<xsl:choose>
<xsl:when test="$charlength >= $framewidth">
<m:mtable align="baseline 1" equalrows="false" columnalign="left">
- <xsl:if test="@helm:xref">
+ <xsl:if test="@id">
<xsl:attribute name="m:xref">
<xsl:value-of select="@id"/>
</xsl:attribute>
<m:mtd>
<m:mrow>
<m:mphantom><m:mtext>__</m:mtext></m:mphantom>
- <m:mo m:xref="{m:in/@id}">=</m:mo>
+ <m:mo>
+ <xsl:if test="m:in/@id">
+ <xsl:attribute name="m:xref">
+ <xsl:value-of select="m:in/@id"/>
+ </xsl:attribute>
+ </xsl:if>=</m:mo>
<xsl:apply-templates select="."/>
</m:mrow>
</m:mtd>
<xsl:choose>
<xsl:when test="$charlength >= $framewidth">
<m:mtable align="baseline 1" equalrows="false" columnalign="left">
- <xsl:if test="@helm:xref">
+ <xsl:if test="@id">
<xsl:attribute name="m:xref">
<xsl:value-of select="@id"/>
</xsl:attribute>
<m:mtd>
<m:mrow>
<m:mphantom><m:mtext>__</m:mtext></m:mphantom>
- <m:mo m:xref="{*[1]/@id}"><xsl:value-of select="$symbol"/></m:mo>
+ <m:mo>
+ <xsl:if test="*[1]/@id">
+ <xsl:attribute name="m:xref">
+ <xsl:value-of select="*[1]/@id"/>
+ </xsl:attribute>
+ </xsl:if><xsl:value-of select="$symbol"/></m:mo>
<xsl:apply-templates select="."/>
</m:mrow>
</m:mtd>
<xsl:template match = "m:set">
<xsl:choose>
<xsl:when test="count(child::*) = 0">
- <m:mi>∅</m:mi>
+ <m:mi>
+ <xsl:if test="@id">
+ <xsl:attribute name="m:xref">
+ <xsl:value-of select="@id"/>
+ </xsl:attribute>
+ </xsl:if>∅</m:mi>
</xsl:when>
<xsl:otherwise>
<xsl:variable name="charlength">
<m:mtr>
<m:mtd>
<m:mrow>
- <m:mo stretchy="false">{</m:mo>
+ <m:mo stretchy="false">
+ <xsl:if test="@id">
+ <xsl:attribute name="m:xref">
+ <xsl:value-of select="@id"/>
+ </xsl:attribute>
+ </xsl:if>{</m:mo>
<xsl:apply-templates select="*[position()=1]"/>
</m:mrow>
</m:mtd>
<m:mtr>
<m:mtd>
<m:mrow>
- <m:mo stretchy="false">}</m:mo>
+ <m:mo stretchy="false">
+ <xsl:if test="@id">
+ <xsl:attribute name="m:xref">
+ <xsl:value-of select="@id"/>
+ </xsl:attribute>
+ </xsl:if>}</m:mo>
</m:mrow>
</m:mtd>
</m:mtr>
<m:mtr>
<m:mtd>
<m:mrow>
- <m:mo stretchy="false">{</m:mo>
+ <m:mo stretchy="false">
+ <xsl:if test="@id">
+ <xsl:attribute name="m:xref">
+ <xsl:value-of select="@id"/>
+ </xsl:attribute>
+ </xsl:if>{</m:mo>
<xsl:apply-templates select="*[position()=1]"/>
<xsl:if test="position() != last()">
<mo>,</mo>
<m:mtr>
<m:mtd>
<m:mrow>
- <m:mo stretchy="false">}</m:mo>
+ <m:mo stretchy="false">
+ <xsl:if test="@id">
+ <xsl:attribute name="m:xref">
+ <xsl:value-of select="@id"/>
+ </xsl:attribute>
+ </xsl:if>}</m:mo>
</m:mrow>
</m:mtd>
</m:mtr>
</m:mfenced>
</xsl:template>
-<!-- *********************************** -->
-<!-- PROOF ELEMENTS -->
-<!-- *********************************** -->
-
-
<!--**********************-->
<!-- COUNTING -->