- <!-- nat_ind -->
- <xsl:when test="$name='nat_ind_complete'">
- <FONT color="red">By induction on </FONT>
- <xsl:apply-templates select="*[2]"/>:
- <br/>
- <xsl:call-template name="make_indent">
- <xsl:with-param name="current_indent" select="$current_indent"/>
- </xsl:call-template>
- <xsl:text>0 </xsl:text>
- <FONT FACE="Symbol" mathcolor="green">Þ</FONT>
- <xsl:apply-templates select="*[3]">
- <xsl:with-param name="current_indent" select="$current_indent + 8"/>
- </xsl:apply-templates>
- <br/>
- <xsl:call-template name="make_indent">
- <xsl:with-param name="current_indent" select="$current_indent"/>
- </xsl:call-template>
- <xsl:text>S(</xsl:text>
- <xsl:apply-templates select="*[4]"/>
- <xsl:text>) </xsl:text>
- <FONT FACE="Symbol" mathcolor="green">Þ</FONT>
- <FONT color="red">Assume by induction</FONT>
- <br/>
- <xsl:call-template name="make_indent">
- <xsl:with-param name="current_indent" select="$current_indent +10"/>
- </xsl:call-template>
- <xsl:text>(</xsl:text>
- <xsl:apply-templates select="*[5]"/>
- <xsl:text>)</xsl:text>
- <xsl:apply-templates select="*[6]">
- <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 +10"/>
- </xsl:call-template>
- <xsl:apply-templates select="*[7]">
- <xsl:with-param name="current_indent" select="$current_indent + 10"/>
- </xsl:apply-templates>
- </xsl:when>