internlm/Lean-Github huggingface dataset:
Theorem: FOL.NV.T_19_4
Proof state before:
case h1.h2
P : Formula
u v : VarName
⊢ ¬isFreeIn v (forall_ u (forall_ v P).not_).not_
Tactic:
simp only [isFreeIn]
Proof state after:
case h1.h2
P : Formula
u v : VarName
⊢ ¬(¬v = u ∧ ¬True ∧ isFreeIn v P)
Theorem: FOL.NV.T_19_4
Proof state before:
case h1.h2
P : Formula
u v : VarName
⊢ ¬(¬v = u ∧ ¬True ∧ isFreeIn v P)
Tactic:
simp
Proof state after:
no goals
Theorem: FOL.NV.T_19_5
Proof state before:
P Q : Formula
v : VarName
h1 : ¬isFreeIn v P
⊢ IsProof ((forall_ v (P.iff_ Q)).imp_ (P.iff_ (forall_ v Q)))
Tactic:
apply IsDeduct.mp_ ((forall_ v P).iff_ P)
Proof state after:
case a
P Q : Formula
v : VarName
h1 : ¬isFreeIn v P
⊢ IsDeduct ∅ (((forall_ v P).iff_ P).imp_ ((forall_ v (P.iff_ Q)).imp_ (P.iff_ (forall_ v Q))))

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

case a.a
P Q : Formula
v : VarName
h1 : ¬isFreeIn v P
⊢ IsDeduct ∅ ((forall_ v (P.iff_ Q)).imp_ ((forall_ v P).iff_ (forall_ v Q)))
Theorem: FOL.NV.T_19_5
Proof state before:
case a.a
P Q : Formula
v : VarName
h1 : ¬isFreeIn v P
⊢ IsDeduct ∅
    (((forall_ v (P.iff_ Q)).imp_ ((forall_ v P).iff_ (forall_ v Q))).imp_
      (((forall_ v P).iff_ P).imp_ ((forall_ v (P.iff_ Q)).imp_ (P.iff_ (forall_ v Q)))))
Tactic:
simp only [def_iff_]
Proof state after:
case a.a
P Q : Formula
v : VarName
h1 : ¬isFreeIn v P
⊢ IsDeduct ∅
    (((forall_ v ((P.imp_ Q).and_ (Q.imp_ P))).imp_
          (((forall_ v P).imp_ (forall_ v Q)).and_ ((forall_ v Q).imp_ (forall_ v P)))).imp_
      ((((forall_ v P).imp_ P).and_ (P.imp_ (forall_ v P))).imp_
        ((forall_ v ((P.imp_ Q).and_ (Q.imp_ P))).imp_ ((P.imp_ (forall_ v Q)).and_ ((forall_ v Q).imp_ P)))))
Theorem: FOL.NV.T_19_5
Proof state before:
case a.a
P Q : Formula
v : VarName
h1 : ¬isFreeIn v P
⊢ IsDeduct ∅
    (((forall_ v ((P.imp_ Q).and_ (Q.imp_ P))).imp_
          (((forall_ v P).imp_ (forall_ v Q)).and_ ((forall_ v Q).imp_ (forall_ v P)))).imp_
      ((((forall_ v P).imp_ P).and_ (P.imp_ (forall_ v P))).imp_
        ((forall_ v ((P.imp_ Q).and_ (Q.imp_ P))).imp_ ((P.imp_ (forall_ v Q)).and_ ((forall_ v Q).imp_ P)))))
Tactic:
simp only [def_and_]
Proof state after:
case a.a
P Q : Formula
v : VarName
h1 : ¬isFreeIn v P
⊢ IsDeduct ∅
    (((forall_ v ((P.imp_ Q).imp_ (Q.imp_ P).not_).not_).imp_
          (((forall_ v P).imp_ (forall_ v Q)).imp_ ((forall_ v Q).imp_ (forall_ v P)).not_).not_).imp_
      ((((forall_ v P).imp_ P).imp_ (P.imp_ (forall_ v P)).not_).not_.imp_
        ((forall_ v ((P.imp_ Q).imp_ (Q.imp_ P).not_).not_).imp_
          ((P.imp_ (forall_ v Q)).imp_ ((forall_ v Q).imp_ P).not_).not_)))
Theorem: FOL.NV.T_19_5
Proof state before:
case a.a
P Q : Formula
v : VarName
h1 : ¬isFreeIn v P
⊢ IsDeduct ∅
    (((forall_ v ((P.imp_ Q).imp_ (Q.imp_ P).not_).not_).imp_
          (((forall_ v P).imp_ (forall_ v Q)).imp_ ((forall_ v Q).imp_ (forall_ v P)).not_).not_).imp_
      ((((forall_ v P).imp_ P).imp_ (P.imp_ (forall_ v P)).not_).not_.imp_
        ((forall_ v ((P.imp_ Q).imp_ (Q.imp_ P).not_).not_).imp_
          ((P.imp_ (forall_ v Q)).imp_ ((forall_ v Q).imp_ P).not_).not_)))
