Theorem: BVExpr.bitblast.blastAdd_eq_eval_getLsb (LeanSAT/Reflect/BVExpr/BitBlast/Lemmas/Add.lean)

State before:
α : Type
inst✝² : BEq α
inst✝¹ : Hashable α
inst✝ : DecidableEq α
w : Nat
aig : AIG α
lhs rhs : BitVec w
assign : α → Bool
input : aig.BinaryRefStream w
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),
    ⟦{ aig := (blastAdd aig input).aig, ref := (blastAdd aig input).stream.getRef idx hidx }, assign⟧ =
      (lhs + rhs).getLsb idx
Tactic:
intro idx hidx
State after:
α : Type
inst✝² : BEq α
inst✝¹ : Hashable α
inst✝ : DecidableEq α
w : Nat
aig : AIG α
lhs rhs : BitVec w
assign : α → Bool
input : aig.BinaryRefStream w
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
⊢ ⟦{ aig := (blastAdd aig input).aig, ref := (blastAdd aig input).stream.getRef idx hidx }, assign⟧ =
    (lhs + rhs).getLsb idx

State before:
α : Type
inst✝² : BEq α
inst✝¹ : Hashable α
inst✝ : DecidableEq α
w : Nat
aig : AIG α
lhs rhs : BitVec w
assign : α → Bool
input : aig.BinaryRefStream w
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
⊢ ⟦{ aig := (blastAdd aig input).aig, ref := (blastAdd aig input).stream.getRef idx hidx }, assign⟧ =
    (lhs + rhs).getLsb idx
Tactic:
rw [BitVec.getLsb_add]
State after:
α : Type
inst✝² : BEq α
inst✝¹ : Hashable α
inst✝ : DecidableEq α
w : Nat
aig : AIG α
lhs rhs : BitVec w
assign : α → Bool
input : aig.BinaryRefStream w
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
⊢ ⟦{ aig := (blastAdd aig input).aig, ref := (blastAdd aig input).stream.getRef idx hidx }, assign⟧ =
    (lhs.getLsb idx).xor ((rhs.getLsb idx).xor (BitVec.carry idx lhs rhs false))

case i_lt
α : Type
inst✝² : BEq α
inst✝¹ : Hashable α
inst✝ : DecidableEq α
w : Nat
aig : AIG α
lhs rhs : BitVec w
assign : α → Bool
input : aig.BinaryRefStream w
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
⊢ idx < w

State before:
α : Type
inst✝² : BEq α
inst✝¹ : Hashable α
inst✝ : DecidableEq α
w : Nat
aig : AIG α
lhs rhs : BitVec w
assign : α → Bool
input : aig.BinaryRefStream w
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
⊢ ⟦{ aig := (blastAdd aig input).aig, ref := (blastAdd aig input).stream.getRef idx hidx }, assign⟧ =
    (lhs.getLsb idx).xor ((rhs.getLsb idx).xor (BitVec.carry idx lhs rhs false))

