1. Der Startbaum stimmt nicht mit dem linken Baum der Aufgabenstellung überein.
2. Der letzte Ergebnisbaum stimmt nicht mit dem rechten Baum der Aufgabenstellung überein.
3. Die Variable einer Substitution ist nicht im ADT definiert.
4. Die Sorte der Variable einer Substitution und des Baums mit dem sie substituiert werden soll, stimmen nicht überein, sodass die Definition A.11 verletzt wird.
5. Die Sorte des Ergebnisbaums stimmt nicht mit der Sorte des vorherigen Baums überein
### Inhaltliche Fehler
6. Der angegebene Unterterm ist kein Unterterm des vorherigen Baums gemäß Definition A.9. D.h., der Unterterm ist Falsch.
7. Der Unterterm passt auf keine der Seiten des Axioms, es ist also der Unterterm oder das Axiom falsch.
8. Der Unterterm passt nur auf die Endseite des Axioms. D.h., die Richtungsangabe ist falsch.
9. Der Unterterm passt auf die Startseite des Axioms, aber die Substitution ist falsch.
10. Der Unterterm passt nur auf die Endseite des Axioms und die Substitution ist falsch. Die Richtungsangabe ist auch falsch.
11. Der Unterterm passt auf die Startseite des Axioms, die Substitution ist korrekt, wurde aber falsch angewandt, sodass der Ergebnisbaum falsch ist.
12. Der Unterterm passt nur auf die Endseite des Axioms, die Substitution ist dafur korrekt, der Unterterm wurde nicht korrekt durch die substituierte Startseite des Axioms ersetzt, sodass der Ergebnisbaum falsch ist. Die Richtungsangabe ist auch falsch.
### Warnungen
13. Eine oder mehrere Variablen, die in der Substitution angegeben worden sind, welche
mit einem Baum substituiert werden sollen, können nicht in dem angegebenen Axiom
gefunden werden.
# Fehler im Zusammenhang mit Lemmata
### Formale Fehler
20. Ein Lemma hat zyklische Abhängigkeiten. Demnach ist das Lemma unbewiesen, außer das Lemma entspricht einer Aufgabenstellung.
21. Im Transformationsschritt wird ein unbewiesenes Lemma angewandt oder es wird ein Lemma aus der Aufgabenstellung entgegen der topologischen Ordnung angewandt. Demnach ist der Transformationsschritt falsch.
22. Ein Lemma, dessen Name mit einem zu beweisenden Lemma ubereinstimmt, stimmt inhaltlich nicht mit dem zu beweisenden Lemma uberein. Demnach ist die entsprechende Aufgabenstellung nicht erfüllt.
### Inhaltliche Fehler
23. Ein Lemma, welches von der Aufgabenstellung vorgegeben wurde, ist fur den Hauptbeweis nicht nützlich eingesetzt.
# Fehler im Zusammenhang mit struktureller Induktion
### Formale Fehler
30. Es wird eine Induktion uber eine feste Variable geführt.
31. Im Beweis wird eine Induktionsvariable gewählt, welche keine Konstruktoren hat.
32. Ein Induktionsfall fehlt.
33. Es liegt ein ungultiger / doppelter Induktionsfall vor.
34. Die Gleichung eines Induktionsfalls oder einer Induktionshypothese ist nicht korrekt.
35. Eine Variable, die fest sein soll wird allquantifiziert.
36. Induktionshypothese wird im Induktionsanfang angewandt.
37. Bei Anwendung einer Regel wird eine feste Variable substituiert.
38. Die Induktionsvariable stimmt nicht mit der Induktionsvariable der Aufgabenstellung überein.
39. Bei vorgegebener Induktionsvariable wird eine Transformation als Beweis verwendet.
### Inhaltliche Fehler
40. Eine Variable, die allquantifiziert sein soll, wird als fest angegeben.
41. Die Angabe der Art des Induktionsfalls ist inkonsistent zur Wahl des Konstruktors
### Warnungen
42. Es liegt eine doppelte Induktionshypothese vor.
43. Die aufbauende Variable der Induktionshypothese wird in keinem Induktionsfall als solche eingesetzt.
