From 11691f38ae62ef17898390183e370798997263f7 Mon Sep 17 00:00:00 2001
From: Edward Sabinus <edward.sabinus@informatik.uni-halle.de>
Date: Wed, 24 Apr 2024 12:00:12 +0200
Subject: [PATCH] Added tests to ExtraTest. Some test cases which violate
grammar do not work with non deadly errors, so they are deadly now. removed
test cases for errors which are now deadly. TODO: improve antlr error
reporting to not start semantic analysis if syntax analysis got errors.
---
.../Parser/Listener_Helper.cs | 2 +-
.../Parser/Proof_Listener.cs | 2 +-
.../Parser/TransformationStep_Listener.cs | 32 ++++++-------
.../Testverwaltung/ExtraTest.cs | 17 ++++++-
.../Tests/extra/NonDeadSemErrs/0riginal.proof | 2 +-
.../Tests/extra/NonDeadSemErrs/axiom.proof | 2 +-
.../extra/NonDeadSemErrs/direction.proof | 2 +-
.../Tests/extra/NonDeadSemErrs/indvar2.proof | 2 +-
.../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, 36 insertions(+), 293 deletions(-)
delete mode 100644 BewerterStrukturellerInduktion/bin/Debug/netcoreapp5.0/Tests/extra/NonDeadSemErrs/resulttree.proof
delete mode 100644 BewerterStrukturellerInduktion/bin/Debug/netcoreapp5.0/Tests/extra/NonDeadSemErrs/starttree.proof
delete mode 100644 BewerterStrukturellerInduktion/bin/Debug/netcoreapp5.0/Tests/extra/NonDeadSemErrs/substitution1.proof
delete mode 100644 BewerterStrukturellerInduktion/bin/Debug/netcoreapp5.0/Tests/extra/NonDeadSemErrs/substitution2.proof
delete mode 100644 BewerterStrukturellerInduktion/bin/Debug/netcoreapp5.0/Tests/extra/NonDeadSemErrs/termpart.proof
delete mode 100644 BewerterStrukturellerInduktion/bin/Debug/netcoreapp5.0/Tests/extra/NonDeadSemErrs/transformation.proof
diff --git a/BewerterStrukturellerInduktion/Eingabeverwaltung/Parser/Listener_Helper.cs b/BewerterStrukturellerInduktion/Eingabeverwaltung/Parser/Listener_Helper.cs
index 1e6d930..78c8c7b 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 d02698f..dec6ed1 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 b84d12c..98081be 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 93800cd..11c688d 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 64a6995..43ebe30 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 fa67982..9dd637d 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 5610fb6..368403c 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 3be4ccd..3579930 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 f9e686b..0000000
--- 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 5bef015..0000000
--- 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 358a11d..0000000
--- 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 94e76ff..0000000
--- 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 c643c2e..0000000
--- 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 3ea70c1..0000000
--- 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
--
GitLab