Theorem: FOL.NV.L_15_7
Proof state before:
F : Formula
Δ_U : Set Formula
V : VarBoolAssignment
h1 : ↑F.primeSet ⊆ Δ_U
⊢ IsDeduct (evalPrimeFfToNot V '' Δ_U) (evalPrimeFfToNot V F)
Tactic:
induction F
Proof state after:
case pred_const_
Δ_U : Set Formula
V : VarBoolAssignment
a✝¹ : PredName
a✝ : List VarName
h1 : ↑(pred_const_ a✝¹ a✝).primeSet ⊆ Δ_U
⊢ IsDeduct (evalPrimeFfToNot V '' Δ_U) (evalPrimeFfToNot V (pred_const_ a✝¹ a✝))

case pred_var_
Δ_U : Set Formula
V : VarBoolAssignment
a✝¹ : PredName
a✝ : List VarName
h1 : ↑(pred_var_ a✝¹ a✝).primeSet ⊆ Δ_U
⊢ IsDeduct (evalPrimeFfToNot V '' Δ_U) (evalPrimeFfToNot V (pred_var_ a✝¹ a✝))

case eq_
Δ_U : Set Formula
V : VarBoolAssignment
a✝¹ a✝ : VarName
h1 : ↑(eq_ a✝¹ a✝).primeSet ⊆ Δ_U
⊢ IsDeduct (evalPrimeFfToNot V '' Δ_U) (evalPrimeFfToNot V (eq_ a✝¹ a✝))

case true_
Δ_U : Set Formula
V : VarBoolAssignment
h1 : ↑true_.primeSet ⊆ Δ_U
⊢ IsDeduct (evalPrimeFfToNot V '' Δ_U) (evalPrimeFfToNot V true_)

case false_
Δ_U : Set Formula
V : VarBoolAssignment
h1 : ↑false_.primeSet ⊆ Δ_U
⊢ IsDeduct (evalPrimeFfToNot V '' Δ_U) (evalPrimeFfToNot V false_)

case not_
Δ_U : Set Formula
V : VarBoolAssignment
a✝ : Formula
a_ih✝ : ↑a✝.primeSet ⊆ Δ_U → IsDeduct (evalPrimeFfToNot V '' Δ_U) (evalPrimeFfToNot V a✝)
h1 : ↑a✝.not_.primeSet ⊆ Δ_U
⊢ IsDeduct (evalPrimeFfToNot V '' Δ_U) (evalPrimeFfToNot V a✝.not_)

case imp_
Δ_U : Set Formula
V : VarBoolAssignment
a✝¹ a✝ : Formula
a_ih✝¹ : ↑a✝¹.primeSet ⊆ Δ_U → IsDeduct (evalPrimeFfToNot V '' Δ_U) (evalPrimeFfToNot V a✝¹)
a_ih✝ : ↑a✝.primeSet ⊆ Δ_U → IsDeduct (evalPrimeFfToNot V '' Δ_U) (evalPrimeFfToNot V a✝)
h1 : ↑(a✝¹.imp_ a✝).primeSet ⊆ Δ_U
⊢ IsDeduct (evalPrimeFfToNot V '' Δ_U) (evalPrimeFfToNot V (a✝¹.imp_ a✝))

case and_
Δ_U : Set Formula
V : VarBoolAssignment
a✝¹ a✝ : Formula
a_ih✝¹ : ↑a✝¹.primeSet ⊆ Δ_U → IsDeduct (evalPrimeFfToNot V '' Δ_U) (evalPrimeFfToNot V a✝¹)
a_ih✝ : ↑a✝.primeSet ⊆ Δ_U → IsDeduct (evalPrimeFfToNot V '' Δ_U) (evalPrimeFfToNot V a✝)
h1 : ↑(a✝¹.and_ a✝).primeSet ⊆ Δ_U
⊢ IsDeduct (evalPrimeFfToNot V '' Δ_U) (evalPrimeFfToNot V (a✝¹.and_ a✝))

case or_
Δ_U : Set Formula
V : VarBoolAssignment
a✝¹ a✝ : Formula
a_ih✝¹ : ↑a✝¹.primeSet ⊆ Δ_U → IsDeduct (evalPrimeFfToNot V '' Δ_U) (evalPrimeFfToNot V a✝¹)
a_ih✝ : ↑a✝.primeSet ⊆ Δ_U → IsDeduct (evalPrimeFfToNot V '' Δ_U) (evalPrimeFfToNot V a✝)
h1 : ↑(a✝¹.or_ a✝).primeSet ⊆ Δ_U
⊢ IsDeduct (evalPrimeFfToNot V '' Δ_U) (evalPrimeFfToNot V (a✝¹.or_ a✝))

case iff_
Δ_U : Set Formula
V : VarBoolAssignment
a✝¹ a✝ : Formula
a_ih✝¹ : ↑a✝¹.primeSet ⊆ Δ_U → IsDeduct (evalPrimeFfToNot V '' Δ_U) (evalPrimeFfToNot V a✝¹)
a_ih✝ : ↑a✝.primeSet ⊆ Δ_U → IsDeduct (evalPrimeFfToNot V '' Δ_U) (evalPrimeFfToNot V a✝)
h1 : ↑(a✝¹.iff_ a✝).primeSet ⊆ Δ_U
⊢ IsDeduct (evalPrimeFfToNot V '' Δ_U) (evalPrimeFfToNot V (a✝¹.iff_ a✝))

case forall_
Δ_U : Set Formula
V : VarBoolAssignment
a✝¹ : VarName
a✝ : Formula
a_ih✝ : ↑a✝.primeSet ⊆ Δ_U → IsDeduct (evalPrimeFfToNot V '' Δ_U) (evalPrimeFfToNot V a✝)
h1 : ↑(forall_ a✝¹ a✝).primeSet ⊆ Δ_U
⊢ IsDeduct (evalPrimeFfToNot V '' Δ_U) (evalPrimeFfToNot V (forall_ a✝¹ a✝))

case exists_
Δ_U : Set Formula
V : VarBoolAssignment
a✝¹ : VarName
a✝ : Formula
a_ih✝ : ↑a✝.primeSet ⊆ Δ_U → IsDeduct (evalPrimeFfToNot V '' Δ_U) (evalPrimeFfToNot V a✝)
h1 : ↑(exists_ a✝¹ a✝).primeSet ⊆ Δ_U
⊢ IsDeduct (evalPrimeFfToNot V '' Δ_U) (evalPrimeFfToNot V (exists_ a✝¹ a✝))

case def_
Δ_U : Set Formula
V : VarBoolAssignment
a✝¹ : DefName
a✝ : List VarName
h1 : ↑(def_ a✝¹ a✝).primeSet ⊆ Δ_U
⊢ IsDeduct (evalPrimeFfToNot V '' Δ_U) (evalPrimeFfToNot V (def_ a✝¹ a✝))