internlm/Lean-Github huggingface dataset:
Theorem: FOL.NV.T_17_10
Proof state before:
case h1.h1.h2
P : Formula
u v : VarName
⊢ ¬isFreeIn u (forall_ u (forall_ v P))
Tactic:
simp only [isFreeIn]
Proof state after:
case h1.h1.h2
P : Formula
u v : VarName
⊢ ¬(¬True ∧ ¬u = v ∧ isFreeIn u P)
Theorem: FOL.NV.T_17_10
Proof state before:
case h1.h1.h2
P : Formula
u v : VarName
⊢ ¬(¬True ∧ ¬u = v ∧ isFreeIn u P)
Tactic:
simp
Proof state after:
no goals
Theorem: FOL.NV.T_17_10
Proof state before:
case h1.h2
P : Formula
u v : VarName
⊢ ∀ H ∈ {forall_ u (forall_ v P)}, ¬isFreeIn v H
Tactic:
simp
Proof state after:
case h1.h2
P : Formula
u v : VarName
⊢ ¬isFreeIn v (forall_ u (forall_ v P))
Theorem: FOL.NV.T_17_10
Proof state before:
case h1.h2
P : Formula
u v : VarName
⊢ ¬isFreeIn v (forall_ u (forall_ v P))
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_17_10
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_17_11
Proof state before:
P Q : Formula
v : VarName
h1 : ¬isFreeIn v Q
⊢ IsProof ((forall_ v (P.imp_ Q)).imp_ ((exists_ v P).imp_ Q))
Tactic:
apply deduction_theorem
Proof state after:
case h1
P Q : Formula
v : VarName
h1 : ¬isFreeIn v Q
⊢ IsDeduct (∅ ∪ {forall_ v (P.imp_ Q)}) ((exists_ v P).imp_ Q)
Theorem: FOL.NV.T_17_11
Proof state before:
case h1
P Q : Formula
v : VarName
h1 : ¬isFreeIn v Q
⊢ IsDeduct (∅ ∪ {forall_ v (P.imp_ Q)}) ((exists_ v P).imp_ Q)
Tactic:
simp
Proof state after:
case h1
P Q : Formula
v : VarName
h1 : ¬isFreeIn v Q
⊢ IsDeduct {forall_ v (P.imp_ Q)} ((exists_ v P).imp_ Q)
Theorem: FOL.NV.T_17_11
Proof state before:
case h1
P Q : Formula
v : VarName
h1 : ¬isFreeIn v Q
⊢ IsDeduct {forall_ v (P.imp_ Q)} ((exists_ v P).imp_ Q)
Tactic:
simp only [def_exists_]
Proof state after:
case h1
P Q : Formula
v : VarName
h1 : ¬isFreeIn v Q
⊢ IsDeduct {forall_ v (P.imp_ Q)} ((forall_ v P.not_).not_.imp_ Q)
Theorem: FOL.NV.T_17_11
Proof state before:
case h1
P Q : Formula
v : VarName
h1 : ¬isFreeIn v Q
⊢ IsDeduct {forall_ v (P.imp_ Q)} ((forall_ v P.not_).not_.imp_ Q)
Tactic:
apply IsDeduct.mp_ (Q.not_.imp_ (forall_ v Q.not_))
Proof state after:
case h1.a
P Q : Formula
v : VarName
h1 : ¬isFreeIn v Q
⊢ IsDeduct {forall_ v (P.imp_ Q)} ((Q.not_.imp_ (forall_ v Q.not_)).imp_ ((forall_ v P.not_).not_.imp_ Q))

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

case h1.a.a
P Q : Formula
v : VarName
h1 : ¬isFreeIn v Q
⊢ IsDeduct {forall_ v (P.imp_ Q)} ((forall_ v Q.not_).imp_ (forall_ v P.not_))
Theorem: FOL.NV.T_17_11
Proof state before:
case h1.a.a
P Q : Formula
v : VarName
h1 : ¬isFreeIn v Q
⊢ IsDeduct {forall_ v (P.imp_ Q)}
    (((forall_ v Q.not_).imp_ (forall_ v P.not_)).imp_
      ((Q.not_.imp_ (forall_ v Q.not_)).imp_ ((forall_ v P.not_).not_.imp_ Q)))
