internlm/Lean-Github huggingface dataset:
Theorem: FOL.NV.T_19_TS_21_left
Proof state before:
case h1.a.a
P Q : Formula
v : VarName
h1 : ¬isFreeIn v P
⊢ IsReplOfFormulaInFormula (forall_ v P) P (forall_ v P) P
Tactic:
apply IsReplOfFormulaInFormula.diff_
Proof state after:
case h1.a.a.a
P Q : Formula
v : VarName
h1 : ¬isFreeIn v P
⊢ forall_ v P = forall_ v P

case h1.a.a.a
P Q : Formula
v : VarName
h1 : ¬isFreeIn v P
⊢ P = P
Theorem: FOL.NV.T_19_TS_21_left
Proof state before:
case h1.a.a.a
P Q : Formula
v : VarName
h1 : ¬isFreeIn v P
⊢ forall_ v P = forall_ v P
Tactic:
rfl
Proof state after:
no goals
Theorem: FOL.NV.T_19_TS_21_left
Proof state before:
case h1.a.a.a
P Q : Formula
v : VarName
h1 : ¬isFreeIn v P
⊢ P = P
Tactic:
rfl
Proof state after:
no goals
Theorem: FOL.NV.T_19_TS_21_left
Proof state before:
case h1.a.a
P Q : Formula
v : VarName
h1 : ¬isFreeIn v P
⊢ IsReplOfFormulaInFormula (forall_ v P) P (forall_ v Q) (forall_ v Q)
Tactic:
apply IsReplOfFormulaInFormula.same_
Proof state after:
case h1.a.a.a
P Q : Formula
v : VarName
h1 : ¬isFreeIn v P
⊢ forall_ v Q = forall_ v Q
Theorem: FOL.NV.T_19_TS_21_left
Proof state before:
case h1.a.a.a
P Q : Formula
v : VarName
h1 : ¬isFreeIn v P
⊢ forall_ v Q = forall_ v Q
Tactic:
rfl
Proof state after:
no goals
Theorem: FOL.NV.T_19_TS_21_left
Proof state before:
case h2
P Q : Formula
v : VarName
h1 : ¬isFreeIn v P
⊢ IsProof ((forall_ v P).iff_ P)
Tactic:
exact T_19_1 P v h1
Proof state after:
no goals
Theorem: FOL.NV.T_19_TS_21_left
Proof state before:
case h3
P Q : Formula
v : VarName
h1 : ¬isFreeIn v P
⊢ IsDeduct ∅ ((forall_ v (P.imp_ Q)).imp_ ((forall_ v P).imp_ (forall_ v Q)))
Tactic:
apply IsDeduct.axiom_
Proof state after:
case h3.a
P Q : Formula
v : VarName
h1 : ¬isFreeIn v P
⊢ IsAxiom ((forall_ v (P.imp_ Q)).imp_ ((forall_ v P).imp_ (forall_ v Q)))
Theorem: FOL.NV.T_19_TS_21_left
Proof state before:
case h3.a
P Q : Formula
v : VarName
h1 : ¬isFreeIn v P
⊢ IsAxiom ((forall_ v (P.imp_ Q)).imp_ ((forall_ v P).imp_ (forall_ v Q)))
Tactic:
apply IsAxiom.pred_1_
Proof state after:
no goals
Theorem: FOL.NV.T_19_TS_21_right
Proof state before:
P Q : Formula
v : VarName
h1 : ¬isFreeIn v P
⊢ IsProof ((P.imp_ (forall_ v Q)).imp_ (forall_ v (P.imp_ Q)))
Tactic:
apply deduction_theorem
Proof state after:
case h1
P Q : Formula
v : VarName
h1 : ¬isFreeIn v P
⊢ IsDeduct (∅ ∪ {P.imp_ (forall_ v Q)}) (forall_ v (P.imp_ Q))
Theorem: FOL.NV.T_19_TS_21_right
Proof state before:
case h1
P Q : Formula
v : VarName
h1 : ¬isFreeIn v P
⊢ IsDeduct (∅ ∪ {P.imp_ (forall_ v Q)}) (forall_ v (P.imp_ Q))
Tactic:
simp
Proof state after:
case h1
P Q : Formula
v : VarName
h1 : ¬isFreeIn v P
⊢ IsDeduct {P.imp_ (forall_ v Q)} (forall_ v (P.imp_ Q))
Theorem: FOL.NV.T_19_TS_21_right
Proof state before:
case h1
P Q : Formula
v : VarName
h1 : ¬isFreeIn v P
⊢ IsDeduct {P.imp_ (forall_ v Q)} (forall_ v (P.imp_ Q))
Tactic:
apply generalization
Proof state after:
case h1.h1
P Q : Formula
v : VarName
h1 : ¬isFreeIn v P
⊢ IsDeduct {P.imp_ (forall_ v Q)} (P.imp_ Q)

