internlm/Lean-Github huggingface dataset:
Theorem: FOL.NV.L_15_7
Proof state before:
Δ_U : Set Formula
V : VarBoolAssignment
h1 : ↑true_.primeSet ⊆ Δ_U
⊢ IsDeduct (evalPrimeFfToNot V '' Δ_U) (evalPrimeFfToNot V true_)
Tactic:
apply IsDeduct.axiom_
Proof state after:
case a
Δ_U : Set Formula
V : VarBoolAssignment
h1 : ↑true_.primeSet ⊆ Δ_U
⊢ IsAxiom (evalPrimeFfToNot V true_)
Theorem: FOL.NV.L_15_7
Proof state before:
case a
Δ_U : Set Formula
V : VarBoolAssignment
h1 : ↑true_.primeSet ⊆ Δ_U
⊢ IsAxiom (evalPrimeFfToNot V true_)
Tactic:
apply IsAxiom.prop_true_
Proof state after:
no goals
Theorem: FOL.NV.L_15_7
Proof state before:
Δ_U : Set Formula
V : VarBoolAssignment
h1 : ↑false_.primeSet ⊆ Δ_U
⊢ IsDeduct (evalPrimeFfToNot V '' Δ_U) (evalPrimeFfToNot V false_)
Tactic:
simp only [Formula.primeSet] at h1
Proof state after:
Δ_U : Set Formula
V : VarBoolAssignment
h1 : ↑∅ ⊆ Δ_U
⊢ IsDeduct (evalPrimeFfToNot V '' Δ_U) (evalPrimeFfToNot V false_)
Theorem: FOL.NV.L_15_7
Proof state before:
Δ_U : Set Formula
V : VarBoolAssignment
h1 : ↑∅ ⊆ Δ_U
⊢ IsDeduct (evalPrimeFfToNot V '' Δ_U) (evalPrimeFfToNot V false_)
Tactic:
simp at h1
Proof state after:
Δ_U : Set Formula
V : VarBoolAssignment
h1 : True
⊢ IsDeduct (evalPrimeFfToNot V '' Δ_U) (evalPrimeFfToNot V false_)
Theorem: FOL.NV.L_15_7
Proof state before:
Δ_U : Set Formula
V : VarBoolAssignment
h1 : True
⊢ IsDeduct (evalPrimeFfToNot V '' Δ_U) (evalPrimeFfToNot V false_)
Tactic:
simp only [evalPrimeFfToNot]
Proof state after:
Δ_U : Set Formula
V : VarBoolAssignment
h1 : True
⊢ IsDeduct ((fun a => if evalPrime V a then a else a.not_) '' Δ_U) (if evalPrime V false_ then false_ else false_.not_)
Theorem: FOL.NV.L_15_7
Proof state before:
Δ_U : Set Formula
V : VarBoolAssignment
h1 : True
⊢ IsDeduct ((fun a => if evalPrime V a then a else a.not_) '' Δ_U) (if evalPrime V false_ then false_ else false_.not_)
Tactic:
simp only [Formula.evalPrime]
Proof state after:
Δ_U : Set Formula
V : VarBoolAssignment
h1 : True
⊢ IsDeduct ((fun a => if evalPrime V a then a else a.not_) '' Δ_U) (if False then false_ else false_.not_)
Theorem: FOL.NV.L_15_7
Proof state before:
Δ_U : Set Formula
V : VarBoolAssignment
h1 : True
⊢ IsDeduct ((fun a => if evalPrime V a then a else a.not_) '' Δ_U) (if False then false_ else false_.not_)
Tactic:
simp
Proof state after:
Δ_U : Set Formula
V : VarBoolAssignment
h1 : True
⊢ IsDeduct ((fun a => if evalPrime V a then a else a.not_) '' Δ_U) false_.not_
Theorem: FOL.NV.L_15_7
Proof state before:
Δ_U : Set Formula
V : VarBoolAssignment
h1 : True
⊢ IsDeduct ((fun a => if evalPrime V a then a else a.not_) '' Δ_U) false_.not_
Tactic:
sorry
Proof state after:
no goals
Theorem: FOL.NV.L_15_7
Proof state before:
Δ_U : Set Formula
V : VarBoolAssignment
phi : Formula
phi_ih : ↑phi.primeSet ⊆ Δ_U → IsDeduct (evalPrimeFfToNot V '' Δ_U) (evalPrimeFfToNot V phi)
h1 : ↑phi.not_.primeSet ⊆ Δ_U
⊢ IsDeduct (evalPrimeFfToNot V '' Δ_U) (evalPrimeFfToNot V phi.not_)
Tactic:
simp only [Formula.primeSet] at h1
Proof state after:
Δ_U : Set Formula
V : VarBoolAssignment
phi : Formula
phi_ih : ↑phi.primeSet ⊆ Δ_U → IsDeduct (evalPrimeFfToNot V '' Δ_U) (evalPrimeFfToNot V phi)
h1 : ↑phi.primeSet ⊆ Δ_U
⊢ IsDeduct (evalPrimeFfToNot V '' Δ_U) (evalPrimeFfToNot V phi.not_)
Theorem: FOL.NV.L_15_7
Proof state before:
Δ_U : Set Formula
V : VarBoolAssignment
phi : Formula
phi_ih : ↑phi.primeSet ⊆ Δ_U → IsDeduct (evalPrimeFfToNot V '' Δ_U) (evalPrimeFfToNot V phi)
h1 : ↑phi.primeSet ⊆ Δ_U
⊢ IsDeduct (evalPrimeFfToNot V '' Δ_U) (evalPrimeFfToNot V phi.not_)
Tactic:
simp only [evalPrimeFfToNot] at phi_ih
Proof state after:
Δ_U : Set Formula
V : VarBoolAssignment
phi : Formula
h1 : ↑phi.primeSet ⊆ Δ_U
phi_ih :
  ↑phi.primeSet ⊆ Δ_U →
    IsDeduct ((fun a => if evalPrime V a then a else a.not_) '' Δ_U) (if evalPrime V phi then phi else phi.not_)
