<xsl:for-each select="Conjecture">
<m:mtr>
<m:mtd>
- <m:mrow>
+ <m:mrow helm:xref="{@helm:xref}">
<m:mphantom><m:mtext>__</m:mtext></m:mphantom>
- <m:mtext><xsl:value-of select="./@no"/>:</m:mtext>
- <xsl:apply-templates select="./*[1]"/>
+ <xsl:for-each select="Decl|Def|Hidden">
+ <xsl:choose>
+ <xsl:when test="name(.)='Decl'">
+ <m:mrow helm:xref="{@helm:xref}">
+ <xsl:choose>
+ <xsl:when test="@name">
+ <m:mi><xsl:value-of select="@name"/></m:mi>
+ </xsl:when>
+ <xsl:otherwise>
+ <m:mi>_</m:mi>
+ </xsl:otherwise>
+ </xsl:choose>
+ <m:mo>:</m:mo>
+ <xsl:apply-templates select="./*[1]"/>
+ </m:mrow>
+ </xsl:when>
+ <xsl:when test="name(.)='Def'">
+ <m:mrow helm:xref="{@helm:xref}">
+ <xsl:choose>
+ <xsl:when test="@name">
+ <m:mi><xsl:value-of select="@name"/></m:mi>
+ </xsl:when>
+ <xsl:otherwise>
+ <m:mi>_</m:mi>
+ </xsl:otherwise>
+ </xsl:choose>
+ <m:mo>:=</m:mo>
+ <xsl:apply-templates select="./*[1]"/>
+ </m:mrow>
+ </xsl:when>
+ <xsl:otherwise>
+ <m:mrow helm:xref="{@helm:xref}">
+ <m:mi>_</m:mi>
+ <m:mo>:?</m:mo>
+ <m:mi>_</m:mi>
+ </m:mrow>
+ </xsl:otherwise>
+ </xsl:choose>
+ <xsl:if test="not (position() = last())">
+ <m:mo>;</m:mo>
+ </xsl:if>
+ </xsl:for-each>
+ <m:mo>|-</m:mo>
+ <m:msub><m:mi>?</m:mi><m:mn><xsl:value-of select="@no"/></m:mn></m:msub>
+ <m:mo>:</m:mo>
+ <xsl:apply-templates select="./Goal/*[1]"/>
</m:mrow>
</m:mtd>
</m:mtr>
<m:mtr>
<m:mtd>
<m:mrow>
- <m:mtext>CORRESPONDING PROOF:</m:mtext>
+ <m:mtext>PROOF:</m:mtext>
</m:mrow>
</m:mtd>
</m:mtr>
</m:math>
</xsl:template>
+<!-- SEQUENT -->
+
+<xsl:template match="Sequent">
+ <xsl:variable name="rowlines">
+ <xsl:for-each select="Decl|Def">
+ <xsl:if test="position() != last()">
+ <xsl:text>none </xsl:text>
+ </xsl:if>
+ </xsl:for-each>
+ <xsl:text>solid</xsl:text>
+ </xsl:variable>
+ <xsl:variable name="no" select="@no"/>
+ <m:math>
+ <m:mi><xsl:text>?</xsl:text><xsl:value-of select="$no"/></m:mi>
+ <m:mo>:</m:mo>
+ <m:mphantom><m:mtext>_</m:mtext></m:mphantom>
+ <m:mtable align="baseline 1" equalrows="false" columnalign="left" helm:xref="{@helm:xref}" rowlines="{$rowlines}">
+ <xsl:for-each select="Decl|Def">
+ <m:mtr>
+ <m:mtd>
+ <m:mrow helm:xref="{@helm:xref}">
+ <m:mi><xsl:value-of select="@name"/></m:mi>
+ <xsl:choose>
+ <xsl:when test="name(.) = 'Decl'">
+ <m:mo>:</m:mo>
+ </xsl:when>
+ <xsl:otherwise>
+ <m:mo>:=</m:mo>
+ </xsl:otherwise>
+ </xsl:choose>
+ <xsl:apply-templates select="*[1]"/>
+ </m:mrow>
+ </m:mtd>
+ </m:mtr>
+ </xsl:for-each>
+ <xsl:if test="not(Decl|Def)">
+ <m:mtr>
+ <m:mtd>
+ <m:mrow>
+ <m:mphantom><m:mtext>_</m:mtext></m:mphantom>
+ </m:mrow>
+ </m:mtd>
+ </m:mtr>
+ </xsl:if>
+ <m:mtr>
+ <m:mtd>
+ <m:mrow>
+ <xsl:apply-templates select="Goal/*[1]"/>
+ </m:mrow>
+ </m:mtd>
+ </m:mtr>
+ </m:mtable>
+ </m:math>
+</xsl:template>
+
<!--**********************-->
<!-- TERMS -->
<!--**********************-->
<xsl:variable name="charlength"><xsl:apply-templates select="m:csymbol" mode="charcount"/></xsl:variable>
<m:mrow>
<xsl:if test="@id">
- <xsl:attribute name="m:xref"><xsl:value-of select="@id"/></xsl:attribute>
+ <xsl:attribute name="xref"><xsl:value-of select="@id"/></xsl:attribute>
</xsl:if>
<xsl:variable name="id" select="m:csymbol/@id"/>
<xsl:choose>
+ <!-- META -->
+ <xsl:when test="$name='meta'">
+ <m:mrow>
+ <xsl:apply-templates select="*[position()=2]"/>
+ <m:mfenced open="[" close="]" separators=";">
+ <xsl:apply-templates select="*[position()>2]"/>
+ </m:mfenced>
+ </m:mrow>
+ </xsl:when>
<!-- FORALL -->
<xsl:when test="$name='forall'">
<xsl:choose>
<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:attribute name="xref"><xsl:value-of select="$id"/></xsl:attribute>
</xsl:if>←</m:mo>
<xsl:apply-templates select="*[2]"/>
<m:mo stretchy="false">]</m:mo>
<m:msup>
<m:mo mathcolor="Green">
<xsl:if test="$id != ''">
- <xsl:attribute name="m:xref"><xsl:value-of select="$id"/></xsl:attribute>
+ <xsl:attribute name="xref"><xsl:value-of select="$id"/></xsl:attribute>
</xsl:if>↑</m:mo>
<xsl:apply-templates select="*[2]"/>
</m:msup>
<m:msubsup>
<m:mo mathcolor="Green">
<xsl:if test="$id != ''">
- <xsl:attribute name="m:xref"><xsl:value-of select="$id"/></xsl:attribute>
+ <xsl:attribute name="xref"><xsl:value-of select="$id"/></xsl:attribute>
</xsl:if>↑</m:mo>
<xsl:apply-templates select="*[3]"/>
<xsl:apply-templates select="*[4]"/>
<m:munder>
<m:mo mathcolor="Green">
<xsl:if test="$id != ''">
- <xsl:attribute name="m:xref"><xsl:value-of select="$id"/></xsl:attribute>
+ <xsl:attribute name="xref"><xsl:value-of select="$id"/></xsl:attribute>
</xsl:if>→</m:mo>
<m:mi mathcolor="Green">β</m:mi>
</m:munder>
<m:munderover>
<m:mo mathcolor="Green">
<xsl:if test="$id != ''">
- <xsl:attribute name="m:xref"><xsl:value-of select="$id"/></xsl:attribute>
+ <xsl:attribute name="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:munder>
<m:mo mathcolor="Green">
<xsl:if test="$id != ''">
- <xsl:attribute name="m:xref"><xsl:value-of select="$id"/></xsl:attribute>
+ <xsl:attribute name="xref"><xsl:value-of select="$id"/></xsl:attribute>
</xsl:if>⇒</m:mo>
<m:mi mathcolor="Green">β</m:mi>
</m:munder>
<m:munderover>
<m:mo mathcolor="Green">
<xsl:if test="$id != ''">
- <xsl:attribute name="m:xref"><xsl:value-of select="$id"/></xsl:attribute>
+ <xsl:attribute name="xref"><xsl:value-of select="$id"/></xsl:attribute>
</xsl:if>⇒</m:mo>
<m:mi mathcolor="Green">β</m:mi>
<m:mi mathcolor="Green">*</m:mi>
<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:attribute name="xref"><xsl:value-of select="$id"/></xsl:attribute>
</xsl:if>
<xsl:apply-templates select="*[2]"/>
</m:mfenced>
<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:attribute name="xref"><xsl:value-of select="$id"/></xsl:attribute>
</xsl:if>≅</m:mo>
<xsl:apply-templates select="*[3]"/>
</xsl:when>
<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:attribute name="xref"><xsl:value-of select="$id"/></xsl:attribute>
</xsl:if>
<xsl:apply-templates select="*[2]"/>
</m:mfenced>
<xsl:variable name="charlength"><xsl:apply-templates select="*[position()=1]" mode="charcount"/></xsl:variable>
<m:mrow>
<xsl:if test="@id">
- <xsl:attribute name="m:xref">
+ <xsl:attribute name="xref">
<xsl:value-of select="@id"/>
</xsl:attribute>
</xsl:if>