The program reads its input into an array, decides well-formedness in one pass over the literal slots, and then either runs the emitter of $EmitProg$ — whose five passes are reused here through the specification each of them carries — or writes the seven-entry word a malformed input is sent to.

Three of the four conditions are immediate. The fourth, that distinct occurrences of one variable carry distinct appearance indices, is decided by bucketing: an occurrence of variable $v$ with appearance index $k$ claims the cell $4v + k$, and a cell claimed twice refutes the condition. The cells fit because the pass runs only when the other three checks have passed, so $v < V ≤ 3C$ and $k < 4$.

Each phase is costed twice, once on each side of the check that guards it. A word whose header lies about its length is rejected by the first check, and the marking pass and the emitter are then both skipped; that is what keeps the cost linear in the length of the word rather than in the number the word claims is its clause count. The whole is $4688 · |x| + 162$ units of IMP+ cost, so $46880 · (|x| + 2)$ machine instructions.

What remains is a change of currency, which $RamBridge$ does once: the bit size bounds the number of entries, and every value the program forms is bounded by the length of the word plus its largest entry, hence by $2 ^ (bitSize x + 8)$.