internlm/Lean-Github huggingface dataset:
Theorem: FOL.NV.existsElim
Proof state before:
P Q : Formula
v t : VarName
Δ : Set Formula
h2 : IsDeduct (Δ ∪ {fastReplaceFree v t P}) Q
h3 : ¬occursIn t P
h4 : ¬occursIn t Q
h5 : ∀ H ∈ Δ, ¬isFreeIn t H
h1 : IsDeduct Δ (forall_ v P.not_).not_
H : Formula
c1 : H = forall_ t (fastReplaceFree v t P.not_)
⊢ ¬isFreeIn t H
Tactic:
subst c1
Proof state after:
P Q : Formula
v t : VarName
Δ : Set Formula
h2 : IsDeduct (Δ ∪ {fastReplaceFree v t P}) Q
h3 : ¬occursIn t P
h4 : ¬occursIn t Q
h5 : ∀ H ∈ Δ, ¬isFreeIn t H
h1 : IsDeduct Δ (forall_ v P.not_).not_
⊢ ¬isFreeIn t (forall_ t (fastReplaceFree v t P.not_))
Theorem: FOL.NV.existsElim
Proof state before:
P Q : Formula
v t : VarName
Δ : Set Formula
h2 : IsDeduct (Δ ∪ {fastReplaceFree v t P}) Q
h3 : ¬occursIn t P
h4 : ¬occursIn t Q
h5 : ∀ H ∈ Δ, ¬isFreeIn t H
h1 : IsDeduct Δ (forall_ v P.not_).not_
⊢ ¬isFreeIn t (forall_ t (fastReplaceFree v t P.not_))
Tactic:
simp only [isFreeIn]
Proof state after:
P Q : Formula
v t : VarName
Δ : Set Formula
h2 : IsDeduct (Δ ∪ {fastReplaceFree v t P}) Q
h3 : ¬occursIn t P
h4 : ¬occursIn t Q
h5 : ∀ H ∈ Δ, ¬isFreeIn t H
h1 : IsDeduct Δ (forall_ v P.not_).not_
⊢ ¬(¬True ∧ isFreeIn t (fastReplaceFree v t P))
Theorem: FOL.NV.existsElim
Proof state before:
P Q : Formula
v t : VarName
Δ : Set Formula
h2 : IsDeduct (Δ ∪ {fastReplaceFree v t P}) Q
h3 : ¬occursIn t P
h4 : ¬occursIn t Q
h5 : ∀ H ∈ Δ, ¬isFreeIn t H
h1 : IsDeduct Δ (forall_ v P.not_).not_
⊢ ¬(¬True ∧ isFreeIn t (fastReplaceFree v t P))
Tactic:
simp
Proof state after:
no goals
Theorem: FOL.NV.existsElim
Proof state before:
P Q : Formula
v t : VarName
Δ : Set Formula
h2 : IsDeduct (Δ ∪ {fastReplaceFree v t P}) Q
h3 : ¬occursIn t P
h4 : ¬occursIn t Q
h5 : ∀ H ∈ Δ, ¬isFreeIn t H
h1 : IsDeduct Δ (forall_ v P.not_).not_
H : Formula
c1 : H ∈ Δ
⊢ ¬isFreeIn t H
Tactic:
exact h5 H c1
Proof state after:
no goals
Theorem: FOL.NV.existsElim
Proof state before:
case refine'_1.a
P Q : Formula
v t : VarName
Δ : Set Formula
h2 : IsDeduct (Δ ∪ {fastReplaceFree v t P}) Q
h3 : ¬occursIn t P
h4 : ¬occursIn t Q
h5 : ∀ H ∈ Δ, ¬isFreeIn t H
h1 : IsDeduct Δ (forall_ v P.not_).not_
⊢ IsDeduct Δ (forall_ v P.not_).not_
Tactic:
exact h1
Proof state after:
no goals
Theorem: FOL.NV.existsElim
Proof state before:
case refine'_2
P Q : Formula
v t : VarName
Δ : Set Formula
h1 : IsDeduct Δ (exists_ v P)
h2 : IsDeduct (Δ ∪ {fastReplaceFree v t P}) Q
h3 : ¬occursIn t P
h4 : ¬occursIn t Q
h5 : ∀ H ∈ Δ, ¬isFreeIn t H
⊢ ¬isFreeIn t Q
Tactic:
intro contra
Proof state after:
case refine'_2
P Q : Formula
v t : VarName
Δ : Set Formula
h1 : IsDeduct Δ (exists_ v P)
h2 : IsDeduct (Δ ∪ {fastReplaceFree v t P}) Q
h3 : ¬occursIn t P
h4 : ¬occursIn t Q
h5 : ∀ H ∈ Δ, ¬isFreeIn t H
contra : isFreeIn t Q
⊢ False
Theorem: FOL.NV.existsElim
Proof state before:
case refine'_2
P Q : Formula
v t : VarName
Δ : Set Formula
h1 : IsDeduct Δ (exists_ v P)
h2 : IsDeduct (Δ ∪ {fastReplaceFree v t P}) Q
h3 : ¬occursIn t P
h4 : ¬occursIn t Q
h5 : ∀ H ∈ Δ, ¬isFreeIn t H
contra : isFreeIn t Q
⊢ False
Tactic:
apply h4
Proof state after:
case refine'_2
P Q : Formula
v t : VarName
Δ : Set Formula
h1 : IsDeduct Δ (exists_ v P)
h2 : IsDeduct (Δ ∪ {fastReplaceFree v t P}) Q
h3 : ¬occursIn t P
h4 : ¬occursIn t Q
h5 : ∀ H ∈ Δ, ¬isFreeIn t H
contra : isFreeIn t Q
⊢ occursIn t Q
Theorem: FOL.NV.existsElim
Proof state before:
case refine'_2
P Q : Formula
v t : VarName
Δ : Set Formula
h1 : IsDeduct Δ (exists_ v P)
h2 : IsDeduct (Δ ∪ {fastReplaceFree v t P}) Q
h3 : ¬occursIn t P
h4 : ¬occursIn t Q
h5 : ∀ H ∈ Δ, ¬isFreeIn t H
contra : isFreeIn t Q
⊢ occursIn t Q
Tactic:
apply isFreeIn_imp_occursIn
Proof state after:
case refine'_2.h1
P Q : Formula
v t : VarName
Δ : Set Formula
h1 : IsDeduct Δ (exists_ v P)
h2 : IsDeduct (Δ ∪ {fastReplaceFree v t P}) Q
h3 : ¬occursIn t P
h4 : ¬occursIn t Q
h5 : ∀ H ∈ Δ, ¬isFreeIn t H
contra : isFreeIn t Q
⊢ isFreeIn t Q
Theorem: FOL.NV.existsElim
Proof state before:
case refine'_2.h1
P Q : Formula
v t : VarName
Δ : Set Formula
h1 : IsDeduct Δ (exists_ v P)
h2 : IsDeduct (Δ ∪ {fastReplaceFree v t P}) Q
h3 : ¬occursIn t P
h4 : ¬occursIn t Q
h5 : ∀ H ∈ Δ, ¬isFreeIn t H
contra : isFreeIn t Q
⊢ isFreeIn t Q
Tactic:
exact contra
Proof state after:
no goals
Theorem: FOL.NV.T_17_14
Proof state before:
P Q : Formula
v : VarName
⊢ IsProof ((exists_ v (P.and_ Q)).imp_ ((exists_ v P).and_ (exists_ v Q)))
Tactic:
apply deduction_theorem
Proof state after:
case h1
P Q : Formula
v : VarName
⊢ IsDeduct (∅ ∪ {exists_ v (P.and_ Q)}) ((exists_ v P).and_ (exists_ v Q))
Theorem: FOL.NV.T_17_14
Proof state before:
case h1
P Q : Formula
v : VarName
⊢ IsDeduct (∅ ∪ {exists_ v (P.and_ Q)}) ((exists_ v P).and_ (exists_ v Q))
Tactic:
simp
Proof state after:
case h1
P Q : Formula
v : VarName
⊢ IsDeduct {exists_ v (P.and_ Q)} ((exists_ v P).and_ (exists_ v Q))
Theorem: FOL.NV.T_17_14
Proof state before:
case h1
P Q : Formula
v : VarName
⊢ IsDeduct {exists_ v (P.and_ Q)} ((exists_ v P).and_ (exists_ v Q))
Tactic:
apply rule_C (P.and_ Q) ((exists_ v P).and_ (exists_ v Q)) v
Proof state after:
case h1.h1
P Q : Formula
v : VarName
⊢ IsDeduct {exists_ v (P.and_ Q)} (exists_ v (P.and_ Q))

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

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

