BewerterStrukturellerInduktion/bin/Debug/netcoreapp5.0/Tests/extra/NonDeadSemErrs/0riginal.adt

+name Peano
+sorts Nat
+constructors null: Nat
+             inc: Nat -> Nat 
+operations plus: Nat >< Nat -> Nat
+           mal:  Nat >< Nat -> Nat
+vars n : Nat, m : Nat
+axioms p0: plus(n,null) = n
+       p1: plus(n,inc(m)) = inc(plus(n,m))
+       m0: mal(n,null) = null
+       m1: mal(n,inc(m)) = plus(mal(n,m),n)
\ No newline at end of file

BewerterStrukturellerInduktion/bin/Debug/netcoreapp5.0/Tests/extra/NonDeadSemErrs/0riginal.proof

+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 induction n
+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

BewerterStrukturellerInduktion/bin/Debug/netcoreapp5.0/Tests/extra/NonDeadSemErrs/0riginal.task

+task forall n:Nat, m:Nat : plus(n,m) = plus(m,n)
+  induction n
+    case null maxpt 2 minsteps 2 maxsteps 3
+    case inc maxpt 3 minsteps 3 maxsteps 5
+    IH maxpt 1
+
+proof lemmata 
+  L1: forall m:Nat : plus(null,m) = m
+    induction m
+      case null maxpt 1 minsteps 1 maxsteps 2
+      case inc maxpt 2 minsteps 2 maxsteps 3
+      IH maxpt 1
+  L2: forall n:Nat, m:Nat : plus(inc(n),m) = inc(plus(n,m))
+    induction m
+      case null maxpt 2 minsteps 2 maxsteps 3
+      case inc maxpt 3 minsteps 3 maxsteps 5
+      IH maxpt 1

BewerterStrukturellerInduktion/bin/Debug/netcoreapp5.0/Tests/extra/NonDeadSemErrs/1riginal.adt

+name Peano
+sorts Nat, Nat2
+constructors null: Nat
+             inc: Nat -> Nat
+             null2: Nat2
+             inc2: Nat2 -> Nat2 
+operations plus: Nat >< Nat -> Nat
+           mal:  Nat >< Nat -> Nat
+           plus2: Nat2 >< Nat2 -> Nat2
+           mal2:  Nat2 >< Nat2 -> Nat2
+vars n : Nat, m : Nat
+axioms p0: plus(n,null) = n
+       p1: plus(n,inc(m)) = inc(plus(n,m))
+       m0: mal(n,null) = null
+       m1: mal(n,inc(m)) = plus(mal(n,m),n)
\ No newline at end of file

BewerterStrukturellerInduktion/bin/Debug/netcoreapp5.0/Tests/extra/NonDeadSemErrs/1riginal.task

+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

BewerterStrukturellerInduktion/bin/Debug/netcoreapp5.0/Tests/extra/NonDeadSemErrs/ax.adt

+name Peano
+sorts Nat
+constructors null: Nat
+             inc: Nat -> Nat 
+operations plus: Nat >< Nat -> Nat
+           mal:  Nat >< Nat -> Nat
+vars n : Nat, m : Nat
+axioms p0: plus(n,null) = n
+       p0: plus(n,inc(m)) = inc(plus(n,m))
+       m0: mal(n,null) = null
+       m1: mal(n,inc(m)) = plus(mal(n,m),n)
\ No newline at end of file

BewerterStrukturellerInduktion/bin/Debug/netcoreapp5.0/Tests/extra/NonDeadSemErrs/axiom.proof

+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 induction n
+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

BewerterStrukturellerInduktion/bin/Debug/netcoreapp5.0/Tests/extra/NonDeadSemErrs/chaos.adt

+name Peano_AllErrorsTogether
+// sorts with building and without basic constructors
+// multiple sorts with same name
+sorts Nat, Nat
+constructors inc: Blub -> Nat 
+// multiple operations with same name
+// operation has sorts undefined in adt
+operations plus: Nat1 >< Nat2 -> Blub
+           plus: Nat 
+           mal:  Blub >< Nat3 -> Nat4
+// variable has sorts undefined in adt
+// multiple variables defined with same name
+vars n : Bla, m : Nat5, n: Bla2
+// Equation with wrong sorts
+// Trees with wrong sorts
+axioms p0: plus(n,null) = n
+       p1: plus(n,inc(m)) = inc(plus(n,m))
+       m0: mal(n,null) = null
+       m1: mal(n,inc(m)) = plus(mal(n,m),n)
\ No newline at end of file

