Theorem: AIG.LawfulStreamOperator.denote_input_stream (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 idx : Nat
hidx : idx < len
assign : α → Bool
s : RefStreamEntry α len
input : β s.aig len
hcast : s.aig.decls.size ≤ (f s.aig input).aig.decls.size
⊢ ⟦{ aig := (f s.aig input).aig, ref := (s.stream.getRef idx hidx).cast hcast }, assign⟧ =
    ⟦{ aig := s.aig, ref := s.stream.getRef idx hidx }, assign⟧
Tactic:
rw [denote_mem_prefix]
State after:
α : 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 idx : Nat
hidx : idx < len
assign : α → Bool
s : RefStreamEntry α len
input : β s.aig len
hcast : s.aig.decls.size ≤ (f s.aig input).aig.decls.size
⊢ ⟦{ aig := s.aig, ref := { gate := ((s.stream.getRef idx hidx).cast hcast).gate, hgate := ?m.4622 } }, assign⟧ =
    ⟦{ aig := s.aig, ref := s.stream.getRef idx hidx }, assign⟧

α : 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 idx : Nat
hidx : idx < len
assign : α → Bool
s : RefStreamEntry α len
input : β s.aig len
hcast : s.aig.decls.size ≤ (f s.aig input).aig.decls.size
⊢ ((s.stream.getRef idx hidx).cast hcast).gate < s.aig.decls.size

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 idx : Nat
hidx : idx < len
assign : α → Bool
s : RefStreamEntry α len
input : β s.aig len
hcast : s.aig.decls.size ≤ (f s.aig input).aig.decls.size
⊢ ⟦{ aig := s.aig, ref := { gate := ((s.stream.getRef idx hidx).cast hcast).gate, hgate := ?m.4622 } }, assign⟧ =
    ⟦{ aig := s.aig, ref := s.stream.getRef idx hidx }, assign⟧

α : 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 idx : Nat
hidx : idx < len
assign : α → Bool
s : RefStreamEntry α len
input : β s.aig len
hcast : s.aig.decls.size ≤ (f s.aig input).aig.decls.size
⊢ ((s.stream.getRef idx hidx).cast hcast).gate < s.aig.decls.size
Tactic:
rfl
State after:
no goals