Theorem: BVExpr.bitblast.blastExtract_eq_eval_getLsb
Proof state before:
case mk.isTrue.isTrue
α : Type
inst✝² : BEq α
inst✝¹ : Hashable α
inst✝ : DecidableEq α
newWidth : Nat
aig : AIG α
assign : α → Bool
idx : Nat
hidx : idx < newWidth
res : RefStreamEntry α newWidth
w✝ : Nat
input : aig.RefStream w✝
hi lo : Nat
hnew : newWidth = hi - lo + 1
h✝¹ : lo ≤ hi
hextract :
  { aig := (aig.mkConstCached false).aig,
      stream := blastExtract.go (input.cast ⋯) lo 0 ⋯ (aig.mkConstCached false).ref RefStream.empty } =
    res
h✝ : lo + idx < w✝
⊢ ⟦{ aig := (aig.mkConstCached false).aig, ref := (input.cast ⋯).getRef (lo + idx) ?mk.isTrue.isTrue.hidx }, assign⟧ =
    ⟦{ aig := aig, ref := input.getRef (lo + idx) h✝ }, assign⟧

case mk.isTrue.isTrue.hidx
α : Type
inst✝² : BEq α
inst✝¹ : Hashable α
inst✝ : DecidableEq α
newWidth : Nat
aig : AIG α
assign : α → Bool
idx : Nat
hidx : idx < newWidth
res : RefStreamEntry α newWidth
w✝ : Nat
input : aig.RefStream w✝
hi lo : Nat
hnew : newWidth = hi - lo + 1
h✝¹ : lo ≤ hi
hextract :
  { aig := (aig.mkConstCached false).aig,
      stream := blastExtract.go (input.cast ⋯) lo 0 ⋯ (aig.mkConstCached false).ref RefStream.empty } =
    res
h✝ : lo + idx < w✝
⊢ lo + idx < w✝
Tactic:
rw [LawfulOperator.denote_mem_prefix (f := mkConstCached)]
Proof state after:
case mk.isTrue.isTrue
α : Type
inst✝² : BEq α
inst✝¹ : Hashable α
inst✝ : DecidableEq α
newWidth : Nat
aig : AIG α
assign : α → Bool
idx : Nat
hidx : idx < newWidth
res : RefStreamEntry α newWidth
w✝ : Nat
input : aig.RefStream w✝
hi lo : Nat
hnew : newWidth = hi - lo + 1
h✝¹ : lo ≤ hi
hextract :
  { aig := (aig.mkConstCached false).aig,
      stream := blastExtract.go (input.cast ⋯) lo 0 ⋯ (aig.mkConstCached false).ref RefStream.empty } =
    res
h✝ : lo + idx < w✝
⊢ ⟦{ aig := aig,
        ref := { gate := ((input.cast ⋯).getRef (lo + idx) ?mk.isTrue.isTrue.hidx).gate, hgate := ?mk.isTrue.isTrue } },
      assign⟧ =
    ⟦{ aig := aig, ref := input.getRef (lo + idx) h✝ }, assign⟧

case mk.isTrue.isTrue
α : Type
inst✝² : BEq α
inst✝¹ : Hashable α
inst✝ : DecidableEq α
newWidth : Nat
aig : AIG α
assign : α → Bool
idx : Nat
hidx : idx < newWidth
res : RefStreamEntry α newWidth
w✝ : Nat
input : aig.RefStream w✝
hi lo : Nat
hnew : newWidth = hi - lo + 1
h✝¹ : lo ≤ hi
hextract :
  { aig := (aig.mkConstCached false).aig,
      stream := blastExtract.go (input.cast ⋯) lo 0 ⋯ (aig.mkConstCached false).ref RefStream.empty } =
    res
h✝ : lo + idx < w✝
⊢ ((input.cast ⋯).getRef (lo + idx) ?mk.isTrue.isTrue.hidx).gate < aig.decls.size

case mk.isTrue.isTrue.hidx
α : Type
inst✝² : BEq α
inst✝¹ : Hashable α
inst✝ : DecidableEq α
newWidth : Nat
aig : AIG α
assign : α → Bool
idx : Nat
hidx : idx < newWidth
res : RefStreamEntry α newWidth
w✝ : Nat
input : aig.RefStream w✝
hi lo : Nat
hnew : newWidth = hi - lo + 1
h✝¹ : lo ≤ hi
hextract :
  { aig := (aig.mkConstCached false).aig,
      stream := blastExtract.go (input.cast ⋯) lo 0 ⋯ (aig.mkConstCached false).ref RefStream.empty } =
    res
h✝ : lo + idx < w✝
⊢ lo + idx < w✝

case mk.isTrue.isTrue.hidx
α : Type
inst✝² : BEq α
inst✝¹ : Hashable α
inst✝ : DecidableEq α
newWidth : Nat
aig : AIG α
assign : α → Bool
idx : Nat
hidx : idx < newWidth
res : RefStreamEntry α newWidth
w✝ : Nat
input : aig.RefStream w✝
hi lo : Nat
hnew : newWidth = hi - lo + 1
h✝¹ : lo ≤ hi
hextract :
  { aig := (aig.mkConstCached false).aig,
      stream := blastExtract.go (input.cast ⋯) lo 0 ⋯ (aig.mkConstCached false).ref RefStream.empty } =
    res
h✝ : lo + idx < w✝
⊢ lo + idx < w✝