Theorem: BVPred.mkEq_denote_eq_eval_beq
Proof state before:
case mp.pred
α : Type
inst✝² : BEq α
inst✝¹ : Hashable α
inst✝ : DecidableEq α
w : Nat
aig : AIG α
pair : aig.BinaryRefStream w
assign : α → Bool
lhs rhs : BitVec w
hleft : ∀ (idx : Nat) (hidx : idx < w), ⟦{ aig := aig, ref := pair.lhs.getRef idx hidx }, assign⟧ = lhs.getLsb idx
hright : ∀ (idx : Nat) (hidx : idx < w), ⟦{ aig := aig, ref := pair.rhs.getRef idx hidx }, assign⟧ = rhs.getLsb idx
h :
  ∀ (idx : Nat) (hidx : idx < w),
    ⟦{ aig := aig, ref := pair.lhs.getRef idx hidx }, assign⟧ =
      ⟦{ aig := aig, ref := pair.rhs.getRef idx hidx }, assign⟧
i✝ : Fin w
⊢ ⟦{ aig := aig, ref := pair.lhs.getRef ↑i✝ ?mp.pred.hidx }, assign⟧ =
    ⟦{ aig := aig, ref := pair.rhs.getRef ↑i✝ ?mp.pred.hidx }, assign⟧

case mp.pred.hidx
α : Type
inst✝² : BEq α
inst✝¹ : Hashable α
inst✝ : DecidableEq α
w : Nat
aig : AIG α
pair : aig.BinaryRefStream w
assign : α → Bool
lhs rhs : BitVec w
hleft : ∀ (idx : Nat) (hidx : idx < w), ⟦{ aig := aig, ref := pair.lhs.getRef idx hidx }, assign⟧ = lhs.getLsb idx
hright : ∀ (idx : Nat) (hidx : idx < w), ⟦{ aig := aig, ref := pair.rhs.getRef idx hidx }, assign⟧ = rhs.getLsb idx
h :
  ∀ (idx : Nat) (hidx : idx < w),
    ⟦{ aig := aig, ref := pair.lhs.getRef idx hidx }, assign⟧ =
      ⟦{ aig := aig, ref := pair.rhs.getRef idx hidx }, assign⟧
i✝ : Fin w
⊢ ↑i✝ < w

case mp.pred.hidx
α : Type
inst✝² : BEq α
inst✝¹ : Hashable α
inst✝ : DecidableEq α
w : Nat
aig : AIG α
pair : aig.BinaryRefStream w
assign : α → Bool
lhs rhs : BitVec w
hleft : ∀ (idx : Nat) (hidx : idx < w), ⟦{ aig := aig, ref := pair.lhs.getRef idx hidx }, assign⟧ = lhs.getLsb idx
hright : ∀ (idx : Nat) (hidx : idx < w), ⟦{ aig := aig, ref := pair.rhs.getRef idx hidx }, assign⟧ = rhs.getLsb idx
h :
  ∀ (idx : Nat) (hidx : idx < w),
    ⟦{ aig := aig, ref := pair.lhs.getRef idx hidx }, assign⟧ =
      ⟦{ aig := aig, ref := pair.rhs.getRef idx hidx }, assign⟧
i✝ : Fin w
⊢ ↑i✝ < w

case mp.pred.hidx
α : Type
inst✝² : BEq α
inst✝¹ : Hashable α
inst✝ : DecidableEq α
w : Nat
aig : AIG α
pair : aig.BinaryRefStream w
assign : α → Bool
lhs rhs : BitVec w
hleft : ∀ (idx : Nat) (hidx : idx < w), ⟦{ aig := aig, ref := pair.lhs.getRef idx hidx }, assign⟧ = lhs.getLsb idx
hright : ∀ (idx : Nat) (hidx : idx < w), ⟦{ aig := aig, ref := pair.rhs.getRef idx hidx }, assign⟧ = rhs.getLsb idx
h :
  ∀ (idx : Nat) (hidx : idx < w),
    ⟦{ aig := aig, ref := pair.lhs.getRef idx hidx }, assign⟧ =
      ⟦{ aig := aig, ref := pair.rhs.getRef idx hidx }, assign⟧
i✝ : Fin w
⊢ ↑i✝ < w
Tactic:
. simp [h]
Proof state after:
case mp.pred.hidx
α : Type
inst✝² : BEq α
inst✝¹ : Hashable α
inst✝ : DecidableEq α
w : Nat
aig : AIG α
pair : aig.BinaryRefStream w
assign : α → Bool
lhs rhs : BitVec w
hleft : ∀ (idx : Nat) (hidx : idx < w), ⟦{ aig := aig, ref := pair.lhs.getRef idx hidx }, assign⟧ = lhs.getLsb idx
hright : ∀ (idx : Nat) (hidx : idx < w), ⟦{ aig := aig, ref := pair.rhs.getRef idx hidx }, assign⟧ = rhs.getLsb idx
h :
  ∀ (idx : Nat) (hidx : idx < w),
    ⟦{ aig := aig, ref := pair.lhs.getRef idx hidx }, assign⟧ =
      ⟦{ aig := aig, ref := pair.rhs.getRef idx hidx }, assign⟧
i✝ : Fin w
⊢ ↑i✝ < w

case mp.pred.hidx
α : Type
inst✝² : BEq α
inst✝¹ : Hashable α
inst✝ : DecidableEq α
w : Nat
aig : AIG α
pair : aig.BinaryRefStream w
assign : α → Bool
lhs rhs : BitVec w
hleft : ∀ (idx : Nat) (hidx : idx < w), ⟦{ aig := aig, ref := pair.lhs.getRef idx hidx }, assign⟧ = lhs.getLsb idx
hright : ∀ (idx : Nat) (hidx : idx < w), ⟦{ aig := aig, ref := pair.rhs.getRef idx hidx }, assign⟧ = rhs.getLsb idx
h :
  ∀ (idx : Nat) (hidx : idx < w),
    ⟦{ aig := aig, ref := pair.lhs.getRef idx hidx }, assign⟧ =
      ⟦{ aig := aig, ref := pair.rhs.getRef idx hidx }, assign⟧
i✝ : Fin w
⊢ ↑i✝ < w

case mp.pred.hidx
α : Type
inst✝² : BEq α
inst✝¹ : Hashable α
inst✝ : DecidableEq α
w : Nat
aig : AIG α
pair : aig.BinaryRefStream w
assign : α → Bool
lhs rhs : BitVec w
hleft : ∀ (idx : Nat) (hidx : idx < w), ⟦{ aig := aig, ref := pair.lhs.getRef idx hidx }, assign⟧ = lhs.getLsb idx
hright : ∀ (idx : Nat) (hidx : idx < w), ⟦{ aig := aig, ref := pair.rhs.getRef idx hidx }, assign⟧ = rhs.getLsb idx
h :
  ∀ (idx : Nat) (hidx : idx < w),
    ⟦{ aig := aig, ref := pair.lhs.getRef idx hidx }, assign⟧ =
      ⟦{ aig := aig, ref := pair.rhs.getRef idx hidx }, assign⟧
i✝ : Fin w
⊢ ↑i✝ < w