BewerterStrukturellerInduktion/bin/Debug/netcoreapp5.0/Tests/extra/NonDeadSemErrs/direction.proof

+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 induction n
+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

BewerterStrukturellerInduktion/bin/Debug/netcoreapp5.0/Tests/extra/NonDeadSemErrs/indvar1.proof

+// 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

BewerterStrukturellerInduktion/bin/Debug/netcoreapp5.0/Tests/extra/NonDeadSemErrs/indvar2.proof

+// 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 induction n
+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

BewerterStrukturellerInduktion/bin/Debug/netcoreapp5.0/Tests/extra/NonDeadSemErrs/lemma.task

+task forall n:Nat, m:Nat : plus(n,m) = plus(m,n)
+  induction n
+    case null maxpt 2 minsteps 2 maxsteps 3
+    case inc maxpt 3 minsteps 3 maxsteps 5
+    IH maxpt 1
+
+proof lemmata 
+  p0: forall m:Nat : plus(null,m) = m
+    induction m
+      case null maxpt 1 minsteps 1 maxsteps 2
+      case inc maxpt 2 minsteps 2 maxsteps 3
+      IH maxpt 1
+  L2: forall n:Nat, m:Nat : plus(inc(n),m) = inc(plus(n,m))
+    induction m
+      case null maxpt 2 minsteps 2 maxsteps 3
+      case inc maxpt 3 minsteps 3 maxsteps 5
+      IH maxpt 1
+
+lemmata L2: forall n:Nat, m:Nat : plus(inc(n),m) = inc(plus(n,m))
+        L3: forall n:Nat, m:Nat : plus(inc(n),m) = inc(plus(n,m))
+        L3: forall n:Nat, m:Nat : plus(inc(n),m) = inc(plus(n,m))

BewerterStrukturellerInduktion/bin/Debug/netcoreapp5.0/Tests/extra/NonDeadSemErrs/op.adt

+name Peano
+sorts Nat
+constructors null: Nat
+             inc: Nat -> Nat 
+operations plus: Nat >< Nat -> Nat
+           mal:  Nat >< Nat -> Nat
+           null: Nat -> Nat2
+vars n : Nat, m : Nat
+axioms p0: plus(n,null) = n
+       p1: plus(n,inc(m)) = inc(plus(n,m))
+       m0: mal(n,null) = null
+       m1: mal(n,inc(m)) = plus(mal(n,m),n)
\ No newline at end of file

BewerterStrukturellerInduktion/bin/Debug/netcoreapp5.0/Tests/extra/NonDeadSemErrs/sort.adt

+name Peano
+// multiple sorts with same name
+// sort with building, but without basic constructor
+sorts Nat, Nat
+constructors inc: Nat -> Nat 
+operations plus: Nat >< Nat -> Nat
+           mal:  Nat >< Nat -> Nat
+           null: Nat
+vars n : Nat, m : Nat
+axioms p0: plus(n,null) = n
+       p1: plus(n,inc(m)) = inc(plus(n,m))
+       m0: mal(n,null) = null
+       m1: mal(n,inc(m)) = plus(mal(n,m),n)
\ No newline at end of file

BewerterStrukturellerInduktion/bin/Debug/netcoreapp5.0/Tests/extra/NonDeadSemErrs/tree1.adt

+name Peano
+sorts Nat
+constructors null: Nat
+             inc: Nat -> Nat 
+operations plus: Nat >< Nat -> Nat
+           mal:  Nat >< Nat -> Nat
+vars n : Nat, m : Nat
+// tree wrong child count
+axioms p0: plus(n) = n
+       p1: plus(n,inc(m),null) = inc(plus(n,m))
+       m0: mal(n,null) = null
+       m1: mal(n,inc(m)) = plus(mal(n,m),n)
\ No newline at end of file

BewerterStrukturellerInduktion/bin/Debug/netcoreapp5.0/Tests/extra/NonDeadSemErrs/tree1.task

