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

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

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

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

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