This module contains the verification of the BitVec.getLsb bitblaster from Impl.Operations.Extract.

@[simp]

theorem Std.Tactic.BVDecide.BVPred.denote_blastGetLsbD {α : Type} [Hashable α] [DecidableEq α] (aig : Std.Sat.AIG α) (target : Std.Tactic.BVDecide.BVPred.GetLsbDTarget aig) (assign : α → Bool) : ⟦assign, Std.Tactic.BVDecide.BVPred.blastGetLsbD aig target⟧ = if h : target.idx < target.w then ⟦assign, { aig := aig, ref := target.vec.get target.idx h }⟧ else false