+// tree wrong child count
+task forall n:Nat, m:Nat : plus(n,m,n) = plus(m,n)
+  induction n
+    case null maxpt 2 minsteps 2 maxsteps 3
+    case inc maxpt 3 minsteps 3 maxsteps 5
+    IH maxpt 1
+
+proof lemmata 
+  L1: forall m:Nat : plus(null,m) = m
+    induction m
+      case null maxpt 1 minsteps 1 maxsteps 2
+      case inc maxpt 2 minsteps 2 maxsteps 3
+      IH maxpt 1
+  L2: forall n:Nat, m:Nat : plus(inc,m) = inc(plus(m),null)
+    induction m
+      case null maxpt 2 minsteps 2 maxsteps 3
+      case inc maxpt 3 minsteps 3 maxsteps 5
+      IH maxpt 1

BewerterStrukturellerInduktion/bin/Debug/netcoreapp5.0/Tests/extra/NonDeadSemErrs/tree2.adt

+name Peano
+sorts Nat
+constructors null: Nat
+             inc: Nat -> Nat 
+operations plus: Nat >< Nat -> Nat
+           mal:  Nat >< Nat -> Nat
+vars n : Nat, m : Nat
+// composed tree names undefined in operation (deadly)
+axioms p0: plus(n,null) = n
+       p1: plus(n,ink(m)) = inc(plus(n,m)) 
+       m0: mal(n,null) = null
+       m1: mal(n,inc(m)) = plus(mal(n,m),n)
\ No newline at end of file

BewerterStrukturellerInduktion/bin/Debug/netcoreapp5.0/Tests/extra/NonDeadSemErrs/tree2.task

+// composed tree names undefined in operation (deadly)
+task forall n:Nat, m:Nat : add(n,m) = plus(m,n)
+  induction n
+    case null maxpt 2 minsteps 2 maxsteps 3
+    case inc maxpt 3 minsteps 3 maxsteps 5
+    IH maxpt 1
+
+proof lemmata 
+  L1: forall m:Nat : plus(null,m) = m
+    induction m
+      case null maxpt 1 minsteps 1 maxsteps 2
+      case inc maxpt 2 minsteps 2 maxsteps 3
+      IH maxpt 1
+  L2: forall n:Nat, m:Nat : plus(inc(n),m) = inc(plus(n,m))
+    induction m
+      case null maxpt 2 minsteps 2 maxsteps 3
+      case inc maxpt 3 minsteps 3 maxsteps 5
+      IH maxpt 1

BewerterStrukturellerInduktion/bin/Debug/netcoreapp5.0/Tests/extra/NonDeadSemErrs/tree3.adt

+name Peano
+sorts Nat
+constructors null: Nat
+             inc: Nat -> Nat 
+operations plus: Nat >< Nat -> Nat
+           mal:  Nat >< Nat -> Nat
+vars n : Nat, m : Nat
+// tree-leaf names undefined in operation or variables
+axioms p0: plus(n,zero) = k
+       p1: plus(n,inc(k)) = inc(plus(n,m))
+       m0: mal(n,null) = null
+       m1: mal(n,inc(m)) = plus(mal(n,m),n)
\ No newline at end of file

BewerterStrukturellerInduktion/bin/Debug/netcoreapp5.0/Tests/extra/NonDeadSemErrs/tree3.task

+// tree-leaf names undefined in operation or variables
+task forall n:Nat : plus(n,k) = plus(m,n)
+  induction n
+    case null maxpt 2 minsteps 2 maxsteps 3
+    case inc maxpt 3 minsteps 3 maxsteps 5
+    IH maxpt 1
+
+proof lemmata 
+  L1: forall m:Nat : plus(zero,m) = m
+    induction m
+      case null maxpt 1 minsteps 1 maxsteps 2
+      case inc maxpt 2 minsteps 2 maxsteps 3
+      IH maxpt 1
+  L2: forall n:Nat, m:Nat : plus(inc(n),m) = inc(plus(n,m))
+    induction m
+      case null maxpt 2 minsteps 2 maxsteps 3
+      case inc maxpt 3 minsteps 3 maxsteps 5
+      IH maxpt 1