Tactic:
SC
Proof state after:
no goals
Theorem: FOL.NV.T_17_11
Proof state before:
case h1.a.a
P Q : Formula
v : VarName
h1 : ¬isFreeIn v Q
⊢ IsDeduct {forall_ v (P.imp_ Q)} ((forall_ v Q.not_).imp_ (forall_ v P.not_))
Tactic:
apply IsDeduct.mp_ (forall_ v (Q.not_.imp_ P.not_))
Proof state after:
case h1.a.a.a
P Q : Formula
v : VarName
h1 : ¬isFreeIn v Q
⊢ IsDeduct {forall_ v (P.imp_ Q)} ((forall_ v (Q.not_.imp_ P.not_)).imp_ ((forall_ v Q.not_).imp_ (forall_ v P.not_)))

case h1.a.a.a
P Q : Formula
v : VarName
h1 : ¬isFreeIn v Q
⊢ IsDeduct {forall_ v (P.imp_ Q)} (forall_ v (Q.not_.imp_ P.not_))
Theorem: FOL.NV.T_17_11
Proof state before:
case h1.a.a.a
P Q : Formula
v : VarName
h1 : ¬isFreeIn v Q
⊢ IsDeduct {forall_ v (P.imp_ Q)} ((forall_ v (Q.not_.imp_ P.not_)).imp_ ((forall_ v Q.not_).imp_ (forall_ v P.not_)))
Tactic:
apply IsDeduct.axiom_
Proof state after:
case h1.a.a.a.a
P Q : Formula
v : VarName
h1 : ¬isFreeIn v Q
⊢ IsAxiom ((forall_ v (Q.not_.imp_ P.not_)).imp_ ((forall_ v Q.not_).imp_ (forall_ v P.not_)))
Theorem: FOL.NV.T_17_11
Proof state before:
case h1.a.a.a.a
P Q : Formula
v : VarName
h1 : ¬isFreeIn v Q
⊢ IsAxiom ((forall_ v (Q.not_.imp_ P.not_)).imp_ ((forall_ v Q.not_).imp_ (forall_ v P.not_)))
Tactic:
apply IsAxiom.pred_1_
Proof state after:
no goals
Theorem: FOL.NV.T_17_11
Proof state before:
case h1.a.a.a
P Q : Formula
v : VarName
h1 : ¬isFreeIn v Q
⊢ IsDeduct {forall_ v (P.imp_ Q)} (forall_ v (Q.not_.imp_ P.not_))
Tactic:
apply generalization
Proof state after:
case h1.a.a.a.h1
P Q : Formula
v : VarName
h1 : ¬isFreeIn v Q
⊢ IsDeduct {forall_ v (P.imp_ Q)} (Q.not_.imp_ P.not_)

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

