Theorem: FOL.NV.L_15_7 (FOL/NV/Margaris/Prop.lean)

State before:
F F' : Formula
Δ_U : Set Formula
V : VarBoolAssignment
Δ_U' : Set Formula
h1 : ↑F.primeSet ⊆ Δ_U
h2 : Δ_U' = evalPrimeFfToNot V '' Δ_U
h3 : F' = evalPrimeFfToNot V F
⊢ IsDeduct Δ_U' F'
Tactic:
subst h2
State after:
F F' : Formula
Δ_U : Set Formula
V : VarBoolAssignment
h1 : ↑F.primeSet ⊆ Δ_U
h3 : F' = evalPrimeFfToNot V F
⊢ IsDeduct (evalPrimeFfToNot V '' Δ_U) F'

State before:
F F' : Formula
Δ_U : Set Formula
V : VarBoolAssignment
h1 : ↑F.primeSet ⊆ Δ_U
h3 : F' = evalPrimeFfToNot V F
⊢ IsDeduct (evalPrimeFfToNot V '' Δ_U) F'
Tactic:
subst h3
State after:
F : Formula
Δ_U : Set Formula
V : VarBoolAssignment
h1 : ↑F.primeSet ⊆ Δ_U
⊢ IsDeduct (evalPrimeFfToNot V '' Δ_U) (evalPrimeFfToNot V F)

State before:
F : Formula
Δ_U : Set Formula
V : VarBoolAssignment
h1 : ↑F.primeSet ⊆ Δ_U
⊢ IsDeduct (evalPrimeFfToNot V '' Δ_U) (evalPrimeFfToNot V F)
Tactic:
induction F
State after:
case pred_const_
Δ_U : Set Formula
V : VarBoolAssignment
a✝¹ : PredName
a✝ : List VarName
h1 : ↑(pred_const_ a✝¹ a✝).primeSet ⊆ Δ_U
⊢ IsDeduct (evalPrimeFfToNot V '' Δ_U) (evalPrimeFfToNot V (pred_const_ a✝¹ a✝))

case pred_var_
Δ_U : Set Formula
V : VarBoolAssignment
a✝¹ : PredName
a✝ : List VarName
h1 : ↑(pred_var_ a✝¹ a✝).primeSet ⊆ Δ_U
⊢ IsDeduct (evalPrimeFfToNot V '' Δ_U) (evalPrimeFfToNot V (pred_var_ a✝¹ a✝))

case eq_
Δ_U : Set Formula
V : VarBoolAssignment
a✝¹ a✝ : VarName
h1 : ↑(eq_ a✝¹ a✝).primeSet ⊆ Δ_U
⊢ IsDeduct (evalPrimeFfToNot V '' Δ_U) (evalPrimeFfToNot V (eq_ a✝¹ a✝))

case true_
Δ_U : Set Formula
V : VarBoolAssignment
h1 : ↑true_.primeSet ⊆ Δ_U
⊢ IsDeduct (evalPrimeFfToNot V '' Δ_U) (evalPrimeFfToNot V true_)

case false_
Δ_U : Set Formula
V : VarBoolAssignment
h1 : ↑false_.primeSet ⊆ Δ_U
⊢ IsDeduct (evalPrimeFfToNot V '' Δ_U) (evalPrimeFfToNot V false_)

case not_
Δ_U : Set Formula
V : VarBoolAssignment
a✝ : Formula
a_ih✝ : ↑a✝.primeSet ⊆ Δ_U → IsDeduct (evalPrimeFfToNot V '' Δ_U) (evalPrimeFfToNot V a✝)
h1 : ↑a✝.not_.primeSet ⊆ Δ_U
⊢ IsDeduct (evalPrimeFfToNot V '' Δ_U) (evalPrimeFfToNot V a✝.not_)

case imp_
Δ_U : Set Formula
V : VarBoolAssignment
a✝¹ a✝ : Formula
a_ih✝¹ : ↑a✝¹.primeSet ⊆ Δ_U → IsDeduct (evalPrimeFfToNot V '' Δ_U) (evalPrimeFfToNot V a✝¹)
a_ih✝ : ↑a✝.primeSet ⊆ Δ_U → IsDeduct (evalPrimeFfToNot V '' Δ_U) (evalPrimeFfToNot V a✝)
h1 : ↑(a✝¹.imp_ a✝).primeSet ⊆ Δ_U
⊢ IsDeduct (evalPrimeFfToNot V '' Δ_U) (evalPrimeFfToNot V (a✝¹.imp_ a✝))

case and_
Δ_U : Set Formula
V : VarBoolAssignment
a✝¹ a✝ : Formula
a_ih✝¹ : ↑a✝¹.primeSet ⊆ Δ_U → IsDeduct (evalPrimeFfToNot V '' Δ_U) (evalPrimeFfToNot V a✝¹)
a_ih✝ : ↑a✝.primeSet ⊆ Δ_U → IsDeduct (evalPrimeFfToNot V '' Δ_U) (evalPrimeFfToNot V a✝)
h1 : ↑(a✝¹.and_ a✝).primeSet ⊆ Δ_U
⊢ IsDeduct (evalPrimeFfToNot V '' Δ_U) (evalPrimeFfToNot V (a✝¹.and_ a✝))

case or_
Δ_U : Set Formula
V : VarBoolAssignment
a✝¹ a✝ : Formula
a_ih✝¹ : ↑a✝¹.primeSet ⊆ Δ_U → IsDeduct (evalPrimeFfToNot V '' Δ_U) (evalPrimeFfToNot V a✝¹)
a_ih✝ : ↑a✝.primeSet ⊆ Δ_U → IsDeduct (evalPrimeFfToNot V '' Δ_U) (evalPrimeFfToNot V a✝)
h1 : ↑(a✝¹.or_ a✝).primeSet ⊆ Δ_U
⊢ IsDeduct (evalPrimeFfToNot V '' Δ_U) (evalPrimeFfToNot V (a✝¹.or_ a✝))

case iff_
Δ_U : Set Formula
V : VarBoolAssignment
a✝¹ a✝ : Formula
a_ih✝¹ : ↑a✝¹.primeSet ⊆ Δ_U → IsDeduct (evalPrimeFfToNot V '' Δ_U) (evalPrimeFfToNot V a✝¹)
a_ih✝ : ↑a✝.primeSet ⊆ Δ_U → IsDeduct (evalPrimeFfToNot V '' Δ_U) (evalPrimeFfToNot V a✝)
h1 : ↑(a✝¹.iff_ a✝).primeSet ⊆ Δ_U
⊢ IsDeduct (evalPrimeFfToNot V '' Δ_U) (evalPrimeFfToNot V (a✝¹.iff_ a✝))

case forall_
Δ_U : Set Formula
V : VarBoolAssignment
a✝¹ : VarName
a✝ : Formula
a_ih✝ : ↑a✝.primeSet ⊆ Δ_U → IsDeduct (evalPrimeFfToNot V '' Δ_U) (evalPrimeFfToNot V a✝)
h1 : ↑(forall_ a✝¹ a✝).primeSet ⊆ Δ_U
⊢ IsDeduct (evalPrimeFfToNot V '' Δ_U) (evalPrimeFfToNot V (forall_ a✝¹ a✝))

case exists_
Δ_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✝))

case def_
Δ_U : Set Formula
V : VarBoolAssignment
a✝¹ : DefName
a✝ : List VarName
h1 : ↑(def_ a✝¹ a✝).primeSet ⊆ Δ_U
⊢ IsDeduct (evalPrimeFfToNot V '' Δ_U) (evalPrimeFfToNot V (def_ a✝¹ a✝))

State before:
Δ_U : Set Formula
V : VarBoolAssignment
X : PredName
xs : List VarName
h1 : ↑(pred_const_ X xs).primeSet ⊆ Δ_U
⊢ IsDeduct (evalPrimeFfToNot V '' Δ_U) (evalPrimeFfToNot V (pred_const_ X xs))
Tactic:
case pred_const_ X xs =>
  let F := pred_const_ X xs
  simp only [Formula.primeSet] at h1
  simp at h1
  simp only [evalPrimeFfToNot]
  simp only [Formula.evalPrime]
  apply IsDeduct.assume_
  simp
  apply Exists.intro F
  tauto
State after:
no goals

State before:
Δ_U : Set Formula
V : VarBoolAssignment
X : PredName
xs : List VarName
h1 : ↑(pred_var_ X xs).primeSet ⊆ Δ_U
⊢ IsDeduct (evalPrimeFfToNot V '' Δ_U) (evalPrimeFfToNot V (pred_var_ X xs))
Tactic:
case pred_var_ X xs =>
  let F := pred_var_ X xs
  simp only [Formula.primeSet] at h1
  simp at h1
  simp only [evalPrimeFfToNot]
  simp only [Formula.evalPrime]
  apply IsDeduct.assume_
  simp
  apply Exists.intro F
  tauto
