Theorem: BVPred.blastGetLsb_denote_eq_eval_getLsb (LeanSAT/Reflect/BVExpr/BitBlast/Lemmas/GetLsb.lean)

State before:
α : Type
inst✝² : BEq α
inst✝¹ : Hashable α
inst✝ : DecidableEq α
aig : AIG α
target : GetLsbTarget aig
assign : α → Bool
⊢ ⟦blastGetLsb aig target, assign⟧ =
    if h : target.idx < target.w then ⟦{ aig := aig, ref := target.stream.getRef target.idx h }, assign⟧ else false
Tactic:
rcases target with ⟨expr, idx⟩
State after:
case mk
α : Type
inst✝² : BEq α
inst✝¹ : Hashable α
inst✝ : DecidableEq α
aig : AIG α
assign : α → Bool
w✝ : Nat
expr : aig.RefStream w✝
idx : Nat
⊢ ⟦blastGetLsb aig (GetLsbTarget.mk expr idx), assign⟧ =
    if h : (GetLsbTarget.mk expr idx).idx < (GetLsbTarget.mk expr idx).w then
      ⟦{ aig := aig, ref := (GetLsbTarget.mk expr idx).stream.getRef (GetLsbTarget.mk expr idx).idx h }, assign⟧
    else false

State before:
case mk
α : Type
inst✝² : BEq α
inst✝¹ : Hashable α
inst✝ : DecidableEq α
aig : AIG α
assign : α → Bool
w✝ : Nat
expr : aig.RefStream w✝
idx : Nat
⊢ ⟦blastGetLsb aig (GetLsbTarget.mk expr idx), assign⟧ =
    if h : (GetLsbTarget.mk expr idx).idx < (GetLsbTarget.mk expr idx).w then
      ⟦{ aig := aig, ref := (GetLsbTarget.mk expr idx).stream.getRef (GetLsbTarget.mk expr idx).idx h }, assign⟧
    else false
Tactic:
unfold blastGetLsb
State after:
case mk
α : Type
inst✝² : BEq α
inst✝¹ : Hashable α
inst✝ : DecidableEq α
aig : AIG α
assign : α → Bool
w✝ : Nat
expr : aig.RefStream w✝
idx : Nat
⊢ ⟦if h : (GetLsbTarget.mk expr idx).idx < (GetLsbTarget.mk expr idx).w then
        { aig := aig, ref := (GetLsbTarget.mk expr idx).stream.getRef (GetLsbTarget.mk expr idx).idx h }
      else aig.mkConstCached false,
      assign⟧ =
    if h : (GetLsbTarget.mk expr idx).idx < (GetLsbTarget.mk expr idx).w then
      ⟦{ aig := aig, ref := (GetLsbTarget.mk expr idx).stream.getRef (GetLsbTarget.mk expr idx).idx h }, assign⟧
    else false

State before:
case mk
α : Type
inst✝² : BEq α
inst✝¹ : Hashable α
inst✝ : DecidableEq α
aig : AIG α
assign : α → Bool
w✝ : Nat
expr : aig.RefStream w✝
idx : Nat
⊢ ⟦if h : (GetLsbTarget.mk expr idx).idx < (GetLsbTarget.mk expr idx).w then
        { aig := aig, ref := (GetLsbTarget.mk expr idx).stream.getRef (GetLsbTarget.mk expr idx).idx h }
      else aig.mkConstCached false,
      assign⟧ =
    if h : (GetLsbTarget.mk expr idx).idx < (GetLsbTarget.mk expr idx).w then
      ⟦{ aig := aig, ref := (GetLsbTarget.mk expr idx).stream.getRef (GetLsbTarget.mk expr idx).idx h }, assign⟧
    else false
Tactic:
dsimp
State after:
case mk
α : Type
inst✝² : BEq α
inst✝¹ : Hashable α
inst✝ : DecidableEq α
aig : AIG α
assign : α → Bool
w✝ : Nat
expr : aig.RefStream w✝
idx : Nat
⊢ ⟦if h : idx < w✝ then { aig := aig, ref := expr.getRef idx h } else aig.mkConstCached false, assign⟧ =
    if h : idx < w✝ then ⟦{ aig := aig, ref := expr.getRef idx h }, assign⟧ else false

State before:
case mk
α : Type
inst✝² : BEq α
inst✝¹ : Hashable α
inst✝ : DecidableEq α
aig : AIG α
assign : α → Bool
w✝ : Nat
expr : aig.RefStream w✝
idx : Nat
⊢ ⟦if h : idx < w✝ then { aig := aig, ref := expr.getRef idx h } else aig.mkConstCached false, assign⟧ =
    if h : idx < w✝ then ⟦{ aig := aig, ref := expr.getRef idx h }, assign⟧ else false
Tactic:
split <;> simp
State after:
no goals