Syntax-der-Eingabe.md

@@ -13,8 +13,11 @@ ADT ::= <name>?
 <operation> ::= <operation_name> ’:’
                   (<sort> (’><’ <sort>)* ’->’)? <sort>
 <vars> ::= <var> ’:’ <sort> (’,’ <var> ’:’ <sort>)*
-<axioms> ::= ’axioms’ (<axiom_name> ’:’ <tree> ’=’ <tree>)+
-<tree> ::= <var> | (<operation_name> (’(’ <tree> (’,’ <tree>)* ’)’)?)
+<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> ')'
 ```
 
 2. Aufgabenstellung
@@ -24,7 +27,7 @@ Task ::= <task> <lemma_tasks?> <task_lemmata>?
 <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> ’:’)? <tree> ’=’ <tree>
+<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>