<grammar xmlns=“relaxng.org/ns/structure/1.0

ns="http://relaxng.org/ns/proofsystem">

<start>

<element name="proofSystem">
  <oneOrMore>
    <element name="rule">
      <attribute name="name"/>
      <zeroOrMore>
        <ref name="antecedent"/>
      </zeroOrMore>
      <ref name="consequent"/>
    </element>
  </oneOrMore>
</element>

</start>

<define name=“formula”>

<element name="formula">
  <choice>
    <ref name="judgement"/>
    <ref name="expr"/>
  </choice>
</element>

</define>

<define name=“consequent”>

<ref name="judgement"/>

</define>

<define name=“antecedent”>

<ref name="judgement"/>

</define>

<define name=“judgement”>

<choice>
  <element name="judgement">
    <attribute name="name"/>
    <zeroOrMore>
      <ref name="expr"/>
    </zeroOrMore>
  </element>
  <element name="not">
    <ref name="judgement"/>
  </element>
</choice>

</define>

<define name=“expr”>

<choice>
  <element name="var">
    <attribute name="range"/>
    <optional>
      <attribute name="index"/>
    </optional>
    <optional>
      <attribute name="sub"/>
    </optional>
  </element>
  <element name="function">
    <attribute name="name"/>
    <zeroOrMore>
      <ref name="expr"/>
    </zeroOrMore>
  </element>
  <element name="element">
    <attribute name="name"/>
    <zeroOrMore>
      <element name="attribute">
        <attribute name="name"/>
        <ref name="expr"/> 
      </element>
    </zeroOrMore>
    <optional>
      <ref name="context"/>
    </optional>
    <zeroOrMore>
      <ref name="expr"/>
    </zeroOrMore>
  </element>
  <element name="group">
    <zeroOrMore>
      <ref name="expr"/>
    </zeroOrMore>
  </element>
  <element name="string"><text/></element>
</choice>

</define>

<define name=“context”>

<element name="context">
  <ref name="expr"/>
</element>

</define>

</grammar>