Bounded encoded sparse-store update -- matching iterations

This file composes the checked match, deletion or replacement, and counter subroutines for the two branches in which the current old entry has the requested address.

theorem Complexity.RAM.RegisterStore.Machine.entryUpdateDeleteIteration_internal {n : ℕ} (tapes : EntryUpdateTapes n) (store : Store) (address : ℕ) (processed emitted : Store) (entry : Entry) (rest : Store) (resultCount : ℕ) (initialWork work : Fin n → Tape) (outPrefix : List Bool) (inp out : Tape) (hinv : EntryUpdateLoopInv tapes store address 0 processed (entry :: rest) emitted false resultCount initialWork work) (haddress : address = entry.1) (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 0 (List.length store), (entryUpdateTM tapes).reachesIn time (entryUpdateTestCfg tapes inp work out) (entryUpdateTestCfg tapes inp nextWork nextOut) ∧ EntryUpdateLoopInv tapes store address 0 (processed ++ [entry]) rest emitted true (resultCount - 1) initialWork nextWork ∧ nextOut.HasBinaryPrefix (outPrefix ++ List.flatMap Entry.encode emitted)

A matching zero write deletes the current entry, decrements both runtime counters, and returns to the loop test with no output contribution.

theorem Complexity.RAM.RegisterStore.Machine.entryUpdateReplaceIteration_internal {n : ℕ} (tapes : EntryUpdateTapes n) (store : Store) (address newValue : ℕ) (processed emitted : Store) (entry : Entry) (rest : Store) (resultCount : ℕ) (initialWork work : Fin n → Tape) (outPrefix : List Bool) (inp out : Tape) (hinv : EntryUpdateLoopInv tapes store address newValue processed (entry :: rest) emitted false resultCount initialWork work) (haddress : address = entry.1) (hvalue : newValue ≠ 0) (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 ++ [(address, newValue)]) true resultCount initialWork nextWork ∧ nextOut.HasBinaryPrefix (outPrefix ++ List.flatMap Entry.encode (emitted ++ [(address, newValue)]))

A matching nonzero write emits the replacement entry, records the hit, decrements the remaining-entry counter, and returns to the loop test.