This module contains the verification of the bitblaster for `BitVec.sub` from `Impl.Operations.Sub`.

source
theorem Std.Tactic.BVDecide.BVExpr.bitblast.denote_blastSub {α : Type} [Hashable α] [DecidableEq α] {w : Nat} (aig : Sat.AIG α) (lhs rhs : BitVec w) (assign : α → Bool) (input : aig.BinaryRefVec w) (hleft : ∀ (idx : Nat) (hidx : idx < w), ⟦assign, { aig := aig, ref := input.lhs.get idx hidx }⟧ = lhs.getLsbD idx) (hright : ∀ (idx : Nat) (hidx : idx < w), ⟦assign, { aig := aig, ref := input.rhs.get idx hidx }⟧ = rhs.getLsbD idx) (idx : Nat) (hidx : idx < w) :
⟦assign, { aig := (blastSub aig input).aig, ref := (blastSub aig input).vec.get idx hidx }⟧ = (lhs - rhs).getLsbD idx