internlm/Lean-Github huggingface dataset:
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_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_
Tactic:
simp only [if_neg c1_right] at psi_ih
Proof state after:
Δ_U : Set Formula
V : VarBoolAssignment
phi psi : Formula
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
psi_ih : ↑psi.primeSet ⊆ Δ_U → IsDeduct ((fun a => if evalPrime V a then a else a.not_) '' Δ_U) psi.not_
⊢ 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
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
psi_ih : ↑psi.primeSet ⊆ Δ_U → IsDeduct ((fun a => if evalPrime V a then a else a.not_) '' Δ_U) psi.not_
⊢ IsDeduct ((fun a => if evalPrime V a then a else a.not_) '' Δ_U) (phi.imp_ psi).not_
Tactic:
apply IsDeduct.mp_ psi.not_
Proof state after:
case a
Δ_U : Set Formula
V : VarBoolAssignment
phi psi : Formula
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
psi_ih : ↑psi.primeSet ⊆ Δ_U → IsDeduct ((fun a => if evalPrime V a then a else a.not_) '' Δ_U) psi.not_
⊢ IsDeduct ((fun a => if evalPrime V a then a else a.not_) '' Δ_U) (psi.not_.imp_ (phi.imp_ psi).not_)

case a
Δ_U : Set Formula
V : VarBoolAssignment
phi psi : Formula
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
psi_ih : ↑psi.primeSet ⊆ Δ_U → IsDeduct ((fun a => if evalPrime V a then a else a.not_) '' Δ_U) psi.not_
⊢ IsDeduct ((fun a => if evalPrime V a then a else a.not_) '' Δ_U) psi.not_
Theorem: FOL.NV.L_15_7
Proof state before:
case a
Δ_U : Set Formula
V : VarBoolAssignment
phi psi : Formula
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
psi_ih : ↑psi.primeSet ⊆ Δ_U → IsDeduct ((fun a => if evalPrime V a then a else a.not_) '' Δ_U) psi.not_
⊢ IsDeduct ((fun a => if evalPrime V a then a else a.not_) '' Δ_U) (psi.not_.imp_ (phi.imp_ psi).not_)
Tactic:
apply IsDeduct.mp_ phi
Proof state after:
case a.a
Δ_U : Set Formula
V : VarBoolAssignment
phi psi : Formula
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
psi_ih : ↑psi.primeSet ⊆ Δ_U → IsDeduct ((fun a => if evalPrime V a then a else a.not_) '' Δ_U) psi.not_
⊢ IsDeduct ((fun a => if evalPrime V a then a else a.not_) '' Δ_U) (phi.imp_ (psi.not_.imp_ (phi.imp_ psi).not_))

