internlm/Lean-Github huggingface dataset:
Theorem: FOL.NV.T_14_3
Proof state before:
P Q : Formula
Δ : Set Formula
h1 : IsDeduct (Δ ∪ {P}) Q
⊢ IsDeduct Δ (P.imp_ Q)
Tactic:
induction h1
Proof state after:
case axiom_
P Q : Formula
Δ : Set Formula
phi✝ : Formula
a✝ : IsAxiom phi✝
⊢ IsDeduct Δ (P.imp_ phi✝)

case assume_
P Q : Formula
Δ : Set Formula
phi✝ : Formula
a✝ : phi✝ ∈ Δ ∪ {P}
⊢ IsDeduct Δ (P.imp_ phi✝)

case mp_
P Q : Formula
Δ : Set Formula
phi✝ psi✝ : Formula
a✝¹ : IsDeduct (Δ ∪ {P}) (phi✝.imp_ psi✝)
a✝ : IsDeduct (Δ ∪ {P}) phi✝
a_ih✝¹ : IsDeduct Δ (P.imp_ (phi✝.imp_ psi✝))
a_ih✝ : IsDeduct Δ (P.imp_ phi✝)
⊢ IsDeduct Δ (P.imp_ psi✝)
Theorem: FOL.NV.T_14_3
Proof state before:
P Q : Formula
Δ : Set Formula
h1_phi : Formula
h1_1 : IsAxiom h1_phi
⊢ IsDeduct Δ (P.imp_ h1_phi)
Tactic:
apply IsDeduct.mp_ h1_phi
Proof state after:
case a
P Q : Formula
Δ : Set Formula
h1_phi : Formula
h1_1 : IsAxiom h1_phi
⊢ IsDeduct Δ (h1_phi.imp_ (P.imp_ h1_phi))

case a
P Q : Formula
Δ : Set Formula
h1_phi : Formula
h1_1 : IsAxiom h1_phi
⊢ IsDeduct Δ h1_phi
Theorem: FOL.NV.T_14_3
Proof state before:
case a
P Q : Formula
Δ : Set Formula
h1_phi : Formula
h1_1 : IsAxiom h1_phi
⊢ IsDeduct Δ (h1_phi.imp_ (P.imp_ h1_phi))
Tactic:
apply IsDeduct.axiom_
Proof state after:
case a.a
P Q : Formula
Δ : Set Formula
h1_phi : Formula
h1_1 : IsAxiom h1_phi
⊢ IsAxiom (h1_phi.imp_ (P.imp_ h1_phi))
Theorem: FOL.NV.T_14_3
Proof state before:
case a.a
P Q : Formula
Δ : Set Formula
h1_phi : Formula
h1_1 : IsAxiom h1_phi
⊢ IsAxiom (h1_phi.imp_ (P.imp_ h1_phi))
Tactic:
exact IsAxiom.prop_1_ h1_phi P
Proof state after:
no goals
Theorem: FOL.NV.T_14_3
Proof state before:
case a
P Q : Formula
Δ : Set Formula
h1_phi : Formula
h1_1 : IsAxiom h1_phi
⊢ IsDeduct Δ h1_phi
Tactic:
apply IsDeduct.axiom_
Proof state after:
case a.a
P Q : Formula
Δ : Set Formula
h1_phi : Formula
h1_1 : IsAxiom h1_phi
⊢ IsAxiom h1_phi
Theorem: FOL.NV.T_14_3
Proof state before:
case a.a
P Q : Formula
Δ : Set Formula
h1_phi : Formula
h1_1 : IsAxiom h1_phi
⊢ IsAxiom h1_phi
Tactic:
exact h1_1
Proof state after:
no goals
Theorem: FOL.NV.T_14_3
Proof state before:
P Q : Formula
Δ : Set Formula
h1_phi : Formula
h1_1 : h1_phi ∈ Δ ∪ {P}
⊢ IsDeduct Δ (P.imp_ h1_phi)
Tactic:
simp at h1_1
Proof state after:
P Q : Formula
Δ : Set Formula
h1_phi : Formula
h1_1 : h1_phi = P ∨ h1_phi ∈ Δ
⊢ IsDeduct Δ (P.imp_ h1_phi)
Theorem: FOL.NV.T_14_3
Proof state before:
P Q : Formula
Δ : Set Formula
h1_phi : Formula
h1_1 : h1_phi = P ∨ h1_phi ∈ Δ
⊢ IsDeduct Δ (P.imp_ h1_phi)
Tactic:
cases h1_1
Proof state after:
case inl
P Q : Formula
Δ : Set Formula
h1_phi : Formula
h✝ : h1_phi = P
⊢ IsDeduct Δ (P.imp_ h1_phi)

case inr
P Q : Formula
Δ : Set Formula
h1_phi : Formula
h✝ : h1_phi ∈ Δ
⊢ IsDeduct Δ (P.imp_ h1_phi)
Theorem: FOL.NV.T_14_3
Proof state before:
P Q : Formula
Δ : Set Formula
h1_phi : Formula
h1_1 : h1_phi = P
⊢ IsDeduct Δ (P.imp_ h1_phi)
Tactic:
case inl h1_1 =>
  subst h1_1
  apply proof_imp_deduct
  exact prop_id h1_phi
