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

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
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

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))
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

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)
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

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
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

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
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

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
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

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
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

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
State after:
no goals

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)
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

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
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

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
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

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
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

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
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

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
State after:
no goals