internlm/Lean-Github huggingface dataset:
Theorem: FOL.NV.mem_primeSet_isPrime
Proof state before:
F' : Formula
h1 : F' ∈ false_.primeSet
⊢ F'.IsPrime
Tactic:
simp only [Formula.primeSet] at h1
Proof state after:
F' : Formula
h1 : F' ∈ ∅
⊢ F'.IsPrime
Theorem: FOL.NV.mem_primeSet_isPrime
Proof state before:
F' : Formula
h1 : F' ∈ ∅
⊢ F'.IsPrime
Tactic:
simp at h1
Proof state after:
no goals
Theorem: FOL.NV.mem_primeSet_isPrime
Proof state before:
F' : Formula
x y : VarName
h1 : F' ∈ (eq_ x y).primeSet
⊢ F'.IsPrime
Tactic:
simp only [Formula.primeSet] at h1
Proof state after:
F' : Formula
x y : VarName
h1 : F' ∈ {eq_ x y}
⊢ F'.IsPrime
Theorem: FOL.NV.mem_primeSet_isPrime
Proof state before:
F' : Formula
x y : VarName
h1 : F' ∈ {eq_ x y}
⊢ F'.IsPrime
Tactic:
simp at h1
Proof state after:
F' : Formula
x y : VarName
h1 : F' = eq_ x y
⊢ F'.IsPrime
Theorem: FOL.NV.mem_primeSet_isPrime
Proof state before:
F' : Formula
x y : VarName
h1 : F' = eq_ x y
⊢ F'.IsPrime
Tactic:
subst h1
Proof state after:
x y : VarName
⊢ (eq_ x y).IsPrime
Theorem: FOL.NV.mem_primeSet_isPrime
Proof state before:
x y : VarName
⊢ (eq_ x y).IsPrime
Tactic:
simp only [Formula.IsPrime]
Proof state after:
no goals
Theorem: FOL.NV.mem_primeSet_isPrime
Proof state before:
F' phi : Formula
phi_ih : F' ∈ phi.primeSet → F'.IsPrime
h1 : F' ∈ phi.not_.primeSet
⊢ F'.IsPrime
Tactic:
simp only [Formula.primeSet] at h1
Proof state after:
F' phi : Formula
phi_ih : F' ∈ phi.primeSet → F'.IsPrime
h1 : F' ∈ phi.primeSet
⊢ F'.IsPrime
Theorem: FOL.NV.mem_primeSet_isPrime
Proof state before:
F' phi : Formula
phi_ih : F' ∈ phi.primeSet → F'.IsPrime
h1 : F' ∈ phi.primeSet
⊢ F'.IsPrime
Tactic:
exact phi_ih h1
Proof state after:
no goals
Theorem: FOL.NV.mem_primeSet_isPrime
Proof state before:
F' phi psi : Formula
phi_ih : F' ∈ phi.primeSet → F'.IsPrime
psi_ih : F' ∈ psi.primeSet → F'.IsPrime
h1 : F' ∈ (phi.iff_ psi).primeSet
⊢ F'.IsPrime
Tactic:
simp only [Formula.primeSet] at h1
Proof state after:
F' phi psi : Formula
phi_ih : F' ∈ phi.primeSet → F'.IsPrime
psi_ih : F' ∈ psi.primeSet → F'.IsPrime
h1 : F' ∈ phi.primeSet ∪ psi.primeSet
⊢ F'.IsPrime
Theorem: FOL.NV.mem_primeSet_isPrime
Proof state before:
F' phi psi : Formula
phi_ih : F' ∈ phi.primeSet → F'.IsPrime
psi_ih : F' ∈ psi.primeSet → F'.IsPrime
h1 : F' ∈ phi.primeSet ∪ psi.primeSet
⊢ F'.IsPrime
Tactic:
simp at h1
Proof state after:
F' phi psi : Formula
phi_ih : F' ∈ phi.primeSet → F'.IsPrime
psi_ih : F' ∈ psi.primeSet → F'.IsPrime
h1 : F' ∈ phi.primeSet ∨ F' ∈ psi.primeSet
⊢ F'.IsPrime
Theorem: FOL.NV.mem_primeSet_isPrime
Proof state before:
F' phi psi : Formula
phi_ih : F' ∈ phi.primeSet → F'.IsPrime
psi_ih : F' ∈ psi.primeSet → F'.IsPrime
h1 : F' ∈ phi.primeSet ∨ F' ∈ psi.primeSet
⊢ F'.IsPrime
Tactic:
tauto
Proof state after:
no goals
Theorem: FOL.NV.mem_primeSet_isPrime
Proof state before:
F' : Formula
a✝ : VarName
x : Formula
phi : F' ∈ x.primeSet → F'.IsPrime
h1 : F' ∈ (exists_ a✝ x).primeSet
⊢ F'.IsPrime
Tactic:
simp only [Formula.primeSet] at h1
Proof state after:
F' : Formula
a✝ : VarName
x : Formula
phi : F' ∈ x.primeSet → F'.IsPrime
h1 : F' ∈ {exists_ a✝ x}
⊢ F'.IsPrime
Theorem: FOL.NV.mem_primeSet_isPrime
Proof state before:
F' : Formula
a✝ : VarName
x : Formula
phi : F' ∈ x.primeSet → F'.IsPrime
h1 : F' ∈ {exists_ a✝ x}
⊢ F'.IsPrime
Tactic:
simp at h1
Proof state after:
F' : Formula
a✝ : VarName
x : Formula
phi : F' ∈ x.primeSet → F'.IsPrime
h1 : F' = exists_ a✝ x
⊢ F'.IsPrime
Theorem: FOL.NV.mem_primeSet_isPrime
Proof state before:
F' : Formula
a✝ : VarName
x : Formula
phi : F' ∈ x.primeSet → F'.IsPrime
h1 : F' = exists_ a✝ x
⊢ F'.IsPrime
Tactic:
subst h1
Proof state after:
a✝ : VarName
x : Formula
phi : exists_ a✝ x ∈ x.primeSet → (exists_ a✝ x).IsPrime
⊢ (exists_ a✝ x).IsPrime
Theorem: FOL.NV.mem_primeSet_isPrime
Proof state before:
a✝ : VarName
x : Formula
phi : exists_ a✝ x ∈ x.primeSet → (exists_ a✝ x).IsPrime
⊢ (exists_ a✝ x).IsPrime
Tactic:
simp only [Formula.IsPrime]
Proof state after:
no goals
Theorem: FOL.NV.mem_primeSet_isPrime
Proof state before:
F' : Formula
a✝¹ : DefName
a✝ : List VarName
h1 : F' ∈ (def_ a✝¹ a✝).primeSet
⊢ F'.IsPrime
Tactic:
simp only [Formula.primeSet] at h1
Proof state after:
F' : Formula
a✝¹ : DefName
a✝ : List VarName
h1 : F' ∈ {def_ a✝¹ a✝}
⊢ F'.IsPrime
Theorem: FOL.NV.mem_primeSet_isPrime
Proof state before:
F' : Formula
a✝¹ : DefName
a✝ : List VarName
h1 : F' ∈ {def_ a✝¹ a✝}
⊢ F'.IsPrime
Tactic:
simp at h1
Proof state after:
F' : Formula
a✝¹ : DefName
a✝ : List VarName
h1 : F' = def_ a✝¹ a✝
⊢ F'.IsPrime
Theorem: FOL.NV.mem_primeSet_isPrime
Proof state before:
F' : Formula
a✝¹ : DefName
a✝ : List VarName
h1 : F' = def_ a✝¹ a✝
⊢ F'.IsPrime
Tactic:
subst h1
Proof state after:
a✝¹ : DefName
a✝ : List VarName
⊢ (def_ a✝¹ a✝).IsPrime
Theorem: FOL.NV.mem_primeSet_isPrime
Proof state before:
a✝¹ : DefName
a✝ : List VarName
⊢ (def_ a✝¹ a✝).IsPrime
Tactic:
simp only [Formula.IsPrime]
Proof state after:
no goals
Theorem: FOL.NV.L_15_7
Proof state before:
F F' : Formula
Δ_U : Set Formula
V : VarBoolAssignment
Δ_U' : Set Formula
h1 : ↑F.primeSet ⊆ Δ_U
h2 : Δ_U' = evalPrimeFfToNot V '' Δ_U
h3 : F' = evalPrimeFfToNot V F
⊢ IsDeduct Δ_U' F'
Tactic:
subst h2
Proof state after:
F F' : Formula
Δ_U : Set Formula
V : VarBoolAssignment
h1 : ↑F.primeSet ⊆ Δ_U
h3 : F' = evalPrimeFfToNot V F
⊢ IsDeduct (evalPrimeFfToNot V '' Δ_U) F'
Theorem: FOL.NV.L_15_7
Proof state before:
F F' : Formula
Δ_U : Set Formula
V : VarBoolAssignment
h1 : ↑F.primeSet ⊆ Δ_U
h3 : F' = evalPrimeFfToNot V F
⊢ IsDeduct (evalPrimeFfToNot V '' Δ_U) F'
Tactic:
subst h3
Proof state after:
F : Formula
Δ_U : Set Formula
V : VarBoolAssignment
h1 : ↑F.primeSet ⊆ Δ_U
⊢ IsDeduct (evalPrimeFfToNot V '' Δ_U) (evalPrimeFfToNot V F)
Theorem: FOL.NV.L_15_7
Proof state before:
Δ_U : Set Formula
V : VarBoolAssignment
X : PredName
xs : List VarName
h1 : ↑(pred_const_ X xs).primeSet ⊆ Δ_U
⊢ IsDeduct (evalPrimeFfToNot V '' Δ_U) (evalPrimeFfToNot V (pred_const_ X xs))
Tactic:
case pred_const_ X xs =>
  let F := pred_const_ X xs
  simp only [Formula.primeSet] at h1
  simp at h1
  simp only [evalPrimeFfToNot]
  simp only [Formula.evalPrime]
  apply IsDeduct.assume_
  simp
  apply Exists.intro F
  tauto
