Documentation

Std.Tactic.BVDecide.Bitblast.BVExpr.Circuit.Lemmas.Operations.Reverse

This module contains the verification of the bitblaster for BitVec.reverse from Impl.Operations.Reverse.

@[simp]
theorem Std.Tactic.BVDecide.BVExpr.bitblast.denote_blastReverse {α : Type} [Hashable α] [DecidableEq α] {w : Nat} (aig : Sat.AIG α) (target : aig.RefVec w) (assign : αBool) (idx : Nat) (hidx : idx < w) :
assign, { aig := (blastReverse aig target).aig, ref := (blastReverse aig target).vec.get idx hidx } = assign, { aig := aig, ref := target.get (w - 1 - idx) }