theorem Std.Tactic.BVDecide.LRAT.Internal.Literal.sat_iff {α : Type u_1} (p : α → Bool) (a : α) (b : Bool) : Entails.eval p (a, b) ↔ p a = b

theorem Std.Tactic.BVDecide.LRAT.Internal.Literal.sat_negate_iff_not_sat {α : Type u_1} {p : α → Bool} {l : Sat.Literal α} : Entails.eval p l.negate ↔ ¬Entails.eval p l

theorem Std.Tactic.BVDecide.LRAT.Internal.Literal.unsat_of_limplies_complement {α : Type u_1} {t : Type u_2} [Entails α t] (x : t) (l : Sat.Literal α) : Limplies α x l → Limplies α x l.negate → Unsatisfiable α x

theorem Std.Tactic.BVDecide.LRAT.Internal.Clause.sat_iff_exists {α : Type u_1} {β : Type u_2} [Clause α β] (p : α → Bool) (c : β) : Entails.eval p c ↔ ∃ (l : Sat.Literal α), l ∈ toList c ∧ Entails.eval p l

theorem Std.Tactic.BVDecide.LRAT.Internal.Clause.limplies_iff_mem {α : Type u_1} {β : Type u_2} [DecidableEq α] [Clause α β] (l : Sat.Literal α) (c : β) : Limplies α l c ↔ l ∈ toList c

theorem Std.Tactic.BVDecide.LRAT.Internal.Clause.entails_of_entails_delete {α : Type u_1} {β : Type u_2} [DecidableEq α] [Clause α β] {p : α → Bool} {c : β} {l : Sat.Literal α} : Entails.eval p (delete c l) → Entails.eval p c

theorem Std.Tactic.BVDecide.LRAT.Internal.Formula.sat_iff_forall {α : Type u_1} {β : Type u_2} {σ : Type u_3} [Clause α β] [Entails α σ] [Formula α β σ] (p : α → Bool) (f : σ) : Entails.eval p f ↔ ∀ (c : β), c ∈ toList f → Entails.eval p c

theorem Std.Tactic.BVDecide.LRAT.Internal.Formula.limplies_insert {α : Type u_1} {β : Type u_2} {σ : Type u_3} [Clause α β] [Entails α σ] [Formula α β σ] {c : β} {f : σ} : Limplies α (insert f c) f

theorem Std.Tactic.BVDecide.LRAT.Internal.Formula.limplies_delete {α : Type u_1} {β : Type u_2} {σ : Type u_3} [Clause α β] [Entails α σ] [Formula α β σ] {f : σ} {arr : Array Nat} : Limplies α f (delete f arr)