Proof state after:
no goals
Theorem: FOL.NV.L_15_7
Proof state before:
Δ_U : Set Formula
V : VarBoolAssignment
X : PredName
xs : List VarName
h1 : ↑(pred_var_ X xs).primeSet ⊆ Δ_U
⊢ IsDeduct (evalPrimeFfToNot V '' Δ_U) (evalPrimeFfToNot V (pred_var_ X xs))
Tactic:
case pred_var_ X xs =>
  let F := pred_var_ X xs
  simp only [Formula.primeSet] at h1
  simp at h1
  simp only [evalPrimeFfToNot]
  simp only [Formula.evalPrime]
  apply IsDeduct.assume_
  simp
  apply Exists.intro F
  tauto
Proof state after:
no goals
Theorem: FOL.NV.L_15_7
Proof state before:
Δ_U : Set Formula
V : VarBoolAssignment
x y : VarName
h1 : ↑(eq_ x y).primeSet ⊆ Δ_U
⊢ IsDeduct (evalPrimeFfToNot V '' Δ_U) (evalPrimeFfToNot V (eq_ x y))
Tactic:
case eq_ x y =>
  let F := eq_ x y
  simp only [Formula.primeSet] at h1
  simp at h1
  simp only [evalPrimeFfToNot]
  simp only [Formula.evalPrime]
  apply IsDeduct.assume_
  simp
  apply Exists.intro F
  tauto
