+ <!-- Algebra equality (eq_transitive_unfolded) -->
+ <!-- It requires a special mode "eq_transitive"-->
+ <!-- togliere il parametro -->
+ <xsl:when test="CONST[attribute::uri='cic:/Algebra/CSetoids/CSetoid_basics/eq_transitive_unfolded.con'] and count(child::*) = 7">
+ <m:apply>
+ <m:csymbol>eq_chain</m:csymbol>
+ <xsl:apply-templates mode="noannot" select="*[3]"/>
+ <xsl:apply-templates mode="eq_transitive" select="*[6]"/>
+ <xsl:apply-templates mode="noannot" select="*[4]"/>
+ <xsl:apply-templates mode="eq_transitive" select="*[7]"/>
+ <xsl:apply-templates mode="noannot" select="*[5]"/>
+ </m:apply>
+ </xsl:when>
+ <!-- Algebra disequalities -->
+ <!-- It requires a special mode "diseq"-->
+ <!-- togliere il parametro -->
+ <xsl:when test="CONST[attribute::uri='cic:/Algebra/COrdFields/Basic_Properties_of_leEq/leEq_transitive.con'] and count(child::*) = 7">
+ <m:apply>
+ <m:csymbol>diseq_chain</m:csymbol>
+ <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:apply-templates mode="noannot" select="*[4]"/>
+ <xsl:apply-templates mode="diseq" select="*[7]">
+ <xsl:with-param name="rel" select="'leq'"/>
+ </xsl:apply-templates>
+ <xsl:apply-templates mode="noannot" select="*[5]"/>
+ </m:apply>
+ </xsl:when>
+ <xsl:when test="CONST[attribute::uri='cic:/Algebra/COrdFields/Basic_Properties_of_leEq/leEq_wdl.con'] and count(child::*) = 7">
+ <m:apply>
+ <m:csymbol>diseq_chain</m:csymbol>
+ <xsl:apply-templates mode="noannot" select="*[5]"/>
+ <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:apply-templates mode="noannot" select="*[4]"/>
+ </m:apply>
+ </xsl:when>
+ <xsl:when test="CONST[attribute::uri='cic:/Algebra/COrdFields/Basic_Properties_of_leEq/leEq_less_trans.con'] and count(child::*) = 7">
+ <m:apply>
+ <m:csymbol>diseq_chain</m:csymbol>
+ <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:apply-templates mode="noannot" select="*[4]"/>
+ <xsl:apply-templates mode="diseq" select="*[7]">
+ <xsl:with-param name="rel" select="'lt'"/>
+ </xsl:apply-templates>
+ <xsl:apply-templates mode="noannot" select="*[5]"/>
+ </m:apply>
+ </xsl:when>
+ <xsl:when test="CONST[attribute::uri='cic:/Algebra/COrdFields/Basic_Properties_of_leEq/less_leEq_trans.con'] and count(child::*) = 7">
+ <m:apply>
+ <m:csymbol>diseq_chain</m:csymbol>
+ <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:apply-templates mode="noannot" select="*[4]"/>
+ <xsl:apply-templates mode="diseq" select="*[7]">
+ <xsl:with-param name="rel" select="'leq'"/>
+ </xsl:apply-templates>
+ <xsl:apply-templates mode="noannot" select="*[5]"/>
+ </m:apply>
+ </xsl:when>
+ <xsl:when test="CONST[attribute::uri='cic:/Algebra/COrdFields/Basic_Properties_of_leEq/leEq_wdr.con'] and count(child::*) = 7">
+ <m:apply>
+ <m:csymbol>diseq_chain</m:csymbol>
+ <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:apply-templates mode="noannot" select="*[4]"/>
+ <xsl:apply-templates mode="diseq" select="*[7]">
+ <xsl:with-param name="rel" select="'eq'"/>
+ </xsl:apply-templates>
+ <xsl:apply-templates mode="noannot" select="*[5]"/>
+ </m:apply>
+ </xsl:when>
+ <xsl:when test="CONST[attribute::uri='cic:/Algebra/COrdFields/COrdField_axioms/less_transitive_unfolded.con'] and count(child::*) = 7">
+ <m:apply>
+ <m:csymbol>diseq_chain</m:csymbol>
+ <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:apply-templates mode="noannot" select="*[4]"/>
+ <xsl:apply-templates mode="diseq" select="*[7]">
+ <xsl:with-param name="rel" select="'lt'"/>
+ </xsl:apply-templates>
+ <xsl:apply-templates mode="noannot" select="*[5]"/>
+ </m:apply>
+ </xsl:when>
+ <!-- togliere il parametro -->
+ <xsl:when test="CONST[attribute::uri='cic:/Algebra/COrdFields/COrdField_axioms/less_wdr.con'] and count(child::*) = 7">
+ <m:apply>
+ <m:csymbol>diseq_chain</m:csymbol>
+ <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:apply-templates mode="noannot" select="*[4]"/>
+ <xsl:apply-templates mode="diseq" select="*[7]">
+ <xsl:with-param name="rel" select="'eq'"/>
+ </xsl:apply-templates>
+ <xsl:apply-templates mode="noannot" select="*[5]"/>
+ </m:apply>
+ </xsl:when>
+ <!-- togliere il parametro -->
+ <xsl:when test="CONST[attribute::uri='cic:/Algebra/COrdFields/COrdField_axioms/less_wdl.con'] and count(child::*) = 7">
+ <m:apply>
+ <m:csymbol>diseq_chain</m:csymbol>
+ <xsl:apply-templates mode="noannot" select="*[5]"/>
+ <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:apply-templates mode="noannot" select="*[4]"/>
+ </m:apply>
+ </xsl:when>