Theorem: BVPred.mkUlt_denote_eq_eval_ult
Proof state before:
case e_a
α : Type
inst✝² : BEq α
inst✝¹ : Hashable α
inst✝ : DecidableEq α
w : Nat
aig : AIG α
lhs rhs : BitVec w
input : aig.BinaryRefStream w
assign : α → Bool
hleft : ∀ (idx : Nat) (hidx : idx < w), ⟦{ aig := aig, ref := input.lhs.getRef idx hidx }, assign⟧ = lhs.getLsb idx
hright : ∀ (idx : Nat) (hidx : idx < w), ⟦{ aig := aig, ref := input.rhs.getRef idx hidx }, assign⟧ = rhs.getLsb idx
⊢ BitVec.carry
      { w := w, stream := { lhs := input.lhs.cast ⋯, rhs := (BVExpr.bitblast.blastNot aig input.rhs).stream.cast ⋯ },
          cin := ((BVExpr.bitblast.blastNot aig input.rhs).aig.mkConstCached true).ref }.w
      lhs (~~~rhs)
      ⟦{ aig := ((BVExpr.bitblast.blastNot aig input.rhs).aig.mkConstCached true).aig,
          ref :=
            { w := w,
                stream := { lhs := input.lhs.cast ⋯, rhs := (BVExpr.bitblast.blastNot aig input.rhs).stream.cast ⋯ },
                cin := ((BVExpr.bitblast.blastNot aig input.rhs).aig.mkConstCached true).ref }.cin },
        assign⟧ =
    BitVec.carry w lhs (~~~rhs) true

case e_a.hleft
α : Type
inst✝² : BEq α
inst✝¹ : Hashable α
inst✝ : DecidableEq α
w : Nat
aig : AIG α
lhs rhs : BitVec w
input : aig.BinaryRefStream w
assign : α → Bool
hleft : ∀ (idx : Nat) (hidx : idx < w), ⟦{ aig := aig, ref := input.lhs.getRef idx hidx }, assign⟧ = lhs.getLsb idx
hright : ∀ (idx : Nat) (hidx : idx < w), ⟦{ aig := aig, ref := input.rhs.getRef idx hidx }, assign⟧ = rhs.getLsb idx
⊢ ∀ (idx : Nat)
    (hidx :
      idx <
        { w := w, stream := { lhs := input.lhs.cast ⋯, rhs := (BVExpr.bitblast.blastNot aig input.rhs).stream.cast ⋯ },
            cin := ((BVExpr.bitblast.blastNot aig input.rhs).aig.mkConstCached true).ref }.w),
    ⟦{ aig := ((BVExpr.bitblast.blastNot aig input.rhs).aig.mkConstCached true).aig,
          ref :=
            { w := w,
                      stream :=
                        { lhs := input.lhs.cast ⋯, rhs := (BVExpr.bitblast.blastNot aig input.rhs).stream.cast ⋯ },
                      cin := ((BVExpr.bitblast.blastNot aig input.rhs).aig.mkConstCached true).ref }.stream.lhs.getRef
              idx hidx },
        assign⟧ =
      lhs.getLsb idx

case e_a.hright
α : Type
inst✝² : BEq α
inst✝¹ : Hashable α
inst✝ : DecidableEq α
w : Nat
aig : AIG α
lhs rhs : BitVec w
input : aig.BinaryRefStream w
assign : α → Bool
hleft : ∀ (idx : Nat) (hidx : idx < w), ⟦{ aig := aig, ref := input.lhs.getRef idx hidx }, assign⟧ = lhs.getLsb idx
hright : ∀ (idx : Nat) (hidx : idx < w), ⟦{ aig := aig, ref := input.rhs.getRef idx hidx }, assign⟧ = rhs.getLsb idx
⊢ ∀ (idx : Nat)
    (hidx :
      idx <
        { w := w, stream := { lhs := input.lhs.cast ⋯, rhs := (BVExpr.bitblast.blastNot aig input.rhs).stream.cast ⋯ },
            cin := ((BVExpr.bitblast.blastNot aig input.rhs).aig.mkConstCached true).ref }.w),
    ⟦{ aig := ((BVExpr.bitblast.blastNot aig input.rhs).aig.mkConstCached true).aig,
          ref :=
            { w := w,
                      stream :=
                        { lhs := input.lhs.cast ⋯, rhs := (BVExpr.bitblast.blastNot aig input.rhs).stream.cast ⋯ },
                      cin := ((BVExpr.bitblast.blastNot aig input.rhs).aig.mkConstCached true).ref }.stream.rhs.getRef
              idx hidx },
        assign⟧ =
      (~~~rhs).getLsb idx