Proof state after:
no goals
Theorem: FOL.NV.L_15_7
Proof state before:
Δ_U : Set Formula
V : VarBoolAssignment
h1 : ↑true_.primeSet ⊆ Δ_U
⊢ IsDeduct (evalPrimeFfToNot V '' Δ_U) (evalPrimeFfToNot V true_)
Tactic:
case true_ =>
  apply IsDeduct.axiom_
  apply IsAxiom.prop_true_
Proof state after:
no goals
Theorem: FOL.NV.L_15_7
Proof state before:
Δ_U : Set Formula
V : VarBoolAssignment
h1 : ↑false_.primeSet ⊆ Δ_U
⊢ IsDeduct (evalPrimeFfToNot V '' Δ_U) (evalPrimeFfToNot V false_)
Tactic:
case false_ =>
  simp only [Formula.primeSet] at h1
  simp at h1
  simp only [evalPrimeFfToNot]
  simp only [Formula.evalPrime]
  simp
  sorry
Proof state after:
no goals
Theorem: FOL.NV.L_15_7
Proof state before:
Δ_U : Set Formula
V : VarBoolAssignment
phi : Formula
phi_ih : ↑phi.primeSet ⊆ Δ_U → IsDeduct (evalPrimeFfToNot V '' Δ_U) (evalPrimeFfToNot V phi)
h1 : ↑phi.not_.primeSet ⊆ Δ_U
⊢ IsDeduct (evalPrimeFfToNot V '' Δ_U) (evalPrimeFfToNot V phi.not_)
Tactic:
case not_ phi phi_ih =>
  simp only [Formula.primeSet] at h1
  simp only [evalPrimeFfToNot] at phi_ih
  simp only [evalPrimeFfToNot]
  simp only [evalPrime]
  simp
  split_ifs
  case _ c1 =>
    simp only [c1] at phi_ih
    simp at phi_ih
    apply IsDeduct.mp_ phi
    apply proof_imp_deduct
    apply T_14_6
    exact phi_ih h1
  case _ c1 =>
    simp only [c1] at phi_ih
    simp at phi_ih
    exact phi_ih h1
