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>