case a.a
Δ_U : Set Formula
V : VarBoolAssignment
phi psi : Formula
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
psi_ih : ↑psi.primeSet ⊆ Δ_U → IsDeduct ((fun a => if evalPrime V a then a else a.not_) '' Δ_U) psi.not_
⊢ 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.a
Δ_U : Set Formula
V : VarBoolAssignment
phi psi : Formula
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
psi_ih : ↑psi.primeSet ⊆ Δ_U → IsDeduct ((fun a => if evalPrime V a then a else a.not_) '' Δ_U) psi.not_
⊢ IsDeduct ((fun a => if evalPrime V a then a else a.not_) '' Δ_U) (phi.imp_ (psi.not_.imp_ (phi.imp_ psi).not_))
Tactic:
apply proof_imp_deduct
Proof state after:
case a.a.h1
Δ_U : Set Formula
V : VarBoolAssignment
phi psi : Formula
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
psi_ih : ↑psi.primeSet ⊆ Δ_U → IsDeduct ((fun a => if evalPrime V a then a else a.not_) '' Δ_U) psi.not_
⊢ IsProof (phi.imp_ (psi.not_.imp_ (phi.imp_ psi).not_))
Theorem: FOL.NV.L_15_7
Proof state before:
case a.a.h1
Δ_U : Set Formula
V : VarBoolAssignment
phi psi : Formula
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
psi_ih : ↑psi.primeSet ⊆ Δ_U → IsDeduct ((fun a => if evalPrime V a then a else a.not_) '' Δ_U) psi.not_
⊢ IsProof (phi.imp_ (psi.not_.imp_ (phi.imp_ psi).not_))
Tactic:
apply T_14_8
Proof state after:
no goals
Theorem: FOL.NV.L_15_7
Proof state before:
case a.a
Δ_U : Set Formula
V : VarBoolAssignment
phi psi : Formula
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
psi_ih : ↑psi.primeSet ⊆ Δ_U → IsDeduct ((fun a => if evalPrime V a then a else a.not_) '' Δ_U) psi.not_
⊢ IsDeduct ((fun a => if evalPrime V a then a else a.not_) '' Δ_U) phi
Tactic:
exact phi_ih h1_left
Proof state after:
no goals
Theorem: FOL.NV.L_15_7
Proof state before:
case a
Δ_U : Set Formula
V : VarBoolAssignment
phi psi : Formula
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
psi_ih : ↑psi.primeSet ⊆ Δ_U → IsDeduct ((fun a => if evalPrime V a then a else a.not_) '' Δ_U) psi.not_
⊢ IsDeduct ((fun a => if evalPrime V a then a else a.not_) '' Δ_U) psi.not_
Tactic:
exact psi_ih h1_right
Proof state after:
no goals
Theorem: FOL.NV.L_15_7
Proof state before:
Δ_U : Set Formula
V : VarBoolAssignment
x : VarName
phi : Formula
phi_ih : ↑phi.primeSet ⊆ Δ_U → IsDeduct (evalPrimeFfToNot V '' Δ_U) (evalPrimeFfToNot V phi)
h1 : ↑(forall_ x phi).primeSet ⊆ Δ_U
⊢ IsDeduct (evalPrimeFfToNot V '' Δ_U) (evalPrimeFfToNot V (forall_ x phi))
Tactic:
let F := forall_ x phi
Proof state after:
Δ_U : Set Formula
V : VarBoolAssignment
x : VarName
phi : Formula
phi_ih : ↑phi.primeSet ⊆ Δ_U → IsDeduct (evalPrimeFfToNot V '' Δ_U) (evalPrimeFfToNot V phi)
h1 : ↑(forall_ x phi).primeSet ⊆ Δ_U
F : Formula := forall_ x phi
⊢ IsDeduct (evalPrimeFfToNot V '' Δ_U) (evalPrimeFfToNot V (forall_ x phi))
Theorem: FOL.NV.L_15_7
Proof state before:
Δ_U : Set Formula
V : VarBoolAssignment
x : VarName
phi : Formula
phi_ih : ↑phi.primeSet ⊆ Δ_U → IsDeduct (evalPrimeFfToNot V '' Δ_U) (evalPrimeFfToNot V phi)
h1 : ↑(forall_ x phi).primeSet ⊆ Δ_U
F : Formula := forall_ x phi
⊢ IsDeduct (evalPrimeFfToNot V '' Δ_U) (evalPrimeFfToNot V (forall_ x phi))
Tactic:
simp only [Formula.primeSet] at h1
Proof state after:
Δ_U : Set Formula
V : VarBoolAssignment
x : VarName
phi : Formula
phi_ih : ↑phi.primeSet ⊆ Δ_U → IsDeduct (evalPrimeFfToNot V '' Δ_U) (evalPrimeFfToNot V phi)
h1 : ↑{forall_ x phi} ⊆ Δ_U
F : Formula := forall_ x phi
⊢ IsDeduct (evalPrimeFfToNot V '' Δ_U) (evalPrimeFfToNot V (forall_ x phi))
Theorem: FOL.NV.L_15_7
Proof state before:
Δ_U : Set Formula
V : VarBoolAssignment
x : VarName
phi : Formula
phi_ih : ↑phi.primeSet ⊆ Δ_U → IsDeduct (evalPrimeFfToNot V '' Δ_U) (evalPrimeFfToNot V phi)
h1 : ↑{forall_ x phi} ⊆ Δ_U
F : Formula := forall_ x phi
⊢ IsDeduct (evalPrimeFfToNot V '' Δ_U) (evalPrimeFfToNot V (forall_ x phi))
Tactic:
simp at h1
Proof state after:
Δ_U : Set Formula
V : VarBoolAssignment
x : VarName
phi : Formula
phi_ih : ↑phi.primeSet ⊆ Δ_U → IsDeduct (evalPrimeFfToNot V '' Δ_U) (evalPrimeFfToNot V phi)
F : Formula := forall_ x phi
h1 : forall_ x phi ∈ Δ_U
⊢ IsDeduct (evalPrimeFfToNot V '' Δ_U) (evalPrimeFfToNot V (forall_ x phi))
Theorem: FOL.NV.L_15_7
Proof state before:
Δ_U : Set Formula
V : VarBoolAssignment
x : VarName
phi : Formula
phi_ih : ↑phi.primeSet ⊆ Δ_U → IsDeduct (evalPrimeFfToNot V '' Δ_U) (evalPrimeFfToNot V phi)
F : Formula := forall_ x phi
h1 : forall_ x phi ∈ Δ_U
⊢ IsDeduct (evalPrimeFfToNot V '' Δ_U) (evalPrimeFfToNot V (forall_ x phi))
Tactic:
simp only [evalPrimeFfToNot]
Proof state after:
Δ_U : Set Formula
V : VarBoolAssignment
x : VarName
phi : Formula
phi_ih : ↑phi.primeSet ⊆ Δ_U → IsDeduct (evalPrimeFfToNot V '' Δ_U) (evalPrimeFfToNot V phi)
F : Formula := forall_ x phi
h1 : forall_ x phi ∈ Δ_U
⊢ IsDeduct ((fun a => if evalPrime V a then a else a.not_) '' Δ_U)
    (if evalPrime V (forall_ x phi) then forall_ x phi else (forall_ x phi).not_)
