1<grammar xmlns="http://relaxng.org/ns/structure/1.0"
2         ns="http://relaxng.org/ns/proofsystem">
3
4<start>
5  <element name="proofSystem">
6    <oneOrMore>
7      <element name="rule">
8        <attribute name="name"/>
9	<zeroOrMore>
10	  <ref name="antecedent"/>
11	</zeroOrMore>
12	<ref name="consequent"/>
13      </element>
14    </oneOrMore>
15  </element>
16</start>
17
18<define name="formula">
19  <element name="formula">
20    <choice>
21      <ref name="judgement"/>
22      <ref name="expr"/>
23    </choice>
24  </element>
25</define>
26
27<define name="consequent">
28  <ref name="judgement"/>
29</define>
30
31<define name="antecedent">
32  <ref name="judgement"/>
33</define>
34
35<define name="judgement">
36  <choice>
37    <element name="judgement">
38      <attribute name="name"/>
39      <zeroOrMore>
40	<ref name="expr"/>
41      </zeroOrMore>
42    </element>
43    <element name="not">
44      <ref name="judgement"/>
45    </element>
46  </choice>
47</define>
48
49<define name="expr">
50  <choice>
51    <element name="var">
52      <attribute name="range"/>
53      <optional>
54	<attribute name="index"/>
55      </optional>
56      <optional>
57	<attribute name="sub"/>
58      </optional>
59    </element>
60    <element name="function">
61      <attribute name="name"/>
62      <zeroOrMore>
63        <ref name="expr"/>
64      </zeroOrMore>
65    </element>
66    <element name="element">
67      <attribute name="name"/>
68      <zeroOrMore>
69        <element name="attribute">
70          <attribute name="name"/>
71          <ref name="expr"/>
72        </element>
73      </zeroOrMore>
74      <optional>
75        <ref name="context"/>
76      </optional>
77      <zeroOrMore>
78        <ref name="expr"/>
79      </zeroOrMore>
80    </element>
81    <element name="group">
82      <zeroOrMore>
83        <ref name="expr"/>
84      </zeroOrMore>
85    </element>
86    <element name="string"><text/></element>
87  </choice>
88</define>
89
90<define name="context">
91  <element name="context">
92    <ref name="expr"/>
93  </element>
94</define>
95
96</grammar>
97