Tactic:
SC
Proof state after:
no goals
Theorem: FOL.NV.T_19_5
Proof state before:
case a.a
P Q : Formula
v : VarName
h1 : ¬isFreeIn v P
⊢ IsDeduct ∅ ((forall_ v (P.iff_ Q)).imp_ ((forall_ v P).iff_ (forall_ v Q)))
Tactic:
exact T_18_1 P Q v
Proof state after:
no goals
Theorem: FOL.NV.T_19_5
Proof state before:
case a
P Q : Formula
v : VarName
h1 : ¬isFreeIn v P
⊢ IsDeduct ∅ ((forall_ v P).iff_ P)
Tactic:
exact T_19_1 P v h1
Proof state after:
no goals
Theorem: FOL.NV.T_19_6_left
Proof state before:
P Q : Formula
v : VarName
⊢ IsProof ((forall_ v (P.iff_ Q)).imp_ ((exists_ v P).imp_ (exists_ v Q)))
Tactic:
apply deduction_theorem
Proof state after:
case h1
P Q : Formula
v : VarName
⊢ IsDeduct (∅ ∪ {forall_ v (P.iff_ Q)}) ((exists_ v P).imp_ (exists_ v Q))
Theorem: FOL.NV.T_19_6_left
Proof state before:
case h1
P Q : Formula
v : VarName
⊢ IsDeduct (∅ ∪ {forall_ v (P.iff_ Q)}) ((exists_ v P).imp_ (exists_ v Q))
Tactic:
apply deduction_theorem
Proof state after:
case h1.h1
P Q : Formula
v : VarName
⊢ IsDeduct (∅ ∪ {forall_ v (P.iff_ Q)} ∪ {exists_ v P}) (exists_ v Q)
Theorem: FOL.NV.T_19_6_left
Proof state before:
case h1.h1
P Q : Formula
v : VarName
⊢ IsDeduct (∅ ∪ {forall_ v (P.iff_ Q)} ∪ {exists_ v P}) (exists_ v Q)
Tactic:
simp
Proof state after:
case h1.h1
P Q : Formula
v : VarName
⊢ IsDeduct {exists_ v P, forall_ v (P.iff_ Q)} (exists_ v Q)
Theorem: FOL.NV.T_19_6_left
Proof state before:
case h1.h1
P Q : Formula
v : VarName
⊢ IsDeduct {exists_ v P, forall_ v (P.iff_ Q)} (exists_ v Q)
Tactic:
apply rule_C P (exists_ v Q) v {exists_ v P, forall_ v (P.iff_ Q)}
Proof state after:
case h1.h1.h1
P Q : Formula
v : VarName
⊢ IsDeduct {exists_ v P, forall_ v (P.iff_ Q)} (exists_ v P)

case h1.h1.h2
P Q : Formula
v : VarName
⊢ IsDeduct ({exists_ v P, forall_ v (P.iff_ Q)} ∪ {P}) (exists_ v Q)

case h1.h1.h3
P Q : Formula
v : VarName
⊢ ∀ H ∈ {exists_ v P, forall_ v (P.iff_ Q)}, ¬isFreeIn v H

case h1.h1.h4
P Q : Formula
v : VarName
⊢ ¬isFreeIn v (exists_ v Q)
Theorem: FOL.NV.T_19_6_left
Proof state before:
case h1.h1.h1
P Q : Formula
v : VarName
⊢ IsDeduct {exists_ v P, forall_ v (P.iff_ Q)} (exists_ v P)
Tactic:
apply IsDeduct.assume_
Proof state after:
case h1.h1.h1.a
P Q : Formula
v : VarName
⊢ exists_ v P ∈ {exists_ v P, forall_ v (P.iff_ Q)}
Theorem: FOL.NV.T_19_6_left
Proof state before:
case h1.h1.h1.a
P Q : Formula
v : VarName
⊢ exists_ v P ∈ {exists_ v P, forall_ v (P.iff_ Q)}
Tactic:
simp
Proof state after:
no goals
Theorem: FOL.NV.T_19_6_left
Proof state before:
case h1.h1.h2
P Q : Formula
v : VarName
⊢ IsDeduct ({exists_ v P, forall_ v (P.iff_ Q)} ∪ {P}) (exists_ v Q)
Tactic:
apply exists_intro Q v v
Proof state after:
case h1.h1.h2.h1
P Q : Formula
v : VarName
⊢ fastAdmits v v Q