Proof state after:
no goals
Theorem: FOL.NV.L_15_7
Proof state before:
Δ_U : Set Formula
V : VarBoolAssignment
x : VarName
phi : Formula
phi_ih : ↑phi.primeSet ⊆ Δ_U → IsDeduct (evalPrimeFfToNot V '' Δ_U) (evalPrimeFfToNot V phi)
h1 : ↑(forall_ x phi).primeSet ⊆ Δ_U
⊢ IsDeduct (evalPrimeFfToNot V '' Δ_U) (evalPrimeFfToNot V (forall_ x phi))
Tactic:
case forall_ x phi phi_ih =>
  let F := forall_ x phi
  simp only [Formula.primeSet] at h1
  simp at h1
  simp only [evalPrimeFfToNot]
  simp only [Formula.evalPrime]
  apply IsDeduct.assume_
  simp
  apply Exists.intro F
  tauto
Proof state after:
no goals
Theorem: FOL.NV.L_15_7
Proof state before:
Δ_U : Set Formula
V : VarBoolAssignment
X : DefName
xs : List VarName
h1 : ↑(def_ X xs).primeSet ⊆ Δ_U
⊢ IsDeduct (evalPrimeFfToNot V '' Δ_U) (evalPrimeFfToNot V (def_ X xs))
Tactic:
case def_ X xs =>
  let F := def_ X xs
  simp only [Formula.primeSet] at h1
  simp at h1
  simp only [evalPrimeFfToNot]
  simp only [Formula.evalPrime]
  apply IsDeduct.assume_
  simp
  apply Exists.intro F
  tauto
Proof state after:
no goals
Theorem: FOL.NV.L_15_7
Proof state before:
Δ_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✝))
Tactic:
case and_ | or_ | iff_ | exists_ =>
  sorry
Proof state after:
no goals
Theorem: FOL.NV.L_15_7
Proof state before:
Δ_U : Set Formula
V : VarBoolAssignment
X : PredName
xs : List VarName
h1 : ↑(pred_const_ X xs).primeSet ⊆ Δ_U
⊢ IsDeduct (evalPrimeFfToNot V '' Δ_U) (evalPrimeFfToNot V (pred_const_ X xs))
Tactic:
let F := pred_const_ X xs
Proof state after:
Δ_U : Set Formula
V : VarBoolAssignment
X : PredName
xs : List VarName
h1 : ↑(pred_const_ X xs).primeSet ⊆ Δ_U
F : Formula := pred_const_ X xs
⊢ IsDeduct (evalPrimeFfToNot V '' Δ_U) (evalPrimeFfToNot V (pred_const_ X xs))
Theorem: FOL.NV.L_15_7
Proof state before:
Δ_U : Set Formula
V : VarBoolAssignment
X : PredName
xs : List VarName
h1 : ↑(pred_const_ X xs).primeSet ⊆ Δ_U
F : Formula := pred_const_ X xs
⊢ IsDeduct (evalPrimeFfToNot V '' Δ_U) (evalPrimeFfToNot V (pred_const_ X xs))
Tactic:
simp only [Formula.primeSet] at h1
Proof state after:
Δ_U : Set Formula
V : VarBoolAssignment
X : PredName
xs : List VarName
h1 : ↑{pred_const_ X xs} ⊆ Δ_U
F : Formula := pred_const_ X xs
⊢ IsDeduct (evalPrimeFfToNot V '' Δ_U) (evalPrimeFfToNot V (pred_const_ X xs))
Theorem: FOL.NV.L_15_7
Proof state before:
Δ_U : Set Formula
V : VarBoolAssignment
X : PredName
xs : List VarName
h1 : ↑{pred_const_ X xs} ⊆ Δ_U
F : Formula := pred_const_ X xs
⊢ IsDeduct (evalPrimeFfToNot V '' Δ_U) (evalPrimeFfToNot V (pred_const_ X xs))
Tactic:
simp at h1
Proof state after:
Δ_U : Set Formula
V : VarBoolAssignment
X : PredName
xs : List VarName
F : Formula := pred_const_ X xs
h1 : pred_const_ X xs ∈ Δ_U
⊢ IsDeduct (evalPrimeFfToNot V '' Δ_U) (evalPrimeFfToNot V (pred_const_ X xs))
Theorem: FOL.NV.L_15_7
Proof state before:
Δ_U : Set Formula
V : VarBoolAssignment
X : PredName
xs : List VarName
F : Formula := pred_const_ X xs
h1 : pred_const_ X xs ∈ Δ_U
⊢ IsDeduct (evalPrimeFfToNot V '' Δ_U) (evalPrimeFfToNot V (pred_const_ X xs))
Tactic:
simp only [evalPrimeFfToNot]
Proof state after:
Δ_U : Set Formula
V : VarBoolAssignment
X : PredName
xs : List VarName
F : Formula := pred_const_ X xs
h1 : pred_const_ X xs ∈ Δ_U
⊢ IsDeduct ((fun a => if evalPrime V a then a else a.not_) '' Δ_U)
    (if evalPrime V (pred_const_ X xs) then pred_const_ X xs else (pred_const_ X xs).not_)