Proof state after:
no goals
Theorem: FOL.NV.T_14_3
Proof state before:
P Q : Formula
Δ : Set Formula
h1_phi : Formula
h1_1 : h1_phi = P
⊢ IsDeduct Δ (P.imp_ h1_phi)
Tactic:
subst h1_1
Proof state after:
Q : Formula
Δ : Set Formula
h1_phi : Formula
⊢ IsDeduct Δ (h1_phi.imp_ h1_phi)
Theorem: FOL.NV.T_14_3
Proof state before:
Q : Formula
Δ : Set Formula
h1_phi : Formula
⊢ IsDeduct Δ (h1_phi.imp_ h1_phi)
Tactic:
apply proof_imp_deduct
Proof state after:
case h1
Q : Formula
Δ : Set Formula
h1_phi : Formula
⊢ IsProof (h1_phi.imp_ h1_phi)
Theorem: FOL.NV.T_14_3
Proof state before:
case h1
Q : Formula
Δ : Set Formula
h1_phi : Formula
⊢ IsProof (h1_phi.imp_ h1_phi)
Tactic:
exact prop_id h1_phi
Proof state after:
no goals
Theorem: FOL.NV.T_14_3
Proof state before:
P Q : Formula
Δ : Set Formula
h1_phi : Formula
h1_1 : h1_phi ∈ Δ
⊢ IsDeduct Δ (P.imp_ h1_phi)
Tactic:
apply IsDeduct.mp_ h1_phi
Proof state after:
case a
P Q : Formula
Δ : Set Formula
h1_phi : Formula
h1_1 : h1_phi ∈ Δ
⊢ IsDeduct Δ (h1_phi.imp_ (P.imp_ h1_phi))

case a
P Q : Formula
Δ : Set Formula
h1_phi : Formula
h1_1 : h1_phi ∈ Δ
⊢ IsDeduct Δ h1_phi
Theorem: FOL.NV.T_14_3
Proof state before:
case a
P Q : Formula
Δ : Set Formula
h1_phi : Formula
h1_1 : h1_phi ∈ Δ
⊢ IsDeduct Δ (h1_phi.imp_ (P.imp_ h1_phi))
Tactic:
apply IsDeduct.axiom_
Proof state after:
case a.a
P Q : Formula
Δ : Set Formula
h1_phi : Formula
h1_1 : h1_phi ∈ Δ
⊢ IsAxiom (h1_phi.imp_ (P.imp_ h1_phi))
Theorem: FOL.NV.T_14_3
Proof state before:
case a.a
P Q : Formula
Δ : Set Formula
h1_phi : Formula
h1_1 : h1_phi ∈ Δ
⊢ IsAxiom (h1_phi.imp_ (P.imp_ h1_phi))
Tactic:
exact IsAxiom.prop_1_ h1_phi P
Proof state after:
no goals
Theorem: FOL.NV.T_14_3
Proof state before:
case a
P Q : Formula
Δ : Set Formula
h1_phi : Formula
h1_1 : h1_phi ∈ Δ
⊢ IsDeduct Δ h1_phi
Tactic:
apply IsDeduct.assume_
Proof state after:
case a.a
P Q : Formula
Δ : Set Formula
h1_phi : Formula
h1_1 : h1_phi ∈ Δ
⊢ h1_phi ∈ Δ
Theorem: FOL.NV.T_14_3
Proof state before:
case a.a
P Q : Formula
Δ : Set Formula
h1_phi : Formula
h1_1 : h1_phi ∈ Δ
⊢ h1_phi ∈ Δ
Tactic:
exact h1_1
Proof state after:
no goals
Theorem: FOL.NV.T_14_3
Proof state before:
P Q : Formula
Δ : Set Formula
h1_phi h1_psi : Formula
a✝¹ : IsDeduct (Δ ∪ {P}) (h1_phi.imp_ h1_psi)
a✝ : IsDeduct (Δ ∪ {P}) h1_phi
h1_ih_1 : IsDeduct Δ (P.imp_ (h1_phi.imp_ h1_psi))
h1_ih_2 : IsDeduct Δ (P.imp_ h1_phi)
⊢ IsDeduct Δ (P.imp_ h1_psi)
Tactic:
apply IsDeduct.mp_ (P.imp_ h1_phi)
Proof state after:
case a
P Q : Formula
Δ : Set Formula
h1_phi h1_psi : Formula
a✝¹ : IsDeduct (Δ ∪ {P}) (h1_phi.imp_ h1_psi)
a✝ : IsDeduct (Δ ∪ {P}) h1_phi
h1_ih_1 : IsDeduct Δ (P.imp_ (h1_phi.imp_ h1_psi))
h1_ih_2 : IsDeduct Δ (P.imp_ h1_phi)
⊢ IsDeduct Δ ((P.imp_ h1_phi).imp_ (P.imp_ h1_psi))

