Theorem: FOL.NV.evalPrimeFfToNot_of_function_updateIte_true
Proof 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
Proof 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✝)