Theorem: FOL.NV.L_15_7
Proof state before:
Δ_U : Set Formula
V : VarBoolAssignment
X : PredName
xs : List VarName
F : Formula := pred_const_ X xs
h1 : pred_const_ X xs ∈ Δ_U
⊢ IsDeduct ((fun a => if evalPrime V a then a else a.not_) '' Δ_U)
    (if evalPrime V (pred_const_ X xs) then pred_const_ X xs else (pred_const_ X xs).not_)
Tactic:
simp only [Formula.evalPrime]
Proof state after:
Δ_U : Set Formula
V : VarBoolAssignment
X : PredName
xs : List VarName
F : Formula := pred_const_ X xs
h1 : pred_const_ X xs ∈ Δ_U
⊢ IsDeduct ((fun a => if evalPrime V a then a else a.not_) '' Δ_U)
    (if V (pred_const_ X xs) = true then pred_const_ X xs else (pred_const_ X xs).not_)
Theorem: FOL.NV.L_15_7
Proof state before:
Δ_U : Set Formula
V : VarBoolAssignment
X : PredName
xs : List VarName
F : Formula := pred_const_ X xs
h1 : pred_const_ X xs ∈ Δ_U
⊢ IsDeduct ((fun a => if evalPrime V a then a else a.not_) '' Δ_U)
    (if V (pred_const_ X xs) = true then pred_const_ X xs else (pred_const_ X xs).not_)
Tactic:
apply IsDeduct.assume_
Proof state after:
case a
Δ_U : Set Formula
V : VarBoolAssignment
X : PredName
xs : List VarName
F : Formula := pred_const_ X xs
h1 : pred_const_ X xs ∈ Δ_U
⊢ (if V (pred_const_ X xs) = true then pred_const_ X xs else (pred_const_ X xs).not_) ∈
    (fun a => if evalPrime V a then a else a.not_) '' Δ_U
Theorem: FOL.NV.L_15_7
Proof state before:
case a
Δ_U : Set Formula
V : VarBoolAssignment
X : PredName
xs : List VarName
F : Formula := pred_const_ X xs
h1 : pred_const_ X xs ∈ Δ_U
⊢ (if V (pred_const_ X xs) = true then pred_const_ X xs else (pred_const_ X xs).not_) ∈
    (fun a => if evalPrime V a then a else a.not_) '' Δ_U
Tactic:
simp
Proof state after:
case a
Δ_U : Set Formula
V : VarBoolAssignment
X : PredName
xs : List VarName
F : Formula := pred_const_ X xs
h1 : pred_const_ X xs ∈ Δ_U
⊢ ∃ x ∈ Δ_U,
    (if evalPrime V x then x else x.not_) =
      if V (pred_const_ X xs) = true then pred_const_ X xs else (pred_const_ X xs).not_
Theorem: FOL.NV.L_15_7
Proof state before:
case a
Δ_U : Set Formula
V : VarBoolAssignment
X : PredName
xs : List VarName
F : Formula := pred_const_ X xs
h1 : pred_const_ X xs ∈ Δ_U
⊢ ∃ x ∈ Δ_U,
    (if evalPrime V x then x else x.not_) =
      if V (pred_const_ X xs) = true then pred_const_ X xs else (pred_const_ X xs).not_
Tactic:
apply Exists.intro F
Proof state after:
case a
Δ_U : Set Formula
V : VarBoolAssignment
X : PredName
xs : List VarName
F : Formula := pred_const_ X xs
h1 : pred_const_ X xs ∈ Δ_U
⊢ F ∈ Δ_U ∧
    (if evalPrime V F then F else F.not_) =
      if V (pred_const_ X xs) = true then pred_const_ X xs else (pred_const_ X xs).not_
Theorem: FOL.NV.L_15_7
Proof state before:
case a
Δ_U : Set Formula
V : VarBoolAssignment
X : PredName
xs : List VarName
F : Formula := pred_const_ X xs
h1 : pred_const_ X xs ∈ Δ_U
⊢ F ∈ Δ_U ∧
    (if evalPrime V F then F else F.not_) =
      if V (pred_const_ X xs) = true then pred_const_ X xs else (pred_const_ X xs).not_