Theorem: FOL.NV.L_15_7
Proof state before:
Δ_U : Set Formula
V : VarBoolAssignment
x : VarName
phi : Formula
phi_ih : ↑phi.primeSet ⊆ Δ_U → IsDeduct (evalPrimeFfToNot V '' Δ_U) (evalPrimeFfToNot V phi)
F : Formula := forall_ x phi
h1 : forall_ x phi ∈ Δ_U
⊢ IsDeduct ((fun a => if evalPrime V a then a else a.not_) '' Δ_U)
    (if evalPrime V (forall_ x phi) then forall_ x phi else (forall_ x phi).not_)
Tactic:
simp only [Formula.evalPrime]
Proof state after:
Δ_U : Set Formula
V : VarBoolAssignment
x : VarName
phi : Formula
phi_ih : ↑phi.primeSet ⊆ Δ_U → IsDeduct (evalPrimeFfToNot V '' Δ_U) (evalPrimeFfToNot V phi)
F : Formula := forall_ x phi
h1 : forall_ x phi ∈ Δ_U
⊢ IsDeduct ((fun a => if evalPrime V a then a else a.not_) '' Δ_U)
    (if V (forall_ x phi) = true then forall_ x phi else (forall_ x phi).not_)
Theorem: FOL.NV.L_15_7
Proof state before:
Δ_U : Set Formula
V : VarBoolAssignment
x : VarName
phi : Formula
phi_ih : ↑phi.primeSet ⊆ Δ_U → IsDeduct (evalPrimeFfToNot V '' Δ_U) (evalPrimeFfToNot V phi)
F : Formula := forall_ x phi
h1 : forall_ x phi ∈ Δ_U
⊢ IsDeduct ((fun a => if evalPrime V a then a else a.not_) '' Δ_U)
    (if V (forall_ x phi) = true then forall_ x phi else (forall_ x phi).not_)
Tactic:
apply IsDeduct.assume_
Proof state after:
case a
Δ_U : Set Formula
V : VarBoolAssignment
x : VarName
phi : Formula
phi_ih : ↑phi.primeSet ⊆ Δ_U → IsDeduct (evalPrimeFfToNot V '' Δ_U) (evalPrimeFfToNot V phi)
F : Formula := forall_ x phi
h1 : forall_ x phi ∈ Δ_U
⊢ (if V (forall_ x phi) = true then forall_ x phi else (forall_ x phi).not_) ∈
    (fun a => if evalPrime V a then a else a.not_) '' Δ_U
