This module contains the verification of the BitVec.append bitblaster from Impl.Operations.Append.

@[simp]

theorem Std.Tactic.BVDecide.BVExpr.bitblast.denote_blastAppend {α : Type} [Hashable α] [DecidableEq α] {newWidth : Nat} (aig : Std.Sat.AIG α) (target : Std.Tactic.BVDecide.BVExpr.bitblast.AppendTarget aig newWidth) (assign : α → Bool) (idx : Nat) (hidx : idx < newWidth) : ⟦assign, { aig := (Std.Tactic.BVDecide.BVExpr.bitblast.blastAppend aig target).aig, ref := (Std.Tactic.BVDecide.BVExpr.bitblast.blastAppend aig target).vec.get idx hidx }⟧ = if hr : idx < target.rw then ⟦assign, { aig := aig, ref := target.rhs.get idx hr }⟧ else let_fun this := ⋯; ⟦assign, { aig := aig, ref := target.lhs.get (idx - target.rw) ⋯ }⟧