Proof checking at higher abstraction level

Replicating proof checking at the level of construction of DoubleStep based proofs.

• the checks for fully parametrized versions of steps replicate checks from SCProofChecker
• where possible, unparameterized versions defer checking by calling the parametrized versions, to centralize checking for a given proof step
• error messages have been uniformized in tone and speech patterns where spotted. I have opted for active instead of passive tones wherever applicable, "x is not y" instead of "x must be y". Previously, both existed simultaneously.
• a requirement during checking was to make sure the correct number of premises has been provided to the step. A suggestion offered was to make the step a function of arity N where N is a type parameter provided as ProofStepWithoutBotNorPrem[N]. I have not found a way to do this in Scala yet, outside of adding a require statement to the function, which in my opinion, produces a relatively unhelpful error message with respect to tracking it down. Currently, I have implemented them as part of the proof checking, and an error is raised in the same manner as a malformed proof step:

if (premises.length != 2)
        invalid(s"Two premises expected, ${premises.length} received.")

Status:

• ✔ Left propositional rules
• ✔ Right propositional rules
• ✔ Reflexivity rules
• ✔ Substitution rules
• ✔ Instantiation rules
• ❌ Printing abstracted proofs with errors (#85)

However, in the short term, this will make error reporting worse till #85 is resolved, since all the errors are expected to be reported through the tactic system. DO NOT MERGE before it is resolved or the status is accordingly updated above.

lisa-utils/src/main/scala/lisa/utils/tactics/BasicStepTactic.scala

@@ -12,13 +12,37 @@ import lisa.utils.tactics.ProofStepLib.{_, given}
 object BasicStepTactic {
 
   case object Hypothesis extends ProofStepWithoutBotNorPrem(0) {
-    def asSCProof(bot: Sequent, premises: Seq[Int], currentProof: Library#Proof): ProofStepJudgement =
-      SC.Hypothesis(bot, bot.left.intersect(bot.right).head)
+    def asSCProof(bot: Sequent, premises: Seq[Int], currentProof: Library#Proof): ProofStepJudgement = {
+      def invalid(msg: String) = ProofStepJudgement.InvalidProofStep(
+        this.asProofStepWithoutBot(premises).asProofStep(bot),
+        msg
+      )
+
+      lazy val intersectedPivot = bot.left.intersect(bot.right)
+
+      if (premises.length != 0)
+        invalid(s"No premises expected, ${premises.length} received.")
+      else if (intersectedPivot.isEmpty)
+        invalid("A formula for input to hypothesis could not be inferred from left and right side of sequent.")
+      else
+        SC.Hypothesis(bot, intersectedPivot.head)
+    }
   }
 
   case object Rewrite extends ProofStepWithoutBotNorPrem(1) {
-    def asSCProof(bot: Sequent, premises: Seq[Int], currentProof: Library#Proof): ProofStepJudgement =
-      SC.Rewrite(bot, premises(0))
+    def asSCProof(bot: Sequent, premises: Seq[Int], currentProof: Library#Proof): ProofStepJudgement = {
+      def invalid(msg: String) = ProofStepJudgement.InvalidProofStep(
+        this.asProofStepWithoutBot(premises).asProofStep(bot),
+        msg
+      )
+
+      if (premises.length != 1)
+        invalid(s"One premise expected, ${premises.length} received.")
+      else if (!SC.isSameSequent(bot, currentProof.getSequent(premises(0))))
+        invalid("The premise and the conclusion are not trivially equivalent.")
+      else
+        SC.Rewrite(bot, premises(0))
+    }
   }
 
   /**
@@ -29,30 +53,54 @@ object BasicStepTactic {
    * </pre>
    */
   case class Cut(phi: Formula) extends ProofStepWithoutBotNorPrem(2) {
-    def asSCProof(bot: Sequent, premises: Seq[Int], currentProof: Library#Proof): ProofStepJudgement =
-      SC.Cut(bot, premises(0), premises(1), phi)
+    def asSCProof(bot: Sequent, premises: Seq[Int], currentProof: Library#Proof): ProofStepJudgement = {
+      def invalid(msg: String) = ProofStepJudgement.InvalidProofStep(
+        this.asProofStepWithoutBot(premises).asProofStep(bot),
+        msg
+      )
+
+      lazy val leftSequent = currentProof.getSequent(premises(0))
+      lazy val rightSequent = currentProof.getSequent(premises(1))
+
+      if (premises.length != 2)
+        invalid(s"Two premises expected, ${premises.length} received.")
+      else if (!contains(leftSequent.right, phi))
+        invalid("Right-hand side of first premise does not contain φ as claimed.")
+      else if (!contains(rightSequent.left, phi))
+        invalid("Left-hand side of second premise does not contain φ as claimed.")
+      else if (!isSameSet(bot.left, leftSequent.left ++ rightSequent.left.filterNot(isSame(_, phi))))
+        invalid("Left-hand side of conclusion + φ is not the union of the left-hand sides of the premises.")
+      else if (!isSameSet(bot.right, leftSequent.right.filterNot(isSame(_, phi)) ++ rightSequent.right))
+        invalid("Right-hand side of conclusion + φ is not the union of the right-hand sides of the premises.")
+      else
+        SC.Cut(bot, premises(0), premises(1), phi)
+    }
   }
 
   case object CutWithoutFormula extends ProofStepWithoutBotNorPrem(2) {
     def asSCProof(bot: Sequent, premises: Seq[Int], currentProof: Library#Proof): ProofStepJudgement = {
-      val leftSequent = currentProof.getSequent(premises(0))
-      val rightSequent = currentProof.getSequent(premises(1))
-      val cutSet = rightSequent.left.diff(bot.left) ++ leftSequent.right.diff(bot.right)
+      def invalid(msg: String) = ProofStepJudgement.InvalidProofStep(
+        this.asProofStepWithoutBot(premises).asProofStep(bot),
+        msg
+      )
+
+      lazy val leftSequent = currentProof.getSequent(premises(0))
+      lazy val rightSequent = currentProof.getSequent(premises(1))
+      lazy val cutSet = rightSequent.left.diff(bot.left) ++ leftSequent.right.diff(bot.right)
       lazy val intersectedCutSet = rightSequent.left & leftSequent.right
 
-      if (!cutSet.isEmpty)
-        if (cutSet.tail.isEmpty) {
-          SC.Cut(bot, premises(0), premises(1), cutSet.head)
-        } else
-          ProofStepJudgement.InvalidProofStep(this.asProofStepWithoutBot(premises).asProofStep(bot), "Inferred cut pivot is not a singleton set.")
+      if (premises.length != 2)
+        invalid(s"Two premises expected, ${premises.length} received.")
+      else if (!cutSet.isEmpty)
+        if (cutSet.tail.isEmpty)
+          Cut(cutSet.head).asSCProof(bot, premises, currentProof)
+        else
+          invalid("Inferred cut pivot is not a singleton set.")
       else if (!intersectedCutSet.isEmpty && intersectedCutSet.tail.isEmpty)
         // can still find a pivot
-        SC.Cut(bot, premises(0), premises(1), intersectedCutSet.head)
+        Cut(intersectedCutSet.head).asSCProof(bot, premises, currentProof)
       else
-        ProofStepJudgement.InvalidProofStep(
-          this.asProofStepWithoutBot(premises).asProofStep(bot),
-          "A consistent cut pivot cannot be inferred from the premises. Possibly a missing or extraneous clause."
-        )
+        invalid("A consistent cut pivot cannot be inferred from the premises. Possibly a missing or extraneous clause.")
     }
   }
 
@@ -76,33 +124,57 @@ object BasicStepTactic {
    * </pre>
    */
   case class LeftAnd(phi: Formula, psi: Formula) extends ProofStepWithoutBotNorPrem(1) {
-    def asSCProof(bot: Sequent, premises: Seq[Int], currentProof: Library#Proof): ProofStepJudgement =
-      SC.LeftAnd(bot, premises(0), phi, psi)
+    def asSCProof(bot: Sequent, premises: Seq[Int], currentProof: Library#Proof): ProofStepJudgement = {
+      def invalid(msg: String) = ProofStepJudgement.InvalidProofStep(
+        this.asProofStepWithoutBot(premises).asProofStep(bot),
+        msg
+      )
+
+      lazy val premiseSequent = currentProof.getSequent(premises(0))
+      lazy val phiAndPsi = ConnectorFormula(And, Seq(phi, psi))
+
+      if (premises.length != 1)
+        invalid(s"One premise expected, ${premises.length} received.")
+      else if (!isSameSet(bot.right, premiseSequent.right))
+        invalid("Right-hand side of the conclusion is not the same as the right-hand side of the premise.")
+      else if (
+        !isSameSet(bot.left + phi, premiseSequent.left + phiAndPsi) &&
+        !isSameSet(bot.left + psi, premiseSequent.left + phiAndPsi) &&
+        !isSameSet(bot.left + phi + psi, premiseSequent.left + phiAndPsi)
+      )
+        invalid("Left-hand side of premise + φ∧ψ is not the same as left-hand side of conclusion + either φ, ψ or both.")
+      else
+        SC.LeftAnd(bot, premises(0), phi, psi)
+    }
   }
 
   case object LeftAndWithoutFormula extends ProofStepWithoutBotNorPrem(1) {
     def asSCProof(bot: Sequent, premises: Seq[Int], currentProof: Library#Proof): ProofStepJudgement = {
-      val premiseSequent = currentProof.getSequent(premises(0))
-      val pivot = bot.left.diff(premiseSequent.left)
+      def invalid(msg: String) = ProofStepJudgement.InvalidProofStep(
+        this.asProofStepWithoutBot(premises).asProofStep(bot),
+        msg
+      )
+
+      lazy val premiseSequent = currentProof.getSequent(premises(0))
+      lazy val pivot = bot.left.diff(premiseSequent.left)
 
-      if (!pivot.isEmpty && pivot.tail.isEmpty)
+      if (premises.length != 1)
+        invalid(s"One premise expected, ${premises.length} received.")
+      else if (!pivot.isEmpty && pivot.tail.isEmpty)
         pivot.head match {
           case ConnectorFormula(And, Seq(phi, psi)) =>
             if (premiseSequent.left.contains(phi))
-              SC.LeftAnd(bot, premises(0), phi, psi)
+              LeftAnd(phi, psi).asSCProof(bot, premises, currentProof)
             else
-              SC.LeftAnd(bot, premises(0), psi, phi)
-          case _ => ProofStepJudgement.InvalidProofStep(this.asProofStepWithoutBot(premises).asProofStep(bot), "Could not infer a conjunction as pivot from premise and conclusion.")
+              LeftAnd(psi, phi).asSCProof(bot, premises, currentProof)
+          case _ => invalid("Could not infer a conjunction as pivot from premise and conclusion.")
         }
       else
       // try a rewrite, if it works, go ahead with it, otherwise malformed
       if (SC.isSameSequent(premiseSequent, bot))
-        SC.Rewrite(bot, premises(0))
+        Rewrite.asSCProof(bot, premises, currentProof)
       else
-        ProofStepJudgement.InvalidProofStep(
-          this.asProofStepWithoutBot(premises).asProofStep(bot),
-          "Left-hand side of conclusion + φ∧ψ must be same as left-hand side of premise + either φ, ψ or both."
-        )
+        invalid("Left-hand side of premise + φ∧ψ is not the same as left-hand side of conclusion + either φ, ψ or both.")
     }
   }
 
@@ -125,31 +197,50 @@ object BasicStepTactic {
    */
   case class LeftOr(disjuncts: Seq[Formula]) extends ProofStepWithoutBotNorPrem(-1) {
     def asSCProof(bot: Sequent, premises: Seq[Int], currentProof: Library#Proof): ProofStepJudgement = {
-      SC.LeftOr(bot, premises, disjuncts)
+      def invalid(msg: String) = ProofStepJudgement.InvalidProofStep(
+        this.asProofStepWithoutBot(premises).asProofStep(bot),
+        msg
+      )
+
+      lazy val premiseSequents = premises.map(currentProof.getSequent(_))
+      lazy val disjunction = ConnectorFormula(Or, disjuncts)
+
+      if (premises.length == 0)
+        invalid(s"Premises expected, ${premises.length} received.")
+      else if (!isSameSet(bot.right, premiseSequents.map(_.right).reduce(_ union _)))
+        invalid("Right-hand side of conclusion is not the union of the right-hand sides of the premises.")
+      else if (!isSameSet(disjuncts.foldLeft(bot.left)(_ + _), premiseSequents.map(_.left).reduce(_ union _) + disjunction))
+        invalid("Left-hand side of conclusion + disjuncts is not the same as the union of the left-hand sides of the premises + φ∨ψ.")
+      else
+        SC.LeftOr(bot, premises, disjuncts)
     }
   }
-  case class LeftOrWithoutFormula() extends ProofStepWithoutBotNorPrem(-1) {
+  case object LeftOrWithoutFormula extends ProofStepWithoutBotNorPrem(-1) {
     def asSCProof(bot: Sequent, premises: Seq[Int], currentProof: Library#Proof): ProofStepJudgement = {
-      val premiseSequents = premises.map(currentProof.getSequent(_))
-      val pivots = premiseSequents.map(_.left.diff(bot.left))
+      def invalid(msg: String) = ProofStepJudgement.InvalidProofStep(
+        this.asProofStepWithoutBot(premises).asProofStep(bot),
+        msg
+      )
 
-      if (pivots.exists(_.isEmpty))
-        SC.Weakening(bot, premises(pivots.indexWhere(_.isEmpty)))
+      lazy val premiseSequents = premises.map(currentProof.getSequent(_))
+      lazy val pivots = premiseSequents.map(_.left.diff(bot.left))
+
+      if (premises.length == 0)
+        invalid(s"Premises expected, ${premises.length} received.")
+      else if (pivots.exists(_.isEmpty))
+        Weakening.asSCProof(bot, Seq(premises(pivots.indexWhere(_.isEmpty))), currentProof)
       else if (pivots.forall(_.tail.isEmpty))
-        SC.LeftOr(bot, premises, pivots.map(_.head))
+        LeftOr(pivots.map(_.head)).asSCProof(bot, premises, currentProof)
       else
         // some extraneous formulae
-        ProofStepJudgement.InvalidProofStep(
-          this.asProofStepWithoutBot(premises).asProofStep(bot),
-          "Left-hand side of conclusion + disjuncts is not the same as the union of the left-hand sides of the premises + φ∨ψ."
-        )
+        invalid("Left-hand side of conclusion + disjuncts is not the same as the union of the left-hand sides of the premises + φ∨ψ.")
     }
   }
 
   case object LeftOr extends ProofStepWithoutBotNorPrem(-1) {
     // default construction:
     // def apply(disjuncts: Seq[Formula]) = new LeftOr(disjuncts)
-    def apply() = new LeftOrWithoutFormula()
+    def apply() = LeftOrWithoutFormula
 
     // usage without an argument list
     def asSCProof(bot: Sequent, premises: Seq[Int], currentProof: Library#Proof): ProofStepJudgement =
@@ -164,28 +255,49 @@ object BasicStepTactic {
    * </pre>
    */
   case class LeftImplies(phi: Formula, psi: Formula) extends ProofStepWithoutBotNorPrem(2) {
-    def asSCProof(bot: Sequent, premises: Seq[Int], currentProof: Library#Proof): ProofStepJudgement =
-      SC.LeftImplies(bot, premises(0), premises(1), phi, psi)
+    def asSCProof(bot: Sequent, premises: Seq[Int], currentProof: Library#Proof): ProofStepJudgement = {
+      def invalid(msg: String) = ProofStepJudgement.InvalidProofStep(
+        this.asProofStepWithoutBot(premises).asProofStep(bot),
+        msg
+      )
+
+      lazy val leftSequent = currentProof.getSequent(premises(0))
+      lazy val rightSequent = currentProof.getSequent(premises(1))
+      lazy val implication = ConnectorFormula(Implies, Seq(phi, psi))
+
+      if (premises.length != 2)
+        invalid(s"Two premises expected, ${premises.length} received.")
+      else if (!isSameSet(bot.right + phi, leftSequent.right union rightSequent.right))
+        invalid("Right-hand side of conclusion + φ is not the union of right-hand sides of premises.")
+      else if (!isSameSet(bot.left + psi, leftSequent.left union rightSequent.left + implication))
+        invalid("Left-hand side of conclusion + ψ is not the union of left-hand sides of premises + φ→ψ.")
+      else
+        SC.LeftImplies(bot, premises(0), premises(1), phi, psi)
+    }
   }
 
   case object LeftImpliesWithoutFormula extends ProofStepWithoutBotNorPrem(2) {
     def asSCProof(bot: Sequent, premises: Seq[Int], currentProof: Library#Proof): ProofStepJudgement = {
-      val leftSequent = currentProof.getSequent(premises(0))
-      val rightSequent = currentProof.getSequent(premises(1))
-      val pivotLeft = leftSequent.right.diff(bot.right)
+      def invalid(msg: String) = ProofStepJudgement.InvalidProofStep(
+        this.asProofStepWithoutBot(premises).asProofStep(bot),
+        msg
+      )
+
+      lazy val leftSequent = currentProof.getSequent(premises(0))
+      lazy val rightSequent = currentProof.getSequent(premises(1))
+      lazy val pivotLeft = leftSequent.right.diff(bot.right)
       lazy val pivotRight = rightSequent.left.diff(bot.left)
 
-      if (pivotLeft.isEmpty)
-        SC.Weakening(bot, premises(0))
+      if (premises.length != 2)
+        invalid(s"Two premises expected, ${premises.length} received.")
+      else if (pivotLeft.isEmpty)
+        Weakening.asSCProof(bot, premises, currentProof)
       else if (pivotRight.isEmpty)
-        SC.Weakening(bot, premises(1))
+        Weakening.asSCProof(bot, premises, currentProof)
       else if (pivotLeft.tail.isEmpty && pivotRight.tail.isEmpty)
-        SC.LeftImplies(bot, premises(0), premises(1), pivotLeft.head, pivotRight.head)
+        LeftImplies(pivotLeft.head, pivotRight.head).asSCProof(bot, premises, currentProof)
       else
-        ProofStepJudgement.InvalidProofStep(
-          this.asProofStepWithoutBot(premises).asProofStep(bot),
-          "Could not infer an implication as a pivot from the premises and conclusion, possible extraneous formulae in premises."
-        )
+        invalid("Could not infer an implication as a pivot from the premises and conclusion, possible extraneous formulae in premises.")
     }
   }
 
@@ -207,21 +319,50 @@ object BasicStepTactic {
    * </pre>
    */
   case class LeftIff(phi: Formula, psi: Formula) extends ProofStepWithoutBotNorPrem(1) {
-    def asSCProof(bot: Sequent, premises: Seq[Int], currentProof: Library#Proof): ProofStepJudgement =
-      SC.LeftIff(bot, premises(0), phi, psi)
+    def asSCProof(bot: Sequent, premises: Seq[Int], currentProof: Library#Proof): ProofStepJudgement = {
+      def invalid(msg: String) = ProofStepJudgement.InvalidProofStep(
+        this.asProofStepWithoutBot(premises).asProofStep(bot),
+        msg
+      )
+
+      lazy val premiseSequent = currentProof.getSequent(premises(0))
+      lazy val implication = ConnectorFormula(Iff, Seq(phi, psi))
+      lazy val impLeft = ConnectorFormula(Implies, Seq(phi, psi))
+      lazy val impRight = ConnectorFormula(Implies, Seq(psi, phi))
+
+      if (premises.length != 1)
+        invalid(s"One premise expected, ${premises.length} received.")
+      else if (!isSameSet(bot.right, premiseSequent.right))
+        invalid("Right-hand side of premise is not the same as right-hand side of conclusion.")
+      else if (
+        !isSameSet(bot.left + impLeft, premiseSequent.left + implication) &&
+        !isSameSet(bot.left + impRight, premiseSequent.left + implication) &&
+        !isSameSet(bot.left + impLeft + impRight, premiseSequent.left + implication)
+      )
+        invalid("Left-hand side of premise + φ↔ψ is not the same as left-hand side of conclusion + either φ→ψ, ψ→φ or both.")
+      else
+        SC.LeftIff(bot, premises(0), phi, psi)
+    }
   }
 
-  case class LeftIffWithoutFormula() extends ProofStepWithoutBotNorPrem(1) {
+  case object LeftIffWithoutFormula extends ProofStepWithoutBotNorPrem(1) {
     def asSCProof(bot: Sequent, premises: Seq[Int], currentProof: Library#Proof): ProofStepJudgement = {
-      val premiseSequent = currentProof.getSequent(premises(0))
-      val pivot = premiseSequent.left.diff(bot.left)
+      def invalid(msg: String) = ProofStepJudgement.InvalidProofStep(
+        this.asProofStepWithoutBot(premises).asProofStep(bot),
+        msg
+      )
 
-      if (pivot.isEmpty)
-        SC.Weakening(bot, premises(0))
+      lazy val premiseSequent = currentProof.getSequent(premises(0))
+      lazy val pivot = premiseSequent.left.diff(bot.left)
+
+      if (premises.length != 1)
+        invalid(s"One premise expected, ${premises.length} received.")
+      else if (pivot.isEmpty)
+        Weakening.asSCProof(bot, premises, currentProof)
       else
         pivot.head match {
-          case ConnectorFormula(Implies, Seq(phi, psi)) => SC.LeftIff(bot, premises(0), phi, psi)
-          case _ => ProofStepJudgement.InvalidProofStep(this.asProofStepWithoutBot(premises).asProofStep(bot), "Could not infer a pivot implication from premise.")
+          case ConnectorFormula(Implies, Seq(phi, psi)) => LeftIff(phi, psi).asSCProof(bot, premises, currentProof)
+          case _ => invalid("Could not infer a pivot implication from premise.")
         }
     }
   }
@@ -229,7 +370,7 @@ object BasicStepTactic {
   case object LeftIff extends ProofStepWithoutBotNorPrem(1) {
     // default construction:
     // def apply(phi: Formula, psi: Formula) = new LeftIff(phi, psi)
-    def apply() = new LeftIffWithoutFormula()
+    def apply() = LeftIffWithoutFormula
 
     // usage without an argument list
     def asSCProof(bot: Sequent, premises: Seq[Int], currentProof: Library#Proof): ProofStepJudgement =
@@ -244,21 +385,44 @@ object BasicStepTactic {
    * </pre>
    */
   case class LeftNot(phi: Formula) extends ProofStepWithoutBotNorPrem(1) {
-    def asSCProof(bot: Sequent, premises: Seq[Int], currentProof: Library#Proof): ProofStepJudgement =
-      SC.LeftNot(bot, premises(0), phi)
+    def asSCProof(bot: Sequent, premises: Seq[Int], currentProof: Library#Proof): ProofStepJudgement = {
+      def invalid(msg: String) = ProofStepJudgement.InvalidProofStep(
+        this.asProofStepWithoutBot(premises).asProofStep(bot),
+        msg
+      )
+
+      lazy val premiseSequent = currentProof.getSequent(premises(0))
+      lazy val negation = ConnectorFormula(Neg, Seq(phi))
+
+      if (premises.length != 1)
+        invalid(s"One premise expected, ${premises.length} received.")
+      else if (!isSameSet(bot.right + phi, premiseSequent.right))
+        invalid("Right-hand side of conclusion + φ is not the same as right-hand side of premise.")
+      else if (!isSameSet(bot.left, premiseSequent.left + negation))
+        invalid("Left-hand side of conclusion is not the same as left-hand side of premise + ¬φ.")
+      else
+        SC.LeftNot(bot, premises(0), phi)
+    }
   }
 
-  case class LeftNotWithoutFormula() extends ProofStepWithoutBotNorPrem(1) {
+  case object LeftNotWithoutFormula extends ProofStepWithoutBotNorPrem(1) {
     def asSCProof(bot: Sequent, premises: Seq[Int], currentProof: Library#Proof): ProofStepJudgement = {
-      val premiseSequent = currentProof.getSequent(premises(0))
-      val pivot = premiseSequent.right.diff(bot.right)
+      def invalid(msg: String) = ProofStepJudgement.InvalidProofStep(
+        this.asProofStepWithoutBot(premises).asProofStep(bot),
+        msg
+      )
 
-      if (pivot.isEmpty)
-        SC.Weakening(bot, premises(0))
+      lazy val premiseSequent = currentProof.getSequent(premises(0))
+      lazy val pivot = premiseSequent.right.diff(bot.right)
+
+      if (premises.length != 1)
+        invalid(s"One premise expected, ${premises.length} received.")
+      else if (pivot.isEmpty)
+        Weakening.asSCProof(bot, premises, currentProof)
       else if (pivot.tail.isEmpty)
-        SC.LeftNot(bot, premises(0), pivot.head)
+        LeftNot(pivot.head).asSCProof(bot, premises, currentProof)
       else
-        ProofStepJudgement.InvalidProofStep(this.asProofStepWithoutBot(premises).asProofStep(bot), "Right-hand side of conclusion + φ must be the same as right-hand side of premise.")
+        invalid("Right-hand side of conclusion + φ is not the same as right-hand side of premise.")
 
     }
   }
@@ -266,7 +430,7 @@ object BasicStepTactic {
   case object LeftNot extends ProofStepWithoutBotNorPrem(1) {
     // default construction:
     // def apply(phi: Formula) = new LeftNot(phi)
-    def apply() = new LeftNotWithoutFormula()
+    def apply() = LeftNotWithoutFormula
 
     // usage without an argument list
     def asSCProof(bot: Sequent, premises: Seq[Int], currentProof: Library#Proof): ProofStepJudgement =
@@ -282,25 +446,48 @@ object BasicStepTactic {
    * </pre>
    */
   case class LeftForall(phi: Formula, x: VariableLabel, t: Term) extends ProofStepWithoutBotNorPrem(1) {
-    def asSCProof(bot: Sequent, premises: Seq[Int], currentProof: Library#Proof): ProofStepJudgement =
-      SC.LeftForall(bot, premises(0), phi, x, t)
+    def asSCProof(bot: Sequent, premises: Seq[Int], currentProof: Library#Proof): ProofStepJudgement = {
+      def invalid(msg: String) = ProofStepJudgement.InvalidProofStep(
+        this.asProofStepWithoutBot(premises).asProofStep(bot),
+        msg
+      )
+
+      lazy val premiseSequent = currentProof.getSequent(premises(0))
+      lazy val quantified = BinderFormula(Forall, x, phi)
+      lazy val instantiated = substituteVariables(phi, Map(x -> t))
+
+      if (premises.length != 1)
+        invalid(s"One premise expected, ${premises.length} received.")
+      else if (!isSameSet(bot.right, premiseSequent.right))
+        invalid("Right-hand side of conclusion is not the same as right-hand side of premise")
+      else if (!isSameSet(bot.left + instantiated, premiseSequent.left + quantified))
+        invalid("Left-hand side of conclusion + φ[t/x] is not the same as left-hand side of premise + ∀x. φ")
+      else
+        SC.LeftForall(bot, premises(0), phi, x, t)
+    }
   }
 
   case class LeftForallWithoutFormula(t: Term) extends ProofStepWithoutBotNorPrem(1) {
     def asSCProof(bot: Sequent, premises: Seq[Int], currentProof: Library#Proof): ProofStepJudgement = {
-      val premiseSequent = currentProof.getSequent(premises(0))
-      val pivot = bot.left.diff(premiseSequent.left)
+      def invalid(msg: String) = ProofStepJudgement.InvalidProofStep(
+        this.asProofStepWithoutBot(premises).asProofStep(bot),
+        msg
+      )
+
+      lazy val premiseSequent = currentProof.getSequent(premises(0))
+      lazy val pivot = bot.left.diff(premiseSequent.left)
       lazy val instantiatedPivot = premiseSequent.left.diff(bot.left)
 
-      if (!pivot.isEmpty)
+      if (premises.length != 1) invalid(s"One premise expected, ${premises.length} received.")
+      else if (!pivot.isEmpty)
         if (pivot.tail.isEmpty)
           pivot.head match {
-            case BinderFormula(Forall, x, phi) => SC.LeftForall(bot, premises(0), phi, x, t)
-            case _ => ProofStepJudgement.InvalidProofStep(this.asProofStepWithoutBot(premises).asProofStep(bot), "Could not infer a universally quantified pivot from premise and conclusion.")
+            case BinderFormula(Forall, x, phi) => LeftForall(phi, x, t).asSCProof(bot, premises, currentProof)
+            case _ => invalid("Could not infer a universally quantified pivot from premise and conclusion.")
           }
         else
-          ProofStepJudgement.InvalidProofStep(this.asProofStepWithoutBot(premises).asProofStep(bot), "Left-hand side of conclusion + φ[t/x] must be the same as left-hand side of premise + ∀x. φ.")
-      else if (instantiatedPivot.isEmpty) SC.Weakening(bot, premises(0))
+          invalid("Left-hand side of conclusion + φ[t/x] is not the same as left-hand side of premise + ∀x. φ.")
+      else if (instantiatedPivot.isEmpty) Weakening.asSCProof(bot, premises, currentProof)
       else if (instantiatedPivot.tail.isEmpty) {
         // go through conclusion to find a matching quantified formula
 
@@ -313,10 +500,10 @@ object BasicStepTactic {
         )
 
         quantifiedPhi match {
-          case Some(BinderFormula(Forall, x, phi)) => SC.LeftForall(bot, premises(0), phi, x, t)
-          case _ => ProofStepJudgement.InvalidProofStep(this.asProofStepWithoutBot(premises).asProofStep(bot), "Could not infer a universally quantified pivot from premise and conclusion.")
+          case Some(BinderFormula(Forall, x, phi)) => LeftForall(phi, x, t).asSCProof(bot, premises, currentProof)
+          case _ => invalid("Could not infer a universally quantified pivot from premise and conclusion.")
         }
-      } else ProofStepJudgement.InvalidProofStep(this.asProofStepWithoutBot(premises).asProofStep(bot), "Left-hand side of conclusion + φ[t/x] must be the same as left-hand side of premise + ∀x. φ.")
+      } else invalid("Left-hand side of conclusion + φ[t/x] is not the same as left-hand side of premise + ∀x. φ.")
     }
   }
 
@@ -343,18 +530,43 @@ object BasicStepTactic {
    * </pre>
    */
   case class LeftExists(phi: Formula, x: VariableLabel) extends ProofStepWithoutBotNorPrem(1) {
-    def asSCProof(bot: Sequent, premises: Seq[Int], currentProof: Library#Proof): ProofStepJudgement =
-      SC.LeftExists(bot, premises(0), phi, x)
+    def asSCProof(bot: Sequent, premises: Seq[Int], currentProof: Library#Proof): ProofStepJudgement = {
+      def invalid(msg: String) = ProofStepJudgement.InvalidProofStep(
+        this.asProofStepWithoutBot(premises).asProofStep(bot),
+        msg
+      )
+
+      lazy val premiseSequent = currentProof.getSequent(premises(0))
+      lazy val quantified = BinderFormula(Exists, x, phi)
+
+      if (premises.length != 1)
+        invalid(s"One premise expected, ${premises.length} received.")
+      else if ((bot.left union bot.right).exists(_.freeVariables.contains(x)))
+        invalid("The variable x must not be free in the resulting sequent.")
+      else if (!isSameSet(bot.right, premiseSequent.right))
+        invalid("Right-hand side of conclusion is not the same as right-hand side of premise")
+      else if (!isSameSet(bot.left + phi, premiseSequent.left + quantified))
+        invalid("Left-hand side of conclusion + φ is not the same as left-hand side of premise + ∃x. φ")
+      else
+        SC.LeftExists(bot, premises(0), phi, x)
+    }
   }
 
-  case class LeftExistsWithoutFormula() extends ProofStepWithoutBotNorPrem(1) {
+  case object LeftExistsWithoutFormula extends ProofStepWithoutBotNorPrem(1) {
     def asSCProof(bot: Sequent, premises: Seq[Int], currentProof: Library#Proof): ProofStepJudgement = {
-      val premiseSequent = currentProof.getSequent(premises(0))
-      val pivot = bot.left.diff(premiseSequent.left)
+      def invalid(msg: String) = ProofStepJudgement.InvalidProofStep(
+        this.asProofStepWithoutBot(premises).asProofStep(bot),
+        msg
+      )
+
+      lazy val premiseSequent = currentProof.getSequent(premises(0))
+      lazy val pivot = bot.left.diff(premiseSequent.left)
       lazy val instantiatedPivot = premiseSequent.left.diff(bot.left)
 
-      if (pivot.isEmpty)
-        if (instantiatedPivot.isEmpty) SC.Rewrite(bot, premises(0))
+      if (premises.length != 1)
+        invalid(s"One premise expected, ${premises.length} received.")
+      else if (pivot.isEmpty)
+        if (instantiatedPivot.isEmpty) Rewrite.asSCProof(bot, premises, currentProof)
         else if (instantiatedPivot.tail.isEmpty) {
           val in: Formula = instantiatedPivot.head
           val quantifiedPhi: Option[Formula] = bot.left.find(f =>
@@ -365,24 +577,24 @@ object BasicStepTactic {
           )
 
           quantifiedPhi match {
-            case Some(BinderFormula(Exists, x, phi)) => SC.LeftExists(bot, premises(0), phi, x)
-            case _ => ProofStepJudgement.InvalidProofStep(this.asProofStepWithoutBot(premises).asProofStep(bot), "Could not infer an existensially quantified pivot from premise and conclusion.")
+            case Some(BinderFormula(Exists, x, phi)) => LeftExists(phi, x).asSCProof(bot, premises, currentProof)
+            case _ => invalid("Could not infer an existensially quantified pivot from premise and conclusion.")
           }
-        } else ProofStepJudgement.InvalidProofStep(this.asProofStepWithoutBot(premises).asProofStep(bot), "Left-hand side of conclusion + φ must be the same as left-hand side of premise + ∃x. φ.")
+        } else invalid("Left-hand side of conclusion + φ is not the same as left-hand side of premise + ∃x. φ.")
       else if (pivot.tail.isEmpty)
         pivot.head match {
-          case BinderFormula(Exists, x, phi) => SC.LeftExists(bot, premises(0), phi, x)
-          case _ => ProofStepJudgement.InvalidProofStep(this.asProofStepWithoutBot(premises).asProofStep(bot), "Could not infer an existentially quantified pivot from premise and conclusion.")
+          case BinderFormula(Exists, x, phi) => LeftExists(phi, x).asSCProof(bot, premises, currentProof)
+          case _ => invalid("Could not infer an existentially quantified pivot from premise and conclusion.")
         }
       else
-        ProofStepJudgement.InvalidProofStep(this.asProofStepWithoutBot(premises).asProofStep(bot), "Left-hand side of conclusion + φ must be the same as left-hand side of premise + ∃x. φ.")
+        invalid("Left-hand side of conclusion + φ is not the same as left-hand side of premise + ∃x. φ.")
     }
   }
 
   case object LeftExists extends ProofStepWithoutBotNorPrem(1) {
     // default construction:
     // def apply(phi: Formula, x: VariableLabel) = new LeftExists(phi, x)
-    def apply() = new LeftExistsWithoutFormula()
+    def apply() = LeftExistsWithoutFormula
 
     // usage without an argument list
     def asSCProof(bot: Sequent, premises: Seq[Int], currentProof: Library#Proof): ProofStepJudgement =
@@ -397,41 +609,66 @@ object BasicStepTactic {
    * </pre>
    */
   case class LeftExistsOne(phi: Formula, x: VariableLabel) extends ProofStepWithoutBotNorPrem(1) {
-    def asSCProof(bot: Sequent, premises: Seq[Int], currentProof: Library#Proof): ProofStepJudgement =
-      SC.LeftExistsOne(bot, premises(0), phi, x)
+    def asSCProof(bot: Sequent, premises: Seq[Int], currentProof: Library#Proof): ProofStepJudgement = {
+      def invalid(msg: String) = ProofStepJudgement.InvalidProofStep(
+        this.asProofStepWithoutBot(premises).asProofStep(bot),
+        msg
+      )
+
+      lazy val premiseSequent = currentProof.getSequent(premises(0))
+      lazy val y = VariableLabel(freshId(phi.freeVariables.map(_.id) + x.id, "y"))
+      lazy val instantiated = BinderFormula(Exists, y, BinderFormula(Forall, x, ConnectorFormula(Iff, List(PredicateFormula(equality, List(VariableTerm(x), VariableTerm(y))), phi))))
+      lazy val quantified = BinderFormula(ExistsOne, x, phi)
+
+      if (premises.length != 1)
+        invalid(s"One premise expected, ${premises.length} received.")
+      else if (!isSameSet(bot.right, premiseSequent.right))
+        invalid("Right-hand side of conclusion is not the same as right-hand side of premise.")
+      else if (!isSameSet(bot.left + instantiated, premiseSequent.left + quantified))
+        invalid("Left-hand side of conclusion + ∃y.∀x. (x=y) ↔ φ is not the same as left-hand side of premise + ∃!x. φ.")
+      else
+        SC.LeftExistsOne(bot, premises(0), phi, x)
+    }
   }
 
-  case class LeftExistsOneWithoutFormula() extends ProofStepWithoutBotNorPrem(1) {
+  case object LeftExistsOneWithoutFormula extends ProofStepWithoutBotNorPrem(1) {
     def asSCProof(bot: Sequent, premises: Seq[Int], currentProof: Library#Proof): ProofStepJudgement = {
-      val premiseSequent = currentProof.getSequent(premises(0))
-      val pivot = bot.left.diff(premiseSequent.left)
+      def invalid(msg: String) = ProofStepJudgement.InvalidProofStep(
+        this.asProofStepWithoutBot(premises).asProofStep(bot),
+        msg
+      )
+
+      lazy val premiseSequent = currentProof.getSequent(premises(0))
+      lazy val pivot = bot.left.diff(premiseSequent.left)
       lazy val instantiatedPivot = premiseSequent.left.diff(bot.left)
 
-      if (pivot.isEmpty)
+      if (premises.length != 1)
+        invalid(s"One premise expected, ${premises.length} received.")
+      else if (pivot.isEmpty)
         if (instantiatedPivot.isEmpty)
-          SC.Rewrite(bot, premises(0))
+          Rewrite.asSCProof(bot, premises, currentProof)
         else if (instantiatedPivot.tail.isEmpty) {
           instantiatedPivot.head match {
             // ∃_. ∀x. _ ↔ φ == extract ==> x, phi
-            case BinderFormula(Exists, _, BinderFormula(Forall, x, ConnectorFormula(Iff, Seq(_, phi)))) => SC.LeftExistsOne(bot, premises(0), phi, x)
+            case BinderFormula(Exists, _, BinderFormula(Forall, x, ConnectorFormula(Iff, Seq(_, phi)))) => LeftExistsOne(phi, x).asSCProof(bot, premises, currentProof)
             case _ => ProofStepJudgement.InvalidProofStep(this.asProofStepWithoutBot(premises).asProofStep(bot), "Could not infer an existentially quantified pivot from premise and conclusion.")
           }
         } else
-          ProofStepJudgement.InvalidProofStep(this.asProofStepWithoutBot(premises).asProofStep(bot), "Left-hand side of conclusion + φ must be the same as left-hand side of premise + ∃x. φ.")
+          invalid("Left-hand side of conclusion + φ is not the same as left-hand side of premise + ∃x. φ.")
       else if (pivot.tail.isEmpty)
         pivot.head match {
           case BinderFormula(ExistsOne, x, phi) => SC.LeftExistsOne(bot, premises(0), phi, x)
-          case _ => ProofStepJudgement.InvalidProofStep(this.asProofStepWithoutBot(premises).asProofStep(bot), "Could not infer an existentially quantified pivot from premise and conclusion.")
+          case _ => invalid("Could not infer an existentially quantified pivot from premise and conclusion.")
         }
       else
-        ProofStepJudgement.InvalidProofStep(this.asProofStepWithoutBot(premises).asProofStep(bot), "Left-hand side of conclusion + φ must be the same as left-hand side of premise + ∃x. φ.")
+        invalid("Left-hand side of conclusion + φ is not the same as left-hand side of premise + ∃x. φ.")
     }
   }
 
   case object LeftExistsOne extends ProofStepWithoutBotNorPrem(1) {
     // default construction:
     // def apply(phi: Formula, x: VariableLabel) = new LeftExistsOne(phi, x)
-    def apply() = new LeftExistsOneWithoutFormula()
+    def apply() = LeftExistsOneWithoutFormula
 
     // usage without an argument list
     def asSCProof(bot: Sequent, premises: Seq[Int], currentProof: Library#Proof): ProofStepJudgement =
@@ -446,25 +683,45 @@ object BasicStepTactic {
    *    Γ, Σ |- φ∧ψ∧..., Π, Δ
    * </pre>
    */
-  case class RightAnd(cunjuncts: Seq[Formula]) extends ProofStepWithoutBotNorPrem(-1) {
-    def asSCProof(bot: Sequent, premises: Seq[Int], currentProof: Library#Proof): ProofStepJudgement =
-      SC.RightAnd(bot, premises, cunjuncts)
+  case class RightAnd(conjuncts: Seq[Formula]) extends ProofStepWithoutBotNorPrem(-1) {
+    def asSCProof(bot: Sequent, premises: Seq[Int], currentProof: Library#Proof): ProofStepJudgement = {
+      def invalid(msg: String) = ProofStepJudgement.InvalidProofStep(
+        this.asProofStepWithoutBot(premises).asProofStep(bot),
+        msg
+      )
+
+      lazy val premiseSequents = premises.map(currentProof.getSequent(_))
+      lazy val conjunction = ConnectorFormula(And, conjuncts)
+
+      if (premises.length == 0)
+        invalid(s"Premises expected, ${premises.length} received.")
+      else if (!isSameSet(bot.left, premiseSequents.map(_.left).reduce(_ union _)))
+        invalid("Left-hand side of conclusion is not the union of the left-hand sides of the premises.")
+      else if (!isSameSet(conjuncts.foldLeft(bot.right)(_ + _), premiseSequents.map(_.right).reduce(_ union _) + conjunction))
+        invalid("Right-hand side of conclusion + conjuncts is not the same as the union of the right-hand sides of the premises + φ∧ψ....")
+      else
+        SC.RightAnd(bot, premises, conjuncts)
+    }
   }
   case object RightAndWithoutFormula extends ProofStepWithoutBotNorPrem(-1) {
     def asSCProof(bot: Sequent, premises: Seq[Int], currentProof: Library#Proof): ProofStepJudgement = {
-      val premiseSequents = premises.map(currentProof.getSequent(_))
-      val pivots = premiseSequents.map(_.right.diff(bot.right))
+      def invalid(msg: String) = ProofStepJudgement.InvalidProofStep(
+        this.asProofStepWithoutBot(premises).asProofStep(bot),
+        msg
+      )
 
-      if (pivots.exists(_.isEmpty))
-        SC.Weakening(bot, premises(pivots.indexWhere(_.isEmpty)))
+      lazy val premiseSequents = premises.map(currentProof.getSequent(_))
+      lazy val pivots = premiseSequents.map(_.right.diff(bot.right))
+
+      if (premises.length == 0)
+        invalid(s"Premises expected, ${premises.length} received.")
+      else if (pivots.exists(_.isEmpty))
+        Weakening.asSCProof(bot, Seq(premises(pivots.indexWhere(_.isEmpty))), currentProof)
       else if (pivots.forall(_.tail.isEmpty))
-        SC.RightAnd(bot, premises, pivots.map(_.head))
+        RightAnd(pivots.map(_.head)).asSCProof(bot, premises, currentProof)
       else
         // some extraneous formulae
-        ProofStepJudgement.InvalidProofStep(
-          this.asProofStepWithoutBot(premises).asProofStep(bot),
-          "Right-hand side of conclusion + φ + ψ is not the same as the union of the right-hand sides of the premises +φ∧ψ."
-        )
+        invalid("Right-hand side of conclusion + φ + ψ is not the same as the union of the right-hand sides of the premises +φ∧ψ.")
     }
   }
 
@@ -486,40 +743,64 @@ object BasicStepTactic {
    * </pre>
    */
   case class RightOr(phi: Formula, psi: Formula) extends ProofStepWithoutBotNorPrem(1) {
-    def asSCProof(bot: Sequent, premises: Seq[Int], currentProof: Library#Proof): ProofStepJudgement =
-      SC.RightOr(bot, premises(0), phi, psi)
+    def asSCProof(bot: Sequent, premises: Seq[Int], currentProof: Library#Proof): ProofStepJudgement = {
+      def invalid(msg: String) = ProofStepJudgement.InvalidProofStep(
+        this.asProofStepWithoutBot(premises).asProofStep(bot),
+        msg
+      )
+
+      lazy val premiseSequent = currentProof.getSequent(premises(0))
+      lazy val phiAndPsi = ConnectorFormula(Or, Seq(phi, psi))
+
+      if (premises.length != 1)
+        invalid(s"One premise expected, ${premises.length} received.")
+      else if (!isSameSet(bot.left, premiseSequent.left))
+        invalid("Left-hand side of the premise is not the same as the left-hand side of the conclusion.")
+      else if (
+        !isSameSet(bot.right + phi, premiseSequent.right + phiAndPsi) &&
+        !isSameSet(bot.right + psi, premiseSequent.right + phiAndPsi) &&
+        !isSameSet(bot.right + phi + psi, premiseSequent.right + phiAndPsi)
+      )
+        invalid("Right-hand side of premise + φ∧ψ is not the same as right-hand side of conclusion + either φ, ψ or both.")
+      else
+        SC.RightOr(bot, premises(0), phi, psi)
+    }
   }
 
-  case class RightOrWithoutFormula() extends ProofStepWithoutBotNorPrem(1) {
+  case object RightOrWithoutFormula extends ProofStepWithoutBotNorPrem(1) {
     def asSCProof(bot: Sequent, premises: Seq[Int], currentProof: Library#Proof): ProofStepJudgement = {
-      val premiseSequent = currentProof.getSequent(premises(0))
-      val pivot = bot.right.diff(premiseSequent.right)
+      def invalid(msg: String) = ProofStepJudgement.InvalidProofStep(
+        this.asProofStepWithoutBot(premises).asProofStep(bot),
+        msg
+      )
 
-      if (!pivot.isEmpty && pivot.tail.isEmpty)
+      lazy val premiseSequent = currentProof.getSequent(premises(0))
+      lazy val pivot = bot.right.diff(premiseSequent.right)
+
+      if (premises.length != 1)
+        invalid(s"One premise expected, ${premises.length} received.")
+      else if (!pivot.isEmpty && pivot.tail.isEmpty)
         pivot.head match {
           case ConnectorFormula(Or, Seq(phi, psi)) =>
             if (premiseSequent.left.contains(phi))
-              SC.RightOr(bot, premises(0), phi, psi)
+              RightOr(phi, psi).asSCProof(bot, premises, currentProof)
             else
-              SC.RightOr(bot, premises(0), psi, phi)
-          case _ => ProofStepJudgement.InvalidProofStep(this.asProofStepWithoutBot(premises).asProofStep(bot), "Could not infer a disjunction as pivot from premise and conclusion.")
+              RightOr(psi, phi).asSCProof(bot, premises, currentProof)
+          case _ => invalid("Could not infer a disjunction as pivot from premise and conclusion.")
         }
       else
       // try a rewrite, if it works, go ahead with it, otherwise malformed
       if (SC.isSameSequent(premiseSequent, bot))
-        SC.Rewrite(bot, premises(0))
+        Rewrite.asSCProof(bot, premises, currentProof)
       else
-        ProofStepJudgement.InvalidProofStep(
-          this.asProofStepWithoutBot(premises).asProofStep(bot),
-          "Right-hand side of conclusion + φ∧ψ must be same as right-hand side of premise + either φ, ψ or both."
-        )
+        invalid("Right-hand side of conclusion + φ∧ψ is not the same as right-hand side of premise + either φ, ψ or both.")
     }
   }
 
   case object RightOr extends ProofStepWithoutBotNorPrem(1) {
     // default construction:
     // def apply(phi: Formula, psi: Formula) = new RightOr(phi, psi)
-    def apply() = new RightOrWithoutFormula()
+    def apply() = RightOrWithoutFormula
 
     // usage without an argument list
     def asSCProof(bot: Sequent, premises: Seq[Int], currentProof: Library#Proof): ProofStepJudgement =
@@ -534,30 +815,53 @@ object BasicStepTactic {
    * </pre>
    */
   case class RightImplies(phi: Formula, psi: Formula) extends ProofStepWithoutBotNorPrem(1) {
-    def asSCProof(bot: Sequent, premises: Seq[Int], currentProof: Library#Proof): ProofStepJudgement =
-      SC.RightImplies(bot, premises(0), phi, psi)
+    def asSCProof(bot: Sequent, premises: Seq[Int], currentProof: Library#Proof): ProofStepJudgement = {
+      def invalid(msg: String) = ProofStepJudgement.InvalidProofStep(
+        this.asProofStepWithoutBot(premises).asProofStep(bot),
+        msg
+      )
+
+      lazy val premiseSequent = currentProof.getSequent(premises(0))
+      lazy val implication = ConnectorFormula(Implies, Seq(phi, psi))
+
+      if (premises.length != 1)
+        invalid(s"One premise expected, ${premises.length} received.")
+      else if (!isSameSet(bot.left + phi, premiseSequent.left))
+        invalid("Left-hand side of conclusion + φ is not the same as left-hand side of premise.")
+      else if (!isSameSet(bot.right + psi, premiseSequent.right + implication))
+        invalid("Right-hand side of conclusion + ψ is not the same as right-hand side of premise + φ→ψ.")
+      else
+        SC.RightImplies(bot, premises(0), phi, psi)
+    }
   }
 
-  case class RightImpliesWithoutFormula() extends ProofStepWithoutBotNorPrem(1) {
+  case object RightImpliesWithoutFormula extends ProofStepWithoutBotNorPrem(1) {
     def asSCProof(bot: Sequent, premises: Seq[Int], currentProof: Library#Proof): ProofStepJudgement = {
-      val premiseSequent = currentProof.getSequent(premises(0))
-      val leftPivot = premiseSequent.left.diff(bot.left)
-      val rightPivot = premiseSequent.right.diff(bot.right)
+      def invalid(msg: String) = ProofStepJudgement.InvalidProofStep(
+        this.asProofStepWithoutBot(premises).asProofStep(bot),
+        msg
+      )
 
-      if (
+      lazy val premiseSequent = currentProof.getSequent(premises(0))
+      lazy val leftPivot = premiseSequent.left.diff(bot.left)
+      lazy val rightPivot = premiseSequent.right.diff(bot.right)
+
+      if (premises.length != 1)
+        invalid(s"One premise expected, ${premises.length} received.")
+      else if (
         !leftPivot.isEmpty && leftPivot.tail.isEmpty &&
         !rightPivot.isEmpty && rightPivot.tail.isEmpty
       )
-        SC.RightImplies(bot, premises(0), leftPivot.head, rightPivot.head)
+        RightImplies(leftPivot.head, rightPivot.head).asSCProof(bot, premises, currentProof)
       else
-        ProofStepJudgement.InvalidProofStep(this.asProofStepWithoutBot(premises).asProofStep(bot), "Right-hand side of conclusion + ψ must be same as right-hand side of premise + φ→ψ.")
+        invalid("Right-hand side of conclusion + ψ is not the same as right-hand side of premise + φ→ψ.")
     }
   }
 
   case object RightImplies extends ProofStepWithoutBotNorPrem(1) {
     // default construction:
     // def apply(phi: Formula, psi: Formula) = new RightImplies(phi, psi)
-    def apply() = new RightImpliesWithoutFormula()
+    def apply() = RightImpliesWithoutFormula
 
     // usage without an argument list
     def asSCProof(bot: Sequent, premises: Seq[Int], currentProof: Library#Proof): ProofStepJudgement =
@@ -572,34 +876,57 @@ object BasicStepTactic {
    * </pre>
    */
   case class RightIff(phi: Formula, psi: Formula) extends ProofStepWithoutBotNorPrem(2) {
-    def asSCProof(bot: Sequent, premises: Seq[Int], currentProof: Library#Proof): ProofStepJudgement =
-      SC.RightIff(bot, premises(0), premises(1), phi, psi)
+    def asSCProof(bot: Sequent, premises: Seq[Int], currentProof: Library#Proof): ProofStepJudgement = {
+      def invalid(msg: String) = ProofStepJudgement.InvalidProofStep(
+        this.asProofStepWithoutBot(premises).asProofStep(bot),
+        msg
+      )
+
+      lazy val leftSequent = currentProof.getSequent(premises(0))
+      lazy val rightSequent = currentProof.getSequent(premises(1))
+      lazy val implication = ConnectorFormula(Iff, Seq(phi, psi))
+      lazy val impLeft = ConnectorFormula(Implies, Seq(phi, psi))
+      lazy val impRight = ConnectorFormula(Implies, Seq(psi, phi))
+
+      if (premises.length != 2)
+        invalid(s"Two premises expected, ${premises.length} received.")
+      else if (!isSameSet(bot.left, leftSequent.left union rightSequent.left))
+        invalid("Left-hand side of conclusion is not the union of the left-hand sides of the premises.")
+      else if (!isSameSet(bot.right + impLeft + impRight, leftSequent.right union rightSequent.right + implication))
+        invalid("Right-hand side of conclusion + φ→ψ + ψ→φ is not the same as the union of the right-hand sides of the premises + φ↔ψ.")
+      else
+        SC.RightIff(bot, premises(0), premises(1), phi, psi)
+    }
   }
 
-  case class RightIffWithoutFormula() extends ProofStepWithoutBotNorPrem(2) {
+  case object RightIffWithoutFormula extends ProofStepWithoutBotNorPrem(2) {
     def asSCProof(bot: Sequent, premises: Seq[Int], currentProof: Library#Proof): ProofStepJudgement = {
-      val premiseSequent = currentProof.getSequent(premises(0))
-      val pivot = premiseSequent.right.diff(bot.right)
+      def invalid(msg: String) = ProofStepJudgement.InvalidProofStep(
+        this.asProofStepWithoutBot(premises).asProofStep(bot),
+        msg
+      )
 
-      if (pivot.isEmpty)
-        SC.Weakening(bot, premises(0))
+      lazy val premiseSequent = currentProof.getSequent(premises(0))
+      lazy val pivot = premiseSequent.right.diff(bot.right)
+
+      if (premises.length != 2)
+        invalid(s"Two premises expected, ${premises.length} received.")
+      else if (pivot.isEmpty)
+        Weakening.asSCProof(bot, Seq(premises(0)), currentProof)
       else if (pivot.tail.isEmpty)
         pivot.head match {
-          case ConnectorFormula(Implies, Seq(phi, psi)) => SC.RightIff(bot, premises(0), premises(1), phi, psi)
-          case _ => ProofStepJudgement.InvalidProofStep(this.asProofStepWithoutBot(premises).asProofStep(bot), "Could not infer an implication as pivot from premise and conclusion.")
+          case ConnectorFormula(Implies, Seq(phi, psi)) => RightIff(phi, psi).asSCProof(bot, premises, currentProof)
+          case _ => invalid("Could not infer an implication as pivot from premise and conclusion.")
         }
       else
-        ProofStepJudgement.InvalidProofStep(
-          this.asProofStepWithoutBot(premises).asProofStep(bot),
-          "Right-hand side of conclusion + φ→ψ + ψ→φ is not the same as the union of the right-hand sides of the premises φ↔ψ."
-        )
+        invalid("Right-hand side of conclusion + φ→ψ + ψ→φ is not the same as the union of the right-hand sides of the premises φ↔ψ.")
     }
   }
 
   case object RightIff extends ProofStepWithoutBotNorPrem(2) {
     // default construction:
     // def apply(phi: Formula, psi: Formula) = new RightIff(phi, psi)
-    def apply() = new RightIffWithoutFormula()
+    def apply() = RightIffWithoutFormula
 
     // usage without an argument list
     def asSCProof(bot: Sequent, premises: Seq[Int], currentProof: Library#Proof): ProofStepJudgement =
@@ -608,27 +935,50 @@ object BasicStepTactic {
 
   /**
    * <pre>
-   *  Γ, φ |- Δ
+   *   Γ, φ |- Δ
    * --------------
    *   Γ |- ¬φ, Δ
    * </pre>
    */
   case class RightNot(phi: Formula) extends ProofStepWithoutBotNorPrem(1) {
-    def asSCProof(bot: Sequent, premises: Seq[Int], currentProof: Library#Proof): ProofStepJudgement =
-      SC.RightNot(bot, premises(0), phi)
+    def asSCProof(bot: Sequent, premises: Seq[Int], currentProof: Library#Proof): ProofStepJudgement = {
+      def invalid(msg: String) = ProofStepJudgement.InvalidProofStep(
+        this.asProofStepWithoutBot(premises).asProofStep(bot),
+        msg
+      )
+
+      lazy val premiseSequent = currentProof.getSequent(premises(0))
+      lazy val negation = ConnectorFormula(Neg, Seq(phi))
+
+      if (premises.length != 1)
+        invalid(s"One premise expected, ${premises.length} received.")
+      else if (!isSameSet(bot.left + phi, premiseSequent.left))
+        invalid("Left-hand side of conclusion + φ is not the same as left-hand side of premise.")
+      else if (!isSameSet(bot.right, premiseSequent.right + negation))
+        invalid("Right-hand side of conclusion is not the same as right-hand side of premise + ¬φ.")
+      else
+        SC.RightNot(bot, premises(0), phi)
+    }
   }
 
-  case class RightNotWithoutFormula() extends ProofStepWithoutBotNorPrem(1) {
+  case object RightNotWithoutFormula extends ProofStepWithoutBotNorPrem(1) {
     def asSCProof(bot: Sequent, premises: Seq[Int], currentProof: Library#Proof): ProofStepJudgement = {
-      val premiseSequent = currentProof.getSequent(premises(0))
-      val pivot = premiseSequent.left.diff(bot.left)
+      def invalid(msg: String) = ProofStepJudgement.InvalidProofStep(
+        this.asProofStepWithoutBot(premises).asProofStep(bot),
+        msg
+      )
 
-      if (pivot.isEmpty)
-        SC.Weakening(bot, premises(0))
+      lazy val premiseSequent = currentProof.getSequent(premises(0))
+      lazy val pivot = premiseSequent.left.diff(bot.left)
+
+      if (premises.length != 1)
+        invalid(s"One premise expected, ${premises.length} received.")
+      else if (pivot.isEmpty)
+        Weakening.asSCProof(bot, Seq(premises(0)), currentProof)
       else if (pivot.tail.isEmpty)
-        SC.RightNot(bot, premises(0), pivot.head)
+        RightNot(pivot.head).asSCProof(bot, premises, currentProof)
       else
-        ProofStepJudgement.InvalidProofStep(this.asProofStepWithoutBot(premises).asProofStep(bot), "Left-hand side of conclusion + φ must be the same as left-hand side of premise.")
+        invalid("Left-hand side of conclusion + φ is not the same as left-hand side of premise.")
 
     }
   }
@@ -636,7 +986,7 @@ object BasicStepTactic {
   case object RightNot extends ProofStepWithoutBotNorPrem(1) {
     // default construction:
     // def apply(phi: Formula) = new RightNot(phi)
-    def apply() = new RightNotWithoutFormula()
+    def apply() = RightNotWithoutFormula
 
     // usage without an argument list
     def asSCProof(bot: Sequent, premises: Seq[Int], currentProof: Library#Proof): ProofStepJudgement =
@@ -651,18 +1001,43 @@ object BasicStepTactic {
    * </pre>
    */
   case class RightForall(phi: Formula, x: VariableLabel) extends ProofStepWithoutBotNorPrem(1) {
-    def asSCProof(bot: Sequent, premises: Seq[Int], currentProof: Library#Proof): ProofStepJudgement =
-      SC.RightForall(bot, premises(0), phi, x)
+    def asSCProof(bot: Sequent, premises: Seq[Int], currentProof: Library#Proof): ProofStepJudgement = {
+      def invalid(msg: String) = ProofStepJudgement.InvalidProofStep(
+        this.asProofStepWithoutBot(premises).asProofStep(bot),
+        msg
+      )
+
+      lazy val premiseSequent = currentProof.getSequent(premises(0))
+      lazy val quantified = BinderFormula(Forall, x, phi)
+
+      if (premises.length != 1)
+        invalid(s"One premise expected, ${premises.length} received.")
+      else if ((bot.left union bot.right).exists(_.freeVariables.contains(x)))
+        invalid("The variable x is free in the resulting sequent.")
+      else if (!isSameSet(bot.left, premiseSequent.left))
+        invalid("Left-hand side of conclusion is not the same as left-hand side of premise.")
+      else if (!isSameSet(bot.right + phi, premiseSequent.right + quantified))
+        invalid("Right-hand side of conclusion + φ is not the same as right-hand side of premise + ∀x. φ.")
+      else
+        SC.RightForall(bot, premises(0), phi, x)
+    }
   }
 
-  case class RightForallWithoutFormula() extends ProofStepWithoutBotNorPrem(1) {
+  case object RightForallWithoutFormula extends ProofStepWithoutBotNorPrem(1) {
     def asSCProof(bot: Sequent, premises: Seq[Int], currentProof: Library#Proof): ProofStepJudgement = {
-      val premiseSequent = currentProof.getSequent(premises(0))
-      val pivot = bot.right.diff(premiseSequent.right)
+      def invalid(msg: String) = ProofStepJudgement.InvalidProofStep(
+        this.asProofStepWithoutBot(premises).asProofStep(bot),
+        msg
+      )
+
+      lazy val premiseSequent = currentProof.getSequent(premises(0))
+      lazy val pivot = bot.right.diff(premiseSequent.right)
       lazy val instantiatedPivot = premiseSequent.right.diff(bot.right)
 
-      if (pivot.isEmpty)
-        if (instantiatedPivot.isEmpty) SC.Rewrite(bot, premises(0))
+      if (premises.length != 1)
+        invalid(s"One premise expected, ${premises.length} received.")
+      else if (pivot.isEmpty)
+        if (instantiatedPivot.isEmpty) Rewrite.asSCProof(bot, Seq(premises(0)), currentProof)
         else if (instantiatedPivot.tail.isEmpty) {
           val in: Formula = instantiatedPivot.head
           val quantifiedPhi: Option[Formula] = bot.right.find(f =>
@@ -673,24 +1048,24 @@ object BasicStepTactic {
           )
 
           quantifiedPhi match {
-            case Some(BinderFormula(Forall, x, phi)) => SC.RightForall(bot, premises(0), phi, x)
-            case _ => ProofStepJudgement.InvalidProofStep(this.asProofStepWithoutBot(premises).asProofStep(bot), "Could not infer a universally quantified pivot from premise and conclusion.")
+            case Some(BinderFormula(Forall, x, phi)) => RightForall(phi, x).asSCProof(bot, premises, currentProof)
+            case _ => invalid("Could not infer a universally quantified pivot from premise and conclusion.")
           }
-        } else ProofStepJudgement.InvalidProofStep(this.asProofStepWithoutBot(premises).asProofStep(bot), "Right-hand side of conclusion + φ must be the same as right-hand side of premise + ∃x. φ.")
+        } else invalid("Right-hand side of conclusion + φ is not the same as right-hand side of premise + ∃x. φ.")
       else if (pivot.tail.isEmpty)
         pivot.head match {
-          case BinderFormula(Forall, x, phi) => SC.RightForall(bot, premises(0), phi, x)
-          case _ => ProofStepJudgement.InvalidProofStep(this.asProofStepWithoutBot(premises).asProofStep(bot), "Could not infer a universally quantified pivot from premise and conclusion.")
+          case BinderFormula(Forall, x, phi) => RightForall(phi, x).asSCProof(bot, premises, currentProof)
+          case _ => invalid("Could not infer a universally quantified pivot from premise and conclusion.")
         }
       else
-        ProofStepJudgement.InvalidProofStep(this.asProofStepWithoutBot(premises).asProofStep(bot), "Right-hand side of conclusion + φ must be the same as right-hand side of premise + ∃x. φ.")
+        invalid("Right-hand side of conclusion + φ is not the same as right-hand side of premise + ∃x. φ.")
     }
   }
 
   case object RightForall extends ProofStepWithoutBotNorPrem(1) {
     // default construction:
     // def apply(phi: Formula, x: VariableLabel) = new RightForall(phi, x)
-    def apply() = new RightForallWithoutFormula()
+    def apply() = RightForallWithoutFormula
 
     // usage without an argument list
     def asSCProof(bot: Sequent, premises: Seq[Int], currentProof: Library#Proof): ProofStepJudgement =
@@ -703,32 +1078,51 @@ object BasicStepTactic {
    * -------------------
    *  Γ |- ∃x. φ, Δ
    *
-   * (ln-x stands for locally nameless x)
    * </pre>
    */
   case class RightExists(phi: Formula, x: VariableLabel, t: Term) extends ProofStepWithoutBotNorPrem(1) {
-    def asSCProof(bot: Sequent, premises: Seq[Int], currentProof: Library#Proof): ProofStepJudgement =
-      SC.RightExists(bot, premises(0), phi, x, t)
+    def asSCProof(bot: Sequent, premises: Seq[Int], currentProof: Library#Proof): ProofStepJudgement = {
+      def invalid(msg: String) = ProofStepJudgement.InvalidProofStep(
+        this.asProofStepWithoutBot(premises).asProofStep(bot),
+        msg
+      )
+
+      lazy val premiseSequent = currentProof.getSequent(premises(0))
+      lazy val quantified = BinderFormula(Exists, x, phi)
+      lazy val instantiated = substituteVariables(phi, Map(x -> t))
+
+      if (premises.length != 1)
+        invalid(s"One premise expected, ${premises.length} received.")
+      else if (!isSameSet(bot.left, premiseSequent.left))
+        invalid("Left-hand side of conclusion is not the same as left-hand side of premise")
+      else if (!isSameSet(bot.right + instantiated, premiseSequent.right + quantified))
+        invalid("Right-hand side of conclusion + φ[t/x] is not the same as right-hand side of premise + ∃x. φ")
+      else
+        SC.RightExists(bot, premises(0), phi, x, t)
+    }
   }
 
   case class RightExistsWithoutFormula(t: Term) extends ProofStepWithoutBotNorPrem(1) {
     def asSCProof(bot: Sequent, premises: Seq[Int], currentProof: Library#Proof): ProofStepJudgement = {
-      val premiseSequent = currentProof.getSequent(premises(0))
-      val pivot = bot.right.diff(premiseSequent.right)
+      def invalid(msg: String) = ProofStepJudgement.InvalidProofStep(
+        this.asProofStepWithoutBot(premises).asProofStep(bot),
+        msg
+      )
+
+      lazy val premiseSequent = currentProof.getSequent(premises(0))
+      lazy val pivot = bot.right.diff(premiseSequent.right)
       lazy val instantiatedPivot = premiseSequent.right.diff(bot.right)
 
-      if (!pivot.isEmpty)
+      if (premises.length != 1) invalid(s"One premise expected, ${premises.length} received.")
+      else if (!pivot.isEmpty)
         if (pivot.tail.isEmpty)
           pivot.head match {
-            case BinderFormula(Exists, x, phi) => SC.RightExists(bot, premises(0), phi, x, t)
-            case _ => ProofStepJudgement.InvalidProofStep(this.asProofStepWithoutBot(premises).asProofStep(bot), "Could not infer an existentially quantified pivot from premise and conclusion.")
+            case BinderFormula(Exists, x, phi) => RightExists(phi, x, t).asSCProof(bot, premises, currentProof)
+            case _ => invalid("Could not infer an existentially quantified pivot from premise and conclusion.")
           }
         else
-          ProofStepJudgement.InvalidProofStep(
-            this.asProofStepWithoutBot(premises).asProofStep(bot),
-            "Right-hand side of conclusion + φ[t/x] must be the same as right-hand side of premise + ∀x. φ."
-          )
-      else if (instantiatedPivot.isEmpty) SC.Weakening(bot, premises(0))
+          invalid("Right-hand side of conclusion + φ[t/x] is not the same as right-hand side of premise + ∀x. φ.")
+      else if (instantiatedPivot.isEmpty) Weakening.asSCProof(bot, premises, currentProof)
       else if (instantiatedPivot.tail.isEmpty) {
         // go through conclusion to find a matching quantified formula
 
@@ -741,14 +1135,10 @@ object BasicStepTactic {
         )
 
         quantifiedPhi match {
-          case Some(BinderFormula(Exists, x, phi)) => SC.RightExists(bot, premises(0), phi, x, t)
-          case _ => ProofStepJudgement.InvalidProofStep(this.asProofStepWithoutBot(premises).asProofStep(bot), "Could not infer an existentially quantified pivot from premise and conclusion.")
+          case Some(BinderFormula(Exists, x, phi)) => RightExists(phi, x, t).asSCProof(bot, premises, currentProof)
+          case _ => invalid("Could not infer an existentially quantified pivot from premise and conclusion.")
         }
-      } else
-        ProofStepJudgement.InvalidProofStep(
-          this.asProofStepWithoutBot(premises).asProofStep(bot),
-          "Right-hand side of conclusion + φ[t/x] must be the same as right-hand side of premise + ∀x. φ."
-        )
+      } else invalid("Right-hand side of conclusion + φ[t/x] is not the same as right-hand side of premise + ∀x. φ.")
     }
   }
 
@@ -774,41 +1164,66 @@ object BasicStepTactic {
    * </pre>
    */
   case class RightExistsOne(phi: Formula, x: VariableLabel) extends ProofStepWithoutBotNorPrem(1) {
-    def asSCProof(bot: Sequent, premises: Seq[Int], currentProof: Library#Proof): ProofStepJudgement =
-      SC.RightExistsOne(bot, premises(0), phi, x)
+    def asSCProof(bot: Sequent, premises: Seq[Int], currentProof: Library#Proof): ProofStepJudgement = {
+      def invalid(msg: String) = ProofStepJudgement.InvalidProofStep(
+        this.asProofStepWithoutBot(premises).asProofStep(bot),
+        msg
+      )
+
+      lazy val premiseSequent = currentProof.getSequent(premises(0))
+      lazy val y = VariableLabel(freshId(phi.freeVariables.map(_.id) + x.id, "y"))
+      lazy val instantiated = BinderFormula(Exists, y, BinderFormula(Forall, x, ConnectorFormula(Iff, List(PredicateFormula(equality, List(VariableTerm(x), VariableTerm(y))), phi))))
+      lazy val quantified = BinderFormula(ExistsOne, x, phi)
+
+      if (premises.length != 1)
+        invalid(s"One premise expected, ${premises.length} received.")
+      else if (!isSameSet(bot.left, premiseSequent.left))
+        invalid("Left-hand side of conclusion is not the same as left-hand side of premise.")
+      else if (!isSameSet(bot.right + instantiated, premiseSequent.right + quantified))
+        invalid("Right-hand side of conclusion + ∃y.∀x. (x=y) ↔ φ is not the same as right-hand side of premise + ∃!x. φ.")
+      else
+        SC.RightExistsOne(bot, premises(0), phi, x)
+    }
   }
 
-  case class RightExistsOneWithoutFormula() extends ProofStepWithoutBotNorPrem(1) {
+  case object RightExistsOneWithoutFormula extends ProofStepWithoutBotNorPrem(1) {
     def asSCProof(bot: Sequent, premises: Seq[Int], currentProof: Library#Proof): ProofStepJudgement = {
-      val premiseSequent = currentProof.getSequent(premises(0))
-      val pivot = bot.right.diff(premiseSequent.right)
+      def invalid(msg: String) = ProofStepJudgement.InvalidProofStep(
+        this.asProofStepWithoutBot(premises).asProofStep(bot),
+        msg
+      )
+
+      lazy val premiseSequent = currentProof.getSequent(premises(0))
+      lazy val pivot = bot.right.diff(premiseSequent.right)
       lazy val instantiatedPivot = premiseSequent.right.diff(bot.right)
 
-      if (pivot.isEmpty)
+      if (premises.length != 1)
+        invalid(s"One premise expected, ${premises.length} received.")
+      else if (pivot.isEmpty)
         if (instantiatedPivot.isEmpty)
-          SC.Rewrite(bot, premises(0))
+          Rewrite.asSCProof(bot, premises, currentProof)
         else if (instantiatedPivot.tail.isEmpty) {
           instantiatedPivot.head match {
             // ∃_. ∀x. _ ↔ φ == extract ==> x, phi
-            case BinderFormula(Exists, _, BinderFormula(Forall, x, ConnectorFormula(Iff, Seq(_, phi)))) => SC.RightExistsOne(bot, premises(0), phi, x)
-            case _ => ProofStepJudgement.InvalidProofStep(this.asProofStepWithoutBot(premises).asProofStep(bot), "Could not infer an existentially quantified pivot from premise and conclusion.")
+            case BinderFormula(Exists, _, BinderFormula(Forall, x, ConnectorFormula(Iff, Seq(_, phi)))) => RightExistsOne(phi, x).asSCProof(bot, premises, currentProof)
+            case _ => invalid("Could not infer an existentially quantified pivot from premise and conclusion.")
           }
         } else
-          ProofStepJudgement.InvalidProofStep(this.asProofStepWithoutBot(premises).asProofStep(bot), "Right-hand side of conclusion + φ must be the same as right-hand side of premise + ∃x. φ.")
+          invalid("Right-hand side of conclusion + φ is not the same as right-hand side of premise + ∃x. φ.")
       else if (pivot.tail.isEmpty)
         pivot.head match {
-          case BinderFormula(ExistsOne, x, phi) => SC.RightExistsOne(bot, premises(0), phi, x)
-          case _ => ProofStepJudgement.InvalidProofStep(this.asProofStepWithoutBot(premises).asProofStep(bot), "Could not infer an existentially quantified pivot from premise and conclusion.")
+          case BinderFormula(ExistsOne, x, phi) => RightExistsOne(phi, x).asSCProof(bot, premises, currentProof)
+          case _ => invalid("Could not infer an existentially quantified pivot from premise and conclusion.")
         }
       else
-        ProofStepJudgement.InvalidProofStep(this.asProofStepWithoutBot(premises).asProofStep(bot), "Right-hand side of conclusion + φ must be the same as right-hand side of premise + ∃x. φ.")
+        invalid("Right-hand side of conclusion + φ is not the same as right-hand side of premise + ∃x. φ.")
     }
   }
 
   case object RightExistsOne extends ProofStepWithoutBotNorPrem(1) {
     // default construction:
     // def apply(phi: Formula, x: VariableLabel) = new RightExistsOne(phi, x)
-    def apply() = new RightExistsOneWithoutFormula()
+    def apply() = RightExistsOneWithoutFormula
 
     // usage without an argument list
     def asSCProof(bot: Sequent, premises: Seq[Int], currentProof: Library#Proof): ProofStepJudgement =
@@ -824,8 +1239,23 @@ object BasicStepTactic {
    * </pre>
    */
   case object Weakening extends ProofStepWithoutBotNorPrem(1) {
-    def asSCProof(bot: Sequent, premises: Seq[Int], currentProof: Library#Proof): ProofStepJudgement =
-      SC.Weakening(bot, premises(0))
+    def asSCProof(bot: Sequent, premises: Seq[Int], currentProof: Library#Proof): ProofStepJudgement = {
+      def invalid(msg: String) = ProofStepJudgement.InvalidProofStep(
+        this.asProofStepWithoutBot(premises).asProofStep(bot),
+        msg
+      )
+
+      lazy val premiseSequent = currentProof.getSequent(premises(0))
+
+      if (premises.length != 1)
+        invalid(s"One premise expected, ${premises.length} received.")
+      else if (!isSubset(premiseSequent.left, bot.left))
+        invalid("Left-hand side of conclusion is not the same as left-hand side of premise.")
+      else if (!isSubset(premiseSequent.right, bot.right))
+        invalid("Left-hand side of premise is not a subset of left-hand side of conclusion.")
+      else
+        SC.Weakening(bot, premises(0))
+    }
   }
 
   // Equality Rules
@@ -836,20 +1266,56 @@ object BasicStepTactic {
    *     Γ |- Δ
    * </pre>
    */
-  case class LeftRefl(fa: Formula) extends ProofStepWithoutBotNorPrem(1) {
-    def asSCProof(bot: Sequent, premises: Seq[Int], currentProof: Library#Proof): ProofStepJudgement =
-      SC.LeftRefl(bot, premises(0), fa)
+  case class LeftRefl(phi: Formula) extends ProofStepWithoutBotNorPrem(1) {
+    def asSCProof(bot: Sequent, premises: Seq[Int], currentProof: Library#Proof): ProofStepJudgement = {
+      def invalid(msg: String) = ProofStepJudgement.InvalidProofStep(
+        this.asProofStepWithoutBot(premises).asProofStep(bot),
+        msg
+      )
+
+      lazy val premiseSequent = currentProof.getSequent(premises(0))
+
+      if (premises.length != 1)
+        invalid(s"One premise expected, ${premises.length} received.")
+      else if (!isSameSet(bot.left + phi, premiseSequent.left))
+        invalid("Left-hand sides of the conclusion + φ is not the same as left-hand side of the premise.")
+      else if (!isSameSet(bot.right, premiseSequent.right))
+        invalid("Right-hand side of the premise is not the same as the right-hand side of the conclusion.")
+      else
+        phi match {
+          case PredicateFormula(`equality`, Seq(left, right)) =>
+            if (isSame(left, right))
+              SC.LeftRefl(bot, premises(0), phi)
+            else
+              invalid("φ is not an instance of reflexivity.")
+          case _ => invalid("φ is not an equality.")
+        }
+    }
   }
 
-  case class LeftReflWithoutFormula() extends ProofStepWithoutBotNorPrem(1) {
-    def asSCProof(bot: Sequent, premises: Seq[Int], currentProof: Library#Proof): ProofStepJudgement =
-      SC.Rewrite(bot, premises(0))
+  case object LeftReflWithoutFormula extends ProofStepWithoutBotNorPrem(1) {
+    def asSCProof(bot: Sequent, premises: Seq[Int], currentProof: Library#Proof): ProofStepJudgement = {
+      def invalid(msg: String) = ProofStepJudgement.InvalidProofStep(
+        this.asProofStepWithoutBot(premises).asProofStep(bot),
+        msg
+      )
+
+      lazy val premiseSequent = currentProof.getSequent(premises(0))
+      lazy val pivot = premiseSequent.left.diff(bot.left)
+
+      if (premises.length != 1)
+        invalid(s"One premise expected, ${premises.length} received.")
+      else if (!pivot.isEmpty && pivot.tail.isEmpty)
+        LeftRefl(pivot.head).asSCProof(bot, premises, currentProof)
+      else
+        invalid("Could not infer an equality as pivot from premise and conclusion.")
+    }
   }
 
   case object LeftRefl extends ProofStepWithoutBotNorPrem(1) {
     // default construction:
     // def apply(fa: Formula) = new LeftRefl(fa)
-    def apply() = new LeftReflWithoutFormula()
+    def apply() = LeftReflWithoutFormula
 
     // usage without an argument list
     def asSCProof(bot: Sequent, premises: Seq[Int], currentProof: Library#Proof): ProofStepJudgement =
@@ -863,20 +1329,61 @@ object BasicStepTactic {
    *     |- s=s
    * </pre>
    */
-  case class RightRefl(fa: Formula) extends ProofStepWithoutBotNorPrem(0) {
-    def asSCProof(bot: Sequent, premises: Seq[Int], currentProof: Library#Proof): ProofStepJudgement =
-      SC.RightRefl(bot, fa)
+  case class RightRefl(phi: Formula) extends ProofStepWithoutBotNorPrem(0) {
+    def asSCProof(bot: Sequent, premises: Seq[Int], currentProof: Library#Proof): ProofStepJudgement = {
+      def invalid(msg: String) = ProofStepJudgement.InvalidProofStep(
+        this.asProofStepWithoutBot(premises).asProofStep(bot),
+        msg
+      )
+
+      if (premises.length != 0)
+        invalid(s"No premises expected, ${premises.length} received.")
+      else if (!contains(bot.right, phi))
+        invalid("Right-hand side of conclusion does not contain φ.")
+      else
+        phi match {
+          case PredicateFormula(`equality`, Seq(left, right)) =>
+            if (isSame(left, right))
+              SC.RightRefl(bot, phi)
+            else
+              invalid("φ is not an instance of reflexivity.")
+          case _ => invalid("φ is not an equality.")
+        }
+    }
   }
 
-  case class RightReflWithoutFormula() extends ProofStepWithoutBotNorPrem(0) {
-    def asSCProof(bot: Sequent, premises: Seq[Int], currentProof: Library#Proof): ProofStepJudgement =
-      SC.RewriteTrue(bot)
+  case object RightReflWithoutFormula extends ProofStepWithoutBotNorPrem(0) {
+    def asSCProof(bot: Sequent, premises: Seq[Int], currentProof: Library#Proof): ProofStepJudgement = {
+      def invalid(msg: String) = ProofStepJudgement.InvalidProofStep(
+        this.asProofStepWithoutBot(premises).asProofStep(bot),
+        msg
+      )
+
+      if (premises.length != 0) invalid(s"No premises expected, ${premises.length} received.")
+      else if (bot.right.isEmpty) invalid("Right-hand side of conclusion does not contain an instance of reflexivity.")
+      else {
+        // go through conclusion to see if you can find an reflexive formula
+        val pivot: Option[Formula] = bot.right.find(f =>
+          f match {
+            case PredicateFormula(`equality`, Seq(l, r)) => isSame(l, r)
+            case _ => false
+          }
+        )
+
+        pivot match {
+          case Some(phi) => RightRefl(phi).asSCProof(bot, premises, currentProof)
+          case _ => invalid("Could not infer an equality as pivot from conclusion.")
+        }
+
+      }
+
+    }
   }
 
   case object RightRefl extends ProofStepWithoutBotNorPrem(0) {
     // default construction:
     // def apply(fa: Formula) = new RightRefl(fa)
-    def apply() = new RightReflWithoutFormula()
+    def apply() = RightReflWithoutFormula
 
     // usage without an argument list
     def asSCProof(bot: Sequent, premises: Seq[Int], currentProof: Library#Proof): ProofStepJudgement =
@@ -891,8 +1398,30 @@ object BasicStepTactic {
    * </pre>
    */
   case class LeftSubstEq(equals: List[(Term, Term)], lambdaPhi: LambdaTermFormula) extends ProofStepWithoutBotNorPrem(1) {
-    def asSCProof(bot: Sequent, premises: Seq[Int], currentProof: Library#Proof): ProofStepJudgement =
-      SC.LeftSubstEq(bot, premises(0), equals, lambdaPhi)
+    def asSCProof(bot: Sequent, premises: Seq[Int], currentProof: Library#Proof): ProofStepJudgement = {
+      def invalid(msg: String) = ProofStepJudgement.InvalidProofStep(
+        this.asProofStepWithoutBot(premises).asProofStep(bot),
+        msg
+      )
+
+      lazy val premiseSequent = currentProof.getSequent(premises(0))
+      lazy val (s_es, t_es) = equals.unzip
+      lazy val phi_s = lambdaPhi(s_es)
+      lazy val phi_t = lambdaPhi(t_es)
+      lazy val equalities = equals map { case (s, t) => PredicateFormula(equality, Seq(s, t)) }
+
+      if (premises.length != 1)
+        invalid(s"One premise expected, ${premises.length} received.")
+      else if (!isSameSet(bot.right, premiseSequent.right))
+        invalid("Right-hand side of the premise is not the same as the right-hand side of the conclusion.")
+      else if (
+        !isSameSet(bot.left + phi_s, premiseSequent.left ++ equalities + phi_t) &&
+        !isSameSet(bot.left + phi_t, premiseSequent.left ++ equalities + phi_s)
+      )
+        invalid("Left-hand side of the conclusion + φ(s_) is not the same as left-hand side of the premise + (s=t)_ + φ(t_) (or with s_ and t_ swapped).")
+      else
+        SC.LeftSubstEq(bot, premises(0), equals, lambdaPhi)
+    }
   }
 
   /**
@@ -903,8 +1432,30 @@ object BasicStepTactic {
    * </pre>
    */
   case class RightSubstEq(equals: List[(Term, Term)], lambdaPhi: LambdaTermFormula) extends ProofStepWithoutBotNorPrem(1) {
-    def asSCProof(bot: Sequent, premises: Seq[Int], currentProof: Library#Proof): ProofStepJudgement =
-      SC.RightSubstEq(bot, premises(0), equals, lambdaPhi)
+    def asSCProof(bot: Sequent, premises: Seq[Int], currentProof: Library#Proof): ProofStepJudgement = {
+      def invalid(msg: String) = ProofStepJudgement.InvalidProofStep(
+        this.asProofStepWithoutBot(premises).asProofStep(bot),
+        msg
+      )
+
+      lazy val premiseSequent = currentProof.getSequent(premises(0))
+      lazy val (s_es, t_es) = equals.unzip
+      lazy val phi_s = lambdaPhi(s_es)
+      lazy val phi_t = lambdaPhi(t_es)
+      lazy val equalities = equals map { case (s, t) => PredicateFormula(equality, Seq(s, t)) }
+
+      if (premises.length != 1)
+        invalid(s"One premise expected, ${premises.length} received.")
+      else if (!isSameSet(bot.left, premiseSequent.left ++ equalities))
+        invalid("Left-hand side of the conclusion is not the same as the left-hand side of the premise + (s=t)_.")
+      else if (
+        !isSameSet(bot.left + phi_s, premiseSequent.left + phi_t) &&
+        !isSameSet(bot.left + phi_t, premiseSequent.left + phi_s)
+      )
+        invalid("Right-hand side of the conclusion + φ(s_) is not the same as right-hand side of the premise + φ(t_) (or with s_ and t_ swapped).")
+      else
+        SC.RightSubstEq(bot, premises(0), equals, lambdaPhi)
+    }
   }
 
   /**
@@ -915,8 +1466,30 @@ object BasicStepTactic {
    * </pre>
    */
   case class LeftSubstIff(equals: List[(Formula, Formula)], lambdaPhi: LambdaFormulaFormula) extends ProofStepWithoutBotNorPrem(1) {
-    def asSCProof(bot: Sequent, premises: Seq[Int], currentProof: Library#Proof): ProofStepJudgement =
-      SC.LeftSubstIff(bot, premises(0), equals, lambdaPhi)
+    def asSCProof(bot: Sequent, premises: Seq[Int], currentProof: Library#Proof): ProofStepJudgement = {
+      def invalid(msg: String) = ProofStepJudgement.InvalidProofStep(
+        this.asProofStepWithoutBot(premises).asProofStep(bot),
+        msg
+      )
+
+      lazy val premiseSequent = currentProof.getSequent(premises(0))
+      lazy val (psi_es, tau_es) = equals.unzip
+      lazy val phi_psi = lambdaPhi(psi_es)
+      lazy val phi_tau = lambdaPhi(tau_es)
+      lazy val implications = equals map { case (s, t) => ConnectorFormula(Iff, Seq(s, t)) }
+
+      if (premises.length != 1)
+        invalid(s"One premise expected, ${premises.length} received.")
+      else if (!isSameSet(bot.right, premiseSequent.right))
+        invalid("Right-hand side of the premise is not the same as the right-hand side of the conclusion.")
+      else if (
+        !isSameSet(bot.left + phi_psi, premiseSequent.left ++ implications + phi_tau) &&
+        !isSameSet(bot.left + phi_tau, premiseSequent.left ++ implications + phi_psi)
+      )
+        invalid("Left-hand side of the conclusion + φ(ψ_) is not the same as left-hand side of the premise + (ψ ↔ τ)_ + φ(τ_) (or with ψ_ and τ_ swapped).")
+      else
+        SC.LeftSubstIff(bot, premises(0), equals, lambdaPhi)
+    }
   }
 
   /**
@@ -927,8 +1500,30 @@ object BasicStepTactic {
    * </pre>
    */
   case class RightSubstIff(equals: List[(Formula, Formula)], lambdaPhi: LambdaFormulaFormula) extends ProofStepWithoutBotNorPrem(1) {
-    def asSCProof(bot: Sequent, premises: Seq[Int], currentProof: Library#Proof): ProofStepJudgement =
-      SC.RightSubstIff(bot, premises(0), equals, lambdaPhi)
+    def asSCProof(bot: Sequent, premises: Seq[Int], currentProof: Library#Proof): ProofStepJudgement = {
+      def invalid(msg: String) = ProofStepJudgement.InvalidProofStep(
+        this.asProofStepWithoutBot(premises).asProofStep(bot),
+        msg
+      )
+
+      lazy val premiseSequent = currentProof.getSequent(premises(0))
+      lazy val (psi_es, tau_es) = equals.unzip
+      lazy val phi_psi = lambdaPhi(psi_es)
+      lazy val phi_tau = lambdaPhi(tau_es)
+      lazy val implications = equals map { case (s, t) => ConnectorFormula(Iff, Seq(s, t)) }
+
+      if (premises.length != 1)
+        invalid(s"One premise expected, ${premises.length} received.")
+      else if (!isSameSet(bot.left, premiseSequent.left ++ implications))
+        invalid("Left-hand side of the conclusion is not the same as the left-hand side of the premise + (ψ ↔ τ)_.")
+      else if (
+        !isSameSet(bot.left + phi_psi, premiseSequent.left + phi_tau) &&
+        !isSameSet(bot.left + phi_tau, premiseSequent.left + phi_psi)
+      )
+        invalid("Right-hand side of the conclusion + φ(ψ_) is not the same as right-hand side of the premise + φ(τ_) (or with ψ_ and τ_ swapped).")
+      else
+        SC.RightSubstIff(bot, premises(0), equals, lambdaPhi)
+    }
   }
 
   /**
@@ -939,8 +1534,23 @@ object BasicStepTactic {
    * </pre>
    */
   case class InstFunSchema(insts: Map[SchematicTermLabel, LambdaTermTerm]) extends ProofStepWithoutBotNorPrem(1) {
-    def asSCProof(bot: Sequent, premises: Seq[Int], currentProof: Library#Proof): ProofStepJudgement =
-      SC.InstFunSchema(bot, premises(0), insts)
+    def asSCProof(bot: Sequent, premises: Seq[Int], currentProof: Library#Proof): ProofStepJudgement = {
+      def invalid(msg: String) = ProofStepJudgement.InvalidProofStep(
+        this.asProofStepWithoutBot(premises).asProofStep(bot),
+        msg
+      )
+
+      lazy val premiseSequent = currentProof.getSequent(premises(0))
+
+      if (premises.length != 1)
+        invalid(s"One premise expected, ${premises.length} received.")
+      else if (!isSameSet(bot.left, premiseSequent.left.map(instantiateTermSchemas(_, insts))))
+        invalid("Left-hand side of premise instantiated with the map 'insts' is not the same as left-hand side of conclusion.")
+      else if (!isSameSet(bot.right, premiseSequent.right.map(instantiateTermSchemas(_, insts))))
+        invalid("Right-hand side of premise instantiated with the map 'insts' is not the same as right-hand side of conclusion.")
+      else
+        SC.InstFunSchema(bot, premises(0), insts)
+    }
   }
 
   /**
@@ -951,16 +1561,43 @@ object BasicStepTactic {
    * </pre>
    */
   case class InstPredSchema(insts: Map[SchematicVarOrPredLabel, LambdaTermFormula]) extends ProofStepWithoutBotNorPrem(1) {
-    def asSCProof(bot: Sequent, premises: Seq[Int], currentProof: Library#Proof): ProofStepJudgement =
-      SC.InstPredSchema(bot, premises(0), insts)
+    def asSCProof(bot: Sequent, premises: Seq[Int], currentProof: Library#Proof): ProofStepJudgement = {
+      def invalid(msg: String) = ProofStepJudgement.InvalidProofStep(
+        this.asProofStepWithoutBot(premises).asProofStep(bot),
+        msg
+      )
+
+      lazy val premiseSequent = currentProof.getSequent(premises(0))
+
+      if (premises.length != 1)
+        invalid(s"One premise expected, ${premises.length} received.")
+      else if (!isSameSet(bot.left, premiseSequent.left.map(instantiatePredicateSchemas(_, insts))))
+        invalid("Left-hand side of premise instantiated with the map 'insts' is not the same as left-hand side of conclusion.")
+      else if (!isSameSet(bot.right, premiseSequent.right.map(instantiatePredicateSchemas(_, insts))))
+        invalid("Right-hand side of premise instantiated with the map 'insts' is not the same as right-hand side of conclusion.")
+      else
+        SC.InstPredSchema(bot, premises(0), insts)
+    }
   }
 
   // Proof Organisation rules
   case class SCSubproof(sp: SCProof, premises: Seq[Int] = Seq.empty, display: Boolean = true) extends ProofStep {
-    def asSCProof(currentProof: Library#Proof): ProofStepJudgement =
-      sp match {
-        case sp: SCProof => SC.SCSubproof(sp, premises)
-      }
+    def asSCProof(currentProof: Library#Proof): ProofStepJudgement = {
+      def invalid(msg: String) = ProofStepJudgement.InvalidProofStep(
+        this,
+        msg
+      )
+
+      lazy val premiseSequents = premises.map(currentProof.getSequent(_))
+      lazy val invalidPremise = premises.zipWithIndex.find((no, p) => !SC.isSameSequent(premiseSequents(no), sp.imports(p)))
+
+      if (premises.length != sp.imports.length)
+        invalid(s"Subproof expected ${sp.imports.length} premises, ${premises.length} received.")
+      else if (!invalidPremise.isEmpty)
+        invalid(s"Premise number ${invalidPremise.get._1} (refering to step ${invalidPremise.get}) is not the same as import number ${invalidPremise.get._1} of the subproof.")
+      else
+        SC.SCSubproof(sp, premises)
+    }
   }
 
 }