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)) : Bool

Equations

• One or more equations did not get rendered due to their size.

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) : ∃ (a' : Nat → Bool), Sat.CNF.Sat a' (s.add clause).toCNF