State after:
no goals

State before:
Δ_U : Set Formula
V : VarBoolAssignment
x y : VarName
h1 : ↑(eq_ x y).primeSet ⊆ Δ_U
⊢ IsDeduct (evalPrimeFfToNot V '' Δ_U) (evalPrimeFfToNot V (eq_ x y))
Tactic:
case eq_ x y =>
  let F := eq_ x y
  simp only [Formula.primeSet] at h1
  simp at h1
  simp only [evalPrimeFfToNot]
  simp only [Formula.evalPrime]
  apply IsDeduct.assume_
  simp
  apply Exists.intro F
  tauto
State after:
no goals

State before:
Δ_U : Set Formula
V : VarBoolAssignment
h1 : ↑true_.primeSet ⊆ Δ_U
⊢ IsDeduct (evalPrimeFfToNot V '' Δ_U) (evalPrimeFfToNot V true_)
Tactic:
case true_ =>
  apply IsDeduct.axiom_
  apply IsAxiom.prop_true_
State after:
no goals

State before:
Δ_U : Set Formula
V : VarBoolAssignment
h1 : ↑false_.primeSet ⊆ Δ_U
⊢ IsDeduct (evalPrimeFfToNot V '' Δ_U) (evalPrimeFfToNot V false_)
Tactic:
case false_ =>
  simp only [Formula.primeSet] at h1
  simp at h1
  simp only [evalPrimeFfToNot]
  simp only [Formula.evalPrime]
  simp
  sorry
State after:
no goals

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:
case not_ phi phi_ih =>
  simp only [Formula.primeSet] at h1
  simp only [evalPrimeFfToNot] at phi_ih
  simp only [evalPrimeFfToNot]
  simp only [evalPrime]
  simp
  split_ifs
  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
  case _ c1 =>
    simp only [c1] at phi_ih
    simp at phi_ih
    exact phi_ih h1
State after:
no goals

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:
case forall_ x phi phi_ih =>
  let F := forall_ x phi
  simp only [Formula.primeSet] at h1
  simp at h1
  simp only [evalPrimeFfToNot]
  simp only [Formula.evalPrime]
  apply IsDeduct.assume_
  simp
  apply Exists.intro F
  tauto
State after:
no goals

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:
case def_ X xs =>
  let F := def_ X xs
  simp only [Formula.primeSet] at h1
  simp at h1
  simp only [evalPrimeFfToNot]
  simp only [Formula.evalPrime]
  apply IsDeduct.assume_
  simp
  apply Exists.intro F
  tauto
State after:
no goals

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:
case and_ | or_ | iff_ | exists_ =>
  sorry
State after:
no goals

State before:
Δ_U : Set Formula
V : VarBoolAssignment
X : PredName
xs : List VarName
h1 : ↑(pred_const_ X xs).primeSet ⊆ Δ_U
⊢ IsDeduct (evalPrimeFfToNot V '' Δ_U) (evalPrimeFfToNot V (pred_const_ X xs))
Tactic:
let F := pred_const_ X xs
State after:
Δ_U : Set Formula
V : VarBoolAssignment
X : PredName
xs : List VarName
h1 : ↑(pred_const_ X xs).primeSet ⊆ Δ_U
F : Formula := pred_const_ X xs
⊢ IsDeduct (evalPrimeFfToNot V '' Δ_U) (evalPrimeFfToNot V (pred_const_ X xs))

State before:
Δ_U : Set Formula
V : VarBoolAssignment
X : PredName
xs : List VarName
h1 : ↑(pred_const_ X xs).primeSet ⊆ Δ_U
F : Formula := pred_const_ X xs
⊢ IsDeduct (evalPrimeFfToNot V '' Δ_U) (evalPrimeFfToNot V (pred_const_ X xs))
Tactic:
simp only [Formula.primeSet] at h1
State after:
Δ_U : Set Formula
V : VarBoolAssignment
X : PredName
xs : List VarName
h1 : ↑{pred_const_ X xs} ⊆ Δ_U
F : Formula := pred_const_ X xs
⊢ IsDeduct (evalPrimeFfToNot V '' Δ_U) (evalPrimeFfToNot V (pred_const_ X xs))

