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

State before:
α : Type
inst✝² : BEq α
inst✝¹ : Hashable α
inst✝ : DecidableEq α
assign : α → Bool
aig : AIG α
input : FullAdderInput aig
⊢ ⟦mkFullAdderOut aig input, assign⟧ =
    xor (xor ⟦{ aig := aig, ref := input.lhs }, assign⟧ ⟦{ aig := aig, ref := input.rhs }, assign⟧)
      ⟦{ aig := aig, ref := input.cin }, assign⟧
Tactic:
simp only [mkFullAdderOut, Ref_cast', denote_mkXorCached, denote_projected_entry, Bool.bne_assoc,
  Bool.bne_left_inj]
State after:
α : Type
inst✝² : BEq α
inst✝¹ : Hashable α
inst✝ : DecidableEq α
assign : α → Bool
aig : AIG α
input : FullAdderInput aig
⊢ ⟦{ aig := (aig.mkXorCached { lhs := input.lhs, rhs := input.rhs }).aig,
        ref := { gate := input.cin.gate, hgate := ⋯ } },
      assign⟧ =
    ⟦{ aig := aig, ref := input.cin }, assign⟧

State before:
α : Type
inst✝² : BEq α
inst✝¹ : Hashable α
inst✝ : DecidableEq α
assign : α → Bool
aig : AIG α
input : FullAdderInput aig
⊢ ⟦{ aig := (aig.mkXorCached { lhs := input.lhs, rhs := input.rhs }).aig,
        ref := { gate := input.cin.gate, hgate := ⋯ } },
      assign⟧ =
    ⟦{ aig := aig, ref := input.cin }, assign⟧
Tactic:
rw [LawfulOperator.denote_mem_prefix (f := mkXorCached)]
State after:
no goals