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

theorem Std.Tactic.BVDecide.BVExpr.bitblast.denote_blastSub {α : Type} [Hashable α] [DecidableEq α] {w : Nat} (aig : Std.Sat.AIG α) (lhs : BitVec w) (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 := (Std.Tactic.BVDecide.BVExpr.bitblast.blastSub aig input).aig, ref := (Std.Tactic.BVDecide.BVExpr.bitblast.blastSub aig input).vec.get idx hidx }⟧ = (lhs - rhs).getLsbD idx