Theorem: AIG.ofBoolExprCached.go_denote_entry (LeanSAT/AIG/BoolExprCached.lean)

State before:
α β : Type
inst✝³ : BEq β
inst✝² : Hashable β
inst✝¹ : DecidableEq β
atomHandler : AIG β → α → Entrypoint β
inst✝ : LawfulOperator β (fun x => α) atomHandler
expr : BoolExpr α
assign : β → Bool
entry : Entrypoint β
h : entry.ref.gate < (go expr entry.aig atomHandler).val.aig.decls.size
⊢ ⟦{ aig := (go expr entry.aig atomHandler).val.aig, ref := { gate := entry.ref.gate, hgate := h } }, assign⟧ =
    ⟦entry, assign⟧
Tactic:
apply denote.eq_of_aig_eq
State after:
case hprefix
α β : Type
inst✝³ : BEq β
inst✝² : Hashable β
inst✝¹ : DecidableEq β
atomHandler : AIG β → α → Entrypoint β
inst✝ : LawfulOperator β (fun x => α) atomHandler
expr : BoolExpr α
assign : β → Bool
entry : Entrypoint β
h : entry.ref.gate < (go expr entry.aig atomHandler).val.aig.decls.size
⊢ IsPrefix entry.aig.decls (go expr entry.aig atomHandler).val.aig.decls

State before:
case hprefix
α β : Type
inst✝³ : BEq β
inst✝² : Hashable β
inst✝¹ : DecidableEq β
atomHandler : AIG β → α → Entrypoint β
inst✝ : LawfulOperator β (fun x => α) atomHandler
expr : BoolExpr α
assign : β → Bool
entry : Entrypoint β
h : entry.ref.gate < (go expr entry.aig atomHandler).val.aig.decls.size
⊢ IsPrefix entry.aig.decls (go expr entry.aig atomHandler).val.aig.decls
Tactic:
apply ofBoolExprCached.go_IsPrefix_aig
State after:
no goals