Bounded encoded sparse-store update -- unmatched entry iteration

theorem Complexity.RAM.RegisterStore.Machine.entryUpdateIteration_miss_internal {n : ℕ} (tapes : EntryUpdateTapes n) (store : Store) (address newValue : ℕ) (processed emitted : Store) (entry : Entry) (rest : Store) (found : Bool) (resultCount : ℕ) (initialWork work : Fin n → Tape) (outPrefix : List Bool) (inp out : Tape) (hinv : EntryUpdateLoopInv tapes store address newValue processed (entry :: rest) emitted found resultCount initialWork work) (hne : entry.1 ≠ address) (hinput : TM.Parked inp) (houtput : out.HasBinaryPrefix (outPrefix ++ List.flatMap Entry.encode emitted)) : ∃ (nextWork : Fin n → Tape) (nextOut : Tape), ∃ time ≤ entryUpdateIterationTime tapes entry rest address newValue (List.length store), (entryUpdateTM tapes).reachesIn time (entryUpdateTestCfg tapes inp work out) (entryUpdateTestCfg tapes inp nextWork nextOut) ∧ EntryUpdateLoopInv tapes store address newValue (processed ++ [entry]) rest (emitted ++ [entry]) found resultCount initialWork nextWork ∧ nextOut.HasBinaryPrefix (outPrefix ++ List.flatMap Entry.encode (emitted ++ [entry]))

One unmatched old entry is copied to the output, its remaining-count unit is consumed, and the update controller returns to its loop-test state.