Tactic:
tauto
Proof state after:
no goals
Theorem: FOL.NV.L_15_7
Proof state before:
Δ_U : Set Formula
V : VarBoolAssignment
X : PredName
xs : List VarName
h1 : ↑(pred_var_ X xs).primeSet ⊆ Δ_U
⊢ IsDeduct (evalPrimeFfToNot V '' Δ_U) (evalPrimeFfToNot V (pred_var_ X xs))
Tactic:
let F := pred_var_ X xs
Proof state after:
Δ_U : Set Formula
V : VarBoolAssignment
X : PredName
xs : List VarName
h1 : ↑(pred_var_ X xs).primeSet ⊆ Δ_U
F : Formula := pred_var_ X xs
⊢ IsDeduct (evalPrimeFfToNot V '' Δ_U) (evalPrimeFfToNot V (pred_var_ X xs))
Theorem: FOL.NV.L_15_7
Proof state before:
Δ_U : Set Formula
V : VarBoolAssignment
X : PredName
xs : List VarName
h1 : ↑(pred_var_ X xs).primeSet ⊆ Δ_U
F : Formula := pred_var_ X xs
⊢ IsDeduct (evalPrimeFfToNot V '' Δ_U) (evalPrimeFfToNot V (pred_var_ X xs))
Tactic:
simp only [Formula.primeSet] at h1
Proof state after:
Δ_U : Set Formula
V : VarBoolAssignment
X : PredName
xs : List VarName
h1 : ↑{pred_var_ X xs} ⊆ Δ_U
F : Formula := pred_var_ X xs
⊢ IsDeduct (evalPrimeFfToNot V '' Δ_U) (evalPrimeFfToNot V (pred_var_ X xs))
Theorem: FOL.NV.L_15_7
Proof state before:
Δ_U : Set Formula
V : VarBoolAssignment
X : PredName
xs : List VarName
h1 : ↑{pred_var_ X xs} ⊆ Δ_U
F : Formula := pred_var_ X xs
⊢ IsDeduct (evalPrimeFfToNot V '' Δ_U) (evalPrimeFfToNot V (pred_var_ X xs))
Tactic:
simp at h1
Proof state after:
Δ_U : Set Formula
V : VarBoolAssignment
X : PredName
xs : List VarName
F : Formula := pred_var_ X xs
h1 : pred_var_ X xs ∈ Δ_U
⊢ IsDeduct (evalPrimeFfToNot V '' Δ_U) (evalPrimeFfToNot V (pred_var_ X xs))
Theorem: FOL.NV.L_15_7
Proof state before:
Δ_U : Set Formula
V : VarBoolAssignment
X : PredName
xs : List VarName
F : Formula := pred_var_ X xs
h1 : pred_var_ X xs ∈ Δ_U
⊢ IsDeduct (evalPrimeFfToNot V '' Δ_U) (evalPrimeFfToNot V (pred_var_ X xs))
Tactic:
simp only [evalPrimeFfToNot]
Proof state after:
Δ_U : Set Formula
V : VarBoolAssignment
X : PredName
xs : List VarName
F : Formula := pred_var_ X xs
h1 : pred_var_ X xs ∈ Δ_U
⊢ IsDeduct ((fun a => if evalPrime V a then a else a.not_) '' Δ_U)
    (if evalPrime V (pred_var_ X xs) then pred_var_ X xs else (pred_var_ X xs).not_)
Theorem: FOL.NV.L_15_7
Proof state before:
Δ_U : Set Formula
V : VarBoolAssignment
X : PredName
xs : List VarName
F : Formula := pred_var_ X xs
h1 : pred_var_ X xs ∈ Δ_U
⊢ IsDeduct ((fun a => if evalPrime V a then a else a.not_) '' Δ_U)
    (if evalPrime V (pred_var_ X xs) then pred_var_ X xs else (pred_var_ X xs).not_)
Tactic:
simp only [Formula.evalPrime]
Proof state after:
Δ_U : Set Formula
V : VarBoolAssignment
X : PredName
xs : List VarName
F : Formula := pred_var_ X xs
h1 : pred_var_ X xs ∈ Δ_U
⊢ IsDeduct ((fun a => if evalPrime V a then a else a.not_) '' Δ_U)
    (if V (pred_var_ X xs) = true then pred_var_ X xs else (pred_var_ X xs).not_)
Theorem: FOL.NV.L_15_7
Proof state before:
Δ_U : Set Formula
V : VarBoolAssignment
X : PredName
xs : List VarName
F : Formula := pred_var_ X xs
h1 : pred_var_ X xs ∈ Δ_U
⊢ IsDeduct ((fun a => if evalPrime V a then a else a.not_) '' Δ_U)
    (if V (pred_var_ X xs) = true then pred_var_ X xs else (pred_var_ X xs).not_)