case h1.h2
P Q : Formula
v : VarName
h1 : ¬isFreeIn v P
⊢ ∀ H ∈ {P.imp_ (forall_ v Q)}, ¬isFreeIn v H
Theorem: FOL.NV.T_19_TS_21_right
Proof state before:
case h1.h1
P Q : Formula
v : VarName
h1 : ¬isFreeIn v P
⊢ IsDeduct {P.imp_ (forall_ v Q)} (P.imp_ Q)
Tactic:
apply deduction_theorem
Proof state after:
case h1.h1.h1
P Q : Formula
v : VarName
h1 : ¬isFreeIn v P
⊢ IsDeduct ({P.imp_ (forall_ v Q)} ∪ {P}) Q
Theorem: FOL.NV.T_19_TS_21_right
Proof state before:
case h1.h1.h1
P Q : Formula
v : VarName
h1 : ¬isFreeIn v P
⊢ IsDeduct ({P.imp_ (forall_ v Q)} ∪ {P}) Q
Tactic:
apply specId v
Proof state after:
case h1.h1.h1.h1
P Q : Formula
v : VarName
h1 : ¬isFreeIn v P
⊢ IsDeduct ({P.imp_ (forall_ v Q)} ∪ {P}) (forall_ v Q)
Theorem: FOL.NV.T_19_TS_21_right
Proof state before:
case h1.h1.h1.h1
P Q : Formula
v : VarName
h1 : ¬isFreeIn v P
⊢ IsDeduct ({P.imp_ (forall_ v Q)} ∪ {P}) (forall_ v Q)
Tactic:
apply IsDeduct.mp_ P
Proof state after:
case h1.h1.h1.h1.a
P Q : Formula
v : VarName
h1 : ¬isFreeIn v P
⊢ IsDeduct ({P.imp_ (forall_ v Q)} ∪ {P}) (P.imp_ (forall_ v Q))

case h1.h1.h1.h1.a
P Q : Formula
v : VarName
h1 : ¬isFreeIn v P
⊢ IsDeduct ({P.imp_ (forall_ v Q)} ∪ {P}) P
Theorem: FOL.NV.T_19_TS_21_right
Proof state before:
case h1.h1.h1.h1.a
P Q : Formula
v : VarName
h1 : ¬isFreeIn v P
⊢ IsDeduct ({P.imp_ (forall_ v Q)} ∪ {P}) (P.imp_ (forall_ v Q))
Tactic:
apply IsDeduct.assume_
Proof state after:
case h1.h1.h1.h1.a.a
P Q : Formula
v : VarName
h1 : ¬isFreeIn v P
⊢ P.imp_ (forall_ v Q) ∈ {P.imp_ (forall_ v Q)} ∪ {P}
Theorem: FOL.NV.T_19_TS_21_right
Proof state before:
case h1.h1.h1.h1.a.a
P Q : Formula
v : VarName
h1 : ¬isFreeIn v P
⊢ P.imp_ (forall_ v Q) ∈ {P.imp_ (forall_ v Q)} ∪ {P}
Tactic:
simp
Proof state after:
no goals
Theorem: FOL.NV.T_19_TS_21_right
Proof state before:
case h1.h1.h1.h1.a
P Q : Formula
v : VarName
h1 : ¬isFreeIn v P
⊢ IsDeduct ({P.imp_ (forall_ v Q)} ∪ {P}) P
Tactic:
apply IsDeduct.assume_
Proof state after:
case h1.h1.h1.h1.a.a
P Q : Formula
v : VarName
h1 : ¬isFreeIn v P
⊢ P ∈ {P.imp_ (forall_ v Q)} ∪ {P}
Theorem: FOL.NV.T_19_TS_21_right
Proof state before:
case h1.h1.h1.h1.a.a
P Q : Formula
v : VarName
h1 : ¬isFreeIn v P
⊢ P ∈ {P.imp_ (forall_ v Q)} ∪ {P}
Tactic:
simp
Proof state after:
no goals
Theorem: FOL.NV.T_19_TS_21_right
Proof state before:
case h1.h2
P Q : Formula
v : VarName
h1 : ¬isFreeIn v P
⊢ ∀ H ∈ {P.imp_ (forall_ v Q)}, ¬isFreeIn v H
Tactic:
intro H a1
Proof state after:
case h1.h2
P Q : Formula
v : VarName
h1 : ¬isFreeIn v P
H : Formula
a1 : H ∈ {P.imp_ (forall_ v Q)}
⊢ ¬isFreeIn v H
Theorem: FOL.NV.T_19_TS_21_right
Proof state before:
case h1.h2
P Q : Formula
v : VarName
h1 : ¬isFreeIn v P
H : Formula
a1 : H ∈ {P.imp_ (forall_ v Q)}
⊢ ¬isFreeIn v H
Tactic:
simp at a1
Proof state after:
case h1.h2
P Q : Formula
v : VarName
h1 : ¬isFreeIn v P
H : Formula
a1 : H = P.imp_ (forall_ v Q)
⊢ ¬isFreeIn v H
Theorem: FOL.NV.T_19_TS_21_right
Proof state before:
case h1.h2
P Q : Formula
v : VarName
h1 : ¬isFreeIn v P
H : Formula
a1 : H = P.imp_ (forall_ v Q)
⊢ ¬isFreeIn v H
Tactic:
subst a1
Proof state after:
case h1.h2
P Q : Formula
v : VarName
h1 : ¬isFreeIn v P
⊢ ¬isFreeIn v (P.imp_ (forall_ v Q))
Theorem: FOL.NV.T_19_TS_21_right
Proof state before:
case h1.h2
P Q : Formula
v : VarName
h1 : ¬isFreeIn v P
⊢ ¬isFreeIn v (P.imp_ (forall_ v Q))
Tactic:
simp only [isFreeIn]
Proof state after:
case h1.h2
P Q : Formula
v : VarName
h1 : ¬isFreeIn v P
⊢ ¬(isFreeIn v P ∨ ¬True ∧ isFreeIn v Q)
Theorem: FOL.NV.T_19_TS_21_right
Proof state before:
case h1.h2
P Q : Formula
v : VarName
h1 : ¬isFreeIn v P
⊢ ¬(isFreeIn v P ∨ ¬True ∧ isFreeIn v Q)
Tactic:
simp
Proof state after:
case h1.h2
P Q : Formula
v : VarName
h1 : ¬isFreeIn v P
⊢ ¬isFreeIn v P
Theorem: FOL.NV.T_19_TS_21_right
Proof state before:
case h1.h2
P Q : Formula
v : VarName
h1 : ¬isFreeIn v P
⊢ ¬isFreeIn v P
Tactic:
exact h1
Proof state after:
no goals
Theorem: FOL.NV.T_19_TS_21
Proof state before:
P Q : Formula
v : VarName
h1 : ¬isFreeIn v P
⊢ IsProof ((forall_ v (P.imp_ Q)).iff_ (P.imp_ (forall_ v Q)))
Tactic:
apply IsDeduct.mp_ ((forall_ v (P.imp_ Q)).imp_ (P.imp_ (forall_ v Q)))
Proof state after:
case a
P Q : Formula
v : VarName
h1 : ¬isFreeIn v P
⊢ IsDeduct ∅
    (((forall_ v (P.imp_ Q)).imp_ (P.imp_ (forall_ v Q))).imp_ ((forall_ v (P.imp_ Q)).iff_ (P.imp_ (forall_ v Q))))

