+<xsl:template mode="eq_transitive" match="*">
+ <!-- <m:ci>eccomi-1: <xsl:value-of select="name()"/></m:ci> -->
+ <xsl:choose>
+ <xsl:when test="name()='APPLY'">
+ <!-- <m:ci>eccomi-2: <xsl:value-of select="CONST[1]/@uri"/></m:ci> -->
+ <xsl:variable name="id" select="@id"/>
+ <xsl:choose>
+ <!-- ricordarsi di trattare il parametro -->
+ <xsl:when test="CONST[attribute::uri='cic:/Algebra/CSetoids/CSetoid_basics/eq_transitive_unfolded.con'] and count(child::*) = 7">
+ <!-- <m:ci>eccomi-3</m:ci> -->
+ <xsl:apply-templates mode="eq_transitive" select="*[6]"/>
+ <xsl:apply-templates mode="noannot" select="*[4]"/>
+ <xsl:apply-templates mode="eq_transitive" select="*[7]"/>
+ </xsl:when>
+ <xsl:otherwise>
+ <xsl:call-template name="generate_side_proof">
+ <xsl:with-param name="proof" select="."/>
+ <xsl:with-param name="show_statement" select="0"/>
+ </xsl:call-template>
+ </xsl:otherwise>
+ </xsl:choose>
+ </xsl:when>
+ <xsl:otherwise>
+ <xsl:call-template name="generate_side_proof">
+ <xsl:with-param name="proof" select="."/>
+ <xsl:with-param name="show_statement" select="0"/>
+ </xsl:call-template>
+ </xsl:otherwise>
+ </xsl:choose>
+</xsl:template>
+
+<xsl:template mode="diseq" match="*">
+ <xsl:param name="rel" select="'eq'"/>
+ <xsl:choose>
+ <xsl:when test="name()='APPLY'">
+ <xsl:variable name="id" select="@id"/>
+ <xsl:choose>
+ <!-- ricordarsi di trattare il parametro -->
+ <xsl:when test="CONST[attribute::uri='cic:/Algebra/COrdFields/Basic_Properties_of_leEq/leEq_transitive.con'] and count(child::*) = 7">
+ <xsl:apply-templates mode="diseq" select="*[6]">
+ <xsl:with-param name="rel" select="'leq'"/>
+ </xsl:apply-templates>
+ <xsl:apply-templates mode="noannot" select="*[4]"/>
+ <xsl:apply-templates mode="diseq" select="*[7]">
+ <xsl:with-param name="rel" select="'leq'"/>
+ </xsl:apply-templates>
+ </xsl:when>
+ <xsl:when test="CONST[attribute::uri='cic:/Algebra/COrdFields/Basic_Properties_of_leEq/leEq_wdl.con'] and count(child::*) = 7">
+ <m:eq/>
+ <!-- <m:ci><xsl:value-of select="'eq'"/></m:ci> -->
+ <xsl:call-template name="generate_side_proof">
+ <xsl:with-param name="proof" select="*[7]"/>
+ <xsl:with-param name="show_statement" select="0"/>
+ </xsl:call-template>
+ <xsl:apply-templates mode="noannot" select="*[3]"/>
+ <xsl:apply-templates mode="diseq" select="*[6]">
+ <xsl:with-param name="rel" select="'leq'"/>
+ </xsl:apply-templates>
+ </xsl:when>
+ <xsl:when test="CONST[attribute::uri='cic:/Algebra/COrdFields/Basic_Properties_of_leEq/leEq_less_trans.con'] and count(child::*) = 7">
+ <xsl:apply-templates mode="diseq" select="*[6]">
+ <xsl:with-param name="rel" select="'leq'"/>
+ </xsl:apply-templates>
+ <xsl:apply-templates mode="noannot" select="*[4]"/>
+ <xsl:apply-templates mode="diseq" select="*[7]">
+ <xsl:with-param name="rel" select="'lt'"/>
+ </xsl:apply-templates>
+ </xsl:when>
+ <xsl:when test="CONST[attribute::uri='cic:/Algebra/COrdFields/Basic_Properties_of_leEq/less_leEq_trans.con'] and count(child::*) = 7">
+ <xsl:apply-templates mode="diseq" select="*[6]">
+ <xsl:with-param name="rel" select="'lt'"/>
+ </xsl:apply-templates>
+ <xsl:apply-templates mode="noannot" select="*[4]"/>
+ <xsl:apply-templates mode="diseq" select="*[7]">
+ <xsl:with-param name="rel" select="'leq'"/>
+ </xsl:apply-templates>
+ </xsl:when>
+ <xsl:when test="CONST[attribute::uri='cic:/Algebra/COrdFields/Basic_Properties_of_leEq/leEq_wdr.con'] and count(child::*) = 7">
+ <xsl:apply-templates mode="diseq" select="*[6]">
+ <xsl:with-param name="rel" select="'leq'"/>
+ </xsl:apply-templates>
+ <xsl:apply-templates mode="noannot" select="*[4]"/>
+ <xsl:apply-templates mode="diseq" select="*[7]">
+ <xsl:with-param name="rel" select="'eq'"/>
+ </xsl:apply-templates>
+ </xsl:when>
+ <xsl:when test="CONST[attribute::uri='cic:/Algebra/COrdFields/COrdField_axioms/less_transitive_unfolded.con'] and count(child::*) = 7">
+ <xsl:apply-templates mode="diseq" select="*[6]">
+ <xsl:with-param name="rel" select="'lt'"/>
+ </xsl:apply-templates>
+ <xsl:apply-templates mode="noannot" select="*[4]"/>
+ <xsl:apply-templates mode="diseq" select="*[7]">
+ <xsl:with-param name="rel" select="'lt'"/>
+ </xsl:apply-templates>
+ </xsl:when>
+ <xsl:when test="CONST[attribute::uri='cic:/Algebra/COrdFields/COrdField_axioms/less_wdr.con'] and count(child::*) = 7">
+ <xsl:apply-templates mode="diseq" select="*[6]">
+ <xsl:with-param name="rel" select="'lt'"/>
+ </xsl:apply-templates>
+ <xsl:apply-templates mode="noannot" select="*[4]"/>
+ <xsl:apply-templates mode="diseq" select="*[7]">
+ <xsl:with-param name="rel" select="'eq'"/>
+ </xsl:apply-templates>
+ </xsl:when>
+ <xsl:when test="CONST[attribute::uri='cic:/Algebra/COrdFields/COrdField_axioms/less_wdl.con'] and count(child::*) = 7">
+ <m:eq/>
+ <!-- <m:ci><xsl:value-of select="'eq'"/></m:ci> -->
+ <xsl:call-template name="generate_side_proof">
+ <xsl:with-param name="proof" select="*[7]"/>
+ <xsl:with-param name="show_statement" select="0"/>
+ </xsl:call-template>
+ <xsl:apply-templates mode="noannot" select="*[3]"/>
+ <xsl:apply-templates mode="diseq" select="*[6]">
+ <xsl:with-param name="rel" select="'lt'"/>
+ </xsl:apply-templates>
+ </xsl:when>
+ <!--
+ <xsl:when test="CONST[attribute::uri='cic:/Algebra/CSetoids/CSetoid_basics/eq_transitive_unfolded.con'] and count(child::*) = 7">
+ <xsl:apply-templates mode="diseq" select="*[6]"/>
+ <m:eq/>
+ <xsl:apply-templates mode="noannot" select="*[4]"/>
+ <m:eq/>
+ <xsl:apply-templates mode="diseq" select="*[7]"/>
+ </xsl:when>
+ -->
+ <xsl:otherwise>
+ <xsl:element name="{concat('m:',$rel)}"/>
+ <!-- <m:ci><xsl:value-of select="$rel"/></m:ci> -->
+ <xsl:call-template name="generate_side_proof">
+ <xsl:with-param name="proof" select="."/>
+ <xsl:with-param name="show_statement" select="0"/>
+ </xsl:call-template>
+ </xsl:otherwise>
+ </xsl:choose>
+ </xsl:when>
+ <xsl:otherwise>
+ <xsl:element name="{concat('m:',$rel)}"/>
+ <!-- <m:ci><xsl:value-of select="$rel"/></m:ci> -->
+ <xsl:call-template name="generate_side_proof">
+ <xsl:with-param name="proof" select="."/>
+ <xsl:with-param name="show_statement" select="0"/>
+ </xsl:call-template>
+ </xsl:otherwise>
+ </xsl:choose>
+</xsl:template>