⊢ IsDeduct (evalPrimeFfToNot V '' Δ_U) (evalPrimeFfToNot V phi.not_)
Theorem: FOL.NV.L_15_7
Proof state before:
Δ_U : Set Formula
V : VarBoolAssignment
phi : Formula
h1 : ↑phi.primeSet ⊆ Δ_U
phi_ih :
  ↑phi.primeSet ⊆ Δ_U →
    IsDeduct ((fun a => if evalPrime V a then a else a.not_) '' Δ_U) (if evalPrime V phi then phi else phi.not_)
⊢ IsDeduct (evalPrimeFfToNot V '' Δ_U) (evalPrimeFfToNot V phi.not_)
Tactic:
simp only [evalPrimeFfToNot]
Proof state after:
Δ_U : Set Formula
V : VarBoolAssignment
phi : Formula
h1 : ↑phi.primeSet ⊆ Δ_U
phi_ih :
  ↑phi.primeSet ⊆ Δ_U →
    IsDeduct ((fun a => if evalPrime V a then a else a.not_) '' Δ_U) (if evalPrime V phi then phi else phi.not_)
⊢ IsDeduct ((fun a => if evalPrime V a then a else a.not_) '' Δ_U)
    (if evalPrime V phi.not_ then phi.not_ else phi.not_.not_)
Theorem: FOL.NV.L_15_7
Proof state before:
Δ_U : Set Formula
V : VarBoolAssignment
phi : Formula
h1 : ↑phi.primeSet ⊆ Δ_U
phi_ih :
  ↑phi.primeSet ⊆ Δ_U →
    IsDeduct ((fun a => if evalPrime V a then a else a.not_) '' Δ_U) (if evalPrime V phi then phi else phi.not_)
⊢ IsDeduct ((fun a => if evalPrime V a then a else a.not_) '' Δ_U)
    (if evalPrime V phi.not_ then phi.not_ else phi.not_.not_)
Tactic:
simp only [evalPrime]
Proof state after:
Δ_U : Set Formula
V : VarBoolAssignment
phi : Formula
h1 : ↑phi.primeSet ⊆ Δ_U
phi_ih :
  ↑phi.primeSet ⊆ Δ_U →
    IsDeduct ((fun a => if evalPrime V a then a else a.not_) '' Δ_U) (if evalPrime V phi then phi else phi.not_)
⊢ IsDeduct ((fun a => if evalPrime V a then a else a.not_) '' Δ_U)
    (if ¬evalPrime V phi then phi.not_ else phi.not_.not_)
Theorem: FOL.NV.L_15_7
Proof state before:
Δ_U : Set Formula
V : VarBoolAssignment
phi : Formula
h1 : ↑phi.primeSet ⊆ Δ_U
phi_ih :
  ↑phi.primeSet ⊆ Δ_U →
    IsDeduct ((fun a => if evalPrime V a then a else a.not_) '' Δ_U) (if evalPrime V phi then phi else phi.not_)
⊢ IsDeduct ((fun a => if evalPrime V a then a else a.not_) '' Δ_U)
    (if ¬evalPrime V phi then phi.not_ else phi.not_.not_)
Tactic:
simp
Proof state after:
Δ_U : Set Formula
V : VarBoolAssignment
phi : Formula
h1 : ↑phi.primeSet ⊆ Δ_U
phi_ih :
  ↑phi.primeSet ⊆ Δ_U →
    IsDeduct ((fun a => if evalPrime V a then a else a.not_) '' Δ_U) (if evalPrime V phi then phi else phi.not_)
