Tovey's theorem hands over a polynomial-time Turing reduction from any NP language to exact $(3,4)$-SAT on bit-encoded formulas. The reduction to scheduling is its composite with five machines: the bits become a word of zeros and ones; a word RAM program parses that word — a one-pass scan of the rigid encoding, then a quadratic pass that renames each variable to the position of its first occurrence and numbers its occurrences — into Construction 2's formula word; Construction 2's own program turns the formula word into an instance word; a second program prints the instance word in the binary instance encoding, as a word of zeros and ones; and the last machine turns that word back into bits. The two RAM programs are polynomial-time Turing computations by the archive's equivalence, and the composite is polynomial by the composition theorem, taken here with the middle alphabet general.

The image lies on the slice because Construction 2's instances do, and the composite preserves and reflects yes-instances because the parser is correct against Tovey's language, Construction 2 is correct, and the printer writes exactly the encoding of the instance its word encodes.