Theorem: FOL.NV.L_15_7
Proof state before:
case a
Δ_U : Set Formula
V : VarBoolAssignment
x : VarName
phi : Formula
phi_ih : ↑phi.primeSet ⊆ Δ_U → IsDeduct (evalPrimeFfToNot V '' Δ_U) (evalPrimeFfToNot V phi)
F : Formula := forall_ x phi
h1 : forall_ x phi ∈ Δ_U
⊢ (if V (forall_ x phi) = true then forall_ x phi else (forall_ x phi).not_) ∈
    (fun a => if evalPrime V a then a else a.not_) '' Δ_U
Tactic:
simp
Proof state after:
case a
Δ_U : Set Formula
V : VarBoolAssignment
x : VarName
phi : Formula
phi_ih : ↑phi.primeSet ⊆ Δ_U → IsDeduct (evalPrimeFfToNot V '' Δ_U) (evalPrimeFfToNot V phi)
F : Formula := forall_ x phi
h1 : forall_ x phi ∈ Δ_U
⊢ ∃ x_1 ∈ Δ_U,
    (if evalPrime V x_1 then x_1 else x_1.not_) =
      if V (forall_ x phi) = true then forall_ x phi else (forall_ x phi).not_
Theorem: FOL.NV.L_15_7
Proof state before:
case a
Δ_U : Set Formula
V : VarBoolAssignment
x : VarName
phi : Formula
phi_ih : ↑phi.primeSet ⊆ Δ_U → IsDeduct (evalPrimeFfToNot V '' Δ_U) (evalPrimeFfToNot V phi)
F : Formula := forall_ x phi
h1 : forall_ x phi ∈ Δ_U
⊢ ∃ x_1 ∈ Δ_U,
    (if evalPrime V x_1 then x_1 else x_1.not_) =
      if V (forall_ x phi) = true then forall_ x phi else (forall_ x phi).not_
Tactic:
apply Exists.intro F
Proof state after:
case a
Δ_U : Set Formula
V : VarBoolAssignment
x : VarName
phi : Formula
phi_ih : ↑phi.primeSet ⊆ Δ_U → IsDeduct (evalPrimeFfToNot V '' Δ_U) (evalPrimeFfToNot V phi)
F : Formula := forall_ x phi
h1 : forall_ x phi ∈ Δ_U
⊢ F ∈ Δ_U ∧
    (if evalPrime V F then F else F.not_) = if V (forall_ x phi) = true then forall_ x phi else (forall_ x phi).not_
Theorem: FOL.NV.L_15_7
Proof state before:
case a
Δ_U : Set Formula
V : VarBoolAssignment
x : VarName
phi : Formula
phi_ih : ↑phi.primeSet ⊆ Δ_U → IsDeduct (evalPrimeFfToNot V '' Δ_U) (evalPrimeFfToNot V phi)
F : Formula := forall_ x phi
h1 : forall_ x phi ∈ Δ_U
⊢ F ∈ Δ_U ∧
    (if evalPrime V F then F else F.not_) = if V (forall_ x phi) = true then forall_ x phi else (forall_ x phi).not_