case h1.h4
P Q : Formula
v : VarName
⊢ ¬isFreeIn v ((exists_ v P).and_ (exists_ v Q))
Theorem: FOL.NV.T_17_14
Proof state before:
case h1.h1
P Q : Formula
v : VarName
⊢ IsDeduct {exists_ v (P.and_ Q)} (exists_ v (P.and_ Q))
Tactic:
apply IsDeduct.assume_
Proof state after:
case h1.h1.a
P Q : Formula
v : VarName
⊢ exists_ v (P.and_ Q) ∈ {exists_ v (P.and_ Q)}
Theorem: FOL.NV.T_17_14
Proof state before:
case h1.h1.a
P Q : Formula
v : VarName
⊢ exists_ v (P.and_ Q) ∈ {exists_ v (P.and_ Q)}
Tactic:
simp
Proof state after:
no goals
Theorem: FOL.NV.T_17_14
Proof state before:
case h1.h2
P Q : Formula
v : VarName
⊢ IsDeduct ({exists_ v (P.and_ Q)} ∪ {P.and_ Q}) ((exists_ v P).and_ (exists_ v Q))
Tactic:
apply IsDeduct.mp_ (exists_ v Q)
Proof state after:
case h1.h2.a
P Q : Formula
v : VarName
⊢ IsDeduct ({exists_ v (P.and_ Q)} ∪ {P.and_ Q}) ((exists_ v Q).imp_ ((exists_ v P).and_ (exists_ v Q)))

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