case a
P Q : Formula
Δ : Set Formula
h1_phi h1_psi : Formula
a✝¹ : IsDeduct (Δ ∪ {P}) (h1_phi.imp_ h1_psi)
a✝ : IsDeduct (Δ ∪ {P}) h1_phi
h1_ih_1 : IsDeduct Δ (P.imp_ (h1_phi.imp_ h1_psi))
h1_ih_2 : IsDeduct Δ (P.imp_ h1_phi)
⊢ IsDeduct Δ (P.imp_ h1_phi)
Theorem: FOL.NV.T_14_3
Proof state before:
case a
P Q : Formula
Δ : Set Formula
h1_phi h1_psi : Formula
a✝¹ : IsDeduct (Δ ∪ {P}) (h1_phi.imp_ h1_psi)
a✝ : IsDeduct (Δ ∪ {P}) h1_phi
h1_ih_1 : IsDeduct Δ (P.imp_ (h1_phi.imp_ h1_psi))
h1_ih_2 : IsDeduct Δ (P.imp_ h1_phi)
⊢ IsDeduct Δ ((P.imp_ h1_phi).imp_ (P.imp_ h1_psi))
Tactic:
apply IsDeduct.mp_ (P.imp_ (h1_phi.imp_ h1_psi))
Proof state after:
case a.a
P Q : Formula
Δ : Set Formula
h1_phi h1_psi : Formula
a✝¹ : IsDeduct (Δ ∪ {P}) (h1_phi.imp_ h1_psi)
a✝ : IsDeduct (Δ ∪ {P}) h1_phi
h1_ih_1 : IsDeduct Δ (P.imp_ (h1_phi.imp_ h1_psi))
h1_ih_2 : IsDeduct Δ (P.imp_ h1_phi)
⊢ IsDeduct Δ ((P.imp_ (h1_phi.imp_ h1_psi)).imp_ ((P.imp_ h1_phi).imp_ (P.imp_ h1_psi)))

case a.a
P Q : Formula
Δ : Set Formula
h1_phi h1_psi : Formula
a✝¹ : IsDeduct (Δ ∪ {P}) (h1_phi.imp_ h1_psi)
a✝ : IsDeduct (Δ ∪ {P}) h1_phi
h1_ih_1 : IsDeduct Δ (P.imp_ (h1_phi.imp_ h1_psi))
h1_ih_2 : IsDeduct Δ (P.imp_ h1_phi)
⊢ IsDeduct Δ (P.imp_ (h1_phi.imp_ h1_psi))
Theorem: FOL.NV.T_14_3
Proof state before:
case a.a
P Q : Formula
Δ : Set Formula
h1_phi h1_psi : Formula
a✝¹ : IsDeduct (Δ ∪ {P}) (h1_phi.imp_ h1_psi)
a✝ : IsDeduct (Δ ∪ {P}) h1_phi
h1_ih_1 : IsDeduct Δ (P.imp_ (h1_phi.imp_ h1_psi))
h1_ih_2 : IsDeduct Δ (P.imp_ h1_phi)
⊢ IsDeduct Δ ((P.imp_ (h1_phi.imp_ h1_psi)).imp_ ((P.imp_ h1_phi).imp_ (P.imp_ h1_psi)))
Tactic:
apply IsDeduct.axiom_
Proof state after:
case a.a.a
P Q : Formula
Δ : Set Formula
h1_phi h1_psi : Formula
a✝¹ : IsDeduct (Δ ∪ {P}) (h1_phi.imp_ h1_psi)
a✝ : IsDeduct (Δ ∪ {P}) h1_phi
h1_ih_1 : IsDeduct Δ (P.imp_ (h1_phi.imp_ h1_psi))
h1_ih_2 : IsDeduct Δ (P.imp_ h1_phi)
⊢ IsAxiom ((P.imp_ (h1_phi.imp_ h1_psi)).imp_ ((P.imp_ h1_phi).imp_ (P.imp_ h1_psi)))
Theorem: FOL.NV.T_14_3
Proof state before:
case a.a.a
P Q : Formula
Δ : Set Formula
h1_phi h1_psi : Formula
a✝¹ : IsDeduct (Δ ∪ {P}) (h1_phi.imp_ h1_psi)
a✝ : IsDeduct (Δ ∪ {P}) h1_phi
h1_ih_1 : IsDeduct Δ (P.imp_ (h1_phi.imp_ h1_psi))
h1_ih_2 : IsDeduct Δ (P.imp_ h1_phi)
⊢ IsAxiom ((P.imp_ (h1_phi.imp_ h1_psi)).imp_ ((P.imp_ h1_phi).imp_ (P.imp_ h1_psi)))
Tactic:
exact IsAxiom.prop_2_ P h1_phi h1_psi
Proof state after:
no goals
Theorem: FOL.NV.T_14_3
Proof state before:
case a.a
P Q : Formula
Δ : Set Formula
h1_phi h1_psi : Formula
a✝¹ : IsDeduct (Δ ∪ {P}) (h1_phi.imp_ h1_psi)
a✝ : IsDeduct (Δ ∪ {P}) h1_phi
h1_ih_1 : IsDeduct Δ (P.imp_ (h1_phi.imp_ h1_psi))
h1_ih_2 : IsDeduct Δ (P.imp_ h1_phi)
⊢ IsDeduct Δ (P.imp_ (h1_phi.imp_ h1_psi))
Tactic:
exact h1_ih_1
Proof state after:
no goals
Theorem: FOL.NV.T_14_3
Proof state before:
case a
P Q : Formula
Δ : Set Formula
h1_phi h1_psi : Formula
a✝¹ : IsDeduct (Δ ∪ {P}) (h1_phi.imp_ h1_psi)
a✝ : IsDeduct (Δ ∪ {P}) h1_phi
h1_ih_1 : IsDeduct Δ (P.imp_ (h1_phi.imp_ h1_psi))
h1_ih_2 : IsDeduct Δ (P.imp_ h1_phi)
⊢ IsDeduct Δ (P.imp_ h1_phi)
Tactic:
exact h1_ih_2
Proof state after:
no goals
Theorem: FOL.NV.T_13_6
Proof state before:
P Q : Formula
⊢ IsProof (P.not_.imp_ (P.imp_ Q))
Tactic:
simp only [IsProof]
Proof state after:
P Q : Formula
⊢ IsDeduct ∅ (P.not_.imp_ (P.imp_ Q))
Theorem: FOL.NV.T_13_6
Proof state before:
P Q : Formula
⊢ IsDeduct ∅ (P.not_.imp_ (P.imp_ Q))
Tactic:
apply deduction_theorem
Proof state after:
case h1
P Q : Formula
⊢ IsDeduct (∅ ∪ {P.not_}) (P.imp_ Q)
Theorem: FOL.NV.T_13_6
Proof state before:
case h1
P Q : Formula
⊢ IsDeduct (∅ ∪ {P.not_}) (P.imp_ Q)
Tactic:
apply IsDeduct.mp_ (Q.not_.imp_ P.not_)
Proof state after:
case h1.a
P Q : Formula
⊢ IsDeduct (∅ ∪ {P.not_}) ((Q.not_.imp_ P.not_).imp_ (P.imp_ Q))