Tactic:
apply IsDeduct.assume_
Proof state after:
case a
Δ_U : Set Formula
V : VarBoolAssignment
X : PredName
xs : List VarName
F : Formula := pred_var_ X xs
h1 : pred_var_ X xs ∈ Δ_U
⊢ (if V (pred_var_ X xs) = true then pred_var_ X xs else (pred_var_ X xs).not_) ∈
    (fun a => if evalPrime V a then a else a.not_) '' Δ_U
Theorem: FOL.NV.L_15_7
Proof state before:
case a
Δ_U : Set Formula
V : VarBoolAssignment
X : PredName
xs : List VarName
F : Formula := pred_var_ X xs
h1 : pred_var_ X xs ∈ Δ_U
⊢ (if V (pred_var_ X xs) = true then pred_var_ X xs else (pred_var_ X xs).not_) ∈
    (fun a => if evalPrime V a then a else a.not_) '' Δ_U
Tactic:
simp
Proof state after:
case a
Δ_U : Set Formula
V : VarBoolAssignment
X : PredName
xs : List VarName
F : Formula := pred_var_ X xs
h1 : pred_var_ X xs ∈ Δ_U
⊢ ∃ x ∈ Δ_U,
    (if evalPrime V x then x else x.not_) = if V (pred_var_ X xs) = true then pred_var_ X xs else (pred_var_ X xs).not_
Theorem: FOL.NV.L_15_7
Proof state before:
case a
Δ_U : Set Formula
V : VarBoolAssignment
X : PredName
xs : List VarName
F : Formula := pred_var_ X xs
h1 : pred_var_ X xs ∈ Δ_U
⊢ ∃ x ∈ Δ_U,
    (if evalPrime V x then x else x.not_) = if V (pred_var_ X xs) = true then pred_var_ X xs else (pred_var_ X xs).not_
Tactic:
apply Exists.intro F
Proof state after:
case a
Δ_U : Set Formula
V : VarBoolAssignment
X : PredName
xs : List VarName
F : Formula := pred_var_ X xs
h1 : pred_var_ X xs ∈ Δ_U
⊢ F ∈ Δ_U ∧
    (if evalPrime V F then F else F.not_) = if V (pred_var_ X xs) = true then pred_var_ X xs else (pred_var_ X xs).not_
Theorem: FOL.NV.L_15_7
Proof state before:
case a
Δ_U : Set Formula
V : VarBoolAssignment
X : PredName
xs : List VarName
F : Formula := pred_var_ X xs
h1 : pred_var_ X xs ∈ Δ_U
⊢ F ∈ Δ_U ∧
    (if evalPrime V F then F else F.not_) = if V (pred_var_ X xs) = true then pred_var_ X xs else (pred_var_ X xs).not_
Tactic:
tauto
Proof state after:
no goals
Theorem: FOL.NV.L_15_7
Proof state before:
Δ_U : Set Formula
V : VarBoolAssignment
x y : VarName
h1 : ↑(eq_ x y).primeSet ⊆ Δ_U
⊢ IsDeduct (evalPrimeFfToNot V '' Δ_U) (evalPrimeFfToNot V (eq_ x y))
Tactic:
let F := eq_ x y
Proof state after:
Δ_U : Set Formula
V : VarBoolAssignment
x y : VarName
h1 : ↑(eq_ x y).primeSet ⊆ Δ_U
F : Formula := eq_ x y
⊢ IsDeduct (evalPrimeFfToNot V '' Δ_U) (evalPrimeFfToNot V (eq_ x y))
Theorem: FOL.NV.L_15_7
Proof state before:
Δ_U : Set Formula
V : VarBoolAssignment
x y : VarName
h1 : ↑(eq_ x y).primeSet ⊆ Δ_U
F : Formula := eq_ x y
⊢ IsDeduct (evalPrimeFfToNot V '' Δ_U) (evalPrimeFfToNot V (eq_ x y))
Tactic:
simp only [Formula.primeSet] at h1
Proof state after:
Δ_U : Set Formula
V : VarBoolAssignment
x y : VarName
h1 : ↑{eq_ x y} ⊆ Δ_U
F : Formula := eq_ x y
⊢ IsDeduct (evalPrimeFfToNot V '' Δ_U) (evalPrimeFfToNot V (eq_ x y))
Theorem: FOL.NV.L_15_7
Proof state before:
Δ_U : Set Formula
V : VarBoolAssignment
x y : VarName
h1 : ↑{eq_ x y} ⊆ Δ_U
F : Formula := eq_ x y
⊢ IsDeduct (evalPrimeFfToNot V '' Δ_U) (evalPrimeFfToNot V (eq_ x y))
Tactic:
simp at h1
Proof state after:
Δ_U : Set Formula
V : VarBoolAssignment
x y : VarName
F : Formula := eq_ x y
h1 : eq_ x y ∈ Δ_U
⊢ IsDeduct (evalPrimeFfToNot V '' Δ_U) (evalPrimeFfToNot V (eq_ x y))
Theorem: FOL.NV.L_15_7
Proof state before:
Δ_U : Set Formula
V : VarBoolAssignment
x y : VarName
F : Formula := eq_ x y
h1 : eq_ x y ∈ Δ_U
⊢ IsDeduct (evalPrimeFfToNot V '' Δ_U) (evalPrimeFfToNot V (eq_ x y))
Tactic:
simp only [evalPrimeFfToNot]
Proof state after:
Δ_U : Set Formula
V : VarBoolAssignment
x y : VarName
F : Formula := eq_ x y
h1 : eq_ x y ∈ Δ_U
⊢ IsDeduct ((fun a => if evalPrime V a then a else a.not_) '' Δ_U)
    (if evalPrime V (eq_ x y) then eq_ x y else (eq_ x y).not_)
