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

State before:
α : Type
inst✝² : BEq α
inst✝¹ : Hashable α
inst✝ : DecidableEq α
assign : α → Bool
aig : AIG α
gate : aig.Ref
⊢ ⟦aig.mkNotCached gate, assign⟧ = !⟦{ aig := aig, ref := { gate := gate.gate, hgate := ⋯ } }, assign⟧
Tactic:
rw [← not_as_aig]
State after:
α : Type
inst✝² : BEq α
inst✝¹ : Hashable α
inst✝ : DecidableEq α
assign : α → Bool
aig : AIG α
gate : aig.Ref
⊢ ⟦aig.mkNotCached gate, assign⟧ = (true && !⟦{ aig := aig, ref := { gate := gate.gate, hgate := ⋯ } }, assign⟧)

State before:
α : Type
inst✝² : BEq α
inst✝¹ : Hashable α
inst✝ : DecidableEq α
assign : α → Bool
aig : AIG α
gate : aig.Ref
⊢ ⟦aig.mkNotCached gate, assign⟧ = (true && !⟦{ aig := aig, ref := { gate := gate.gate, hgate := ⋯ } }, assign⟧)
Tactic:
simp [mkNotCached, LawfulOperator.denote_mem_prefix (f := mkConstCached) gate.hgate]
State after:
no goals