case h1.a
P Q : Formula
⊢ IsDeduct (∅ ∪ {P.not_}) (Q.not_.imp_ P.not_)
Theorem: FOL.NV.T_13_6
Proof state before:
case h1.a
P Q : Formula
⊢ IsDeduct (∅ ∪ {P.not_}) ((Q.not_.imp_ P.not_).imp_ (P.imp_ Q))
Tactic:
apply IsDeduct.axiom_
Proof state after:
case h1.a.a
P Q : Formula
⊢ IsAxiom ((Q.not_.imp_ P.not_).imp_ (P.imp_ Q))
Theorem: FOL.NV.T_13_6
Proof state before:
case h1.a.a
P Q : Formula
⊢ IsAxiom ((Q.not_.imp_ P.not_).imp_ (P.imp_ Q))
Tactic:
exact IsAxiom.prop_3_ Q P
Proof state after:
no goals
Theorem: FOL.NV.T_13_6
Proof state before:
case h1.a
P Q : Formula
⊢ IsDeduct (∅ ∪ {P.not_}) (Q.not_.imp_ P.not_)
Tactic:
apply IsDeduct.mp_ P.not_
Proof state after:
case h1.a.a
P Q : Formula
⊢ IsDeduct (∅ ∪ {P.not_}) (P.not_.imp_ (Q.not_.imp_ P.not_))

case h1.a.a
P Q : Formula
⊢ IsDeduct (∅ ∪ {P.not_}) P.not_
Theorem: FOL.NV.T_13_6
Proof state before:
case h1.a.a
P Q : Formula
⊢ IsDeduct (∅ ∪ {P.not_}) (P.not_.imp_ (Q.not_.imp_ P.not_))
Tactic:
apply IsDeduct.axiom_
Proof state after:
case h1.a.a.a
P Q : Formula
⊢ IsAxiom (P.not_.imp_ (Q.not_.imp_ P.not_))
Theorem: FOL.NV.T_13_6
Proof state before:
case h1.a.a.a
P Q : Formula
⊢ IsAxiom (P.not_.imp_ (Q.not_.imp_ P.not_))
Tactic:
exact IsAxiom.prop_1_ P.not_ Q.not_
Proof state after:
no goals
Theorem: FOL.NV.T_13_6
Proof state before:
case h1.a.a
P Q : Formula
⊢ IsDeduct (∅ ∪ {P.not_}) P.not_
Tactic:
apply IsDeduct.assume_
Proof state after:
case h1.a.a.a
P Q : Formula
⊢ P.not_ ∈ ∅ ∪ {P.not_}
Theorem: FOL.NV.T_13_6
Proof state before:
case h1.a.a.a
P Q : Formula
⊢ P.not_ ∈ ∅ ∪ {P.not_}
Tactic:
simp
Proof state after:
no goals
Theorem: FOL.NV.T_14_5
Proof state before:
P : Formula
⊢ IsProof (P.not_.not_.imp_ P)
Tactic:
simp only [IsProof]
Proof state after:
P : Formula
⊢ IsDeduct ∅ (P.not_.not_.imp_ P)
Theorem: FOL.NV.T_14_5
Proof state before:
P : Formula
⊢ IsDeduct ∅ (P.not_.not_.imp_ P)
Tactic:
apply deduction_theorem
Proof state after:
case h1
P : Formula
⊢ IsDeduct (∅ ∪ {P.not_.not_}) P
Theorem: FOL.NV.T_14_5
Proof state before:
case h1
P : Formula
⊢ IsDeduct (∅ ∪ {P.not_.not_}) P
Tactic:
apply IsDeduct.mp_ P.not_.not_
Proof state after:
case h1.a
P : Formula
⊢ IsDeduct (∅ ∪ {P.not_.not_}) (P.not_.not_.imp_ P)

case h1.a
P : Formula
⊢ IsDeduct (∅ ∪ {P.not_.not_}) P.not_.not_
Theorem: FOL.NV.T_14_5
Proof state before:
case h1.a
P : Formula
⊢ IsDeduct (∅ ∪ {P.not_.not_}) (P.not_.not_.imp_ P)
Tactic:
apply IsDeduct.mp_ (P.not_.imp_ P.not_.not_.not_)
Proof state after:
case h1.a.a
P : Formula
⊢ IsDeduct (∅ ∪ {P.not_.not_}) ((P.not_.imp_ P.not_.not_.not_).imp_ (P.not_.not_.imp_ P))

case h1.a.a
P : Formula
⊢ IsDeduct (∅ ∪ {P.not_.not_}) (P.not_.imp_ P.not_.not_.not_)
Theorem: FOL.NV.T_14_5
Proof state before:
case h1.a.a
P : Formula
⊢ IsDeduct (∅ ∪ {P.not_.not_}) ((P.not_.imp_ P.not_.not_.not_).imp_ (P.not_.not_.imp_ P))
Tactic:
apply IsDeduct.axiom_
Proof state after:
case h1.a.a.a
P : Formula
⊢ IsAxiom ((P.not_.imp_ P.not_.not_.not_).imp_ (P.not_.not_.imp_ P))
Theorem: FOL.NV.T_14_5
Proof state before:
case h1.a.a.a
P : Formula
⊢ IsAxiom ((P.not_.imp_ P.not_.not_.not_).imp_ (P.not_.not_.imp_ P))
Tactic:
apply IsAxiom.prop_3_
Proof state after:
no goals
Theorem: FOL.NV.T_14_5
Proof state before:
case h1.a.a
P : Formula
⊢ IsDeduct (∅ ∪ {P.not_.not_}) (P.not_.imp_ P.not_.not_.not_)
Tactic:
apply IsDeduct.mp_ P.not_.not_
Proof state after:
case h1.a.a.a
P : Formula
⊢ IsDeduct (∅ ∪ {P.not_.not_}) (P.not_.not_.imp_ (P.not_.imp_ P.not_.not_.not_))

case h1.a.a.a
P : Formula
⊢ IsDeduct (∅ ∪ {P.not_.not_}) P.not_.not_
Theorem: FOL.NV.T_14_5
Proof state before:
case h1.a.a.a
P : Formula
⊢ IsDeduct (∅ ∪ {P.not_.not_}) (P.not_.not_.imp_ (P.not_.imp_ P.not_.not_.not_))
Tactic:
apply proof_imp_deduct
Proof state after:
case h1.a.a.a.h1
P : Formula
⊢ IsProof (P.not_.not_.imp_ (P.not_.imp_ P.not_.not_.not_))
Theorem: FOL.NV.T_14_5
Proof state before:
case h1.a.a.a.h1
P : Formula
⊢ IsProof (P.not_.not_.imp_ (P.not_.imp_ P.not_.not_.not_))
Tactic:
apply T_13_6
Proof state after:
no goals
Theorem: FOL.NV.T_14_5
Proof state before:
case h1.a.a.a
P : Formula
⊢ IsDeduct (∅ ∪ {P.not_.not_}) P.not_.not_
Tactic:
apply IsDeduct.assume_
Proof state after:
case h1.a.a.a.a
P : Formula
⊢ P.not_.not_ ∈ ∅ ∪ {P.not_.not_}
Theorem: FOL.NV.T_14_5
Proof state before:
case h1.a.a.a.a
P : Formula
⊢ P.not_.not_ ∈ ∅ ∪ {P.not_.not_}
Tactic:
simp
Proof state after:
no goals
Theorem: FOL.NV.T_14_5
Proof state before:
case h1.a
P : Formula
⊢ IsDeduct (∅ ∪ {P.not_.not_}) P.not_.not_
Tactic:
apply IsDeduct.assume_
Proof state after:
case h1.a.a
P : Formula
⊢ P.not_.not_ ∈ ∅ ∪ {P.not_.not_}
Theorem: FOL.NV.T_14_5
Proof state before:
case h1.a.a
P : Formula
⊢ P.not_.not_ ∈ ∅ ∪ {P.not_.not_}
Tactic:
simp
Proof state after:
no goals
Theorem: FOL.NV.T_14_6
Proof state before:
P : Formula
⊢ IsProof (P.imp_ P.not_.not_)
Tactic:
simp only [IsProof]
Proof state after:
P : Formula
⊢ IsDeduct ∅ (P.imp_ P.not_.not_)
Theorem: FOL.NV.T_14_6
Proof state before:
P : Formula
⊢ IsDeduct ∅ (P.imp_ P.not_.not_)
Tactic:
apply IsDeduct.mp_ (P.not_.not_.not_.imp_ P.not_)
Proof state after:
case a
P : Formula
⊢ IsDeduct ∅ ((P.not_.not_.not_.imp_ P.not_).imp_ (P.imp_ P.not_.not_))

case a
P : Formula
⊢ IsDeduct ∅ (P.not_.not_.not_.imp_ P.not_)
Theorem: FOL.NV.T_14_6
Proof state before:
case a
P : Formula
⊢ IsDeduct ∅ ((P.not_.not_.not_.imp_ P.not_).imp_ (P.imp_ P.not_.not_))
Tactic:
apply IsDeduct.axiom_
Proof state after:
case a.a
P : Formula
⊢ IsAxiom ((P.not_.not_.not_.imp_ P.not_).imp_ (P.imp_ P.not_.not_))
Theorem: FOL.NV.T_14_6
Proof state before:
case a.a
P : Formula
⊢ IsAxiom ((P.not_.not_.not_.imp_ P.not_).imp_ (P.imp_ P.not_.not_))
Tactic:
exact IsAxiom.prop_3_ P.not_.not_ P
Proof state after:
no goals
Theorem: FOL.NV.T_14_6
Proof state before:
case a
P : Formula
⊢ IsDeduct ∅ (P.not_.not_.not_.imp_ P.not_)
Tactic:
apply proof_imp_deduct
Proof state after:
case a.h1
P : Formula
⊢ IsProof (P.not_.not_.not_.imp_ P.not_)
Theorem: FOL.NV.T_14_6
Proof state before:
case a.h1
P : Formula
⊢ IsProof (P.not_.not_.not_.imp_ P.not_)
Tactic:
exact T_14_5 P.not_
Proof state after:
no goals
Theorem: FOL.NV.T_14_7
Proof state before:
P Q : Formula
⊢ IsProof ((P.imp_ Q).imp_ (Q.not_.imp_ P.not_))
Tactic:
simp only [IsProof]
Proof state after:
P Q : Formula
⊢ IsDeduct ∅ ((P.imp_ Q).imp_ (Q.not_.imp_ P.not_))
Theorem: FOL.NV.T_14_7
Proof state before:
P Q : Formula
⊢ IsDeduct ∅ ((P.imp_ Q).imp_ (Q.not_.imp_ P.not_))
Tactic:
apply deduction_theorem
Proof state after:
case h1
P Q : Formula
⊢ IsDeduct (∅ ∪ {P.imp_ Q}) (Q.not_.imp_ P.not_)
Theorem: FOL.NV.T_14_7
Proof state before:
case h1
P Q : Formula
⊢ IsDeduct (∅ ∪ {P.imp_ Q}) (Q.not_.imp_ P.not_)
Tactic:
apply IsDeduct.mp_ (P.not_.not_.imp_ Q.not_.not_)
Proof state after:
case h1.a
P Q : Formula
⊢ IsDeduct (∅ ∪ {P.imp_ Q}) ((P.not_.not_.imp_ Q.not_.not_).imp_ (Q.not_.imp_ P.not_))

case h1.a
P Q : Formula
⊢ IsDeduct (∅ ∪ {P.imp_ Q}) (P.not_.not_.imp_ Q.not_.not_)
Theorem: FOL.NV.T_14_7
Proof state before:
case h1.a
P Q : Formula
⊢ IsDeduct (∅ ∪ {P.imp_ Q}) ((P.not_.not_.imp_ Q.not_.not_).imp_ (Q.not_.imp_ P.not_))
Tactic:
apply IsDeduct.axiom_
Proof state after:
case h1.a.a
P Q : Formula
⊢ IsAxiom ((P.not_.not_.imp_ Q.not_.not_).imp_ (Q.not_.imp_ P.not_))
Theorem: FOL.NV.T_14_7
Proof state before:
case h1.a.a
P Q : Formula
⊢ IsAxiom ((P.not_.not_.imp_ Q.not_.not_).imp_ (Q.not_.imp_ P.not_))
Tactic:
apply IsAxiom.prop_3_
Proof state after:
no goals
Theorem: FOL.NV.T_14_7
Proof state before:
case h1.a
P Q : Formula
⊢ IsDeduct (∅ ∪ {P.imp_ Q}) (P.not_.not_.imp_ Q.not_.not_)
Tactic:
apply deduction_theorem
Proof state after:
case h1.a.h1
P Q : Formula
⊢ IsDeduct (∅ ∪ {P.imp_ Q} ∪ {P.not_.not_}) Q.not_.not_
Theorem: FOL.NV.T_14_7
Proof state before:
case h1.a.h1
P Q : Formula
⊢ IsDeduct (∅ ∪ {P.imp_ Q} ∪ {P.not_.not_}) Q.not_.not_
Tactic:
apply IsDeduct.mp_ Q
Proof state after:
case h1.a.h1.a
P Q : Formula
⊢ IsDeduct (∅ ∪ {P.imp_ Q} ∪ {P.not_.not_}) (Q.imp_ Q.not_.not_)

case h1.a.h1.a
P Q : Formula
⊢ IsDeduct (∅ ∪ {P.imp_ Q} ∪ {P.not_.not_}) Q
Theorem: FOL.NV.T_14_7
Proof state before:
case h1.a.h1.a
P Q : Formula
⊢ IsDeduct (∅ ∪ {P.imp_ Q} ∪ {P.not_.not_}) (Q.imp_ Q.not_.not_)
Tactic:
apply proof_imp_deduct
Proof state after:
case h1.a.h1.a.h1
P Q : Formula
⊢ IsProof (Q.imp_ Q.not_.not_)
Theorem: FOL.NV.T_14_7
Proof state before:
case h1.a.h1.a.h1
P Q : Formula
⊢ IsProof (Q.imp_ Q.not_.not_)
Tactic:
apply T_14_6
Proof state after:
no goals
Theorem: FOL.NV.T_14_7
Proof state before:
case h1.a.h1.a
P Q : Formula
⊢ IsDeduct (∅ ∪ {P.imp_ Q} ∪ {P.not_.not_}) Q
Tactic:
apply IsDeduct.mp_ P
Proof state after:
case h1.a.h1.a.a
P Q : Formula
⊢ IsDeduct (∅ ∪ {P.imp_ Q} ∪ {P.not_.not_}) (P.imp_ Q)

