conv =>
  lhs
  rhs
  lhs
  rw [LawfulOperator.denote_mem_prefix (f := mkXorCached) (h := input.lhs.hgate)]
α : Type
inst✝² : BEq α
inst✝¹ : Hashable α
inst✝ : DecidableEq α
assign : α → Bool
aig : AIG α
input : FullAdderInput aig
⊢ (xor ⟦{ aig := aig, ref := input.lhs }, assign⟧ ⟦{ aig := aig, ref := input.rhs }, assign⟧ &&
        ⟦{ aig := aig, ref := { gate := input.cin.gate, hgate := ⋯ } }, assign⟧ ||
      ⟦{ aig := (aig.mkXorCached { lhs := input.lhs, rhs := input.rhs }).aig,
            ref := { gate := input.lhs.gate, hgate := ⋯ } },
          assign⟧ &&
        ⟦{
            aig :=
              ((aig.mkXorCached { lhs := input.lhs, rhs := input.rhs }).aig.mkAndCached
                  { lhs := (aig.mkXorCached { lhs := input.lhs, rhs := input.rhs }).ref,
                    rhs := { gate := input.cin.gate, hgate := ⋯ } }).aig,
            ref := { gate := input.rhs.gate, hgate := ⋯ } },
          assign⟧) =
    (xor ⟦{ aig := aig, ref := input.lhs }, assign⟧ ⟦{ aig := aig, ref := input.rhs }, assign⟧ &&
        ⟦{ aig := aig, ref := input.cin }, assign⟧ ||
      ⟦{ aig := aig, ref := input.lhs }, assign⟧ && ⟦{ aig := aig, ref := input.rhs }, assign⟧)
α : Type
inst✝² : BEq α
inst✝¹ : Hashable α
inst✝ : DecidableEq α
assign : α → Bool
aig : AIG α
input : FullAdderInput aig
⊢ (xor ⟦{ aig := aig, ref := input.lhs }, assign⟧ ⟦{ aig := aig, ref := input.rhs }, assign⟧ &&
        ⟦{ aig := aig, ref := { gate := input.cin.gate, hgate := ⋯ } }, assign⟧ ||
      ⟦{ aig := aig, ref := { gate := input.lhs.gate, hgate := ⋯ } }, assign⟧ &&
        ⟦{
            aig :=
              ((aig.mkXorCached { lhs := input.lhs, rhs := input.rhs }).aig.mkAndCached
                  { lhs := (aig.mkXorCached { lhs := input.lhs, rhs := input.rhs }).ref,
                    rhs := { gate := input.cin.gate, hgate := ⋯ } }).aig,
            ref := { gate := input.rhs.gate, hgate := ⋯ } },
          assign⟧) =
    (xor ⟦{ aig := aig, ref := input.lhs }, assign⟧ ⟦{ aig := aig, ref := input.rhs }, assign⟧ &&
        ⟦{ aig := aig, ref := input.cin }, assign⟧ ||
      ⟦{ aig := aig, ref := input.lhs }, assign⟧ && ⟦{ aig := aig, ref := input.rhs }, assign⟧)