case h1.a.a.a.h1.a
P Q : Formula
v : VarName
h1 : ¬isFreeIn v Q
⊢ IsDeduct {forall_ v (P.imp_ Q)} (P.imp_ Q)
Theorem: FOL.NV.T_17_11
Proof state before:
case h1.a.a.a.h1.a
P Q : Formula
v : VarName
h1 : ¬isFreeIn v Q
⊢ IsDeduct {forall_ v (P.imp_ Q)} ((P.imp_ Q).imp_ (Q.not_.imp_ P.not_))
Tactic:
apply proof_imp_deduct
Proof state after:
case h1.a.a.a.h1.a.h1
P Q : Formula
v : VarName
h1 : ¬isFreeIn v Q
⊢ IsProof ((P.imp_ Q).imp_ (Q.not_.imp_ P.not_))
Theorem: FOL.NV.T_17_11
Proof state before:
case h1.a.a.a.h1.a.h1
P Q : Formula
v : VarName
h1 : ¬isFreeIn v Q
⊢ IsProof ((P.imp_ Q).imp_ (Q.not_.imp_ P.not_))
Tactic:
apply T_14_7
Proof state after:
no goals
Theorem: FOL.NV.T_17_11
Proof state before:
case h1.a.a.a.h1.a
P Q : Formula
v : VarName
h1 : ¬isFreeIn v Q
⊢ IsDeduct {forall_ v (P.imp_ Q)} (P.imp_ Q)
Tactic:
apply specId v (P.imp_ Q)
Proof state after:
case h1.a.a.a.h1.a.h1
P Q : Formula
v : VarName
h1 : ¬isFreeIn v Q
⊢ IsDeduct {forall_ v (P.imp_ Q)} (forall_ v (P.imp_ Q))
Theorem: FOL.NV.T_17_11
Proof state before:
case h1.a.a.a.h1.a.h1
P Q : Formula
v : VarName
h1 : ¬isFreeIn v Q
⊢ IsDeduct {forall_ v (P.imp_ Q)} (forall_ v (P.imp_ Q))
Tactic:
apply IsDeduct.assume_
Proof state after:
case h1.a.a.a.h1.a.h1.a
P Q : Formula
v : VarName
h1 : ¬isFreeIn v Q
⊢ forall_ v (P.imp_ Q) ∈ {forall_ v (P.imp_ Q)}
Theorem: FOL.NV.T_17_11
Proof state before:
case h1.a.a.a.h1.a.h1.a
P Q : Formula
v : VarName
h1 : ¬isFreeIn v Q
⊢ forall_ v (P.imp_ Q) ∈ {forall_ v (P.imp_ Q)}
Tactic:
simp
Proof state after:
no goals
Theorem: FOL.NV.T_17_11
Proof state before:
case h1.a.a.a.h2
P Q : Formula
v : VarName
h1 : ¬isFreeIn v Q
⊢ ∀ H ∈ {forall_ v (P.imp_ Q)}, ¬isFreeIn v H
Tactic:
simp
Proof state after:
case h1.a.a.a.h2
P Q : Formula
v : VarName
h1 : ¬isFreeIn v Q
⊢ ¬isFreeIn v (forall_ v (P.imp_ Q))
Theorem: FOL.NV.T_17_11
Proof state before:
case h1.a.a.a.h2
P Q : Formula
v : VarName
h1 : ¬isFreeIn v Q
⊢ ¬isFreeIn v (forall_ v (P.imp_ Q))
Tactic:
simp only [isFreeIn]
Proof state after:
case h1.a.a.a.h2
P Q : Formula
v : VarName
h1 : ¬isFreeIn v Q
⊢ ¬(¬True ∧ (isFreeIn v P ∨ isFreeIn v Q))
Theorem: FOL.NV.T_17_11
Proof state before:
case h1.a.a.a.h2
P Q : Formula
v : VarName
h1 : ¬isFreeIn v Q
⊢ ¬(¬True ∧ (isFreeIn v P ∨ isFreeIn v Q))
Tactic:
simp
Proof state after:
no goals
Theorem: FOL.NV.T_17_11
Proof state before:
case h1.a
P Q : Formula
v : VarName
h1 : ¬isFreeIn v Q
⊢ IsDeduct {forall_ v (P.imp_ Q)} (Q.not_.imp_ (forall_ v Q.not_))
Tactic:
apply IsDeduct.axiom_
Proof state after:
case h1.a.a
P Q : Formula
v : VarName
h1 : ¬isFreeIn v Q
⊢ IsAxiom (Q.not_.imp_ (forall_ v Q.not_))
Theorem: FOL.NV.T_17_11
Proof state before:
case h1.a.a
P Q : Formula
v : VarName
h1 : ¬isFreeIn v Q
⊢ IsAxiom (Q.not_.imp_ (forall_ v Q.not_))
Tactic:
apply IsAxiom.pred_3_
Proof state after:
case h1.a.a.a
P Q : Formula
v : VarName
h1 : ¬isFreeIn v Q
⊢ ¬isFreeIn v Q.not_
Theorem: FOL.NV.T_17_11
Proof state before:
case h1.a.a.a
P Q : Formula
v : VarName
h1 : ¬isFreeIn v Q
⊢ ¬isFreeIn v Q.not_
Tactic:
simp only [isFreeIn]
Proof state after:
case h1.a.a.a
P Q : Formula
v : VarName
h1 : ¬isFreeIn v Q
⊢ ¬isFreeIn v Q
Theorem: FOL.NV.T_17_11
Proof state before:
case h1.a.a.a
P Q : Formula
v : VarName
h1 : ¬isFreeIn v Q
⊢ ¬isFreeIn v Q
Tactic:
exact h1
Proof state after:
no goals
Theorem: FOL.NV.T_17_12
Proof state before:
P Q : Formula
v : VarName
Δ : Set Formula
h1 : IsDeduct Δ (exists_ v P)
h2 : IsDeduct (Δ ∪ {P}) Q
h3 : ∀ H ∈ Δ, ¬isFreeIn v H
h4 : ¬isFreeIn v Q
⊢ IsDeduct Δ Q
Tactic:
apply IsDeduct.mp_ (exists_ v P)
Proof state after:
case a
P Q : Formula
v : VarName
Δ : Set Formula
h1 : IsDeduct Δ (exists_ v P)
h2 : IsDeduct (Δ ∪ {P}) Q
h3 : ∀ H ∈ Δ, ¬isFreeIn v H
h4 : ¬isFreeIn v Q
⊢ IsDeduct Δ ((exists_ v P).imp_ Q)

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

