internlm/Lean-Github huggingface dataset:
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:
simp only [evalPrime] at c1
Proof state after:
Δ_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 → evalPrime V psi
⊢ IsDeduct ((fun a => if evalPrime V a then a else a.not_) '' Δ_U) (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 ((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 → evalPrime V psi
⊢ IsDeduct ((fun a => if evalPrime V a then a else a.not_) '' Δ_U) (phi.imp_ psi)
Tactic:
simp only [imp_iff_not_or] at c1
Proof state after:
Δ_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 ∨ evalPrime V psi
⊢ IsDeduct ((fun a => if evalPrime V a then a else a.not_) '' Δ_U) (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 ((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 ∨ evalPrime V psi
⊢ IsDeduct ((fun a => if evalPrime V a then a else a.not_) '' Δ_U) (phi.imp_ psi)
Tactic:
cases c1
Proof state after:
case inl
Δ_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
⊢ IsDeduct ((fun a => if evalPrime V a then a else a.not_) '' Δ_U) (phi.imp_ psi)

case inr
Δ_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 psi
⊢ IsDeduct ((fun a => if evalPrime V a then a else a.not_) '' Δ_U) (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 ((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
⊢ IsDeduct ((fun a => if evalPrime V a then a else a.not_) '' Δ_U) (phi.imp_ psi)
Tactic:
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
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 ((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 psi
⊢ IsDeduct ((fun a => if evalPrime V a then a else a.not_) '' Δ_U) (phi.imp_ psi)
Tactic:
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
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
⊢ IsDeduct ((fun a => if evalPrime V a then a else a.not_) '' Δ_U) (phi.imp_ psi)
Tactic:
simp only [if_neg c1] at phi_ih
Proof state after:
Δ_U : Set Formula
V : VarBoolAssignment
phi psi : Formula
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
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.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 ((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
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.imp_ psi)
Tactic:
apply IsDeduct.mp_ (not_ phi)
Proof state after:
case a
Δ_U : Set Formula
V : VarBoolAssignment
phi psi : Formula
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
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_.imp_ (phi.imp_ psi))

case a
Δ_U : Set Formula
V : VarBoolAssignment
phi psi : Formula
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
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:
case a
Δ_U : Set Formula
V : VarBoolAssignment
phi psi : Formula
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
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_.imp_ (phi.imp_ psi))

case a
Δ_U : Set Formula
V : VarBoolAssignment
phi psi : Formula
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
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:
apply proof_imp_deduct
Proof state after:
case a.h1
Δ_U : Set Formula
V : VarBoolAssignment
phi psi : Formula
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
phi_ih : ↑phi.primeSet ⊆ Δ_U → IsDeduct ((fun a => if evalPrime V a then a else a.not_) '' Δ_U) phi.not_
⊢ IsProof (phi.not_.imp_ (phi.imp_ psi))

case a
Δ_U : Set Formula
V : VarBoolAssignment
phi psi : Formula
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
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:
case a.h1
Δ_U : Set Formula
V : VarBoolAssignment
phi psi : Formula
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
phi_ih : ↑phi.primeSet ⊆ Δ_U → IsDeduct ((fun a => if evalPrime V a then a else a.not_) '' Δ_U) phi.not_
⊢ IsProof (phi.not_.imp_ (phi.imp_ psi))

case a
Δ_U : Set Formula
V : VarBoolAssignment
phi psi : Formula
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
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:
apply T_13_6
Proof state after:
case a
Δ_U : Set Formula
V : VarBoolAssignment
phi psi : Formula
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
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:
case a
Δ_U : Set Formula
V : VarBoolAssignment
phi psi : Formula
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
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:
apply phi_ih h1_left
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 ((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 psi
⊢ IsDeduct ((fun a => if evalPrime V a then a else a.not_) '' Δ_U) (phi.imp_ psi)
Tactic:
simp only [if_pos c1] at psi_ih
Proof state after:
Δ_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_)
h1_left : ↑phi.primeSet ⊆ Δ_U
h1_right : ↑psi.primeSet ⊆ Δ_U
c1 : evalPrime V psi
psi_ih : ↑psi.primeSet ⊆ Δ_U → IsDeduct ((fun a => if evalPrime V a then a else a.not_) '' Δ_U) psi
⊢ IsDeduct ((fun a => if evalPrime V a then a else a.not_) '' Δ_U) (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 ((fun a => if evalPrime V a then a else a.not_) '' Δ_U) (if evalPrime V phi then phi else phi.not_)
h1_left : ↑phi.primeSet ⊆ Δ_U
h1_right : ↑psi.primeSet ⊆ Δ_U
c1 : evalPrime V psi
psi_ih : ↑psi.primeSet ⊆ Δ_U → IsDeduct ((fun a => if evalPrime V a then a else a.not_) '' Δ_U) psi
⊢ IsDeduct ((fun a => if evalPrime V a then a else a.not_) '' Δ_U) (phi.imp_ psi)
Tactic:
apply IsDeduct.mp_ psi
Proof state after:
case a
Δ_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_)
h1_left : ↑phi.primeSet ⊆ Δ_U
h1_right : ↑psi.primeSet ⊆ Δ_U
c1 : evalPrime V psi
psi_ih : ↑psi.primeSet ⊆ Δ_U → IsDeduct ((fun a => if evalPrime V a then a else a.not_) '' Δ_U) psi
⊢ IsDeduct ((fun a => if evalPrime V a then a else a.not_) '' Δ_U) (psi.imp_ (phi.imp_ psi))

case a
Δ_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_)
h1_left : ↑phi.primeSet ⊆ Δ_U
h1_right : ↑psi.primeSet ⊆ Δ_U
c1 : evalPrime V psi
psi_ih : ↑psi.primeSet ⊆ Δ_U → IsDeduct ((fun a => if evalPrime V a then a else a.not_) '' Δ_U) psi
⊢ IsDeduct ((fun a => if evalPrime V a then a else a.not_) '' Δ_U) psi
Theorem: FOL.NV.L_15_7
Proof state before:
case a
Δ_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_)
h1_left : ↑phi.primeSet ⊆ Δ_U
h1_right : ↑psi.primeSet ⊆ Δ_U
c1 : evalPrime V psi
psi_ih : ↑psi.primeSet ⊆ Δ_U → IsDeduct ((fun a => if evalPrime V a then a else a.not_) '' Δ_U) psi
⊢ IsDeduct ((fun a => if evalPrime V a then a else a.not_) '' Δ_U) (psi.imp_ (phi.imp_ psi))

case a
Δ_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_)
h1_left : ↑phi.primeSet ⊆ Δ_U
h1_right : ↑psi.primeSet ⊆ Δ_U
c1 : evalPrime V psi
psi_ih : ↑psi.primeSet ⊆ Δ_U → IsDeduct ((fun a => if evalPrime V a then a else a.not_) '' Δ_U) psi
⊢ IsDeduct ((fun a => if evalPrime V a then a else a.not_) '' Δ_U) psi
Tactic:
apply IsDeduct.axiom_
Proof state after:
case a.a
Δ_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_)
h1_left : ↑phi.primeSet ⊆ Δ_U
h1_right : ↑psi.primeSet ⊆ Δ_U
c1 : evalPrime V psi
psi_ih : ↑psi.primeSet ⊆ Δ_U → IsDeduct ((fun a => if evalPrime V a then a else a.not_) '' Δ_U) psi
⊢ IsAxiom (psi.imp_ (phi.imp_ psi))

case a
Δ_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_)
h1_left : ↑phi.primeSet ⊆ Δ_U
h1_right : ↑psi.primeSet ⊆ Δ_U
c1 : evalPrime V psi
psi_ih : ↑psi.primeSet ⊆ Δ_U → IsDeduct ((fun a => if evalPrime V a then a else a.not_) '' Δ_U) psi
⊢ IsDeduct ((fun a => if evalPrime V a then a else a.not_) '' Δ_U) psi
Theorem: FOL.NV.L_15_7
Proof state before:
case a.a
Δ_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_)
h1_left : ↑phi.primeSet ⊆ Δ_U
h1_right : ↑psi.primeSet ⊆ Δ_U
c1 : evalPrime V psi
psi_ih : ↑psi.primeSet ⊆ Δ_U → IsDeduct ((fun a => if evalPrime V a then a else a.not_) '' Δ_U) psi
⊢ IsAxiom (psi.imp_ (phi.imp_ psi))

case a
Δ_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_)
h1_left : ↑phi.primeSet ⊆ Δ_U
h1_right : ↑psi.primeSet ⊆ Δ_U
c1 : evalPrime V psi
psi_ih : ↑psi.primeSet ⊆ Δ_U → IsDeduct ((fun a => if evalPrime V a then a else a.not_) '' Δ_U) psi
⊢ IsDeduct ((fun a => if evalPrime V a then a else a.not_) '' Δ_U) psi
Tactic:
apply IsAxiom.prop_1_
Proof state after:
case a
Δ_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_)
h1_left : ↑phi.primeSet ⊆ Δ_U
h1_right : ↑psi.primeSet ⊆ Δ_U
c1 : evalPrime V psi
psi_ih : ↑psi.primeSet ⊆ Δ_U → IsDeduct ((fun a => if evalPrime V a then a else a.not_) '' Δ_U) psi
⊢ IsDeduct ((fun a => if evalPrime V a then a else a.not_) '' Δ_U) psi
Theorem: FOL.NV.L_15_7
Proof state before:
case a
Δ_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_)
h1_left : ↑phi.primeSet ⊆ Δ_U
h1_right : ↑psi.primeSet ⊆ Δ_U
c1 : evalPrime V psi
psi_ih : ↑psi.primeSet ⊆ Δ_U → IsDeduct ((fun a => if evalPrime V a then a else a.not_) '' Δ_U) psi
⊢ IsDeduct ((fun a => if evalPrime V a then a else a.not_) '' Δ_U) psi
Tactic:
apply psi_ih
Proof state after:
case a
Δ_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_)
h1_left : ↑phi.primeSet ⊆ Δ_U
h1_right : ↑psi.primeSet ⊆ Δ_U
c1 : evalPrime V psi
psi_ih : ↑psi.primeSet ⊆ Δ_U → IsDeduct ((fun a => if evalPrime V a then a else a.not_) '' Δ_U) psi
⊢ ↑psi.primeSet ⊆ Δ_U
Theorem: FOL.NV.L_15_7
Proof state before:
case a
Δ_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_)
h1_left : ↑phi.primeSet ⊆ Δ_U
h1_right : ↑psi.primeSet ⊆ Δ_U
c1 : evalPrime V psi
psi_ih : ↑psi.primeSet ⊆ Δ_U → IsDeduct ((fun a => if evalPrime V a then a else a.not_) '' Δ_U) psi
⊢ ↑psi.primeSet ⊆ Δ_U
Tactic:
exact h1_right
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 ((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).not_
Tactic:
simp only [evalPrime] at c1
Proof state after:
Δ_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 → evalPrime V 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 → evalPrime V psi)
⊢ IsDeduct ((fun a => if evalPrime V a then a else a.not_) '' Δ_U) (phi.imp_ psi).not_
Tactic:
simp at c1
Proof state after:
Δ_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 ∧ ¬evalPrime V 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 ∧ ¬evalPrime V psi
⊢ IsDeduct ((fun a => if evalPrime V a then a else a.not_) '' Δ_U) (phi.imp_ psi).not_
Tactic:
cases c1
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_)
h1_left : ↑phi.primeSet ⊆ Δ_U
h1_right : ↑psi.primeSet ⊆ Δ_U
left✝ : evalPrime V phi
right✝ : ¬evalPrime V 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_left : evalPrime V phi
c1_right : ¬evalPrime V psi
⊢ IsDeduct ((fun a => if evalPrime V a then a else a.not_) '' Δ_U) (phi.imp_ psi).not_
Tactic:
simp only [if_pos c1_left] at phi_ih
Proof state after:
Δ_U : Set Formula
V : VarBoolAssignment
phi psi : Formula
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_left : evalPrime V phi
c1_right : ¬evalPrime V psi
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_ psi).not_