Dense-overlay immediate instruction

theorem Complexity.RAM.RegisterStore.Machine.denseImmediateInstructionTM_hoareTime_frame {n : ℕ} (tapes : BinaryInstructionTapes n) (overlay : Store) (destination value : ℕ) (emittedBits : List Bool) (initialWork : Fin n → Tape) (inp₀ out₀ : Tape) (hcanonical : Canonical overlay) (hinitial : EntryLookupStaticReady tapes.lhsLookup overlay initialWork) (hreplacement : (initialWork tapes.update.replacement).HasBinaryNat 0) (hinput : TM.Parked inp₀) (houtput : out₀.HasBinaryPrefix emittedBits) : (denseImmediateInstructionTM tapes destination value).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₀ ∧ DenseImmediateInstructionResult tapes overlay destination value initialWork work ∧ out.HasBinaryPrefix (emittedBits ++ List.flatMap Entry.encode (DenseOverlay.write overlay destination value))) (denseImmediateInstructionTime tapes overlay destination value)

Exact semantic and time contract for one immediate dense-overlay write.