case h1.h1.h2.h2
P Q : Formula
v : VarName
⊢ IsDeduct ({exists_ v P, forall_ v (P.iff_ Q)} ∪ {P}) (fastReplaceFree v v Q)
Theorem: FOL.NV.T_19_6_left
Proof state before:
case h1.h1.h2.h1
P Q : Formula
v : VarName
⊢ fastAdmits v v Q
Tactic:
apply fastAdmits_self
Proof state after:
no goals
Theorem: FOL.NV.T_19_6_left
Proof state before:
case h1.h1.h2.h2
P Q : Formula
v : VarName
⊢ IsDeduct ({exists_ v P, forall_ v (P.iff_ Q)} ∪ {P}) (fastReplaceFree v v Q)
Tactic:
simp only [fastReplaceFree_self]
Proof state after:
case h1.h1.h2.h2
P Q : Formula
v : VarName
⊢ IsDeduct ({exists_ v P, forall_ v (P.iff_ Q)} ∪ {P}) Q
Theorem: FOL.NV.T_19_6_left
Proof state before:
case h1.h1.h2.h2
P Q : Formula
v : VarName
⊢ IsDeduct ({exists_ v P, forall_ v (P.iff_ Q)} ∪ {P}) Q
Tactic:
apply IsDeduct.mp_ P
Proof state after:
case h1.h1.h2.h2.a
P Q : Formula
v : VarName
⊢ IsDeduct ({exists_ v P, forall_ v (P.iff_ Q)} ∪ {P}) (P.imp_ Q)

case h1.h1.h2.h2.a
P Q : Formula
v : VarName
⊢ IsDeduct ({exists_ v P, forall_ v (P.iff_ Q)} ∪ {P}) P
Theorem: FOL.NV.T_19_6_left
Proof state before:
case h1.h1.h2.h2.a
P Q : Formula
v : VarName
⊢ IsDeduct ({exists_ v P, forall_ v (P.iff_ Q)} ∪ {P}) (P.imp_ Q)
Tactic:
apply IsDeduct.mp_ (P.iff_ Q)
Proof state after:
case h1.h1.h2.h2.a.a
P Q : Formula
v : VarName
⊢ IsDeduct ({exists_ v P, forall_ v (P.iff_ Q)} ∪ {P}) ((P.iff_ Q).imp_ (P.imp_ Q))

case h1.h1.h2.h2.a.a
P Q : Formula
v : VarName
⊢ IsDeduct ({exists_ v P, forall_ v (P.iff_ Q)} ∪ {P}) (P.iff_ Q)
Theorem: FOL.NV.T_19_6_left
Proof state before:
case h1.h1.h2.h2.a.a
P Q : Formula
v : VarName
⊢ IsDeduct ({exists_ v P, forall_ v (P.iff_ Q)} ∪ {P}) ((P.iff_ Q).imp_ (P.imp_ Q))
Tactic:
simp only [def_iff_]
Proof state after:
case h1.h1.h2.h2.a.a
P Q : Formula
v : VarName
⊢ IsDeduct ({exists_ v P, forall_ v ((P.imp_ Q).and_ (Q.imp_ P))} ∪ {P}) (((P.imp_ Q).and_ (Q.imp_ P)).imp_ (P.imp_ Q))
Theorem: FOL.NV.T_19_6_left
Proof state before:
case h1.h1.h2.h2.a.a
P Q : Formula
v : VarName
⊢ IsDeduct ({exists_ v P, forall_ v ((P.imp_ Q).and_ (Q.imp_ P))} ∪ {P}) (((P.imp_ Q).and_ (Q.imp_ P)).imp_ (P.imp_ Q))
Tactic:
simp only [def_and_]
Proof state after:
case h1.h1.h2.h2.a.a
P Q : Formula
v : VarName
⊢ IsDeduct ({exists_ v P, forall_ v ((P.imp_ Q).imp_ (Q.imp_ P).not_).not_} ∪ {P})
    (((P.imp_ Q).imp_ (Q.imp_ P).not_).not_.imp_ (P.imp_ Q))
Theorem: FOL.NV.T_19_6_left
Proof state before:
case h1.h1.h2.h2.a.a
P Q : Formula
v : VarName
⊢ IsDeduct ({exists_ v P, forall_ v ((P.imp_ Q).imp_ (Q.imp_ P).not_).not_} ∪ {P})
    (((P.imp_ Q).imp_ (Q.imp_ P).not_).not_.imp_ (P.imp_ Q))