State before:
Δ_U : Set Formula
V : VarBoolAssignment
X : PredName
xs : List VarName
h1 : ↑{pred_const_ X xs} ⊆ Δ_U
F : Formula := pred_const_ X xs
⊢ IsDeduct (evalPrimeFfToNot V '' Δ_U) (evalPrimeFfToNot V (pred_const_ X xs))
Tactic:
simp at h1
State after:
Δ_U : Set Formula
V : VarBoolAssignment
X : PredName
xs : List VarName
F : Formula := pred_const_ X xs
h1 : pred_const_ X xs ∈ Δ_U
⊢ IsDeduct (evalPrimeFfToNot V '' Δ_U) (evalPrimeFfToNot V (pred_const_ X xs))

State before:
Δ_U : Set Formula
V : VarBoolAssignment
X : PredName
xs : List VarName
F : Formula := pred_const_ X xs
h1 : pred_const_ X xs ∈ Δ_U
⊢ IsDeduct (evalPrimeFfToNot V '' Δ_U) (evalPrimeFfToNot V (pred_const_ X xs))
Tactic:
simp only [evalPrimeFfToNot]
State after:
Δ_U : Set Formula
V : VarBoolAssignment
X : PredName
xs : List VarName
F : Formula := pred_const_ X xs
h1 : pred_const_ X xs ∈ Δ_U
⊢ IsDeduct ((fun a => if evalPrime V a then a else a.not_) '' Δ_U)
    (if evalPrime V (pred_const_ X xs) then pred_const_ X xs else (pred_const_ X xs).not_)

State before:
Δ_U : Set Formula
V : VarBoolAssignment
X : PredName
xs : List VarName
F : Formula := pred_const_ X xs
h1 : pred_const_ X xs ∈ Δ_U
⊢ IsDeduct ((fun a => if evalPrime V a then a else a.not_) '' Δ_U)
    (if evalPrime V (pred_const_ X xs) then pred_const_ X xs else (pred_const_ X xs).not_)
Tactic:
simp only [Formula.evalPrime]
State after:
Δ_U : Set Formula
V : VarBoolAssignment
X : PredName
xs : List VarName
F : Formula := pred_const_ X xs
h1 : pred_const_ X xs ∈ Δ_U
⊢ IsDeduct ((fun a => if evalPrime V a then a else a.not_) '' Δ_U)
    (if V (pred_const_ X xs) = true then pred_const_ X xs else (pred_const_ X xs).not_)

State before:
Δ_U : Set Formula
V : VarBoolAssignment
X : PredName
xs : List VarName
F : Formula := pred_const_ X xs
h1 : pred_const_ X xs ∈ Δ_U
⊢ IsDeduct ((fun a => if evalPrime V a then a else a.not_) '' Δ_U)
    (if V (pred_const_ X xs) = true then pred_const_ X xs else (pred_const_ X xs).not_)
Tactic:
apply IsDeduct.assume_
State after:
case a
Δ_U : Set Formula
V : VarBoolAssignment
X : PredName
xs : List VarName
F : Formula := pred_const_ X xs
h1 : pred_const_ X xs ∈ Δ_U
⊢ (if V (pred_const_ X xs) = true then pred_const_ X xs else (pred_const_ X xs).not_) ∈
    (fun a => if evalPrime V a then a else a.not_) '' Δ_U

State before:
case a
Δ_U : Set Formula
V : VarBoolAssignment
X : PredName
xs : List VarName
F : Formula := pred_const_ X xs
h1 : pred_const_ X xs ∈ Δ_U
⊢ (if V (pred_const_ X xs) = true then pred_const_ X xs else (pred_const_ X xs).not_) ∈
    (fun a => if evalPrime V a then a else a.not_) '' Δ_U
Tactic:
simp
State after:
case a
Δ_U : Set Formula
V : VarBoolAssignment
X : PredName
xs : List VarName
F : Formula := pred_const_ X xs
h1 : pred_const_ X xs ∈ Δ_U
⊢ ∃ x ∈ Δ_U,
    (if evalPrime V x then x else x.not_) =
      if V (pred_const_ X xs) = true then pred_const_ X xs else (pred_const_ X xs).not_