Tactic:
. simp
Proof state after:
case e_a.hleft
α : Type
inst✝² : BEq α
inst✝¹ : Hashable α
inst✝ : DecidableEq α
w : Nat
aig : AIG α
lhs rhs : BitVec w
input : aig.BinaryRefStream w
assign : α → Bool
hleft : ∀ (idx : Nat) (hidx : idx < w), ⟦{ aig := aig, ref := input.lhs.getRef idx hidx }, assign⟧ = lhs.getLsb idx
hright : ∀ (idx : Nat) (hidx : idx < w), ⟦{ aig := aig, ref := input.rhs.getRef idx hidx }, assign⟧ = rhs.getLsb idx
⊢ ∀ (idx : Nat)
    (hidx :
      idx <
        { w := w, stream := { lhs := input.lhs.cast ⋯, rhs := (BVExpr.bitblast.blastNot aig input.rhs).stream.cast ⋯ },
            cin := ((BVExpr.bitblast.blastNot aig input.rhs).aig.mkConstCached true).ref }.w),
    ⟦{ aig := ((BVExpr.bitblast.blastNot aig input.rhs).aig.mkConstCached true).aig,
          ref :=
            { w := w,
                      stream :=
                        { lhs := input.lhs.cast ⋯, rhs := (BVExpr.bitblast.blastNot aig input.rhs).stream.cast ⋯ },
                      cin := ((BVExpr.bitblast.blastNot aig input.rhs).aig.mkConstCached true).ref }.stream.lhs.getRef
              idx hidx },
        assign⟧ =
      lhs.getLsb idx

case e_a.hright
α : Type
inst✝² : BEq α
inst✝¹ : Hashable α
inst✝ : DecidableEq α
w : Nat
aig : AIG α
lhs rhs : BitVec w
input : aig.BinaryRefStream w
assign : α → Bool
hleft : ∀ (idx : Nat) (hidx : idx < w), ⟦{ aig := aig, ref := input.lhs.getRef idx hidx }, assign⟧ = lhs.getLsb idx
hright : ∀ (idx : Nat) (hidx : idx < w), ⟦{ aig := aig, ref := input.rhs.getRef idx hidx }, assign⟧ = rhs.getLsb idx
⊢ ∀ (idx : Nat)
    (hidx :
      idx <
        { w := w, stream := { lhs := input.lhs.cast ⋯, rhs := (BVExpr.bitblast.blastNot aig input.rhs).stream.cast ⋯ },
            cin := ((BVExpr.bitblast.blastNot aig input.rhs).aig.mkConstCached true).ref }.w),
    ⟦{ aig := ((BVExpr.bitblast.blastNot aig input.rhs).aig.mkConstCached true).aig,
          ref :=
            { w := w,
                      stream :=
                        { lhs := input.lhs.cast ⋯, rhs := (BVExpr.bitblast.blastNot aig input.rhs).stream.cast ⋯ },
                      cin := ((BVExpr.bitblast.blastNot aig input.rhs).aig.mkConstCached true).ref }.stream.rhs.getRef
              idx hidx },
        assign⟧ =
      (~~~rhs).getLsb idx