The count includes explicit $halt$ and exhausted $read$, but charges nothing for an out-of-range program counter. Input is the supplied raw list: there is no implicit header or marker. EOF testing and indexed read-only input access, with original length metadata, are available at unit cost, as specified in $Ram$. No initial input-loading scan is charged. The complete append-only output must equal the function value.

The number of instructions comes from the machine semantics, so a time bound is a statement about the program: nothing is annotated onto the program and then trusted. Only inputs in $D$ are constrained; a program is free to do anything at all on malformed input, which is what a statement about an algorithm on encoded objects should say.

The bound is stated elementarily — an explicit $T$ that the step count does not exceed — rather than through asymptotic notation. Asymptotics would require a filter on inputs and would obscure, rather than clarify, a statement that quantifies over encodings of every graph; a linear bound is spelled out at the point of use as $c * (x.length + 1)$ with an explicit constant, a fixed-parameter bound as $c * 2 ^ k * (x.length + 1)$ with the parameter dependence written in, the $+ 1$ making both meaningful for the empty input as well.

The word length $w$ is an explicit argument, and statements built on this notion quantify it visibly, in the order $∃ p, ∀ …, ∀ w, (word-length hypothesis) → ComputesInTime w p D f T$. The program is quantified before the word length: one program that works at every sufficiently large word length, so that $w$ cannot smuggle advice into the machine — a program chosen after $w$ could hide an arbitrary amount of information in its literals. This is the same uniformity discipline the quantifier order enforces for the parameter of a fixed-parameter bound.

Word-length hypotheses are written as explicit inequalities against $2 ^ w$ — $c * (x.length + 1) ≤ 2 ^ w$, or "every entry of $x$ is less than $2 ^ w$" — never through logarithms. This keeps the no-asymptotics style of the surrounding statements and says exactly what a proof needs: that the quantities the program manipulates fit into a word. Where honesty requires it, the same fitting conditions appear in the admissible set $D$ itself, alongside the well-formedness conditions of the encoding, since the machine reduces oversized input entries modulo $2 ^ w$ rather than rejecting them.

Only the timed notion is defined: every statement built on this machine carries a bound, and plain computability is the special case in which $T$ is unconstrained.