case i_lt
α : Type
inst✝² : BEq α
inst✝¹ : Hashable α
inst✝ : DecidableEq α
w : Nat
aig : AIG α
lhs rhs : BitVec w
assign : α → Bool
input : aig.BinaryRefStream w
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
⊢ idx < w
Tactic:
. rw [← hleft idx hidx]
  rw [← hright idx hidx]
  unfold blastAdd
  dsimp
  rw [blastAdd.go_eq_eval_getLsb _ 0 (by omega) _ _ _ _ assign lhs rhs _ _]
  . simp only [BinaryRefStream.lhs_getRef_cast, Ref_cast', BinaryRefStream.rhs_getRef_cast]
    rw [LawfulOperator.denote_mem_prefix (f := mkConstCached)]
    rw [LawfulOperator.denote_mem_prefix (f := mkConstCached)]
  . simp
  . omega
  . intros
    simp only [BinaryRefStream.lhs_getRef_cast, Ref_cast']
    rw [LawfulOperator.denote_mem_prefix (f := mkConstCached)]
    rw [hleft]
  . intros
    simp only [BinaryRefStream.rhs_getRef_cast, Ref_cast']
    rw [LawfulOperator.denote_mem_prefix (f := mkConstCached)]
    rw [hright]
State after:
case i_lt
α : Type
inst✝² : BEq α
inst✝¹ : Hashable α
inst✝ : DecidableEq α
w : Nat
aig : AIG α
lhs rhs : BitVec w
assign : α → Bool
input : aig.BinaryRefStream w
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
⊢ idx < w

State before:
case i_lt
α : Type
inst✝² : BEq α
inst✝¹ : Hashable α
inst✝ : DecidableEq α
w : Nat
aig : AIG α
lhs rhs : BitVec w
assign : α → Bool
input : aig.BinaryRefStream w
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
⊢ idx < w
Tactic:
. assumption
State after:
no goals

State before:
α : Type
inst✝² : BEq α
inst✝¹ : Hashable α
inst✝ : DecidableEq α
w : Nat
aig : AIG α
lhs rhs : BitVec w
assign : α → Bool
input : aig.BinaryRefStream w
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
⊢ ⟦{ aig := (blastAdd aig input).aig, ref := (blastAdd aig input).stream.getRef idx hidx }, assign⟧ =
    (lhs.getLsb idx).xor ((rhs.getLsb idx).xor (BitVec.carry idx lhs rhs false))
Tactic:
rw [← hleft idx hidx]
State after:
α : Type
inst✝² : BEq α
inst✝¹ : Hashable α
inst✝ : DecidableEq α
w : Nat
aig : AIG α
lhs rhs : BitVec w
assign : α → Bool
input : aig.BinaryRefStream w
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
⊢ ⟦{ aig := (blastAdd aig input).aig, ref := (blastAdd aig input).stream.getRef idx hidx }, assign⟧ =
    ⟦{ aig := aig, ref := input.lhs.getRef idx hidx }, assign⟧.xor
      ((rhs.getLsb idx).xor (BitVec.carry idx lhs rhs false))

State before:
α : Type
inst✝² : BEq α
inst✝¹ : Hashable α
inst✝ : DecidableEq α
w : Nat
aig : AIG α
lhs rhs : BitVec w
assign : α → Bool
input : aig.BinaryRefStream w
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
⊢ ⟦{ aig := (blastAdd aig input).aig, ref := (blastAdd aig input).stream.getRef idx hidx }, assign⟧ =
    ⟦{ aig := aig, ref := input.lhs.getRef idx hidx }, assign⟧.xor
      ((rhs.getLsb idx).xor (BitVec.carry idx lhs rhs false))
Tactic:
rw [← hright idx hidx]
State after:
α : Type
inst✝² : BEq α
inst✝¹ : Hashable α
inst✝ : DecidableEq α
w : Nat
aig : AIG α
lhs rhs : BitVec w
assign : α → Bool
input : aig.BinaryRefStream w
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
⊢ ⟦{ aig := (blastAdd aig input).aig, ref := (blastAdd aig input).stream.getRef idx hidx }, assign⟧ =
    ⟦{ aig := aig, ref := input.lhs.getRef idx hidx }, assign⟧.xor
      (⟦{ aig := aig, ref := input.rhs.getRef idx hidx }, assign⟧.xor (BitVec.carry idx lhs rhs false))

State before:
α : Type
inst✝² : BEq α
inst✝¹ : Hashable α
inst✝ : DecidableEq α
w : Nat
aig : AIG α
lhs rhs : BitVec w
assign : α → Bool
input : aig.BinaryRefStream w
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
⊢ ⟦{ aig := (blastAdd aig input).aig, ref := (blastAdd aig input).stream.getRef idx hidx }, assign⟧ =
    ⟦{ aig := aig, ref := input.lhs.getRef idx hidx }, assign⟧.xor
      (⟦{ aig := aig, ref := input.rhs.getRef idx hidx }, assign⟧.xor (BitVec.carry idx lhs rhs false))
Tactic:
unfold blastAdd
State after:
α : Type
inst✝² : BEq α
inst✝¹ : Hashable α
inst✝ : DecidableEq α
w : Nat
aig : AIG α
lhs rhs : BitVec w
assign : α → Bool
input : aig.BinaryRefStream w
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
⊢ ⟦{
        aig :=
          (let res := aig.mkConstCached false;
            let aig_1 := res.aig;
            let cin := res.ref;
            let input := input.cast ⋯;
            match input with
            | { lhs := lhs, rhs := rhs } => blastAdd.go aig_1 0 ⋯ cin RefStream.empty lhs rhs).aig,
        ref :=
          (let res := aig.mkConstCached false;
                let aig_1 := res.aig;
                let cin := res.ref;
                let input := input.cast ⋯;
                match input with
                | { lhs := lhs, rhs := rhs } => blastAdd.go aig_1 0 ⋯ cin RefStream.empty lhs rhs).stream.getRef
            idx hidx },
      assign⟧ =
    ⟦{ aig := aig, ref := input.lhs.getRef idx hidx }, assign⟧.xor
      (⟦{ aig := aig, ref := input.rhs.getRef idx hidx }, assign⟧.xor (BitVec.carry idx lhs rhs false))

State before:
α : Type
inst✝² : BEq α
inst✝¹ : Hashable α
inst✝ : DecidableEq α
w : Nat
aig : AIG α
lhs rhs : BitVec w
assign : α → Bool
input : aig.BinaryRefStream w
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
⊢ ⟦{
        aig :=
          (let res := aig.mkConstCached false;
            let aig_1 := res.aig;
            let cin := res.ref;
            let input := input.cast ⋯;
            match input with
            | { lhs := lhs, rhs := rhs } => blastAdd.go aig_1 0 ⋯ cin RefStream.empty lhs rhs).aig,
        ref :=
          (let res := aig.mkConstCached false;
                let aig_1 := res.aig;
                let cin := res.ref;
                let input := input.cast ⋯;
                match input with
                | { lhs := lhs, rhs := rhs } => blastAdd.go aig_1 0 ⋯ cin RefStream.empty lhs rhs).stream.getRef
            idx hidx },
      assign⟧ =
    ⟦{ aig := aig, ref := input.lhs.getRef idx hidx }, assign⟧.xor
      (⟦{ aig := aig, ref := input.rhs.getRef idx hidx }, assign⟧.xor (BitVec.carry idx lhs rhs false))
Tactic:
dsimp
State after:
α : Type
inst✝² : BEq α
inst✝¹ : Hashable α
inst✝ : DecidableEq α
w : Nat
aig : AIG α
lhs rhs : BitVec w
assign : α → Bool
input : aig.BinaryRefStream w
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
⊢ ⟦{
        aig :=
          (blastAdd.go (aig.mkConstCached false).aig 0 ⋯ (aig.mkConstCached false).ref RefStream.empty
              (input.cast ⋯).lhs (input.cast ⋯).rhs).aig,
        ref :=
          (blastAdd.go (aig.mkConstCached false).aig 0 ⋯ (aig.mkConstCached false).ref RefStream.empty
                  (input.cast ⋯).lhs (input.cast ⋯).rhs).stream.getRef
            idx hidx },
      assign⟧ =
    ⟦{ aig := aig, ref := input.lhs.getRef idx hidx }, assign⟧.xor
      (⟦{ aig := aig, ref := input.rhs.getRef idx hidx }, assign⟧.xor (BitVec.carry idx lhs rhs false))

State before:
α : Type
inst✝² : BEq α
inst✝¹ : Hashable α
inst✝ : DecidableEq α
w : Nat
aig : AIG α
lhs rhs : BitVec w
assign : α → Bool
input : aig.BinaryRefStream w
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
⊢ ⟦{
        aig :=
          (blastAdd.go (aig.mkConstCached false).aig 0 ⋯ (aig.mkConstCached false).ref RefStream.empty
              (input.cast ⋯).lhs (input.cast ⋯).rhs).aig,
        ref :=
          (blastAdd.go (aig.mkConstCached false).aig 0 ⋯ (aig.mkConstCached false).ref RefStream.empty
                  (input.cast ⋯).lhs (input.cast ⋯).rhs).stream.getRef
            idx hidx },
      assign⟧ =
    ⟦{ aig := aig, ref := input.lhs.getRef idx hidx }, assign⟧.xor
      (⟦{ aig := aig, ref := input.rhs.getRef idx hidx }, assign⟧.xor (BitVec.carry idx lhs rhs false))
Tactic:
rw [blastAdd.go_eq_eval_getLsb _ 0 (by omega) _ _ _ _ assign lhs rhs _ _]
State after:
α : Type
inst✝² : BEq α
inst✝¹ : Hashable α
inst✝ : DecidableEq α
w : Nat
aig : AIG α
lhs rhs : BitVec w
assign : α → Bool
input : aig.BinaryRefStream w
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
⊢ ⟦{ aig := (aig.mkConstCached false).aig, ref := (input.cast ⋯).lhs.getRef idx hidx }, assign⟧.xor
      (⟦{ aig := (aig.mkConstCached false).aig, ref := (input.cast ⋯).rhs.getRef idx hidx }, assign⟧.xor
        (BitVec.carry idx lhs rhs false)) =
    ⟦{ aig := aig, ref := input.lhs.getRef idx hidx }, assign⟧.xor
      (⟦{ aig := aig, ref := input.rhs.getRef idx hidx }, assign⟧.xor (BitVec.carry idx lhs rhs false))

case hcin
α : Type
inst✝² : BEq α
inst✝¹ : Hashable α
inst✝ : DecidableEq α
w : Nat
aig : AIG α
lhs rhs : BitVec w
assign : α → Bool
input : aig.BinaryRefStream w
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
⊢ ⟦{ aig := (aig.mkConstCached false).aig, ref := (aig.mkConstCached false).ref }, assign⟧ =
    BitVec.carry 0 lhs rhs false

case a
α : Type
inst✝² : BEq α
inst✝¹ : Hashable α
inst✝ : DecidableEq α
w : Nat
aig : AIG α
lhs rhs : BitVec w
assign : α → Bool
input : aig.BinaryRefStream w
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
⊢ 0 ≤ idx

α : Type
inst✝² : BEq α
inst✝¹ : Hashable α
inst✝ : DecidableEq α
w : Nat
aig : AIG α
lhs rhs : BitVec w
assign : α → Bool
input : aig.BinaryRefStream w
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
⊢ ∀ (idx : Nat) (hidx : idx < w),
    ⟦{ aig := (aig.mkConstCached false).aig, ref := (input.cast ⋯).lhs.getRef idx hidx }, assign⟧ = lhs.getLsb idx

α : Type
inst✝² : BEq α
inst✝¹ : Hashable α
inst✝ : DecidableEq α
w : Nat
aig : AIG α
lhs rhs : BitVec w
assign : α → Bool
input : aig.BinaryRefStream w
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
⊢ ∀ (idx : Nat) (hidx : idx < w),
    ⟦{ aig := (aig.mkConstCached false).aig, ref := (input.cast ⋯).rhs.getRef idx hidx }, assign⟧ = rhs.getLsb idx

State before:
α : Type
inst✝² : BEq α
inst✝¹ : Hashable α
inst✝ : DecidableEq α
w : Nat
aig : AIG α
lhs rhs : BitVec w
assign : α → Bool
input : aig.BinaryRefStream w
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
⊢ ⟦{ aig := (aig.mkConstCached false).aig, ref := (input.cast ⋯).lhs.getRef idx hidx }, assign⟧.xor
      (⟦{ aig := (aig.mkConstCached false).aig, ref := (input.cast ⋯).rhs.getRef idx hidx }, assign⟧.xor
        (BitVec.carry idx lhs rhs false)) =
    ⟦{ aig := aig, ref := input.lhs.getRef idx hidx }, assign⟧.xor
      (⟦{ aig := aig, ref := input.rhs.getRef idx hidx }, assign⟧.xor (BitVec.carry idx lhs rhs false))

case hcin
α : Type
inst✝² : BEq α
inst✝¹ : Hashable α
inst✝ : DecidableEq α
w : Nat
aig : AIG α
lhs rhs : BitVec w
assign : α → Bool
input : aig.BinaryRefStream w
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
⊢ ⟦{ aig := (aig.mkConstCached false).aig, ref := (aig.mkConstCached false).ref }, assign⟧ =
    BitVec.carry 0 lhs rhs false

case a
α : Type
inst✝² : BEq α
inst✝¹ : Hashable α
inst✝ : DecidableEq α
w : Nat
aig : AIG α
lhs rhs : BitVec w
assign : α → Bool
input : aig.BinaryRefStream w
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
⊢ 0 ≤ idx

α : Type
inst✝² : BEq α
inst✝¹ : Hashable α
inst✝ : DecidableEq α
w : Nat
aig : AIG α
lhs rhs : BitVec w
assign : α → Bool
input : aig.BinaryRefStream w
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
⊢ ∀ (idx : Nat) (hidx : idx < w),
    ⟦{ aig := (aig.mkConstCached false).aig, ref := (input.cast ⋯).lhs.getRef idx hidx }, assign⟧ = lhs.getLsb idx

α : Type
inst✝² : BEq α
inst✝¹ : Hashable α
inst✝ : DecidableEq α
w : Nat
aig : AIG α
lhs rhs : BitVec w
assign : α → Bool
input : aig.BinaryRefStream w
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
⊢ ∀ (idx : Nat) (hidx : idx < w),
    ⟦{ aig := (aig.mkConstCached false).aig, ref := (input.cast ⋯).rhs.getRef idx hidx }, assign⟧ = rhs.getLsb idx
Tactic:
. simp only [BinaryRefStream.lhs_getRef_cast, Ref_cast', BinaryRefStream.rhs_getRef_cast]
  rw [LawfulOperator.denote_mem_prefix (f := mkConstCached)]
  rw [LawfulOperator.denote_mem_prefix (f := mkConstCached)]
State after:
case hcin
α : Type
inst✝² : BEq α
inst✝¹ : Hashable α
inst✝ : DecidableEq α
w : Nat
aig : AIG α
lhs rhs : BitVec w
assign : α → Bool
input : aig.BinaryRefStream w
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
⊢ ⟦{ aig := (aig.mkConstCached false).aig, ref := (aig.mkConstCached false).ref }, assign⟧ =
    BitVec.carry 0 lhs rhs false

case a
α : Type
inst✝² : BEq α
inst✝¹ : Hashable α
inst✝ : DecidableEq α
w : Nat
aig : AIG α
lhs rhs : BitVec w
assign : α → Bool
input : aig.BinaryRefStream w
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
⊢ 0 ≤ idx

α : Type
inst✝² : BEq α
inst✝¹ : Hashable α
inst✝ : DecidableEq α
w : Nat
aig : AIG α
lhs rhs : BitVec w
assign : α → Bool
input : aig.BinaryRefStream w
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
⊢ ∀ (idx : Nat) (hidx : idx < w),
    ⟦{ aig := (aig.mkConstCached false).aig, ref := (input.cast ⋯).lhs.getRef idx hidx }, assign⟧ = lhs.getLsb idx

α : Type
inst✝² : BEq α
inst✝¹ : Hashable α
inst✝ : DecidableEq α
w : Nat
aig : AIG α
lhs rhs : BitVec w
assign : α → Bool
input : aig.BinaryRefStream w
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
⊢ ∀ (idx : Nat) (hidx : idx < w),
    ⟦{ aig := (aig.mkConstCached false).aig, ref := (input.cast ⋯).rhs.getRef idx hidx }, assign⟧ = rhs.getLsb idx

State before:
case hcin
α : Type
inst✝² : BEq α
inst✝¹ : Hashable α
inst✝ : DecidableEq α
w : Nat
aig : AIG α
lhs rhs : BitVec w
assign : α → Bool
input : aig.BinaryRefStream w
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
⊢ ⟦{ aig := (aig.mkConstCached false).aig, ref := (aig.mkConstCached false).ref }, assign⟧ =
    BitVec.carry 0 lhs rhs false

case a
α : Type
inst✝² : BEq α
inst✝¹ : Hashable α
inst✝ : DecidableEq α
w : Nat
aig : AIG α
lhs rhs : BitVec w
assign : α → Bool
input : aig.BinaryRefStream w
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
⊢ 0 ≤ idx

α : Type
inst✝² : BEq α
inst✝¹ : Hashable α
inst✝ : DecidableEq α
w : Nat
aig : AIG α
lhs rhs : BitVec w
assign : α → Bool
input : aig.BinaryRefStream w
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
⊢ ∀ (idx : Nat) (hidx : idx < w),
    ⟦{ aig := (aig.mkConstCached false).aig, ref := (input.cast ⋯).lhs.getRef idx hidx }, assign⟧ = lhs.getLsb idx

α : Type
inst✝² : BEq α
inst✝¹ : Hashable α
inst✝ : DecidableEq α
w : Nat
aig : AIG α
lhs rhs : BitVec w
assign : α → Bool
input : aig.BinaryRefStream w
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
⊢ ∀ (idx : Nat) (hidx : idx < w),
    ⟦{ aig := (aig.mkConstCached false).aig, ref := (input.cast ⋯).rhs.getRef idx hidx }, assign⟧ = rhs.getLsb idx
Tactic:
. simp
State after:
case a
α : Type
inst✝² : BEq α
inst✝¹ : Hashable α
inst✝ : DecidableEq α
w : Nat
aig : AIG α
lhs rhs : BitVec w
assign : α → Bool
input : aig.BinaryRefStream w
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
⊢ 0 ≤ idx

α : Type
inst✝² : BEq α
inst✝¹ : Hashable α
inst✝ : DecidableEq α
w : Nat
aig : AIG α
lhs rhs : BitVec w
assign : α → Bool
input : aig.BinaryRefStream w
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
⊢ ∀ (idx : Nat) (hidx : idx < w),
    ⟦{ aig := (aig.mkConstCached false).aig, ref := (input.cast ⋯).lhs.getRef idx hidx }, assign⟧ = lhs.getLsb idx

α : Type
inst✝² : BEq α
inst✝¹ : Hashable α
inst✝ : DecidableEq α
w : Nat
aig : AIG α
lhs rhs : BitVec w
assign : α → Bool
input : aig.BinaryRefStream w
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
⊢ ∀ (idx : Nat) (hidx : idx < w),
    ⟦{ aig := (aig.mkConstCached false).aig, ref := (input.cast ⋯).rhs.getRef idx hidx }, assign⟧ = rhs.getLsb idx

State before:
case a
α : Type
inst✝² : BEq α
inst✝¹ : Hashable α
inst✝ : DecidableEq α
w : Nat
aig : AIG α
lhs rhs : BitVec w
assign : α → Bool
input : aig.BinaryRefStream w
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
⊢ 0 ≤ idx

α : Type
inst✝² : BEq α
inst✝¹ : Hashable α
inst✝ : DecidableEq α
w : Nat
aig : AIG α
lhs rhs : BitVec w
assign : α → Bool
input : aig.BinaryRefStream w
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
⊢ ∀ (idx : Nat) (hidx : idx < w),
    ⟦{ aig := (aig.mkConstCached false).aig, ref := (input.cast ⋯).lhs.getRef idx hidx }, assign⟧ = lhs.getLsb idx

α : Type
inst✝² : BEq α
inst✝¹ : Hashable α
inst✝ : DecidableEq α
w : Nat
aig : AIG α
lhs rhs : BitVec w
assign : α → Bool
input : aig.BinaryRefStream w
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
⊢ ∀ (idx : Nat) (hidx : idx < w),
    ⟦{ aig := (aig.mkConstCached false).aig, ref := (input.cast ⋯).rhs.getRef idx hidx }, assign⟧ = rhs.getLsb idx
Tactic:
. omega
State after:
α : Type
inst✝² : BEq α
inst✝¹ : Hashable α
inst✝ : DecidableEq α
w : Nat
aig : AIG α
lhs rhs : BitVec w
assign : α → Bool
input : aig.BinaryRefStream w
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
⊢ ∀ (idx : Nat) (hidx : idx < w),
    ⟦{ aig := (aig.mkConstCached false).aig, ref := (input.cast ⋯).lhs.getRef idx hidx }, assign⟧ = lhs.getLsb idx

α : Type
inst✝² : BEq α
inst✝¹ : Hashable α
inst✝ : DecidableEq α
w : Nat
aig : AIG α
lhs rhs : BitVec w
assign : α → Bool
input : aig.BinaryRefStream w
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
⊢ ∀ (idx : Nat) (hidx : idx < w),
    ⟦{ aig := (aig.mkConstCached false).aig, ref := (input.cast ⋯).rhs.getRef idx hidx }, assign⟧ = rhs.getLsb idx

State before:
α : Type
inst✝² : BEq α
inst✝¹ : Hashable α
inst✝ : DecidableEq α
w : Nat
aig : AIG α
lhs rhs : BitVec w
assign : α → Bool
input : aig.BinaryRefStream w
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
⊢ ∀ (idx : Nat) (hidx : idx < w),
    ⟦{ aig := (aig.mkConstCached false).aig, ref := (input.cast ⋯).lhs.getRef idx hidx }, assign⟧ = lhs.getLsb idx

α : Type
inst✝² : BEq α
inst✝¹ : Hashable α
inst✝ : DecidableEq α
w : Nat
aig : AIG α
lhs rhs : BitVec w
assign : α → Bool
input : aig.BinaryRefStream w
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
⊢ ∀ (idx : Nat) (hidx : idx < w),
    ⟦{ aig := (aig.mkConstCached false).aig, ref := (input.cast ⋯).rhs.getRef idx hidx }, assign⟧ = rhs.getLsb idx
Tactic:
. intros
  simp only [BinaryRefStream.lhs_getRef_cast, Ref_cast']
  rw [LawfulOperator.denote_mem_prefix (f := mkConstCached)]
  rw [hleft]
State after:
α : Type
inst✝² : BEq α
inst✝¹ : Hashable α
inst✝ : DecidableEq α
w : Nat
aig : AIG α
lhs rhs : BitVec w
assign : α → Bool
input : aig.BinaryRefStream w
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
⊢ ∀ (idx : Nat) (hidx : idx < w),
    ⟦{ aig := (aig.mkConstCached false).aig, ref := (input.cast ⋯).rhs.getRef idx hidx }, assign⟧ = rhs.getLsb idx

State before:
α : Type
inst✝² : BEq α
inst✝¹ : Hashable α
inst✝ : DecidableEq α
w : Nat
aig : AIG α
lhs rhs : BitVec w
assign : α → Bool
input : aig.BinaryRefStream w
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
⊢ ∀ (idx : Nat) (hidx : idx < w),
    ⟦{ aig := (aig.mkConstCached false).aig, ref := (input.cast ⋯).rhs.getRef idx hidx }, assign⟧ = rhs.getLsb idx
Tactic:
. intros
  simp only [BinaryRefStream.rhs_getRef_cast, Ref_cast']
  rw [LawfulOperator.denote_mem_prefix (f := mkConstCached)]
  rw [hright]
State after:
no goals

State before:
α : Type
inst✝² : BEq α
inst✝¹ : Hashable α
inst✝ : DecidableEq α
w : Nat
aig : AIG α
lhs rhs : BitVec w
assign : α → Bool
input : aig.BinaryRefStream w
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
⊢ 0 ≤ w
Tactic:
omega
State after:
no goals

State before:
α : Type
inst✝² : BEq α
inst✝¹ : Hashable α
inst✝ : DecidableEq α
w : Nat
aig : AIG α
lhs rhs : BitVec w
assign : α → Bool
input : aig.BinaryRefStream w
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
⊢ ⟦{ aig := (aig.mkConstCached false).aig, ref := (input.cast ⋯).lhs.getRef idx hidx }, assign⟧.xor
      (⟦{ aig := (aig.mkConstCached false).aig, ref := (input.cast ⋯).rhs.getRef idx hidx }, assign⟧.xor
        (BitVec.carry idx lhs rhs false)) =
    ⟦{ aig := aig, ref := input.lhs.getRef idx hidx }, assign⟧.xor
      (⟦{ aig := aig, ref := input.rhs.getRef idx hidx }, assign⟧.xor (BitVec.carry idx lhs rhs false))
Tactic:
simp only [BinaryRefStream.lhs_getRef_cast, Ref_cast', BinaryRefStream.rhs_getRef_cast]
State after:
α : Type
inst✝² : BEq α
inst✝¹ : Hashable α
inst✝ : DecidableEq α
w : Nat
aig : AIG α
lhs rhs : BitVec w
assign : α → Bool
input : aig.BinaryRefStream w
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
⊢ ⟦{ aig := (aig.mkConstCached false).aig, ref := { gate := (input.lhs.getRef idx hidx).gate, hgate := ⋯ } },
          assign⟧.xor
      (⟦{ aig := (aig.mkConstCached false).aig, ref := { gate := (input.rhs.getRef idx hidx).gate, hgate := ⋯ } },
            assign⟧.xor
        (BitVec.carry idx lhs rhs false)) =
    ⟦{ aig := aig, ref := input.lhs.getRef idx hidx }, assign⟧.xor
      (⟦{ aig := aig, ref := input.rhs.getRef idx hidx }, assign⟧.xor (BitVec.carry idx lhs rhs false))

State before:
α : Type
inst✝² : BEq α
inst✝¹ : Hashable α
inst✝ : DecidableEq α
w : Nat
aig : AIG α
lhs rhs : BitVec w
assign : α → Bool
input : aig.BinaryRefStream w
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
⊢ ⟦{ aig := (aig.mkConstCached false).aig, ref := { gate := (input.lhs.getRef idx hidx).gate, hgate := ⋯ } },
          assign⟧.xor
      (⟦{ aig := (aig.mkConstCached false).aig, ref := { gate := (input.rhs.getRef idx hidx).gate, hgate := ⋯ } },
            assign⟧.xor
        (BitVec.carry idx lhs rhs false)) =
    ⟦{ aig := aig, ref := input.lhs.getRef idx hidx }, assign⟧.xor
      (⟦{ aig := aig, ref := input.rhs.getRef idx hidx }, assign⟧.xor (BitVec.carry idx lhs rhs false))
Tactic:
rw [LawfulOperator.denote_mem_prefix (f := mkConstCached)]
State after:
α : Type
inst✝² : BEq α
inst✝¹ : Hashable α
inst✝ : DecidableEq α
w : Nat
aig : AIG α
lhs rhs : BitVec w
assign : α → Bool
input : aig.BinaryRefStream w
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
⊢ ⟦{ aig := aig, ref := { gate := (input.lhs.getRef idx hidx).gate, hgate := ?m.39871 } }, assign⟧.xor
      (⟦{ aig := (aig.mkConstCached false).aig, ref := { gate := (input.rhs.getRef idx hidx).gate, hgate := ⋯ } },
            assign⟧.xor
        (BitVec.carry idx lhs rhs false)) =
    ⟦{ aig := aig, ref := input.lhs.getRef idx hidx }, assign⟧.xor
      (⟦{ aig := aig, ref := input.rhs.getRef idx hidx }, assign⟧.xor (BitVec.carry idx lhs rhs false))

α : Type
inst✝² : BEq α
inst✝¹ : Hashable α
inst✝ : DecidableEq α
w : Nat
aig : AIG α
lhs rhs : BitVec w
assign : α → Bool
input : aig.BinaryRefStream w
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
⊢ (input.lhs.getRef idx hidx).gate < aig.decls.size

State before:
α : Type
inst✝² : BEq α
inst✝¹ : Hashable α
inst✝ : DecidableEq α
w : Nat
aig : AIG α
lhs rhs : BitVec w
assign : α → Bool
input : aig.BinaryRefStream w
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
⊢ ⟦{ aig := aig, ref := { gate := (input.lhs.getRef idx hidx).gate, hgate := ?m.39871 } }, assign⟧.xor
      (⟦{ aig := (aig.mkConstCached false).aig, ref := { gate := (input.rhs.getRef idx hidx).gate, hgate := ⋯ } },
            assign⟧.xor
        (BitVec.carry idx lhs rhs false)) =
    ⟦{ aig := aig, ref := input.lhs.getRef idx hidx }, assign⟧.xor
      (⟦{ aig := aig, ref := input.rhs.getRef idx hidx }, assign⟧.xor (BitVec.carry idx lhs rhs false))

α : Type
inst✝² : BEq α
inst✝¹ : Hashable α
inst✝ : DecidableEq α
w : Nat
aig : AIG α
lhs rhs : BitVec w
assign : α → Bool
input : aig.BinaryRefStream w
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
⊢ (input.lhs.getRef idx hidx).gate < aig.decls.size
Tactic:
rw [LawfulOperator.denote_mem_prefix (f := mkConstCached)]
State after:
no goals

State before:
case hcin
α : Type
inst✝² : BEq α
inst✝¹ : Hashable α
inst✝ : DecidableEq α
w : Nat
aig : AIG α
lhs rhs : BitVec w
assign : α → Bool
input : aig.BinaryRefStream w
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
⊢ ⟦{ aig := (aig.mkConstCached false).aig, ref := (aig.mkConstCached false).ref }, assign⟧ =
    BitVec.carry 0 lhs rhs false
Tactic:
simp
State after:
no goals

State before:
case a
α : Type
inst✝² : BEq α
inst✝¹ : Hashable α
inst✝ : DecidableEq α
w : Nat
aig : AIG α
lhs rhs : BitVec w
assign : α → Bool
input : aig.BinaryRefStream w
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
⊢ 0 ≤ idx
Tactic:
omega
State after:
no goals

State before:
α : Type
inst✝² : BEq α
inst✝¹ : Hashable α
inst✝ : DecidableEq α
w : Nat
aig : AIG α
lhs rhs : BitVec w
assign : α → Bool
input : aig.BinaryRefStream w
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
⊢ ∀ (idx : Nat) (hidx : idx < w),
    ⟦{ aig := (aig.mkConstCached false).aig, ref := (input.cast ⋯).lhs.getRef idx hidx }, assign⟧ = lhs.getLsb idx
Tactic:
intros
State after:
α : Type
inst✝² : BEq α
inst✝¹ : Hashable α
inst✝ : DecidableEq α
w : Nat
aig : AIG α
lhs rhs : BitVec w
assign : α → Bool
input : aig.BinaryRefStream w
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
idx✝ : Nat
hidx✝ : idx✝ < w
⊢ ⟦{ aig := (aig.mkConstCached false).aig, ref := (input.cast ⋯).lhs.getRef idx✝ hidx✝ }, assign⟧ = lhs.getLsb idx✝

State before:
α : Type
inst✝² : BEq α
inst✝¹ : Hashable α
inst✝ : DecidableEq α
w : Nat
aig : AIG α
lhs rhs : BitVec w
assign : α → Bool
input : aig.BinaryRefStream w
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
idx✝ : Nat
hidx✝ : idx✝ < w
⊢ ⟦{ aig := (aig.mkConstCached false).aig, ref := (input.cast ⋯).lhs.getRef idx✝ hidx✝ }, assign⟧ = lhs.getLsb idx✝
Tactic:
simp only [BinaryRefStream.lhs_getRef_cast, Ref_cast']
State after:
α : Type
inst✝² : BEq α
inst✝¹ : Hashable α
inst✝ : DecidableEq α
w : Nat
aig : AIG α
lhs rhs : BitVec w
assign : α → Bool
input : aig.BinaryRefStream w
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
idx✝ : Nat
hidx✝ : idx✝ < w
⊢ ⟦{ aig := (aig.mkConstCached false).aig, ref := { gate := (input.lhs.getRef idx✝ hidx✝).gate, hgate := ⋯ } },
      assign⟧ =
    lhs.getLsb idx✝

State before:
α : Type
inst✝² : BEq α
inst✝¹ : Hashable α
inst✝ : DecidableEq α
w : Nat
aig : AIG α
lhs rhs : BitVec w
assign : α → Bool
input : aig.BinaryRefStream w
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
idx✝ : Nat
hidx✝ : idx✝ < w
⊢ ⟦{ aig := (aig.mkConstCached false).aig, ref := { gate := (input.lhs.getRef idx✝ hidx✝).gate, hgate := ⋯ } },
      assign⟧ =
    lhs.getLsb idx✝
Tactic:
rw [LawfulOperator.denote_mem_prefix (f := mkConstCached)]
State after:
α : Type
inst✝² : BEq α
inst✝¹ : Hashable α
inst✝ : DecidableEq α
w : Nat
aig : AIG α
lhs rhs : BitVec w
assign : α → Bool
input : aig.BinaryRefStream w
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
idx✝ : Nat
hidx✝ : idx✝ < w
⊢ ⟦{ aig := aig, ref := { gate := (input.lhs.getRef idx✝ hidx✝).gate, hgate := ?m.42315 } }, assign⟧ = lhs.getLsb idx✝

α : Type
inst✝² : BEq α
inst✝¹ : Hashable α
inst✝ : DecidableEq α
w : Nat
aig : AIG α
lhs rhs : BitVec w
assign : α → Bool
input : aig.BinaryRefStream w
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
idx✝ : Nat
hidx✝ : idx✝ < w
⊢ (input.lhs.getRef idx✝ hidx✝).gate < aig.decls.size

State before:
α : Type
inst✝² : BEq α
inst✝¹ : Hashable α
inst✝ : DecidableEq α
w : Nat
aig : AIG α
lhs rhs : BitVec w
assign : α → Bool
input : aig.BinaryRefStream w
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
idx✝ : Nat
hidx✝ : idx✝ < w
⊢ ⟦{ aig := aig, ref := { gate := (input.lhs.getRef idx✝ hidx✝).gate, hgate := ?m.42315 } }, assign⟧ = lhs.getLsb idx✝

α : Type
inst✝² : BEq α
inst✝¹ : Hashable α
inst✝ : DecidableEq α
w : Nat
aig : AIG α
lhs rhs : BitVec w
assign : α → Bool
input : aig.BinaryRefStream w
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
idx✝ : Nat
hidx✝ : idx✝ < w
⊢ (input.lhs.getRef idx✝ hidx✝).gate < aig.decls.size
Tactic:
rw [hleft]
State after:
no goals

State before:
α : Type
inst✝² : BEq α
inst✝¹ : Hashable α
inst✝ : DecidableEq α
w : Nat
aig : AIG α
lhs rhs : BitVec w
assign : α → Bool
input : aig.BinaryRefStream w
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
⊢ ∀ (idx : Nat) (hidx : idx < w),
    ⟦{ aig := (aig.mkConstCached false).aig, ref := (input.cast ⋯).rhs.getRef idx hidx }, assign⟧ = rhs.getLsb idx
Tactic:
intros
State after:
α : Type
inst✝² : BEq α
inst✝¹ : Hashable α
inst✝ : DecidableEq α
w : Nat
aig : AIG α
lhs rhs : BitVec w
assign : α → Bool
input : aig.BinaryRefStream w
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
idx✝ : Nat
hidx✝ : idx✝ < w
⊢ ⟦{ aig := (aig.mkConstCached false).aig, ref := (input.cast ⋯).rhs.getRef idx✝ hidx✝ }, assign⟧ = rhs.getLsb idx✝

State before:
α : Type
inst✝² : BEq α
inst✝¹ : Hashable α
inst✝ : DecidableEq α
w : Nat
aig : AIG α
lhs rhs : BitVec w
assign : α → Bool
input : aig.BinaryRefStream w
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
idx✝ : Nat
hidx✝ : idx✝ < w
⊢ ⟦{ aig := (aig.mkConstCached false).aig, ref := (input.cast ⋯).rhs.getRef idx✝ hidx✝ }, assign⟧ = rhs.getLsb idx✝
Tactic:
simp only [BinaryRefStream.rhs_getRef_cast, Ref_cast']
State after:
α : Type
inst✝² : BEq α
inst✝¹ : Hashable α
inst✝ : DecidableEq α
w : Nat
aig : AIG α
lhs rhs : BitVec w
assign : α → Bool
input : aig.BinaryRefStream w
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
idx✝ : Nat
hidx✝ : idx✝ < w
⊢ ⟦{ aig := (aig.mkConstCached false).aig, ref := { gate := (input.rhs.getRef idx✝ hidx✝).gate, hgate := ⋯ } },
      assign⟧ =
    rhs.getLsb idx✝

State before:
α : Type
inst✝² : BEq α
inst✝¹ : Hashable α
inst✝ : DecidableEq α
w : Nat
aig : AIG α
lhs rhs : BitVec w
assign : α → Bool
input : aig.BinaryRefStream w
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
idx✝ : Nat
hidx✝ : idx✝ < w
⊢ ⟦{ aig := (aig.mkConstCached false).aig, ref := { gate := (input.rhs.getRef idx✝ hidx✝).gate, hgate := ⋯ } },
      assign⟧ =
    rhs.getLsb idx✝
Tactic:
rw [LawfulOperator.denote_mem_prefix (f := mkConstCached)]
State after:
α : Type
inst✝² : BEq α
inst✝¹ : Hashable α
inst✝ : DecidableEq α
w : Nat
aig : AIG α
lhs rhs : BitVec w
assign : α → Bool
input : aig.BinaryRefStream w
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
idx✝ : Nat
hidx✝ : idx✝ < w
⊢ ⟦{ aig := aig, ref := { gate := (input.rhs.getRef idx✝ hidx✝).gate, hgate := ?m.43169 } }, assign⟧ = rhs.getLsb idx✝

α : Type
inst✝² : BEq α
inst✝¹ : Hashable α
inst✝ : DecidableEq α
w : Nat
aig : AIG α
lhs rhs : BitVec w
assign : α → Bool
input : aig.BinaryRefStream w
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
idx✝ : Nat
hidx✝ : idx✝ < w
⊢ (input.rhs.getRef idx✝ hidx✝).gate < aig.decls.size

State before:
α : Type
inst✝² : BEq α
inst✝¹ : Hashable α
inst✝ : DecidableEq α
w : Nat
aig : AIG α
lhs rhs : BitVec w
assign : α → Bool
input : aig.BinaryRefStream w
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
idx✝ : Nat
hidx✝ : idx✝ < w
⊢ ⟦{ aig := aig, ref := { gate := (input.rhs.getRef idx✝ hidx✝).gate, hgate := ?m.43169 } }, assign⟧ = rhs.getLsb idx✝

α : Type
inst✝² : BEq α
inst✝¹ : Hashable α
inst✝ : DecidableEq α
w : Nat
aig : AIG α
lhs rhs : BitVec w
assign : α → Bool
input : aig.BinaryRefStream w
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
idx✝ : Nat
hidx✝ : idx✝ < w
⊢ (input.rhs.getRef idx✝ hidx✝).gate < aig.decls.size
Tactic:
rw [hright]
State after:
no goals

State before:
case i_lt
α : Type
inst✝² : BEq α
inst✝¹ : Hashable α
inst✝ : DecidableEq α
w : Nat
aig : AIG α
lhs rhs : BitVec w
assign : α → Bool
input : aig.BinaryRefStream w
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
⊢ idx < w
Tactic:
assumption
State after:
no goals