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>
|
---|