State before:
case a
Δ_U : Set Formula
V : VarBoolAssignment
X : PredName
xs : List VarName
F : Formula := pred_const_ X xs
h1 : pred_const_ X xs ∈ Δ_U
⊢ ∃ x ∈ Δ_U,
    (if evalPrime V x then x else x.not_) =
      if V (pred_const_ X xs) = true then pred_const_ X xs else (pred_const_ X xs).not_
Tactic:
apply Exists.intro F
State after:
case a
Δ_U : Set Formula
V : VarBoolAssignment
X : PredName
xs : List VarName
F : Formula := pred_const_ X xs
h1 : pred_const_ X xs ∈ Δ_U
⊢ F ∈ Δ_U ∧
    (if evalPrime V F then F else F.not_) =
      if V (pred_const_ X xs) = true then pred_const_ X xs else (pred_const_ X xs).not_

State before:
case a
Δ_U : Set Formula
V : VarBoolAssignment
X : PredName
xs : List VarName
F : Formula := pred_const_ X xs
h1 : pred_const_ X xs ∈ Δ_U
⊢ F ∈ Δ_U ∧
    (if evalPrime V F then F else F.not_) =
      if V (pred_const_ X xs) = true then pred_const_ X xs else (pred_const_ X xs).not_
Tactic:
tauto
State after:
no goals

State before:
Δ_U : Set Formula
V : VarBoolAssignment
X : PredName
xs : List VarName
h1 : ↑(pred_var_ X xs).primeSet ⊆ Δ_U
⊢ IsDeduct (evalPrimeFfToNot V '' Δ_U) (evalPrimeFfToNot V (pred_var_ X xs))
Tactic:
let F := pred_var_ X xs
State after:
Δ_U : Set Formula
V : VarBoolAssignment
X : PredName
xs : List VarName
h1 : ↑(pred_var_ X xs).primeSet ⊆ Δ_U
F : Formula := pred_var_ X xs
⊢ IsDeduct (evalPrimeFfToNot V '' Δ_U) (evalPrimeFfToNot V (pred_var_ X xs))

State before:
Δ_U : Set Formula
V : VarBoolAssignment
X : PredName
xs : List VarName
h1 : ↑(pred_var_ X xs).primeSet ⊆ Δ_U
F : Formula := pred_var_ X xs
⊢ IsDeduct (evalPrimeFfToNot V '' Δ_U) (evalPrimeFfToNot V (pred_var_ X xs))
Tactic:
simp only [Formula.primeSet] at h1
State after:
Δ_U : Set Formula
V : VarBoolAssignment
X : PredName
xs : List VarName
h1 : ↑{pred_var_ X xs} ⊆ Δ_U
F : Formula := pred_var_ X xs
⊢ IsDeduct (evalPrimeFfToNot V '' Δ_U) (evalPrimeFfToNot V (pred_var_ X xs))

State before:
Δ_U : Set Formula
V : VarBoolAssignment
X : PredName
xs : List VarName
h1 : ↑{pred_var_ X xs} ⊆ Δ_U
F : Formula := pred_var_ X xs
⊢ IsDeduct (evalPrimeFfToNot V '' Δ_U) (evalPrimeFfToNot V (pred_var_ X xs))
Tactic:
simp at h1
State after:
Δ_U : Set Formula
V : VarBoolAssignment
X : PredName
xs : List VarName
F : Formula := pred_var_ X xs
h1 : pred_var_ X xs ∈ Δ_U
⊢ IsDeduct (evalPrimeFfToNot V '' Δ_U) (evalPrimeFfToNot V (pred_var_ X xs))

State before:
Δ_U : Set Formula
V : VarBoolAssignment
X : PredName
xs : List VarName
F : Formula := pred_var_ X xs
h1 : pred_var_ X xs ∈ Δ_U
⊢ IsDeduct (evalPrimeFfToNot V '' Δ_U) (evalPrimeFfToNot V (pred_var_ X xs))
Tactic:
simp only [evalPrimeFfToNot]
State after:
Δ_U : Set Formula
V : VarBoolAssignment
X : PredName
xs : List VarName
F : Formula := pred_var_ X xs
h1 : pred_var_ X xs ∈ Δ_U
⊢ IsDeduct ((fun a => if evalPrime V a then a else a.not_) '' Δ_U)
    (if evalPrime V (pred_var_ X xs) then pred_var_ X xs else (pred_var_ X xs).not_)