Tactic:
SC
Proof state after:
no goals
Theorem: FOL.NV.T_19_6_left
Proof state before:
case h1.h1.h2.h2.a.a
P Q : Formula
v : VarName
⊢ IsDeduct ({exists_ v P, forall_ v (P.iff_ Q)} ∪ {P}) (P.iff_ Q)
Tactic:
apply specId v
Proof state after:
case h1.h1.h2.h2.a.a.h1
P Q : Formula
v : VarName
⊢ IsDeduct ({exists_ v P, forall_ v (P.iff_ Q)} ∪ {P}) (forall_ v (P.iff_ Q))
Theorem: FOL.NV.T_19_6_left
Proof state before:
case h1.h1.h2.h2.a.a.h1
P Q : Formula
v : VarName
⊢ IsDeduct ({exists_ v P, forall_ v (P.iff_ Q)} ∪ {P}) (forall_ v (P.iff_ Q))
Tactic:
apply IsDeduct.assume_
Proof state after:
case h1.h1.h2.h2.a.a.h1.a
P Q : Formula
v : VarName
⊢ forall_ v (P.iff_ Q) ∈ {exists_ v P, forall_ v (P.iff_ Q)} ∪ {P}
Theorem: FOL.NV.T_19_6_left
Proof state before:
case h1.h1.h2.h2.a.a.h1.a
P Q : Formula
v : VarName
⊢ forall_ v (P.iff_ Q) ∈ {exists_ v P, forall_ v (P.iff_ Q)} ∪ {P}
Tactic:
simp
Proof state after:
no goals
Theorem: FOL.NV.T_19_6_left
Proof state before:
case h1.h1.h2.h2.a
P Q : Formula
v : VarName
⊢ IsDeduct ({exists_ v P, forall_ v (P.iff_ Q)} ∪ {P}) P
Tactic:
apply IsDeduct.assume_
Proof state after:
case h1.h1.h2.h2.a.a
P Q : Formula
v : VarName
⊢ P ∈ {exists_ v P, forall_ v (P.iff_ Q)} ∪ {P}
Theorem: FOL.NV.T_19_6_left
Proof state before:
case h1.h1.h2.h2.a.a
P Q : Formula
v : VarName
⊢ P ∈ {exists_ v P, forall_ v (P.iff_ Q)} ∪ {P}
Tactic:
simp
Proof state after:
no goals
Theorem: FOL.NV.T_19_6_left
Proof state before:
case h1.h1.h3
P Q : Formula
v : VarName
⊢ ∀ H ∈ {exists_ v P, forall_ v (P.iff_ Q)}, ¬isFreeIn v H
Tactic:
simp only [def_exists_]
Proof state after:
case h1.h1.h3
P Q : Formula
v : VarName
⊢ ∀ H ∈ {(forall_ v P.not_).not_, forall_ v (P.iff_ Q)}, ¬isFreeIn v H
Theorem: FOL.NV.T_19_6_left
Proof state before:
case h1.h1.h3
P Q : Formula
v : VarName
⊢ ∀ H ∈ {(forall_ v P.not_).not_, forall_ v (P.iff_ Q)}, ¬isFreeIn v H
Tactic:
simp
Proof state after:
case h1.h1.h3
P Q : Formula
v : VarName
⊢ ¬isFreeIn v (forall_ v P.not_).not_ ∧ ¬isFreeIn v (forall_ v (P.iff_ Q))
Theorem: FOL.NV.T_19_6_left
Proof state before:
case h1.h1.h3
P Q : Formula
v : VarName
⊢ ¬isFreeIn v (forall_ v P.not_).not_ ∧ ¬isFreeIn v (forall_ v (P.iff_ Q))
Tactic:
simp only [isFreeIn]
Proof state after:
case h1.h1.h3
P Q : Formula
v : VarName
⊢ ¬(¬True ∧ isFreeIn v P) ∧ ¬(¬True ∧ (isFreeIn v P ∨ isFreeIn v Q))
Theorem: FOL.NV.T_19_6_left
Proof state before:
case h1.h1.h3
P Q : Formula
v : VarName
⊢ ¬(¬True ∧ isFreeIn v P) ∧ ¬(¬True ∧ (isFreeIn v P ∨ isFreeIn v Q))
Tactic:
simp
Proof state after:
no goals
Theorem: FOL.NV.T_19_6_left
Proof state before:
case h1.h1.h4
P Q : Formula
v : VarName
⊢ ¬isFreeIn v (exists_ v Q)
Tactic:
simp only [def_exists_]
Proof state after:
case h1.h1.h4
P Q : Formula
v : VarName
⊢ ¬isFreeIn v (forall_ v Q.not_).not_
Theorem: FOL.NV.T_19_6_left
Proof state before:
case h1.h1.h4
P Q : Formula
v : VarName
⊢ ¬isFreeIn v (forall_ v Q.not_).not_
Tactic:
simp only [isFreeIn]
Proof state after:
case h1.h1.h4
P Q : Formula
v : VarName
⊢ ¬(¬True ∧ isFreeIn v Q)
Theorem: FOL.NV.T_19_6_left
Proof state before:
case h1.h1.h4
P Q : Formula
v : VarName
⊢ ¬(¬True ∧ isFreeIn v Q)
Tactic:
simp
Proof state after:
no goals
Theorem: FOL.NV.T_19_6_right
Proof state before:
P Q : Formula
v : VarName
⊢ IsProof ((forall_ v (P.iff_ Q)).imp_ ((exists_ v Q).imp_ (exists_ v P)))
Tactic:
apply deduction_theorem
Proof state after:
case h1
P Q : Formula
v : VarName
⊢ IsDeduct (∅ ∪ {forall_ v (P.iff_ Q)}) ((exists_ v Q).imp_ (exists_ v P))
Theorem: FOL.NV.T_19_6_right
Proof state before:
case h1
P Q : Formula
v : VarName
⊢ IsDeduct (∅ ∪ {forall_ v (P.iff_ Q)}) ((exists_ v Q).imp_ (exists_ v P))
Tactic:
simp
Proof state after:
case h1
P Q : Formula
v : VarName
⊢ IsDeduct {forall_ v (P.iff_ Q)} ((exists_ v Q).imp_ (exists_ v P))
Theorem: FOL.NV.T_19_6_right
Proof state before:
case h1
P Q : Formula
v : VarName
⊢ IsDeduct {forall_ v (P.iff_ Q)} ((exists_ v Q).imp_ (exists_ v P))
Tactic:
apply IsDeduct.mp_ (forall_ v (Q.iff_ P))
Proof state after:
case h1.a
P Q : Formula
v : VarName
⊢ IsDeduct {forall_ v (P.iff_ Q)} ((forall_ v (Q.iff_ P)).imp_ ((exists_ v Q).imp_ (exists_ v P)))