case a
P Q : Formula
v : VarName
h1 : ¬isFreeIn v P
⊢ IsDeduct ∅ ((forall_ v (P.imp_ Q)).imp_ (P.imp_ (forall_ v Q)))
Theorem: FOL.NV.T_19_TS_21
Proof state before:
case a
P Q : Formula
v : VarName
h1 : ¬isFreeIn v P
⊢ IsDeduct ∅
    (((forall_ v (P.imp_ Q)).imp_ (P.imp_ (forall_ v Q))).imp_ ((forall_ v (P.imp_ Q)).iff_ (P.imp_ (forall_ v Q))))
Tactic:
apply IsDeduct.mp_ ((P.imp_ (forall_ v Q)).imp_ (forall_ v (P.imp_ Q)))
Proof state after:
case a.a
P Q : Formula
v : VarName
h1 : ¬isFreeIn v P
⊢ IsDeduct ∅
    (((P.imp_ (forall_ v Q)).imp_ (forall_ v (P.imp_ Q))).imp_
      (((forall_ v (P.imp_ Q)).imp_ (P.imp_ (forall_ v Q))).imp_ ((forall_ v (P.imp_ Q)).iff_ (P.imp_ (forall_ v Q)))))

case a.a
P Q : Formula
v : VarName
h1 : ¬isFreeIn v P
⊢ IsDeduct ∅ ((P.imp_ (forall_ v Q)).imp_ (forall_ v (P.imp_ Q)))
Theorem: FOL.NV.T_19_TS_21
Proof state before:
case a.a
P Q : Formula
v : VarName
h1 : ¬isFreeIn v P
⊢ IsDeduct ∅
    (((P.imp_ (forall_ v Q)).imp_ (forall_ v (P.imp_ Q))).imp_
      (((forall_ v (P.imp_ Q)).imp_ (P.imp_ (forall_ v Q))).imp_ ((forall_ v (P.imp_ Q)).iff_ (P.imp_ (forall_ v Q)))))
Tactic:
simp only [def_iff_]
Proof state after:
case a.a
P Q : Formula
v : VarName
h1 : ¬isFreeIn v P
⊢ IsDeduct ∅
    (((P.imp_ (forall_ v Q)).imp_ (forall_ v (P.imp_ Q))).imp_
      (((forall_ v (P.imp_ Q)).imp_ (P.imp_ (forall_ v Q))).imp_
        (((forall_ v (P.imp_ Q)).imp_ (P.imp_ (forall_ v Q))).and_
          ((P.imp_ (forall_ v Q)).imp_ (forall_ v (P.imp_ Q))))))
Theorem: FOL.NV.T_19_TS_21
Proof state before:
case a.a
P Q : Formula
v : VarName
h1 : ¬isFreeIn v P
⊢ IsDeduct ∅
    (((P.imp_ (forall_ v Q)).imp_ (forall_ v (P.imp_ Q))).imp_
      (((forall_ v (P.imp_ Q)).imp_ (P.imp_ (forall_ v Q))).imp_
        (((forall_ v (P.imp_ Q)).imp_ (P.imp_ (forall_ v Q))).and_
          ((P.imp_ (forall_ v Q)).imp_ (forall_ v (P.imp_ Q))))))
