Theorem: AIG.LawfulStreamOperator.denote_input_entry (LeanSAT/AIG/LawfulStreamOperator.lean)

State before:
α : Type
inst✝³ : BEq α
inst✝² : Hashable α
inst✝¹ : DecidableEq α
β : AIG α → Nat → Type
f : {len : Nat} → (aig : AIG α) → β aig len → RefStreamEntry α len
inst✝ : LawfulStreamOperator α β fun {len} => f
len : Nat
assign : α → Bool
entry : Entrypoint α
input : β entry.aig len
h : entry.ref.gate < (f entry.aig input).aig.decls.size
⊢ ⟦{ aig := (f entry.aig input).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 α
β : AIG α → Nat → Type
f : {len : Nat} → (aig : AIG α) → β aig len → RefStreamEntry α len
inst✝ : LawfulStreamOperator α β fun {len} => f
len : Nat
assign : α → Bool
entry : Entrypoint α
input : β entry.aig len
h : entry.ref.gate < (f entry.aig input).aig.decls.size
⊢ IsPrefix entry.aig.decls (f entry.aig input).aig.decls

State before:
case hprefix
α : Type
inst✝³ : BEq α
inst✝² : Hashable α
inst✝¹ : DecidableEq α
β : AIG α → Nat → Type
f : {len : Nat} → (aig : AIG α) → β aig len → RefStreamEntry α len
inst✝ : LawfulStreamOperator α β fun {len} => f
len : Nat
assign : α → Bool
entry : Entrypoint α
input : β entry.aig len
h : entry.ref.gate < (f entry.aig input).aig.decls.size
⊢ IsPrefix entry.aig.decls (f entry.aig input).aig.decls
Tactic:
apply IsPrefix_aig
State after:
no goals