Tactic:
tauto
Proof state after:
no goals
Theorem: FOL.NV.L_15_7
Proof state before:
Δ_U : Set Formula
V : VarBoolAssignment
X : DefName
xs : List VarName
h1 : ↑(def_ X xs).primeSet ⊆ Δ_U
⊢ IsDeduct (evalPrimeFfToNot V '' Δ_U) (evalPrimeFfToNot V (def_ X xs))
Tactic:
let F := def_ X xs
Proof state after:
Δ_U : Set Formula
V : VarBoolAssignment
X : DefName
xs : List VarName
h1 : ↑(def_ X xs).primeSet ⊆ Δ_U
F : Formula := def_ X xs
⊢ IsDeduct (evalPrimeFfToNot V '' Δ_U) (evalPrimeFfToNot V (def_ X xs))
Theorem: FOL.NV.L_15_7
Proof state before:
Δ_U : Set Formula
V : VarBoolAssignment
X : DefName
xs : List VarName
h1 : ↑(def_ X xs).primeSet ⊆ Δ_U
F : Formula := def_ X xs
⊢ IsDeduct (evalPrimeFfToNot V '' Δ_U) (evalPrimeFfToNot V (def_ X xs))
Tactic:
simp only [Formula.primeSet] at h1
Proof state after:
Δ_U : Set Formula
V : VarBoolAssignment
X : DefName
xs : List VarName
h1 : ↑{def_ X xs} ⊆ Δ_U
F : Formula := def_ X xs
⊢ IsDeduct (evalPrimeFfToNot V '' Δ_U) (evalPrimeFfToNot V (def_ X xs))
Theorem: FOL.NV.L_15_7
Proof state before:
Δ_U : Set Formula
V : VarBoolAssignment
X : DefName
xs : List VarName
h1 : ↑{def_ X xs} ⊆ Δ_U
F : Formula := def_ X xs
⊢ IsDeduct (evalPrimeFfToNot V '' Δ_U) (evalPrimeFfToNot V (def_ X xs))
Tactic:
simp at h1
Proof state after:
Δ_U : Set Formula
V : VarBoolAssignment
X : DefName
xs : List VarName
F : Formula := def_ X xs
h1 : def_ X xs ∈ Δ_U
⊢ IsDeduct (evalPrimeFfToNot V '' Δ_U) (evalPrimeFfToNot V (def_ X xs))
Theorem: FOL.NV.L_15_7
Proof state before:
Δ_U : Set Formula
V : VarBoolAssignment
X : DefName
xs : List VarName
F : Formula := def_ X xs
h1 : def_ X xs ∈ Δ_U
⊢ IsDeduct (evalPrimeFfToNot V '' Δ_U) (evalPrimeFfToNot V (def_ X xs))
Tactic:
simp only [evalPrimeFfToNot]
Proof state after:
Δ_U : Set Formula
V : VarBoolAssignment
X : DefName
xs : List VarName
F : Formula := def_ X xs
h1 : def_ X xs ∈ Δ_U
⊢ IsDeduct ((fun a => if evalPrime V a then a else a.not_) '' Δ_U)
    (if evalPrime V (def_ X xs) then def_ X xs else (def_ X xs).not_)
Theorem: FOL.NV.L_15_7
Proof state before:
Δ_U : Set Formula
V : VarBoolAssignment
X : DefName
xs : List VarName
F : Formula := def_ X xs
h1 : def_ X xs ∈ Δ_U
⊢ IsDeduct ((fun a => if evalPrime V a then a else a.not_) '' Δ_U)
    (if evalPrime V (def_ X xs) then def_ X xs else (def_ X xs).not_)
Tactic:
simp only [Formula.evalPrime]
Proof state after:
Δ_U : Set Formula
V : VarBoolAssignment
X : DefName
xs : List VarName
F : Formula := def_ X xs
h1 : def_ X xs ∈ Δ_U
⊢ IsDeduct ((fun a => if evalPrime V a then a else a.not_) '' Δ_U)
    (if V (def_ X xs) = true then def_ X xs else (def_ X xs).not_)
Theorem: FOL.NV.L_15_7
Proof state before:
Δ_U : Set Formula
V : VarBoolAssignment
X : DefName
xs : List VarName
F : Formula := def_ X xs
h1 : def_ X xs ∈ Δ_U
⊢ IsDeduct ((fun a => if evalPrime V a then a else a.not_) '' Δ_U)
    (if V (def_ X xs) = true then def_ X xs else (def_ X xs).not_)