Tactic:
simp only [def_and_]
Proof state after:
case a.a
P Q : Formula
v : VarName
h1 : ¬isFreeIn v P
⊢ IsDeduct ∅
    (((P.imp_ (forall_ v Q)).imp_ (forall_ v (P.imp_ Q))).imp_
      (((forall_ v (P.imp_ Q)).imp_ (P.imp_ (forall_ v Q))).imp_
        (((forall_ v (P.imp_ Q)).imp_ (P.imp_ (forall_ v Q))).imp_
            ((P.imp_ (forall_ v Q)).imp_ (forall_ v (P.imp_ Q))).not_).not_))
Theorem: FOL.NV.T_19_TS_21
Proof state before:
case a.a
P Q : Formula
v : VarName
h1 : ¬isFreeIn v P
⊢ IsDeduct ∅
    (((P.imp_ (forall_ v Q)).imp_ (forall_ v (P.imp_ Q))).imp_
      (((forall_ v (P.imp_ Q)).imp_ (P.imp_ (forall_ v Q))).imp_
        (((forall_ v (P.imp_ Q)).imp_ (P.imp_ (forall_ v Q))).imp_
            ((P.imp_ (forall_ v Q)).imp_ (forall_ v (P.imp_ Q))).not_).not_))
Tactic:
SC
Proof state after:
no goals
Theorem: FOL.NV.T_19_TS_21
Proof state before:
case a.a
P Q : Formula
v : VarName
h1 : ¬isFreeIn v P
⊢ IsDeduct ∅ ((P.imp_ (forall_ v Q)).imp_ (forall_ v (P.imp_ Q)))
Tactic:
exact T_19_TS_21_right P Q v h1
Proof state after:
no goals
Theorem: FOL.NV.T_19_TS_21
Proof state before:
case a
P Q : Formula
v : VarName
h1 : ¬isFreeIn v P
⊢ IsDeduct ∅ ((forall_ v (P.imp_ Q)).imp_ (P.imp_ (forall_ v Q)))
Tactic:
exact T_19_TS_21_left P Q v h1
Proof state after:
no goals
Theorem: FOL.NV.T_21_1
Proof state before:
x y : VarName
⊢ IsProof (forall_ x (forall_ y ((eq_ x y).imp_ (eq_ y x))))
Tactic:
apply generalization
Proof state after:
case h1
x y : VarName
⊢ IsDeduct ∅ (forall_ y ((eq_ x y).imp_ (eq_ y x)))

case h2
x y : VarName
⊢ ∀ H ∈ ∅, ¬isFreeIn x H
Theorem: FOL.NV.T_21_1
Proof state before:
case h1
x y : VarName
⊢ IsDeduct ∅ (forall_ y ((eq_ x y).imp_ (eq_ y x)))
Tactic:
apply generalization
Proof state after:
case h1.h1
x y : VarName
⊢ IsDeduct ∅ ((eq_ x y).imp_ (eq_ y x))

case h1.h2
x y : VarName
⊢ ∀ H ∈ ∅, ¬isFreeIn y H
Theorem: FOL.NV.T_21_1
Proof state before:
case h1.h1
x y : VarName
⊢ IsDeduct ∅ ((eq_ x y).imp_ (eq_ y x))
Tactic:
apply IsDeduct.mp_ (eq_ y y)
Proof state after:
case h1.h1.a
x y : VarName
⊢ IsDeduct ∅ ((eq_ y y).imp_ ((eq_ x y).imp_ (eq_ y x)))

case h1.h1.a
x y : VarName
⊢ IsDeduct ∅ (eq_ y y)
Theorem: FOL.NV.T_21_1
Proof state before:
case h1.h1.a
x y : VarName
⊢ IsDeduct ∅ ((eq_ y y).imp_ ((eq_ x y).imp_ (eq_ y x)))
Tactic:
apply IsDeduct.mp_ (((eq_ y y).and_ (eq_ x y)).imp_ ((eq_ y x).iff_ (eq_ y y)))
Proof state after:
case h1.h1.a.a
x y : VarName
⊢ IsDeduct ∅
    ((((eq_ y y).and_ (eq_ x y)).imp_ ((eq_ y x).iff_ (eq_ y y))).imp_ ((eq_ y y).imp_ ((eq_ x y).imp_ (eq_ y x))))

case h1.h1.a.a
x y : VarName
⊢ IsDeduct ∅ (((eq_ y y).and_ (eq_ x y)).imp_ ((eq_ y x).iff_ (eq_ y y)))
Theorem: FOL.NV.T_21_1
Proof state before:
case h1.h1.a.a
x y : VarName
⊢ IsDeduct ∅
    ((((eq_ y y).and_ (eq_ x y)).imp_ ((eq_ y x).iff_ (eq_ y y))).imp_ ((eq_ y y).imp_ ((eq_ x y).imp_ (eq_ y x))))