⊢ IsDeduct ((fun a => if evalPrime V a then a else a.not_) '' Δ_U) (if evalPrime V phi then phi.not_.not_ else phi.not_)
Theorem: FOL.NV.L_15_7
Proof state before:
Δ_U : Set Formula
V : VarBoolAssignment
phi : Formula
h1 : ↑phi.primeSet ⊆ Δ_U
phi_ih :
  ↑phi.primeSet ⊆ Δ_U →
    IsDeduct ((fun a => if evalPrime V a then a else a.not_) '' Δ_U) (if evalPrime V phi then phi else phi.not_)
⊢ IsDeduct ((fun a => if evalPrime V a then a else a.not_) '' Δ_U) (if evalPrime V phi then phi.not_.not_ else phi.not_)
Tactic:
split_ifs
Proof state after:
case pos
Δ_U : Set Formula
V : VarBoolAssignment
phi : Formula
h1 : ↑phi.primeSet ⊆ Δ_U
phi_ih :
  ↑phi.primeSet ⊆ Δ_U →
    IsDeduct ((fun a => if evalPrime V a then a else a.not_) '' Δ_U) (if evalPrime V phi then phi else phi.not_)
h✝ : evalPrime V phi
⊢ IsDeduct ((fun a => if evalPrime V a then a else a.not_) '' Δ_U) phi.not_.not_

case neg
Δ_U : Set Formula
V : VarBoolAssignment
phi : Formula
h1 : ↑phi.primeSet ⊆ Δ_U
phi_ih :
  ↑phi.primeSet ⊆ Δ_U →
    IsDeduct ((fun a => if evalPrime V a then a else a.not_) '' Δ_U) (if evalPrime V phi then phi else phi.not_)
h✝ : ¬evalPrime V phi
⊢ IsDeduct ((fun a => if evalPrime V a then a else a.not_) '' Δ_U) phi.not_
Theorem: FOL.NV.L_15_7
Proof state before:
Δ_U : Set Formula
V : VarBoolAssignment
phi : Formula
h1 : ↑phi.primeSet ⊆ Δ_U
phi_ih :
  ↑phi.primeSet ⊆ Δ_U →
    IsDeduct ((fun a => if evalPrime V a then a else a.not_) '' Δ_U) (if evalPrime V phi then phi else phi.not_)
c1 : evalPrime V phi
⊢ IsDeduct ((fun a => if evalPrime V a then a else a.not_) '' Δ_U) phi.not_.not_
Tactic:
case _ c1 =>
  simp only [c1] at phi_ih
  simp at phi_ih
  apply IsDeduct.mp_ phi
  apply proof_imp_deduct
  apply T_14_6
  exact phi_ih h1
Proof state after:
no goals
Theorem: FOL.NV.L_15_7
Proof state before:
Δ_U : Set Formula
V : VarBoolAssignment
phi : Formula
h1 : ↑phi.primeSet ⊆ Δ_U
phi_ih :
  ↑phi.primeSet ⊆ Δ_U →
    IsDeduct ((fun a => if evalPrime V a then a else a.not_) '' Δ_U) (if evalPrime V phi then phi else phi.not_)
c1 : ¬evalPrime V phi
⊢ IsDeduct ((fun a => if evalPrime V a then a else a.not_) '' Δ_U) phi.not_
Tactic:
case _ c1 =>
  simp only [c1] at phi_ih
  simp at phi_ih
  exact phi_ih h1
Proof state after:
no goals
Theorem: FOL.NV.L_15_7
Proof state before:
Δ_U : Set Formula
V : VarBoolAssignment
phi : Formula
h1 : ↑phi.primeSet ⊆ Δ_U
phi_ih :
  ↑phi.primeSet ⊆ Δ_U →
    IsDeduct ((fun a => if evalPrime V a then a else a.not_) '' Δ_U) (if evalPrime V phi then phi else phi.not_)
c1 : evalPrime V phi
⊢ IsDeduct ((fun a => if evalPrime V a then a else a.not_) '' Δ_U) phi.not_.not_
Tactic:
simp only [c1] at phi_ih
Proof state after:
Δ_U : Set Formula
V : VarBoolAssignment
phi : Formula
h1 : ↑phi.primeSet ⊆ Δ_U
c1 : evalPrime V phi
phi_ih :
  ↑phi.primeSet ⊆ Δ_U →
    IsDeduct ((fun a => if evalPrime V a then a else a.not_) '' Δ_U) (if True then phi else phi.not_)