Tactic:
apply IsDeduct.assume_
Proof state after:
case a
Δ_U : Set Formula
V : VarBoolAssignment
X : DefName
xs : List VarName
F : Formula := def_ X xs
h1 : def_ X xs ∈ Δ_U
⊢ (if V (def_ X xs) = true then def_ X xs else (def_ X xs).not_) ∈ (fun a => if evalPrime V a then a else a.not_) '' Δ_U
Theorem: FOL.NV.L_15_7
Proof state before:
case a
Δ_U : Set Formula
V : VarBoolAssignment
X : DefName
xs : List VarName
F : Formula := def_ X xs
h1 : def_ X xs ∈ Δ_U
⊢ (if V (def_ X xs) = true then def_ X xs else (def_ X xs).not_) ∈ (fun a => if evalPrime V a then a else a.not_) '' Δ_U
Tactic:
simp
Proof state after:
case a
Δ_U : Set Formula
V : VarBoolAssignment
X : DefName
xs : List VarName
F : Formula := def_ X xs
h1 : def_ X xs ∈ Δ_U
⊢ ∃ x ∈ Δ_U, (if evalPrime V x then x else x.not_) = if V (def_ X xs) = true then def_ X xs else (def_ X xs).not_
Theorem: FOL.NV.L_15_7
Proof state before:
case a
Δ_U : Set Formula
V : VarBoolAssignment
X : DefName
xs : List VarName
F : Formula := def_ X xs
h1 : def_ X xs ∈ Δ_U
⊢ ∃ x ∈ Δ_U, (if evalPrime V x then x else x.not_) = if V (def_ X xs) = true then def_ X xs else (def_ X xs).not_
Tactic:
apply Exists.intro F
Proof state after:
case a
Δ_U : Set Formula
V : VarBoolAssignment
X : DefName
xs : List VarName
F : Formula := def_ X xs
h1 : def_ X xs ∈ Δ_U
⊢ F ∈ Δ_U ∧ (if evalPrime V F then F else F.not_) = if V (def_ X xs) = true then def_ X xs else (def_ X xs).not_
Theorem: FOL.NV.L_15_7
Proof state before:
case a
Δ_U : Set Formula
V : VarBoolAssignment
X : DefName
xs : List VarName
F : Formula := def_ X xs
h1 : def_ X xs ∈ Δ_U
⊢ F ∈ Δ_U ∧ (if evalPrime V F then F else F.not_) = if V (def_ X xs) = true then def_ X xs else (def_ X xs).not_
Tactic:
tauto
Proof state after:
no goals
Theorem: FOL.NV.L_15_7
Proof state before:
Δ_U : Set Formula
V : VarBoolAssignment
a✝¹ : VarName
a✝ : Formula
a_ih✝ : ↑a✝.primeSet ⊆ Δ_U → IsDeduct (evalPrimeFfToNot V '' Δ_U) (evalPrimeFfToNot V a✝)
h1 : ↑(exists_ a✝¹ a✝).primeSet ⊆ Δ_U
⊢ IsDeduct (evalPrimeFfToNot V '' Δ_U) (evalPrimeFfToNot V (exists_ a✝¹ a✝))
Tactic:
sorry
Proof state after:
no goals
Theorem: FOL.NV.T_14_9_Deduct
Proof state before:
P U : Formula
Δ : Set Formula
h1 : IsDeduct (Δ ∪ {U}) P
h2 : IsDeduct (Δ ∪ {U.not_}) P
⊢ IsDeduct Δ P
Tactic:
apply IsDeduct.mp_ (U.not_.imp_ P)
Proof state after:
case a
P U : Formula
Δ : Set Formula
h1 : IsDeduct (Δ ∪ {U}) P
h2 : IsDeduct (Δ ∪ {U.not_}) P
⊢ IsDeduct Δ ((U.not_.imp_ P).imp_ P)

case a
P U : Formula
Δ : Set Formula
h1 : IsDeduct (Δ ∪ {U}) P
h2 : IsDeduct (Δ ∪ {U.not_}) P
⊢ IsDeduct Δ (U.not_.imp_ P)
Theorem: FOL.NV.T_14_9_Deduct
Proof state before:
case a
P U : Formula
Δ : Set Formula
h1 : IsDeduct (Δ ∪ {U}) P
h2 : IsDeduct (Δ ∪ {U.not_}) P
⊢ IsDeduct Δ ((U.not_.imp_ P).imp_ P)
Tactic:
apply IsDeduct.mp_ (U.imp_ P)
Proof state after:
case a.a
P U : Formula
Δ : Set Formula
h1 : IsDeduct (Δ ∪ {U}) P
h2 : IsDeduct (Δ ∪ {U.not_}) P
⊢ IsDeduct Δ ((U.imp_ P).imp_ ((U.not_.imp_ P).imp_ P))

