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