State before:
Δ_U : Set Formula
V : VarBoolAssignment
X : PredName
xs : List VarName
F : Formula := pred_var_ X xs
h1 : pred_var_ X xs ∈ Δ_U
⊢ IsDeduct ((fun a => if evalPrime V a then a else a.not_) '' Δ_U)
    (if evalPrime V (pred_var_ X xs) then pred_var_ X xs else (pred_var_ X xs).not_)
Tactic:
simp only [Formula.evalPrime]
State after:
Δ_U : Set Formula
V : VarBoolAssignment
X : PredName
xs : List VarName
F : Formula := pred_var_ X xs
h1 : pred_var_ X xs ∈ Δ_U
⊢ IsDeduct ((fun a => if evalPrime V a then a else a.not_) '' Δ_U)
    (if V (pred_var_ X xs) = true then pred_var_ X xs else (pred_var_ X xs).not_)

State before:
Δ_U : Set Formula
V : VarBoolAssignment
X : PredName
xs : List VarName
F : Formula := pred_var_ X xs
h1 : pred_var_ X xs ∈ Δ_U
⊢ IsDeduct ((fun a => if evalPrime V a then a else a.not_) '' Δ_U)
    (if V (pred_var_ X xs) = true then pred_var_ X xs else (pred_var_ X xs).not_)
Tactic:
apply IsDeduct.assume_
State after:
case a
Δ_U : Set Formula
V : VarBoolAssignment
X : PredName
xs : List VarName
F : Formula := pred_var_ X xs
h1 : pred_var_ X xs ∈ Δ_U
⊢ (if V (pred_var_ X xs) = true then pred_var_ X xs else (pred_var_ X xs).not_) ∈
    (fun a => if evalPrime V a then a else a.not_) '' Δ_U

State before:
case a
Δ_U : Set Formula
V : VarBoolAssignment
X : PredName
xs : List VarName
F : Formula := pred_var_ X xs
h1 : pred_var_ X xs ∈ Δ_U
⊢ (if V (pred_var_ X xs) = true then pred_var_ X xs else (pred_var_ X xs).not_) ∈
    (fun a => if evalPrime V a then a else a.not_) '' Δ_U
Tactic:
simp
State after:
case a
Δ_U : Set Formula
V : VarBoolAssignment
X : PredName
xs : List VarName
F : Formula := pred_var_ X xs
h1 : pred_var_ X xs ∈ Δ_U
⊢ ∃ x ∈ Δ_U,
    (if evalPrime V x then x else x.not_) = if V (pred_var_ X xs) = true then pred_var_ X xs else (pred_var_ X xs).not_

State before:
case a
Δ_U : Set Formula
V : VarBoolAssignment
X : PredName
xs : List VarName
F : Formula := pred_var_ X xs
h1 : pred_var_ X xs ∈ Δ_U
⊢ ∃ x ∈ Δ_U,
    (if evalPrime V x then x else x.not_) = if V (pred_var_ X xs) = true then pred_var_ X xs else (pred_var_ X xs).not_
Tactic:
apply Exists.intro F
State after:
case a
Δ_U : Set Formula
V : VarBoolAssignment
X : PredName
xs : List VarName
F : Formula := pred_var_ X xs
h1 : pred_var_ X xs ∈ Δ_U
⊢ F ∈ Δ_U ∧
    (if evalPrime V F then F else F.not_) = if V (pred_var_ X xs) = true then pred_var_ X xs else (pred_var_ X xs).not_

State before:
case a
Δ_U : Set Formula
V : VarBoolAssignment
X : PredName
xs : List VarName
F : Formula := pred_var_ X xs
h1 : pred_var_ X xs ∈ Δ_U
⊢ F ∈ Δ_U ∧
    (if evalPrime V F then F else F.not_) = if V (pred_var_ X xs) = true then pred_var_ X xs else (pred_var_ X xs).not_
Tactic:
tauto
State after:
no goals

State before:
Δ_U : Set Formula
V : VarBoolAssignment
x y : VarName
h1 : ↑(eq_ x y).primeSet ⊆ Δ_U
⊢ IsDeduct (evalPrimeFfToNot V '' Δ_U) (evalPrimeFfToNot V (eq_ x y))
Tactic:
let F := eq_ x y
State after:
Δ_U : Set Formula
V : VarBoolAssignment
x y : VarName
h1 : ↑(eq_ x y).primeSet ⊆ Δ_U
F : Formula := eq_ x y
⊢ IsDeduct (evalPrimeFfToNot V '' Δ_U) (evalPrimeFfToNot V (eq_ x y))