case a.a
P Q : Formula
v : VarName
Δ : Set Formula
h1 : IsDeduct Δ (exists_ v P)
h2 : IsDeduct (Δ ∪ {P}) Q
h3 : ∀ H ∈ Δ, ¬isFreeIn v H
h4 : ¬isFreeIn v Q
⊢ IsDeduct Δ (forall_ v (P.imp_ Q))
Theorem: FOL.NV.T_17_12
Proof state before:
case a.a
P Q : Formula
v : VarName
Δ : Set Formula
h1 : IsDeduct Δ (exists_ v P)
h2 : IsDeduct (Δ ∪ {P}) Q
h3 : ∀ H ∈ Δ, ¬isFreeIn v H
h4 : ¬isFreeIn v Q
⊢ IsDeduct Δ ((forall_ v (P.imp_ Q)).imp_ ((exists_ v P).imp_ Q))
Tactic:
apply proof_imp_deduct
Proof state after:
case a.a.h1
P Q : Formula
v : VarName
Δ : Set Formula
h1 : IsDeduct Δ (exists_ v P)
h2 : IsDeduct (Δ ∪ {P}) Q
h3 : ∀ H ∈ Δ, ¬isFreeIn v H
h4 : ¬isFreeIn v Q
⊢ IsProof ((forall_ v (P.imp_ Q)).imp_ ((exists_ v P).imp_ Q))
Theorem: FOL.NV.T_17_12
Proof state before:
case a.a.h1
P Q : Formula
v : VarName
Δ : Set Formula
h1 : IsDeduct Δ (exists_ v P)
h2 : IsDeduct (Δ ∪ {P}) Q
h3 : ∀ H ∈ Δ, ¬isFreeIn v H
h4 : ¬isFreeIn v Q
⊢ IsProof ((forall_ v (P.imp_ Q)).imp_ ((exists_ v P).imp_ Q))
Tactic:
exact T_17_11 P Q v h4
Proof state after:
no goals
Theorem: FOL.NV.T_17_12
Proof state before:
case a.a
P Q : Formula
v : VarName
Δ : Set Formula
h1 : IsDeduct Δ (exists_ v P)
h2 : IsDeduct (Δ ∪ {P}) Q
h3 : ∀ H ∈ Δ, ¬isFreeIn v H
h4 : ¬isFreeIn v Q
⊢ IsDeduct Δ (forall_ v (P.imp_ Q))
Tactic:
apply generalization
Proof state after:
case a.a.h1
P Q : Formula
v : VarName
Δ : Set Formula
h1 : IsDeduct Δ (exists_ v P)
h2 : IsDeduct (Δ ∪ {P}) Q
h3 : ∀ H ∈ Δ, ¬isFreeIn v H
h4 : ¬isFreeIn v Q
⊢ IsDeduct Δ (P.imp_ Q)

