+ <!-- letin1 -->
+ <xsl:when test="$name='letin1'">
+ <xsl:text>letin1 (inline error)</xsl:text>
+ </xsl:when>
+ <!-- false_ind -->
+ <xsl:when test="$name='false_ind'">
+ <xsl:apply-templates mode="inline" select="*[3]"/>
+ <FONT color="red">Contradiction.</FONT>
+ </xsl:when>
+ <!-- and_ind -->
+ <xsl:when test="$name='and_ind'">
+ <FONT color="red">From </FONT>
+ <xsl:apply-templates select="*[2]"/>
+ <FONT color="red"> we get</FONT>
+ (
+ <xsl:apply-templates select="*[3]"/>
+ ) 
+ <xsl:apply-templates mode="inline" select="*[4]"/>
+ <FONT color="red"> and </FONT>
+ (
+ <xsl:apply-templates select="*[5]"/>
+ ) 
+ <xsl:apply-templates mode="inline" select="*[6]"/>
+ ;
+ <FONT color="red"> hence </FONT>
+ <xsl:apply-templates mode="inline" select="*[7]"/>
+ </xsl:when>
+
+ <xsl:when test="$name='subst'">
+ <xsl:apply-templates select="*[3]" mode="inline"/>
+ <xsl:text>[</xsl:text>
+ <xsl:apply-templates select="*[4]" mode="inline"/>
+ <xsl:choose>
+ <xsl:when test="$uri != ''">
+ <a href="{$uri}">
+ <xsl:call-template name="mksymbol-1">
+ <xsl:with-param name="symbol" select="$name"/>
+ <xsl:with-param name="color" select="'green'"/>
+ <xsl:with-param name="size" select="'+0'"/>
+ </xsl:call-template>
+ </a>
+ </xsl:when>
+ <xsl:otherwise>
+ <xsl:call-template name="mksymbol-1">
+ <xsl:with-param name="symbol" select="$name"/>
+ <xsl:with-param name="color" select="'green'"/>
+ <xsl:with-param name="size" select="'+0'"/>
+ </xsl:call-template>
+ </xsl:otherwise>
+ </xsl:choose>
+ <xsl:apply-templates select="*[2]" mode="inline"/>
+ <xsl:text>]</xsl:text>
+ </xsl:when>
+
+ <xsl:when test="$name='lift_with_base'">
+ <SUB>
+ <xsl:apply-templates select="*[3]" mode="inline"/>
+ </SUB>
+ <xsl:choose>
+ <xsl:when test="$uri != ''">
+ <a href="{$uri}">
+ <xsl:call-template name="mksymbol-1">
+ <xsl:with-param name="symbol" select="$name"/>
+ <xsl:with-param name="color" select="'green'"/>
+ <xsl:with-param name="size" select="'+0'"/>
+ </xsl:call-template>
+ </a>
+ </xsl:when>
+ <xsl:otherwise>
+ <xsl:call-template name="mksymbol-1">
+ <xsl:with-param name="symbol" select="$name"/>
+ <xsl:with-param name="color" select="'green'"/>
+ <xsl:with-param name="size" select="'+0'"/>
+ </xsl:call-template>
+ </xsl:otherwise>
+ </xsl:choose>
+ <SUP>
+ <xsl:apply-templates select="*[4]" mode="inline"/>
+ </SUP>
+ <xsl:text>(</xsl:text>
+ <xsl:apply-templates select="*[2]" mode="inline"/>
+ <xsl:text>)</xsl:text>
+ </xsl:when>
+
+ <xsl:when test="$name='lift'">
+ <xsl:choose>
+ <xsl:when test="$uri != ''">
+ <a href="{$uri}">
+ <xsl:call-template name="mksymbol-1">
+ <xsl:with-param name="symbol" select="$name"/>
+ <xsl:with-param name="color" select="'green'"/>
+ <xsl:with-param name="size" select="'+0'"/>
+ </xsl:call-template>
+ </a>
+ </xsl:when>
+ <xsl:otherwise>
+ <xsl:call-template name="mksymbol-1">
+ <xsl:with-param name="symbol" select="$name"/>
+ <xsl:with-param name="color" select="'green'"/>
+ <xsl:with-param name="size" select="'+0'"/>
+ </xsl:call-template>
+ </xsl:otherwise>
+ </xsl:choose>
+ <SUP>
+ <xsl:apply-templates select="*[2]" mode="inline"/>
+ </SUP>
+ <xsl:text>(</xsl:text>
+ <xsl:apply-templates select="*[3]" mode="inline"/>
+ <xsl:text>)</xsl:text>
+ </xsl:when>
+
+ <!-- reduction -->
+ <xsl:when test="$name='beta_red1'">
+ <xsl:apply-templates select="*[2]" mode="inline"/>
+ <xsl:choose>
+ <xsl:when test="$uri != ''">
+ <a href="{$uri}">
+ <xsl:call-template name="mksymbol-1">
+ <xsl:with-param name="symbol" select="$name"/>
+ <xsl:with-param name="color" select="'green'"/>
+ <xsl:with-param name="size" select="'+0'"/>
+ </xsl:call-template>
+ <SUB>
+ <xsl:call-template name="mksymbol-1">
+ <xsl:with-param name="symbol" select="'beta'"/>
+ <xsl:with-param name="color" select="'green'"/>
+ <xsl:with-param name="size" select="'+0'"/>
+ </xsl:call-template>
+ </SUB>
+ </a>
+ </xsl:when>
+ <xsl:otherwise>
+ <xsl:call-template name="mksymbol-1">
+ <xsl:with-param name="symbol" select="$name"/>
+ <xsl:with-param name="color" select="'green'"/>
+ <xsl:with-param name="size" select="'+0'"/>
+ </xsl:call-template>
+ <SUB>
+ <xsl:call-template name="mksymbol-1">
+ <xsl:with-param name="symbol" select="'beta'"/>
+ <xsl:with-param name="color" select="'green'"/>
+ <xsl:with-param name="size" select="'+0'"/>
+ </xsl:call-template>
+ </SUB>
+ </xsl:otherwise>
+ </xsl:choose>
+ <xsl:apply-templates select="*[3]" mode="inline"/>
+ </xsl:when>
+
+ <xsl:when test="$name='beta_red'">
+ <xsl:apply-templates select="*[2]" mode="inline"/>
+ <xsl:choose>
+ <xsl:when test="$uri != ''">
+ <a href="{$uri}">
+ <xsl:call-template name="mksymbol-1">
+ <xsl:with-param name="symbol" select="$name"/>
+ <xsl:with-param name="color" select="'green'"/>
+ <xsl:with-param name="size" select="'+0'"/>
+ </xsl:call-template>
+ <SUB>
+ <xsl:call-template name="mksymbol-1">
+ <xsl:with-param name="symbol" select="'beta'"/>
+ <xsl:with-param name="color" select="'green'"/>
+ <xsl:with-param name="size" select="'+0'"/>
+ </xsl:call-template>
+ <xsl:text>*</xsl:text>
+ </SUB>
+ </a>
+ </xsl:when>
+ <xsl:otherwise>
+ <xsl:call-template name="mksymbol-1">
+ <xsl:with-param name="symbol" select="$name"/>
+ <xsl:with-param name="color" select="'green'"/>
+ <xsl:with-param name="size" select="'+0'"/>
+ </xsl:call-template>
+ <SUB>
+ <xsl:call-template name="mksymbol-1">
+ <xsl:with-param name="symbol" select="'beta'"/>
+ <xsl:with-param name="color" select="'green'"/>
+ <xsl:with-param name="size" select="'+0'"/>
+ </xsl:call-template>
+ <xsl:text>*</xsl:text>
+ </SUB>
+ </xsl:otherwise>
+ </xsl:choose>
+ <xsl:apply-templates select="*[3]" mode="inline"/>
+ </xsl:when>
+
+ <xsl:when test="$name='par_beta_red1'">
+ <xsl:apply-templates select="*[2]" mode="inline"/>
+ <xsl:choose>
+ <xsl:when test="$uri != ''">
+ <a href="{$uri}">
+ <xsl:call-template name="mksymbol-1">
+ <xsl:with-param name="symbol" select="$name"/>
+ <xsl:with-param name="color" select="'green'"/>
+ <xsl:with-param name="size" select="'+0'"/>
+ </xsl:call-template>
+ <SUB>
+ <xsl:call-template name="mksymbol-1">
+ <xsl:with-param name="symbol" select="'beta'"/>
+ <xsl:with-param name="color" select="'green'"/>
+ <xsl:with-param name="size" select="'+0'"/>
+ </xsl:call-template>
+ </SUB>
+ </a>
+ </xsl:when>
+ <xsl:otherwise>
+ <xsl:call-template name="mksymbol-1">
+ <xsl:with-param name="symbol" select="$name"/>
+ <xsl:with-param name="color" select="'green'"/>
+ <xsl:with-param name="size" select="'+0'"/>
+ </xsl:call-template>
+ <SUB>
+ <xsl:call-template name="mksymbol-1">
+ <xsl:with-param name="symbol" select="'beta'"/>
+ <xsl:with-param name="color" select="'green'"/>
+ <xsl:with-param name="size" select="'+0'"/>
+ </xsl:call-template>
+ </SUB>
+ </xsl:otherwise>
+ </xsl:choose>
+ <xsl:apply-templates select="*[3]" mode="inline"/>
+ </xsl:when>
+
+ <xsl:when test="$name='par_beta_red'">
+ <xsl:apply-templates select="*[2]" mode="inline"/>
+ <xsl:choose>
+ <xsl:when test="$uri != ''">
+ <a href="{$uri}">
+ <xsl:call-template name="mksymbol-1">
+ <xsl:with-param name="symbol" select="$name"/>
+ <xsl:with-param name="color" select="'green'"/>
+ <xsl:with-param name="size" select="'+0'"/>
+ </xsl:call-template>
+ <SUB>
+ <xsl:call-template name="mksymbol-1">
+ <xsl:with-param name="symbol" select="'beta'"/>
+ <xsl:with-param name="color" select="'green'"/>
+ <xsl:with-param name="size" select="'+0'"/>
+ </xsl:call-template>
+ <xsl:text>*</xsl:text>
+ </SUB>
+ </a>
+ </xsl:when>
+ <xsl:otherwise>
+ <xsl:call-template name="mksymbol-1">
+ <xsl:with-param name="symbol" select="$name"/>
+ <xsl:with-param name="color" select="'green'"/>
+ <xsl:with-param name="size" select="'+0'"/>
+ </xsl:call-template>
+ <SUB>
+ <xsl:call-template name="mksymbol-1">
+ <xsl:with-param name="symbol" select="'beta'"/>
+ <xsl:with-param name="color" select="'green'"/>
+ <xsl:with-param name="size" select="'+0'"/>
+ </xsl:call-template>
+ <xsl:text>*</xsl:text>
+ </SUB>
+ </xsl:otherwise>
+ </xsl:choose>
+ <xsl:apply-templates select="*[3]" mode="inline"/>
+ </xsl:when>
+
+ <!-- forgetful -->
+ <xsl:when test="$name='forgetful'">
+ <xsl:choose>
+ <xsl:when test="$uri != ''">
+ <a href="{$uri}">|</a>
+ </xsl:when>
+ <xsl:otherwise>
+ |
+ </xsl:otherwise>
+ </xsl:choose>
+ <xsl:apply-templates select="*[2]" mode="inline"/>
+ <xsl:choose>
+ <xsl:when test="$uri != ''">
+ <a href="{$uri}">|</a>
+ </xsl:when>
+ <xsl:otherwise>
+ |
+ </xsl:otherwise>
+ </xsl:choose>
+ </xsl:when>
+
+ <!-- boolean algebra of redexes -->
+
+ <!-- isomorphic -->
+ <xsl:when test="$name='isomorphic'">
+ <xsl:apply-templates select="*[2]" mode="inline"/>
+ <xsl:choose>
+ <xsl:when test="$uri != ''">
+ <a href="{$uri}">
+ <xsl:call-template name="mksymbol-1">
+ <xsl:with-param name="symbol" select="$name"/>
+ <xsl:with-param name="color" select="'green'"/>
+ <xsl:with-param name="size" select="'+0'"/>
+ </xsl:call-template>
+ </a>
+ </xsl:when>
+ <xsl:otherwise>
+ <xsl:call-template name="mksymbol-1">
+ <xsl:with-param name="symbol" select="$name"/>
+ <xsl:with-param name="color" select="'green'"/>
+ <xsl:with-param name="size" select="'+0'"/>
+ </xsl:call-template>
+ </xsl:otherwise>
+ </xsl:choose>
+ <xsl:apply-templates select="*[3]" mode="inline"/>
+ </xsl:when>
+
+ <!-- INTERP -->
+ <xsl:when test="$name='interp'">
+ <font color="green">[</font>
+ <xsl:apply-templates select="*[2]"/>
+ <font color="green">]</font>
+ </xsl:when>
+