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