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

+name Peano
+sorts Nat, Nat2
+constructors null: Nat
+             inc: Nat -> Nat 
+operations plus: Nat >< Nat -> Nat
+           mal:  Nat >< Nat -> Nat2
+vars n : Nat, m : Nat, k : Nat2
+// wrong sorts in trees and equation
+axioms p0: plus(k,null) = k
+       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/tree4.task

+// wrong sorts in trees and equation
+task forall n:Nat2, 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(null2,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(inc2(n),m) = inc2(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/tree5.adt

+name Peano
+sorts Nat, Nat2
+constructors null: Nat
+             inc: Nat -> Nat 
+operations plus: Nat >< Nat -> Nat
+           mal:  Nat >< Nat -> Nat
+// variable defined multiple times
+vars n : Nat, m : Nat, n : Nat2
+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/tree5.task

+// variable defined multiple times
+task forall n:Nat, m:Nat, n: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: fixed m:Nat : 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/var.task

+task forall n:Nat, m:Nat : plus(n,m) = plus(m,n)
+  induction k
+    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, n:Nat2 : plus(null,m) = m
+    induction n
+      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))
+      case null maxpt 2 minsteps 2 maxsteps 3
+      case inc maxpt 3 minsteps 3 maxsteps 5
+      IH maxpt 1