⊢ IsDeduct ((fun a => if evalPrime V a then a else a.not_) '' Δ_U) phi.not_.not_
Theorem: FOL.NV.L_15_7
Proof state before:
Δ_U : Set Formula
V : VarBoolAssignment
phi : Formula
h1 : ↑phi.primeSet ⊆ Δ_U
c1 : evalPrime V phi
phi_ih :
  ↑phi.primeSet ⊆ Δ_U →
    IsDeduct ((fun a => if evalPrime V a then a else a.not_) '' Δ_U) (if True then phi else phi.not_)
⊢ IsDeduct ((fun a => if evalPrime V a then a else a.not_) '' Δ_U) phi.not_.not_
Tactic:
simp at phi_ih
Proof state after:
Δ_U : Set Formula
V : VarBoolAssignment
phi : Formula
h1 : ↑phi.primeSet ⊆ Δ_U
c1 : evalPrime V phi
phi_ih : ↑phi.primeSet ⊆ Δ_U → IsDeduct ((fun a => if evalPrime V a then a else a.not_) '' Δ_U) phi
⊢ IsDeduct ((fun a => if evalPrime V a then a else a.not_) '' Δ_U) phi.not_.not_
Theorem: FOL.NV.L_15_7
Proof state before:
Δ_U : Set Formula
V : VarBoolAssignment
phi : Formula
h1 : ↑phi.primeSet ⊆ Δ_U
c1 : evalPrime V phi
phi_ih : ↑phi.primeSet ⊆ Δ_U → IsDeduct ((fun a => if evalPrime V a then a else a.not_) '' Δ_U) phi
⊢ IsDeduct ((fun a => if evalPrime V a then a else a.not_) '' Δ_U) phi.not_.not_
Tactic:
apply IsDeduct.mp_ phi
Proof state after:
case a
Δ_U : Set Formula
V : VarBoolAssignment
phi : Formula
h1 : ↑phi.primeSet ⊆ Δ_U
c1 : evalPrime V phi
phi_ih : ↑phi.primeSet ⊆ Δ_U → IsDeduct ((fun a => if evalPrime V a then a else a.not_) '' Δ_U) phi
⊢ IsDeduct ((fun a => if evalPrime V a then a else a.not_) '' Δ_U) (phi.imp_ phi.not_.not_)

case a
Δ_U : Set Formula
V : VarBoolAssignment
phi : Formula
h1 : ↑phi.primeSet ⊆ Δ_U
c1 : evalPrime V phi
phi_ih : ↑phi.primeSet ⊆ Δ_U → IsDeduct ((fun a => if evalPrime V a then a else a.not_) '' Δ_U) phi
⊢ IsDeduct ((fun a => if evalPrime V a then a else a.not_) '' Δ_U) phi
Theorem: FOL.NV.L_15_7
Proof state before:
case a
Δ_U : Set Formula
V : VarBoolAssignment
phi : Formula
h1 : ↑phi.primeSet ⊆ Δ_U
c1 : evalPrime V phi
phi_ih : ↑phi.primeSet ⊆ Δ_U → IsDeduct ((fun a => if evalPrime V a then a else a.not_) '' Δ_U) phi
⊢ IsDeduct ((fun a => if evalPrime V a then a else a.not_) '' Δ_U) (phi.imp_ phi.not_.not_)

case a
Δ_U : Set Formula
V : VarBoolAssignment
phi : Formula
h1 : ↑phi.primeSet ⊆ Δ_U
c1 : evalPrime V phi
phi_ih : ↑phi.primeSet ⊆ Δ_U → IsDeduct ((fun a => if evalPrime V a then a else a.not_) '' Δ_U) phi
⊢ IsDeduct ((fun a => if evalPrime V a then a else a.not_) '' Δ_U) phi
Tactic:
apply proof_imp_deduct
Proof state after:
case a.h1
Δ_U : Set Formula
V : VarBoolAssignment
phi : Formula
h1 : ↑phi.primeSet ⊆ Δ_U
c1 : evalPrime V phi
phi_ih : ↑phi.primeSet ⊆ Δ_U → IsDeduct ((fun a => if evalPrime V a then a else a.not_) '' Δ_U) phi
⊢ IsProof (phi.imp_ phi.not_.not_)

case a
Δ_U : Set Formula
V : VarBoolAssignment
phi : Formula
h1 : ↑phi.primeSet ⊆ Δ_U
c1 : evalPrime V phi
phi_ih : ↑phi.primeSet ⊆ Δ_U → IsDeduct ((fun a => if evalPrime V a then a else a.not_) '' Δ_U) phi
⊢ IsDeduct ((fun a => if evalPrime V a then a else a.not_) '' Δ_U) phi
Theorem: FOL.NV.L_15_7
Proof state before:
case a.h1
Δ_U : Set Formula
V : VarBoolAssignment
phi : Formula
h1 : ↑phi.primeSet ⊆ Δ_U
c1 : evalPrime V phi
phi_ih : ↑phi.primeSet ⊆ Δ_U → IsDeduct ((fun a => if evalPrime V a then a else a.not_) '' Δ_U) phi
⊢ IsProof (phi.imp_ phi.not_.not_)

