The program reads the two header entries, copies the clause block into an array, and writes the six blocks of the encoding in order. The copy costs $12$ per entry; the three passes that decode a clause job cost $104$, $104$ and $124$ per job, the weights $10$, the offsets $24$; and the compiler charges ten machine instructions per unit of IMP+ cost. With $V ≤ 3C$ the number of jobs is at most $12C$ and the word's length is $2 + 9C$, so the whole is linear in the length of the input, and $5881 · (|x| + 1)$ covers it.

The bound on the values is the length of the word plus its largest entry: every number the program forms is an entry it read, a count of them, or a machine index, and the machine indices are bounded by $2V + 3C$.