case h1.a
P Q : Formula
v : VarName
⊢ IsDeduct {forall_ v (P.iff_ Q)} (forall_ v (Q.iff_ P))
Theorem: FOL.NV.T_19_6_right
Proof state before:
case h1.a
P Q : Formula
v : VarName
⊢ IsDeduct {forall_ v (P.iff_ Q)} ((forall_ v (Q.iff_ P)).imp_ ((exists_ v Q).imp_ (exists_ v P)))
Tactic:
apply proof_imp_deduct
Proof state after:
case h1.a.h1
P Q : Formula
v : VarName
⊢ IsProof ((forall_ v (Q.iff_ P)).imp_ ((exists_ v Q).imp_ (exists_ v P)))
Theorem: FOL.NV.T_19_6_right
Proof state before:
case h1.a.h1
P Q : Formula
v : VarName
⊢ IsProof ((forall_ v (Q.iff_ P)).imp_ ((exists_ v Q).imp_ (exists_ v P)))
Tactic:
apply T_19_6_left Q P v
Proof state after:
no goals
Theorem: FOL.NV.T_19_6_right
Proof state before:
case h1.a
P Q : Formula
v : VarName
⊢ IsDeduct {forall_ v (P.iff_ Q)} (forall_ v (Q.iff_ P))
Tactic:
apply generalization
Proof state after:
case h1.a.h1
P Q : Formula
v : VarName
⊢ IsDeduct {forall_ v (P.iff_ Q)} (Q.iff_ P)

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

case h1.a.h1.a
P Q : Formula
v : VarName
⊢ IsDeduct {forall_ v (P.iff_ Q)} (P.iff_ Q)
Theorem: FOL.NV.T_19_6_right
Proof state before:
case h1.a.h1.a
P Q : Formula
v : VarName
⊢ IsDeduct {forall_ v (P.iff_ Q)} ((P.iff_ Q).imp_ (Q.iff_ P))
Tactic:
simp only [def_iff_]
Proof state after:
case h1.a.h1.a
P Q : Formula
v : VarName
⊢ IsDeduct {forall_ v ((P.imp_ Q).and_ (Q.imp_ P))} (((P.imp_ Q).and_ (Q.imp_ P)).imp_ ((Q.imp_ P).and_ (P.imp_ Q)))
Theorem: FOL.NV.T_19_6_right
Proof state before:
case h1.a.h1.a
P Q : Formula
v : VarName
⊢ IsDeduct {forall_ v ((P.imp_ Q).and_ (Q.imp_ P))} (((P.imp_ Q).and_ (Q.imp_ P)).imp_ ((Q.imp_ P).and_ (P.imp_ Q)))
Tactic:
simp only [def_and_]
Proof state after:
case h1.a.h1.a
P Q : Formula
v : VarName
⊢ IsDeduct {forall_ v ((P.imp_ Q).imp_ (Q.imp_ P).not_).not_}
    (((P.imp_ Q).imp_ (Q.imp_ P).not_).not_.imp_ ((Q.imp_ P).imp_ (P.imp_ Q).not_).not_)
