Theorem: BVExpr.bitblast.go_denote_eq_eval_getLsb
Proof state before:
case signExtend.inr
w : Nat
assign : Assignment
originalWidth v : Nat
inner : BVExpr originalWidth
ih :
  ∀ (aig : AIG BVBit) (idx : Nat) (hidx : idx < originalWidth),
    ⟦{ aig := (go aig inner).val.aig, ref := (go aig inner).val.stream.getRef idx hidx }, assign.toAIGAssignment⟧ =
      (eval assign inner).getLsb idx
aig : AIG BVBit
idx : Nat
hidx : idx < v
res : RefStreamEntry BVBit v
hgo : blastSignExtend (go aig inner).1.aig { w := originalWidth, stream := (go aig inner).1.stream } = res
this : 0 ≤ originalWidth
hlt : 0 < originalWidth
⊢ (if hidx : idx < { w := originalWidth, stream := (go aig inner).1.stream }.w then
      ⟦{ aig := (go aig inner).1.aig,
          ref := { w := originalWidth, stream := (go aig inner).1.stream }.stream.getRef idx hidx },
        assign.toAIGAssignment⟧
    else
      ⟦{ aig := (go aig inner).1.aig,
          ref :=
            { w := originalWidth, stream := (go aig inner).1.stream }.stream.getRef
              ({ w := originalWidth, stream := (go aig inner).1.stream }.w - 1) ⋯ },
        assign.toAIGAssignment⟧) =
    (eval assign (signExtend v inner)).getLsb idx

case signExtend.inr.htarget
w : Nat
assign : Assignment
originalWidth v : Nat
inner : BVExpr originalWidth
ih :
  ∀ (aig : AIG BVBit) (idx : Nat) (hidx : idx < originalWidth),
    ⟦{ aig := (go aig inner).val.aig, ref := (go aig inner).val.stream.getRef idx hidx }, assign.toAIGAssignment⟧ =
      (eval assign inner).getLsb idx
aig : AIG BVBit
idx : Nat
hidx : idx < v
res : RefStreamEntry BVBit v
hgo : blastSignExtend (go aig inner).1.aig { w := originalWidth, stream := (go aig inner).1.stream } = res
this : 0 ≤ originalWidth
hlt : 0 < originalWidth
⊢ 0 < { w := originalWidth, stream := (go aig inner).1.stream }.w
Tactic:
simp only [eval_signExtend]
Proof state after:
case signExtend.inr
w : Nat
assign : Assignment
originalWidth v : Nat
inner : BVExpr originalWidth
ih :
  ∀ (aig : AIG BVBit) (idx : Nat) (hidx : idx < originalWidth),
    ⟦{ aig := (go aig inner).val.aig, ref := (go aig inner).val.stream.getRef idx hidx }, assign.toAIGAssignment⟧ =
      (eval assign inner).getLsb idx
aig : AIG BVBit
idx : Nat
hidx : idx < v
res : RefStreamEntry BVBit v
hgo : blastSignExtend (go aig inner).1.aig { w := originalWidth, stream := (go aig inner).1.stream } = res
this : 0 ≤ originalWidth
hlt : 0 < originalWidth
⊢ (if h : idx < originalWidth then
      ⟦{ aig := (go aig inner).1.aig, ref := (go aig inner).1.stream.getRef idx ⋯ }, assign.toAIGAssignment⟧
    else
      ⟦{ aig := (go aig inner).1.aig, ref := (go aig inner).1.stream.getRef (originalWidth - 1) ⋯ },
        assign.toAIGAssignment⟧) =
    (BitVec.signExtend v (eval assign inner)).getLsb idx

case signExtend.inr.htarget
w : Nat
assign : Assignment
originalWidth v : Nat
inner : BVExpr originalWidth
ih :
  ∀ (aig : AIG BVBit) (idx : Nat) (hidx : idx < originalWidth),
    ⟦{ aig := (go aig inner).val.aig, ref := (go aig inner).val.stream.getRef idx hidx }, assign.toAIGAssignment⟧ =
      (eval assign inner).getLsb idx
aig : AIG BVBit
idx : Nat
hidx : idx < v
res : RefStreamEntry BVBit v
hgo : blastSignExtend (go aig inner).1.aig { w := originalWidth, stream := (go aig inner).1.stream } = res
this : 0 ≤ originalWidth
hlt : 0 < originalWidth
⊢ 0 < { w := originalWidth, stream := (go aig inner).1.stream }.w