case a
Δ_U : Set Formula
V : VarBoolAssignment
phi : Formula
h1 : ↑phi.primeSet ⊆ Δ_U
c1 : evalPrime V phi
phi_ih : ↑phi.primeSet ⊆ Δ_U → IsDeduct ((fun a => if evalPrime V a then a else a.not_) '' Δ_U) phi
⊢ IsDeduct ((fun a => if evalPrime V a then a else a.not_) '' Δ_U) phi
Tactic:
apply T_14_6
Proof state after:
case a
Δ_U : Set Formula
V : VarBoolAssignment
phi : Formula
h1 : ↑phi.primeSet ⊆ Δ_U
c1 : evalPrime V phi
phi_ih : ↑phi.primeSet ⊆ Δ_U → IsDeduct ((fun a => if evalPrime V a then a else a.not_) '' Δ_U) phi
⊢ IsDeduct ((fun a => if evalPrime V a then a else a.not_) '' Δ_U) phi
Theorem: FOL.NV.L_15_7
Proof state before:
case a
Δ_U : Set Formula
V : VarBoolAssignment
phi : Formula
h1 : ↑phi.primeSet ⊆ Δ_U
c1 : evalPrime V phi
phi_ih : ↑phi.primeSet ⊆ Δ_U → IsDeduct ((fun a => if evalPrime V a then a else a.not_) '' Δ_U) phi
⊢ IsDeduct ((fun a => if evalPrime V a then a else a.not_) '' Δ_U) phi
Tactic:
exact phi_ih h1
Proof state after:
no goals
Theorem: FOL.NV.L_15_7
Proof state before:
Δ_U : Set Formula
V : VarBoolAssignment
phi : Formula
h1 : ↑phi.primeSet ⊆ Δ_U
phi_ih :
  ↑phi.primeSet ⊆ Δ_U →
    IsDeduct ((fun a => if evalPrime V a then a else a.not_) '' Δ_U) (if evalPrime V phi then phi else phi.not_)
c1 : ¬evalPrime V phi
⊢ IsDeduct ((fun a => if evalPrime V a then a else a.not_) '' Δ_U) phi.not_
Tactic:
simp only [c1] at phi_ih
Proof state after:
Δ_U : Set Formula
V : VarBoolAssignment
phi : Formula
h1 : ↑phi.primeSet ⊆ Δ_U
c1 : ¬evalPrime V phi
phi_ih :
  ↑phi.primeSet ⊆ Δ_U →
    IsDeduct ((fun a => if evalPrime V a then a else a.not_) '' Δ_U) (if False then phi else phi.not_)
⊢ IsDeduct ((fun a => if evalPrime V a then a else a.not_) '' Δ_U) phi.not_
Theorem: FOL.NV.L_15_7
Proof state before:
Δ_U : Set Formula
V : VarBoolAssignment
phi : Formula
h1 : ↑phi.primeSet ⊆ Δ_U
c1 : ¬evalPrime V phi
phi_ih :
  ↑phi.primeSet ⊆ Δ_U →
    IsDeduct ((fun a => if evalPrime V a then a else a.not_) '' Δ_U) (if False then phi else phi.not_)