Theorem: FOL.NV.T_19_6_right
Proof state before:
case h1.a.h1.a
P Q : Formula
v : VarName
⊢ IsDeduct {forall_ v ((P.imp_ Q).imp_ (Q.imp_ P).not_).not_}
    (((P.imp_ Q).imp_ (Q.imp_ P).not_).not_.imp_ ((Q.imp_ P).imp_ (P.imp_ Q).not_).not_)
Tactic:
SC
Proof state after:
no goals
Theorem: FOL.NV.T_19_6_right
Proof state before:
case h1.a.h1.a
P Q : Formula
v : VarName
⊢ IsDeduct {forall_ v (P.iff_ Q)} (P.iff_ Q)
Tactic:
apply specId v
Proof state after:
case h1.a.h1.a.h1
P Q : Formula
v : VarName
⊢ IsDeduct {forall_ v (P.iff_ Q)} (forall_ v (P.iff_ Q))
Theorem: FOL.NV.T_19_6_right
Proof state before:
case h1.a.h1.a.h1
P Q : Formula
v : VarName
⊢ IsDeduct {forall_ v (P.iff_ Q)} (forall_ v (P.iff_ Q))
Tactic:
apply IsDeduct.assume_
Proof state after:
case h1.a.h1.a.h1.a
P Q : Formula
v : VarName
⊢ forall_ v (P.iff_ Q) ∈ {forall_ v (P.iff_ Q)}
Theorem: FOL.NV.T_19_6_right
Proof state before:
case h1.a.h1.a.h1.a
P Q : Formula
v : VarName
⊢ forall_ v (P.iff_ Q) ∈ {forall_ v (P.iff_ Q)}
Tactic:
simp
Proof state after:
no goals
Theorem: FOL.NV.T_19_6_right
Proof state before:
case h1.a.h2
P Q : Formula
v : VarName
⊢ ∀ H ∈ {forall_ v (P.iff_ Q)}, ¬isFreeIn v H
Tactic:
simp
Proof state after:
case h1.a.h2
P Q : Formula
v : VarName
⊢ ¬isFreeIn v (forall_ v (P.iff_ Q))
Theorem: FOL.NV.T_19_6_right
Proof state before:
case h1.a.h2
P Q : Formula
v : VarName
⊢ ¬isFreeIn v (forall_ v (P.iff_ Q))
Tactic:
simp only [isFreeIn]
Proof state after:
case h1.a.h2
P Q : Formula
v : VarName
⊢ ¬(¬True ∧ (isFreeIn v P ∨ isFreeIn v Q))
Theorem: FOL.NV.T_19_6_right
Proof state before:
case h1.a.h2
P Q : Formula
v : VarName
⊢ ¬(¬True ∧ (isFreeIn v P ∨ isFreeIn v Q))
Tactic:
simp
Proof state after:
no goals
Theorem: FOL.NV.T_19_6
Proof state before:
P Q : Formula
v : VarName
⊢ IsProof ((forall_ v (P.iff_ Q)).imp_ ((exists_ v P).iff_ (exists_ v Q)))
Tactic:
apply IsDeduct.mp_ ((forall_ v (P.iff_ Q)).imp_ ((exists_ v P).imp_ (exists_ v Q)))
Proof state after:
case a
P Q : Formula
v : VarName
⊢ IsDeduct ∅
    (((forall_ v (P.iff_ Q)).imp_ ((exists_ v P).imp_ (exists_ v Q))).imp_
      ((forall_ v (P.iff_ Q)).imp_ ((exists_ v P).iff_ (exists_ v Q))))

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

case a.a
P Q : Formula
v : VarName
⊢ IsDeduct ∅ ((forall_ v (P.iff_ Q)).imp_ ((exists_ v Q).imp_ (exists_ v P)))
Theorem: FOL.NV.T_19_6
Proof state before:
case a.a
P Q : Formula
v : VarName
⊢ IsDeduct ∅
    (((forall_ v (P.iff_ Q)).imp_ ((exists_ v Q).imp_ (exists_ v P))).imp_
      (((forall_ v (P.iff_ Q)).imp_ ((exists_ v P).imp_ (exists_ v Q))).imp_
        ((forall_ v (P.iff_ Q)).imp_ ((exists_ v P).iff_ (exists_ v Q)))))