State before:
Δ_U : Set Formula
V : VarBoolAssignment
x y : VarName
h1 : ↑(eq_ x y).primeSet ⊆ Δ_U
F : Formula := eq_ x y
⊢ IsDeduct (evalPrimeFfToNot V '' Δ_U) (evalPrimeFfToNot V (eq_ x y))
Tactic:
simp only [Formula.primeSet] at h1
State after:
Δ_U : Set Formula
V : VarBoolAssignment
x y : VarName
h1 : ↑{eq_ x y} ⊆ Δ_U
F : Formula := eq_ x y
⊢ IsDeduct (evalPrimeFfToNot V '' Δ_U) (evalPrimeFfToNot V (eq_ x y))

State before:
Δ_U : Set Formula
V : VarBoolAssignment
x y : VarName
h1 : ↑{eq_ x y} ⊆ Δ_U
F : Formula := eq_ x y
⊢ IsDeduct (evalPrimeFfToNot V '' Δ_U) (evalPrimeFfToNot V (eq_ x y))
Tactic:
simp at h1
State after:
Δ_U : Set Formula
V : VarBoolAssignment
x y : VarName
F : Formula := eq_ x y
h1 : eq_ x y ∈ Δ_U
⊢ IsDeduct (evalPrimeFfToNot V '' Δ_U) (evalPrimeFfToNot V (eq_ x y))

State before:
Δ_U : Set Formula
V : VarBoolAssignment
x y : VarName
F : Formula := eq_ x y
h1 : eq_ x y ∈ Δ_U
⊢ IsDeduct (evalPrimeFfToNot V '' Δ_U) (evalPrimeFfToNot V (eq_ x y))
Tactic:
simp only [evalPrimeFfToNot]
State after:
Δ_U : Set Formula
V : VarBoolAssignment
x y : VarName
F : Formula := eq_ x y
h1 : eq_ x y ∈ Δ_U
⊢ IsDeduct ((fun a => if evalPrime V a then a else a.not_) '' Δ_U)
    (if evalPrime V (eq_ x y) then eq_ x y else (eq_ x y).not_)

State before:
Δ_U : Set Formula
V : VarBoolAssignment
x y : VarName
F : Formula := eq_ x y
h1 : eq_ x y ∈ Δ_U
⊢ IsDeduct ((fun a => if evalPrime V a then a else a.not_) '' Δ_U)
    (if evalPrime V (eq_ x y) then eq_ x y else (eq_ x y).not_)
Tactic:
simp only [Formula.evalPrime]
State after:
Δ_U : Set Formula
V : VarBoolAssignment
x y : VarName
F : Formula := eq_ x y
h1 : eq_ x y ∈ Δ_U
⊢ IsDeduct ((fun a => if evalPrime V a then a else a.not_) '' Δ_U)
    (if V (eq_ x y) = true then eq_ x y else (eq_ x y).not_)

State before:
Δ_U : Set Formula
V : VarBoolAssignment
x y : VarName
F : Formula := eq_ x y
h1 : eq_ x y ∈ Δ_U
⊢ IsDeduct ((fun a => if evalPrime V a then a else a.not_) '' Δ_U)
    (if V (eq_ x y) = true then eq_ x y else (eq_ x y).not_)
Tactic:
apply IsDeduct.assume_
State after:
case a
Δ_U : Set Formula
V : VarBoolAssignment
x y : VarName
F : Formula := eq_ x y
h1 : eq_ x y ∈ Δ_U
⊢ (if V (eq_ x y) = true then eq_ x y else (eq_ x y).not_) ∈ (fun a => if evalPrime V a then a else a.not_) '' Δ_U

State before:
case a
Δ_U : Set Formula
V : VarBoolAssignment
x y : VarName
F : Formula := eq_ x y
h1 : eq_ x y ∈ Δ_U
⊢ (if V (eq_ x y) = true then eq_ x y else (eq_ x y).not_) ∈ (fun a => if evalPrime V a then a else a.not_) '' Δ_U
Tactic:
simp
State after:
case a
Δ_U : Set Formula
V : VarBoolAssignment
x y : VarName
F : Formula := eq_ x y
h1 : eq_ x y ∈ Δ_U
⊢ ∃ x_1 ∈ Δ_U, (if evalPrime V x_1 then x_1 else x_1.not_) = if V (eq_ x y) = true then eq_ x y else (eq_ x y).not_

