The witness is the compiled driver $ccProgram$. Its IMP+ source $ccCom$ reads the encoding into four arrays, sweeps the vertices in increasing order starting a breadth-first search at every unlabelled one, and writes the label array out; $ccCom_run$ is that run, end to end, with output $ccLabels G$ and cost at most $84 * (|x| + 1)$. The cost is a single amortized argument — one potential $c₁·(2m − scanned) + c₀·(n − tail) + c₀·(tail − head) + c₂·(n − u)$ for the whole sweep, so the searches are never counted separately — and the linearity in $|x|$ comes from the encoding's $length_eq$, which makes $n$ and $2m$ both at most the length of the word.

$computesInTime_of_solves$ discharges the compiler, the layout invariant and the machine in one step, charging $layout.const = 10$ machine steps per unit of IMP+ cost, plus one for the final $halt$. The array extents are chosen per input, as that lemma allows: $ccExt n m$ declares $off ↦ n+1$, $tgt ↦ 2m$, $lab ↦ n$, $q ↦ n$, which is what the reads fill.

The machine truncates every value modulo $2 ^ w$, so the run on the machine is the run in the unbounded semantics only as long as nothing the program computes reaches $2 ^ w$. The bound the driver is proved under is the length of the input word itself: every entry of an encoding is smaller than the encoding is long ($mem_lt_length$), and every quantity the algorithm keeps of its own — vertex numbers, offsets, the queue pointers, the counter of scanned slots — is bounded by $n$ or by $2m$, hence again by the length. So the whole run needs the single hypothesis $|x| ≤ B$, and the compiled program needs in addition that the cells the layout addresses are words, which is $19 + 4|x| ≤ 2 ^ w$. The statement's hypothesis, $841(|x| + 1) ≤ 2 ^ w$, gives both with room to spare; it is stated in that form because a bound on the running time is the condition a reader of an algorithm expects, and because it is the one inequality the machine model actually needs to be told.

Two details of the program are shaped by the cost proof rather than by the algorithm, and a reader is entitled to ask whether either of them smuggles work out of the bound. Neither does.

The queue is global. It is never reset between searches: a search leaves its head and tail pointers equal, and the next search continues from there. So the tail only ever increases, and since a vertex is put on the queue only in the step that labels it, the tail never passes the number of vertices. "Queue capacity not yet used" is therefore a budget for the whole run out of which every enqueue is paid, instead of a budget per search that would force the searches to be counted one at a time. Resetting the queue is what would cost something; not resetting it is free.

A scalar counts the adjacency slots already scanned. The potential has to be a function of the program's own scalars, and "how much of the target array has been looked at" is not otherwise one of them, since the scan pointer restarts inside each vertex's block. The counter is incremented once per slot and read nowhere, so it costs one addition per slot — a constant factor on work already being done — and deleting it would leave the computed labels unchanged.

Nothing else is precomputed. The input word is read once into the four arrays in the order the tape presents it, so the reading phase is a plain copy and the encoding stays the dumb one the concept fixes.

The first theorem of the submission; the algorithm is the textbook sweep of breadth-first searches.