Theorem: BVExpr.bitblast.blastVar_eq_eval_getLsb (LeanSAT/Reflect/BVExpr/BitBlast/Lemmas/Var.lean)

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

State before:
w : Nat
aig : AIG BVBit
var : BVVar w
assign : Assignment
idx✝ : Nat
hidx✝ : idx✝ < w
⊢ ⟦{ aig := (blastVar aig var).aig, ref := (blastVar aig var).stream.getRef idx✝ hidx✝ }, assign.toAIGAssignment⟧ =
    (eval assign (BVExpr.var var.ident)).getLsb idx✝
Tactic:
apply blastVar.go_eq_eval_getLsb
State after:
case a
w : Nat
aig : AIG BVBit
var : BVVar w
assign : Assignment
idx✝ : Nat
hidx✝ : idx✝ < w
⊢ 0 ≤ idx✝

State before:
case a
w : Nat
aig : AIG BVBit
var : BVVar w
assign : Assignment
idx✝ : Nat
hidx✝ : idx✝ < w
⊢ 0 ≤ idx✝
Tactic:
omega
State after:
no goals