⊢ IsDeduct ((fun a => if evalPrime V a then a else a.not_) '' Δ_U) phi.not_
Tactic:
simp at phi_ih
Proof state after:
Δ_U : Set Formula
V : VarBoolAssignment
phi : Formula
h1 : ↑phi.primeSet ⊆ Δ_U
c1 : ¬evalPrime V phi
phi_ih : ↑phi.primeSet ⊆ Δ_U → IsDeduct ((fun a => if evalPrime V a then a else a.not_) '' Δ_U) phi.not_
⊢ IsDeduct ((fun a => if evalPrime V a then a else a.not_) '' Δ_U) phi.not_
Theorem: FOL.NV.L_15_7
Proof state before:
Δ_U : Set Formula
V : VarBoolAssignment
phi : Formula
h1 : ↑phi.primeSet ⊆ Δ_U
c1 : ¬evalPrime V phi
phi_ih : ↑phi.primeSet ⊆ Δ_U → IsDeduct ((fun a => if evalPrime V a then a else a.not_) '' Δ_U) phi.not_
⊢ IsDeduct ((fun a => if evalPrime V a then a else a.not_) '' Δ_U) phi.not_
Tactic:
exact phi_ih h1
Proof state after:
no goals
Theorem: FOL.NV.L_15_7
Proof state before:
Δ_U : Set Formula
V : VarBoolAssignment
phi psi : Formula
phi_ih : ↑phi.primeSet ⊆ Δ_U → IsDeduct (evalPrimeFfToNot V '' Δ_U) (evalPrimeFfToNot V phi)
psi_ih : ↑psi.primeSet ⊆ Δ_U → IsDeduct (evalPrimeFfToNot V '' Δ_U) (evalPrimeFfToNot V psi)
h1 : ↑(phi.imp_ psi).primeSet ⊆ Δ_U
⊢ IsDeduct (evalPrimeFfToNot V '' Δ_U) (evalPrimeFfToNot V (phi.imp_ psi))
Tactic:
simp only [Formula.primeSet] at h1
Proof state after:
Δ_U : Set Formula
V : VarBoolAssignment
phi psi : Formula
phi_ih : ↑phi.primeSet ⊆ Δ_U → IsDeduct (evalPrimeFfToNot V '' Δ_U) (evalPrimeFfToNot V phi)
psi_ih : ↑psi.primeSet ⊆ Δ_U → IsDeduct (evalPrimeFfToNot V '' Δ_U) (evalPrimeFfToNot V psi)
h1 : ↑(phi.primeSet ∪ psi.primeSet) ⊆ Δ_U
⊢ IsDeduct (evalPrimeFfToNot V '' Δ_U) (evalPrimeFfToNot V (phi.imp_ psi))
Theorem: FOL.NV.L_15_7
Proof state before:
Δ_U : Set Formula
V : VarBoolAssignment
phi psi : Formula
phi_ih : ↑phi.primeSet ⊆ Δ_U → IsDeduct (evalPrimeFfToNot V '' Δ_U) (evalPrimeFfToNot V phi)
psi_ih : ↑psi.primeSet ⊆ Δ_U → IsDeduct (evalPrimeFfToNot V '' Δ_U) (evalPrimeFfToNot V psi)
h1 : ↑(phi.primeSet ∪ psi.primeSet) ⊆ Δ_U
⊢ IsDeduct (evalPrimeFfToNot V '' Δ_U) (evalPrimeFfToNot V (phi.imp_ psi))
Tactic:
simp at h1
Proof state after:
Δ_U : Set Formula
V : VarBoolAssignment
phi psi : Formula
phi_ih : ↑phi.primeSet ⊆ Δ_U → IsDeduct (evalPrimeFfToNot V '' Δ_U) (evalPrimeFfToNot V phi)
psi_ih : ↑psi.primeSet ⊆ Δ_U → IsDeduct (evalPrimeFfToNot V '' Δ_U) (evalPrimeFfToNot V psi)
h1 : ↑phi.primeSet ⊆ Δ_U ∧ ↑psi.primeSet ⊆ Δ_U
⊢ IsDeduct (evalPrimeFfToNot V '' Δ_U) (evalPrimeFfToNot V (phi.imp_ psi))
Theorem: FOL.NV.L_15_7
Proof state before:
Δ_U : Set Formula
V : VarBoolAssignment
phi psi : Formula
phi_ih : ↑phi.primeSet ⊆ Δ_U → IsDeduct (evalPrimeFfToNot V '' Δ_U) (evalPrimeFfToNot V phi)
psi_ih : ↑psi.primeSet ⊆ Δ_U → IsDeduct (evalPrimeFfToNot V '' Δ_U) (evalPrimeFfToNot V psi)
h1 : ↑phi.primeSet ⊆ Δ_U ∧ ↑psi.primeSet ⊆ Δ_U
⊢ IsDeduct (evalPrimeFfToNot V '' Δ_U) (evalPrimeFfToNot V (phi.imp_ psi))
Tactic:
simp only [evalPrimeFfToNot] at phi_ih
Proof state after:
Δ_U : Set Formula
V : VarBoolAssignment
phi psi : Formula
psi_ih : ↑psi.primeSet ⊆ Δ_U → IsDeduct (evalPrimeFfToNot V '' Δ_U) (evalPrimeFfToNot V psi)
h1 : ↑phi.primeSet ⊆ Δ_U ∧ ↑psi.primeSet ⊆ Δ_U
phi_ih :
  ↑phi.primeSet ⊆ Δ_U →
    IsDeduct ((fun a => if evalPrime V a then a else a.not_) '' Δ_U) (if evalPrime V phi then phi else phi.not_)
