def
Std.Tactic.BVDecide.LRAT.Internal.State.checkRat
(s : State)
(clause : Sat.CNF.Clause Nat)
(pivot : Sat.Literal Nat)
(rupHints : Array Nat)
(ratHints : Array (Nat × Array Nat))
:
Equations
- One or more equations did not get rendered due to their size.
Instances For
theorem
Std.Tactic.BVDecide.LRAT.Internal.State.unsat_of_unsat_of_checkRat
{a : Nat → Bool}
{s : State}
{clause : Sat.CNF.Clause Nat}
{pivot : Sat.Literal Nat}
{rupHints : Array Nat}
{ratHints : Array (Nat × Array Nat)}
(h1 : s.checkRat clause pivot rupHints ratHints = true)
(h2 : Sat.CNF.Sat a s.toCNF)
: