internlm/Lean-Github huggingface dataset:
Theorem: FOL.NV.evalPrimeFfToNot_of_function_updateIte_true
Proof 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
Proof state after:
no goals
Theorem: FOL.NV.evalPrimeFfToNot_of_function_updateIte_true
Proof 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
Proof state after:
no goals
Theorem: FOL.NV.evalPrimeFfToNot_of_function_updateIte_false
Proof 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
Proof state after:
no goals
Theorem: FOL.NV.evalPrimeFfToNot_of_function_updateIte_false
Proof 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
Proof state after:
no goals
Theorem: FOL.NV.evalPrimeFfToNot_of_function_updateIte_false
Proof 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
Proof 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✝)
Theorem: FOL.NV.evalPrimeFfToNot_of_function_updateIte_false
Proof 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]
Proof 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_
Theorem: FOL.NV.evalPrimeFfToNot_of_function_updateIte_false
Proof 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]
Proof 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_
Theorem: FOL.NV.evalPrimeFfToNot_of_function_updateIte_false
Proof 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
Proof state after:
no goals
Theorem: FOL.NV.evalPrimeFfToNot_of_function_updateIte_false
Proof 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
Proof state after:
no goals
Theorem: FOL.NV.image_of_evalPrimeFfToNot_of_function_updateIte
Proof state before:
U : Formula
Δ : Set Formula
V : VarBoolAssignment
b : Bool
h1_Δ : ∀ U' ∈ Δ, U'.IsPrime
h1_U : U.IsPrime
h2 : U ∉ Δ
⊢ evalPrimeFfToNot (Function.updateITE V U b) '' Δ = evalPrimeFfToNot V '' Δ
Tactic:
apply Set.image_congr
Proof state after:
case h
U : Formula
Δ : Set Formula
V : VarBoolAssignment
b : Bool
h1_Δ : ∀ U' ∈ Δ, U'.IsPrime
h1_U : U.IsPrime
h2 : U ∉ Δ
⊢ ∀ a ∈ Δ, evalPrimeFfToNot (Function.updateITE V U b) a = evalPrimeFfToNot V a
Theorem: FOL.NV.image_of_evalPrimeFfToNot_of_function_updateIte
Proof state before:
case h
U : Formula
Δ : Set Formula
V : VarBoolAssignment
b : Bool
h1_Δ : ∀ U' ∈ Δ, U'.IsPrime
h1_U : U.IsPrime
h2 : U ∉ Δ
⊢ ∀ a ∈ Δ, evalPrimeFfToNot (Function.updateITE V U b) a = evalPrimeFfToNot V a
Tactic:
intro U' a1
Proof state after:
case h
U : Formula
Δ : Set Formula
V : VarBoolAssignment
b : Bool
h1_Δ : ∀ U' ∈ Δ, U'.IsPrime
h1_U : U.IsPrime
h2 : U ∉ Δ
U' : Formula
a1 : U' ∈ Δ
⊢ evalPrimeFfToNot (Function.updateITE V U b) U' = evalPrimeFfToNot V U'
Theorem: FOL.NV.image_of_evalPrimeFfToNot_of_function_updateIte
Proof state before:
case h
U : Formula
Δ : Set Formula
V : VarBoolAssignment
b : Bool
h1_Δ : ∀ U' ∈ Δ, U'.IsPrime
h1_U : U.IsPrime
h2 : U ∉ Δ
U' : Formula
a1 : U' ∈ Δ
⊢ evalPrimeFfToNot (Function.updateITE V U b) U' = evalPrimeFfToNot V U'
Tactic:
specialize h1_Δ U' a1
Proof state after:
case h
U : Formula
Δ : Set Formula
V : VarBoolAssignment
b : Bool
h1_U : U.IsPrime
h2 : U ∉ Δ
U' : Formula
a1 : U' ∈ Δ
h1_Δ : U'.IsPrime
⊢ evalPrimeFfToNot (Function.updateITE V U b) U' = evalPrimeFfToNot V U'
Theorem: FOL.NV.image_of_evalPrimeFfToNot_of_function_updateIte
Proof state before:
case h
U : Formula
Δ : Set Formula
V : VarBoolAssignment
b : Bool
h1_U : U.IsPrime
h2 : U ∉ Δ
U' : Formula
a1 : U' ∈ Δ
h1_Δ : U'.IsPrime
⊢ evalPrimeFfToNot (Function.updateITE V U b) U' = evalPrimeFfToNot V U'
Tactic:
cases b
Proof state after:
case h.false
U : Formula
Δ : Set Formula
V : VarBoolAssignment
h1_U : U.IsPrime
h2 : U ∉ Δ
U' : Formula
a1 : U' ∈ Δ
h1_Δ : U'.IsPrime
⊢ evalPrimeFfToNot (Function.updateITE V U false) U' = evalPrimeFfToNot V U'