case h1.h2.a.a
P Q : Formula
v : VarName
⊢ IsDeduct ({exists_ v (P.and_ Q)} ∪ {P.and_ Q}) (exists_ v P)
Theorem: FOL.NV.T_17_14
Proof state before:
case h1.h2.a.a
P Q : Formula
v : VarName
⊢ IsDeduct ({exists_ v (P.and_ Q)} ∪ {P.and_ Q})
    ((exists_ v P).imp_ ((exists_ v Q).imp_ ((exists_ v P).and_ (exists_ v Q))))
Tactic:
simp only [def_and_]
Proof state after:
case h1.h2.a.a
P Q : Formula
v : VarName
⊢ IsDeduct ({exists_ v (P.imp_ Q.not_).not_} ∪ {(P.imp_ Q.not_).not_})
    ((exists_ v P).imp_ ((exists_ v Q).imp_ ((exists_ v P).imp_ (exists_ v Q).not_).not_))
Theorem: FOL.NV.T_17_14
Proof state before:
case h1.h2.a.a
P Q : Formula
v : VarName
⊢ IsDeduct ({exists_ v (P.imp_ Q.not_).not_} ∪ {(P.imp_ Q.not_).not_})
    ((exists_ v P).imp_ ((exists_ v Q).imp_ ((exists_ v P).imp_ (exists_ v Q).not_).not_))
Tactic:
SC
Proof state after:
no goals
Theorem: FOL.NV.T_17_14
Proof state before:
case h1.h2.a.a
P Q : Formula
v : VarName
⊢ IsDeduct ({exists_ v (P.and_ Q)} ∪ {P.and_ Q}) (exists_ v P)
Tactic:
apply exists_intro P v v
Proof state after:
case h1.h2.a.a.h1
P Q : Formula
v : VarName
⊢ fastAdmits v v P

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