case h1.a.h1.a.a
P Q : Formula
⊢ IsDeduct (∅ ∪ {P.imp_ Q} ∪ {P.not_.not_}) P
Theorem: FOL.NV.T_14_7
Proof state before:
case h1.a.h1.a.a
P Q : Formula
⊢ IsDeduct (∅ ∪ {P.imp_ Q} ∪ {P.not_.not_}) (P.imp_ Q)
Tactic:
apply IsDeduct.assume_
Proof state after:
case h1.a.h1.a.a.a
P Q : Formula
⊢ P.imp_ Q ∈ ∅ ∪ {P.imp_ Q} ∪ {P.not_.not_}
Theorem: FOL.NV.T_14_7
Proof state before:
case h1.a.h1.a.a.a
P Q : Formula
⊢ P.imp_ Q ∈ ∅ ∪ {P.imp_ Q} ∪ {P.not_.not_}
Tactic:
simp
Proof state after:
no goals
Theorem: FOL.NV.T_14_7
Proof state before:
case h1.a.h1.a.a
P Q : Formula
⊢ IsDeduct (∅ ∪ {P.imp_ Q} ∪ {P.not_.not_}) P
Tactic:
apply IsDeduct.mp_ P.not_.not_
Proof state after:
case h1.a.h1.a.a.a
P Q : Formula
⊢ IsDeduct (∅ ∪ {P.imp_ Q} ∪ {P.not_.not_}) (P.not_.not_.imp_ P)

case h1.a.h1.a.a.a
P Q : Formula
⊢ IsDeduct (∅ ∪ {P.imp_ Q} ∪ {P.not_.not_}) P.not_.not_
Theorem: FOL.NV.T_14_7
Proof state before:
case h1.a.h1.a.a.a
P Q : Formula
⊢ IsDeduct (∅ ∪ {P.imp_ Q} ∪ {P.not_.not_}) (P.not_.not_.imp_ P)
Tactic:
apply proof_imp_deduct
Proof state after:
case h1.a.h1.a.a.a.h1
P Q : Formula
⊢ IsProof (P.not_.not_.imp_ P)
Theorem: FOL.NV.T_14_7
Proof state before:
case h1.a.h1.a.a.a.h1
P Q : Formula
⊢ IsProof (P.not_.not_.imp_ P)
Tactic:
apply T_14_5
Proof state after:
no goals
Theorem: FOL.NV.T_14_7
Proof state before:
case h1.a.h1.a.a.a
P Q : Formula
⊢ IsDeduct (∅ ∪ {P.imp_ Q} ∪ {P.not_.not_}) P.not_.not_
Tactic:
apply IsDeduct.assume_
Proof state after:
case h1.a.h1.a.a.a.a
P Q : Formula
⊢ P.not_.not_ ∈ ∅ ∪ {P.imp_ Q} ∪ {P.not_.not_}
Theorem: FOL.NV.T_14_7
Proof state before:
case h1.a.h1.a.a.a.a
P Q : Formula
⊢ P.not_.not_ ∈ ∅ ∪ {P.imp_ Q} ∪ {P.not_.not_}
Tactic:
simp
Proof state after:
no goals
Theorem: FOL.NV.T_14_8
Proof state before:
Q R : Formula
⊢ IsProof (Q.imp_ (R.not_.imp_ (Q.imp_ R).not_))
Tactic:
simp only [IsProof]
Proof state after:
Q R : Formula
⊢ IsDeduct ∅ (Q.imp_ (R.not_.imp_ (Q.imp_ R).not_))
Theorem: FOL.NV.T_14_8
Proof state before:
Q R : Formula
⊢ IsDeduct ∅ (Q.imp_ (R.not_.imp_ (Q.imp_ R).not_))
Tactic:
apply deduction_theorem
Proof state after:
case h1
Q R : Formula
⊢ IsDeduct (∅ ∪ {Q}) (R.not_.imp_ (Q.imp_ R).not_)
Theorem: FOL.NV.T_14_8
Proof state before:
case h1
Q R : Formula
⊢ IsDeduct (∅ ∪ {Q}) (R.not_.imp_ (Q.imp_ R).not_)
Tactic:
apply IsDeduct.mp_ ((Q.imp_ R).imp_ R)
Proof state after:
case h1.a
Q R : Formula
⊢ IsDeduct (∅ ∪ {Q}) (((Q.imp_ R).imp_ R).imp_ (R.not_.imp_ (Q.imp_ R).not_))

case h1.a
Q R : Formula
⊢ IsDeduct (∅ ∪ {Q}) ((Q.imp_ R).imp_ R)
Theorem: FOL.NV.T_14_8
Proof state before:
case h1.a
Q R : Formula
⊢ IsDeduct (∅ ∪ {Q}) (((Q.imp_ R).imp_ R).imp_ (R.not_.imp_ (Q.imp_ R).not_))
Tactic:
apply proof_imp_deduct
Proof state after:
case h1.a.h1
Q R : Formula
⊢ IsProof (((Q.imp_ R).imp_ R).imp_ (R.not_.imp_ (Q.imp_ R).not_))
Theorem: FOL.NV.T_14_8
Proof state before:
case h1.a.h1
Q R : Formula
⊢ IsProof (((Q.imp_ R).imp_ R).imp_ (R.not_.imp_ (Q.imp_ R).not_))
Tactic:
apply T_14_7
Proof state after:
no goals
Theorem: FOL.NV.T_14_8
Proof state before:
case h1.a
Q R : Formula
⊢ IsDeduct (∅ ∪ {Q}) ((Q.imp_ R).imp_ R)
Tactic:
apply deduction_theorem
Proof state after:
case h1.a.h1
Q R : Formula
⊢ IsDeduct (∅ ∪ {Q} ∪ {Q.imp_ R}) R
Theorem: FOL.NV.T_14_8
Proof state before:
case h1.a.h1
Q R : Formula
⊢ IsDeduct (∅ ∪ {Q} ∪ {Q.imp_ R}) R
Tactic:
apply IsDeduct.mp_ Q
Proof state after:
case h1.a.h1.a
Q R : Formula
⊢ IsDeduct (∅ ∪ {Q} ∪ {Q.imp_ R}) (Q.imp_ R)

