Fixed-address sparse-register lookup -- proof internals

theorem Complexity.RAM.RegisterStore.Machine.staticAdd_ready_internal {n : ℕ} (tapes : EntryLookupRestoreTapes n) (store : Store) (address : ℕ) (initialWork : Fin n → Tape) (hready : EntryLookupStaticReady tapes store initialWork) : EntryLookupRestoreReady tapes store address (Function.update initialWork tapes.querySource ((Tape.init (List.map Γ.ofBool address.bits)).move Dir3.right))

theorem Complexity.RAM.RegisterStore.Machine.entryLookupStatic_hoareTime_internal {n : ℕ} (tapes : EntryLookupRestoreTapes n) (store : Store) (address : ℕ) (initialWork : Fin n → Tape) (inp₀ out₀ : Tape) (hready : EntryLookupStaticReady tapes store initialWork) (hinput : TM.Parked inp₀) (houtput : TM.Parked out₀) : (entryLookupStaticTM tapes address).HoareTime (fun (inp : Tape) (work : Fin n → Tape) (out : Tape) => inp = inp₀ ∧ work = initialWork ∧ out = out₀) (fun (inp : Tape) (work : Fin n → Tape) (out : Tape) => inp = inp₀ ∧ EntryLookupStaticResult tapes store address initialWork work ∧ out = out₀) (entryLookupStaticTime tapes store address)