This module contains the verification of the bitblaster for BitVec.ult from Impl.Operations.Ult.

theorem Std.Tactic.BVDecide.BVPred.mkUlt_denote_eq {α : Type} [Hashable α] [DecidableEq α] {w : Nat} (aig : Std.Sat.AIG α) (lhs : BitVec w) (rhs : BitVec w) (input : aig.BinaryRefVec w) (assign : α → Bool) (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) : ⟦assign, { aig := (Std.Tactic.BVDecide.BVPred.mkUlt aig input).aig, ref := (Std.Tactic.BVDecide.BVPred.mkUlt aig input).ref }⟧ = lhs.ult rhs