State before:
case a
Δ_U : Set Formula
V : VarBoolAssignment
x y : VarName
F : Formula := eq_ x y
h1 : eq_ x y ∈ Δ_U
⊢ ∃ x_1 ∈ Δ_U, (if evalPrime V x_1 then x_1 else x_1.not_) = if V (eq_ x y) = true then eq_ x y else (eq_ x y).not_
Tactic:
apply Exists.intro F
State after:
case a
Δ_U : Set Formula
V : VarBoolAssignment
x y : VarName
F : Formula := eq_ x y
h1 : eq_ x y ∈ Δ_U
⊢ F ∈ Δ_U ∧ (if evalPrime V F then F else F.not_) = if V (eq_ x y) = true then eq_ x y else (eq_ x y).not_

State before:
case a
Δ_U : Set Formula
V : VarBoolAssignment
x y : VarName
F : Formula := eq_ x y
h1 : eq_ x y ∈ Δ_U
⊢ F ∈ Δ_U ∧ (if evalPrime V F then F else F.not_) = if V (eq_ x y) = true then eq_ x y else (eq_ x y).not_
Tactic:
tauto
State after:
no goals

State before:
Δ_U : Set Formula
V : VarBoolAssignment
h1 : ↑true_.primeSet ⊆ Δ_U
⊢ IsDeduct (evalPrimeFfToNot V '' Δ_U) (evalPrimeFfToNot V true_)
Tactic:
apply IsDeduct.axiom_
State after:
case a
Δ_U : Set Formula
V : VarBoolAssignment
h1 : ↑true_.primeSet ⊆ Δ_U
⊢ IsAxiom (evalPrimeFfToNot V true_)

State before:
case a
Δ_U : Set Formula
V : VarBoolAssignment
h1 : ↑true_.primeSet ⊆ Δ_U
⊢ IsAxiom (evalPrimeFfToNot V true_)
Tactic:
apply IsAxiom.prop_true_
State after:
no goals

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
State after:
Δ_U : Set Formula
V : VarBoolAssignment
h1 : ↑∅ ⊆ Δ_U
⊢ IsDeduct (evalPrimeFfToNot V '' Δ_U) (evalPrimeFfToNot V false_)

State before:
Δ_U : Set Formula
V : VarBoolAssignment
h1 : ↑∅ ⊆ Δ_U
⊢ IsDeduct (evalPrimeFfToNot V '' Δ_U) (evalPrimeFfToNot V false_)
Tactic:
simp at h1
State after:
Δ_U : Set Formula
V : VarBoolAssignment
h1 : True
⊢ IsDeduct (evalPrimeFfToNot V '' Δ_U) (evalPrimeFfToNot V false_)

State before:
Δ_U : Set Formula
V : VarBoolAssignment
h1 : True
⊢ IsDeduct (evalPrimeFfToNot V '' Δ_U) (evalPrimeFfToNot V false_)
Tactic:
simp only [evalPrimeFfToNot]
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_)

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]
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_)

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
State after:
Δ_U : Set Formula
V : VarBoolAssignment
h1 : True
⊢ IsDeduct ((fun a => if evalPrime V a then a else a.not_) '' Δ_U) false_.not_

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
State after:
no goals

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
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_)

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
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_)

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]
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_)

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]
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_)

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
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_)

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
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_

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
State after:
no goals

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
State after:
no goals

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
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_

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
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_

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
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

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
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

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
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

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
State after:
no goals

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
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_

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
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_

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
State after:
no goals

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
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))

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
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))

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
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))

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
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))

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]
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_)

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
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_)

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
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_

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
State after:
no goals

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
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)

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
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)

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
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)

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
State after:
no goals

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
State after:
no goals

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
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)

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)
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_

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
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_

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
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_

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
State after:
no goals

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
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)

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
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

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_
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

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_
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

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
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

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
State after:
no goals

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
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_

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
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_

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
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_

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
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_

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
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_

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_
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_

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
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

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
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_))

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
State after:
no goals

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
State after:
no goals

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
State after:
no goals

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
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))

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
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))

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
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))

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]
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_)

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]
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_)

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_
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

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
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_

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
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_

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
State after:
no goals

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
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))

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
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))

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
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))

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]
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_)

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]
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_)

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_
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

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
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_

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
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_

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
State after:
no goals

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
State after:
no goals