Theorem: AIG.denote_mkXorCached (LeanSAT/AIG/CachedGatesLemmas.lean)

State before:
α : Type
inst✝² : BEq α
inst✝¹ : Hashable α
inst✝ : DecidableEq α
assign : α → Bool
aig : AIG α
input : aig.BinaryInput
⊢ ⟦aig.mkXorCached input, assign⟧ =
    xor ⟦{ aig := aig, ref := input.lhs }, assign⟧ ⟦{ aig := aig, ref := input.rhs }, assign⟧
Tactic:
rw [← xor_as_aig]
State after:
α : Type
inst✝² : BEq α
inst✝¹ : Hashable α
inst✝ : DecidableEq α
assign : α → Bool
aig : AIG α
input : aig.BinaryInput
⊢ ⟦aig.mkXorCached input, assign⟧ =
    (!(⟦{ aig := aig, ref := input.lhs }, assign⟧ && ⟦{ aig := aig, ref := input.rhs }, assign⟧) &&
      !(!⟦{ aig := aig, ref := input.lhs }, assign⟧ && !⟦{ aig := aig, ref := input.rhs }, assign⟧))

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