This module contains the verification of the BitVec equality bitblaster from Impl.Operations.Eq.

theorem Std.Tactic.BVDecide.BVPred.mkEq_denote_eq {α : Type} [Hashable α] [DecidableEq α] {w : Nat} (aig : Sat.AIG α) (pair : aig.BinaryRefVec w) (assign : α → Bool) (lhs rhs : BitVec w) (hleft : ∀ (idx : Nat) (hidx : idx < w), ⟦assign, { aig := aig, ref := pair.lhs.get idx hidx }⟧ = lhs.getLsbD idx) (hright : ∀ (idx : Nat) (hidx : idx < w), ⟦assign, { aig := aig, ref := pair.rhs.get idx hidx }⟧ = rhs.getLsbD idx) : ⟦assign, mkEq aig pair⟧ = (lhs == rhs)