def Std.Sat.CNF.Entails {α : Type u_1} (f1 f2 : CNF α) : Prop

Equations

• f1.Entails f2 = ∀ (a : α → Bool), Std.Sat.CNF.Sat a f1 → Std.Sat.CNF.Sat a f2

def Std.Sat.CNF.EntailsClause {α : Type u_1} (f : CNF α) (c : Clause α) : Prop

Equations

• f.EntailsClause c = ∀ (a : α → Bool), Std.Sat.CNF.Sat a f → Std.Sat.CNF.Clause.Sat a c

theorem Std.Sat.CNF.entails_def {α : Type u_1} (f1 f2 : CNF α) : f1.Entails f2 ↔ ∀ (a : α → Bool), Sat a f1 → Sat a f2

theorem Std.Sat.CNF.entails_refl {α : Type u_1} (f : CNF α) : f.Entails f

theorem Std.Sat.CNF.entails_trans {α : Type u_1} {f1 f2 f3 : CNF α} (h1 : f1.Entails f2) (h2 : f2.Entails f3) : f1.Entails f3

theorem Std.Sat.CNF.entails_clause_def {α : Type u_1} {f : CNF α} {c : Clause α} : f.EntailsClause c ↔ ∀ (a : α → Bool), Sat a f → Clause.Sat a c

theorem Std.Sat.CNF.entails_of_forall_sat {α : Type u_1} (f1 f2 : CNF α) (h : ∀ (a : α → Bool), Sat a f2) : f1.Entails f2

theorem Std.Sat.CNF.entails_add_of_entails_clause {α : Type u_1} (f : CNF α) (c : Clause α) (h : f.EntailsClause c) : f.Entails (f.add c)

theorem Std.Sat.CNF.entails_add_iff {α : Type u_1} {f g : CNF α} {c : Clause α} : g.Entails (f.add c) ↔ g.Entails f ∧ g.EntailsClause c

theorem Std.Sat.CNF.entails_of_all_mem {α : Type u_1} (f1 f2 : CNF α) (h : ∀ (c : Clause α), c ∈ f1 → c ∈ f2) : f2.Entails f1

theorem Std.Sat.CNF.entails_iff_all_mem_entails_clause {α : Type u_1} {f g : CNF α} : f.Entails g ↔ ∀ (c : Clause α), c ∈ g → f.EntailsClause c

theorem Std.Sat.CNF.unsat_of_entails_unsat {α : Type u_1} {f1 f2 : CNF α} (h1 : f2.Unsat) (h2 : f1.Entails f2) : f1.Unsat

theorem Std.Sat.CNF.unsat_of_entails_clause_unsat {α : Type u_1} {f : CNF α} {c : Clause α} (h1 : c.Unsat) (h2 : f.EntailsClause c) : f.Unsat

theorem Std.Sat.CNF.entails_append_of_entails {α : Type u_1} {f1 f2 f3 : CNF α} (h1 : f1.Entails f2) (h2 : f1.Entails f3) : f1.Entails (f2 ++ f3)

@[simp]

theorem Std.Sat.CNF.append_entails_left {α : Type u_1} {f1 f2 : CNF α} : (f1 ++ f2).Entails f1

@[simp]

theorem Std.Sat.CNF.append_entails_right {α : Type u_1} {f1 f2 : CNF α} : (f1 ++ f2).Entails f2

theorem Std.Sat.CNF.entails_append_congr_right {α : Type u_1} {f1 f2 f3 : CNF α} (h1 : f2.Entails f3) : (f1 ++ f2).Entails (f1 ++ f3)

theorem Std.Sat.CNF.entails_append_congr_left {α : Type u_1} {f1 f2 f3 : CNF α} (h1 : f2.Entails f3) : (f2 ++ f1).Entails (f3 ++ f1)

theorem Std.Sat.CNF.entails_append_comm {α : Type u_1} {f1 f2 : CNF α} : (f1 ++ f2).Entails (f2 ++ f1)

