]> matita.cs.unibo.it Git - helm.git/blobdiff - helm/nuprl_stylesheets/nuprl_rules.xsl
First commit of the NuPRL stylesheets.
[helm.git] / helm / nuprl_stylesheets / nuprl_rules.xsl
diff --git a/helm/nuprl_stylesheets/nuprl_rules.xsl b/helm/nuprl_stylesheets/nuprl_rules.xsl
new file mode 100644 (file)
index 0000000..6926dde
--- /dev/null
@@ -0,0 +1,876 @@
+<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>