case h1.h2.a.a.h2.a
P Q : Formula
v : VarName
⊢ IsDeduct ({exists_ v (P.and_ Q)} ∪ {P.and_ Q}) (P.and_ Q)
Theorem: FOL.NV.T_17_14
Proof state before:
case h1.h2.a.a.h2.a
P Q : Formula
v : VarName
⊢ IsDeduct ({exists_ v (P.and_ Q)} ∪ {P.and_ Q}) ((P.and_ Q).imp_ P)
Tactic:
simp only [def_and_]
Proof state after:
case h1.h2.a.a.h2.a
P Q : Formula
v : VarName
⊢ IsDeduct ({exists_ v (P.imp_ Q.not_).not_} ∪ {(P.imp_ Q.not_).not_}) ((P.imp_ Q.not_).not_.imp_ P)
Theorem: FOL.NV.T_17_14
Proof state before:
case h1.h2.a.a.h2.a
P Q : Formula
v : VarName
⊢ IsDeduct ({exists_ v (P.imp_ Q.not_).not_} ∪ {(P.imp_ Q.not_).not_}) ((P.imp_ Q.not_).not_.imp_ P)
Tactic:
SC
Proof state after:
no goals
Theorem: FOL.NV.T_17_14
Proof state before:
case h1.h2.a.a.h2.a
P Q : Formula
v : VarName
⊢ IsDeduct ({exists_ v (P.and_ Q)} ∪ {P.and_ Q}) (P.and_ Q)
Tactic:
apply IsDeduct.assume_
Proof state after:
case h1.h2.a.a.h2.a.a
P Q : Formula
v : VarName
⊢ P.and_ Q ∈ {exists_ v (P.and_ Q)} ∪ {P.and_ Q}
Theorem: FOL.NV.T_17_14
Proof state before:
case h1.h2.a.a.h2.a.a
P Q : Formula
v : VarName
⊢ P.and_ Q ∈ {exists_ v (P.and_ Q)} ∪ {P.and_ Q}
Tactic:
simp
Proof state after:
no goals
Theorem: FOL.NV.T_17_14
Proof state before:
case h1.h2.a
P Q : Formula
v : VarName
⊢ IsDeduct ({exists_ v (P.and_ Q)} ∪ {P.and_ Q}) (exists_ v Q)
Tactic:
apply exists_intro Q v v
Proof state after:
case h1.h2.a.h1
P Q : Formula
v : VarName
⊢ fastAdmits v v Q

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

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

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

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

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

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

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

case h1.h1.h1.a.a
P Q : Formula
v : VarName
⊢ IsDeduct {forall_ v Q, forall_ v ((P.imp_ Q).and_ (Q.imp_ P))} ((P.imp_ Q).and_ (Q.imp_ P))
Theorem: FOL.NV.T_18_1_right
Proof state before:
case h1.h1.h1.a.a
P Q : Formula
v : VarName
⊢ IsDeduct {forall_ v Q, forall_ v ((P.imp_ Q).and_ (Q.imp_ P))} (((P.imp_ Q).and_ (Q.imp_ P)).imp_ (Q.imp_ P))
Tactic:
simp only [def_and_]
Proof state after:
case h1.h1.h1.a.a
P Q : Formula
v : VarName
⊢ IsDeduct {forall_ v Q, forall_ v ((P.imp_ Q).imp_ (Q.imp_ P).not_).not_}
    (((P.imp_ Q).imp_ (Q.imp_ P).not_).not_.imp_ (Q.imp_ P))
Theorem: FOL.NV.T_18_1_right
Proof state before:
case h1.h1.h1.a.a
P Q : Formula
v : VarName
⊢ IsDeduct {forall_ v Q, forall_ v ((P.imp_ Q).imp_ (Q.imp_ P).not_).not_}
    (((P.imp_ Q).imp_ (Q.imp_ P).not_).not_.imp_ (Q.imp_ P))
Tactic:
SC
Proof state after:
no goals