diff --git a/src/main/scala/lisa/KernelHelpers.scala b/src/main/scala/lisa/KernelHelpers.scala
index 1541d31ab35712cdfc4ce11125accf0a6073d702..5b0e55adbd4aa56134a161157ac9e0a3ae417ab4 100644
--- a/src/main/scala/lisa/KernelHelpers.scala
+++ b/src/main/scala/lisa/KernelHelpers.scala
@@ -136,4 +136,14 @@ object KernelHelpers {
extension [A, T1 <: A](left: T1)(using SetConverter[Formula, T1])
infix def |-[B, T2 <: B](right: T2)(using SetConverter[Formula, T2]): Sequent = Sequent(any2set(left), any2set(right))
+
+ def instantiatePredicateSchemaInSequent(s: Sequent, p: SchematicPredicateLabel, psi: Formula, a: Seq[VariableLabel]): Sequent = {
+ s.left.map(phi => instantiatePredicateSchema(phi, p, psi, a)) |- s.right.map(phi => instantiatePredicateSchema(phi, p, psi, a))
+ }
+ def instantiateFunctionSchemaInSequent(s: Sequent, f: SchematicFunctionLabel, r: Term, a: Seq[VariableLabel]): Sequent = {
+ s.left.map(phi => instantiateFunctionSchema(phi, f, r, a)) |- s.right.map(phi => instantiateFunctionSchema(phi, f, r, a))
+ }
+
+
+
}
diff --git a/src/main/scala/lisa/kernel/fol/EquivalenceChecker.scala b/src/main/scala/lisa/kernel/fol/EquivalenceChecker.scala
index a4f79c526ad5ed0fde2ed8eb2bf1dbef6c70bda7..d652b045e0216b9bc272736eedcf85b2f75df041 100644
--- a/src/main/scala/lisa/kernel/fol/EquivalenceChecker.scala
+++ b/src/main/scala/lisa/kernel/fol/EquivalenceChecker.scala
@@ -256,25 +256,31 @@ private[fol] trait EquivalenceChecker extends FormulaDefinitions {
parent.normalForm = Some(NLiteral(true))
parent.normalForm.get :: acc
case SOr(children) =>
- val T = children.sortBy(_.size)
- val r1 = T.tail.foldLeft(List[NormalFormula]())((p, a) => pDisj(a, p))
- val r2 = r1 zip (r1 map (_.code))
- val r3 = r2.sortBy(_._2).distinctBy(_._2).filterNot(_._2 == 0)
- if (r3.isEmpty) pNeg(T.head, parent, acc)
+ if (children.isEmpty) {
+ parent.normalForm = Some(NLiteral(true))
+ parent.normalForm.get :: acc
+ }
else {
- val s1 = pDisj(T.head, r1)
- val s2 = s1 zip (s1 map (_.code))
- val s3 = s2.sortBy(_._2).distinctBy(_._2).filterNot(_._2 == 0)
- if (s3.exists(_._2 == 1) || checkForContradiction(s3) ) {
- phi.normalForm=Some(NLiteral(true))
- parent.normalForm = Some(NLiteral(false))
- parent.normalForm.get :: acc
- } else if (s3.length == 1) {
- pNegNormal(s3.head._1, parent, acc)
- } else {
- phi.normalForm = Some(NOr(s3.map(_._1), updateCodesSig(("or", s3.map(_._2)))))
- parent.normalForm = Some(NNeg(phi.normalForm.get, updateCodesSig(("neg", List(phi.normalForm.get.code)))))
- parent.normalForm.get :: acc
+ val T = children.sortBy(_.size)
+ val r1 = T.tail.foldLeft(List[NormalFormula]())((p, a) => pDisj(a, p))
+ val r2 = r1 zip (r1 map (_.code))
+ val r3 = r2.sortBy(_._2).distinctBy(_._2).filterNot(_._2 == 0)
+ if (r3.isEmpty) pNeg(T.head, parent, acc)
+ else {
+ val s1 = pDisj(T.head, r1)
+ val s2 = s1 zip (s1 map (_.code))
+ val s3 = s2.sortBy(_._2).distinctBy(_._2).filterNot(_._2 == 0)
+ if (s3.exists(_._2 == 1) || checkForContradiction(s3)) {
+ phi.normalForm = Some(NLiteral(true))
+ parent.normalForm = Some(NLiteral(false))
+ parent.normalForm.get :: acc
+ } else if (s3.length == 1) {
+ pNegNormal(s3.head._1, parent, acc)
+ } else {
+ phi.normalForm = Some(NOr(s3.map(_._1), updateCodesSig(("or", s3.map(_._2)))))
+ parent.normalForm = Some(NNeg(phi.normalForm.get, updateCodesSig(("neg", List(phi.normalForm.get.code)))))
+ parent.normalForm.get :: acc
+ }
}
}
}
diff --git a/src/main/scala/lisa/kernel/fol/FormulaDefinitions.scala b/src/main/scala/lisa/kernel/fol/FormulaDefinitions.scala
index da0ab913031b47a7465a2d510c4568b47676060f..d9561a39722ccfb5b7bdea4ca185f19066b98484 100644
--- a/src/main/scala/lisa/kernel/fol/FormulaDefinitions.scala
+++ b/src/main/scala/lisa/kernel/fol/FormulaDefinitions.scala
@@ -79,7 +79,7 @@ private[fol] trait FormulaDefinitions extends FormulaLabelDefinitions with TermD
}
def bindAll(binder: BinderLabel, vars: Seq[VariableLabel], phi:Formula): Formula =
- vars.sortBy(_.name).foldLeft(phi)((f, v) => BinderFormula(binder, v, f))
+ vars.foldLeft(phi)((f, v) => BinderFormula(binder, v, f))
/**
* Performs simultaneous substitution of multiple variables by multiple terms in a formula f.
diff --git a/src/main/scala/lisa/kernel/proof/RunningTheory.scala b/src/main/scala/lisa/kernel/proof/RunningTheory.scala
index 49a4688bc4b56e1e5333e04320da7824ddcc0d88..9c87f3aff0c755478a3d53c729e65942fb15eea0 100644
--- a/src/main/scala/lisa/kernel/proof/RunningTheory.scala
+++ b/src/main/scala/lisa/kernel/proof/RunningTheory.scala
@@ -121,8 +121,9 @@ class RunningTheory {
proof.conclusion match{
case Sequent(l, r) if l.isEmpty && r.size == 1 =>
- val subst = bindAll(ExistsOne, args, phi)
- if (isSame(r.head, subst)){
+ val subst = bindAll(Forall, args, BinderFormula(ExistsOne, out, phi))
+ val subst2 = bindAll(Forall, args.reverse, BinderFormula(ExistsOne, out, phi))
+ if (isSame(r.head, subst) || isSame(r.head, subst2)){
val newDef = FunctionDefinition(label, args, out, phi)
funDefinitions.update(label, Some(newDef))
Some(newDef)
diff --git a/src/main/scala/lisa/kernel/proof/SCProofChecker.scala b/src/main/scala/lisa/kernel/proof/SCProofChecker.scala
index 6602e1cea1c6768b219ec0b6cf68a32d14a9a842..616b2e14537472079bd279ec3e917664fb205ba3 100644
--- a/src/main/scala/lisa/kernel/proof/SCProofChecker.scala
+++ b/src/main/scala/lisa/kernel/proof/SCProofChecker.scala
@@ -429,7 +429,8 @@ object SCProofChecker {
if (isSameSet(bot.left, expected._1))
if (isSameSet(bot.right, expected._2))
SCValidProof
- else SCInvalidProof(Nil, "Right-hand side of premise instantiated with [?p/ψ(a)] must be the same as right-hand side of conclusion.")
+ else
+ SCInvalidProof(Nil, "Right-hand side of premise instantiated with [?p/ψ(a)] must be the same as right-hand side of conclusion.")
else SCInvalidProof(Nil, "Left-hand side of premise instantiated with [?p/ψ(a)] must be the same as left-hand side of conclusion.")
case SCSubproof(sp, premises, _) =>
diff --git a/src/main/scala/lisa/kernel/proof/SequentCalculus.scala b/src/main/scala/lisa/kernel/proof/SequentCalculus.scala
index 5c1470c96a5535899cd8a828835a3128ec1e6fe1..1166e1c46705195f1235e4b6090952d4542464d1 100644
--- a/src/main/scala/lisa/kernel/proof/SequentCalculus.scala
+++ b/src/main/scala/lisa/kernel/proof/SequentCalculus.scala
@@ -284,7 +284,7 @@ object SequentCalculus {
* Γ[r(a)/?f] |- Δ[r(a)/?f]
* </pre>
*/
- case class InstFunSchema(bot:Sequent, t1:Int, f:SchematicFunctionLabel, r:Term, a: Seq[VariableLabel] )
+ case class InstFunSchema(bot:Sequent, t1:Int, f:SchematicFunctionLabel, r:Term, a: Seq[VariableLabel] ) extends SCProofStep{val premises = Seq(t1)}
/**
* <pre>
* Γ |- Δ
@@ -292,7 +292,7 @@ object SequentCalculus {
* Γ[ψ(a)/?p] |- Δ[ψ(a)/?p]
* </pre>
*/
- case class InstPredSchema(bot:Sequent, t1:Int, p:SchematicPredicateLabel, psi:Formula, a: Seq[VariableLabel] )
+ case class InstPredSchema(bot:Sequent, t1:Int, p:SchematicPredicateLabel, psi:Formula, a: Seq[VariableLabel] ) extends SCProofStep{val premises = Seq(t1)}
// Proof Organisation rules
case class SCSubproof(sp: SCProof, premises: Seq[Int] = Seq.empty, display:Boolean = true) extends SCProofStep {
diff --git a/src/main/scala/lisa/settheory/SetTheoryDefinitions.scala b/src/main/scala/lisa/settheory/SetTheoryDefinitions.scala
index bf8b7bf4fe62efa8c0a0c9fe281d9e348593b34d..6b6d1de060e2cb0c40a0521f3077dea7ec4561f0 100644
--- a/src/main/scala/lisa/settheory/SetTheoryDefinitions.scala
+++ b/src/main/scala/lisa/settheory/SetTheoryDefinitions.scala
@@ -12,8 +12,8 @@ private[settheory] trait SetTheoryDefinitions{
def axioms: Set[Axiom] = Set.empty
private[settheory] final val (x, y, z, a, b) =
(VariableLabel("x"), VariableLabel("y"), VariableLabel("z"), VariableLabel("A"), VariableLabel("B"))
- private[settheory] final val sPhi = SchematicPredicateLabel("P", 2)
- private[settheory] final val sPsi = SchematicPredicateLabel("P", 3)
+ final val sPhi = SchematicPredicateLabel("P", 2)
+ final val sPsi = SchematicPredicateLabel("P", 3)
// Predicates
final val in: PredicateLabel = ConstantPredicateLabel("set_membership", 2)
final val subset: PredicateLabel = ConstantPredicateLabel("subset_of", 2)
diff --git a/src/main/scala/lisa/settheory/SetTheoryZAxioms.scala b/src/main/scala/lisa/settheory/SetTheoryZAxioms.scala
index da30c8780d16dbeaf9dbf1acb94464a29aff1bc2..46071edaa86050f87444b5b555215699209f666e 100644
--- a/src/main/scala/lisa/settheory/SetTheoryZAxioms.scala
+++ b/src/main/scala/lisa/settheory/SetTheoryZAxioms.scala
@@ -16,9 +16,9 @@ private[settheory] trait SetTheoryZAxioms extends SetTheoryDefinitions {
final val foundationAxiom: Axiom = forall(x, !(x === emptySet()) ==> exists(y, in(y, x) /\ forall(z, in(z, x) ==> !in(z, y))))
- final val comprehensionSchema: Axiom = forall(z, exists(y, forall(x, in(x,y) <=> (in(x,y) /\ sPhi(x,z)))))
+ final val comprehensionSchema: Axiom = forall(z, exists(y, forall(x, in(x,y) <=> (in(x,z) /\ sPhi(x,z)))))
- private val zAxioms: Set[Axiom] = Set(emptySetAxiom, extensionalityAxiom, pairAxiom, unionAxiom, powerAxiom, foundationAxiom)
+ private val zAxioms: Set[Axiom] = Set(emptySetAxiom, extensionalityAxiom, pairAxiom, unionAxiom, powerAxiom, foundationAxiom, comprehensionSchema)
diff --git a/src/main/scala/lisa/settheory/SetTheoryZFAxioms.scala b/src/main/scala/lisa/settheory/SetTheoryZFAxioms.scala
index 2b77f013d58533e80f783d7dc4dd6bce6250653e..6ea73c22866260ea2152894f499ab443430498a9 100644
--- a/src/main/scala/lisa/settheory/SetTheoryZFAxioms.scala
+++ b/src/main/scala/lisa/settheory/SetTheoryZFAxioms.scala
@@ -11,6 +11,9 @@ private[settheory] trait SetTheoryZFAxioms extends SetTheoryZAxioms {
forall(x, (in(x, a)) ==> existsOne(y, sPsi(a,x,y))) ==>
exists(b, forall(x, in(x, a) ==> exists(y, in(y, b) /\ sPsi(a,x,y))))
)
+ runningSetTheory.addAxiom(replacementSchema)
+
+ override def axioms: Set[Axiom] = super.axioms + replacementSchema
}
\ No newline at end of file
diff --git a/src/main/scala/proven/DSetTheory/Part1.scala b/src/main/scala/proven/DSetTheory/Part1.scala
new file mode 100644
index 0000000000000000000000000000000000000000..dbdd6a43583fcfe8a511190aaf2fbd9162133d6c
--- /dev/null
+++ b/src/main/scala/proven/DSetTheory/Part1.scala
@@ -0,0 +1,467 @@
+package proven.DSetTheory
+import lisa.kernel.fol.FOL.*
+import lisa.kernel.proof.SequentCalculus.*
+import lisa.KernelHelpers.{*, given}
+import lisa.kernel.Printer
+import lisa.kernel.Printer.{prettyFormula, prettySCProof}
+import proven.tactics.ProofTactics.*
+import proven.tactics.Destructors.*
+import lisa.settheory.AxiomaticSetTheory.*
+import proven.ElementsOfSetTheory.{oPair, orderedPairDefinition}
+
+import scala.collection.immutable.SortedSet
+import lisa.kernel.proof.{SCProof, SCProofChecker}
+import lisa.settheory.AxiomaticSetTheory
+
+import scala.collection.immutable
+object Part1 {
+ val theory = AxiomaticSetTheory.runningSetTheory
+ def axiom(f:Formula) = theory.getAxioms.find(c => c.ax == f).get
+
+
+ private val x = SchematicFunctionLabel("x", 0)()
+ private val y = SchematicFunctionLabel("y", 0)()
+ private val x1 = VariableLabel("x")
+ private val y1 = VariableLabel("y")
+ private val z1 = VariableLabel("z")
+ private val z = SchematicFunctionLabel("z", 0)()
+ private val f = SchematicFunctionLabel("f", 0)
+ private val g = SchematicFunctionLabel("g", 0)
+ private val h = SchematicPredicateLabel("h", 0)
+
+
+/**
+
+ */
+ val russelParadox: SCProof = {
+ val contra = (in(y,y)) <=> !(in(y,y))
+ val s0 = Hypothesis(contra |- contra, contra)
+ val s1 = LeftForall(forall(x1, in(x1,y) <=> !in(x1, x1)) |- contra, 0, in(x1, y) <=> !in(x1, x1), x1, y)
+ val s2 = Rewrite(forall(x1, in(x1,y) <=> !in(x1, x1)) |- (), 1)
+ //val s3 = LeftExists(exists(y1, forall(x1, in(x,y) <=> !in(x, x))) |- (), 2, forall(x1, in(x,y) <=> !in(x, x)), y1)
+ //val s4 = Rewrite(() |- !exists(y1, forall(x1, in(x1,y1) <=> !in(x1, x1))), 3)
+ SCProof(s0, s1, s2)
+ }
+ val thm_russelParadox = theory.proofToTheorem(russelParadox, Nil).get
+
+ val thm4:SCProof = {
+ //forall(z, exists(y, forall(x, in(x,y) <=> (in(x,y) /\ sPhi(x,z)))))
+ val i1 = () |- comprehensionSchema
+ val i2 = russelParadox.conclusion // forall(x1, in(x1,y) <=> !in(x1, x1)) |- ()
+ val p0: SCProofStep = InstPredSchema(() |- forall(z1, exists(y1, forall(x1, in(x1,y1) <=> (in(x1,z1) /\ !in(x1, x1))))), -1, sPhi, !in(x1, x1), Seq(x1, z1))
+ val s0 = SCSubproof(instantiateForall(SCProof(IndexedSeq(p0), IndexedSeq(i1)), z), Seq(-1)) //exists(y1, forall(x1, in(x1,y1) <=> (in(x1,z1) /\ !in(x1, x1))))
+ val s1 = hypothesis(in(x1,y1) <=> (in(x1,z) /\ !in(x1, x1))) //in(x,y) <=> (in(x,z) /\ in(x, x)) |- in(x,y) <=> (in(x,z) /\ in(x, x))
+ val s2 = RightSubstIff((in(x1, z) <=> And(), in(x1,y1) <=> (in(x1,z) /\ !in(x1, x1))) |- in(x1,y1) <=> (And() /\ !in(x1, x1)), 1, in(x1, z), And(), in(x1,y1) <=> (h() /\ !in(x1, x1)), h) //in(x1,y1) <=> (in(x1,z1) /\ in(x1, x1)) |- in(x,y) <=> (And() /\ in(x1, x1))
+ val s3 = Rewrite((in(x1, z), in(x1,y1) <=> (in(x1,z) /\ !in(x1, x1))) |- in(x1,y1) <=> !in(x1, x1), 2)
+ val s4 = LeftForall((forall(x1, in(x1, z)), in(x1,y1) <=> (in(x1,z) /\ !in(x1, x1))) |- in(x1,y1) <=> !in(x1, x1), 3, in(x1, z), x1, x1)
+ val s5 = LeftForall((forall(x1, in(x1, z)), forall(x1, in(x1,y1) <=> (in(x1,z) /\ !in(x1, x1)))) |- in(x1,y1) <=> !in(x1, x1), 4, in(x1,y1) <=> (in(x1,z) /\ !in(x1, x1)), x1, x1)
+ val s6 = RightForall((forall(x1, in(x1, z)), forall(x1, in(x1,y1) <=> (in(x1,z) /\ !in(x1, x1)))) |- forall(x1, in(x1,y1) <=> !in(x1, x1)), 5, in(x1,y1) <=> !in(x1, x1), x1)
+ val s7 = InstFunSchema(forall(x1, in(x1,y1) <=> !in(x1, x1)) |- (), -2, SchematicFunctionLabel("y", 0), y1, Nil)
+ val s8 = Cut((forall(x1, in(x1, z)), forall(x1, in(x1,y1) <=> (in(x1,z) /\ !in(x1, x1)))) |- (), 6, 7, forall(x1, in(x1,y1) <=> !in(x1, x1)))
+ val s9 = LeftExists((forall(x1, in(x1, z)), exists(y1, forall(x1, in(x1,y1) <=> (in(x1,z) /\ !in(x1, x1))))) |- (), 8, forall(x1, in(x1,y1) <=> (in(x1,z) /\ !in(x1, x1))), y1)
+ val s10 = Cut(forall(x1, in(x1, z)) |- (), 0, 9, exists(y1, forall(x1, in(x1,y1) <=> (in(x1,z) /\ !in(x1, x1)))) )
+ SCProof(Vector(s0, s1, s2, s3, s4, s5, s6, s7, s8, s9, s10), Vector(i1, i2))
+ }
+ val thm_thm4 = theory.proofToTheorem(thm4, Seq(axiom(comprehensionSchema), thm_russelParadox)).get
+
+ val thmMapFunctional: SCProof = {
+ val a = VariableLabel("a")
+ val b = VariableLabel("b")
+ val x = VariableLabel("x")
+ val y = VariableLabel("y")
+ val z = VariableLabel("z")
+ val A = SchematicFunctionLabel("A", 0)()
+ val X = VariableLabel("X")
+ val B = VariableLabel("B")
+ val B1 = VariableLabel("B1")
+ val phi = SchematicPredicateLabel("phi", 2)
+ val H = existsOne(x, phi(x, a))
+ val H1 = forall(a, in(a, A) ==> H)
+ val s0 = hypothesis(H)// () |- existsOne(x, phi(x, a)))
+ val s1 = Weakening((H, in(a, A)) |- existsOne(x, phi(x, a)), 0)
+ val s2 = Rewrite( (H) |- in(a, A) ==> existsOne(x, phi(x, a)), 1)
+ //val s3 = RightForall((H) |- forall(a, in(a, A) ==> existsOne(x, phi(x, a))), 2, in(a, A) ==> existsOne(x, phi(x, a)), a) // () |- ∀a∈A. ∃!x. phi(x, a)
+ val s3 = hypothesis(H1)
+ val i1 = ()|- replacementSchema
+ val p0 = InstPredSchema(()|- instantiatePredicateSchema(replacementSchema, sPsi, phi(x, a), Seq(y,a,x)), -1, sPsi, phi(x, a), Seq(y,a,x))
+ val p1 = instantiateForall(SCProof(Vector(p0), Vector(i1)), A)
+ val s4 = SCSubproof(p1, Seq(-1)) //
+ val s5 = Rewrite(s3.bot.right.head |- exists(B, forall(x, in(x, A) ==> exists(y, in(y, B) /\ (phi(y, x)) ))), 4)
+ val s6 = Cut((H1) |- exists(B, forall(x, in(x, A) ==> exists(y, in(y, B) /\ (phi(y, x)) ))), 3,5, s3.bot.right.head) // ⊢ ∃B. ∀x. (x ∈ A) ⇒ ∃y. (y ∈ B) ∧ (y = (x, b))
+
+ val i2 = () |- comprehensionSchema // forall(z, exists(y, forall(x, in(x,y) <=> (in(x,z) /\ sPhi(x,z)))))
+ val q0 = InstPredSchema(() |- instantiatePredicateSchema(comprehensionSchema, sPhi, exists(a, in(a, A) /\ (phi(x, a))), Seq(x,z)), -1, sPhi, exists(a, in(a, A) /\ (phi(x, a))), Seq(x,z))
+ val q1 = instantiateForall(SCProof(Vector(q0), Vector(i2)), B)
+ val s7 = SCSubproof(q1, Seq(-2)) //∃y. ∀x. (x ∈ y) ↔ (x ∈ B) ∧ ∃a. a ∈ A /\ x = (a, b) := exists(y, F(y) )
+ SCProof(Vector(s0, s1, s2, s3, s4, s5, s6, s7), Vector(i1, i2))
+ val s8 = SCSubproof({
+ val y1 = VariableLabel("y1")
+ val f = SchematicFunctionLabel("f", 0)
+ /*
+ val s0 = hypothesis(in(y, B)) // redgoal (y ∈ B) |- (y ∈ B) TRUE
+ val s1 = RightSubstEq((in(y, B), y===x) |- in(x, B), 0, x, y, in(f(), B), f)// redgoal (y ∈ B), (y = x) |- (x ∈ B)
+ val s2 = LeftSubstEq((phi(x, a), in(y, B), phi(y, a)) |- in(x, B), 1, x, oPair(a,b), y===f(), f )// redGoal x = (a, b), (y ∈ B), (y = (a, b)) |- (x ∈ B)
+ val s3 = Rewrite((phi(x, a), in(y, B) /\ (phi(y, a))) |- in(x, B), 2)
+ val s4 = LeftExists((phi(x, a), exists(y, in(y, B) /\ (phi(y, a)))) |- in(x, B), 3, in(y, B) /\ (phi(y, a)), y)// redGoal x = (a, b), ∃y. (y ∈ B) ∧ (y = (a, b)) |- (x ∈ B)
+ val s5 = Rewrite( (phi(x, a), And()==> exists(y, in(y, B) /\ (phi(y, a)))) |- in(x, B), 4) //redGoal (T) ⇒ ∃y. y ∈ B ∧ y = (a, b), x = (a, b) |- (x ∈ B)
+ val s6 = LeftSubstIff(Set(phi(x, a), in(a, A)==> exists(y, in(y, B) /\ (phi(y, a))), And()<=>in(a, A)) |- in(x, B),5, And(), in(a, A), h()==> exists(y, in(y, B) /\ (phi(y, a))), h) //redGoal (a ∈ A) ⇒ ∃y. y ∈ B ∧ y = (a, b), a ∈ A <=> T, x = (a, b) |- (x ∈ B)
+ val s7 = Rewrite(Set(in(a, A)==> exists(y, in(y, B) /\ (phi(y, a))), in(a, A) /\ (phi(x, a))) |- in(x, B), 6) //redGoal (a ∈ A) ⇒ ∃y. y ∈ B ∧ y = (a, b), a ∈ A ∧ x = (a, b) |- (x ∈ B)
+ val s8 = LeftForall((forall(a, in(a, A)==> exists(y, in(y, B) /\ (phi(y, a)))), in(a, A) /\ (phi(x, a)))|- in(x, B), 7, in(a, A)==> exists(y, in(y, B) /\ (phi(y, a))), a, a) //redGoal ∀a. (a ∈ A) ⇒ ∃y. y ∈ B ∧ y = (a, b), a ∈ A ∧ x = (a, b) |- (x ∈ B)
+ val s9 = LeftExists((forall(a, in(a, A)==> exists(y, in(y, B) /\ (phi(y, a)))), exists(a, in(a, A) /\ (phi(x, a))))|- in(x, B), 8, in(a, A) /\ (phi(x, a)), a) //∀a. (a ∈ A) ⇒ ∃y. y ∈ B ∧ y = (a, b), ∃a. a ∈ A ∧ x = (a, b) |- (x ∈ B)
+ SCProof(Vector(s0, s1, s2, s3, s4, s5, s6, s7, s8, s9))
+*/
+
+ val s0 = hypothesis(in(y1, B))
+ val s1 = RightSubstEq((in(y1, B), x===y1) |- in(x, B), 0, x, y1, in(f(), B), f)
+ val s2 = LeftSubstIff(Set( in(y1, B), (x===y1) <=> phi(x, a), phi(x, a)) |- in(x, B), 1, (x===y1), phi(x, a), h(), h)
+ val s3 = LeftSubstEq(Set( y===y1, in(y1, B), (x===y) <=> phi(x, a), phi(x, a)) |- in(x, B), 2, y, y1, (x===f()) <=> phi(x, a), f)
+ val s4 = LeftSubstIff(Set( (y===y1) <=> phi(y1, a), phi(y1, a), in(y1, B), (x===y) <=> phi(x, a), phi(x, a)) |- in(x, B), 3, phi(y1, a), y1===y, h(), h)
+ val s5 = LeftForall(Set( forall(x, (y===x) <=> phi(x, a)), phi(y1, a), in(y1, B), (x===y) <=> phi(x, a), phi(x, a)) |- in(x, B), 4, (y===x) <=> phi(x, a), x, y1)
+ val s6 = LeftForall(Set( forall(x, (y===x) <=> phi(x, a)), phi(y1, a), in(y1, B), phi(x, a)) |- in(x, B), 5, (x===y) <=> phi(x, a), x, x)
+ val s7 = LeftExists(Set( exists(y, forall(x, (y===x) <=> phi(x, a))), phi(y1, a), in(y1, B), phi(x, a)) |- in(x, B), 6, forall(x, (y===x) <=> phi(x, a)), y)
+ val s8 = Rewrite(Set( exists(y, forall(x, (y===x) <=> phi(x, a))), phi(y1, a) /\ in(y1, B), phi(x, a)) |- in(x, B), 7)
+ val s9 = LeftExists(Set( exists(y, forall(x, (y===x) <=> phi(x, a))), exists(y1, phi(y1, a) /\ in(y1, B)), phi(x, a)) |- in(x, B), 8, phi(y1, a) /\ in(y1, B), y1)
+ val s10 = Rewrite(Set( exists(y, forall(x, (y===x) <=> phi(x, a))), And() ==> exists(y, phi(y, a) /\ in(y, B)), phi(x, a)) |- in(x, B), 9)
+ val s11 = LeftSubstIff(Set( exists(y, forall(x, (y===x) <=> phi(x, a))), in(a, A) ==> exists(y, phi(y, a) /\ in(y, B)), phi(x, a), in(a, A))|- in(x, B), 10, And(), in(a, A), h() ==> exists(y, phi(y, a) /\ in(y, B)), h )
+ val s12 = LeftForall(Set( exists(y, forall(x, (y===x) <=> phi(x, a))), forall(a, in(a, A) ==> exists(y, phi(y, a) /\ in(y, B))), phi(x, a), in(a, A))|- in(x, B), 11, in(a, A) ==> exists(y, phi(y, a) /\ in(y, B)), a, a)
+ val s13 = LeftSubstIff(Set( in(a, A) ==> exists(y, forall(x, (y===x) <=> phi(x, a))), forall(a, in(a, A) ==> exists(y, phi(y, a) /\ in(y, B))), phi(x, a), in(a, A))|- in(x, B), 12, And(), in(a, A), h() ==> exists(y, forall(x, (y===x) <=> phi(x, a))), h )
+ val s14 = LeftForall(Set( forall(a, in(a, A) ==> exists(y, forall(x, (y===x) <=> phi(x, a)))), forall(a, in(a, A) ==> exists(y, phi(y, a) /\ in(y, B))), phi(x, a), in(a, A))|- in(x, B), 13, in(a, A) ==> exists(y, forall(x, (y===x) <=> phi(x, a))), a, a)
+ val s15 = Rewrite(Set( forall(a, in(a, A) ==> exists(y, forall(x, (y===x) <=> phi(x, a)))), forall(a, in(a, A) ==> exists(y, phi(y, a) /\ in(y, B))), phi(x, a) /\ in(a, A))|- in(x, B), 14)
+ val s16 = LeftExists(Set( forall(a, in(a, A) ==> exists(y, forall(x, (y===x) <=> phi(x, a)))), forall(a, in(a, A) ==> exists(y, phi(y, a) /\ in(y, B))), exists(a, phi(x, a) /\ in(a, A)))|- in(x, B), 15, phi(x, a) /\ in(a, A), a)
+ val truc = forall(a, in(a, A) ==> exists(y, phi(y, a) /\ in(y, B)))
+ val s17 = Rewrite(Set( forall(a, in(a, A) ==> existsOne(x, phi(x, a))), forall(a, in(a, A) ==> exists(y, phi(y, a) /\ in(y, B))), exists(a, phi(x, a) /\ in(a, A)))|- in(x, B), 16)
+ SCProof(Vector(s0,s1,s2,s3,s4,s5,s6,s7,s8,s9,s10,s11,s12,s13,s14,s15,s16,s17))
+ //goal H, ∀a. (a ∈ A) ⇒ ∃y. y ∈ B ∧ phi(y, a), ∃a. a ∈ A ∧ phi(x, a) |- (x ∈ B)
+ //redGoal ∀a.(a ∈ A) => ∃!x. phi(x, a), ∀a. (a ∈ A) ⇒ ∃y. y ∈ B ∧ phi(y, a), ∃a. a ∈ A ∧ phi(x, a) |- (x ∈ B) s17
+ //redGoal ∀a.(a ∈ A) => ∃y. ∀x. (x=y) ↔ phi(x, a), ∀a. (a ∈ A) ⇒ ∃y. y ∈ B ∧ phi(y, a), ∃a. a ∈ A ∧ phi(x, a) |- (x ∈ B) s16
+ //redGoal ∀a.(a ∈ A) => ∃y. ∀x. (x=y) ↔ phi(x, a), ∀a. (a ∈ A) ⇒ ∃y. y ∈ B ∧ phi(y, a), a ∈ A ∧ phi(x, a) |- (x ∈ B) s15
+ //redGoal ∀a.(a ∈ A) => ∃y. ∀x. (x=y) ↔ phi(x, a), ∀a. (a ∈ A) ⇒ ∃y. y ∈ B ∧ phi(y, a), a ∈ A, phi(x, a) |- (x ∈ B) s14
+ //redGoal (a ∈ A) => ∃y. ∀x. (x=y) ↔ phi(x, a), ∀a. (a ∈ A) ⇒ ∃y. y ∈ B ∧ phi(y, a), a ∈ A, phi(x, a) |- (x ∈ B) s13
+ //redGoal ∃y. ∀x. (x=y) ↔ phi(x, a), ∀a. (a ∈ A) ⇒ ∃y. y ∈ B ∧ phi(y, a), a ∈ A, phi(x, a) |- (x ∈ B) s12
+ //redGoal ∃y. ∀x. (x=y) ↔ phi(x, a), (a ∈ A) ⇒ ∃y. y ∈ B ∧ phi(y, a), a ∈ A, phi(x, a) |- (x ∈ B) s11
+ //redGoal ∃y. ∀x. (x=y) ↔ phi(x, a), (a ∈ A) ⇒ ∃y. y ∈ B ∧ phi(y, a), a ∈ A <=> T, phi(x, a) |- (x ∈ B) s11
+ //redGoal ∃y. ∀x. (x=y) ↔ phi(x, a), T ⇒ ∃y. y ∈ B ∧ phi(y, a), a ∈ A <=> T, phi(x, a) |- (x ∈ B) s10
+ //redGoal ∃y. ∀x. (x=y) ↔ phi(x, a), ∃y1. y1 ∈ B ∧ phi(y1, a), a ∈ A, phi(x, a) |- (x ∈ B) s9
+ //redGoal ∃y. ∀x. (x=y) ↔ phi(x, a), y1 ∈ B ∧ phi(y1, a), a ∈ A, phi(x, a) |- (x ∈ B) s8
+ //redGoal ∃y. ∀x. (x=y) ↔ phi(x, a), y1 ∈ B, phi(y1, a), a ∈ A, phi(x, a) |- (x ∈ B) s7
+ //redGoal ∀x. (x=y) ↔ phi(x, a), y1 ∈ B, phi(y1, a), a ∈ A, phi(x, a) |- (x ∈ B) s6
+ //redGoal (x=y) ↔ phi(x, a), ∀x. (x=y) ↔ phi(x, a), y1 ∈ B, phi(y1, a), a ∈ A, phi(x, a) |- (x ∈ B) s5
+ //redGoal (x=y) ↔ phi(x, a), (y1=y) ↔ phi(y1, a), y1 ∈ B, phi(y1, a), a ∈ A, phi(x, a) |- (x ∈ B) s4
+ //redGoal (x=y) ↔ phi(x, a), (y1=y) ↔ phi(y1, a), y1 ∈ B, (y1=y), a ∈ A, phi(x, a) |- (x ∈ B) s3
+ //redGoal (x=y1) ↔ phi(x, a), (y1=y) ↔ phi(y1, a), y1 ∈ B, (y1=y), a ∈ A, phi(x, a) |- (x ∈ B) s2
+ //redGoal (x=y1) ↔ phi(x, a), (y1=y) ↔ phi(y1, a), y1 ∈ B, (y1=y), a ∈ A, x=y1 |- (x ∈ B) s1
+ //redGoal (x=y1) ↔ phi(x, a), (y1=y) ↔ phi(y1, a), y1 ∈ B, (y1=y), a ∈ A, x=y1 |- (y1 ∈ B) s0
+
+ }) // H, ∀a. (a ∈ A) ⇒ ∃y. y ∈ B ∧ phi(y, a), ∃a. a ∈ A ∧ phi(x, a) |- (x ∈ B)
+
+ val G = forall(a, in(a, A)==> exists(y, in(y, B) /\ (phi(y, a))))
+ val F = forall(x, iff(in(x, B1), in(x, B) /\ exists(a, in(a, A) /\ (phi(x, a)))))
+ val s9 = SCSubproof({
+ val p0 = instantiateForall(SCProof(hypothesis(F)), x)
+ val left = in(x, B1)
+ val right = in(x, B) /\ exists(a, in(a, A) /\ (phi(x, a)))
+ val p1 = p0.withNewSteps(Vector(Rewrite(F |- (left ==> right) /\ (right ==> left), p0.length-1) ))
+ val p2 = destructRightAnd( p1, (right ==> left), (left ==> right)) // F |- in(x, B) /\ exists(a, in(a, A) /\ (phi(x, a))) => in(x, B1)
+ val p3 = p2.withNewSteps(Vector(Rewrite(Set(F, in(x, B), exists(a, in(a, A) /\ (phi(x, a)))) |- in(x, B1) , p2.length-1)))
+ p3
+ }) // have F, (x ∈ B), ∃a. a ∈ A ∧ x = (a, b) |- (x ∈ B1)
+ val s10 = Cut( Set(F, G, H1, exists(a, in(a, A) /\ (phi(x, a)) )) |- in(x, B1), 8, 9, in(x, B)) // redGoal F, ∃a. a ∈ A ∧ x = (a, b), ∀a. (a ∈ A) ⇒ ∃y. y ∈ B ∧ y = (a, b) |- (x ∈ B1)
+ val s11 = Rewrite(Set(H1, G, F) |- exists(a, in(a, A) /\ (phi(x, a))) ==> in(x, B1), 10) // F |- ∃a. a ∈ A ∧ x = (a, b) => (x ∈ B1) --- half
+ val s12 = SCSubproof({
+ val p0 = instantiateForall(SCProof(hypothesis(F)), x)
+ val left = in(x, B1)
+ val right = in(x, B) /\ exists(a, in(a, A) /\ (phi(x, a)))
+ val p1 = p0.withNewSteps(Vector(Rewrite(F |- (left ==> right) /\ (right ==> left), p0.length-1) ))
+ val p2 = destructRightAnd( p1, (left ==> right), (right ==> left)) // F |- in(x, B1) => in(x, B) /\ exists(a, in(a, A) /\ (phi(x, a))) =>
+ val p3 = p2.withNewSteps(Vector(Rewrite(Set(F, in(x, B1)) |- exists(a, in(a, A) /\ (phi(x, a))) /\ in(x, B) , p2.length-1)))
+ val p4 = destructRightAnd(p3, exists(a, in(a, A) /\ (phi(x, a))), in(x, B))
+ val p5 = p4.withNewSteps(Vector(Rewrite(F |- in(x, B1) ==> exists(a, in(a, A) /\ (phi(x, a))) , p4.length-1)))
+ p5
+ }) // have F |- (x ∈ B1) ⇒ ∃a. a ∈ A ∧ x = (a, b) --- other half
+ val s13 = RightIff((H1, G, F) |- in(x, B1) <=> exists(a, in(a, A) /\ (phi(x, a))), 11, 12, in(x, B1), exists(a, in(a, A) /\ (phi(x, a)))) // have F |- (x ∈ B1) <=> ∃a. a ∈ A ∧ x = (a, b)
+ val s14 = RightForall((H1, G, F) |- forall(x, in(x, B1) <=> exists(a, in(a, A) /\ (phi(x, a)))), 13, in(x, B1) <=> exists(a, in(a, A) /\ (phi(x, a))), x) // G, F |- ∀x. (x ∈ B1) <=> ∃a. a ∈ A ∧ x = (a, b)
+
+ val i3 = () |- extensionalityAxiom
+ val s15 = SCSubproof({
+ val i1 = s13.bot // G, F |- (x ∈ B1) <=> ∃a. a ∈ A ∧ x = (a, b)
+ val i2 = ()|- extensionalityAxiom
+ val t0 = RightSubstIff(Set(H1, G, F, in(x, X) <=> exists(a, in(a, A) /\ (phi(x, a)))) |- in(x, X) <=> in(x, B1), -1, in(x, X), exists(a, in(a, A) /\ (phi(x, a))), h() <=> in(x, B1), h) //redGoal2 F, (z ∈ X) <=> ∃a. a ∈ A ∧ z = (a, b) |- (z ∈ X) <=> (z ∈ B1)
+ val t1 = LeftForall(Set(H1, G, F, forall(x, in(x, X) <=> exists(a, in(a, A) /\ (phi(x, a))))) |- in(x, X) <=> in(x, B1), 0, in(x, X) <=> exists(a, in(a, A) /\ (phi(x, a))), x, x ) //redGoal2 F, [∀x. (x ∈ X) <=> ∃a. a ∈ A ∧ x = (a, b)] |- (z ∈ X) <=> (z ∈ B1)
+ val t2 = RightForall(t1.bot.left |- forall(x, in(x, X) <=> in(x, B1)), 1, in(x, X) <=> in(x, B1), x) //redGoal2 F, [∀x. (x ∈ X) <=> ∃a. a ∈ A ∧ x = (a, b)] |- ∀z. (z ∈ X) <=> (z ∈ B1)
+ val t3 = SCSubproof(instantiateForall(SCProof(Vector(Rewrite(()|- extensionalityAxiom, -1)), Vector(()|-extensionalityAxiom)), X, B1), Vector(-2)) // (∀z. (z ∈ X) <=> (z ∈ B1)) <=> (X === B1)))
+ val t4 = RightSubstIff(t1.bot.left++t3.bot.right |- X===B1, 2, X===B1, forall(z, in(z, X) <=> in(z, B1)), h(), h) //redGoal2 F, [∀x. (x ∈ X) <=> ∃a. a ∈ A ∧ x = (a, b)], (∀z. (z ∈ X) <=> (z ∈ B1)) <=> (X === B1))) |- X=B1
+ val t5 = Cut(t1.bot.left |- X===B1, 3, 4, t3.bot.right.head) //redGoal2 F, [∀x. (x ∈ X) <=> ∃a. a ∈ A ∧ x = (a, b)] |- X=B1
+ val t6 = Rewrite(Set(H1, G, F) |- forall(x, in(x, X) <=> exists(a, in(a, A) /\ (phi(x, a)))) ==> (X===B1), 5) // F |- [∀x. (x ∈ X) <=> ∃a. a ∈ A ∧ x = (a, b)] ==> X=B1
+ val i3 = s14.bot // F |- ∀x. (x ∈ B1) <=> ∃a. a ∈ A ∧ x = (a, b)
+ val t7 = RightSubstEq(Set(H1, G, F, X===B1) |- forall(x, in(x, X) <=> exists(a, in(a, A) /\ (phi(x, a)))), -3, X, B1, forall(x, in(x, f()) <=> exists(a, in(a, A) /\ (phi(x, a)))), f) //redGoal1 F, X=B1 |- [∀x. (x ∈ X) <=> ∃a. a ∈ A ∧ x = (a, b)]
+ val t8 = Rewrite(Set(H1, G, F) |- X===B1 ==> forall(x, in(x, X) <=> exists(a, in(a, A) /\ (phi(x, a)))), 7) //redGoal1 F |- X=B1 ==> [∀x. (x ∈ X) <=> ∃a. a ∈ A ∧ x = (a, b)] -------second half with t6
+ val t9 = RightIff(Set(H1, G, F) |- (X===B1) <=> forall(x, in(x, X) <=> exists(a, in(a, A) /\ (phi(x, a)))), 6, 8, X===B1, forall(x, in(x, X) <=> exists(a, in(a, A) /\ (phi(x, a))))) //goal F |- X=B1 <=> [∀x. (x ∈ X) <=> ∃a. a ∈ A ∧ x = (a, b)]
+
+ SCProof(Vector(t0,t1,t2,t3,t4,t5,t6,t7,t8,t9), Vector(i1, i2, i3))
+ }, Vector(13, -3, 14)) //goal F |- X=B1 <=> [∀x. (x ∈ X) <=> ∃a. a ∈ A ∧ x = (a, b)]
+ val s16 = RightForall((H1, G, F) |- forall(X, (X===B1) <=> forall(x, in(x, X) <=> exists(a, in(a, A) /\ (phi(x, a))))), 15, (X===B1) <=> forall(x, in(x, X) <=> exists(a, in(a, A) /\ (phi(x, a)))), X) //goal F |- ∀X. X=B1 <=> [∀x. (x ∈ X) <=> ∃a. a ∈ A ∧ x = (a, b)]
+ val s17 = RightExists((H1, G, F) |- exists(y, forall(X, (X===y) <=> forall(x, in(x, X) <=> exists(a, in(a, A) /\ (phi(x, a)))))), 16, forall(X, (X===y) <=> forall(x, in(x, X) <=> exists(a, in(a, A) /\ (phi(x, a))))), y, B1 )
+ val s18 = LeftExists((exists(B1, F), G, H1)|- s17.bot.right, 17, F, B1) // ∃B1. F |- ∃B1. ∀X. X=B1 <=> [∀x. (x ∈ X) <=> ∃a. a ∈ A ∧ x = (a, b)]
+ val s19 = Rewrite(s18.bot.left |- existsOne(X, forall(x, in(x, X) <=> exists(a, in(a, A) /\ (phi(x, a))))), 18) // ∃B1. F |- ∃!X. [∀x. (x ∈ X) <=> ∃a. a ∈ A ∧ x = (a, b)]
+ val s20 = Cut((G, H1) |- existsOne(X, forall(x, in(x, X) <=> exists(a, in(a, A) /\ (phi(x, a))))), 7, 19, exists(B1, F))
+ val s21 = LeftExists((H1, exists(B, G)) |- existsOne(X, forall(x, in(x, X) <=> exists(a, in(a, A) /\ (phi(x, a))))), 20, G, B)
+ val s22 = Cut((H1) |- existsOne(X, forall(x, in(x, X) <=> exists(a, in(a, A) /\ phi(x, a)))), 6, 21, exists(B, G))
+ val steps = Vector(s0,s1,s2,s3,s4,s5,s6,s7,s8,s9,s10,s11,s12,s13,s14,s15,s16,s17,s18,s19,s20,s21,s22)
+ SCProof(steps, Vector(i1, i2, i3))
+ }
+ val thm_thmMapFunctional = theory.proofToTheorem(thmMapFunctional, Seq(axiom(replacementSchema), axiom(comprehensionSchema),axiom(extensionalityAxiom))).get
+
+ /**
+ * ∀ b. (b ∈ B) ⇒ ∀a. (a ∈ A) ⇒ ∃!x. ?psi(x, a, b) |- ∃!X. ∀x. (x ∈ X) ↔ ∃b. (b ∈ B) ∧ ∀x1. (x1 ∈ x) ↔ ∃a. (a ∈ A) ∧ ?psi(x1, a, b)
+ */
+ val lemma1 : SCProof = {
+ val a = VariableLabel("a")
+ val b = VariableLabel("b")
+ val x = VariableLabel("x")
+ val x1 = VariableLabel("x1")
+ val y = VariableLabel("y")
+ val z = VariableLabel("z")
+ val A = SchematicFunctionLabel("A", 0)()
+ val X = VariableLabel("X")
+ val B = SchematicFunctionLabel("B", 0)()
+ val B1 = VariableLabel("B1")
+ val phi = SchematicPredicateLabel("phi", 2)
+ val psi = SchematicPredicateLabel("psi", 3)
+ val H = existsOne(x, phi(x, a))
+ val H1 = forall(a, in(a, A) ==> H)
+ val i1 = thmMapFunctional.conclusion
+ val H2 = instantiatePredicateSchema(H1, phi, psi(x, a, b), Seq(x, a))
+ val s0 = InstPredSchema((H2) |- existsOne(X, forall(x, in(x, X) <=> exists(a, in(a, A) /\ psi(x, a, b)))), -1, phi, psi(x, a, b), Seq(x, a))
+ val s1 = Weakening((H2, in(b, B)) |- existsOne(X, forall(x, in(x, X) <=> exists(a, in(a, A) /\ psi(x, a, b)))), 0)
+ val s2 = LeftSubstIff((in(b, B) ==> H2, in(b, B)) |- existsOne(X, forall(x, in(x, X) <=> exists(a, in(a, A) /\ psi(x, a, b)))), 1, in(b, B), And(), h() ==> H2, h)
+ val s3 = LeftForall((forall(b, in(b, B) ==> H2), in(b, B)) |- existsOne(X, forall(x, in(x, X) <=> exists(a, in(a, A) /\ psi(x, a, b)))), 2, in(b, B) ==> H2, b, b)
+ val s4 = Rewrite(forall(b, in(b, B) ==> H2) |- in(b, B) ==> existsOne(X, forall(x, in(x, X) <=> exists(a, in(a, A) /\ psi(x, a, b)))), 3)
+ val s5 = RightForall(forall(b, in(b, B) ==> H2) |- forall(b, in(b, B) ==> existsOne(X, forall(x, in(x, X) <=> exists(a, in(a, A) /\ psi(x, a, b))))), 4, in(b, B) ==> existsOne(X, forall(x, in(x, X) <=> exists(a, in(a, A) /\ psi(x, a, b)))), b)
+ val s6 = InstFunSchema(forall(b, in(b, B) ==> existsOne(X, phi(X, b))) |- instantiateFunctionSchema(i1.right.head, SchematicFunctionLabel("A", 0), B, Seq()), -1, SchematicFunctionLabel("A", 0), B, Seq())
+ val s7 = InstPredSchema(forall(b, in(b, B) ==> existsOne(X, forall(x, in(x, X) <=> exists(a, in(a, A) /\ psi(x, a, b))))) |- existsOne(X, forall(x, in(x, X) <=> exists(b, in(b, B) /\ forall(x1,in(x1, x) <=> exists(a, in(a, A) /\ psi(x1, a, b)))))), 6, phi, forall(x,in(x, X) <=> exists(a, in(a, A) /\ psi(x, a, b))), Seq(X, b))
+ val s8 = Cut(forall(b, in(b, B) ==> H2) |- existsOne(X, forall(x, in(x, X) <=> exists(b, in(b, B) /\ forall(x1,in(x1, x) <=> exists(a, in(a, A) /\ psi(x1, a, b)))))), 5, 7, forall(b, in(b, B) ==> existsOne(X, forall(x, in(x, X) <=> exists(a, in(a, A) /\ psi(x, a, b))))))
+ SCProof(Vector(s0,s1,s2,s3,s4,s5,s6,s7, s8), Vector(i1))
+
+ // have ∀a. (a ∈ A) ⇒ ∃!x. ?psi(x, a, b) ⊢ ∃!X. ∀x. (x ∈ X) ↔ ∃a. (a ∈ A) ∧ ?psi(x, a, b) s0
+ // have (b ∈ B), ∀a. (a ∈ A) ⇒ ∃!x. ?psi(x, a, b) ⊢ ∃!X. ∀x. (x ∈ X) ↔ ∃a. (a ∈ A) ∧ ?psi(x, a, b) s1
+ // have (b ∈ B), (b ∈ B) ⇒ ∀a. (a ∈ A) ⇒ ∃!x. ?psi(x, a, b) ⊢ ∃!X. ∀x. (x ∈ X) ↔ ∃a. (a ∈ A) ∧ ?psi(x, a, b) s2
+ // have (b ∈ B), ∀b. (b ∈ B) ⇒ ∀a. (a ∈ A) ⇒ ∃!x. ?psi(x, a, b) ⊢ ∃!X. ∀x. (x ∈ X) ↔ ∃a. (a ∈ A) ∧ ?psi(x, a, b) s3
+ // have ∀b. (b ∈ B) ⇒ ∀a. (a ∈ A) ⇒ ∃!x. ?psi(x, a, b) ⊢ (b ∈ B) ⇒ ∃!X. ∀x. (x ∈ X) ↔ ∃a. (a ∈ A) ∧ ?psi(x, a, b) s4
+ // have ∀b. (b ∈ B) ⇒ ∀a. (a ∈ A) ⇒ ∃!x. ?psi(x, a, b) ⊢ ∀b. (b ∈ B) ⇒ ∃!X. ∀x. (x ∈ X) ↔ ∃a. (a ∈ A) ∧ ?psi(x, a, b) s5
+ // by thmMapFunctional have ∀b. (b ∈ B) ⇒ ∃!x. ∀x1. (x1 ∈ x) ↔ ∃a. (a ∈ A) ∧ ?psi(x1, a, b) ⊢ ∃!X. ∀x. (x ∈ X) ↔ ∃b. (b ∈ B) ∧ ∀x1. (x1 ∈ x) ↔ ∃a. (a ∈ A) ∧ ?psi(x1, a, b) phi(x, b) = ∀x1. (x1 ∈ x) ↔ ∃a. (a ∈ A) ∧ ?psi(x1, a, b) s6
+ // have ∀b. (b ∈ B) ⇒ ∀a. (a ∈ A) ⇒ ∃!x. ?psi(x, a, b) |- ∃!X. ∀x. (x ∈ X) ↔ ∃b. (b ∈ B) ∧ ∀x1. (x1 ∈ x) ↔ ∃a. (a ∈ A) ∧ ?psi(x1, a, b) s7
+ }
+ val thm_lemma1 = theory.proofToTheorem(lemma1, Seq(thm_thmMapFunctional)).get
+
+/*
+ val lemma2 = SCProof({
+
+
+ // goal ∀b. (b ∈ ?B) ⇒ ∀a. (a ∈ ?A) ⇒ ∃!x. ?psi(x, a, b) ⊢ ∃!Z. ∃X. Z=UX /\ ∀x. (x ∈ X) ↔ ∃b. (b ∈ ?B) ∧ ∀x1. (x1 ∈ x) ↔ ∃a. (a ∈ ?A) ∧ ?psi(x1, a, b)
+ // redGoal ∀b. (b ∈ ?B) ⇒ ∀a. (a ∈ ?A) ⇒ ∃!x. ?psi(x, a, b) ⊢ ∃Z1. ∀Z. Z=Z1 <=> ∃X. Z=UX /\ ∀x. (x ∈ X) ↔ ∃b. (b ∈ ?B) ∧ ∀x1. (x1 ∈ x) ↔ ∃a. (a ∈ ?A) ∧ ?psi(x1, a, b)
+ // redGoal ∀b. (b ∈ ?B) ⇒ ∀a. (a ∈ ?A) ⇒ ∃!x. ?psi(x, a, b) ⊢ ∀Z. Z=UX <=> ∃X. Z=UX /\ ∀x. (x ∈ X) ↔ ∃b. (b ∈ ?B) ∧ ∀x1. (x1 ∈ x) ↔ ∃a. (a ∈ ?A) ∧ ?psi(x1, a, b)
+ // redGoal ∀b. (b ∈ ?B) ⇒ ∀a. (a ∈ ?A) ⇒ ∃!x. ?psi(x, a, b) ⊢ ∀Z. Z=UX <=> ∃X. Z=UX /\ ∀x. (x ∈ X) ↔ ∃b. (b ∈ ?B) ∧ ∀x1. (x1 ∈ x) ↔ ∃a. (a ∈ ?A) ∧ ?psi(x1, a, b)
+ })
+*/
+
+ /**
+ * ∃!x. ?phi(x) ⊢ ∃!z. ∃x. z=?F(x) /\ ?phi(x)
+ */
+ val lemmaApplyFToObject : SCProof = {
+ val x = VariableLabel("x")
+ val x1 = VariableLabel("x1")
+ val z = VariableLabel("z")
+ val z1 = VariableLabel("z1")
+ val F = SchematicFunctionLabel("F", 1)
+ val f = SchematicFunctionLabel("f", 0)
+ val phi = SchematicPredicateLabel("phi", 1)
+ val g = SchematicPredicateLabel("g", 0)
+
+ val g2 = SCSubproof({
+ val s0 = hypothesis(F(x1) === z)
+ val s1 = LeftSubstEq((x === x1, F(x) === z) |- F(x1) === z, 0, x, x1, F(f()) === z, f)
+ val s2 = LeftSubstIff(Set(phi(x) <=> (x === x1), phi(x), F(x) === z) |- F(x1) === z, 1, x === x1, phi(x), g(), g)
+ val s3 = LeftForall(Set(forall(x, phi(x) <=> (x === x1)), phi(x), F(x) === z) |- F(x1) === z, 2, phi(x) <=> (x === x1), x, x)
+ val s4 = Rewrite(Set(forall(x, phi(x) <=> (x === x1)), phi(x) /\ (F(x) === z)) |- F(x1) === z, 3)
+ val s5 = LeftExists(Set(forall(x, phi(x) <=> (x === x1)), exists(x, phi(x) /\ (F(x) === z))) |- F(x1) === z, 4,phi(x) /\ (F(x) === z), x)
+ val s6 = Rewrite(forall(x, phi(x) <=> (x === x1)) |- exists(x, phi(x) /\ (F(x) === z)) ==> (F(x1) === z), 5)
+ SCProof(Vector(s0, s1, s2, s3, s4, s5, s6))
+ }) // redGoal2 ∀x. x=x1 <=> phi(x) ⊢ ∃x. z=F(x) /\ phi(x) ==> F(x1)=z g2.s5
+
+ val g1 = SCSubproof({
+ val s0 = hypothesis(phi(x1))
+ val s1 = LeftForall(forall(x, (x===x1) <=> phi(x)) |- phi(x1), 0, (x===x1) <=> phi(x), x , x1)
+ val s2 = hypothesis(z===F(x1))
+ val s3 = RightAnd((forall(x, (x===x1) <=> phi(x)), z===F(x1)) |- (z===F(x1)) /\ phi(x1), Seq(2, 1), Seq(z===F(x1), phi(x1)) )
+ val s4 = RightExists((forall(x, (x===x1) <=> phi(x)), z===F(x1)) |- exists(x, (z===F(x)) /\ phi(x)), 3, (z===F(x)) /\ phi(x), x, x1)
+ val s5 = Rewrite(forall(x, (x===x1) <=> phi(x)) |- z===F(x1) ==> exists(x, (z===F(x)) /\ phi(x)), 4)
+ SCProof(Vector(s0, s1, s2, s3, s4, s5))
+ })
+
+ val s0 = g1
+ val s1 = g2
+ val s2 = RightIff(forall(x, (x===x1) <=> phi(x)) |- (z===F(x1)) <=> exists(x, (z===F(x)) /\ phi(x)), 0, 1, z===F(x1), exists(x, (z===F(x)) /\ phi(x)))
+ val s3 = RightForall(forall(x, (x===x1) <=> phi(x)) |- forall(z, (z===F(x1)) <=> exists(x, (z===F(x)) /\ phi(x))), 2, (z===F(x1)) <=> exists(x, (z===F(x)) /\ phi(x)), z)
+ val s4 = RightExists(forall(x, (x===x1) <=> phi(x)) |- exists(z1, forall(z, (z===z1) <=> exists(x, (z===F(x)) /\ phi(x)))), 3, forall(z, (z===z1) <=> exists(x, (z===F(x)) /\ phi(x))), z1, F(x1))
+ val s5 = LeftExists(exists(x1, forall(x, (x===x1) <=> phi(x))) |- exists(z1, forall(z, (z===z1) <=> exists(x, (z===F(x)) /\ phi(x)))), 4, forall(x, (x===x1) <=> phi(x)), x1)
+ val s6 = Rewrite(existsOne(x, phi(x)) |- existsOne(z, exists(x, (z===F(x)) /\ phi(x))), 5) // goal ∃!x. phi(x) ⊢ ∃!z. ∃x. z=F(x) /\ phi(x)
+
+ SCProof(Vector(s0, s1, s2, s3, s4, s5, s6))
+
+ // goal ∃!x. phi(x) ⊢ ∃!z. ∃x. z=F(x) /\ phi(x)
+ // redGoal ∃x1. ∀X. x=x1 <=> phi(x) ⊢ ∃z1. ∀z. z1=z <=> ∃x. Z=F(x) /\ phi(x) s4, s5
+ // redGoal ∀x. x=x1 <=> phi(x) ⊢ ∀z. F(x1)=z <=> ∃x. Z=F(x) /\ phi(x) s3
+ // redGoal ∀x. x=x1 <=> phi(x) ⊢ F(x1)=z <=> ∃x. Z=F(x) /\ phi(x) s2
+ // redGoal1 ∀x. x=x1 <=> phi(x) ⊢ F(x1)=z ==> ∃x. Z=F(x) /\ phi(x) g1.s5
+ // redGoal1 ∀x. x=x1 <=> phi(x), F(x1)=z ⊢ ∃x. z=F(x) /\ phi(x) g1.s4
+ // redGoal1 ∀x. x=x1 <=> phi(x), F(x1)=z ⊢ z=F(x1) /\ phi(x1) g1.s3
+ // redGoal11 ∀x. x=x1 <=> phi(x), F(x1)=z ⊢ z=F(x1) TRUE g1.s2
+ // redGoal12 ∀x. x=x1 <=> phi(x) ⊢ phi(x1) g1.s1
+ // redGoal12 x1=x1 <=> phi(x1) ⊢ phi(x1)
+ // redGoal12 phi(x1) ⊢ phi(x1) g1.s0
+ // redGoal2 ∀x. x=x1 <=> phi(x) ⊢ ∃x. z=F(x) /\ phi(x) ==> F(x1)=z g2.s5
+ // redGoal2 ∀x. x=x1 <=> phi(x), ∃x. z=F(x) /\ phi(x) ⊢ F(x1)=z g2.s4
+ // redGoal2 ∀x. x=x1 <=> phi(x), z=F(x), phi(x) ⊢ F(x1)=z g2.s3
+ // redGoal2 x=x1 <=> phi(x), z=F(x), phi(x) ⊢ F(x1)=z g2.s2
+ // redGoal2 x=x1 <=> phi(x), z=F(x), x=x1 ⊢ F(x1)=z g2.s1
+ // redGoal2 x=x1 <=> phi(x), z=F(x1), x=x1 ⊢ F(x1)=z TRUE g2.s0
+ }
+ val thm_lemmaApplyFToObject = theory.proofToTheorem(lemmaApplyFToObject, Nil).get
+
+ /**
+ * ∀b. (b ∈ ?B) ⇒ ∀a. (a ∈ ?A) ⇒ ∃!x. ?psi(x, a, b) ⊢ ∃!z. ∃x. (z = U(x)) ∧ ∀x_0. (x_0 ∈ x) ↔ ∃b. (b ∈ ?B) ∧ ∀x1. (x1 ∈ x_0) ↔ ∃a. (a ∈ ?A) ∧ ?psi(x1, a, b)
+ */
+ val lemmaMapTwoArguments : SCProof = {
+ val a = VariableLabel("a")
+ val b = VariableLabel("b")
+ val x = VariableLabel("x")
+ val x1 = VariableLabel("x1")
+ val F = SchematicFunctionLabel("F", 1)
+ val A = SchematicFunctionLabel("A", 0)()
+ val X = VariableLabel("X")
+ val B = SchematicFunctionLabel("B", 0)()
+ val phi = SchematicPredicateLabel("phi", 1)
+ val psi = SchematicPredicateLabel("psi", 3)
+
+ val i1 = lemma1.conclusion
+ val i2 = lemmaApplyFToObject.conclusion
+ val rPhi = forall(x, in(x, X) <=> exists(b, in(b, B) /\ forall(x1,in(x1, x) <=> exists(a, in(a, A) /\ psi(x1, a, b)))))
+ val seq0 = instantiatePredicateSchemaInSequent(i2, phi, rPhi, Seq(X))
+ val s0 = InstPredSchema(instantiatePredicateSchemaInSequent(i2, phi, rPhi, Seq(X)), -2, phi, rPhi, Seq(X))
+ val seq1 = instantiateFunctionSchemaInSequent(seq0, F, union(x), Seq(x))
+ val s1 = InstFunSchema(seq1, 0, F, union(x), Seq(x))
+ val s2 = Cut(i1.left |- seq1.right, -1, 1, seq1.left.head)
+ SCProof(Vector(s0,s1,s2), Vector(i1, i2))
+ }
+ val thm_lemmaMapTwoArguments = theory.proofToTheorem(lemmaMapTwoArguments, Seq(thm_lemma1, thm_lemmaApplyFToObject)).get
+
+ /**
+ * ⊢ ∃!z. ∃x. (z = U(x)) ∧ ∀x_0. (x_0 ∈ x) ↔ ∃b. (b ∈ ?B) ∧ ∀x1. (x1 ∈ x_0) ↔ ∃a. (a ∈ ?A) ∧ (x1 = (a, b))
+ */
+ val lemmaCartesianProduct : SCProof = {
+ val a = VariableLabel("a")
+ val b = VariableLabel("b")
+ val x = VariableLabel("x")
+ val x1 = VariableLabel("x1")
+ val F = SchematicFunctionLabel("F", 1)
+ val A = SchematicFunctionLabel("A", 0)()
+ val X = VariableLabel("X")
+ val B = SchematicFunctionLabel("B", 0)()
+ val phi = SchematicPredicateLabel("phi", 1)
+ val psi = SchematicPredicateLabel("psi", 3)
+
+ val i1 = lemmaMapTwoArguments.conclusion //∀b. (b ∈ ?B) ⇒ ∀a. (a ∈ ?A) ⇒ ∃!x. ?psi(x, a, b) ⊢ ∃!z. ∃x. (z = U(x)) ∧ ∀x_0. (x_0 ∈ x) ↔ ∃b. (b ∈ ?B) ∧ ∀x1. (x1 ∈ x_0) ↔ ∃a. (a ∈ ?A) ∧ ?psi(x1, a, b)
+ val s0 = SCSubproof({
+ val s0 = SCSubproof(makeFunctional(oPair(a, b)))
+ val s1 = Weakening((in(b, B), in(a, A)) |- s0.bot.right, 0)
+ val s2 = Rewrite(in(b, B) |- in(a, A) ==> s0.bot.right.head, 1)
+ val s3 = RightForall(in(b, B) |- forall(a, in(a, A) ==> s0.bot.right.head), 2, in(a, A) ==> s0.bot.right.head, a)
+ val s4 = Rewrite(() |- in(b, B) ==> forall(a, in(a, A) ==> s0.bot.right.head), 3)
+ val s5 = RightForall(() |- forall(b, in(b, B) ==> forall(a, in(a, A) ==> s0.bot.right.head)), 4, in(b, B) ==> forall(a, in(a, A) ==> s0.bot.right.head), b)
+ SCProof(Vector(s0,s1,s2,s3,s4,s5))
+ }) // ∀b. (b ∈ ?B) ⇒ ∀a. (a ∈ ?A) ⇒ ∃!x. x= (a, b)
+
+ val s1 = InstPredSchema(instantiatePredicateSchemaInSequent(i1, psi, x===oPair(a,b), Seq(x, a, b)), -1, psi, x===oPair(a,b), Seq(x, a, b))
+ val s2 = Cut(()|-s1.bot.right, 0, 1, s1.bot.left.head)
+
+ val vA = VariableLabel("A")
+ val vB = VariableLabel("B")
+ val s3 = InstFunSchema(instantiateFunctionSchemaInSequent(s2.bot, SchematicFunctionLabel("A", 0), vA, Nil), 2, SchematicFunctionLabel("A", 0), vA, Nil)
+ val s4 = InstFunSchema(instantiateFunctionSchemaInSequent(s3.bot, SchematicFunctionLabel("B", 0), vA, Nil), 3, SchematicFunctionLabel("B", 0), vA, Nil)
+ val s5 = RightForall(()|- forall(vA, s4.bot.right.head), 4, s4.bot.right.head, vA)
+ val s6 = RightForall(()|- forall(vB, s5.bot.right.head), 5, s5.bot.right.head, vB)
+ SCProof(Vector(s0, s1, s2, s3, s4, s5, s6), Vector(i1))
+
+ }
+ println("cartesian")
+ val thm_lemmaCartesianProduct = theory.proofToTheorem(lemmaCartesianProduct, Seq(thm_lemmaMapTwoArguments)).get
+
+ val vA = VariableLabel("A")
+ val vB = VariableLabel("B")
+ val cart_product = ConstantFunctionLabel("cart_cross", 2)
+ val def_oPair = theory.makeFunctionDefinition(lemmaCartesianProduct, Seq(thm_lemmaMapTwoArguments), cart_product, Seq(vA, vB), VariableLabel("z"), innerOfDefinition(lemmaCartesianProduct.conclusion.right.head)).get
+
+
+
+
+
+
+ def innerOfDefinition(f:Formula):Formula = f match {
+ case BinderFormula(Forall, bound, inner) => innerOfDefinition(inner)
+ case BinderFormula(ExistsOne, bound, inner) => inner
+ case _ => f
+ }
+
+
+ //def makeFunctionalReplacement(t:Term)
+ def makeFunctional(t:Term):SCProof = {
+ val x = VariableLabel(freshId(t.freeVariables.map(_.id), "x"))
+ val y = VariableLabel(freshId(t.freeVariables.map(_.id), "y"))
+ val s0 = RightRefl(()|- t===t, t===t)
+ val s1 = Rewrite(() |- (x===t) <=> (x===t), 0)
+ val s2 = RightForall(() |- forall(x, (x===t) <=> (x===t)), 1, (x===t) <=> (x===t), x)
+ val s3 = RightExists(() |- exists(y, forall(x, (x===y) <=> (x===t))), 2, forall(x, (x===y) <=> (x===t)), y, t)
+ val s4 = Rewrite(() |- existsOne(x, x===t), 3)
+ SCProof(s0, s1, s2, s3, s4)
+ }
+
+
+
+ def main(args: Array[String]):Unit = {
+ def checkProof(proof: SCProof): Unit = {
+ val error = SCProofChecker.checkSCProof(proof)
+ println(prettySCProof(proof, error))
+ }
+/*
+ println("thmMapFunctional")
+ checkProof(thmMapFunctional)
+ println("lemma1")
+ checkProof(lemma1)
+ println("lemmaApplyFToObject")
+ checkProof(lemmaApplyFToObject)
+ println("lemmaMapTwoArguments")
+ checkProof(lemmaMapTwoArguments)
+ println("lemmaCartesianProduct")
+ checkProof(lemmaCartesianProduct)
+*/
+
+ }
+}
+// have union ∀x. ∀z. x ∈ Uz <=> ∃y. (x ∈ y /\ y ∈ z)
+// have x ∈ UY <=> ∃y. (x ∈ y /\ y ∈ Y)
+//
+//
+// goal ∀b. (b ∈ B) ⇒ ∀a. (a ∈ A) ⇒ ∃!x. ?psi(x, a, b) ⊢ ∃!X. ∀x. (x ∈ X) ↔ ∃b. (b ∈ B) ∧ ∃a. (a ∈ A) ∧ ?psi(x, a, b)
+// redGoal ∀b. (b ∈ B) ⇒ ∀a. (a ∈ A) ⇒ ∃!x. ?psi(x, a, b) ⊢ ∃Y. ∀X. (Y=X) <=> ∀x. (x ∈ X) ↔ ∃b. (b ∈ B) ∧ ∃a. (a ∈ A) ∧ ?psi(x, a, b)
+// redGoal ∀b. (b ∈ B) ⇒ ∀a. (a ∈ A) ⇒ ∃!x. ?psi(x, a, b), ∃!X. ∀x. (x ∈ X) ↔ ∃b. (b ∈ B) ∧ ∀x1. (x1 ∈ x) ↔ ∃a. (a ∈ A) ∧ ?psi(x1, a, b) ⊢ ∃Y. ∀X. (UY=X) <=> ∀x. (x ∈ X) ↔ ∃b. (b ∈ B) ∧ ∃a. (a ∈ A) ∧ ?psi(x, a, b)
+// redGoal ∀b. (b ∈ B) ⇒ ∀a. (a ∈ A) ⇒ ∃!x. ?psi(x, a, b), ∃Y. ∀X. (Y=X) <=> ∀x. (x ∈ X) ↔ ∃b. (b ∈ B) ∧ ∀x1. (x1 ∈ x) ↔ ∃a. (a ∈ A) ∧ ?psi(x1, a, b) ⊢ ∃Y. ∀X. (UY=X) <=> ∀x. (x ∈ X) ↔ ∃b. (b ∈ B) ∧ ∃a. (a ∈ A) ∧ ?psi(x, a, b)
+// redGoal ∀b. (b ∈ B) ⇒ ∀a. (a ∈ A) ⇒ ∃!x. ?psi(x, a, b), ∀X. (Y=X) <=> ∀x. (x ∈ X) ↔ ∃b. (b ∈ B) ∧ ∀x1. (x1 ∈ x) ↔ ∃a. (a ∈ A) ∧ ?psi(x1, a, b) ⊢ ∃Y. ∀X. (UY=X) <=> ∀x. (x ∈ X) ↔ ∃b. (b ∈ B) ∧ ∃a. (a ∈ A) ∧ ?psi(x, a, b)
+// redGoal ∀b. (b ∈ B) ⇒ ∀a. (a ∈ A) ⇒ ∃!x. ?psi(x, a, b), ∀X. (Y=X) <=> ∀x. (x ∈ X) ↔ ∃b. (b ∈ B) ∧ ∀x1. (x1 ∈ x) ↔ ∃a. (a ∈ A) ∧ ?psi(x1, a, b) ⊢ ∀X. (UY=X) <=> ∀x. (x ∈ X) ↔ ∃b. (b ∈ B) ∧ ∃a. (a ∈ A) ∧ ?psi(x, a, b)
+// redGoal ∀b. (b ∈ B) ⇒ ∀a. (a ∈ A) ⇒ ∃!x. ?psi(x, a, b), ∀X. (Y=X) <=> ∀x. (x ∈ X) ↔ ∃b. (b ∈ B) ∧ ∀x1. (x1 ∈ x) ↔ ∃a. (a ∈ A) ∧ ?psi(x1, a, b) ⊢ (UY=X) <=> ∀x. (x ∈ X) ↔ ∃b. (b ∈ B) ∧ ∃a. (a ∈ A) ∧ ?psi(x, a, b)
+// redGoal ∀b. (b ∈ B) ⇒ ∀a. (a ∈ A) ⇒ ∃!x. ?psi(x, a, b), (Y=X) <=> ∀x. (x ∈ X) ↔ ∃b. (b ∈ B) ∧ ∀x1. (x1 ∈ x) ↔ ∃a. (a ∈ A) ∧ ?psi(x1, a, b) ⊢ (UY=X) <=> ∀x. (x ∈ X) ↔ ∃b. (b ∈ B) ∧ ∃a. (a ∈ A) ∧ ?psi(x, a, b)
+// redGoal ∀b. (b ∈ B) ⇒ ∀a. (a ∈ A) ⇒ ∃!x. ?psi(x, a, b), (Y=X) <=> ∀x. (x ∈ X) ↔ ∃b. (b ∈ B) ∧ ∀x1. (x1 ∈ x) ↔ ∃a. (a ∈ A) ∧ ?psi(x1, a, b), x ∈ UY <=> ∃y. (x ∈ y /\ y ∈ Y) ⊢ (UY=X) <=> ∀x. (x ∈ X) ↔ ∃b. (b ∈ B) ∧ ∃a. (a ∈ A) ∧ ?psi(x, a, b)
+// redGoal1 ∀b. (b ∈ B) ⇒ ∀a. (a ∈ A) ⇒ ∃!x. ?psi(x, a, b), (Y=X) <=> ∀x. (x ∈ X) ↔ ∃b. (b ∈ B) ∧ ∀x1. (x1 ∈ x) ↔ ∃a. (a ∈ A) ∧ ?psi(x1, a, b), x ∈ UY <=> ∃y. (x ∈ y /\ y ∈ Y) ⊢ (UY=X) => ∀x. (x ∈ X) ↔ ∃b. (b ∈ B) ∧ ∃a. (a ∈ A) ∧ ?psi(x, a, b)
+// redGoal1 ∀b. (b ∈ B) ⇒ ∀a. (a ∈ A) ⇒ ∃!x. ?psi(x, a, b), (Y=X) <=> ∀x. (x ∈ X) ↔ ∃b. (b ∈ B) ∧ ∀x1. (x1 ∈ x) ↔ ∃a. (a ∈ A) ∧ ?psi(x1, a, b), x ∈ UY <=> ∃y. (x ∈ y /\ y ∈ Y), (UY=X) ⊢ ∀x. (x ∈ X) ↔ ∃b. (b ∈ B) ∧ ∃a. (a ∈ A) ∧ ?psi(x, a, b)
+// redGoal1 ∀b. (b ∈ B) ⇒ ∀a. (a ∈ A) ⇒ ∃!x. ?psi(x, a, b), (Y=X) <=> ∀x. (x ∈ X) ↔ ∃b. (b ∈ B) ∧ ∀x1. (x1 ∈ x) ↔ ∃a. (a ∈ A) ∧ ?psi(x1, a, b), x ∈ UY <=> ∃y. (x ∈ y /\ y ∈ Y), (UY=X) ⊢ ∀x. (x ∈ UY) ↔ ∃b. (b ∈ B) ∧ ∃a. (a ∈ A) ∧ ?psi(x, a, b)
+// redGoal1 ∀b. (b ∈ B) ⇒ ∀a. (a ∈ A) ⇒ ∃!x. ?psi(x, a, b), (Y=X) <=> ∀x. (x ∈ X) ↔ ∃b. (b ∈ B) ∧ ∀x1. (x1 ∈ x) ↔ ∃a. (a ∈ A) ∧ ?psi(x1, a, b), x ∈ UY <=> ∃y. (x ∈ y /\ y ∈ Y), (UY=X) ⊢ ∀x. (x ∈ UY) ↔ ∃b. (b ∈ B) ∧ ∃a. (a ∈ A) ∧ ?psi(x, a, b)
+// redGoal2 ∀b. (b ∈ B) ⇒ ∀a. (a ∈ A) ⇒ ∃!x. ?psi(x, a, b), (Y=X) <=> ∀x. (x ∈ X) ↔ ∃b. (b ∈ B) ∧ ∀x1. (x1 ∈ x) ↔ ∃a. (a ∈ A) ∧ ?psi(x1, a, b), x ∈ UY <=> ∃y. (x ∈ y /\ y ∈ Y) ⊢ (UY=X) <= ∀x. (x ∈ X) ↔ ∃b. (b ∈ B) ∧ ∃a. (a ∈ A) ∧ ?psi(x, a, b)
diff --git a/src/main/scala/proven/ElementsOfSetTheory.scala b/src/main/scala/proven/ElementsOfSetTheory.scala
index 532affc320fa833ab89d643aa76a76450ef347ed..a103dbe012cb0c87d5bf4dfe44dc9027716c8009 100644
--- a/src/main/scala/proven/ElementsOfSetTheory.scala
+++ b/src/main/scala/proven/ElementsOfSetTheory.scala
@@ -9,6 +9,7 @@ import lisa.settheory.AxiomaticSetTheory.*
import scala.collection.immutable.SortedSet
import lisa.kernel.proof.{SCProof, SCProofChecker}
+import lisa.settheory.AxiomaticSetTheory
import scala.collection.immutable
@@ -17,6 +18,9 @@ import scala.collection.immutable
*/
object ElementsOfSetTheory {
+ val theory = AxiomaticSetTheory.runningSetTheory
+ def axiom(f:Formula) = theory.getAxioms.find(c => c.ax == f).get
+
private val x = VariableLabel("x")
private val y = VariableLabel("y")
private val x1 = VariableLabel("x'")
@@ -25,9 +29,9 @@ object ElementsOfSetTheory {
private val g = SchematicFunctionLabel("g", 0)
private val h = SchematicPredicateLabel("h", 0)
- val oPair: FunctionLabel = ConstantFunctionLabel("ordered_pair", 2)
- val oPairFirstElement: FunctionLabel = ConstantFunctionLabel("ordered_pair_first_element", 1)
- val oPairSecondElement: FunctionLabel = ConstantFunctionLabel("ordered_pair_second_element", 1)
+ val oPair: ConstantFunctionLabel = ConstantFunctionLabel("ordered_pair", 2)
+ val oPairFirstElement: ConstantFunctionLabel = ConstantFunctionLabel("ordered_pair_first_element", 1)
+ val oPairSecondElement: ConstantFunctionLabel = ConstantFunctionLabel("ordered_pair_second_element", 1)
val proofUnorderedPairSymmetry: SCProof = {
val imps: IndexedSeq[Sequent] = IndexedSeq(() |- extensionalityAxiom, () |- pairAxiom)
@@ -61,6 +65,8 @@ object ElementsOfSetTheory {
val fin4 = generalizeToForall(fin3, fin3.conclusion.right.head, y)
fin4.copy(imports = imps)
} // |- ∀∀({x$1,y$2}={y$2,x$1})
+ val thm_proofUnorderedPairSymmetry = theory.proofToTheorem(proofUnorderedPairSymmetry, Seq(axiom(extensionalityAxiom), axiom(pairAxiom))).get
+
val proofUnorderedPairDeconstruction: SCProof = {
val pxy = pair(x, y)
@@ -217,11 +223,14 @@ object ElementsOfSetTheory {
val p2 = RightImplies(emptySeq +> (p1.bot.left.head ==> p1.bot.right.head), 1, p1.bot.left.head, p1.bot.right.head) // |- ({x,y}={x',y'}) ==> (x=x' /\ y=y')\/(x=y' /\ y=x')
generalizeToForall(SCProof(IndexedSeq(p0, p1, p2), IndexedSeq(()|-pairAxiom)), x, y, x1, y1)
} // |- ∀∀∀∀(({x$4,y$3}={x'$2,y'$1})⇒(((y'$1=y$3)∧(x'$2=x$4))∨((x$4=y'$1)∧(y$3=x'$2))))
-
+ val thm_proofUnorderedPairDeconstruction = theory.proofToTheorem(proofUnorderedPairDeconstruction, Seq(axiom(pairAxiom))).get
// i2, i1, p0, p1, p2, p3
- val orderedPairDefinition: SCProof = simpleFunctionDefinition(oPair, pair(pair(x, y), pair(x, x)), Seq(x, y))
+ val orderedPairDefinition: SCProof = simpleFunctionDefinition(pair(pair(x, y), pair(x, x)), Seq(x, y))
+
+ println("def_oPair")
+ val def_oPair = theory.makeFunctionDefinition(orderedPairDefinition, Nil, oPair, Seq(x, y), x1, x1 === pair(pair(x, y), pair(x, x)))
/*
val proofOrderedPairDeconstruction: SCProof = {
diff --git a/src/main/scala/proven/tactics/Destructors.scala b/src/main/scala/proven/tactics/Destructors.scala
index 9bec6109136a16befdc89f2278ef76cc0c44a78f..55b47107cb506a769cc89a071757f081d62aa0ed 100644
--- a/src/main/scala/proven/tactics/Destructors.scala
+++ b/src/main/scala/proven/tactics/Destructors.scala
@@ -19,7 +19,7 @@ object Destructors {
def destructRightAnd(p: SCProof, f: Formula, g: Formula): SCProof = {
val p0 = hypothesis(f) // n
val p1 = LeftAnd(emptySeq +< (f /\ g) +> f, p.length, f, g) // n+1
- val p2 = Cut(p.conclusion -> (f /\ g) +> f, p.length - 1, p.length + 1, f /\ g)
+ val p2 = Cut(p.conclusion -> (f /\ g) ->(g/\f) +> f, p.length - 1, p.length + 1, f /\ g)
p withNewSteps IndexedSeq(p0, p1, p2)
}
def destructRightImplies(p: SCProof, f: Formula, g: Formula): SCProof = { // |- f=>g
diff --git a/src/main/scala/proven/tactics/ProofTactics.scala b/src/main/scala/proven/tactics/ProofTactics.scala
index d7d087186f71eb88c570d1867910f595e36e56ae..d78ba8e88aefab7c947a4a8d5262bea9e88f2367 100644
--- a/src/main/scala/proven/tactics/ProofTactics.scala
+++ b/src/main/scala/proven/tactics/ProofTactics.scala
@@ -65,23 +65,22 @@ object ProofTactics {
case _ => throw new Error("not applicable")
}
}
- def simpleFunctionDefinition(f: FunctionLabel, t: Term, args: Seq[VariableLabel]): SCProof = {
- assert(t.freeVariables subsetOf args.toSet)
+
+ def simpleFunctionDefinition(t: Term, args: Seq[VariableLabel]): SCProof = {
val x = VariableLabel(freshId(t.freeVariables.map(_.id), "x"))
- val y = VariableLabel(freshId(t.freeVariables.map(_.id)+x.id, "x"))
- val p0 = RightRefl(emptySeq +> (t === t), t === t) // |- t===t
- val p1 = hypothesis(y === t) // (t===y)|-(t===y)
- val p2 = RightImplies(emptySeq +> ((t === y) ==> (t === y)), 1, t === y, t === y) // |- (t===y)==>(t===y)
- val p3 = RightForall(emptySeq +> forall(y, (t === y) ==> (t === y)), 2, p2.bot.right.head, y) // |- ∀y (t===y)==>(t===y)
- val p4 = RightAnd(emptySeq +> p0.bot.right.head /\ p3.bot.right.head, Seq(0, 3), Seq(p0.bot.right.head, p3.bot.right.head)) // |- t===t /\ ∀y(t===y)==>(t===y)
- val p5 = RightExists(emptySeq +> exists(x, (x === t) /\ forall(y, (t === y) ==> (x === y))), 4,
- (x === t) /\ forall(y, (t === y) ==> (x === y)), x, t) // |- ∃x x === t /\ ∀y(t===y)==>(x===y)
- val definition = SCProof(IndexedSeq(p0, p1, p2, p3, p4, p5))
- val fdef = args.foldLeft((definition.steps, p5.bot.right.head, 5))((prev, x) => {
+ val y = VariableLabel(freshId(t.freeVariables.map(_.id), "y"))
+ val s0 = RightRefl(() |- t === t, t === t)
+ val s1 = Rewrite(() |- (x === t) <=> (x === t), 0)
+ val s2 = RightForall(() |- forall(x, (x === t) <=> (x === t)), 1, (x === t) <=> (x === t), x)
+ val s3 = RightExists(() |- exists(y, forall(x, (x === y) <=> (x === t))), 2, forall(x, (x === y) <=> (x === t)), y, t)
+ val s4 = Rewrite(() |- existsOne(x, x === t), 3)
+ val v = Vector(s0, s1, s2, s3, s4)
+ val v2 = args.foldLeft((v, s4.bot.right.head, 4))((prev, x) => {
val fo = forall(x, prev._2)
(prev._1 appended RightForall(emptySeq +> fo, prev._3, prev._2, x), fo, prev._3 + 1)
})
- SCProof(fdef._1 )
+ SCProof(v2._1)
+
}
// p1 is a proof of psi given phi, p2 is a proof of psi given !phi
def byCase(phi: Formula)(pa: SCProofStep, pb: SCProofStep): SCProof = {
@@ -112,7 +111,7 @@ object ProofTactics {
SCProof(pa, pb, p2, p3, p4)
}
}
-
+
def detectSubstitution(x: VariableLabel, f: Formula, s: Formula, c: Option[Term] = None): (Option[Term], Boolean) = (f, s) match {
case (PredicateFormula(la1, args1), PredicateFormula(la2, args2)) if isSame(la1, la2) => {
args1.zip(args2).foldLeft[(Option[Term], Boolean)](c, true)((r1, a) => {