Tactic:
simp only [def_iff_]
Proof state after:
case h1.h1.a.a
x y : VarName
⊢ IsDeduct ∅
    ((((eq_ y y).and_ (eq_ x y)).imp_ (((eq_ y x).imp_ (eq_ y y)).and_ ((eq_ y y).imp_ (eq_ y x)))).imp_
      ((eq_ y y).imp_ ((eq_ x y).imp_ (eq_ y x))))
Theorem: FOL.NV.T_21_1
Proof state before:
case h1.h1.a.a
x y : VarName
⊢ IsDeduct ∅
    ((((eq_ y y).and_ (eq_ x y)).imp_ (((eq_ y x).imp_ (eq_ y y)).and_ ((eq_ y y).imp_ (eq_ y x)))).imp_
      ((eq_ y y).imp_ ((eq_ x y).imp_ (eq_ y x))))
Tactic:
simp only [def_and_]
Proof state after:
case h1.h1.a.a
x y : VarName
⊢ IsDeduct ∅
    ((((eq_ y y).imp_ (eq_ x y).not_).not_.imp_
          (((eq_ y x).imp_ (eq_ y y)).imp_ ((eq_ y y).imp_ (eq_ y x)).not_).not_).imp_
      ((eq_ y y).imp_ ((eq_ x y).imp_ (eq_ y x))))
Theorem: FOL.NV.T_21_1
Proof state before:
case h1.h1.a.a
x y : VarName
⊢ IsDeduct ∅
    ((((eq_ y y).imp_ (eq_ x y).not_).not_.imp_
          (((eq_ y x).imp_ (eq_ y y)).imp_ ((eq_ y y).imp_ (eq_ y x)).not_).not_).imp_
      ((eq_ y y).imp_ ((eq_ x y).imp_ (eq_ y x))))
Tactic:
SC
Proof state after:
no goals
Theorem: FOL.NV.T_21_1
Proof state before:
case h1.h1.a.a
x y : VarName
⊢ IsDeduct ∅ (((eq_ y y).and_ (eq_ x y)).imp_ ((eq_ y x).iff_ (eq_ y y)))
Tactic:
apply specId y
Proof state after:
case h1.h1.a.a.h1
x y : VarName
⊢ IsDeduct ∅ (forall_ y (((eq_ y y).and_ (eq_ x y)).imp_ ((eq_ y x).iff_ (eq_ y y))))
Theorem: FOL.NV.T_21_1
Proof state before:
case h1.h1.a.a.h1
x y : VarName
⊢ IsDeduct ∅ (forall_ y (((eq_ y y).and_ (eq_ x y)).imp_ ((eq_ y x).iff_ (eq_ y y))))
Tactic:
apply specId y
Proof state after:
case h1.h1.a.a.h1.h1
x y : VarName
⊢ IsDeduct ∅ (forall_ y (forall_ y (((eq_ y y).and_ (eq_ x y)).imp_ ((eq_ y x).iff_ (eq_ y y)))))
Theorem: FOL.NV.T_21_1
Proof state before:
case h1.h1.a.a.h1.h1
x y : VarName
⊢ IsDeduct ∅ (forall_ y (forall_ y (((eq_ y y).and_ (eq_ x y)).imp_ ((eq_ y x).iff_ (eq_ y y)))))
Tactic:
apply specId x
Proof state after:
case h1.h1.a.a.h1.h1.h1
x y : VarName
⊢ IsDeduct ∅ (forall_ x (forall_ y (forall_ y (((eq_ y y).and_ (eq_ x y)).imp_ ((eq_ y x).iff_ (eq_ y y))))))
Theorem: FOL.NV.T_21_1
Proof state before:
case h1.h1.a.a.h1.h1.h1
x y : VarName
⊢ IsDeduct ∅ (forall_ x (forall_ y (forall_ y (((eq_ y y).and_ (eq_ x y)).imp_ ((eq_ y x).iff_ (eq_ y y))))))
Tactic:
apply specId y
Proof state after:
case h1.h1.a.a.h1.h1.h1.h1
x y : VarName
⊢ IsDeduct ∅
    (forall_ y (forall_ x (forall_ y (forall_ y (((eq_ y y).and_ (eq_ x y)).imp_ ((eq_ y x).iff_ (eq_ y y)))))))
Theorem: FOL.NV.T_21_1
Proof state before:
case h1.h1.a.a.h1.h1.h1.h1
x y : VarName
⊢ IsDeduct ∅
    (forall_ y (forall_ x (forall_ y (forall_ y (((eq_ y y).and_ (eq_ x y)).imp_ ((eq_ y x).iff_ (eq_ y y)))))))