case h1.a.h1.a
Q R : Formula
⊢ IsDeduct (∅ ∪ {Q} ∪ {Q.imp_ R}) Q
Theorem: FOL.NV.T_14_8
Proof state before:
case h1.a.h1.a
Q R : Formula
⊢ IsDeduct (∅ ∪ {Q} ∪ {Q.imp_ R}) (Q.imp_ R)
Tactic:
apply IsDeduct.assume_
Proof state after:
case h1.a.h1.a.a
Q R : Formula
⊢ Q.imp_ R ∈ ∅ ∪ {Q} ∪ {Q.imp_ R}
Theorem: FOL.NV.T_14_8
Proof state before:
case h1.a.h1.a.a
Q R : Formula
⊢ Q.imp_ R ∈ ∅ ∪ {Q} ∪ {Q.imp_ R}
Tactic:
simp
Proof state after:
no goals
Theorem: FOL.NV.T_14_8
Proof state before:
case h1.a.h1.a
Q R : Formula
⊢ IsDeduct (∅ ∪ {Q} ∪ {Q.imp_ R}) Q
Tactic:
apply IsDeduct.assume_
Proof state after:
case h1.a.h1.a.a
Q R : Formula
⊢ Q ∈ ∅ ∪ {Q} ∪ {Q.imp_ R}
Theorem: FOL.NV.T_14_8
Proof state before:
case h1.a.h1.a.a
Q R : Formula
⊢ Q ∈ ∅ ∪ {Q} ∪ {Q.imp_ R}
Tactic:
simp
Proof state after:
no goals
Theorem: FOL.NV.T_14_9
Proof state before:
P S : Formula
⊢ IsProof ((S.imp_ P).imp_ ((S.not_.imp_ P).imp_ P))
Tactic:
simp only [IsProof]
Proof state after:
P S : Formula
⊢ IsDeduct ∅ ((S.imp_ P).imp_ ((S.not_.imp_ P).imp_ P))
Theorem: FOL.NV.T_14_9
Proof state before:
P S : Formula
⊢ IsDeduct ∅ ((S.imp_ P).imp_ ((S.not_.imp_ P).imp_ P))
Tactic:
apply deduction_theorem
Proof state after:
case h1
P S : Formula
⊢ IsDeduct (∅ ∪ {S.imp_ P}) ((S.not_.imp_ P).imp_ P)
Theorem: FOL.NV.T_14_9
Proof state before:
case h1
P S : Formula
⊢ IsDeduct (∅ ∪ {S.imp_ P}) ((S.not_.imp_ P).imp_ P)
Tactic:
apply IsDeduct.mp_ (P.not_.imp_ (S.not_.imp_ P).not_)
Proof state after:
case h1.a
P S : Formula
⊢ IsDeduct (∅ ∪ {S.imp_ P}) ((P.not_.imp_ (S.not_.imp_ P).not_).imp_ ((S.not_.imp_ P).imp_ P))

case h1.a
P S : Formula
⊢ IsDeduct (∅ ∪ {S.imp_ P}) (P.not_.imp_ (S.not_.imp_ P).not_)
Theorem: FOL.NV.T_14_9
Proof state before:
case h1.a
P S : Formula
⊢ IsDeduct (∅ ∪ {S.imp_ P}) ((P.not_.imp_ (S.not_.imp_ P).not_).imp_ ((S.not_.imp_ P).imp_ P))
Tactic:
apply IsDeduct.axiom_
Proof state after:
case h1.a.a
P S : Formula
⊢ IsAxiom ((P.not_.imp_ (S.not_.imp_ P).not_).imp_ ((S.not_.imp_ P).imp_ P))
Theorem: FOL.NV.T_14_9
Proof state before:
case h1.a.a
P S : Formula
⊢ IsAxiom ((P.not_.imp_ (S.not_.imp_ P).not_).imp_ ((S.not_.imp_ P).imp_ P))
Tactic:
apply IsAxiom.prop_3_
Proof state after:
no goals
Theorem: FOL.NV.T_14_9
Proof state before:
case h1.a
P S : Formula
⊢ IsDeduct (∅ ∪ {S.imp_ P}) (P.not_.imp_ (S.not_.imp_ P).not_)
Tactic:
apply deduction_theorem
Proof state after:
case h1.a.h1
P S : Formula
⊢ IsDeduct (∅ ∪ {S.imp_ P} ∪ {P.not_}) (S.not_.imp_ P).not_
Theorem: FOL.NV.T_14_9
Proof state before:
case h1.a.h1
P S : Formula
⊢ IsDeduct (∅ ∪ {S.imp_ P} ∪ {P.not_}) (S.not_.imp_ P).not_
Tactic:
apply IsDeduct.mp_ P.not_
Proof state after:
case h1.a.h1.a
P S : Formula
⊢ IsDeduct (∅ ∪ {S.imp_ P} ∪ {P.not_}) (P.not_.imp_ (S.not_.imp_ P).not_)

case h1.a.h1.a
P S : Formula
⊢ IsDeduct (∅ ∪ {S.imp_ P} ∪ {P.not_}) P.not_