This module contains the verification of the bitblaster for BitVec.cpop, implemented in Impl.Operations.Cpop.

@[simp]

theorem Std.Tactic.BVDecide.BVExpr.bitblast.denote_blastCpop {α : Type} [Hashable α] [DecidableEq α] {w : Nat} (aig : Sat.AIG α) (xc : aig.RefVec w) (x : BitVec w) (assign : α → Bool) (hx : ∀ (idx : Nat) (hidx : idx < w), ⟦assign, { aig := aig, ref := xc.get idx hidx }⟧ = x.getLsbD idx) (idx : Nat) (hidx : idx < w) : ⟦assign, { aig := (blastCpop aig xc).aig, ref := (blastCpop aig xc).vec.get idx hidx }⟧ = x.cpop.getLsbD idx