Sparse-entry final append — proof internals

theorem Complexity.RAM.RegisterStore.Machine.entryAppendRestoreTM_hoareTime_frame_internal {n : ℕ} (tapes : EntryReplaceTapes n) (address newValue : ℕ) (emitted : List Bool) (initialWork readyWork : Fin n → Tape) (inp₀ out₀ : Tape) (hready : EntryScanReady tapes.entry [] address.bits initialWork readyWork) (hreplacement : (readyWork tapes.replacement).HasBinaryNat newValue) (hinput : TM.Parked inp₀) (houtput : out₀.HasBinaryPrefix emitted) : (entryAppendRestoreTM tapes).HoareTime (fun (inp : Tape) (work : Fin n → Tape) (out : Tape) => inp = inp₀ ∧ work = readyWork ∧ out = out₀) (fun (inp : Tape) (work : Fin n → Tape) (out : Tape) => inp = inp₀ ∧ work = readyWork ∧ out.HasBinaryPrefix (emitted ++ Entry.encode (address, newValue))) (entryAppendRestoreTime address newValue)