case a.a.h2
P Q : Formula
v : VarName
Δ : Set Formula
h1 : IsDeduct Δ (exists_ v P)
h2 : IsDeduct (Δ ∪ {P}) Q
h3 : ∀ H ∈ Δ, ¬isFreeIn v H
h4 : ¬isFreeIn v Q
⊢ ∀ H ∈ Δ, ¬isFreeIn v H
Theorem: FOL.NV.T_17_12
Proof state before:
case a.a.h1
P Q : Formula
v : VarName
Δ : Set Formula
h1 : IsDeduct Δ (exists_ v P)
h2 : IsDeduct (Δ ∪ {P}) Q
h3 : ∀ H ∈ Δ, ¬isFreeIn v H
h4 : ¬isFreeIn v Q
⊢ IsDeduct Δ (P.imp_ Q)
Tactic:
apply deduction_theorem
Proof state after:
case a.a.h1.h1
P Q : Formula
v : VarName
Δ : Set Formula
h1 : IsDeduct Δ (exists_ v P)
h2 : IsDeduct (Δ ∪ {P}) Q
h3 : ∀ H ∈ Δ, ¬isFreeIn v H
h4 : ¬isFreeIn v Q
⊢ IsDeduct (Δ ∪ {P}) Q
Theorem: FOL.NV.T_17_12
Proof state before:
case a.a.h1.h1
P Q : Formula
v : VarName
Δ : Set Formula
h1 : IsDeduct Δ (exists_ v P)
h2 : IsDeduct (Δ ∪ {P}) Q
h3 : ∀ H ∈ Δ, ¬isFreeIn v H
h4 : ¬isFreeIn v Q
⊢ IsDeduct (Δ ∪ {P}) Q
Tactic:
exact h2
Proof state after:
no goals
Theorem: FOL.NV.T_17_12
Proof state before:
case a.a.h2
P Q : Formula
v : VarName
Δ : Set Formula
h1 : IsDeduct Δ (exists_ v P)
h2 : IsDeduct (Δ ∪ {P}) Q
h3 : ∀ H ∈ Δ, ¬isFreeIn v H
h4 : ¬isFreeIn v Q
⊢ ∀ H ∈ Δ, ¬isFreeIn v H
Tactic:
exact h3
Proof state after:
no goals
Theorem: FOL.NV.T_17_12
Proof state before:
case a
P Q : Formula
v : VarName
Δ : Set Formula
h1 : IsDeduct Δ (exists_ v P)
h2 : IsDeduct (Δ ∪ {P}) Q
h3 : ∀ H ∈ Δ, ¬isFreeIn v H
h4 : ¬isFreeIn v Q
⊢ IsDeduct Δ (exists_ v P)
Tactic:
exact h1
Proof state after:
no goals
Theorem: FOL.NV.existsElim
Proof state before:
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
⊢ IsDeduct Δ Q
Tactic:
refine' rule_C (fastReplaceFree v t P) Q t Δ _ h2 h5 _
Proof state after:
case refine'_1
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
⊢ IsDeduct Δ (exists_ t (fastReplaceFree v t P))

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
Theorem: FOL.NV.existsElim
Proof state before:
case refine'_1
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
⊢ IsDeduct Δ (exists_ t (fastReplaceFree v t P))
Tactic:
simp only [def_exists_] at h1
Proof state after:
case refine'_1
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 Δ (exists_ t (fastReplaceFree v t P))
Theorem: FOL.NV.existsElim
Proof state before:
case refine'_1
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 Δ (exists_ t (fastReplaceFree v t P))
Tactic:
simp only [def_exists_]
Proof state after:
case refine'_1
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_ t (fastReplaceFree v t P).not_).not_
Theorem: FOL.NV.existsElim
Proof state before:
case refine'_1
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_ t (fastReplaceFree v t P).not_).not_
Tactic:
apply IsDeduct.mp_ (forall_ v P.not_).not_
Proof state after:
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_.imp_ (forall_ t (fastReplaceFree v t P).not_).not_)

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_
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_.imp_ (forall_ t (fastReplaceFree v t P).not_).not_)
Tactic:
apply IsDeduct.mp_ ((forall_ t (fastReplaceFree v t P.not_)).imp_ (forall_ v P.not_))
Proof state after:
case refine'_1.a.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_ t (fastReplaceFree v t P.not_)).imp_ (forall_ v P.not_)).imp_
      ((forall_ v P.not_).not_.imp_ (forall_ t (fastReplaceFree v t P).not_).not_))