case a.a
P U : Formula
Δ : Set Formula
h1 : IsDeduct (Δ ∪ {U}) P
h2 : IsDeduct (Δ ∪ {U.not_}) P
⊢ IsDeduct Δ (U.imp_ P)
Theorem: FOL.NV.T_14_9_Deduct
Proof state before:
case a.a
P U : Formula
Δ : Set Formula
h1 : IsDeduct (Δ ∪ {U}) P
h2 : IsDeduct (Δ ∪ {U.not_}) P
⊢ IsDeduct Δ ((U.imp_ P).imp_ ((U.not_.imp_ P).imp_ P))
Tactic:
apply proof_imp_deduct
Proof state after:
case a.a.h1
P U : Formula
Δ : Set Formula
h1 : IsDeduct (Δ ∪ {U}) P
h2 : IsDeduct (Δ ∪ {U.not_}) P
⊢ IsProof ((U.imp_ P).imp_ ((U.not_.imp_ P).imp_ P))
Theorem: FOL.NV.T_14_9_Deduct
Proof state before:
case a.a.h1
P U : Formula
Δ : Set Formula
h1 : IsDeduct (Δ ∪ {U}) P
h2 : IsDeduct (Δ ∪ {U.not_}) P
⊢ IsProof ((U.imp_ P).imp_ ((U.not_.imp_ P).imp_ P))
Tactic:
apply T_14_9
Proof state after:
no goals
Theorem: FOL.NV.T_14_9_Deduct
Proof state before:
case a.a
P U : Formula
Δ : Set Formula
h1 : IsDeduct (Δ ∪ {U}) P
h2 : IsDeduct (Δ ∪ {U.not_}) P
⊢ IsDeduct Δ (U.imp_ P)
Tactic:
apply deduction_theorem
Proof state after:
case a.a.h1
P U : Formula
Δ : Set Formula
h1 : IsDeduct (Δ ∪ {U}) P
h2 : IsDeduct (Δ ∪ {U.not_}) P
⊢ IsDeduct (Δ ∪ {U}) P
Theorem: FOL.NV.T_14_9_Deduct
Proof state before:
case a.a.h1
P U : Formula
Δ : Set Formula
h1 : IsDeduct (Δ ∪ {U}) P
h2 : IsDeduct (Δ ∪ {U.not_}) P
⊢ IsDeduct (Δ ∪ {U}) P
Tactic:
exact h1
Proof state after:
no goals
Theorem: FOL.NV.T_14_9_Deduct
Proof state before:
case a
P U : Formula
Δ : Set Formula
h1 : IsDeduct (Δ ∪ {U}) P
h2 : IsDeduct (Δ ∪ {U.not_}) P
⊢ IsDeduct Δ (U.not_.imp_ P)
Tactic:
apply deduction_theorem
Proof state after:
case a.h1
P U : Formula
Δ : Set Formula
h1 : IsDeduct (Δ ∪ {U}) P
h2 : IsDeduct (Δ ∪ {U.not_}) P
⊢ IsDeduct (Δ ∪ {U.not_}) P
Theorem: FOL.NV.T_14_9_Deduct
Proof state before:
case a.h1
P U : Formula
Δ : Set Formula
h1 : IsDeduct (Δ ∪ {U}) P
h2 : IsDeduct (Δ ∪ {U.not_}) P
⊢ IsDeduct (Δ ∪ {U.not_}) P
Tactic:
exact h2
Proof state after:
no goals
Theorem: FOL.NV.evalPrimeFfToNot_of_function_updateIte_true
Proof state before:
F' : Formula
V : VarBoolAssignment
a✝¹ : DefName
a✝ : List VarName
h1 : (def_ a✝¹ a✝).IsPrime
⊢ evalPrimeFfToNot (Function.updateITE V F' true) (def_ a✝¹ a✝) =
    Function.updateITE (evalPrimeFfToNot V) F' (def_ a✝¹ a✝) (def_ a✝¹ a✝)
Tactic:
case pred_const_ | pred_var_ | eq_ | forall_ | exists_ | def_ =>
  unfold Function.updateITE
  simp only [evalPrimeFfToNot]
  simp only [Formula.evalPrime]
  split_ifs <;> tauto
Proof state after:
no goals
Theorem: FOL.NV.evalPrimeFfToNot_of_function_updateIte_true
Proof state before:
F' : Formula
V : VarBoolAssignment
a✝¹ a✝ : Formula
a_ih✝¹ :
  a✝¹.IsPrime → evalPrimeFfToNot (Function.updateITE V F' true) a✝¹ = Function.updateITE (evalPrimeFfToNot V) F' a✝¹ a✝¹
a_ih✝ :
  a✝.IsPrime → evalPrimeFfToNot (Function.updateITE V F' true) a✝ = Function.updateITE (evalPrimeFfToNot V) F' a✝ a✝
h1 : (a✝¹.iff_ a✝).IsPrime
⊢ evalPrimeFfToNot (Function.updateITE V F' true) (a✝¹.iff_ a✝) =
    Function.updateITE (evalPrimeFfToNot V) F' (a✝¹.iff_ a✝) (a✝¹.iff_ a✝)
Tactic:
case true_ | false_ | not_ | imp_ | and_ | or_ | iff_ =>
  simp only [Formula.IsPrime] at h1
Proof state after:
no goals
Theorem: FOL.NV.evalPrimeFfToNot_of_function_updateIte_true
Proof state before:
F' : Formula
V : VarBoolAssignment
a✝¹ : DefName
a✝ : List VarName
h1 : (def_ a✝¹ a✝).IsPrime
⊢ evalPrimeFfToNot (Function.updateITE V F' true) (def_ a✝¹ a✝) =
    Function.updateITE (evalPrimeFfToNot V) F' (def_ a✝¹ a✝) (def_ a✝¹ a✝)
Tactic:
unfold Function.updateITE
Proof state after:
F' : Formula
V : VarBoolAssignment
a✝¹ : DefName
a✝ : List VarName
h1 : (def_ a✝¹ a✝).IsPrime
⊢ evalPrimeFfToNot (fun c => if c = F' then true else V c) (def_ a✝¹ a✝) =
    if def_ a✝¹ a✝ = F' then def_ a✝¹ a✝ else evalPrimeFfToNot V (def_ a✝¹ a✝)
Theorem: FOL.NV.evalPrimeFfToNot_of_function_updateIte_true
Proof state before:
F' : Formula
V : VarBoolAssignment
a✝¹ : DefName
a✝ : List VarName
h1 : (def_ a✝¹ a✝).IsPrime
⊢ evalPrimeFfToNot (fun c => if c = F' then true else V c) (def_ a✝¹ a✝) =
    if def_ a✝¹ a✝ = F' then def_ a✝¹ a✝ else evalPrimeFfToNot V (def_ a✝¹ a✝)
Tactic:
simp only [evalPrimeFfToNot]
Proof state after:
F' : Formula
V : VarBoolAssignment
a✝¹ : DefName
a✝ : List VarName
h1 : (def_ a✝¹ a✝).IsPrime
⊢ (if evalPrime (fun c => if c = F' then true else V c) (def_ a✝¹ a✝) then def_ a✝¹ a✝ else (def_ a✝¹ a✝).not_) =
    if def_ a✝¹ a✝ = F' then def_ a✝¹ a✝ else if evalPrime V (def_ a✝¹ a✝) then def_ a✝¹ a✝ else (def_ a✝¹ a✝).not_
Theorem: FOL.NV.evalPrimeFfToNot_of_function_updateIte_true
Proof state before:
F' : Formula
V : VarBoolAssignment
a✝¹ : DefName
a✝ : List VarName
h1 : (def_ a✝¹ a✝).IsPrime
⊢ (if evalPrime (fun c => if c = F' then true else V c) (def_ a✝¹ a✝) then def_ a✝¹ a✝ else (def_ a✝¹ a✝).not_) =
    if def_ a✝¹ a✝ = F' then def_ a✝¹ a✝ else if evalPrime V (def_ a✝¹ a✝) then def_ a✝¹ a✝ else (def_ a✝¹ a✝).not_
Tactic:
simp only [Formula.evalPrime]
Proof state after:
F' : Formula
V : VarBoolAssignment
a✝¹ : DefName
a✝ : List VarName
h1 : (def_ a✝¹ a✝).IsPrime
⊢ (if (if def_ a✝¹ a✝ = F' then true else V (def_ a✝¹ a✝)) = true then def_ a✝¹ a✝ else (def_ a✝¹ a✝).not_) =
    if def_ a✝¹ a✝ = F' then def_ a✝¹ a✝ else if V (def_ a✝¹ a✝) = true then def_ a✝¹ a✝ else (def_ a✝¹ a✝).not_