unfold blastAdd
α : 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))
α : 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))