Tactic:
apply IsDeduct.axiom_
Proof state after:
case h1.h1.a.a.h1.h1.h1.h1.a
x y : VarName
⊢ IsAxiom (forall_ y (forall_ x (forall_ y (forall_ y (((eq_ y y).and_ (eq_ x y)).imp_ ((eq_ y x).iff_ (eq_ y y)))))))
Theorem: FOL.NV.T_21_1
Proof state before:
case h1.h1.a.a.h1.h1.h1.h1.a
x y : VarName
⊢ IsAxiom (forall_ y (forall_ x (forall_ y (forall_ y (((eq_ y y).and_ (eq_ x y)).imp_ ((eq_ y x).iff_ (eq_ y y)))))))
Tactic:
exact IsAxiom.eq_2_eq_ y x y y
Proof state after:
no goals
Theorem: FOL.NV.T_21_1
Proof state before:
case h1.h1.a
x y : VarName
⊢ IsDeduct ∅ (eq_ y y)
Tactic:
apply specId y
Proof state after:
case h1.h1.a.h1
x y : VarName
⊢ IsDeduct ∅ (forall_ y (eq_ y y))
Theorem: FOL.NV.T_21_1
Proof state before:
case h1.h1.a.h1
x y : VarName
⊢ IsDeduct ∅ (forall_ y (eq_ y y))
Tactic:
apply IsDeduct.axiom_
Proof state after:
case h1.h1.a.h1.a
x y : VarName
⊢ IsAxiom (forall_ y (eq_ y y))
Theorem: FOL.NV.T_21_1
Proof state before:
case h1.h1.a.h1.a
x y : VarName
⊢ IsAxiom (forall_ y (eq_ y y))
Tactic:
exact IsAxiom.eq_1_ y
Proof state after:
no goals
Theorem: FOL.NV.T_21_1
Proof state before:
case h1.h2
x y : VarName
⊢ ∀ H ∈ ∅, ¬isFreeIn y H
Tactic:
intro H a1
Proof state after:
case h1.h2
x y : VarName
H : Formula
a1 : H ∈ ∅
⊢ ¬isFreeIn y H
Theorem: FOL.NV.T_21_1
Proof state before:
case h1.h2
x y : VarName
H : Formula
a1 : H ∈ ∅
⊢ ¬isFreeIn y H
Tactic:
simp at a1
Proof state after:
no goals
Theorem: FOL.NV.T_21_1
Proof state before:
case h2
x y : VarName
⊢ ∀ H ∈ ∅, ¬isFreeIn x H
Tactic:
intro H a1
Proof state after:
case h2
x y : VarName
H : Formula
a1 : H ∈ ∅
⊢ ¬isFreeIn x H
Theorem: FOL.NV.T_21_1
Proof state before:
case h2
x y : VarName
H : Formula
a1 : H ∈ ∅
⊢ ¬isFreeIn x H
Tactic:
simp at a1
Proof state after:
no goals
Theorem: FOL.NV.T_21_2
Proof state before:
x y z : VarName
⊢ IsProof (forall_ x (forall_ y (forall_ z (((eq_ x y).and_ (eq_ y z)).imp_ (eq_ x z)))))
Tactic:
apply generalization
Proof state after:
case h1
x y z : VarName
⊢ IsDeduct ∅ (forall_ y (forall_ z (((eq_ x y).and_ (eq_ y z)).imp_ (eq_ x z))))

case h2
x y z : VarName
⊢ ∀ H ∈ ∅, ¬isFreeIn x H
Theorem: FOL.NV.T_21_2
Proof state before:
case h1
x y z : VarName
⊢ IsDeduct ∅ (forall_ y (forall_ z (((eq_ x y).and_ (eq_ y z)).imp_ (eq_ x z))))
Tactic:
apply generalization
Proof state after:
case h1.h1
x y z : VarName
⊢ IsDeduct ∅ (forall_ z (((eq_ x y).and_ (eq_ y z)).imp_ (eq_ x z)))

case h1.h2
x y z : VarName
⊢ ∀ H ∈ ∅, ¬isFreeIn y H
Theorem: FOL.NV.T_21_2
Proof state before:
case h1.h1
x y z : VarName
⊢ IsDeduct ∅ (forall_ z (((eq_ x y).and_ (eq_ y z)).imp_ (eq_ x z)))
Tactic:
apply generalization
Proof state after:
case h1.h1.h1
x y z : VarName
⊢ IsDeduct ∅ (((eq_ x y).and_ (eq_ y z)).imp_ (eq_ x z))

case h1.h1.h2
x y z : VarName
⊢ ∀ H ∈ ∅, ¬isFreeIn z H
Theorem: FOL.NV.T_21_2
Proof state before:
case h1.h1.h1
x y z : VarName
⊢ IsDeduct ∅ (((eq_ x y).and_ (eq_ y z)).imp_ (eq_ x z))
Tactic:
apply IsDeduct.mp_ (eq_ z z)
Proof state after:
case h1.h1.h1.a
x y z : VarName
⊢ IsDeduct ∅ ((eq_ z z).imp_ (((eq_ x y).and_ (eq_ y z)).imp_ (eq_ x z)))

case h1.h1.h1.a
x y z : VarName
⊢ IsDeduct ∅ (eq_ z z)
Theorem: FOL.NV.T_21_2
Proof state before:
case h1.h1.h1.a
x y z : VarName
⊢ IsDeduct ∅ ((eq_ z z).imp_ (((eq_ x y).and_ (eq_ y z)).imp_ (eq_ x z)))
Tactic:
apply IsDeduct.mp_ (((eq_ x y).and_ (eq_ z z)).imp_ ((eq_ x z).iff_ (eq_ y z)))
Proof state after:
case h1.h1.h1.a.a
x y z : VarName
⊢ IsDeduct ∅
    ((((eq_ x y).and_ (eq_ z z)).imp_ ((eq_ x z).iff_ (eq_ y z))).imp_
      ((eq_ z z).imp_ (((eq_ x y).and_ (eq_ y z)).imp_ (eq_ x z))))

case h1.h1.h1.a.a
x y z : VarName
⊢ IsDeduct ∅ (((eq_ x y).and_ (eq_ z z)).imp_ ((eq_ x z).iff_ (eq_ y z)))
Theorem: FOL.NV.T_21_2
Proof state before:
case h1.h1.h1.a.a
x y z : VarName
⊢ IsDeduct ∅
    ((((eq_ x y).and_ (eq_ z z)).imp_ ((eq_ x z).iff_ (eq_ y z))).imp_
      ((eq_ z z).imp_ (((eq_ x y).and_ (eq_ y z)).imp_ (eq_ x z))))
Tactic:
simp only [def_iff_]
Proof state after:
case h1.h1.h1.a.a
x y z : VarName
⊢ IsDeduct ∅
    ((((eq_ x y).and_ (eq_ z z)).imp_ (((eq_ x z).imp_ (eq_ y z)).and_ ((eq_ y z).imp_ (eq_ x z)))).imp_
      ((eq_ z z).imp_ (((eq_ x y).and_ (eq_ y z)).imp_ (eq_ x z))))
Theorem: FOL.NV.T_21_2
Proof state before:
case h1.h1.h1.a.a
x y z : VarName
⊢ IsDeduct ∅
    ((((eq_ x y).and_ (eq_ z z)).imp_ (((eq_ x z).imp_ (eq_ y z)).and_ ((eq_ y z).imp_ (eq_ x z)))).imp_
      ((eq_ z z).imp_ (((eq_ x y).and_ (eq_ y z)).imp_ (eq_ x z))))
Tactic:
simp only [def_and_]
Proof state after:
case h1.h1.h1.a.a
x y z : VarName
⊢ IsDeduct ∅
    ((((eq_ x y).imp_ (eq_ z z).not_).not_.imp_
          (((eq_ x z).imp_ (eq_ y z)).imp_ ((eq_ y z).imp_ (eq_ x z)).not_).not_).imp_
      ((eq_ z z).imp_ (((eq_ x y).imp_ (eq_ y z).not_).not_.imp_ (eq_ x z))))
Theorem: FOL.NV.T_21_2
Proof state before:
case h1.h1.h1.a.a
x y z : VarName
⊢ IsDeduct ∅
    ((((eq_ x y).imp_ (eq_ z z).not_).not_.imp_
          (((eq_ x z).imp_ (eq_ y z)).imp_ ((eq_ y z).imp_ (eq_ x z)).not_).not_).imp_
      ((eq_ z z).imp_ (((eq_ x y).imp_ (eq_ y z).not_).not_.imp_ (eq_ x z))))
Tactic:
SC
Proof state after:
no goals
Theorem: FOL.NV.T_21_2
Proof state before:
case h1.h1.h1.a.a
x y z : VarName
⊢ IsDeduct ∅ (((eq_ x y).and_ (eq_ z z)).imp_ ((eq_ x z).iff_ (eq_ y z)))
Tactic:
apply specId z
Proof state after:
case h1.h1.h1.a.a.h1
x y z : VarName
⊢ IsDeduct ∅ (forall_ z (((eq_ x y).and_ (eq_ z z)).imp_ ((eq_ x z).iff_ (eq_ y z))))
Theorem: FOL.NV.T_21_2
Proof state before:
case h1.h1.h1.a.a.h1
x y z : VarName
⊢ IsDeduct ∅ (forall_ z (((eq_ x y).and_ (eq_ z z)).imp_ ((eq_ x z).iff_ (eq_ y z))))
Tactic:
apply specId y
Proof state after:
case h1.h1.h1.a.a.h1.h1
x y z : VarName
⊢ IsDeduct ∅ (forall_ y (forall_ z (((eq_ x y).and_ (eq_ z z)).imp_ ((eq_ x z).iff_ (eq_ y z)))))
Theorem: FOL.NV.T_21_2
Proof state before:
case h1.h1.h1.a.a.h1.h1
x y z : VarName
⊢ IsDeduct ∅ (forall_ y (forall_ z (((eq_ x y).and_ (eq_ z z)).imp_ ((eq_ x z).iff_ (eq_ y z)))))
Tactic:
apply specId z
Proof state after:
case h1.h1.h1.a.a.h1.h1.h1
x y z : VarName
⊢ IsDeduct ∅ (forall_ z (forall_ y (forall_ z (((eq_ x y).and_ (eq_ z z)).imp_ ((eq_ x z).iff_ (eq_ y z))))))
Theorem: FOL.NV.T_21_2
Proof state before:
case h1.h1.h1.a.a.h1.h1.h1
x y z : VarName
⊢ IsDeduct ∅ (forall_ z (forall_ y (forall_ z (((eq_ x y).and_ (eq_ z z)).imp_ ((eq_ x z).iff_ (eq_ y z))))))
Tactic:
apply specId x
Proof state after:
case h1.h1.h1.a.a.h1.h1.h1.h1
x y z : VarName
⊢ IsDeduct ∅
    (forall_ x (forall_ z (forall_ y (forall_ z (((eq_ x y).and_ (eq_ z z)).imp_ ((eq_ x z).iff_ (eq_ y z)))))))
