theorem
Std.Tactic.BVDecide.LRAT.Internal.Literal.sat_iff
{α : Type u_1}
(p : α → Bool)
(a : α)
(b : Bool)
:
Std.Tactic.BVDecide.LRAT.Internal.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 : Std.Sat.Literal α}
:
theorem
Std.Tactic.BVDecide.LRAT.Internal.Literal.unsat_of_limplies_complement
{α : Type u_1}
{t : Type u_2}
[Std.Tactic.BVDecide.LRAT.Internal.Entails α t]
(x : t)
(l : Std.Sat.Literal α)
:
theorem
Std.Tactic.BVDecide.LRAT.Internal.Clause.sat_iff_exists
{α : Type u_1}
{β : Type u_2}
[Std.Tactic.BVDecide.LRAT.Internal.Clause α β]
(p : α → Bool)
(c : β)
:
theorem
Std.Tactic.BVDecide.LRAT.Internal.Clause.limplies_iff_mem
{α : Type u_1}
{β : Type u_2}
[DecidableEq α]
[Std.Tactic.BVDecide.LRAT.Internal.Clause α β]
(l : Std.Sat.Literal α)
(c : β)
:
theorem
Std.Tactic.BVDecide.LRAT.Internal.Clause.entails_of_entails_delete
{α : Type u_1}
{β : Type u_2}
[DecidableEq α]
[Std.Tactic.BVDecide.LRAT.Internal.Clause α β]
{p : α → Bool}
{c : β}
{l : Std.Sat.Literal α}
:
theorem
Std.Tactic.BVDecide.LRAT.Internal.Formula.sat_iff_forall
{α : Type u_1}
{β : Type u_2}
{σ : Type u_3}
[Std.Tactic.BVDecide.LRAT.Internal.Clause α β]
[Std.Tactic.BVDecide.LRAT.Internal.Entails α σ]
[Std.Tactic.BVDecide.LRAT.Internal.Formula α β σ]
(p : α → Bool)
(f : σ)
:
theorem
Std.Tactic.BVDecide.LRAT.Internal.Formula.limplies_insert
{α : Type u_1}
{β : Type u_2}
{σ : Type u_3}
[Std.Tactic.BVDecide.LRAT.Internal.Clause α β]
[Std.Tactic.BVDecide.LRAT.Internal.Entails α σ]
[Std.Tactic.BVDecide.LRAT.Internal.Formula α β σ]
{c : β}
{f : σ}
:
theorem
Std.Tactic.BVDecide.LRAT.Internal.Formula.limplies_delete
{α : Type u_1}
{β : Type u_2}
{σ : Type u_3}
[Std.Tactic.BVDecide.LRAT.Internal.Clause α β]
[Std.Tactic.BVDecide.LRAT.Internal.Entails α σ]
[Std.Tactic.BVDecide.LRAT.Internal.Formula α β σ]
{f : σ}
{arr : Array Nat}
: