def Std.Tactic.BVDecide.LRAT.Internal.State.deleteMany (s : State) (idxs : Array Nat) : State

Equations

• s.deleteMany idxs = Array.foldl Std.Tactic.BVDecide.LRAT.Internal.State.deleteOne✝ s idxs

theorem Std.Tactic.BVDecide.LRAT.Internal.State.entails_deleteMany {idxs : Array Nat} {s : State} : s.toCNF.Entails (s.deleteMany idxs).toCNF