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