Tactic:
simp only [def_exists_]
Proof state after:
case a.a
P Q : Formula
v : VarName
⊢ IsDeduct ∅
    (((forall_ v (P.iff_ Q)).imp_ ((forall_ v Q.not_).not_.imp_ (forall_ v P.not_).not_)).imp_
      (((forall_ v (P.iff_ Q)).imp_ ((forall_ v P.not_).not_.imp_ (forall_ v Q.not_).not_)).imp_
        ((forall_ v (P.iff_ Q)).imp_ ((forall_ v P.not_).not_.iff_ (forall_ v Q.not_).not_))))
Theorem: FOL.NV.T_19_6
Proof state before:
case a.a
P Q : Formula
v : VarName
⊢ IsDeduct ∅
    (((forall_ v (P.iff_ Q)).imp_ ((forall_ v Q.not_).not_.imp_ (forall_ v P.not_).not_)).imp_
      (((forall_ v (P.iff_ Q)).imp_ ((forall_ v P.not_).not_.imp_ (forall_ v Q.not_).not_)).imp_
        ((forall_ v (P.iff_ Q)).imp_ ((forall_ v P.not_).not_.iff_ (forall_ v Q.not_).not_))))
Tactic:
simp only [def_iff_]
Proof state after:
case a.a
P Q : Formula
v : VarName
⊢ IsDeduct ∅
    (((forall_ v ((P.imp_ Q).and_ (Q.imp_ P))).imp_ ((forall_ v Q.not_).not_.imp_ (forall_ v P.not_).not_)).imp_
      (((forall_ v ((P.imp_ Q).and_ (Q.imp_ P))).imp_ ((forall_ v P.not_).not_.imp_ (forall_ v Q.not_).not_)).imp_
        ((forall_ v ((P.imp_ Q).and_ (Q.imp_ P))).imp_
          (((forall_ v P.not_).not_.imp_ (forall_ v Q.not_).not_).and_
            ((forall_ v Q.not_).not_.imp_ (forall_ v P.not_).not_)))))
Theorem: FOL.NV.T_19_6
Proof state before:
case a.a
P Q : Formula
v : VarName
⊢ IsDeduct ∅
    (((forall_ v ((P.imp_ Q).and_ (Q.imp_ P))).imp_ ((forall_ v Q.not_).not_.imp_ (forall_ v P.not_).not_)).imp_
      (((forall_ v ((P.imp_ Q).and_ (Q.imp_ P))).imp_ ((forall_ v P.not_).not_.imp_ (forall_ v Q.not_).not_)).imp_
        ((forall_ v ((P.imp_ Q).and_ (Q.imp_ P))).imp_
          (((forall_ v P.not_).not_.imp_ (forall_ v Q.not_).not_).and_
            ((forall_ v Q.not_).not_.imp_ (forall_ v P.not_).not_)))))
Tactic:
simp only [def_and_]
Proof state after:
case a.a
P Q : Formula
v : VarName
⊢ IsDeduct ∅
    (((forall_ v ((P.imp_ Q).imp_ (Q.imp_ P).not_).not_).imp_
          ((forall_ v Q.not_).not_.imp_ (forall_ v P.not_).not_)).imp_
      (((forall_ v ((P.imp_ Q).imp_ (Q.imp_ P).not_).not_).imp_
            ((forall_ v P.not_).not_.imp_ (forall_ v Q.not_).not_)).imp_
        ((forall_ v ((P.imp_ Q).imp_ (Q.imp_ P).not_).not_).imp_
          (((forall_ v P.not_).not_.imp_ (forall_ v Q.not_).not_).imp_
              ((forall_ v Q.not_).not_.imp_ (forall_ v P.not_).not_).not_).not_)))
Theorem: FOL.NV.T_19_6
Proof state before:
case a.a
P Q : Formula
v : VarName
⊢ IsDeduct ∅
    (((forall_ v ((P.imp_ Q).imp_ (Q.imp_ P).not_).not_).imp_
          ((forall_ v Q.not_).not_.imp_ (forall_ v P.not_).not_)).imp_
      (((forall_ v ((P.imp_ Q).imp_ (Q.imp_ P).not_).not_).imp_
            ((forall_ v P.not_).not_.imp_ (forall_ v Q.not_).not_)).imp_
        ((forall_ v ((P.imp_ Q).imp_ (Q.imp_ P).not_).not_).imp_
          (((forall_ v P.not_).not_.imp_ (forall_ v Q.not_).not_).imp_
              ((forall_ v Q.not_).not_.imp_ (forall_ v P.not_).not_).not_).not_)))
