def Std.Tactic.BVDecide.LRAT.Internal.check (proof : Array IntAction) (formula : Sat.CNF Nat) : Bool

Equations

• Std.Tactic.BVDecide.LRAT.Internal.check proof formula = Std.Tactic.BVDecide.LRAT.Internal.check.go✝ (Std.Tactic.BVDecide.LRAT.Internal.State.ofCNF formula) proof 0

theorem Std.Tactic.BVDecide.LRAT.Internal.unsat_of_check {proof : Array IntAction} {formula : Sat.CNF Nat} (h : check proof formula = true) : formula.Unsat