Execution is $Lax808846.Ram.RunsTo$ on the registered word RAM. The supplied input is exactly $encodeInput$, with no implicit length prefix. The constants and program precede the input and word width in the quantifiers. The natural-number time bound uses $\lceil1/\varepsilon\rceil$ and $1+\lfloor\log_2(n+2)\rfloor$ to cover small inputs.

The same bound is a sufficient word width, and the program must work at every larger width. In particular it works at that explicitly prescribed width; there is no advice hidden in a choice of width. Allowing this many bits accommodates exact rational subroutines. Simulating these bounded-word operations with bit operations costs a polynomial in the time bound, which remains of the displayed form after increasing its constants and exponent: $(A+B)^k\le2^{k-1}(A^k+B^k)$. Thus the additive polynomial dependence on $\ell$ is preserved. Correctness and time are promised only on well-formed inputs whose graphs belong to $\mathcal C$.