Tactic:
SC
Proof state after:
no goals
Theorem: FOL.NV.T_19_6
Proof state before:
case a.a
P Q : Formula
v : VarName
⊢ IsDeduct ∅ ((forall_ v (P.iff_ Q)).imp_ ((exists_ v Q).imp_ (exists_ v P)))
Tactic:
apply T_19_6_right
Proof state after:
no goals
Theorem: FOL.NV.T_19_6
Proof state before:
case a
P Q : Formula
v : VarName
⊢ IsDeduct ∅ ((forall_ v (P.iff_ Q)).imp_ ((exists_ v P).imp_ (exists_ v Q)))
Tactic:
apply T_19_6_left
Proof state after:
no goals
Theorem: FOL.NV.T_19_TS_21_left
Proof state before:
P Q : Formula
v : VarName
h1 : ¬isFreeIn v P
⊢ IsProof ((forall_ v (P.imp_ Q)).imp_ (P.imp_ (forall_ v Q)))
Tactic:
apply C_18_4 (forall_ v P) P ((forall_ v (P.imp_ Q)).imp_ ((forall_ v P).imp_ (forall_ v Q)))
Proof state after:
case h1
P Q : Formula
v : VarName
h1 : ¬isFreeIn v P
⊢ IsReplOfFormulaInFormula (forall_ v P) P ((forall_ v (P.imp_ Q)).imp_ ((forall_ v P).imp_ (forall_ v Q)))
    ((forall_ v (P.imp_ Q)).imp_ (P.imp_ (forall_ v Q)))

case h2
P Q : Formula
v : VarName
h1 : ¬isFreeIn v P
⊢ IsProof ((forall_ v P).iff_ P)

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)))
Theorem: FOL.NV.T_19_TS_21_left
Proof state before:
case h1
P Q : Formula
v : VarName
h1 : ¬isFreeIn v P
⊢ IsReplOfFormulaInFormula (forall_ v P) P ((forall_ v (P.imp_ Q)).imp_ ((forall_ v P).imp_ (forall_ v Q)))
    ((forall_ v (P.imp_ Q)).imp_ (P.imp_ (forall_ v Q)))
Tactic:
apply IsReplOfFormulaInFormula.imp_
Proof state after:
case h1.a
P Q : Formula
v : VarName
h1 : ¬isFreeIn v P
⊢ IsReplOfFormulaInFormula (forall_ v P) P (forall_ v (P.imp_ Q)) (forall_ v (P.imp_ Q))

case h1.a
P Q : Formula
v : VarName
h1 : ¬isFreeIn v P
⊢ IsReplOfFormulaInFormula (forall_ v P) P ((forall_ v P).imp_ (forall_ v Q)) (P.imp_ (forall_ v Q))
Theorem: FOL.NV.T_19_TS_21_left
Proof state before:
case h1.a
P Q : Formula
v : VarName
h1 : ¬isFreeIn v P
⊢ IsReplOfFormulaInFormula (forall_ v P) P (forall_ v (P.imp_ Q)) (forall_ v (P.imp_ Q))
Tactic:
apply IsReplOfFormulaInFormula.same_
Proof state after:
case h1.a.a
P Q : Formula
v : VarName
h1 : ¬isFreeIn v P
⊢ forall_ v (P.imp_ Q) = forall_ v (P.imp_ Q)
Theorem: FOL.NV.T_19_TS_21_left
Proof state before:
case h1.a.a
P Q : Formula
v : VarName
h1 : ¬isFreeIn v P
⊢ forall_ v (P.imp_ Q) = forall_ v (P.imp_ Q)
Tactic:
rfl
Proof state after:
no goals
Theorem: FOL.NV.T_19_TS_21_left
Proof state before:
case h1.a
P Q : Formula
v : VarName
h1 : ¬isFreeIn v P
⊢ IsReplOfFormulaInFormula (forall_ v P) P ((forall_ v P).imp_ (forall_ v Q)) (P.imp_ (forall_ v Q))
Tactic:
apply IsReplOfFormulaInFormula.imp_
Proof state after:
case h1.a.a
P Q : Formula
v : VarName
h1 : ¬isFreeIn v P
⊢ IsReplOfFormulaInFormula (forall_ v P) P (forall_ v P) P

case h1.a.a
P Q : Formula
v : VarName
h1 : ¬isFreeIn v P
⊢ IsReplOfFormulaInFormula (forall_ v P) P (forall_ v Q) (forall_ v Q)