case h.true
U : Formula
Δ : Set Formula
V : VarBoolAssignment
h1_U : U.IsPrime
h2 : U ∉ Δ
U' : Formula
a1 : U' ∈ Δ
h1_Δ : U'.IsPrime
⊢ evalPrimeFfToNot (Function.updateITE V U true) U' = evalPrimeFfToNot V U'
Theorem: FOL.NV.image_of_evalPrimeFfToNot_of_function_updateIte
Proof state before:
case h.false
U : Formula
Δ : Set Formula
V : VarBoolAssignment
h1_U : U.IsPrime
h2 : U ∉ Δ
U' : Formula
a1 : U' ∈ Δ
h1_Δ : U'.IsPrime
⊢ evalPrimeFfToNot (Function.updateITE V U false) U' = evalPrimeFfToNot V U'
Tactic:
simp only [evalPrimeFfToNot_of_function_updateIte_false U' U V h1_Δ]
Proof state after:
case h.false
U : Formula
Δ : Set Formula
V : VarBoolAssignment
h1_U : U.IsPrime
h2 : U ∉ Δ
U' : Formula
a1 : U' ∈ Δ
h1_Δ : U'.IsPrime
⊢ Function.updateITE (evalPrimeFfToNot V) U U'.not_ U' = evalPrimeFfToNot V U'
Theorem: FOL.NV.image_of_evalPrimeFfToNot_of_function_updateIte
Proof state before:
case h.false
U : Formula
Δ : Set Formula
V : VarBoolAssignment
h1_U : U.IsPrime
h2 : U ∉ Δ
U' : Formula
a1 : U' ∈ Δ
h1_Δ : U'.IsPrime
⊢ Function.updateITE (evalPrimeFfToNot V) U U'.not_ U' = evalPrimeFfToNot V U'
Tactic:
simp only [Function.updateITE]
Proof state after:
case h.false
U : Formula
Δ : Set Formula
V : VarBoolAssignment
h1_U : U.IsPrime
h2 : U ∉ Δ
U' : Formula
a1 : U' ∈ Δ
h1_Δ : U'.IsPrime
⊢ (if U' = U then U'.not_ else evalPrimeFfToNot V U') = evalPrimeFfToNot V U'
Theorem: FOL.NV.image_of_evalPrimeFfToNot_of_function_updateIte
Proof state before:
case h.false
U : Formula
Δ : Set Formula
V : VarBoolAssignment
h1_U : U.IsPrime
h2 : U ∉ Δ
U' : Formula
a1 : U' ∈ Δ
h1_Δ : U'.IsPrime
⊢ (if U' = U then U'.not_ else evalPrimeFfToNot V U') = evalPrimeFfToNot V U'
Tactic:
simp
Proof state after:
case h.false
U : Formula
Δ : Set Formula
V : VarBoolAssignment
h1_U : U.IsPrime
h2 : U ∉ Δ
U' : Formula
a1 : U' ∈ Δ
h1_Δ : U'.IsPrime
⊢ U' = U → U'.not_ = evalPrimeFfToNot V U'
Theorem: FOL.NV.image_of_evalPrimeFfToNot_of_function_updateIte
Proof state before:
case h.false
U : Formula
Δ : Set Formula
V : VarBoolAssignment
h1_U : U.IsPrime
h2 : U ∉ Δ
U' : Formula
a1 : U' ∈ Δ
h1_Δ : U'.IsPrime
⊢ U' = U → U'.not_ = evalPrimeFfToNot V U'
Tactic:
intro a2
Proof state after:
case h.false
U : Formula
Δ : Set Formula
V : VarBoolAssignment
h1_U : U.IsPrime
h2 : U ∉ Δ
U' : Formula
a1 : U' ∈ Δ
h1_Δ : U'.IsPrime
a2 : U' = U
⊢ U'.not_ = evalPrimeFfToNot V U'
Theorem: FOL.NV.image_of_evalPrimeFfToNot_of_function_updateIte
Proof state before:
case h.false
U : Formula
Δ : Set Formula
V : VarBoolAssignment
h1_U : U.IsPrime
h2 : U ∉ Δ
U' : Formula
a1 : U' ∈ Δ
h1_Δ : U'.IsPrime
a2 : U' = U
⊢ U'.not_ = evalPrimeFfToNot V U'
Tactic:
subst a2
Proof state after:
case h.false
Δ : Set Formula
V : VarBoolAssignment
U' : Formula
a1 : U' ∈ Δ
h1_Δ h1_U : U'.IsPrime
h2 : U' ∉ Δ
⊢ U'.not_ = evalPrimeFfToNot V U'
Theorem: FOL.NV.image_of_evalPrimeFfToNot_of_function_updateIte
Proof state before:
case h.false
Δ : Set Formula
V : VarBoolAssignment
U' : Formula
a1 : U' ∈ Δ
h1_Δ h1_U : U'.IsPrime
h2 : U' ∉ Δ
⊢ U'.not_ = evalPrimeFfToNot V U'
Tactic:
contradiction
Proof state after:
no goals
Theorem: FOL.NV.image_of_evalPrimeFfToNot_of_function_updateIte
Proof state before:
case h.true
U : Formula
Δ : Set Formula
V : VarBoolAssignment
h1_U : U.IsPrime
h2 : U ∉ Δ
U' : Formula
a1 : U' ∈ Δ
h1_Δ : U'.IsPrime
⊢ evalPrimeFfToNot (Function.updateITE V U true) U' = evalPrimeFfToNot V U'
Tactic:
simp only [evalPrimeFfToNot_of_function_updateIte_true U' U V h1_Δ]
Proof state after:
case h.true
U : Formula
Δ : Set Formula
V : VarBoolAssignment
h1_U : U.IsPrime
h2 : U ∉ Δ
U' : Formula
a1 : U' ∈ Δ
h1_Δ : U'.IsPrime
⊢ Function.updateITE (evalPrimeFfToNot V) U U' U' = evalPrimeFfToNot V U'
Theorem: FOL.NV.image_of_evalPrimeFfToNot_of_function_updateIte
Proof state before:
case h.true
U : Formula
Δ : Set Formula
V : VarBoolAssignment
h1_U : U.IsPrime
h2 : U ∉ Δ
U' : Formula
a1 : U' ∈ Δ
h1_Δ : U'.IsPrime
⊢ Function.updateITE (evalPrimeFfToNot V) U U' U' = evalPrimeFfToNot V U'
Tactic:
simp only [Function.updateITE]
Proof state after:
case h.true
U : Formula
Δ : Set Formula
V : VarBoolAssignment
h1_U : U.IsPrime
h2 : U ∉ Δ
U' : Formula
a1 : U' ∈ Δ
h1_Δ : U'.IsPrime
⊢ (if U' = U then U' else evalPrimeFfToNot V U') = evalPrimeFfToNot V U'
Theorem: FOL.NV.image_of_evalPrimeFfToNot_of_function_updateIte
Proof state before:
case h.true
U : Formula
Δ : Set Formula
V : VarBoolAssignment
h1_U : U.IsPrime
h2 : U ∉ Δ
U' : Formula
a1 : U' ∈ Δ
h1_Δ : U'.IsPrime
⊢ (if U' = U then U' else evalPrimeFfToNot V U') = evalPrimeFfToNot V U'
Tactic:
simp
Proof state after:
case h.true
U : Formula
Δ : Set Formula
V : VarBoolAssignment
h1_U : U.IsPrime
h2 : U ∉ Δ
U' : Formula
a1 : U' ∈ Δ
h1_Δ : U'.IsPrime
⊢ U' = U → U' = evalPrimeFfToNot V U'
Theorem: FOL.NV.image_of_evalPrimeFfToNot_of_function_updateIte
Proof state before:
case h.true
U : Formula
Δ : Set Formula
V : VarBoolAssignment
h1_U : U.IsPrime
h2 : U ∉ Δ
U' : Formula
a1 : U' ∈ Δ
h1_Δ : U'.IsPrime
⊢ U' = U → U' = evalPrimeFfToNot V U'
Tactic:
intro a2
Proof state after:
case h.true
U : Formula
Δ : Set Formula
V : VarBoolAssignment
h1_U : U.IsPrime
h2 : U ∉ Δ
U' : Formula
a1 : U' ∈ Δ
h1_Δ : U'.IsPrime
a2 : U' = U
⊢ U' = evalPrimeFfToNot V U'
Theorem: FOL.NV.image_of_evalPrimeFfToNot_of_function_updateIte
Proof state before:
case h.true
U : Formula
Δ : Set Formula
V : VarBoolAssignment
h1_U : U.IsPrime
h2 : U ∉ Δ
U' : Formula
a1 : U' ∈ Δ
h1_Δ : U'.IsPrime
a2 : U' = U
⊢ U' = evalPrimeFfToNot V U'
Tactic:
subst a2
Proof state after:
case h.true
Δ : Set Formula
V : VarBoolAssignment
U' : Formula
a1 : U' ∈ Δ
h1_Δ h1_U : U'.IsPrime
h2 : U' ∉ Δ
⊢ U' = evalPrimeFfToNot V U'
Theorem: FOL.NV.image_of_evalPrimeFfToNot_of_function_updateIte
Proof state before:
case h.true
Δ : Set Formula
V : VarBoolAssignment
U' : Formula
a1 : U' ∈ Δ
h1_Δ h1_U : U'.IsPrime
h2 : U' ∉ Δ
⊢ U' = evalPrimeFfToNot V U'
Tactic:
contradiction
Proof state after:
no goals
Theorem: FOL.NV.propCompleteAuxAux
Proof state before:
P U : Formula
Δ : Set Formula
h1_Δ : ∀ U' ∈ Δ, U'.IsPrime
h1_U : U.IsPrime
h2 : U ∉ Δ
h3 : ∀ (V : VarBoolAssignment), IsDeduct (evalPrimeFfToNot V '' Δ ∪ {evalPrimeFfToNot V U}) P
⊢ ∀ (V : VarBoolAssignment), IsDeduct (evalPrimeFfToNot V '' Δ) P
Tactic:
intro V
Proof state after:
P U : Formula
Δ : Set Formula
h1_Δ : ∀ U' ∈ Δ, U'.IsPrime
h1_U : U.IsPrime
h2 : U ∉ Δ
h3 : ∀ (V : VarBoolAssignment), IsDeduct (evalPrimeFfToNot V '' Δ ∪ {evalPrimeFfToNot V U}) P
V : VarBoolAssignment
⊢ IsDeduct (evalPrimeFfToNot V '' Δ) P
Theorem: FOL.NV.propCompleteAuxAux
Proof state before:
P U : Formula
Δ : Set Formula
h1_Δ : ∀ U' ∈ Δ, U'.IsPrime
h1_U : U.IsPrime
h2 : U ∉ Δ
h3 : ∀ (V : VarBoolAssignment), IsDeduct (evalPrimeFfToNot V '' Δ ∪ {evalPrimeFfToNot V U}) P
V : VarBoolAssignment
⊢ IsDeduct (evalPrimeFfToNot V '' Δ) P
Tactic:
apply T_14_9_Deduct P U (Δ.image (evalPrimeFfToNot V))
Proof state after:
case h1
P U : Formula
Δ : Set Formula
h1_Δ : ∀ U' ∈ Δ, U'.IsPrime
h1_U : U.IsPrime
h2 : U ∉ Δ
h3 : ∀ (V : VarBoolAssignment), IsDeduct (evalPrimeFfToNot V '' Δ ∪ {evalPrimeFfToNot V U}) P
V : VarBoolAssignment
⊢ IsDeduct (evalPrimeFfToNot V '' Δ ∪ {U}) P

case h2
P U : Formula
Δ : Set Formula
h1_Δ : ∀ U' ∈ Δ, U'.IsPrime
h1_U : U.IsPrime
h2 : U ∉ Δ
h3 : ∀ (V : VarBoolAssignment), IsDeduct (evalPrimeFfToNot V '' Δ ∪ {evalPrimeFfToNot V U}) P
V : VarBoolAssignment
⊢ IsDeduct (evalPrimeFfToNot V '' Δ ∪ {U.not_}) P
Theorem: FOL.NV.propCompleteAuxAux
Proof state before:
case h1
P U : Formula
Δ : Set Formula
h1_Δ : ∀ U' ∈ Δ, U'.IsPrime
h1_U : U.IsPrime
h2 : U ∉ Δ
h3 : ∀ (V : VarBoolAssignment), IsDeduct (evalPrimeFfToNot V '' Δ ∪ {evalPrimeFfToNot V U}) P
V : VarBoolAssignment
⊢ IsDeduct (evalPrimeFfToNot V '' Δ ∪ {U}) P
Tactic:
specialize h3 (Function.updateITE V U true)
Proof state after:
case h1
P U : Formula
Δ : Set Formula
h1_Δ : ∀ U' ∈ Δ, U'.IsPrime
h1_U : U.IsPrime
h2 : U ∉ Δ
V : VarBoolAssignment
h3 :
  IsDeduct (evalPrimeFfToNot (Function.updateITE V U true) '' Δ ∪ {evalPrimeFfToNot (Function.updateITE V U true) U}) P
⊢ IsDeduct (evalPrimeFfToNot V '' Δ ∪ {U}) P
Theorem: FOL.NV.propCompleteAuxAux
Proof state before:
case h1
P U : Formula
Δ : Set Formula
h1_Δ : ∀ U' ∈ Δ, U'.IsPrime
h1_U : U.IsPrime
h2 : U ∉ Δ
V : VarBoolAssignment
h3 :
  IsDeduct (evalPrimeFfToNot (Function.updateITE V U true) '' Δ ∪ {evalPrimeFfToNot (Function.updateITE V U true) U}) P
⊢ IsDeduct (evalPrimeFfToNot V '' Δ ∪ {U}) P
Tactic:
simp only [image_of_evalPrimeFfToNot_of_function_updateIte U Δ V true h1_Δ h1_U h2] at h3
Proof state after:
case h1
P U : Formula
Δ : Set Formula
h1_Δ : ∀ U' ∈ Δ, U'.IsPrime
h1_U : U.IsPrime
h2 : U ∉ Δ
V : VarBoolAssignment
h3 : IsDeduct (evalPrimeFfToNot V '' Δ ∪ {evalPrimeFfToNot (Function.updateITE V U true) U}) P
⊢ IsDeduct (evalPrimeFfToNot V '' Δ ∪ {U}) P
Theorem: FOL.NV.propCompleteAuxAux
Proof state before:
case h1
P U : Formula
Δ : Set Formula
h1_Δ : ∀ U' ∈ Δ, U'.IsPrime
h1_U : U.IsPrime
h2 : U ∉ Δ
V : VarBoolAssignment
h3 : IsDeduct (evalPrimeFfToNot V '' Δ ∪ {evalPrimeFfToNot (Function.updateITE V U true) U}) P
⊢ IsDeduct (evalPrimeFfToNot V '' Δ ∪ {U}) P
Tactic:
simp only [evalPrimeFfToNot_of_function_updateIte_true U U V h1_U] at h3
Proof state after:
case h1
P U : Formula
Δ : Set Formula
h1_Δ : ∀ U' ∈ Δ, U'.IsPrime
h1_U : U.IsPrime
h2 : U ∉ Δ
V : VarBoolAssignment
h3 : IsDeduct (evalPrimeFfToNot V '' Δ ∪ {Function.updateITE (evalPrimeFfToNot V) U U U}) P
⊢ IsDeduct (evalPrimeFfToNot V '' Δ ∪ {U}) P
Theorem: FOL.NV.propCompleteAuxAux
Proof state before:
case h1
P U : Formula
Δ : Set Formula
h1_Δ : ∀ U' ∈ Δ, U'.IsPrime
h1_U : U.IsPrime
h2 : U ∉ Δ
V : VarBoolAssignment
h3 : IsDeduct (evalPrimeFfToNot V '' Δ ∪ {Function.updateITE (evalPrimeFfToNot V) U U U}) P
⊢ IsDeduct (evalPrimeFfToNot V '' Δ ∪ {U}) P
Tactic:
simp only [Function.updateITE] at h3
Proof state after:
case h1
P U : Formula
Δ : Set Formula
h1_Δ : ∀ U' ∈ Δ, U'.IsPrime
h1_U : U.IsPrime
h2 : U ∉ Δ
V : VarBoolAssignment
h3 : IsDeduct (evalPrimeFfToNot V '' Δ ∪ {if True then U else evalPrimeFfToNot V U}) P
⊢ IsDeduct (evalPrimeFfToNot V '' Δ ∪ {U}) P
Theorem: FOL.NV.propCompleteAuxAux
Proof state before:
case h1
P U : Formula
Δ : Set Formula
h1_Δ : ∀ U' ∈ Δ, U'.IsPrime
h1_U : U.IsPrime
h2 : U ∉ Δ
V : VarBoolAssignment
h3 : IsDeduct (evalPrimeFfToNot V '' Δ ∪ {if True then U else evalPrimeFfToNot V U}) P
⊢ IsDeduct (evalPrimeFfToNot V '' Δ ∪ {U}) P
Tactic:
simp only [eq_self_iff_true, if_true] at h3
Proof state after:
case h1
P U : Formula
Δ : Set Formula
h1_Δ : ∀ U' ∈ Δ, U'.IsPrime
h1_U : U.IsPrime
h2 : U ∉ Δ
V : VarBoolAssignment
h3 : IsDeduct (evalPrimeFfToNot V '' Δ ∪ {U}) P
⊢ IsDeduct (evalPrimeFfToNot V '' Δ ∪ {U}) P
Theorem: FOL.NV.propCompleteAuxAux
Proof state before:
case h1
P U : Formula
Δ : Set Formula
h1_Δ : ∀ U' ∈ Δ, U'.IsPrime
h1_U : U.IsPrime
h2 : U ∉ Δ
V : VarBoolAssignment
h3 : IsDeduct (evalPrimeFfToNot V '' Δ ∪ {U}) P
⊢ IsDeduct (evalPrimeFfToNot V '' Δ ∪ {U}) P
Tactic:
exact h3
Proof state after:
no goals
Theorem: FOL.NV.propCompleteAuxAux
Proof state before:
case h2
P U : Formula
Δ : Set Formula
h1_Δ : ∀ U' ∈ Δ, U'.IsPrime
h1_U : U.IsPrime
h2 : U ∉ Δ
h3 : ∀ (V : VarBoolAssignment), IsDeduct (evalPrimeFfToNot V '' Δ ∪ {evalPrimeFfToNot V U}) P
V : VarBoolAssignment
⊢ IsDeduct (evalPrimeFfToNot V '' Δ ∪ {U.not_}) P
Tactic:
specialize h3 (Function.updateITE V U Bool.false)
Proof state after:
case h2
P U : Formula
Δ : Set Formula
h1_Δ : ∀ U' ∈ Δ, U'.IsPrime
h1_U : U.IsPrime
h2 : U ∉ Δ
V : VarBoolAssignment
h3 :
  IsDeduct (evalPrimeFfToNot (Function.updateITE V U false) '' Δ ∪ {evalPrimeFfToNot (Function.updateITE V U false) U})
    P
⊢ IsDeduct (evalPrimeFfToNot V '' Δ ∪ {U.not_}) P
Theorem: FOL.NV.propCompleteAuxAux
Proof state before:
case h2
P U : Formula
Δ : Set Formula
h1_Δ : ∀ U' ∈ Δ, U'.IsPrime
h1_U : U.IsPrime
h2 : U ∉ Δ
V : VarBoolAssignment
h3 :
  IsDeduct (evalPrimeFfToNot (Function.updateITE V U false) '' Δ ∪ {evalPrimeFfToNot (Function.updateITE V U false) U})
    P
⊢ IsDeduct (evalPrimeFfToNot V '' Δ ∪ {U.not_}) P
Tactic:
simp only [image_of_evalPrimeFfToNot_of_function_updateIte U Δ V false h1_Δ h1_U h2] at h3
Proof state after:
case h2
P U : Formula
Δ : Set Formula
h1_Δ : ∀ U' ∈ Δ, U'.IsPrime
h1_U : U.IsPrime
h2 : U ∉ Δ
V : VarBoolAssignment
h3 : IsDeduct (evalPrimeFfToNot V '' Δ ∪ {evalPrimeFfToNot (Function.updateITE V U false) U}) P
⊢ IsDeduct (evalPrimeFfToNot V '' Δ ∪ {U.not_}) P
Theorem: FOL.NV.propCompleteAuxAux
Proof state before:
case h2
P U : Formula
Δ : Set Formula
h1_Δ : ∀ U' ∈ Δ, U'.IsPrime
h1_U : U.IsPrime
h2 : U ∉ Δ
V : VarBoolAssignment
h3 : IsDeduct (evalPrimeFfToNot V '' Δ ∪ {evalPrimeFfToNot (Function.updateITE V U false) U}) P
⊢ IsDeduct (evalPrimeFfToNot V '' Δ ∪ {U.not_}) P
Tactic:
simp only [evalPrimeFfToNot_of_function_updateIte_false U U V h1_U] at h3
Proof state after:
case h2
P U : Formula
Δ : Set Formula
h1_Δ : ∀ U' ∈ Δ, U'.IsPrime
h1_U : U.IsPrime
h2 : U ∉ Δ
V : VarBoolAssignment
h3 : IsDeduct (evalPrimeFfToNot V '' Δ ∪ {Function.updateITE (evalPrimeFfToNot V) U U.not_ U}) P
⊢ IsDeduct (evalPrimeFfToNot V '' Δ ∪ {U.not_}) P
Theorem: FOL.NV.propCompleteAuxAux
Proof state before:
case h2
P U : Formula
Δ : Set Formula
h1_Δ : ∀ U' ∈ Δ, U'.IsPrime
h1_U : U.IsPrime
h2 : U ∉ Δ
V : VarBoolAssignment
h3 : IsDeduct (evalPrimeFfToNot V '' Δ ∪ {Function.updateITE (evalPrimeFfToNot V) U U.not_ U}) P
⊢ IsDeduct (evalPrimeFfToNot V '' Δ ∪ {U.not_}) P
Tactic:
simp only [Function.updateITE] at h3
Proof state after:
case h2
P U : Formula
Δ : Set Formula
h1_Δ : ∀ U' ∈ Δ, U'.IsPrime
h1_U : U.IsPrime
h2 : U ∉ Δ
V : VarBoolAssignment
h3 : IsDeduct (evalPrimeFfToNot V '' Δ ∪ {if True then U.not_ else evalPrimeFfToNot V U}) P
⊢ IsDeduct (evalPrimeFfToNot V '' Δ ∪ {U.not_}) P
Theorem: FOL.NV.propCompleteAuxAux
Proof state before:
case h2
P U : Formula
Δ : Set Formula
h1_Δ : ∀ U' ∈ Δ, U'.IsPrime
h1_U : U.IsPrime
h2 : U ∉ Δ
V : VarBoolAssignment
h3 : IsDeduct (evalPrimeFfToNot V '' Δ ∪ {if True then U.not_ else evalPrimeFfToNot V U}) P
⊢ IsDeduct (evalPrimeFfToNot V '' Δ ∪ {U.not_}) P
Tactic:
simp only [eq_self_iff_true, if_true] at h3
Proof state after:
case h2
P U : Formula
Δ : Set Formula
h1_Δ : ∀ U' ∈ Δ, U'.IsPrime
h1_U : U.IsPrime
h2 : U ∉ Δ
V : VarBoolAssignment
h3 : IsDeduct (evalPrimeFfToNot V '' Δ ∪ {U.not_}) P
⊢ IsDeduct (evalPrimeFfToNot V '' Δ ∪ {U.not_}) P
Theorem: FOL.NV.propCompleteAuxAux
Proof state before:
case h2
P U : Formula
Δ : Set Formula
h1_Δ : ∀ U' ∈ Δ, U'.IsPrime
h1_U : U.IsPrime
h2 : U ∉ Δ
V : VarBoolAssignment
h3 : IsDeduct (evalPrimeFfToNot V '' Δ ∪ {U.not_}) P
⊢ IsDeduct (evalPrimeFfToNot V '' Δ ∪ {U.not_}) P
Tactic:
exact h3
Proof state after:
no goals
Theorem: FOL.NV.propCompleteAux
Proof state before:
P : Formula
Δ_U : Finset Formula
h1 : Δ_U ⊆ P.primeSet
h2 : ∀ (V : VarBoolAssignment), IsDeduct (↑(Finset.image (evalPrimeFfToNot V) Δ_U)) P
⊢ IsDeduct ∅ P
Tactic:
induction Δ_U using Finset.induction_on
Proof state after:
case empty
P : Formula
h1 : ∅ ⊆ P.primeSet
h2 : ∀ (V : VarBoolAssignment), IsDeduct (↑(Finset.image (evalPrimeFfToNot V) ∅)) P
⊢ IsDeduct ∅ P

case insert
P a✝² : Formula
s✝ : Finset Formula
a✝¹ : a✝² ∉ s✝
a✝ : s✝ ⊆ P.primeSet → (∀ (V : VarBoolAssignment), IsDeduct (↑(Finset.image (evalPrimeFfToNot V) s✝)) P) → IsDeduct ∅ P
h1 : insert a✝² s✝ ⊆ P.primeSet
h2 : ∀ (V : VarBoolAssignment), IsDeduct (↑(Finset.image (evalPrimeFfToNot V) (insert a✝² s✝))) P
⊢ IsDeduct ∅ P
Theorem: FOL.NV.propCompleteAux
Proof state before:
P : Formula
h1 : ∅ ⊆ P.primeSet
h2 : ∀ (V : VarBoolAssignment), IsDeduct (↑(Finset.image (evalPrimeFfToNot V) ∅)) P
⊢ IsDeduct ∅ P
Tactic:
case empty =>
  simp at h2
  exact h2
Proof state after:
no goals
Theorem: FOL.NV.propCompleteAux
Proof state before:
P : Formula
h1 : ∅ ⊆ P.primeSet
h2 : ∀ (V : VarBoolAssignment), IsDeduct (↑(Finset.image (evalPrimeFfToNot V) ∅)) P
⊢ IsDeduct ∅ P
Tactic:
simp at h2
Proof state after:
P : Formula
h1 : ∅ ⊆ P.primeSet
h2 : IsDeduct ∅ P
⊢ IsDeduct ∅ P
Theorem: FOL.NV.propCompleteAux
Proof state before:
P : Formula
h1 : ∅ ⊆ P.primeSet
h2 : IsDeduct ∅ P
⊢ IsDeduct ∅ P
Tactic:
exact h2
Proof state after:
no goals