One bounded sparse-entry scan iteration — proof internals

theorem Complexity.RAM.RegisterStore.Machine.entryScanStepTM_hoareTime_frame_internal {n : ℕ} (tapes : EntryMatchTapes n) (entry : Entry) (rest queryBits : List Bool) (initialWork iterationWork : Fin n → Tape) (inp₀ out₀ : Tape) (hready : EntryScanReady tapes (entry.encode ++ rest) queryBits initialWork iterationWork) (hinput : TM.Parked inp₀) (houtput : TM.Parked out₀) : (entryScanStepTM tapes).HoareTime (fun (inp : Tape) (work : Fin n → Tape) (out : Tape) => inp = inp₀ ∧ work = iterationWork ∧ out = out₀) (fun (inp : Tape) (work : Fin n → Tape) (out : Tape) => inp = inp₀ ∧ (entry.1.bits = queryBits ∧ EntryScanHit tapes entry rest queryBits initialWork work ∨ entry.1.bits ≠ queryBits ∧ EntryScanReady tapes rest queryBits initialWork work) ∧ out = out₀) (entryScanStepTime tapes entry queryBits iterationWork)