def Std.Sat.CNF.Clause.unit {α : Type u_1} (atom : α) (pol : Bool) : Clause α

Equations

• Std.Sat.CNF.Clause.unit atom pol = Std.Sat.CNF.Clause.empty.add atom pol

theorem Std.Sat.CNF.Clause.unit_def {α✝ : Type u_1} {atom : α✝} {pol : Bool} : unit atom pol = empty.add atom pol

@[simp]

theorem Std.Sat.CNF.Clause.eval_unit {α✝ : Type u_1} {a : α✝ → Bool} {atom : α✝} {pol : Bool} : eval a (unit atom pol) = (a atom == pol)

@[simp]

theorem Std.Sat.CNF.Clause.mem_unit {α : Type u_1} {atom : α} {pol : Bool} {l : Literal α} : l ∈ unit atom pol ↔ l = (atom, pol)

theorem Std.Sat.CNF.Clause.unit_ne_empty {α : Type u_1} {pol : Bool} {atom : α} : unit atom pol ≠ empty

@[simp]

theorem Std.Sat.CNF.Clause.VarMem_unit {α : Type u_1} {atom : α} {pol : Bool} {v : α} : VarMem v (unit atom pol) ↔ v = atom

@[simp]

theorem Std.Sat.CNF.Clause.relabel_unit {α : Type u_1} {β : Type u_2} {atom : α} {pol : Bool} {r : α → β} : relabel r (unit atom pol) = unit (r atom) pol

@[simp]

theorem Std.Sat.CNF.Clause.sat_unit_iff {α✝ : Type u_1} {a : α✝ → Bool} {atom : α✝} {pol : Bool} : Sat a (unit atom pol) ↔ a atom = pol

@[simp]

theorem Std.Sat.CNF.Clause.not_sat_unit_iff {α✝ : Type u_1} {a : α✝ → Bool} {atom : α✝} {pol : Bool} : ¬Sat a (unit atom pol) ↔ a atom = !pol

@[simp]

theorem Std.Sat.CNF.Clause.not_unsat_unit {α✝ : Type u_1} {atom : α✝} {p : Bool} : ¬(unit atom p).Unsat

@[simp]

theorem Std.Sat.CNF.sat_add_unit_iff {α : Type u_1} {a : α → Bool} (f : CNF α) (atom : α) (pol : Bool) : Sat a (f.add (Clause.unit atom pol)) ↔ a atom = pol ∧ Sat a f

theorem Std.Sat.CNF.entails_clause_unit_iff_unsat_add_neg {α : Type u_1} {f : CNF α} {atom : α} {pol : Bool} : f.EntailsClause (Clause.unit atom pol) ↔ (f.add (Clause.unit atom !pol)).Unsat