theorem Std.Sat.CNF.entails_clause_append_iff {α : Type u_1} {f : CNF α} {c1 c2 : Clause α} : f.EntailsClause (c1 ++ c2) ↔ ∀ (a : α → Bool), Sat a f → Clause.Sat a c1 ∨ Clause.Sat a c2

theorem Std.Sat.CNF.entails_clause_append_of_forall {α : Type u_1} {f : CNF α} {c1 c2 : Clause α} (h : ∀ (a : α → Bool), Sat a f → Clause.Sat a c1 ∨ Clause.Sat a c2) : f.EntailsClause (c1 ++ c2)

theorem Std.Sat.CNF.entails_clause_append_left {α : Type u_1} {f : CNF α} {c1 c2 : Clause α} (h : f.EntailsClause c1) : f.EntailsClause (c1 ++ c2)

theorem Std.Sat.CNF.entails_clause_append_right {α : Type u_1} {f : CNF α} {c1 c2 : Clause α} (h : f.EntailsClause c2) : f.EntailsClause (c1 ++ c2)

theorem Std.Sat.CNF.entails_clause_append_comm {α : Type u_1} {f : CNF α} {c1 c2 : Clause α} (h : f.EntailsClause (c1 ++ c2)) : f.EntailsClause (c2 ++ c1)

theorem Std.Sat.CNF.unsat_of_entails_clause_append_unsat {α : Type u_1} {f : CNF α} {c1 c2 : Clause α} (h1 : c1.Unsat) (h2 : c2.Unsat) (h3 : f.EntailsClause (c1 ++ c2)) : f.Unsat

theorem Std.Sat.CNF.entails_clause_of_mem {α : Type u_1} {f : CNF α} {c : Clause α} (h : c ∈ f) : f.EntailsClause c

@[simp]

theorem Std.Sat.CNF.add_entails_left {α : Type u_1} {f : CNF α} {c : Clause α} : (f.add c).Entails f

@[simp]

theorem Std.Sat.CNF.entails_clause_add {α : Type u_1} {f : CNF α} {c : Clause α} : (f.add c).EntailsClause c

theorem Std.Sat.CNF.entails_clause_trans {α : Type u_1} {f g : CNF α} {c : Clause α} (h1 : f.Entails g) (h2 : g.EntailsClause c) : f.EntailsClause c

theorem Std.Sat.CNF.entails_add_congr {α : Type u_1} {f g : CNF α} {c : Clause α} (h : f.Entails g) : (f.add c).Entails (g.add c)

@[simp]

theorem Std.Sat.CNF.entails_empty {α : Type u_1} {f : CNF α} : f.Entails empty

theorem Std.Sat.CNF.unsat_iff_entails_clause_empty {α : Type u_1} {f : CNF α} : f.Unsat ↔ f.EntailsClause Clause.empty

def Std.Sat.CNF.BiEntails {α : Type u_1} (f1 f2 : CNF α) : Prop

Equations

• f1.BiEntails f2 = (f1.Entails f2 ∧ f2.Entails f1)

theorem Std.Sat.CNF.biEntails_def {α✝ : Type u_1} {f1 f2 : CNF α✝} : f1.BiEntails f2 ↔ f1.Entails f2 ∧ f2.Entails f1

theorem Std.Sat.CNF.biEntails_refl {α✝ : Type u_1} {f : CNF α✝} : f.BiEntails f

theorem Std.Sat.CNF.biEntails_trans {α : Type u_1} {f1 f2 f3 : CNF α} (h1 : f1.BiEntails f2) (h2 : f2.BiEntails f3) : f1.BiEntails f3

theorem Std.Sat.CNF.biEntails_symm {α✝ : Type u_1} {f1 f2 : CNF α✝} (h : f1.BiEntails f2) : f2.BiEntails f1

theorem Std.Sat.CNF.biEntails_comm {α✝ : Type u_1} {f1 f2 : CNF α✝} : f1.BiEntails f2 ↔ f2.BiEntails f1