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

State before:
F F' : Formula
V : VarBoolAssignment
h1 : F.IsPrime
⊢ evalPrimeFfToNot (Function.updateITE V F' false) F = Function.updateITE (evalPrimeFfToNot V) F' F.not_ F
Tactic:
induction F
State after:
case pred_const_
F' : Formula
V : VarBoolAssignment
a✝¹ : PredName
a✝ : List VarName
h1 : (pred_const_ a✝¹ a✝).IsPrime
⊢ evalPrimeFfToNot (Function.updateITE V F' false) (pred_const_ a✝¹ a✝) =
    Function.updateITE (evalPrimeFfToNot V) F' (pred_const_ a✝¹ a✝).not_ (pred_const_ a✝¹ a✝)

case pred_var_
F' : Formula
V : VarBoolAssignment
a✝¹ : PredName
a✝ : List VarName
h1 : (pred_var_ a✝¹ a✝).IsPrime
⊢ evalPrimeFfToNot (Function.updateITE V F' false) (pred_var_ a✝¹ a✝) =
    Function.updateITE (evalPrimeFfToNot V) F' (pred_var_ a✝¹ a✝).not_ (pred_var_ a✝¹ a✝)

case eq_
F' : Formula
V : VarBoolAssignment
a✝¹ a✝ : VarName
h1 : (eq_ a✝¹ a✝).IsPrime
⊢ evalPrimeFfToNot (Function.updateITE V F' false) (eq_ a✝¹ a✝) =
    Function.updateITE (evalPrimeFfToNot V) F' (eq_ a✝¹ a✝).not_ (eq_ a✝¹ a✝)

case true_
F' : Formula
V : VarBoolAssignment
h1 : true_.IsPrime
⊢ evalPrimeFfToNot (Function.updateITE V F' false) true_ = Function.updateITE (evalPrimeFfToNot V) F' true_.not_ true_

case false_
F' : Formula
V : VarBoolAssignment
h1 : false_.IsPrime
⊢ evalPrimeFfToNot (Function.updateITE V F' false) false_ =
    Function.updateITE (evalPrimeFfToNot V) F' false_.not_ false_

case not_
F' : Formula
V : VarBoolAssignment
a✝ : Formula
a_ih✝ :
  a✝.IsPrime →
    evalPrimeFfToNot (Function.updateITE V F' false) a✝ = Function.updateITE (evalPrimeFfToNot V) F' a✝.not_ a✝
h1 : a✝.not_.IsPrime
⊢ evalPrimeFfToNot (Function.updateITE V F' false) a✝.not_ =
    Function.updateITE (evalPrimeFfToNot V) F' a✝.not_.not_ a✝.not_

case imp_
F' : Formula
V : VarBoolAssignment
a✝¹ a✝ : Formula
a_ih✝¹ :
  a✝¹.IsPrime →
    evalPrimeFfToNot (Function.updateITE V F' false) a✝¹ = Function.updateITE (evalPrimeFfToNot V) F' a✝¹.not_ a✝¹
a_ih✝ :
  a✝.IsPrime →
    evalPrimeFfToNot (Function.updateITE V F' false) a✝ = Function.updateITE (evalPrimeFfToNot V) F' a✝.not_ a✝
h1 : (a✝¹.imp_ a✝).IsPrime
⊢ evalPrimeFfToNot (Function.updateITE V F' false) (a✝¹.imp_ a✝) =
    Function.updateITE (evalPrimeFfToNot V) F' (a✝¹.imp_ a✝).not_ (a✝¹.imp_ a✝)

case and_
F' : Formula
V : VarBoolAssignment
a✝¹ a✝ : Formula
a_ih✝¹ :
  a✝¹.IsPrime →
    evalPrimeFfToNot (Function.updateITE V F' false) a✝¹ = Function.updateITE (evalPrimeFfToNot V) F' a✝¹.not_ a✝¹
a_ih✝ :
  a✝.IsPrime →
    evalPrimeFfToNot (Function.updateITE V F' false) a✝ = Function.updateITE (evalPrimeFfToNot V) F' a✝.not_ a✝
h1 : (a✝¹.and_ a✝).IsPrime
⊢ evalPrimeFfToNot (Function.updateITE V F' false) (a✝¹.and_ a✝) =
    Function.updateITE (evalPrimeFfToNot V) F' (a✝¹.and_ a✝).not_ (a✝¹.and_ a✝)

case or_
F' : Formula
V : VarBoolAssignment
a✝¹ a✝ : Formula
a_ih✝¹ :
  a✝¹.IsPrime →
    evalPrimeFfToNot (Function.updateITE V F' false) a✝¹ = Function.updateITE (evalPrimeFfToNot V) F' a✝¹.not_ a✝¹
a_ih✝ :
  a✝.IsPrime →
    evalPrimeFfToNot (Function.updateITE V F' false) a✝ = Function.updateITE (evalPrimeFfToNot V) F' a✝.not_ a✝
h1 : (a✝¹.or_ a✝).IsPrime
⊢ evalPrimeFfToNot (Function.updateITE V F' false) (a✝¹.or_ a✝) =
    Function.updateITE (evalPrimeFfToNot V) F' (a✝¹.or_ a✝).not_ (a✝¹.or_ a✝)

case iff_
F' : Formula
V : VarBoolAssignment
a✝¹ a✝ : Formula
a_ih✝¹ :
  a✝¹.IsPrime →
    evalPrimeFfToNot (Function.updateITE V F' false) a✝¹ = Function.updateITE (evalPrimeFfToNot V) F' a✝¹.not_ a✝¹
a_ih✝ :
  a✝.IsPrime →
    evalPrimeFfToNot (Function.updateITE V F' false) a✝ = Function.updateITE (evalPrimeFfToNot V) F' a✝.not_ a✝
h1 : (a✝¹.iff_ a✝).IsPrime
⊢ evalPrimeFfToNot (Function.updateITE V F' false) (a✝¹.iff_ a✝) =
    Function.updateITE (evalPrimeFfToNot V) F' (a✝¹.iff_ a✝).not_ (a✝¹.iff_ a✝)

case forall_
F' : Formula
V : VarBoolAssignment
a✝¹ : VarName
a✝ : Formula
a_ih✝ :
  a✝.IsPrime →
    evalPrimeFfToNot (Function.updateITE V F' false) a✝ = Function.updateITE (evalPrimeFfToNot V) F' a✝.not_ a✝
h1 : (forall_ a✝¹ a✝).IsPrime
⊢ evalPrimeFfToNot (Function.updateITE V F' false) (forall_ a✝¹ a✝) =
    Function.updateITE (evalPrimeFfToNot V) F' (forall_ a✝¹ a✝).not_ (forall_ a✝¹ a✝)

case exists_
F' : Formula
V : VarBoolAssignment
a✝¹ : VarName
a✝ : Formula
a_ih✝ :
  a✝.IsPrime →
    evalPrimeFfToNot (Function.updateITE V F' false) a✝ = Function.updateITE (evalPrimeFfToNot V) F' a✝.not_ a✝
h1 : (exists_ a✝¹ a✝).IsPrime
⊢ evalPrimeFfToNot (Function.updateITE V F' false) (exists_ a✝¹ a✝) =
    Function.updateITE (evalPrimeFfToNot V) F' (exists_ a✝¹ a✝).not_ (exists_ a✝¹ a✝)

case def_
F' : Formula
V : VarBoolAssignment
a✝¹ : DefName
a✝ : List VarName
h1 : (def_ a✝¹ a✝).IsPrime
⊢ evalPrimeFfToNot (Function.updateITE V F' false) (def_ a✝¹ a✝) =
    Function.updateITE (evalPrimeFfToNot V) F' (def_ a✝¹ a✝).not_ (def_ a✝¹ a✝)

State before:
F' : Formula
V : VarBoolAssignment
a✝¹ : DefName
a✝ : List VarName
h1 : (def_ a✝¹ a✝).IsPrime
⊢ evalPrimeFfToNot (Function.updateITE V F' false) (def_ a✝¹ a✝) =
    Function.updateITE (evalPrimeFfToNot V) F' (def_ a✝¹ a✝).not_ (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
State after:
no goals

State before:
F' : Formula
V : VarBoolAssignment
a✝¹ a✝ : Formula
a_ih✝¹ :
  a✝¹.IsPrime →
    evalPrimeFfToNot (Function.updateITE V F' false) a✝¹ = Function.updateITE (evalPrimeFfToNot V) F' a✝¹.not_ a✝¹
a_ih✝ :
  a✝.IsPrime →
    evalPrimeFfToNot (Function.updateITE V F' false) a✝ = Function.updateITE (evalPrimeFfToNot V) F' a✝.not_ a✝
h1 : (a✝¹.iff_ a✝).IsPrime
⊢ evalPrimeFfToNot (Function.updateITE V F' false) (a✝¹.iff_ a✝) =
    Function.updateITE (evalPrimeFfToNot V) F' (a✝¹.iff_ a✝).not_ (a✝¹.iff_ a✝)
Tactic:
case true_ | false_ | not_ | imp_ | and_ | or_ | iff_ =>
  simp only [Formula.IsPrime] at h1
State after:
no goals

State before:
F' : Formula
V : VarBoolAssignment
a✝¹ : DefName
a✝ : List VarName
h1 : (def_ a✝¹ a✝).IsPrime
⊢ evalPrimeFfToNot (Function.updateITE V F' false) (def_ a✝¹ a✝) =
    Function.updateITE (evalPrimeFfToNot V) F' (def_ a✝¹ a✝).not_ (def_ a✝¹ a✝)
Tactic:
unfold Function.updateITE
State after:
F' : Formula
V : VarBoolAssignment
a✝¹ : DefName
a✝ : List VarName
h1 : (def_ a✝¹ a✝).IsPrime
⊢ evalPrimeFfToNot (fun c => if c = F' then false else V c) (def_ a✝¹ a✝) =
    if def_ a✝¹ a✝ = F' then (def_ a✝¹ a✝).not_ else evalPrimeFfToNot V (def_ a✝¹ a✝)

State before:
F' : Formula
V : VarBoolAssignment
a✝¹ : DefName
a✝ : List VarName
h1 : (def_ a✝¹ a✝).IsPrime
⊢ evalPrimeFfToNot (fun c => if c = F' then false else V c) (def_ a✝¹ a✝) =
    if def_ a✝¹ a✝ = F' then (def_ a✝¹ a✝).not_ else evalPrimeFfToNot V (def_ a✝¹ a✝)
Tactic:
simp only [evalPrimeFfToNot]
State after:
F' : Formula
V : VarBoolAssignment
a✝¹ : DefName
a✝ : List VarName
h1 : (def_ a✝¹ a✝).IsPrime
⊢ (if evalPrime (fun c => if c = F' then false else V c) (def_ a✝¹ a✝) then def_ a✝¹ a✝ else (def_ a✝¹ a✝).not_) =
    if def_ a✝¹ a✝ = F' then (def_ a✝¹ a✝).not_
    else if evalPrime V (def_ a✝¹ a✝) then def_ a✝¹ a✝ else (def_ a✝¹ a✝).not_

State before:
F' : Formula
V : VarBoolAssignment
a✝¹ : DefName
a✝ : List VarName
h1 : (def_ a✝¹ a✝).IsPrime
⊢ (if evalPrime (fun c => if c = F' then false else V c) (def_ a✝¹ a✝) then def_ a✝¹ a✝ else (def_ a✝¹ a✝).not_) =
    if def_ a✝¹ a✝ = F' then (def_ a✝¹ a✝).not_
    else if evalPrime V (def_ a✝¹ a✝) then def_ a✝¹ a✝ else (def_ a✝¹ a✝).not_
Tactic:
simp only [Formula.evalPrime]
State after:
F' : Formula
V : VarBoolAssignment
a✝¹ : DefName
a✝ : List VarName
h1 : (def_ a✝¹ a✝).IsPrime
⊢ (if (if def_ a✝¹ a✝ = F' then false else V (def_ a✝¹ a✝)) = true then def_ a✝¹ a✝ else (def_ a✝¹ a✝).not_) =
    if def_ a✝¹ a✝ = F' then (def_ a✝¹ a✝).not_ else if V (def_ a✝¹ a✝) = true then def_ a✝¹ a✝ else (def_ a✝¹ a✝).not_

State before:
F' : Formula
V : VarBoolAssignment
a✝¹ : DefName
a✝ : List VarName
h1 : (def_ a✝¹ a✝).IsPrime
⊢ (if (if def_ a✝¹ a✝ = F' then false else V (def_ a✝¹ a✝)) = true then def_ a✝¹ a✝ else (def_ a✝¹ a✝).not_) =
    if def_ a✝¹ a✝ = F' then (def_ a✝¹ a✝).not_ else if V (def_ a✝¹ a✝) = true then def_ a✝¹ a✝ else (def_ a✝¹ a✝).not_
Tactic:
split_ifs <;> tauto
State after:
no goals

State before:
F' : Formula
V : VarBoolAssignment
a✝¹ a✝ : Formula
a_ih✝¹ :
  a✝¹.IsPrime →
    evalPrimeFfToNot (Function.updateITE V F' false) a✝¹ = Function.updateITE (evalPrimeFfToNot V) F' a✝¹.not_ a✝¹
a_ih✝ :
  a✝.IsPrime →
    evalPrimeFfToNot (Function.updateITE V F' false) a✝ = Function.updateITE (evalPrimeFfToNot V) F' a✝.not_ a✝
h1 : (a✝¹.iff_ a✝).IsPrime
⊢ evalPrimeFfToNot (Function.updateITE V F' false) (a✝¹.iff_ a✝) =
    Function.updateITE (evalPrimeFfToNot V) F' (a✝¹.iff_ a✝).not_ (a✝¹.iff_ a✝)
Tactic:
simp only [Formula.IsPrime] at h1
State after:
no goals