rw [LawfulOperator.denote_mem_prefix (f := mkConstCached)]
α : 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
no goals