<grammar xmlns="http://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>