Theorem: FOL.NV.T_21_2
Proof state before:
case h1.h1.h1.a.a.h1.h1.h1.h1
x y z : VarName
⊢ IsDeduct ∅
    (forall_ x (forall_ z (forall_ y (forall_ z (((eq_ x y).and_ (eq_ z z)).imp_ ((eq_ x z).iff_ (eq_ y z)))))))
Tactic:
apply IsDeduct.axiom_
Proof state after:
case h1.h1.h1.a.a.h1.h1.h1.h1.a
x y z : VarName
⊢ IsAxiom (forall_ x (forall_ z (forall_ y (forall_ z (((eq_ x y).and_ (eq_ z z)).imp_ ((eq_ x z).iff_ (eq_ y z)))))))
Theorem: FOL.NV.T_21_2
Proof state before:
case h1.h1.h1.a.a.h1.h1.h1.h1.a
x y z : VarName
⊢ IsAxiom (forall_ x (forall_ z (forall_ y (forall_ z (((eq_ x y).and_ (eq_ z z)).imp_ ((eq_ x z).iff_ (eq_ y z)))))))
Tactic:
exact IsAxiom.eq_2_eq_ x z y z
Proof state after:
no goals
Theorem: FOL.NV.T_21_2
Proof state before:
case h1.h1.h1.a
x y z : VarName
⊢ IsDeduct ∅ (eq_ z z)
Tactic:
apply specId z
Proof state after:
case h1.h1.h1.a.h1
x y z : VarName
⊢ IsDeduct ∅ (forall_ z (eq_ z z))
Theorem: FOL.NV.T_21_2
Proof state before:
case h1.h1.h1.a.h1
x y z : VarName
⊢ IsDeduct ∅ (forall_ z (eq_ z z))
Tactic:
apply IsDeduct.axiom_
Proof state after:
case h1.h1.h1.a.h1.a
x y z : VarName
⊢ IsAxiom (forall_ z (eq_ z z))
Theorem: FOL.NV.T_21_2
Proof state before:
case h1.h1.h1.a.h1.a
x y z : VarName
⊢ IsAxiom (forall_ z (eq_ z z))
Tactic:
exact IsAxiom.eq_1_ z
Proof state after:
no goals
Theorem: FOL.NV.T_21_2
Proof state before:
case h1.h1.h2
x y z : VarName
⊢ ∀ H ∈ ∅, ¬isFreeIn z H
Tactic:
intro H a1
Proof state after:
case h1.h1.h2
x y z : VarName
H : Formula
a1 : H ∈ ∅
⊢ ¬isFreeIn z H
Theorem: FOL.NV.T_21_2
Proof state before:
case h1.h1.h2
x y z : VarName
H : Formula
a1 : H ∈ ∅
⊢ ¬isFreeIn z H
Tactic:
simp at a1
Proof state after:
no goals
Theorem: FOL.NV.T_21_2
Proof state before:
case h1.h2
x y z : VarName
⊢ ∀ H ∈ ∅, ¬isFreeIn y H
Tactic:
intro H a1
Proof state after:
case h1.h2
x y z : VarName
H : Formula
a1 : H ∈ ∅
⊢ ¬isFreeIn y H
Theorem: FOL.NV.T_21_2
Proof state before:
case h1.h2
x y z : VarName
H : Formula
a1 : H ∈ ∅
⊢ ¬isFreeIn y H
Tactic:
simp at a1
Proof state after:
no goals
Theorem: FOL.NV.T_21_2
Proof state before:
case h2
x y z : VarName
⊢ ∀ H ∈ ∅, ¬isFreeIn x H
Tactic:
intro H a1
Proof state after:
case h2
x y z : VarName
H : Formula
a1 : H ∈ ∅
⊢ ¬isFreeIn x H
Theorem: FOL.NV.T_21_2
Proof state before:
case h2
x y z : VarName
H : Formula
a1 : H ∈ ∅
⊢ ¬isFreeIn x H
Tactic:
simp at a1
Proof state after:
no goals
Theorem: FOL.NV.T_21_8
Proof state before:
P_r P_s : Formula
r s : VarName
h2 : ¬isBoundIn r true_
h3 : ¬isBoundIn s true_
⊢ IsProof ((eq_ r s).imp_ (true_.iff_ true_))
Tactic:
case true_ =>
  simp only [def_iff_]
  simp only [def_and_]
  SC
Proof state after:
no goals