case refine'_1.a.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_ t (fastReplaceFree v t P.not_)).imp_ (forall_ v P.not_))
Theorem: FOL.NV.existsElim
Proof state before:
case refine'_1.a.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_ t (fastReplaceFree v t P.not_)).imp_ (forall_ v P.not_)).imp_
      ((forall_ v P.not_).not_.imp_ (forall_ t (fastReplaceFree v t P).not_).not_))
Tactic:
SC
Proof state after:
no goals
Theorem: FOL.NV.existsElim
Proof state before:
case refine'_1.a.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_ t (fastReplaceFree v t P.not_)).imp_ (forall_ v P.not_))
Tactic:
apply deduction_theorem
Proof state after:
case refine'_1.a.a.h1
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_ t (fastReplaceFree v t P.not_)}) (forall_ v P.not_)
Theorem: FOL.NV.existsElim
Proof state before:
case refine'_1.a.a.h1
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_ t (fastReplaceFree v t P.not_)}) (forall_ v P.not_)
Tactic:
apply univIntro P.not_ v t _ h3
Proof state after:
case refine'_1.a.a.h1.h2
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_ t (fastReplaceFree v t P.not_)}) (fastReplaceFree v t P.not_)

case refine'_1.a.a.h1.h3
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 ∈ Δ ∪ {forall_ t (fastReplaceFree v t P.not_)}, ¬isFreeIn t H
Theorem: FOL.NV.existsElim
Proof state before:
case refine'_1.a.a.h1.h2
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_ t (fastReplaceFree v t P.not_)}) (fastReplaceFree v t P.not_)
Tactic:
apply specId t
Proof state after:
case refine'_1.a.a.h1.h2.h1
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_ t (fastReplaceFree v t P.not_)}) (forall_ t (fastReplaceFree v t P.not_))
Theorem: FOL.NV.existsElim
Proof state before:
case refine'_1.a.a.h1.h2.h1
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_ t (fastReplaceFree v t P.not_)}) (forall_ t (fastReplaceFree v t P.not_))
Tactic:
apply IsDeduct.assume_
Proof state after:
case refine'_1.a.a.h1.h2.h1.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_
⊢ forall_ t (fastReplaceFree v t P.not_) ∈ Δ ∪ {forall_ t (fastReplaceFree v t P.not_)}
Theorem: FOL.NV.existsElim
Proof state before:
case refine'_1.a.a.h1.h2.h1.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_
⊢ forall_ t (fastReplaceFree v t P.not_) ∈ Δ ∪ {forall_ t (fastReplaceFree v t P.not_)}
Tactic:
simp
Proof state after:
no goals
Theorem: FOL.NV.existsElim
Proof state before:
case refine'_1.a.a.h1.h3
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 ∈ Δ ∪ {forall_ t (fastReplaceFree v t P.not_)}, ¬isFreeIn t H
Tactic:
intro H a1
Proof state after:
case refine'_1.a.a.h1.h3
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
a1 : H ∈ Δ ∪ {forall_ t (fastReplaceFree v t P.not_)}
⊢ ¬isFreeIn t H
Theorem: FOL.NV.existsElim
Proof state before:
case refine'_1.a.a.h1.h3
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
a1 : H ∈ Δ ∪ {forall_ t (fastReplaceFree v t P.not_)}
⊢ ¬isFreeIn t H
Tactic:
simp at a1
Proof state after:
case refine'_1.a.a.h1.h3
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
a1 : H = forall_ t (fastReplaceFree v t P.not_) ∨ H ∈ Δ
⊢ ¬isFreeIn t H
Theorem: FOL.NV.existsElim
Proof state before:
case refine'_1.a.a.h1.h3
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
a1 : H = forall_ t (fastReplaceFree v t P.not_) ∨ H ∈ Δ
⊢ ¬isFreeIn t H
Tactic:
cases a1
Proof state after:
case refine'_1.a.a.h1.h3.inl
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
h✝ : H = forall_ t (fastReplaceFree v t P.not_)
⊢ ¬isFreeIn t H

case refine'_1.a.a.h1.h3.inr
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
h✝ : H ∈ Δ
⊢ ¬isFreeIn t H
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:
case _ c1 =>
  subst c1
  simp only [isFreeIn]
  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:
case _ c1 =>
  exact h5 H c1
Proof state after:
no goals