⊢ IsDeduct (evalPrimeFfToNot V '' Δ_U) (evalPrimeFfToNot V (phi.imp_ psi))
Theorem: FOL.NV.L_15_7
Proof state before:
Δ_U : Set Formula
V : VarBoolAssignment
phi psi : Formula
psi_ih : ↑psi.primeSet ⊆ Δ_U → IsDeduct (evalPrimeFfToNot V '' Δ_U) (evalPrimeFfToNot V psi)
h1 : ↑phi.primeSet ⊆ Δ_U ∧ ↑psi.primeSet ⊆ Δ_U
phi_ih :
  ↑phi.primeSet ⊆ Δ_U →
    IsDeduct ((fun a => if evalPrime V a then a else a.not_) '' Δ_U) (if evalPrime V phi then phi else phi.not_)
⊢ IsDeduct (evalPrimeFfToNot V '' Δ_U) (evalPrimeFfToNot V (phi.imp_ psi))
Tactic:
simp only [evalPrimeFfToNot] at psi_ih
Proof state after:
Δ_U : Set Formula
V : VarBoolAssignment
phi psi : Formula
h1 : ↑phi.primeSet ⊆ Δ_U ∧ ↑psi.primeSet ⊆ Δ_U
phi_ih :
  ↑phi.primeSet ⊆ Δ_U →
    IsDeduct ((fun a => if evalPrime V a then a else a.not_) '' Δ_U) (if evalPrime V phi then phi else phi.not_)
psi_ih :
  ↑psi.primeSet ⊆ Δ_U →
    IsDeduct ((fun a => if evalPrime V a then a else a.not_) '' Δ_U) (if evalPrime V psi then psi else psi.not_)
⊢ IsDeduct (evalPrimeFfToNot V '' Δ_U) (evalPrimeFfToNot V (phi.imp_ psi))
Theorem: FOL.NV.L_15_7
Proof state before:
Δ_U : Set Formula
V : VarBoolAssignment
phi psi : Formula
h1 : ↑phi.primeSet ⊆ Δ_U ∧ ↑psi.primeSet ⊆ Δ_U
phi_ih :
  ↑phi.primeSet ⊆ Δ_U →
    IsDeduct ((fun a => if evalPrime V a then a else a.not_) '' Δ_U) (if evalPrime V phi then phi else phi.not_)
psi_ih :
  ↑psi.primeSet ⊆ Δ_U →
    IsDeduct ((fun a => if evalPrime V a then a else a.not_) '' Δ_U) (if evalPrime V psi then psi else psi.not_)
⊢ IsDeduct (evalPrimeFfToNot V '' Δ_U) (evalPrimeFfToNot V (phi.imp_ psi))
Tactic:
simp only [evalPrimeFfToNot]
Proof state after:
Δ_U : Set Formula
V : VarBoolAssignment
phi psi : Formula
h1 : ↑phi.primeSet ⊆ Δ_U ∧ ↑psi.primeSet ⊆ Δ_U
phi_ih :
  ↑phi.primeSet ⊆ Δ_U →
    IsDeduct ((fun a => if evalPrime V a then a else a.not_) '' Δ_U) (if evalPrime V phi then phi else phi.not_)
psi_ih :
  ↑psi.primeSet ⊆ Δ_U →
    IsDeduct ((fun a => if evalPrime V a then a else a.not_) '' Δ_U) (if evalPrime V psi then psi else psi.not_)
⊢ IsDeduct ((fun a => if evalPrime V a then a else a.not_) '' Δ_U)
    (if evalPrime V (phi.imp_ psi) then phi.imp_ psi else (phi.imp_ psi).not_)
Theorem: FOL.NV.L_15_7
Proof state before:
Δ_U : Set Formula
V : VarBoolAssignment
phi psi : Formula
h1 : ↑phi.primeSet ⊆ Δ_U ∧ ↑psi.primeSet ⊆ Δ_U
phi_ih :
  ↑phi.primeSet ⊆ Δ_U →
    IsDeduct ((fun a => if evalPrime V a then a else a.not_) '' Δ_U) (if evalPrime V phi then phi else phi.not_)
psi_ih :
  ↑psi.primeSet ⊆ Δ_U →
    IsDeduct ((fun a => if evalPrime V a then a else a.not_) '' Δ_U) (if evalPrime V psi then psi else psi.not_)
⊢ IsDeduct ((fun a => if evalPrime V a then a else a.not_) '' Δ_U)
    (if evalPrime V (phi.imp_ psi) then phi.imp_ psi else (phi.imp_ psi).not_)
Tactic:
cases h1
Proof state after:
case intro
Δ_U : Set Formula
V : VarBoolAssignment
phi psi : Formula
phi_ih :
  ↑phi.primeSet ⊆ Δ_U →
    IsDeduct ((fun a => if evalPrime V a then a else a.not_) '' Δ_U) (if evalPrime V phi then phi else phi.not_)
