+ <!-- ***************************************** -->
+ <!-- *********** PROOF ELEMENTS ************** -->
+ <!-- ***************************************** -->
+ <!-- PROOF -->
+ <xsl:when test="$name='proof'">
+ <xsl:apply-templates select="*[position()=2]">
+ <xsl:with-param name="current_indent" select="$current_indent"/>
+ </xsl:apply-templates>
+ <br/>
+ <!-- <xsl:element name="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>
+ </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'">
+ <m:mtext>(</m:mtext>
+ <xsl:apply-templates select="m:ci"/>
+ <m:mtext>) </m:mtext>
+ <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>
+ <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 select="*[3]"/>
+ <FONT color="red"> with </FONT>
+ <xsl:apply-templates select="*[4]"/>
+ <FONT color="red"> by </FONT>
+ <xsl:apply-templates select="*[5]"/>
+ </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>
+ <!-- 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>
+ <m:mtext>(</m:mtext>
+ <xsl:apply-templates select="*[3]"/>
+ <m:mtext>) </m:mtext>
+ <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>
+ <m:mtext>(</m:mtext>
+ <xsl:apply-templates select="*[5]"/>
+ <m:mtext>) </m:mtext>
+ <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>
+ <!-- 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>
+ <m:mtext>*</m:mtext>
+ <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>
+ <m:mtext>*</m:mtext>
+ <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]"/>
+ <m:mtext>:</m:mtext>
+ <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>
+ <m:mtext>(</m:mtext>
+ <xsl:apply-templates mode="inline" select="*[5]"/>
+ <m:mtext>)</m:mtext>
+ <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>
+ </xsl:choose>