diff --git a/BewerterStrukturellerInduktion/Eingabeverwaltung/Parser/Listener_Helper.cs b/BewerterStrukturellerInduktion/Eingabeverwaltung/Parser/Listener_Helper.cs
index 1e6d930ee0f2fa1dd8511632c1330ea5c783254a..78c8c7bf0e78dccc43b02c2f8507714b070d1e6d 100644
--- a/BewerterStrukturellerInduktion/Eingabeverwaltung/Parser/Listener_Helper.cs
+++ b/BewerterStrukturellerInduktion/Eingabeverwaltung/Parser/Listener_Helper.cs
@@ -378,7 +378,7 @@ namespace Eingabeverwaltung.Parser
{
if (leftTree.sort.name != rightTree.sort.name)
errors.Add(new SemanticAnalysisError(coords, "The Equation has not the same Sort on its 2 sides! Sort of leftTree: " + leftTree.sort.name + " Sort of rightTree: " + rightTree.sort.name));
- }catch(NullReferenceException n) { errors.Add(new SemanticAnalysisError(coords, "One or more sides of one Equation are null!")); }
+ }catch(NullReferenceException) { errors.Add(new SemanticAnalysisError(coords, "One or more sides of one Equation are null!")); }
}
/// <summary>
diff --git a/BewerterStrukturellerInduktion/Eingabeverwaltung/Parser/Proof_Listener.cs b/BewerterStrukturellerInduktion/Eingabeverwaltung/Parser/Proof_Listener.cs
index d02698f3fb948e373fe9bcff1e0ba769c6bd6c38..dec6ed114978a7ea21b9733c16e8d2406fb712e7 100644
--- a/BewerterStrukturellerInduktion/Eingabeverwaltung/Parser/Proof_Listener.cs
+++ b/BewerterStrukturellerInduktion/Eingabeverwaltung/Parser/Proof_Listener.cs
@@ -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) 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)));
+ if (LH.trees.Count != 1) throw new SemanticAnalysisDeadlyError(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];
}
diff --git a/BewerterStrukturellerInduktion/Eingabeverwaltung/Parser/TransformationStep_Listener.cs b/BewerterStrukturellerInduktion/Eingabeverwaltung/Parser/TransformationStep_Listener.cs
index b84d12cb3811f5cadb1e83b6ea175582b74fbb50..98081be8a8a13b93e1bef85f818ba64cd172162b 100644
--- a/BewerterStrukturellerInduktion/Eingabeverwaltung/Parser/TransformationStep_Listener.cs
+++ b/BewerterStrukturellerInduktion/Eingabeverwaltung/Parser/TransformationStep_Listener.cs
@@ -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) LH.errors.Add(new SemanticAnalysisError(new Coords(context),"No TransformationSteps found in Transformation at ExitTransformation!"));
+ if (TSs.Count < 1) throw new SemanticAnalysisDeadlyError(new Coords(context),"No TransformationSteps found in Transformation at ExitTransformation!");
Tree startT = currentTR.startTree;
for (int i = 0; i < TSs.Count; i++)
{
@@ -128,6 +128,10 @@ namespace Eingabeverwaltung.Parser
{
Coords coords = new Coords(context);
Rule rule = null;
+ // begin preparation for exception case (this is for exception case to avoid NullReferenceException on reading TS.rule.eq)
+ Tree exceptionTree = new TreeVariable(new Variable("", new Sort("")));
+ Equation exeptionEquation = new Equation(exceptionTree, exceptionTree, new List<Variable>());
+ // end preparation for exception case
if (context.BEZ() != null)
{
string ruleName = context.BEZ().GetText();
@@ -151,9 +155,9 @@ namespace Eingabeverwaltung.Parser
{
rule = findRuleIn(ruleName, currentInd.indHyps.Cast<Rule>().ToList());
if (rule != null) TS.rule = rule;
- 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 { LH.errors.Add(new SemanticAnalysisError(coords, "The rule " + ruleName + " is not defined!")); TS.rule = new InductionHypothesis(coords, ruleName, exeptionEquation, new List<Variable>()); }
}
- 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 { LH.errors.Add(new SemanticAnalysisError(coords, "The rule " + ruleName + " is not defined!")); TS.rule = new InductionHypothesis(coords, ruleName, exeptionEquation, new List<Variable>()); }
}
}
}
@@ -163,7 +167,7 @@ namespace Eingabeverwaltung.Parser
{
if (currentInd != null) rule = findRuleIn("IH", currentInd.indHyps.Cast<Rule>().ToList());
if (rule != null) TS.rule = rule;
- 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>()); }
+ else { LH.errors.Add(new SemanticAnalysisError(coords,"The Inductionhypothesis is not defined for the current TransformationStep!")); TS.rule = new InductionHypothesis(coords,"IH", exeptionEquation, new List<Variable>()); }
}
}
@@ -183,8 +187,8 @@ namespace Eingabeverwaltung.Parser
public void EnterTermpart([NotNull] ProofParser.TermpartContext context) => LH.trees = new List<Tree>();
public void ExitTermpart([NotNull] ProofParser.TermpartContext context)
{
- 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];
+ if (LH.trees.Count != 1) throw new SemanticAnalysisDeadlyError(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];
LH.trees = null;
}
@@ -212,23 +216,15 @@ namespace Eingabeverwaltung.Parser
string variableName = context.BEZ().GetText();
Variable variable = LH.findVariable(variableName, TS.rule.eq.variables);
Test_Substitution_Variable_isCorrect(variableName, variable,coords);
- 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]));
+ if (LH.trees.Count != 1) throw new SemanticAnalysisDeadlyError(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, 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)
- {
- 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];
+ if (LH.trees.Count != 1) throw (new SemanticAnalysisDeadlyError(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];
}
// Induction
diff --git a/BewerterStrukturellerInduktion/Testverwaltung/ExtraTest.cs b/BewerterStrukturellerInduktion/Testverwaltung/ExtraTest.cs
index 93800cd791b78dc1eb59fc6786287f7d9e13b894..11c688d356280c6245ccb58e0c892b254e3f5c09 100644
--- a/BewerterStrukturellerInduktion/Testverwaltung/ExtraTest.cs
+++ b/BewerterStrukturellerInduktion/Testverwaltung/ExtraTest.cs
@@ -1,4 +1,5 @@
-using System;
+using Eingabeverwaltung.Metamodell;
+using System;
using System.Collections.Generic;
using Ueberpruefung;
@@ -37,6 +38,7 @@ namespace Testverwaltung
/// <param name="path"></param>
private void NonDeadSemErrsTest(string path)
{
+ // Test ADT
List<string> adtFileNames = new List<string>() { "tree1","tree2","tree3","tree4","tree5","sort","op","ax","chaos" };
List<string> adtShallValues = new List<string>()
{
@@ -52,6 +54,7 @@ namespace Testverwaltung
};
for (int i = 0; i < adtFileNames.Count; i++)
ExceptionTesting("ADT", path + adtFileNames[i]+".adt", adtShallValues[i]);
+ // Test Task
List<string> taskFileNames = new List<string>() { "tree1", "tree2", "tree3", "tree4", "tree5", "var", "lemma" };
List<string> taskShallValues = new List<string>()
{
@@ -66,6 +69,18 @@ namespace Testverwaltung
ein.Eingabe_Interface("ADT", path + "1riginal.adt");
for (int i = 0; i < taskFileNames.Count; i++)
ExceptionTesting("Task", path + taskFileNames[i] + ".task", taskShallValues[i]);
+ // Test Proof
+ List<string> proofFileNames = new List<string>() { "axiom", "direction", "indvar1", "indvar2" }; // wierd grammar errors:, "resulttree", "starttree", "substitution", "termpart", "transformation" };
+ List<string> proofShallValues = new List<string>() {
+ "Errors:\r\nError in 4:5: The rule bla0 is not defined!\r\n",
+ "Errors:\r\nError in 4:9: The Direction of the TransformationStep is undefined! Expected 'rl' or 'lr' but found \"leftright\".\r\n",
+ "Errors:\r\nError in 3:0: Induction variable of proof L1 is neither definied in proof nor in task!\r\nError in 16:0: Induction variable of proof L2 is neither definied in proof nor in task!\r\nError in 33:0: Induction variable of proof main proof is neither definied in proof nor in task!\r\n",
+ "Errors:\r\nError in 16:64: Could not find Induction variable x in current context of variables.\r\nError in 16:64: Induction variable of proof L2 is neither definied in proof nor in task!\r\n",
+ };
+ ein.Eingabe_Interface("ADT", path + "0riginal.adt");
+ ein.Eingabe_Interface("Task", path + "1riginal.task");
+ for (int i = 0; i < proofFileNames.Count; i++)
+ ExceptionTesting("Proof", path + proofFileNames[i] + ".proof", proofShallValues[i]);
}
private void ExceptionTesting(string inputType, string inputPath, string shallMessage)
diff --git a/BewerterStrukturellerInduktion/bin/Debug/netcoreapp5.0/Tests/extra/NonDeadSemErrs/0riginal.proof b/BewerterStrukturellerInduktion/bin/Debug/netcoreapp5.0/Tests/extra/NonDeadSemErrs/0riginal.proof
index 64a6995aee628216ac96123e2be02a42fef89b32..43ebe30419668835c4e0070d364e2bea0622a846 100644
--- a/BewerterStrukturellerInduktion/bin/Debug/netcoreapp5.0/Tests/extra/NonDeadSemErrs/0riginal.proof
+++ b/BewerterStrukturellerInduktion/bin/Debug/netcoreapp5.0/Tests/extra/NonDeadSemErrs/0riginal.proof
@@ -28,7 +28,7 @@ plus(inc(a),inc(b))
{p1,rl,inc(plus(a,b)),[a/n,b/m]}
= inc(plus(a,inc(b)))
-proof
+proof induction n
IA: zu zeigen: forall m:Nat : plus(null,m) = plus(m,null)
plus(null,m)
{L1,lr,plus(null,m),[m/y]}
diff --git a/BewerterStrukturellerInduktion/bin/Debug/netcoreapp5.0/Tests/extra/NonDeadSemErrs/axiom.proof b/BewerterStrukturellerInduktion/bin/Debug/netcoreapp5.0/Tests/extra/NonDeadSemErrs/axiom.proof
index fa67982650eabc9ce3014252efc2aec52a096e31..9dd637df2c5ae4e018def08a849243009e042fca 100644
--- a/BewerterStrukturellerInduktion/bin/Debug/netcoreapp5.0/Tests/extra/NonDeadSemErrs/axiom.proof
+++ b/BewerterStrukturellerInduktion/bin/Debug/netcoreapp5.0/Tests/extra/NonDeadSemErrs/axiom.proof
@@ -28,7 +28,7 @@ plus(inc(a),inc(b))
{p1,rl,inc(plus(a,b)),[a/n,b/m]}
= inc(plus(a,inc(b)))
-proof
+proof induction n
IA: zu zeigen: forall m:Nat : plus(null,m) = plus(m,null)
plus(null,m)
{L1,lr,plus(null,m),[m/y]}
diff --git a/BewerterStrukturellerInduktion/bin/Debug/netcoreapp5.0/Tests/extra/NonDeadSemErrs/direction.proof b/BewerterStrukturellerInduktion/bin/Debug/netcoreapp5.0/Tests/extra/NonDeadSemErrs/direction.proof
index 5610fb6c97a67d4d7586d401364d9b6c95be8990..368403c0be2117111761fddd726db482b99b5f4a 100644
--- a/BewerterStrukturellerInduktion/bin/Debug/netcoreapp5.0/Tests/extra/NonDeadSemErrs/direction.proof
+++ b/BewerterStrukturellerInduktion/bin/Debug/netcoreapp5.0/Tests/extra/NonDeadSemErrs/direction.proof
@@ -28,7 +28,7 @@ plus(inc(a),inc(b))
{p1,rl,inc(plus(a,b)),[a/n,b/m]}
= inc(plus(a,inc(b)))
-proof
+proof induction n
IA: zu zeigen: forall m:Nat : plus(null,m) = plus(m,null)
plus(null,m)
{L1,lr,plus(null,m),[m/y]}
diff --git a/BewerterStrukturellerInduktion/bin/Debug/netcoreapp5.0/Tests/extra/NonDeadSemErrs/indvar2.proof b/BewerterStrukturellerInduktion/bin/Debug/netcoreapp5.0/Tests/extra/NonDeadSemErrs/indvar2.proof
index 3be4ccd96b6f830d926edbb915384e5c29611e83..3579930f77464a671d38048d69f928622c071299 100644
--- a/BewerterStrukturellerInduktion/bin/Debug/netcoreapp5.0/Tests/extra/NonDeadSemErrs/indvar2.proof
+++ b/BewerterStrukturellerInduktion/bin/Debug/netcoreapp5.0/Tests/extra/NonDeadSemErrs/indvar2.proof
@@ -30,7 +30,7 @@ plus(inc(a),inc(b))
{p1,rl,inc(plus(a,b)),[a/n,b/m]}
= inc(plus(a,inc(b)))
-proof
+proof induction n
IA: zu zeigen: forall m:Nat : plus(null,m) = plus(m,null)
plus(null,m)
{L1,lr,plus(null,m),[m/y]}
diff --git a/BewerterStrukturellerInduktion/bin/Debug/netcoreapp5.0/Tests/extra/NonDeadSemErrs/resulttree.proof b/BewerterStrukturellerInduktion/bin/Debug/netcoreapp5.0/Tests/extra/NonDeadSemErrs/resulttree.proof
deleted file mode 100644
index f9e686b09c72410c3df2d630b4864f80dd3faa88..0000000000000000000000000000000000000000
--- a/BewerterStrukturellerInduktion/bin/Debug/netcoreapp5.0/Tests/extra/NonDeadSemErrs/resulttree.proof
+++ /dev/null
@@ -1,46 +0,0 @@
-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
deleted file mode 100644
index 5bef01581d93233640934dc8307fff3ce85c7334..0000000000000000000000000000000000000000
--- a/BewerterStrukturellerInduktion/bin/Debug/netcoreapp5.0/Tests/extra/NonDeadSemErrs/starttree.proof
+++ /dev/null
@@ -1,45 +0,0 @@
-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
deleted file mode 100644
index 358a11dc3df394cfdb7211ad1bcc4102e3671f7d..0000000000000000000000000000000000000000
--- a/BewerterStrukturellerInduktion/bin/Debug/netcoreapp5.0/Tests/extra/NonDeadSemErrs/substitution1.proof
+++ /dev/null
@@ -1,46 +0,0 @@
-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
deleted file mode 100644
index 94e76ff418cfd87b020bdcb7e832641658a11d35..0000000000000000000000000000000000000000
--- a/BewerterStrukturellerInduktion/bin/Debug/netcoreapp5.0/Tests/extra/NonDeadSemErrs/substitution2.proof
+++ /dev/null
@@ -1,46 +0,0 @@
-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
deleted file mode 100644
index c643c2e0dd333abe2fae0d8f4e36cc06cfc2d0fc..0000000000000000000000000000000000000000
--- a/BewerterStrukturellerInduktion/bin/Debug/netcoreapp5.0/Tests/extra/NonDeadSemErrs/termpart.proof
+++ /dev/null
@@ -1,46 +0,0 @@
-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
deleted file mode 100644
index 3ea70c1332ec5bd40493db4de1a04ad86a2c4bb0..0000000000000000000000000000000000000000
--- a/BewerterStrukturellerInduktion/bin/Debug/netcoreapp5.0/Tests/extra/NonDeadSemErrs/transformation.proof
+++ /dev/null
@@ -1,39 +0,0 @@
-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