psi_ih :
  ↑psi.primeSet ⊆ Δ_U →
    IsDeduct ((fun a => if evalPrime V a then a else a.not_) '' Δ_U) (if evalPrime V psi then psi else psi.not_)
left✝ : ↑phi.primeSet ⊆ Δ_U
right✝ : ↑psi.primeSet ⊆ Δ_U
⊢ IsDeduct ((fun a => if evalPrime V a then a else a.not_) '' Δ_U)
    (if evalPrime V (phi.imp_ psi) then phi.imp_ psi else (phi.imp_ psi).not_)
Theorem: FOL.NV.L_15_7
Proof state before:
Δ_U : Set Formula
V : VarBoolAssignment
phi psi : Formula
phi_ih :
  ↑phi.primeSet ⊆ Δ_U →
    IsDeduct ((fun a => if evalPrime V a then a else a.not_) '' Δ_U) (if evalPrime V phi then phi else phi.not_)
psi_ih :
  ↑psi.primeSet ⊆ Δ_U →
    IsDeduct ((fun a => if evalPrime V a then a else a.not_) '' Δ_U) (if evalPrime V psi then psi else psi.not_)
h1_left : ↑phi.primeSet ⊆ Δ_U
h1_right : ↑psi.primeSet ⊆ Δ_U
⊢ IsDeduct ((fun a => if evalPrime V a then a else a.not_) '' Δ_U)
    (if evalPrime V (phi.imp_ psi) then phi.imp_ psi else (phi.imp_ psi).not_)
Tactic:
split_ifs
Proof state after:
case pos
Δ_U : Set Formula
V : VarBoolAssignment
phi psi : Formula
phi_ih :
  ↑phi.primeSet ⊆ Δ_U →
    IsDeduct ((fun a => if evalPrime V a then a else a.not_) '' Δ_U) (if evalPrime V phi then phi else phi.not_)
psi_ih :
  ↑psi.primeSet ⊆ Δ_U →
    IsDeduct ((fun a => if evalPrime V a then a else a.not_) '' Δ_U) (if evalPrime V psi then psi else psi.not_)
h1_left : ↑phi.primeSet ⊆ Δ_U
h1_right : ↑psi.primeSet ⊆ Δ_U
h✝ : evalPrime V (phi.imp_ psi)
⊢ IsDeduct ((fun a => if evalPrime V a then a else a.not_) '' Δ_U) (phi.imp_ psi)

case neg
Δ_U : Set Formula
V : VarBoolAssignment
phi psi : Formula
phi_ih :
  ↑phi.primeSet ⊆ Δ_U →
    IsDeduct ((fun a => if evalPrime V a then a else a.not_) '' Δ_U) (if evalPrime V phi then phi else phi.not_)
psi_ih :
  ↑psi.primeSet ⊆ Δ_U →
    IsDeduct ((fun a => if evalPrime V a then a else a.not_) '' Δ_U) (if evalPrime V psi then psi else psi.not_)
h1_left : ↑phi.primeSet ⊆ Δ_U
h1_right : ↑psi.primeSet ⊆ Δ_U
h✝ : ¬evalPrime V (phi.imp_ psi)
⊢ IsDeduct ((fun a => if evalPrime V a then a else a.not_) '' Δ_U) (phi.imp_ psi).not_
Theorem: FOL.NV.L_15_7
Proof state before:
Δ_U : Set Formula
V : VarBoolAssignment
phi psi : Formula
phi_ih :
  ↑phi.primeSet ⊆ Δ_U →
    IsDeduct ((fun a => if evalPrime V a then a else a.not_) '' Δ_U) (if evalPrime V phi then phi else phi.not_)
psi_ih :
  ↑psi.primeSet ⊆ Δ_U →
    IsDeduct ((fun a => if evalPrime V a then a else a.not_) '' Δ_U) (if evalPrime V psi then psi else psi.not_)
h1_left : ↑phi.primeSet ⊆ Δ_U
h1_right : ↑psi.primeSet ⊆ Δ_U
c1 : evalPrime V (phi.imp_ psi)
⊢ IsDeduct ((fun a => if evalPrime V a then a else a.not_) '' Δ_U) (phi.imp_ psi)
Tactic:
case _ c1 =>
  simp only [evalPrime] at c1
  simp only [imp_iff_not_or] at c1
  cases c1
  case _ c1 =>
    simp only [if_neg c1] at phi_ih
    apply IsDeduct.mp_ (not_ phi)
    apply proof_imp_deduct
    apply T_13_6
    apply phi_ih h1_left
  case _ c1 =>
    simp only [if_pos c1] at psi_ih
    apply IsDeduct.mp_ psi
    apply IsDeduct.axiom_
    apply IsAxiom.prop_1_
    apply psi_ih
    exact h1_right
Proof state after:
no goals