From d56a6b1d89621ec6060f5780f9ddecc627a1ac3e Mon Sep 17 00:00:00 2001
From: Edward Sabinus <edward.sabinus@informatik.uni-halle.de>
Date: Tue, 23 Apr 2024 16:04:39 +0200
Subject: [PATCH] changed possible errrors to non deadly in both proof
listener; Added test cases for all non deadly semantic errors. TODO: employ
those tests in the test manager (some of the tests may be impossible to test
due to syntax error from antlr)
---
.../Parser/Proof_Listener.cs | 35 ++++++-----
.../Parser/TransformationStep_Listener.cs | 58 +++++++++----------
.../Tests/extra/NonDeadSemErrs/0riginal.proof | 46 +++++++++++++++
.../Tests/extra/NonDeadSemErrs/1riginal.task | 8 +++
.../Tests/extra/NonDeadSemErrs/axiom.proof | 46 +++++++++++++++
.../extra/NonDeadSemErrs/direction.proof | 46 +++++++++++++++
.../Tests/extra/NonDeadSemErrs/indvar1.proof | 47 +++++++++++++++
.../Tests/extra/NonDeadSemErrs/indvar2.proof | 48 +++++++++++++++
.../extra/NonDeadSemErrs/resulttree.proof | 46 +++++++++++++++
.../extra/NonDeadSemErrs/starttree.proof | 45 ++++++++++++++
.../extra/NonDeadSemErrs/substitution1.proof | 46 +++++++++++++++
.../extra/NonDeadSemErrs/substitution2.proof | 46 +++++++++++++++
.../Tests/extra/NonDeadSemErrs/termpart.proof | 46 +++++++++++++++
.../extra/NonDeadSemErrs/transformation.proof | 39 +++++++++++++
14 files changed, 555 insertions(+), 47 deletions(-)
create mode 100644 BewerterStrukturellerInduktion/bin/Debug/netcoreapp5.0/Tests/extra/NonDeadSemErrs/0riginal.proof
create mode 100644 BewerterStrukturellerInduktion/bin/Debug/netcoreapp5.0/Tests/extra/NonDeadSemErrs/1riginal.task
create mode 100644 BewerterStrukturellerInduktion/bin/Debug/netcoreapp5.0/Tests/extra/NonDeadSemErrs/axiom.proof
create mode 100644 BewerterStrukturellerInduktion/bin/Debug/netcoreapp5.0/Tests/extra/NonDeadSemErrs/direction.proof
create mode 100644 BewerterStrukturellerInduktion/bin/Debug/netcoreapp5.0/Tests/extra/NonDeadSemErrs/indvar1.proof
create mode 100644 BewerterStrukturellerInduktion/bin/Debug/netcoreapp5.0/Tests/extra/NonDeadSemErrs/indvar2.proof
create mode 100644 BewerterStrukturellerInduktion/bin/Debug/netcoreapp5.0/Tests/extra/NonDeadSemErrs/resulttree.proof
create mode 100644 BewerterStrukturellerInduktion/bin/Debug/netcoreapp5.0/Tests/extra/NonDeadSemErrs/starttree.proof
create mode 100644 BewerterStrukturellerInduktion/bin/Debug/netcoreapp5.0/Tests/extra/NonDeadSemErrs/substitution1.proof
create mode 100644 BewerterStrukturellerInduktion/bin/Debug/netcoreapp5.0/Tests/extra/NonDeadSemErrs/substitution2.proof
create mode 100644 BewerterStrukturellerInduktion/bin/Debug/netcoreapp5.0/Tests/extra/NonDeadSemErrs/termpart.proof
create mode 100644 BewerterStrukturellerInduktion/bin/Debug/netcoreapp5.0/Tests/extra/NonDeadSemErrs/transformation.proof
diff --git a/BewerterStrukturellerInduktion/Eingabeverwaltung/Parser/Proof_Listener.cs b/BewerterStrukturellerInduktion/Eingabeverwaltung/Parser/Proof_Listener.cs
index 3108f13..d02698f 100644
--- a/BewerterStrukturellerInduktion/Eingabeverwaltung/Parser/Proof_Listener.cs
+++ b/BewerterStrukturellerInduktion/Eingabeverwaltung/Parser/Proof_Listener.cs
@@ -55,7 +55,7 @@ namespace Eingabeverwaltung.Parser
public void EnterProof([NotNull] ProofParser.ProofContext context) => lemmata = new List<Lemma>();
public void ExitProof([NotNull] ProofParser.ProofContext context)
{
- if (mainProof == null) throw new KontextException(new Coords(context),"No main proof found in ExitProof!");
+ if (mainProof == null) throw new SemanticAnalysisDeadlyError(new Coords(context),"No main proof found in ExitProof!");
container.Proof = new Proof(mainProof, lemmata);
}
public void EnterMainProof([NotNull] ProofParser.MainProofContext context)
@@ -96,7 +96,7 @@ namespace Eingabeverwaltung.Parser
public void EnterSingleProof([NotNull] ProofParser.SingleProofContext context) => SP = null;
public void ExitSingleProof([NotNull] ProofParser.SingleProofContext context)
{
- if (SP == null) throw new KontextException(new Coords(context),"No SingleProof found in ExitSingleProof!");
+ if (SP == null) throw new SemanticAnalysisDeadlyError(new Coords(context),"No SingleProof found in ExitSingleProof!");
}
public void EnterProof_end([NotNull] ProofParser.Proof_endContext context) { }
public void ExitProof_end([NotNull] ProofParser.Proof_endContext context) { }
@@ -111,7 +111,7 @@ namespace Eingabeverwaltung.Parser
public void EnterStart_tree([NotNull] ProofParser.Start_treeContext context) => LH.trees = new List<Tree>();
public void ExitStart_tree([NotNull] ProofParser.Start_treeContext context)
{
- if (LH.trees.Count != 1) throw new KontextException(new Coords(context),"Trees was Expected to have 1 Tree for Start_tree, but found " + LH.trees.Count + " trees! They are: " + LH.TreeListToString(LH.trees));
+ if (LH.trees.Count != 1) LH.errors.Add(new SemanticAnalysisError(new Coords(context),"Trees was Expected to have 1 Tree for Start_tree, but found " + LH.trees.Count + " trees! They are: " + LH.TreeListToString(LH.trees)));
startTree = LH.trees[0];
}
@@ -153,10 +153,9 @@ namespace Eingabeverwaltung.Parser
foreach (SingleTask lemmaTask in container.Task.lemmaTasks)
if (lemmaTask.name == proofName) { indVar = lemmaTask.indVariable; lemmaIndVarTask = lemmaTask; break; }
}
- else throw new KontextException(coords,"ExitInduction with Context = " + context.GetText() + " was not able to find the sense of its life.");
+ else throw new SemanticAnalysisDeadlyError(coords,"ExitInduction with Context = " + context.GetText() + " was not able to find the sense of its life.");
}
- if (indVar == null) throw new KontextException(coords,"Induction variable of proof "+ proofName + " is neither definied in proof nor in task!");
Equation eq = null; List<Variable> fixedVars = null;
if (lemmaDef != null)
{// this SP is in lemma lemmaDef
@@ -165,11 +164,12 @@ namespace Eingabeverwaltung.Parser
{// this SP is in Mainproof
eq = container.Task.task.eq; fixedVars = container.Task.task.fixedVars;
}
- if (lemmaIndVarTask != null)
+ if (indVar == null) LH.errors.Add(new SemanticAnalysisError(coords, "Induction variable of proof " + proofName + " is neither definied in proof nor in task!"));
+ else if (lemmaIndVarTask != null)
{ // inVar must be of context of its lemma: find substitution to get correct variable.
Ueberpruefung.CheckHelper.getSubsAndRenamings(eq, lemmaIndVarTask.eq, out List<Substitution> subs, out List<Substitution> renamings);
bool changed = false;
- if (subs != null) // then lemma is not proving the task (error 22), do nothing then
+ if (subs != null) // else lemma is not proving the task (error 22), do nothing then
foreach(Substitution renaming in renamings)
if (renaming.tree is TreeVariable tv)
if (tv.variable == indVar) { indVar = renaming.variable; changed = true; break; }
@@ -181,7 +181,7 @@ namespace Eingabeverwaltung.Parser
{
string variableName = context.BEZ().GetText();
Variable variable = LH.findVariableInADT_Vars(variableName);
- if (variable == null) throw new KontextException(new Coords(context),"Could not find Induction variable " + variableName + " in current context of variables.");
+ if (variable == null) LH.errors.Add(new SemanticAnalysisError(new Coords(context),"Could not find Induction variable " + variableName + " in current context of variables."));
indVar = variable;
}
public void ExitInd_var([NotNull] ProofParser.Ind_varContext context) { }
@@ -191,7 +191,7 @@ namespace Eingabeverwaltung.Parser
Coords coords = new Coords(context);
if (SP is Transformation tr)
indCases.Add(new InductionCase(coords,"IA", LH.equation, LH.fixedVars, tr));
- else throw new KontextException(coords,"Found Singleproof in induction basis that is not a transformation!");
+ else throw new SemanticAnalysisDeadlyError(coords,"Found Singleproof in induction basis that is not a transformation!");
}
public void EnterInd_step([NotNull] ProofParser.Ind_stepContext context) => SP = null;
public void ExitInd_step([NotNull] ProofParser.Ind_stepContext context)
@@ -199,7 +199,7 @@ namespace Eingabeverwaltung.Parser
Coords coords = new Coords(context);
if (SP is Transformation tr)
indCases.Add(new InductionCase(coords, "IS", LH.equation, LH.fixedVars, tr));
- else throw new KontextException(coords,"Found Singleproof in induction step that is not a transformation!");
+ else throw new SemanticAnalysisDeadlyError(coords,"Found Singleproof in induction step that is not a transformation!");
}
public void EnterInd_hyp([NotNull] ProofParser.Ind_hypContext context) { }
public void ExitInd_hyp([NotNull] ProofParser.Ind_hypContext context)
@@ -210,10 +210,9 @@ namespace Eingabeverwaltung.Parser
name = context.BEZ().GetText();
else name = "IH";
foreach (InductionHypothesis ih in indHyps)
- if (ih.name == name) throw new KontextException(coords,"There are more then 1 inductionhypothesis with name "+name+"!");
- Test_Lemmata_all_Unique(name,"InductionHypothesis",coords);
- indHyps.Add(new InductionHypothesis(coords,name,LH.equation, LH.fixedVars));
-
+ if (ih.name == name) LH.errors.Add(new SemanticAnalysisError(coords,"There are more then 1 inductionhypothesis with name "+name+"!"));
+ Test_Lemmata_all_Unique(name, "InductionHypothesis", coords);
+ indHyps.Add(new InductionHypothesis(coords, name, LH.equation, LH.fixedVars));
}
public void EnterInd_case([NotNull] ProofParser.Ind_caseContext context) { }
public void ExitInd_case([NotNull] ProofParser.Ind_caseContext context)
@@ -290,11 +289,11 @@ namespace Eingabeverwaltung.Parser
private void Test_Lemmata_all_Unique(string name, string type, Coords coords)
{
foreach (Rule axiom in LH.adt_axioms)
- if (axiom.name == name) throw new KontextException(coords,"The " + type + " "+ name + " has same name like 1 Axiom of ADT!");
- foreach (Rule lemma in lemmata)
- if (lemma.name == name) throw new KontextException(coords,"The " + type + " "+ name + " has same name like 1 Lemma of Proof!");
+ if (axiom.name == name) LH.errors.Add(new SemanticAnalysisError(coords,"The " + type + " "+ name + " has same name like 1 Axiom of ADT!"));
+ foreach (Rule lemma in lemmata)
+ if (lemma.name == name) LH.errors.Add(new SemanticAnalysisError(coords, "The " + type + " " + name + " has same name like 1 Lemma of Proof!"));
foreach (Rule lemma in container.Task.lemmata)
- if (lemma.name == name) throw new KontextException(coords,"The " + type + " "+ name + " has same name like 1 Lemma of Task!");
+ if (lemma.name == name) LH.errors.Add(new SemanticAnalysisError(coords, "The " + type + " " + name + " has same name like 1 Lemma of Task!"));
}
}
}
diff --git a/BewerterStrukturellerInduktion/Eingabeverwaltung/Parser/TransformationStep_Listener.cs b/BewerterStrukturellerInduktion/Eingabeverwaltung/Parser/TransformationStep_Listener.cs
index d33b3af..b84d12c 100644
--- a/BewerterStrukturellerInduktion/Eingabeverwaltung/Parser/TransformationStep_Listener.cs
+++ b/BewerterStrukturellerInduktion/Eingabeverwaltung/Parser/TransformationStep_Listener.cs
@@ -58,7 +58,7 @@ namespace Eingabeverwaltung.Parser
{
if (container.Proof.proof is Transformation tr) currentTR = tr;
else if (container.Proof.proof is Induction ind) currentInd = ind; // will find tr by ind rules
- else throw new KontextException(new Coords(context),"Error: The proof of MainProof is wether Transformation nor Induction!");
+ else throw new SemanticAnalysisDeadlyError(new Coords(context),"Error: The proof of MainProof is neither Transformation nor Induction!");
// Variablen der Aufgabenstellung gelten im Hauptbeweis als erstes
List<List<Variable>> variableDefinitionContext;
variableDefinitionContext = new List<List<Variable>>() { container.Task.task.eq.variables };
@@ -76,10 +76,10 @@ namespace Eingabeverwaltung.Parser
currentLemma = null;
foreach(Lemma lemma in container.Proof.lemmata)
if (lemma.name == lemmaName) currentLemma = lemma;
- if (currentLemma == null) throw new KontextException(coords,"Cannot find current Lemma: "+lemmaName+" in Container!");
+ if (currentLemma == null) throw new SemanticAnalysisDeadlyError(coords,"Cannot find current Lemma: "+lemmaName+" in Container!");
if (currentLemma.proof is Transformation tr) currentTR = tr;
else if (currentLemma.proof is Induction ind) currentInd = ind; // will find tr by ind rules
- else throw new KontextException(coords,"Error: The proof of Lemma "+lemmaName+" is wether Transformation nor Induction!");
+ else throw new SemanticAnalysisDeadlyError(coords,"Error: The proof of Lemma "+lemmaName+" is neither Transformation nor Induction!");
}
public void ExitLemma([NotNull] ProofParser.LemmaContext context) => currentLemma = null;
@@ -103,7 +103,7 @@ namespace Eingabeverwaltung.Parser
public void EnterTransformation([NotNull] ProofParser.TransformationContext context) => TSs = new List<Transformation_Step>();
public void ExitTransformation([NotNull] ProofParser.TransformationContext context)
{
- if (TSs.Count < 1) throw new KontextException(new Coords(context),"No TransformationSteps found in Transformation at ExitTransformation!");
+ if (TSs.Count < 1) LH.errors.Add(new SemanticAnalysisError(new Coords(context),"No TransformationSteps found in Transformation at ExitTransformation!"));
Tree startT = currentTR.startTree;
for (int i = 0; i < TSs.Count; i++)
{
@@ -151,9 +151,9 @@ namespace Eingabeverwaltung.Parser
{
rule = findRuleIn(ruleName, currentInd.indHyps.Cast<Rule>().ToList());
if (rule != null) TS.rule = rule;
- else throw new KontextException(coords,"The rule " + ruleName + " is not defined!");
+ else { LH.errors.Add(new SemanticAnalysisError(coords, "The rule " + ruleName + " is not defined!")); TS.rule = new Lemma(coords, ruleName, null, new List<Variable>(), null); }
}
- else throw new KontextException(coords,"The rule " + ruleName + " is not defined!");
+ else { LH.errors.Add(new SemanticAnalysisError(coords, "The rule " + ruleName + " is not defined!")); TS.rule = new Lemma(coords, ruleName, null, new List<Variable>(), null); }
}
}
}
@@ -161,18 +161,9 @@ namespace Eingabeverwaltung.Parser
}
else if (context.GetChild(0).GetText() == "IH")
{
- if (currentInd != null) rule = findRuleIn("IH", currentInd.indHyps.Cast<Rule>().ToList()); ;
+ if (currentInd != null) rule = findRuleIn("IH", currentInd.indHyps.Cast<Rule>().ToList());
if (rule != null) TS.rule = rule;
- else
- {
- string position = "";
- if (currentLemma == null) position += "main proof > ";
- else position += "lemma: " + currentLemma.name + " > ";
- if (currentInd != null) position += "induction ";
- if (currentIndCase != null) position += " of case " + currentIndCase.type + " > ";
- position += " TransformationStep No " + (TSs.Count+1);
- throw new KontextException(coords,"The Inductionhypothesis is not defined for the current TransformationStep (" + position + ")!");
- }
+ else { LH.errors.Add(new SemanticAnalysisError(coords,"The Inductionhypothesis is not defined for the current TransformationStep!")); TS.rule = new InductionHypothesis(coords,"IH",null,new List<Variable>()); }
}
}
@@ -184,15 +175,16 @@ namespace Eingabeverwaltung.Parser
{
case "rl": TS.direction = '<'; break;
case "lr": TS.direction = '>'; break;
- default: throw new KontextException(new Coords(context),"The Direction of the TransformationStep is undefined! Expected \'rl\' or \'lr' but found \"" + direction + "\".");
+ default: LH.errors.Add(new SemanticAnalysisError(new Coords(context),"The Direction of the TransformationStep is undefined! Expected \'rl\' or \'lr\' but found \"" + direction + "\"."));
+ TS.direction = '>'; break;
}
}
public void EnterTermpart([NotNull] ProofParser.TermpartContext context) => LH.trees = new List<Tree>();
public void ExitTermpart([NotNull] ProofParser.TermpartContext context)
{
- if (LH.trees.Count != 1) throw new KontextException(new Coords(context),"Trees was Expected to have 1 Tree for Termpart, but found " + LH.trees.Count + " trees! They are: " + LH.TreeListToString(LH.trees));
- TS.termpart = LH.trees[0];
+ if (LH.trees.Count != 1) LH.errors.Add(new SemanticAnalysisError(new Coords(context), "Trees was Expected to have 1 Tree for Termpart, but found " + LH.trees.Count + " trees! They are: " + LH.TreeListToString(LH.trees)));
+ else TS.termpart = LH.trees[0];
LH.trees = null;
}
@@ -217,18 +209,26 @@ namespace Eingabeverwaltung.Parser
public void ExitSub([NotNull] ProofParser.SubContext context)
{
Coords coords = new Coords(context);
- if (LH.trees.Count != 1) throw new KontextException(coords,"Trees was Expected to have 1 Tree for Termpart, but found " + LH.trees.Count + " trees! They are: " + LH.TreeListToString(LH.trees));
string variableName = context.BEZ().GetText();
Variable variable = LH.findVariable(variableName, TS.rule.eq.variables);
Test_Substitution_Variable_isCorrect(variableName, variable,coords);
- TS.subs.Add(new Substitution(coords,variableName, variable, LH.trees[0]));
+ if (LH.trees.Count != 1)
+ {
+ LH.errors.Add(new SemanticAnalysisError(coords, "Trees was Expected to have 1 Tree for Termpart, but found " + LH.trees.Count + " trees! They are: " + LH.TreeListToString(LH.trees)));
+ TS.subs.Add(new Substitution(coords, variableName, variable, null));
+ }
+ else TS.subs.Add(new Substitution(coords, variableName, variable, LH.trees[0]));
}
public void EnterResult_tree([NotNull] ProofParser.Result_treeContext context) => LH.trees = new List<Tree>();
public void ExitResult_tree([NotNull] ProofParser.Result_treeContext context)
{
- if (LH.trees.Count != 1) throw new KontextException(new Coords(context),"Trees was Expected to have 1 Tree for ResultTree, but found " + LH.trees.Count + " trees! They are: " + LH.TreeListToString(LH.trees));
- TS.resultTree = LH.trees[0];
+ if (LH.trees.Count != 1)
+ {
+ LH.errors.Add(new SemanticAnalysisError(new Coords(context), "Trees was Expected to have 1 Tree for ResultTree, but found " + LH.trees.Count + " trees! They are: " + LH.TreeListToString(LH.trees)));
+ TS.resultTree = null;
+ }
+ else TS.resultTree = LH.trees[0];
}
// Induction
@@ -239,10 +239,10 @@ namespace Eingabeverwaltung.Parser
public void EnterInd_basis([NotNull] ProofParser.Ind_basisContext context)
{
Coords coords = new Coords(context);
- if (currentInd.GetIndBasises().Count < 1) throw new KontextException(coords,"Error: Found no Inductionbasis in the current Induction!");
+ if (currentInd.GetIndBasises().Count < 1) throw new SemanticAnalysisDeadlyError(coords,"Error: Found no Inductionbasis in the current Induction!");
else try { currentIndCase = currentInd.indCases[++currentIndCaseIndex]; }
catch(ArgumentOutOfRangeException)
- { throw new KontextException(coords,"Error: Found more Inductionbasises: "
+ { throw new SemanticAnalysisDeadlyError(coords,"Error: Found more Inductionbasises: "
+currentIndCaseIndex+" than Inductioncases in the current Induction!");
}
}
@@ -250,11 +250,11 @@ namespace Eingabeverwaltung.Parser
public void EnterInd_step([NotNull] ProofParser.Ind_stepContext context)
{
Coords coords = new Coords(context);
- if (currentInd.GetIndSteps().Count < 1) throw new KontextException(coords,"Error: Found no Inductionstep in the current Induction while entering Inductionstep!");
+ if (currentInd.GetIndSteps().Count < 1) throw new SemanticAnalysisDeadlyError(coords,"Error: Found no Inductionstep in the current Induction while entering Inductionstep!");
else try { currentIndCase = currentInd.indCases[++currentIndCaseIndex]; }
catch (ArgumentOutOfRangeException)
{
- throw new KontextException(coords,"Error: Found more Inductionbasises and Inductionsteps: "
+ throw new SemanticAnalysisDeadlyError(coords,"Error: Found more Inductionbasises and Inductionsteps: "
+ currentIndCaseIndex + " than Inductioncases in the current Induction!");
}
}
@@ -350,7 +350,7 @@ namespace Eingabeverwaltung.Parser
private void Test_Substitution_Variable_isCorrect(string variableName, Variable variable, Coords coords)
{
if (variable != null && variableName != variable.name)
- throw new KontextException(coords,"The found Variable " + variable.ToString() + " has a different name than the inputed variableName " + variableName);
+ LH.errors.Add(new SemanticAnalysisError(coords,"The found Variable " + variable.ToString() + " has a different name than the inputed variableName " + variableName));
}
}
}
diff --git a/BewerterStrukturellerInduktion/bin/Debug/netcoreapp5.0/Tests/extra/NonDeadSemErrs/0riginal.proof b/BewerterStrukturellerInduktion/bin/Debug/netcoreapp5.0/Tests/extra/NonDeadSemErrs/0riginal.proof
new file mode 100644
index 0000000..64a6995
--- /dev/null
+++ b/BewerterStrukturellerInduktion/bin/Debug/netcoreapp5.0/Tests/extra/NonDeadSemErrs/0riginal.proof
@@ -0,0 +1,46 @@
+lemma L1: forall y:Nat : plus(null,y) = y induction y
+IA: zu zeigen: plus(null,null) = null
+plus(null,null)
+ {p0, lr, plus(null,null), [null/n]}
+= null
+IH: fixed y:Nat : plus(null,y) = y
+IS: zu zeigen: fixed y:Nat : plus(null,inc(y)) = inc(y)
+plus(null,inc(y))
+ {p1, lr, plus(null,inc(y)), [null/n,y/m]}
+= inc(plus(null,y))
+ {IH, lr, plus(null,y), []}
+= inc(y)
+
+lemma L2: forall a:Nat, b:Nat : plus(inc(a),b) = inc(plus(a,b)) induction b
+IA: zu zeigen: forall a:Nat : plus(inc(a),null) = inc(plus(a,null))
+plus(inc(a),null)
+ {p0,lr,plus(inc(a),null),[inc(a)/n]}
+= inc(a)
+ {p0,rl,a,[a/n]}
+= inc(plus(a,null))
+IH: forall a:Nat : fixed b:Nat : plus(inc(a),b) = inc(plus(a,b))
+IS: zu zeigen: forall a:Nat : fixed b:Nat : plus(inc(a),inc(b)) = inc(plus(a,inc(b)))
+plus(inc(a),inc(b))
+ {p1,lr,plus(inc(a),inc(b)),[inc(a)/n,b/m]}
+= inc(plus(inc(a),b))
+ {IH,lr,plus(inc(a),b),[]}
+= inc(inc(plus(a,b)))
+ {p1,rl,inc(plus(a,b)),[a/n,b/m]}
+= inc(plus(a,inc(b)))
+
+proof
+IA: zu zeigen: forall m:Nat : plus(null,m) = plus(m,null)
+plus(null,m)
+ {L1,lr,plus(null,m),[m/y]}
+= m
+ {p0,rl,m,[m/n]}
+= plus(m,null)
+IH: fixed k:Nat : forall m:Nat : plus(k,m) = plus(m,k)
+IS: zu zeigen: forall m:Nat : fixed k:Nat : plus(inc(k),m) = plus(m,inc(k))
+plus(m,inc(k))
+ {p1,lr,plus(m,inc(k)),[m/n,k/m]}
+= inc(plus(m,k))
+ {IH,rl,plus(m,k),[]}
+= inc(plus(k,m))
+ {L2,rl,inc(plus(k,m)),[k/a,m/b]}
+= plus(inc(k),m)
\ No newline at end of file
diff --git a/BewerterStrukturellerInduktion/bin/Debug/netcoreapp5.0/Tests/extra/NonDeadSemErrs/1riginal.task b/BewerterStrukturellerInduktion/bin/Debug/netcoreapp5.0/Tests/extra/NonDeadSemErrs/1riginal.task
new file mode 100644
index 0000000..29f59b5
--- /dev/null
+++ b/BewerterStrukturellerInduktion/bin/Debug/netcoreapp5.0/Tests/extra/NonDeadSemErrs/1riginal.task
@@ -0,0 +1,8 @@
+task forall n:Nat, m:Nat : plus(n,m) = plus(m,n)
+ maxpt 6 minsteps 6 maxsteps 9
+
+proof lemmata
+ L1: forall m:Nat : plus(null,m) = m
+ maxpt 4 minsteps 4 maxsteps 6
+ L2: forall n:Nat, m:Nat : plus(inc(n),m) = inc(plus(n,m))
+ maxpt 6 minsteps 6 maxsteps 9
diff --git a/BewerterStrukturellerInduktion/bin/Debug/netcoreapp5.0/Tests/extra/NonDeadSemErrs/axiom.proof b/BewerterStrukturellerInduktion/bin/Debug/netcoreapp5.0/Tests/extra/NonDeadSemErrs/axiom.proof
new file mode 100644
index 0000000..fa67982
--- /dev/null
+++ b/BewerterStrukturellerInduktion/bin/Debug/netcoreapp5.0/Tests/extra/NonDeadSemErrs/axiom.proof
@@ -0,0 +1,46 @@
+lemma L1: forall y:Nat : plus(null,y) = y induction y
+IA: zu zeigen: plus(null,null) = null
+plus(null,null)
+ {bla0, lr, plus(null,null), [null/n]} // unknown axiom
+= null
+IH: fixed y:Nat : plus(null,y) = y
+IS: zu zeigen: fixed y:Nat : plus(null,inc(y)) = inc(y)
+plus(null,inc(y))
+ {p1, lr, plus(null,inc(y)), [null/n,y/m]}
+= inc(plus(null,y))
+ {IH, lr, plus(null,y), []}
+= inc(y)
+
+lemma L2: forall a:Nat, b:Nat : plus(inc(a),b) = inc(plus(a,b)) induction b
+IA: zu zeigen: forall a:Nat : plus(inc(a),null) = inc(plus(a,null))
+plus(inc(a),null)
+ {p0,lr,plus(inc(a),null),[inc(a)/n]}
+= inc(a)
+ {p0,rl,a,[a/n]}
+= inc(plus(a,null))
+IH: forall a:Nat : fixed b:Nat : plus(inc(a),b) = inc(plus(a,b))
+IS: zu zeigen: forall a:Nat : fixed b:Nat : plus(inc(a),inc(b)) = inc(plus(a,inc(b)))
+plus(inc(a),inc(b))
+ {p1,lr,plus(inc(a),inc(b)),[inc(a)/n,b/m]}
+= inc(plus(inc(a),b))
+ {IH,lr,plus(inc(a),b),[]}
+= inc(inc(plus(a,b)))
+ {p1,rl,inc(plus(a,b)),[a/n,b/m]}
+= inc(plus(a,inc(b)))
+
+proof
+IA: zu zeigen: forall m:Nat : plus(null,m) = plus(m,null)
+plus(null,m)
+ {L1,lr,plus(null,m),[m/y]}
+= m
+ {p0,rl,m,[m/n]}
+= plus(m,null)
+IH: fixed k:Nat : forall m:Nat : plus(k,m) = plus(m,k)
+IS: zu zeigen: forall m:Nat : fixed k:Nat : plus(inc(k),m) = plus(m,inc(k))
+plus(m,inc(k))
+ {p1,lr,plus(m,inc(k)),[m/n,k/m]}
+= inc(plus(m,k))
+ {IH,rl,plus(m,k),[]}
+= inc(plus(k,m))
+ {L2,rl,inc(plus(k,m)),[k/a,m/b]}
+= plus(inc(k),m)
\ No newline at end of file
diff --git a/BewerterStrukturellerInduktion/bin/Debug/netcoreapp5.0/Tests/extra/NonDeadSemErrs/direction.proof b/BewerterStrukturellerInduktion/bin/Debug/netcoreapp5.0/Tests/extra/NonDeadSemErrs/direction.proof
new file mode 100644
index 0000000..5610fb6
--- /dev/null
+++ b/BewerterStrukturellerInduktion/bin/Debug/netcoreapp5.0/Tests/extra/NonDeadSemErrs/direction.proof
@@ -0,0 +1,46 @@
+lemma L1: forall y:Nat : plus(null,y) = y induction y
+IA: zu zeigen: plus(null,null) = null
+plus(null,null)
+ {p0, leftright, plus(null,null), [null/n]} // unknown direction
+= null
+IH: fixed y:Nat : plus(null,y) = y
+IS: zu zeigen: fixed y:Nat : plus(null,inc(y)) = inc(y)
+plus(null,inc(y))
+ {p1, lr, plus(null,inc(y)), [null/n,y/m]}
+= inc(plus(null,y))
+ {IH, lr, plus(null,y), []}
+= inc(y)
+
+lemma L2: forall a:Nat, b:Nat : plus(inc(a),b) = inc(plus(a,b)) induction b
+IA: zu zeigen: forall a:Nat : plus(inc(a),null) = inc(plus(a,null))
+plus(inc(a),null)
+ {p0,lr,plus(inc(a),null),[inc(a)/n]}
+= inc(a)
+ {p0,rl,a,[a/n]}
+= inc(plus(a,null))
+IH: forall a:Nat : fixed b:Nat : plus(inc(a),b) = inc(plus(a,b))
+IS: zu zeigen: forall a:Nat : fixed b:Nat : plus(inc(a),inc(b)) = inc(plus(a,inc(b)))
+plus(inc(a),inc(b))
+ {p1,lr,plus(inc(a),inc(b)),[inc(a)/n,b/m]}
+= inc(plus(inc(a),b))
+ {IH,lr,plus(inc(a),b),[]}
+= inc(inc(plus(a,b)))
+ {p1,rl,inc(plus(a,b)),[a/n,b/m]}
+= inc(plus(a,inc(b)))
+
+proof
+IA: zu zeigen: forall m:Nat : plus(null,m) = plus(m,null)
+plus(null,m)
+ {L1,lr,plus(null,m),[m/y]}
+= m
+ {p0,rl,m,[m/n]}
+= plus(m,null)
+IH: fixed k:Nat : forall m:Nat : plus(k,m) = plus(m,k)
+IS: zu zeigen: forall m:Nat : fixed k:Nat : plus(inc(k),m) = plus(m,inc(k))
+plus(m,inc(k))
+ {p1,lr,plus(m,inc(k)),[m/n,k/m]}
+= inc(plus(m,k))
+ {IH,rl,plus(m,k),[]}
+= inc(plus(k,m))
+ {L2,rl,inc(plus(k,m)),[k/a,m/b]}
+= plus(inc(k),m)
\ No newline at end of file
diff --git a/BewerterStrukturellerInduktion/bin/Debug/netcoreapp5.0/Tests/extra/NonDeadSemErrs/indvar1.proof b/BewerterStrukturellerInduktion/bin/Debug/netcoreapp5.0/Tests/extra/NonDeadSemErrs/indvar1.proof
new file mode 100644
index 0000000..53d48ff
--- /dev/null
+++ b/BewerterStrukturellerInduktion/bin/Debug/netcoreapp5.0/Tests/extra/NonDeadSemErrs/indvar1.proof
@@ -0,0 +1,47 @@
+// no ind vars: neither in task, nor in proof
+lemma L1: forall y:Nat : plus(null,y) = y
+IA: zu zeigen: plus(null,null) = null
+plus(null,null)
+ {p0, lr, plus(null,null), [null/n]}
+= null
+IH: fixed y:Nat : plus(null,y) = y
+IS: zu zeigen: fixed y:Nat : plus(null,inc(y)) = inc(y)
+plus(null,inc(y))
+ {p1, lr, plus(null,inc(y)), [null/n,y/m]}
+= inc(plus(null,y))
+ {IH, lr, plus(null,y), []}
+= inc(y)
+
+lemma L2: forall a:Nat, b:Nat : plus(inc(a),b) = inc(plus(a,b))
+IA: zu zeigen: forall a:Nat : plus(inc(a),null) = inc(plus(a,null))
+plus(inc(a),null)
+ {p0,lr,plus(inc(a),null),[inc(a)/n]}
+= inc(a)
+ {p0,rl,a,[a/n]}
+= inc(plus(a,null))
+IH: forall a:Nat : fixed b:Nat : plus(inc(a),b) = inc(plus(a,b))
+IS: zu zeigen: forall a:Nat : fixed b:Nat : plus(inc(a),inc(b)) = inc(plus(a,inc(b)))
+plus(inc(a),inc(b))
+ {p1,lr,plus(inc(a),inc(b)),[inc(a)/n,b/m]}
+= inc(plus(inc(a),b))
+ {IH,lr,plus(inc(a),b),[]}
+= inc(inc(plus(a,b)))
+ {p1,rl,inc(plus(a,b)),[a/n,b/m]}
+= inc(plus(a,inc(b)))
+
+proof
+IA: zu zeigen: forall m:Nat : plus(null,m) = plus(m,null)
+plus(null,m)
+ {L1,lr,plus(null,m),[m/y]}
+= m
+ {p0,rl,m,[m/n]}
+= plus(m,null)
+IH: fixed k:Nat : forall m:Nat : plus(k,m) = plus(m,k)
+IS: zu zeigen: forall m:Nat : fixed k:Nat : plus(inc(k),m) = plus(m,inc(k))
+plus(m,inc(k))
+ {p1,lr,plus(m,inc(k)),[m/n,k/m]}
+= inc(plus(m,k))
+ {IH,rl,plus(m,k),[]}
+= inc(plus(k,m))
+ {L2,rl,inc(plus(k,m)),[k/a,m/b]}
+= plus(inc(k),m)
\ No newline at end of file
diff --git a/BewerterStrukturellerInduktion/bin/Debug/netcoreapp5.0/Tests/extra/NonDeadSemErrs/indvar2.proof b/BewerterStrukturellerInduktion/bin/Debug/netcoreapp5.0/Tests/extra/NonDeadSemErrs/indvar2.proof
new file mode 100644
index 0000000..3be4ccd
--- /dev/null
+++ b/BewerterStrukturellerInduktion/bin/Debug/netcoreapp5.0/Tests/extra/NonDeadSemErrs/indvar2.proof
@@ -0,0 +1,48 @@
+// induction variable that is not in equation, but in adt
+lemma L1: forall y:Nat : plus(null,y) = y induction n
+IA: zu zeigen: plus(null,null) = null
+plus(null,null)
+ {p0, lr, plus(null,null), [null/n]}
+= null
+IH: fixed y:Nat : plus(null,y) = y
+IS: zu zeigen: fixed y:Nat : plus(null,inc(y)) = inc(y)
+plus(null,inc(y))
+ {p1, lr, plus(null,inc(y)), [null/n,y/m]}
+= inc(plus(null,y))
+ {IH, lr, plus(null,y), []}
+= inc(y)
+
+// induction variable that is neither in equation nor in adt
+lemma L2: forall a:Nat, b:Nat : plus(inc(a),b) = inc(plus(a,b)) induction x
+IA: zu zeigen: forall a:Nat : plus(inc(a),null) = inc(plus(a,null))
+plus(inc(a),null)
+ {p0,lr,plus(inc(a),null),[inc(a)/n]}
+= inc(a)
+ {p0,rl,a,[a/n]}
+= inc(plus(a,null))
+IH: forall a:Nat : fixed b:Nat : plus(inc(a),b) = inc(plus(a,b))
+IS: zu zeigen: forall a:Nat : fixed b:Nat : plus(inc(a),inc(b)) = inc(plus(a,inc(b)))
+plus(inc(a),inc(b))
+ {p1,lr,plus(inc(a),inc(b)),[inc(a)/n,b/m]}
+= inc(plus(inc(a),b))
+ {IH,lr,plus(inc(a),b),[]}
+= inc(inc(plus(a,b)))
+ {p1,rl,inc(plus(a,b)),[a/n,b/m]}
+= inc(plus(a,inc(b)))
+
+proof
+IA: zu zeigen: forall m:Nat : plus(null,m) = plus(m,null)
+plus(null,m)
+ {L1,lr,plus(null,m),[m/y]}
+= m
+ {p0,rl,m,[m/n]}
+= plus(m,null)
+IH: fixed k:Nat : forall m:Nat : plus(k,m) = plus(m,k)
+IS: zu zeigen: forall m:Nat : fixed k:Nat : plus(inc(k),m) = plus(m,inc(k))
+plus(m,inc(k))
+ {p1,lr,plus(m,inc(k)),[m/n,k/m]}
+= inc(plus(m,k))
+ {IH,rl,plus(m,k),[]}
+= inc(plus(k,m))
+ {L2,rl,inc(plus(k,m)),[k/a,m/b]}
+= plus(inc(k),m)
\ No newline at end of file
diff --git a/BewerterStrukturellerInduktion/bin/Debug/netcoreapp5.0/Tests/extra/NonDeadSemErrs/resulttree.proof b/BewerterStrukturellerInduktion/bin/Debug/netcoreapp5.0/Tests/extra/NonDeadSemErrs/resulttree.proof
new file mode 100644
index 0000000..f9e686b
--- /dev/null
+++ b/BewerterStrukturellerInduktion/bin/Debug/netcoreapp5.0/Tests/extra/NonDeadSemErrs/resulttree.proof
@@ -0,0 +1,46 @@
+lemma L1: forall y:Nat : plus(null,y) = y induction y
+IA: zu zeigen: plus(null,null) = null
+plus(null,null)
+ {p0, lr, plus(null,null), [null/n]}
+= null null // two result trees
+IH: fixed y:Nat : plus(null,y) = y
+IS: zu zeigen: fixed y:Nat : plus(null,inc(y)) = inc(y)
+plus(null,inc(y))
+ {p1, lr, plus(null,inc(y)), [null/n,y/m]}
+= inc(plus(null,y))
+ {IH, lr, plus(null,y), []}
+= // no result tree
+
+lemma L2: forall a:Nat, b:Nat : plus(inc(a),b) = inc(plus(a,b)) induction b
+IA: zu zeigen: forall a:Nat : plus(inc(a),null) = inc(plus(a,null))
+plus(inc(a),null)
+ {p0,lr,plus(inc(a),null),[inc(a)/n]}
+= inc(a)
+ {p0,rl,a,[a/n]}
+= inc(plus(a,null))
+IH: forall a:Nat : fixed b:Nat : plus(inc(a),b) = inc(plus(a,b))
+IS: zu zeigen: forall a:Nat : fixed b:Nat : plus(inc(a),inc(b)) = inc(plus(a,inc(b)))
+plus(inc(a),inc(b))
+ {p1,lr,plus(inc(a),inc(b)),[inc(a)/n,b/m]}
+= inc(plus(inc(a),b))
+ {IH,lr,plus(inc(a),b),[]}
+= inc(inc(plus(a,b)))
+ {p1,rl,inc(plus(a,b)),[a/n,b/m]}
+= inc(plus(a,inc(b)))
+
+proof
+IA: zu zeigen: forall m:Nat : plus(null,m) = plus(m,null)
+plus(null,m)
+ {L1,lr,plus(null,m),[m/y]}
+= m
+ {p0,rl,m,[m/n]}
+= plus(m,null)
+IH: fixed k:Nat : forall m:Nat : plus(k,m) = plus(m,k)
+IS: zu zeigen: forall m:Nat : fixed k:Nat : plus(inc(k),m) = plus(m,inc(k))
+plus(m,inc(k))
+ {p1,lr,plus(m,inc(k)),[m/n,k/m]}
+= inc(plus(m,k))
+ {IH,rl,plus(m,k),[]}
+= inc(plus(k,m))
+ {L2,rl,inc(plus(k,m)),[k/a,m/b]}
+= plus(inc(k),m)
\ No newline at end of file
diff --git a/BewerterStrukturellerInduktion/bin/Debug/netcoreapp5.0/Tests/extra/NonDeadSemErrs/starttree.proof b/BewerterStrukturellerInduktion/bin/Debug/netcoreapp5.0/Tests/extra/NonDeadSemErrs/starttree.proof
new file mode 100644
index 0000000..5bef015
--- /dev/null
+++ b/BewerterStrukturellerInduktion/bin/Debug/netcoreapp5.0/Tests/extra/NonDeadSemErrs/starttree.proof
@@ -0,0 +1,45 @@
+lemma L1: forall y:Nat : plus(null,y) = y induction y
+IA: zu zeigen: plus(null,null) = null
+ {p0, lr, plus(null,null), [null/n]} // missing starttree
+= null
+IH: fixed y:Nat : plus(null,y) = y
+IS: zu zeigen: fixed y:Nat : plus(null,inc(y)) = inc(y)
+plus(null,inc(y)) plus(null,null) // two starttrees
+ {p1, lr, plus(null,inc(y)), [null/n,y/m]}
+= inc(plus(null,y))
+ {IH, lr, plus(null,y), []}
+= inc(y)
+
+lemma L2: forall a:Nat, b:Nat : plus(inc(a),b) = inc(plus(a,b)) induction b
+IA: zu zeigen: forall a:Nat : plus(inc(a),null) = inc(plus(a,null))
+plus(inc(a),null)
+ {p0,lr,plus(inc(a),null),[inc(a)/n]}
+= inc(a)
+ {p0,rl,a,[a/n]}
+= inc(plus(a,null))
+IH: forall a:Nat : fixed b:Nat : plus(inc(a),b) = inc(plus(a,b))
+IS: zu zeigen: forall a:Nat : fixed b:Nat : plus(inc(a),inc(b)) = inc(plus(a,inc(b)))
+plus(inc(a),inc(b))
+ {p1,lr,plus(inc(a),inc(b)),[inc(a)/n,b/m]}
+= inc(plus(inc(a),b))
+ {IH,lr,plus(inc(a),b),[]}
+= inc(inc(plus(a,b)))
+ {p1,rl,inc(plus(a,b)),[a/n,b/m]}
+= inc(plus(a,inc(b)))
+
+proof
+IA: zu zeigen: forall m:Nat : plus(null,m) = plus(m,null)
+plus(null,m)
+ {L1,lr,plus(null,m),[m/y]}
+= m
+ {p0,rl,m,[m/n]}
+= plus(m,null)
+IH: fixed k:Nat : forall m:Nat : plus(k,m) = plus(m,k)
+IS: zu zeigen: forall m:Nat : fixed k:Nat : plus(inc(k),m) = plus(m,inc(k))
+plus(m,inc(k))
+ {p1,lr,plus(m,inc(k)),[m/n,k/m]}
+= inc(plus(m,k))
+ {IH,rl,plus(m,k),[]}
+= inc(plus(k,m))
+ {L2,rl,inc(plus(k,m)),[k/a,m/b]}
+= plus(inc(k),m)
\ No newline at end of file
diff --git a/BewerterStrukturellerInduktion/bin/Debug/netcoreapp5.0/Tests/extra/NonDeadSemErrs/substitution1.proof b/BewerterStrukturellerInduktion/bin/Debug/netcoreapp5.0/Tests/extra/NonDeadSemErrs/substitution1.proof
new file mode 100644
index 0000000..358a11d
--- /dev/null
+++ b/BewerterStrukturellerInduktion/bin/Debug/netcoreapp5.0/Tests/extra/NonDeadSemErrs/substitution1.proof
@@ -0,0 +1,46 @@
+lemma L1: forall y:Nat : plus(null,y) = y induction y
+IA: zu zeigen: plus(null,null) = null
+plus(null,null)
+ {p0, lr, plus(null,null), [/n]} // 0 trees in sub
+= null
+IH: fixed y:Nat : plus(null,y) = y
+IS: zu zeigen: fixed y:Nat : plus(null,inc(y)) = inc(y)
+plus(null,inc(y))
+ {p1, lr, plus(null,inc(y)), [null null/n,y/m]} // two trees in sub
+= inc(plus(null,y))
+ {IH, lr, plus(null,y), []}
+= inc(y)
+
+lemma L2: forall a:Nat, b:Nat : plus(inc(a),b) = inc(plus(a,b)) induction b
+IA: zu zeigen: forall a:Nat : plus(inc(a),null) = inc(plus(a,null))
+plus(inc(a),null)
+ {p0,lr,plus(inc(a),null),[inc(a)/n]}
+= inc(a)
+ {p0,rl,a,[a/n]}
+= inc(plus(a,null))
+IH: forall a:Nat : fixed b:Nat : plus(inc(a),b) = inc(plus(a,b))
+IS: zu zeigen: forall a:Nat : fixed b:Nat : plus(inc(a),inc(b)) = inc(plus(a,inc(b)))
+plus(inc(a),inc(b))
+ {p1,lr,plus(inc(a),inc(b)),[inc(a)/n,b/m]}
+= inc(plus(inc(a),b))
+ {IH,lr,plus(inc(a),b),[]}
+= inc(inc(plus(a,b)))
+ {p1,rl,inc(plus(a,b)),[a/n,b/m]}
+= inc(plus(a,inc(b)))
+
+proof
+IA: zu zeigen: forall m:Nat : plus(null,m) = plus(m,null)
+plus(null,m)
+ {L1,lr,plus(null,m),[m/y]}
+= m
+ {p0,rl,m,[m/n]}
+= plus(m,null)
+IH: fixed k:Nat : forall m:Nat : plus(k,m) = plus(m,k)
+IS: zu zeigen: forall m:Nat : fixed k:Nat : plus(inc(k),m) = plus(m,inc(k))
+plus(m,inc(k))
+ {p1,lr,plus(m,inc(k)),[m/n,k/m]}
+= inc(plus(m,k))
+ {IH,rl,plus(m,k),[]}
+= inc(plus(k,m))
+ {L2,rl,inc(plus(k,m)),[k/a,m/b]}
+= plus(inc(k),m)
\ No newline at end of file
diff --git a/BewerterStrukturellerInduktion/bin/Debug/netcoreapp5.0/Tests/extra/NonDeadSemErrs/substitution2.proof b/BewerterStrukturellerInduktion/bin/Debug/netcoreapp5.0/Tests/extra/NonDeadSemErrs/substitution2.proof
new file mode 100644
index 0000000..94e76ff
--- /dev/null
+++ b/BewerterStrukturellerInduktion/bin/Debug/netcoreapp5.0/Tests/extra/NonDeadSemErrs/substitution2.proof
@@ -0,0 +1,46 @@
+lemma L1: forall y:Nat : plus(null,y) = y induction y
+IA: zu zeigen: plus(null,null) = null
+plus(null,null)
+ {p0, lr, plus(null,null), [null/x]} // unknown variable in substitution
+= null
+IH: fixed y:Nat : plus(null,y) = y
+IS: zu zeigen: fixed y:Nat : plus(null,inc(y)) = inc(y)
+plus(null,inc(y))
+ {p1, lr, plus(null,inc(y)), [null/n,y/m]}
+= inc(plus(null,y))
+ {IH, lr, plus(null,y), []}
+= inc(y)
+
+lemma L2: forall a:Nat, b:Nat : plus(inc(a),b) = inc(plus(a,b)) induction b
+IA: zu zeigen: forall a:Nat : plus(inc(a),null) = inc(plus(a,null))
+plus(inc(a),null)
+ {p0,lr,plus(inc(a),null),[inc(a)/n]}
+= inc(a)
+ {p0,rl,a,[a/n]}
+= inc(plus(a,null))
+IH: forall a:Nat : fixed b:Nat : plus(inc(a),b) = inc(plus(a,b))
+IS: zu zeigen: forall a:Nat : fixed b:Nat : plus(inc(a),inc(b)) = inc(plus(a,inc(b)))
+plus(inc(a),inc(b))
+ {p1,lr,plus(inc(a),inc(b)),[inc(a)/n,b/m]}
+= inc(plus(inc(a),b))
+ {IH,lr,plus(inc(a),b),[]}
+= inc(inc(plus(a,b)))
+ {p1,rl,inc(plus(a,b)),[a/n,b/m]}
+= inc(plus(a,inc(b)))
+
+proof
+IA: zu zeigen: forall m:Nat : plus(null,m) = plus(m,null)
+plus(null,m)
+ {L1,lr,plus(null,m),[m/y]}
+= m
+ {p0,rl,m,[m/n]}
+= plus(m,null)
+IH: fixed k:Nat : forall m:Nat : plus(k,m) = plus(m,k)
+IS: zu zeigen: forall m:Nat : fixed k:Nat : plus(inc(k),m) = plus(m,inc(k))
+plus(m,inc(k))
+ {p1,lr,plus(m,inc(k)),[m/n,k/m]}
+= inc(plus(m,k))
+ {IH,rl,plus(m,k),[]}
+= inc(plus(k,m))
+ {L2,rl,inc(plus(k,m)),[k/a,m/b]}
+= plus(inc(k),m)
\ No newline at end of file
diff --git a/BewerterStrukturellerInduktion/bin/Debug/netcoreapp5.0/Tests/extra/NonDeadSemErrs/termpart.proof b/BewerterStrukturellerInduktion/bin/Debug/netcoreapp5.0/Tests/extra/NonDeadSemErrs/termpart.proof
new file mode 100644
index 0000000..c643c2e
--- /dev/null
+++ b/BewerterStrukturellerInduktion/bin/Debug/netcoreapp5.0/Tests/extra/NonDeadSemErrs/termpart.proof
@@ -0,0 +1,46 @@
+lemma L1: forall y:Nat : plus(null,y) = y induction y
+IA: zu zeigen: plus(null,null) = null
+plus(null,null)
+ {p0, lr, , [null/n]} // no term part
+= null
+IH: fixed y:Nat : plus(null,y) = y
+IS: zu zeigen: fixed y:Nat : plus(null,inc(y)) = inc(y)
+plus(null,inc(y))
+ {p1, lr, plus(null,inc(y)) plus(null,null), [null/n,y/m]} // two term parts
+= inc(plus(null,y))
+ {IH, lr, plus(null,y), []}
+= inc(y)
+
+lemma L2: forall a:Nat, b:Nat : plus(inc(a),b) = inc(plus(a,b)) induction b
+IA: zu zeigen: forall a:Nat : plus(inc(a),null) = inc(plus(a,null))
+plus(inc(a),null)
+ {p0,lr,plus(inc(a),null),[inc(a)/n]}
+= inc(a)
+ {p0,rl,a,[a/n]}
+= inc(plus(a,null))
+IH: forall a:Nat : fixed b:Nat : plus(inc(a),b) = inc(plus(a,b))
+IS: zu zeigen: forall a:Nat : fixed b:Nat : plus(inc(a),inc(b)) = inc(plus(a,inc(b)))
+plus(inc(a),inc(b))
+ {p1,lr,plus(inc(a),inc(b)),[inc(a)/n,b/m]}
+= inc(plus(inc(a),b))
+ {IH,lr,plus(inc(a),b),[]}
+= inc(inc(plus(a,b)))
+ {p1,rl,inc(plus(a,b)),[a/n,b/m]}
+= inc(plus(a,inc(b)))
+
+proof
+IA: zu zeigen: forall m:Nat : plus(null,m) = plus(m,null)
+plus(null,m)
+ {L1,lr,plus(null,m),[m/y]}
+= m
+ {p0,rl,m,[m/n]}
+= plus(m,null)
+IH: fixed k:Nat : forall m:Nat : plus(k,m) = plus(m,k)
+IS: zu zeigen: forall m:Nat : fixed k:Nat : plus(inc(k),m) = plus(m,inc(k))
+plus(m,inc(k))
+ {p1,lr,plus(m,inc(k)),[m/n,k/m]}
+= inc(plus(m,k))
+ {IH,rl,plus(m,k),[]}
+= inc(plus(k,m))
+ {L2,rl,inc(plus(k,m)),[k/a,m/b]}
+= plus(inc(k),m)
\ No newline at end of file
diff --git a/BewerterStrukturellerInduktion/bin/Debug/netcoreapp5.0/Tests/extra/NonDeadSemErrs/transformation.proof b/BewerterStrukturellerInduktion/bin/Debug/netcoreapp5.0/Tests/extra/NonDeadSemErrs/transformation.proof
new file mode 100644
index 0000000..3ea70c1
--- /dev/null
+++ b/BewerterStrukturellerInduktion/bin/Debug/netcoreapp5.0/Tests/extra/NonDeadSemErrs/transformation.proof
@@ -0,0 +1,39 @@
+lemma L1: forall y:Nat : plus(null,y) = y induction y
+IA: zu zeigen: plus(null,null) = null // No transformationsteps
+IH: fixed y:Nat : plus(null,y) = y
+IS: zu zeigen: fixed y:Nat : plus(null,inc(y)) = inc(y)
+plus(null,inc(y)) // only startTree
+
+lemma L2: forall a:Nat, b:Nat : plus(inc(a),b) = inc(plus(a,b)) induction b
+IA: zu zeigen: forall a:Nat : plus(inc(a),null) = inc(plus(a,null))
+plus(inc(a),null)
+ {p0,lr,plus(inc(a),null),[inc(a)/n]}
+= inc(a)
+ {p0,rl,a,[a/n]}
+= inc(plus(a,null))
+IH: forall a:Nat : fixed b:Nat : plus(inc(a),b) = inc(plus(a,b))
+IS: zu zeigen: forall a:Nat : fixed b:Nat : plus(inc(a),inc(b)) = inc(plus(a,inc(b)))
+plus(inc(a),inc(b))
+ {p1,lr,plus(inc(a),inc(b)),[inc(a)/n,b/m]}
+= inc(plus(inc(a),b))
+ {IH,lr,plus(inc(a),b),[]}
+= inc(inc(plus(a,b)))
+ {p1,rl,inc(plus(a,b)),[a/n,b/m]}
+= inc(plus(a,inc(b)))
+
+proof
+IA: zu zeigen: forall m:Nat : plus(null,m) = plus(m,null)
+plus(null,m)
+ {L1,lr,plus(null,m),[m/y]}
+= m
+ {p0,rl,m,[m/n]}
+= plus(m,null)
+IH: fixed k:Nat : forall m:Nat : plus(k,m) = plus(m,k)
+IS: zu zeigen: forall m:Nat : fixed k:Nat : plus(inc(k),m) = plus(m,inc(k))
+plus(m,inc(k))
+ {p1,lr,plus(m,inc(k)),[m/n,k/m]}
+= inc(plus(m,k))
+ {IH,rl,plus(m,k),[]}
+= inc(plus(k,m))
+ {L2,rl,inc(plus(k,m)),[k/a,m/b]}
+= plus(inc(k),m)
\ No newline at end of file
--
GitLab