Syntax-der-Eingabe.md

+1. Abstrakter Datentyp
+```
+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> ’:’ <tree> ’=’ <tree>)+
+<tree> ::= <var> | (<operation_name> (’(’ <tree> (’,’ <tree>)* ’)’)?)
+```
+
+2. Aufgabenstellung
+```
+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> ’:’)? <tree> ’=’ <tree>
+<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>
+```
+
+3. Beweis
+```
+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>
+```
+
+4. Syntax der Konfigurationsdatei:
+```
+(’Round’ <WhiteSpace> <Integer> ’\n’)?
+(<i> <WhiteSpace> <Double> ’\n’)*
+```
\ No newline at end of file