Theorem: BVExpr.bitblast_denote_eq_eval_getLsb (LeanSAT/Reflect/BVExpr/BitBlast/Lemmas/Expr.lean)

State before:
w : Nat
aig : AIG BVBit
expr : BVExpr w
assign : Assignment
⊢ ∀ (idx : Nat) (hidx : idx < w),
    ⟦{ aig := (bitblast aig expr).aig, ref := (bitblast aig expr).stream.getRef idx hidx }, assign.toAIGAssignment⟧ =
      (eval assign expr).getLsb idx
Tactic:
intros
State after:
w : Nat
aig : AIG BVBit
expr : BVExpr w
assign : Assignment
idx✝ : Nat
hidx✝ : idx✝ < w
⊢ ⟦{ aig := (bitblast aig expr).aig, ref := (bitblast aig expr).stream.getRef idx✝ hidx✝ }, assign.toAIGAssignment⟧ =
    (eval assign expr).getLsb idx✝

State before:
w : Nat
aig : AIG BVBit
expr : BVExpr w
assign : Assignment
idx✝ : Nat
hidx✝ : idx✝ < w
⊢ ⟦{ aig := (bitblast aig expr).aig, ref := (bitblast aig expr).stream.getRef idx✝ hidx✝ }, assign.toAIGAssignment⟧ =
    (eval assign expr).getLsb idx✝
Tactic:
rw [← bitblast.go_val_eq_bitblast]
State after:
w : Nat
aig : AIG BVBit
expr : BVExpr w
assign : Assignment
idx✝ : Nat
hidx✝ : idx✝ < w
⊢ ⟦{ aig := (bitblast.go aig expr).val.aig, ref := (bitblast.go aig expr).val.stream.getRef idx✝ hidx✝ },
      assign.toAIGAssignment⟧ =
    (eval assign expr).getLsb idx✝

State before:
w : Nat
aig : AIG BVBit
expr : BVExpr w
assign : Assignment
idx✝ : Nat
hidx✝ : idx✝ < w
⊢ ⟦{ aig := (bitblast.go aig expr).val.aig, ref := (bitblast.go aig expr).val.stream.getRef idx✝ hidx✝ },
      assign.toAIGAssignment⟧ =
    (eval assign expr).getLsb idx✝
Tactic:
rw [bitblast.go_denote_eq_eval_getLsb]
State after:
no goals