Dense overlay lookup -- proof internals

theorem Complexity.RAM.RegisterStore.Machine.denseOverlayLookupTM_hoareTime_internal {n : ℕ} (tapes : EntryLookupRestoreTapes n) (input : List Bool) (overlay : Store) (address : ℕ) (initialWork : Fin n → Tape) (out₀ : Tape) (hvalid : DenseOverlay.Valid overlay) (hready : EntryLookupRestoreReady tapes overlay address initialWork) (houtput : TM.Parked out₀) : (denseOverlayLookupTM tapes).HoareTime (fun (inp : Tape) (work : Fin n → Tape) (out : Tape) => inp = (Tape.init (List.map Γ.ofBool input)).move Dir3.right ∧ work = initialWork ∧ out = out₀) (fun (inp : Tape) (work : Fin n → Tape) (out : Tape) => inp = (Tape.init (List.map Γ.ofBool input)).move Dir3.right ∧ DenseOverlayLookupResult tapes input overlay address initialWork work ∧ out = out₀) (denseOverlayLookupTime tapes input.length overlay address)

theorem Complexity.RAM.RegisterStore.Machine.denseOverlayLookupStaticTM_hoareTime_internal {n : ℕ} (tapes : EntryLookupRestoreTapes n) (input : List Bool) (overlay : Store) (address : ℕ) (initialWork : Fin n → Tape) (out₀ : Tape) (hvalid : DenseOverlay.Valid overlay) (hready : EntryLookupStaticReady tapes overlay initialWork) (houtput : TM.Parked out₀) : (denseOverlayLookupStaticTM tapes address).HoareTime (fun (inp : Tape) (work : Fin n → Tape) (out : Tape) => inp = (Tape.init (List.map Γ.ofBool input)).move Dir3.right ∧ work = initialWork ∧ out = out₀) (fun (inp : Tape) (work : Fin n → Tape) (out : Tape) => inp = (Tape.init (List.map Γ.ofBool input)).move Dir3.right ∧ DenseOverlayLookupStaticResult tapes input overlay address initialWork work ∧ out = out₀) (denseOverlayLookupStaticTime tapes input.length overlay address)