Theorem: FOL.NV.L_15_7
Proof state before:
Δ_U : Set Formula
V : VarBoolAssignment
x y : VarName
F : Formula := eq_ x y
h1 : eq_ x y ∈ Δ_U
⊢ IsDeduct ((fun a => if evalPrime V a then a else a.not_) '' Δ_U)
    (if evalPrime V (eq_ x y) then eq_ x y else (eq_ x y).not_)
Tactic:
simp only [Formula.evalPrime]
Proof state after:
Δ_U : Set Formula
V : VarBoolAssignment
x y : VarName
F : Formula := eq_ x y
h1 : eq_ x y ∈ Δ_U
⊢ IsDeduct ((fun a => if evalPrime V a then a else a.not_) '' Δ_U)
    (if V (eq_ x y) = true then eq_ x y else (eq_ x y).not_)
Theorem: FOL.NV.L_15_7
Proof state before:
Δ_U : Set Formula
V : VarBoolAssignment
x y : VarName
F : Formula := eq_ x y
h1 : eq_ x y ∈ Δ_U
⊢ IsDeduct ((fun a => if evalPrime V a then a else a.not_) '' Δ_U)
    (if V (eq_ x y) = true then eq_ x y else (eq_ x y).not_)
Tactic:
apply IsDeduct.assume_
Proof state after:
case a
Δ_U : Set Formula
V : VarBoolAssignment
x y : VarName
F : Formula := eq_ x y
h1 : eq_ x y ∈ Δ_U
⊢ (if V (eq_ x y) = true then eq_ x y else (eq_ x y).not_) ∈ (fun a => if evalPrime V a then a else a.not_) '' Δ_U
Theorem: FOL.NV.L_15_7
Proof state before:
case a
Δ_U : Set Formula
V : VarBoolAssignment
x y : VarName
F : Formula := eq_ x y
h1 : eq_ x y ∈ Δ_U
⊢ (if V (eq_ x y) = true then eq_ x y else (eq_ x y).not_) ∈ (fun a => if evalPrime V a then a else a.not_) '' Δ_U
Tactic:
simp
Proof state after:
case a
Δ_U : Set Formula
V : VarBoolAssignment
x y : VarName
F : Formula := eq_ x y
h1 : eq_ x y ∈ Δ_U
⊢ ∃ x_1 ∈ Δ_U, (if evalPrime V x_1 then x_1 else x_1.not_) = if V (eq_ x y) = true then eq_ x y else (eq_ x y).not_
Theorem: FOL.NV.L_15_7
Proof state before:
case a
Δ_U : Set Formula
V : VarBoolAssignment
x y : VarName
F : Formula := eq_ x y
h1 : eq_ x y ∈ Δ_U
⊢ ∃ x_1 ∈ Δ_U, (if evalPrime V x_1 then x_1 else x_1.not_) = if V (eq_ x y) = true then eq_ x y else (eq_ x y).not_
Tactic:
apply Exists.intro F
Proof state after:
case a
Δ_U : Set Formula
V : VarBoolAssignment
x y : VarName
F : Formula := eq_ x y
h1 : eq_ x y ∈ Δ_U
⊢ F ∈ Δ_U ∧ (if evalPrime V F then F else F.not_) = if V (eq_ x y) = true then eq_ x y else (eq_ x y).not_
Theorem: FOL.NV.L_15_7
Proof state before:
case a
Δ_U : Set Formula
V : VarBoolAssignment
x y : VarName
F : Formula := eq_ x y
h1 : eq_ x y ∈ Δ_U
⊢ F ∈ Δ_U ∧ (if evalPrime V F then F else F.not_) = if V (eq_ x y) = true then eq_ x y else (eq_ x y).not_
Tactic:
tauto
Proof state after:
no goals