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

State before:
F F' : Formula
V : VarBoolAssignment
h1 : F.IsPrime
⊢ evalPrimeFfToNot (Function.updateITE V F' true) F = Function.updateITE (evalPrimeFfToNot V) F' F 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' true) (pred_const_ a✝¹ a✝) =
    Function.updateITE (evalPrimeFfToNot V) F' (pred_const_ a✝¹ a✝) (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' true) (pred_var_ a✝¹ a✝) =
    Function.updateITE (evalPrimeFfToNot V) F' (pred_var_ a✝¹ a✝) (pred_var_ a✝¹ a✝)

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

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

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

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

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

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

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

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

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

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

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

State before:
F' : Formula
V : VarBoolAssignment
a✝¹ : DefName
a✝ : List VarName
h1 : (def_ a✝¹ a✝).IsPrime
⊢ evalPrimeFfToNot (Function.updateITE V F' true) (def_ a✝¹ a✝) =
    Function.updateITE (evalPrimeFfToNot V) F' (def_ a✝¹ a✝) (def_ a✝¹ a✝)
Tactic:
case pred_const_ | pred_var_ | eq_ | forall_ | exists_ | def_ =>
  unfold Function.updateITE
  simp only [evalPrimeFfToNot]
  simp only [Formula.evalPrime]
  split_ifs <;> tauto
State after:
no goals

State before:
F' : Formula
V : VarBoolAssignment
a✝¹ a✝ : Formula
a_ih✝¹ :
  a✝¹.IsPrime → evalPrimeFfToNot (Function.updateITE V F' true) a✝¹ = Function.updateITE (evalPrimeFfToNot V) F' a✝¹ a✝¹
a_ih✝ :
  a✝.IsPrime → evalPrimeFfToNot (Function.updateITE V F' true) a✝ = Function.updateITE (evalPrimeFfToNot V) F' a✝ a✝
h1 : (a✝¹.iff_ a✝).IsPrime
⊢ evalPrimeFfToNot (Function.updateITE V F' true) (a✝¹.iff_ a✝) =
    Function.updateITE (evalPrimeFfToNot V) F' (a✝¹.iff_ a✝) (a✝¹.iff_ a✝)
Tactic:
case true_ | false_ | not_ | imp_ | and_ | or_ | iff_ =>
  simp only [Formula.IsPrime] at h1
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' true) (def_ a✝¹ a✝) =
    Function.updateITE (evalPrimeFfToNot V) F' (def_ a✝¹ a✝) (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 true else V c) (def_ a✝¹ a✝) =
    if def_ a✝¹ a✝ = F' then def_ a✝¹ a✝ 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 true else V c) (def_ a✝¹ a✝) =
    if def_ a✝¹ a✝ = F' then def_ a✝¹ a✝ else evalPrimeFfToNot V (def_ a✝¹ a✝)
Tactic:
simp only [evalPrimeFfToNot]
State after:
F' : Formula
V : VarBoolAssignment
a✝¹ : DefName
a✝ : List VarName
h1 : (def_ a✝¹ a✝).IsPrime
⊢ (if evalPrime (fun c => if c = F' then true else V c) (def_ a✝¹ a✝) then def_ a✝¹ a✝ else (def_ a✝¹ a✝).not_) =
    if def_ a✝¹ a✝ = F' then def_ a✝¹ a✝ else if evalPrime V (def_ a✝¹ a✝) then def_ a✝¹ a✝ else (def_ a✝¹ a✝).not_

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

State before:
F' : Formula
V : VarBoolAssignment
a✝¹ : DefName
a✝ : List VarName
h1 : (def_ a✝¹ a✝).IsPrime
⊢ (if (if def_ a✝¹ a✝ = F' then true else V (def_ a✝¹ a✝)) = true then def_ a✝¹ a✝ else (def_ a✝¹ a✝).not_) =
    if def_ a✝¹ a✝ = F' then def_ a✝¹ a✝ else if V (def_ a✝¹ a✝) = true then def_ a✝¹ a✝ else (def_ a✝¹ a✝).not_
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' true) a✝¹ = Function.updateITE (evalPrimeFfToNot V) F' a✝¹ a✝¹
a_ih✝ :
  a✝.IsPrime → evalPrimeFfToNot (Function.updateITE V F' true) a✝ = Function.updateITE (evalPrimeFfToNot V) F' a✝ a✝
h1 : (a✝¹.iff_ a✝).IsPrime
⊢ evalPrimeFfToNot (Function.updateITE V F' true) (a✝¹.iff_ a✝) =
    Function.updateITE (evalPrimeFfToNot V) F' (a✝¹.iff_ a✝) (a✝¹.iff_ a✝)
Tactic:
simp only [Formula.IsPrime] at h1
State after:
no goals