Theorem: AIG.denote.eq_of_aig_eq (LeanSAT/AIG/LawfulOperator.lean)

State before:
α : Type
inst✝² : BEq α
inst✝¹ : Hashable α
inst✝ : DecidableEq α
assign : α → Bool
entry : Entrypoint α
newAIG : AIG α
hprefix : IsPrefix entry.aig.decls newAIG.decls
⊢ entry.ref.gate < newAIG.decls.size
Tactic:
have := entry.ref.hgate
State after:
α : Type
inst✝² : BEq α
inst✝¹ : Hashable α
inst✝ : DecidableEq α
assign : α → Bool
entry : Entrypoint α
newAIG : AIG α
hprefix : IsPrefix entry.aig.decls newAIG.decls
this : entry.ref.gate < entry.aig.decls.size
⊢ entry.ref.gate < newAIG.decls.size

State before:
α : Type
inst✝² : BEq α
inst✝¹ : Hashable α
inst✝ : DecidableEq α
assign : α → Bool
entry : Entrypoint α
newAIG : AIG α
hprefix : IsPrefix entry.aig.decls newAIG.decls
this : entry.ref.gate < entry.aig.decls.size
⊢ entry.ref.gate < newAIG.decls.size
Tactic:
have := hprefix.size_le
State after:
α : Type
inst✝² : BEq α
inst✝¹ : Hashable α
inst✝ : DecidableEq α
assign : α → Bool
entry : Entrypoint α
newAIG : AIG α
hprefix : IsPrefix entry.aig.decls newAIG.decls
this✝ : entry.ref.gate < entry.aig.decls.size
this : entry.aig.decls.size ≤ newAIG.decls.size
⊢ entry.ref.gate < newAIG.decls.size

State before:
α : Type
inst✝² : BEq α
inst✝¹ : Hashable α
inst✝ : DecidableEq α
assign : α → Bool
entry : Entrypoint α
newAIG : AIG α
hprefix : IsPrefix entry.aig.decls newAIG.decls
this✝ : entry.ref.gate < entry.aig.decls.size
this : entry.aig.decls.size ≤ newAIG.decls.size
⊢ entry.ref.gate < newAIG.decls.size
Tactic:
omega
State after:
no goals

State before:
α : Type
inst✝² : BEq α
inst✝¹ : Hashable α
inst✝ : DecidableEq α
assign : α → Bool
entry : Entrypoint α
newAIG : AIG α
hprefix : IsPrefix entry.aig.decls newAIG.decls
⊢ ⟦{ aig := newAIG, ref := { gate := entry.ref.gate, hgate := ⋯ } }, assign⟧ = ⟦entry, assign⟧
Tactic:
unfold denote
State after:
α : Type
inst✝² : BEq α
inst✝¹ : Hashable α
inst✝ : DecidableEq α
assign : α → Bool
entry : Entrypoint α
newAIG : AIG α
hprefix : IsPrefix entry.aig.decls newAIG.decls
⊢ go { aig := newAIG, ref := { gate := entry.ref.gate, hgate := ⋯ } }.ref.gate
      { aig := newAIG, ref := { gate := entry.ref.gate, hgate := ⋯ } }.aig.decls assign ⋯ ⋯ =
    go entry.ref.gate entry.aig.decls assign ⋯ ⋯

State before:
α : Type
inst✝² : BEq α
inst✝¹ : Hashable α
inst✝ : DecidableEq α
assign : α → Bool
entry : Entrypoint α
newAIG : AIG α
hprefix : IsPrefix entry.aig.decls newAIG.decls
⊢ go { aig := newAIG, ref := { gate := entry.ref.gate, hgate := ⋯ } }.ref.gate
      { aig := newAIG, ref := { gate := entry.ref.gate, hgate := ⋯ } }.aig.decls assign ⋯ ⋯ =
    go entry.ref.gate entry.aig.decls assign ⋯ ⋯
Tactic:
apply denote.go_eq_of_aig_eq
State after:
case hprefix
α : Type
inst✝² : BEq α
inst✝¹ : Hashable α
inst✝ : DecidableEq α
assign : α → Bool
entry : Entrypoint α
newAIG : AIG α
hprefix : IsPrefix entry.aig.decls newAIG.decls
⊢ IsPrefix entry.aig.decls { aig := newAIG, ref := { gate := entry.ref.gate, hgate := ⋯ } }.aig.decls

State before:
case hprefix
α : Type
inst✝² : BEq α
inst✝¹ : Hashable α
inst✝ : DecidableEq α
assign : α → Bool
entry : Entrypoint α
newAIG : AIG α
hprefix : IsPrefix entry.aig.decls newAIG.decls
⊢ IsPrefix entry.aig.decls { aig := newAIG, ref := { gate := entry.ref.gate, hgate := ⋯ } }.aig.decls
Tactic:
assumption
State after:
no goals