+++ /dev/null
-<xsl:stylesheet version="1.0" xmlns:xsl="http://www.w3.org/1999/XSL/Transform"
- xmlns:m="http://www.w3.org/1998/Math/MathML"
- xmlns:cn="http://www.......">
-
-<xsl:template match="level-expression">
- <m:apply>
- <m:ci>level-exp</m:ci>
- <m:ci>
- <xsl:value-of select="@level"/>
- </m:ci>
- </m:apply>
-</xsl:template>
-
-<xsl:template match="parameter-substitution-list">
- <m:apply>
- <m:ci>parameter-substitution-list</m:ci>
- <m:ci>
- <xsl:value-of select="@val"/>
- </m:ci>
- </m:apply>
-</xsl:template>
-
-
-<xsl:template match="tag">
- <m:apply>
- <m:ci>tag <xsl:value-of select="@step"/>:</m:ci>
- <xsl:apply-templates/>
- </m:apply>
-</xsl:template>
-
-<xsl:template match="dependent_functionFormation">
- <m:apply>
- <m:ci>dependent_functionFormation</m:ci>
- <xsl:apply-templates/>
- </m:apply>
-</xsl:template>
-
-<xsl:template match="independent_functionFormation">
- <m:ci>independent_functionFormation</m:ci>
-</xsl:template>
-
-<xsl:template match="functionEquality">
- <m:apply>
- <m:ci>functionEquality</m:ci>
- <xsl:apply-templates/>
- </m:apply>
-</xsl:template>
-
-<xsl:template match="independent_functionEquality">
- <m:ci>independent_functionEquality</m:ci>
-</xsl:template>
-
-<xsl:template match="lambdaEquality">
- <m:apply>
- <m:ci>lambdaEquality</m:ci>
- <xsl:apply-templates/>
- </m:apply>
-</xsl:template>
-
-<xsl:template match="lambdaFormation">
- <m:apply>
- <m:ci>lambdaFormation</m:ci>
- <xsl:apply-templates/>
- </m:apply>
-</xsl:template>
-
-<xsl:template match="applyEquality">
- <m:apply>
- <m:ci>applyEquality</m:ci>
- <xsl:apply-templates/>
- </m:apply>
-</xsl:template>
-
-<xsl:template match="independent_functionElimination">
- <m:apply>
- <m:ci>independent_functionElimination</m:ci>
- <m:cn>
- <xsl:value-of select="@number_hyp"/>
- </m:cn>
- <xsl:apply-templates/>
- </m:apply>
-</xsl:template>
-
-<xsl:template match="dependent_functionElimination">
- <m:apply>
- <m:ci>dependent_functionElimination</m:ci>
- <m:cn>
- <xsl:value-of select="@number_hyp"/>
- </m:cn>
- <xsl:apply-templates/>
- </m:apply>
-</xsl:template>
-
-<xsl:template match="applyReduce">
- <m:ci>functionEquality</m:ci>
-</xsl:template>
-
-<xsl:template match="functionExtensionality">
- <m:apply>
- <m:ci>functionExtensionality</m:ci>
- <xsl:apply-templates/>
- </m:apply>
-</xsl:template>
-
-<xsl:template match="dependent_productFormation">
- <m:apply>
- <m:ci>dependent_productFormation</m:ci>
- <xsl:apply-templates/>
- </m:apply>
-</xsl:template>
-
-<xsl:template match="independent_productFormation">
- <m:ci>independent_productFormation</m:ci>
-</xsl:template>
-
-<xsl:template match="productEquality">
- <m:apply>
- <m:ci>productEquality</m:ci>
- <xsl:apply-templates/>
- </m:apply>
-</xsl:template>
-
-<xsl:template match="independent_productEquality">
- <m:ci>independent_productEquality</m:ci>
-</xsl:template>
-
-<xsl:template match="dependent_pairEquality">
- <m:apply>
- <m:ci>dependent_pairEquality</m:ci>
- <xsl:apply-templates/>
- </m:apply>
-</xsl:template>
-
-<xsl:template match="dependent_pairFormation">
- <m:apply>
- <m:ci>dependent_pairFormation</m:ci>
- <xsl:apply-templates/>
- </m:apply>
-</xsl:template>
-
-<xsl:template match="independent_pairEquality">
- <m:ci>independent_pairEquality</m:ci>
-</xsl:template>
-
-<xsl:template match="independent_pairFormation">
- <m:ci>independent_pairFormation</m:ci>
-</xsl:template>
-
-<xsl:template match="spreadEquality">
- <m:apply>
- <m:ci>spreadEquality</m:ci>
- <m:cn>
- <xsl:value-of select="@number_hyp"/>
- </m:cn>
- <xsl:apply-templates/>
- </m:apply>
-</xsl:template>
-
-<xsl:template match="productElimination">
- <m:apply>
- <m:ci>productElimination</m:ci>
- <xsl:apply-templates/>
- </m:apply>
-</xsl:template>
-
-<xsl:template match="spreadReduce">
- <m:ci>spreadReduce</m:ci>
-</xsl:template>
-
-<xsl:template match="unionFormation">
- <m:ci>unionFormation</m:ci>
-</xsl:template>
-
-<xsl:template match="unionEquality">
- <m:ci>unionEquality</m:ci>
-</xsl:template>
-
-<xsl:template match="inlEquality">
- <m:apply>
- <m:ci>inlEquality</m:ci>
- <xsl:apply-templates/>
- </m:apply>
-</xsl:template>
-
-<xsl:template match="inlFormation">
- <m:apply>
- <m:ci>inlFormation</m:ci>
- <xsl:apply-templates/>
- </m:apply>
-</xsl:template>
-
-<xsl:template match="inrEquality">
- <m:apply>
- <m:ci>inrEquality</m:ci>
- <xsl:apply-templates/>
- </m:apply>
-</xsl:template>
-
-<xsl:template match="inrFormation">
- <m:apply>
- <m:ci>inrFormation</m:ci>
- <xsl:apply-templates/>
- </m:apply>
-</xsl:template>
-
-<xsl:template match="decideEquality">
- <m:apply>
- <m:ci>decideEquality</m:ci>
- <xsl:apply-templates/>
- </m:apply>
-</xsl:template>
-
-<xsl:template match="unionElimination">
- <m:apply>
- <m:ci>unionElimination</m:ci>
- <m:cn>
- <xsl:value-of select="@number_hyp"/>
- </m:cn>
- <xsl:apply-templates/>
- </m:apply>
-</xsl:template>
-
-<xsl:template match="decideReduceLeft">
- <m:ci>decideReduceLeft</m:ci>
-</xsl:template>
-
-<xsl:template match="decideReduceRight">
- <m:ci>decideReduceRight</m:ci>
-</xsl:template>
-
-<xsl:template match="universeFormation">
- <m:apply>
- <m:ci>universeFormation</m:ci>
- <xsl:apply-templates/>
- </m:apply>
-</xsl:template>
-
-<xsl:template match="universeEquality">
- <m:ci>universeEquality</m:ci>
-</xsl:template>
-
-<xsl:template match="cumulativity">
- <m:apply>
- <m:ci>cumulativity</m:ci>
- <xsl:apply-templates/>
- </m:apply>
-</xsl:template>
-
-<xsl:template match="equalityFormation">
- <m:apply>
- <m:ci>equalityFormation</m:ci>
- <xsl:apply-templates/>
- </m:apply>
-</xsl:template>
-
-<xsl:template match="equalityEquality">
- <m:ci>equalityEquality</m:ci>
-</xsl:template>
-
-<xsl:template match="axiomEquality">
- <m:ci>axiomEquality</m:ci>
-</xsl:template>
-
-<xsl:template match="equalityElimination">
- <m:apply>
- <m:ci>equalityElimination</m:ci>
- <m:cn>
- <xsl:value-of select="@number_hyp"/>
- </m:cn>
- </m:apply>
-</xsl:template>
-
-<xsl:template match="hypothesisEquality">
- <m:apply>
- <m:ci>hypothesisEquality</m:ci>
- <m:cn>
- <xsl:value-of select="@number_hyp"/>
- </m:cn>
- </m:apply>
-</xsl:template>
-
-<xsl:template match="substitution">
- <m:apply>
- <m:ci>substitution</m:ci>
- <xsl:apply-templates/>
- </m:apply>
-</xsl:template>
-
-<xsl:template match="equality">
- <m:ci>equality</m:ci>
-</xsl:template>
-
-<xsl:template match="voidFormation">
- <m:ci>voidFormation</m:ci>
-</xsl:template>
-
-<xsl:template match="voidEquality">
- <m:ci>voidEquality</m:ci>
-</xsl:template>
-
-<xsl:template match="anyEquality">
- <m:ci>anyEquality</m:ci>
-</xsl:template>
-
-<xsl:template match="voidElimination">
- <m:apply>
- <m:ci>voidElimination</m:ci>
- <m:cn>
- <xsl:value-of select="@number_hyp"/>
- </m:cn>
- </m:apply>
-</xsl:template>
-
-<xsl:template match="atomFormation">
- <m:ci>atomFormation</m:ci>
-</xsl:template>
-
-<xsl:template match="atomEquality">
- <m:ci>atomEquality</m:ci>
-</xsl:template>
-
-<xsl:template match="tokenEquality">
- <m:ci>tokenEquality</m:ci>
-</xsl:template>
-
-<xsl:template match="tokenFormation">
- <m:apply>
- <m:ci>tokenFormation</m:ci>
- <xsl:apply-templates/>
- </m:apply>
-</xsl:template>
-
-<xsl:template match="atom_eqEquality">
- <m:apply>
- <m:ci>atom_eqEquality</m:ci>
- <xsl:apply-templates/>
- </m:apply>
-</xsl:template>
-
-<xsl:template match="atom_eqReduceTrue">
- <m:apply>
- <m:ci>atom_eqReduceTrue</m:ci>
- <xsl:apply-templates/>
- </m:apply>
-</xsl:template>
-
-<xsl:template match="atom_eqReduceFalse">
- <m:ci>atom_eqReduceFalse</m:ci>
-</xsl:template>
-
-<xsl:template match="intFormation">
- <m:ci>intFormation</m:ci>
-</xsl:template>
-
-<xsl:template match="intEquality">
- <m:ci>intEquality</m:ci>
-</xsl:template>
-
-<xsl:template match="natural_numberEquality">
- <m:ci>natural_numberEquality</m:ci>
-</xsl:template>
-
-<xsl:template match="minusEquality">
- <m:ci>minusEquality</m:ci>
-</xsl:template>
-
-<xsl:template match="addEquality">
- <m:ci>addEquality</m:ci>
-</xsl:template>
-
-<xsl:template match="subtractEquality">
- <m:ci>subtractEquality</m:ci>
-</xsl:template>
-
-<xsl:template match="multiplyEquality">
- <m:ci>multiplyEquality</m:ci>
-</xsl:template>
-
-<xsl:template match="divideFormation">
- <m:ci>divideFormation</m:ci>
-</xsl:template>
-
-<xsl:template match="addEquality">
- <m:ci>addEquality</m:ci>
-</xsl:template>
-
-<xsl:template match="subtractEquality">
- <m:ci>subtractEquality</m:ci>
-</xsl:template>
-
-<xsl:template match="multiplyEquality">
- <m:ci>multiplyEquality</m:ci>
-</xsl:template>
-
-<xsl:template match="divideEquality">
- <m:ci>divideEquality</m:ci>
-</xsl:template>
-
-<xsl:template match="remainderBounds1">
- <m:ci>remainderBounds1</m:ci>
-</xsl:template>
-
-<xsl:template match="remainderBounds2">
- <m:ci>remainderBounds2</m:ci>
-</xsl:template>
-
-<xsl:template match="remainderBounds3">
- <m:ci>remainderBounds3</m:ci>
-</xsl:template>
-
-<xsl:template match="remainderBounds4">
- <m:ci>remainderBounds4</m:ci>
-</xsl:template>
-
-<xsl:template match="divideRemainderSum">
- <m:ci>divideRemainderSum</m:ci>
-</xsl:template>
-
-<xsl:template match="arith">
- <m:apply>
- <m:ci>arith</m:ci>
- <xsl:apply-templates/>
- </m:apply>
-</xsl:template>
-
-<xsl:template match="indEquality">
- <m:apply>
- <m:ci>indEquality</m:ci>
- <xsl:apply-templates/>
- </m:apply>
-</xsl:template>
-
-<xsl:template match="intElimination">
- <m:apply>
- <m:ci>intElimination</m:ci>
- <m:cn>
- <xsl:value-of select="@number_hyp"/>
- </m:cn>
- <xsl:apply-templates/>
- </m:apply>
-</xsl:template>
-
-<xsl:template match="indReduceDown">
- <m:ci>indReduceDown</m:ci>
-</xsl:template>
-
-<xsl:template match="indReduceUp">
- <m:ci>indReduceUp</m:ci>
-</xsl:template>
-
-<xsl:template match="indReduceBase">
- <m:ci>indReduceBase</m:ci>
-</xsl:template>
-
-<xsl:template match="ind_eqEquality">
- <m:ci>ind_eqEquality</m:ci>
-</xsl:template>
-
-<xsl:template match="ind_eqReduceTrue">
- <m:ci>ind_eqReduceTrue</m:ci>
-</xsl:template>
-
-<xsl:template match="ind_eqReduceFalse">
- <m:ci>ind_eqReduceFalse</m:ci>
-</xsl:template>
-
-<xsl:template match="lessEquality">
- <m:ci>lessEquality</m:ci>
-</xsl:template>
-
-<xsl:template match="lessReduceTrue">
- <m:ci>lessReduceTrue</m:ci>
-</xsl:template>
-
-<xsl:template match="lessReduceFalse">
- <m:ci>lessReduceFalse</m:ci>
-</xsl:template>
-
-<xsl:template match="less_thanEquality">
- <m:ci>less_thanEquality</m:ci>
-</xsl:template>
-
-<xsl:template match="less_thanFormation">
- <m:ci>less_thanFormation</m:ci>
-</xsl:template>
-
-<xsl:template match="less_thanMember">
- <m:ci>less_thanMember</m:ci>
-</xsl:template>
-
-<xsl:template match="listFormation">
- <m:ci>listFormation</m:ci>
-</xsl:template>
-
-<xsl:template match="listEquality">
- <m:ci>listEquality</m:ci>
-</xsl:template>
-
-<xsl:template match="nilEquality">
- <m:apply>
- <m:ci>nilEquality</m:ci>
- <xsl:apply-templates/>
- </m:apply>
-</xsl:template>
-
-<xsl:template match="nilFormation">
- <m:apply>
- <m:ci>nilFormation</m:ci>
- <xsl:apply-templates/>
- </m:apply>
-</xsl:template>
-
-<xsl:template match="consFormation">
- <m:ci>consFormation</m:ci>
-</xsl:template>
-
-<xsl:template match="consEquality">
- <m:ci>consEquality</m:ci>
-</xsl:template>
-
-<xsl:template match="list_indEquality">
- <m:apply>
- <m:ci>list_indEquality</m:ci>
- <xsl:apply-templates/>
- </m:apply>
-</xsl:template>
-
-<xsl:template match="listElimination">
- <m:apply>
- <m:ci>listElimination</m:ci>
- <m:cn>
- <xsl:value-of select="@number_hyp"/>
- </m:cn>
- <xsl:apply-templates/>
- </m:apply>
-</xsl:template>
-
-<xsl:template match="list_indReduceUp">
- <m:ci>list_indReduceUp</m:ci>
-</xsl:template>
-
-<xsl:template match="list_indReduceBase">
- <m:ci>list_indReduceBase</m:ci>
-</xsl:template>
-
-<xsl:template match="recEquality">
- <m:apply>
- <m:ci>recEquality</m:ci>
- <xsl:apply-templates/>
- </m:apply>
-</xsl:template>
-
-<xsl:template match="rec_memberEquality">
- <m:apply>
- <m:ci>rec_memberEquality</m:ci>
- <xsl:apply-templates/>
- </m:apply>
-</xsl:template>
-
-<xsl:template match="rec_memberFormation">
- <m:apply>
- <m:ci>rec_memberFormation</m:ci>
- <xsl:apply-templates/>
- </m:apply>
-</xsl:template>
-
-<xsl:template match="rec_indEquality">
- <m:apply>
- <m:ci>rec_indEquality</m:ci>
- <xsl:apply-templates/>
- </m:apply>
-</xsl:template>
-
-<xsl:template match="recElimination">
- <m:apply>
- <m:ci>recElimination</m:ci>
- <m:cn>
- <xsl:value-of select="@number_hyp"/>
- </m:cn>
- <xsl:apply-templates/>
- </m:apply>
-</xsl:template>
-
-<xsl:template match="recUnrollElimination">
- <m:apply>
- <m:ci>recUnrollElimination</m:ci>
- <m:cn>
- <xsl:value-of select="@number_hyp"/>
- </m:cn>
- <xsl:apply-templates/>
- </m:apply>
-</xsl:template>
-
-<xsl:template match="dependent_setFormation">
- <m:apply>
- <m:ci>dependent_setFormation</m:ci>
- <xsl:apply-templates/>
- </m:apply>
-</xsl:template>
-
-<xsl:template match="independent_setFormation">
- <m:ci>independent_setFormation</m:ci>
-</xsl:template>
-
-<xsl:template match="setEquality">
- <m:apply>
- <m:ci>setEquality</m:ci>
- <xsl:apply-templates/>
- </m:apply>
-</xsl:template>
-
-<xsl:template match="dependent_set_memberEquality">
- <m:apply>
- <m:ci>dependent_set_memberEquality</m:ci>
- <xsl:apply-templates/>
- </m:apply>
-</xsl:template>
-
-<xsl:template match="dependent_set_memberFormation">
- <m:apply>
- <m:ci>dependent_set_memberFormation</m:ci>
- <xsl:apply-templates/>
- </m:apply>
-</xsl:template>
-
-<xsl:template match="independent_set_memberEquality">
- <m:ci>independent_set_memberEquality</m:ci>
-</xsl:template>
-
-<xsl:template match="independent_set_memberFormation">
- <m:apply>
- <m:ci>independent_set_memberFormation</m:ci>
- <xsl:apply-templates/>
- </m:apply>
-</xsl:template>
-
-<xsl:template match="setElimination">
- <m:apply>
- <m:ci>setElimination</m:ci>
- <m:cn>
- <xsl:value-of select="@number_hyp"/>
- </m:cn>
- <xsl:apply-templates/>
- </m:apply>
-</xsl:template>
-
-<xsl:template match="isectFormation">
- <m:apply>
- <m:ci>isectFormation</m:ci>
- <xsl:apply-templates/>
- </m:apply>
-</xsl:template>
-
-<xsl:template match="isectEquality">
- <m:apply>
- <m:ci>isectEquality</m:ci>
- <xsl:apply-templates/>
- </m:apply>
-</xsl:template>
-
-<xsl:template match="isect_memberEquality">
- <m:apply>
- <m:ci>isect_memberEquality</m:ci>
- <xsl:apply-templates/>
- </m:apply>
-</xsl:template>
-
-<xsl:template match="isect_memberFormation">
- <m:apply>
- <m:ci>isect_memberFormation</m:ci>
- <xsl:apply-templates/>
- </m:apply>
-</xsl:template>
-
-<xsl:template match="isect_member_caseEquality">
- <m:apply>
- <m:ci>isect_member_caseEquality</m:ci>
- <xsl:apply-templates/>
- </m:apply>
-</xsl:template>
-
-<xsl:template match="isectElimination">
- <m:apply>
- <m:ci>isectElimination</m:ci>
- <m:cn>
- <xsl:value-of select="@number_hyp"/>
- </m:cn>
- <xsl:apply-templates/>
- </m:apply>
-</xsl:template>
-
-<xsl:template match="quotientFormation">
- <m:apply>
- <m:ci>quotientFormation</m:ci>
- <xsl:apply-templates/>
- </m:apply>
-</xsl:template>
-
-<xsl:template match="quotientWeakEquality">
- <m:apply>
- <m:ci>quotientWeakEquality</m:ci>
- <xsl:apply-templates/>
- </m:apply>
-</xsl:template>
-
-<xsl:template match="quotientEquality">
- <m:ci>quotientEquality</m:ci>
-</xsl:template>
-
-<xsl:template match="quotient_memberWeakEquality">
- <m:apply>
- <m:ci>quotient_memberWeakEquality</m:ci>
- <xsl:apply-templates/>
- </m:apply>
-</xsl:template>
-
-<xsl:template match="quotient_memberFormation">
- <m:apply>
- <m:ci>quotient_memberFormation</m:ci>
- <xsl:apply-templates/>
- </m:apply>
-</xsl:template>
-
-<xsl:template match="quotient_memberEquality">
- <m:apply>
- <m:ci>quotient_memberEquality</m:ci>
- <xsl:apply-templates/>
- </m:apply>
-</xsl:template>
-
-<xsl:template match="quotient_equalityElimination">
- <m:apply>
- <m:ci>quotient_equalityElimination</m:ci>
- <m:cn>
- <xsl:value-of select="@number_hyp"/>
- </m:cn>
- <xsl:apply-templates/>
- </m:apply>
-</xsl:template>
-
-<xsl:template match="quotientElimination">
- <m:apply>
- <m:ci>quotientElimination</m:ci>
- <m:cn>
- <xsl:value-of select="@number_hyp"/>
- </m:cn>
- <xsl:apply-templates/>
- </m:apply>
-</xsl:template>
-
-<xsl:template match="quotientElimination_2">
- <m:apply>
- <m:ci>quotientElimination_2</m:ci>
- <m:cn>
- <xsl:value-of select="@number_hyp"/>
- </m:cn>
- <xsl:apply-templates/>
- </m:apply>
-</xsl:template>
-
-<xsl:template match="direct_computation">
- <m:apply>
- <m:ci>direct_computation</m:ci>
- <xsl:apply-templates/>
- </m:apply>
-</xsl:template>
-
-<xsl:template match="reverse_direct_computation">
- <m:apply>
- <m:ci>reverse_direct_computation</m:ci>
- <xsl:apply-templates/>
- </m:apply>
-</xsl:template>
-
-<xsl:template match="direct_computation_hypothesis">
- <m:apply>
- <m:ci>direct_computation_hypothesis</m:ci>
- <m:cn>
- <xsl:value-of select="@number_hyp"/>
- </m:cn>
- <xsl:apply-templates/>
- </m:apply>
-</xsl:template>
-
-<xsl:template match="reverse_direct_computation_hypothesis">
- <m:apply>
- <m:ci>reverse_direct_computation_hypothesis</m:ci>
- <m:cn>
- <xsl:value-of select="@number_hyp"/>
- </m:cn>
- <xsl:apply-templates/>
- </m:apply>
-</xsl:template>
-
-<xsl:template match="ruleinstance/hypothesis">
- <m:apply>
- <m:ci>hypothesis</m:ci>
- <m:cn>
- <xsl:value-of select="@number_hyp"/>
- </m:cn>
- </m:apply>
-</xsl:template>
-
-<xsl:template match="thin">
- <m:apply>
- <m:ci>thin</m:ci>
- <m:cn>
- <xsl:value-of select="@number_hyp"/>
- </m:cn>
- </m:apply>
-</xsl:template>
-
-<xsl:template match="cut">
- <m:apply>
- <m:ci>cut</m:ci>
- <m:cn>
- <xsl:value-of select="@number_hyp"/>
- </m:cn>
- <xsl:apply-templates/>
- </m:apply>
-</xsl:template>
-
-<xsl:template match="hyp_replacement">
- <m:apply>
- <m:ci>hyp_replacement</m:ci>
- <m:cn>
- <xsl:value-of select="@number_hyp"/>
- </m:cn>
- <xsl:apply-templates/>
- </m:apply>
-</xsl:template>
-
-<xsl:template match="lemma">
- <m:apply>
- <m:ci>lemma</m:ci>
- <m:ci>
- <xsl:value-of select="@name"/>
- </m:ci>
- </m:apply>
-</xsl:template>
-
-<xsl:template match="extract">
- <m:apply>
- <m:ci>extract</m:ci>
- <m:ci>
- <xsl:value-of select="@name"/>
- </m:ci>
- </m:apply>
-</xsl:template>
-
-<xsl:template match="instantiate">
- <m:apply>
- <m:ci>instantiate</m:ci>
- <xsl:apply-templates/>
- </m:apply>
-</xsl:template>
-
-<xsl:template match="because">
- <m:ci>because</m:ci>
-</xsl:template>
-
-<xsl:template match="rename">
- <m:apply>
- <m:ci>rename</m:ci>
- <xsl:apply-templates/>
- </m:apply>
-</xsl:template>
-
-<xsl:template match="introduction">
- <m:apply>
- <m:ci>introducition</m:ci>
- <xsl:apply-templates/>
- </m:apply>
-</xsl:template>
-
-</xsl:stylesheet>
projects / helm.git / blobdiff