This module contains the verification of the bitblaster for BitVec.neg from Impl.Operations.Neg.

theorem Std.Tactic.BVDecide.BVExpr.bitblast.denote_blastNeg {α : Type} [Hashable α] [DecidableEq α] {w : Nat} (aig : Std.Sat.AIG α) (value : BitVec w) (target : aig.RefVec w) (assign : α → Bool) (htarget : ∀ (idx : Nat) (hidx : idx < w), ⟦assign, { aig := aig, ref := target.get idx hidx }⟧ = value.getLsbD idx) (idx : Nat) (hidx : idx < w) : ⟦assign, { aig := (Std.Tactic.BVDecide.BVExpr.bitblast.blastNeg aig target).aig, ref := (Std.Tactic.BVDecide.BVExpr.bitblast.blastNeg aig target).vec.get idx hidx }⟧ = (-value).getLsbD idx