Syntax der Eingabe

<identifier> ::=  ([a-z] | [A-Z]) ([a-z] | [A-Z] | [0-9] | '_')*
<comment>    ::= '/*' <anything> '*/' | '//' <anything> '\n'

ADT ::= <name>?
        <sorts>
        <constructors>?
        <operations>
        <vars>
        <axioms>?
<name> ::= ’name’ <id>
<sorts> ::= ’sorts’ <sort> (’,’ <sort>)*
<constructors>::= ’constructors’ <operation>+
<operations> ::= ’operations’ <operation>+
<operation> ::= <operation_name> ’:’
                  (<sort> (’><’ <sort>)* ’->’)? <sort>
<vars> ::= <var> ’:’ <sort> (’,’ <var> ’:’ <sort>)*
<axioms> ::= ’axioms’ (<axiom_name> ’:’ <eq_s>)+
<eq_s> ::= <classic_tree> '=' <classic_tree> (';' |':')? | <function_tree> '=' <function_tree> (';' |':')
<tree> ::= <classic_tree> <function_tree>
<classic_tree> ::= <var> | (<operation_name> (’(’ <classic_tree> (’,’ <classic_tree>)* ’)’)?)
<function_tree> ::= <var> | <operation_name> <function_tree>* | '(' <function_tree> ')'

Task ::= <task> <lemma_tasks?> <task_lemmata>?
<task> ::= ’task’ <eq> <task_ind_var>? (<task_pt> | <ind_pt>)
<task_ind_var>::= ’induction’ <var>
<lemma_tasks> ::= ’proof lemmata’ (<lemma_name> ’:’ <eq> <task_ind_var>? (<task_pt> | <ind_pt>))+
<task_lemmata>::= ’lemmata’ (<lemma_name> ’:’ <eq>)+
<eq> ::= (<fixed> ’:’)? (<forall> ’:’)? <eq_s>
<fixed> ::= ’fixed’ <var> ’:’ <sort> (’,’ <var> ’:’ <sort>)*
<forall> ::= ’forall’ <var> ’:’ <sort> (’,’ <var> ’:’ <sort>)*
<task_pt> ::= ’maxpt’ <nat> ’minsteps’ <nat> ’maxsteps’ <nat>
<ind_pt> ::= <case_pt>+ <ih_pt>
<case_pt> ::= ’case’ <constructor_name> <task_pt>
<ih_pt> ::= ’IH’ ’maxpt’ <nat>

Proof ::= <lemma>* <mainProof> <lemma>*
<mainProof> ::= ’proof’ <singleProof> <proof_end>?
<lemma> ::= <lemmaDef> <singleProof>
<lemmaDef> ::=’lemma’ <lemma_name> ’:’ <eq>
<singleProof> ::= <ind_proof> | <transformation>
<proof_end> ::= ’q.e.d.’ | ’w.z.b.w.’
<ind_proof> ::= <ind_var>? <ind>
<ind_var> ::= ’induction’ <var>
<ind> ::= <ind_basis>+ <ind_hyp>+ <ind_step>*
<ind_basis> ::= ’IA’ <ind_case> <transformation>
<ind_hyp> ::= ’IH’ <IH_name>? <eq>
<ind_step> ::= ’IS’ <ind_case> <transformation>
<ind_case> ::= ’zu zeigen:’ <eq>
<transformation> ::= <start_tree> <transformation_step>+
<start_tree> ::= <tree>
<transformation_step>::= ’{’ <rule>
                         ’,’ <direction>
                         ’,’ <termpart>
                         ’,’ <subst> ’}’
                         ’=’ <result_tree>
<rule> ::= <rule_name>
<direction> ::= ( ’lr’ | ’rl’ )
<termpart> ::= <tree>
<subst> ::= ’[’ ( <tree> ’/’ <var> (’,’ <tree> ’/’ <var>)*)? ’]’
<result_tree> ::= <tree>

(’Round’ <WhiteSpace> <Integer> ’\n’)?
(<i> <WhiteSpace> <Double> ’\n’)*