A nondeterministic Turing machine, together with its input, is presented as a finite structure: the universe holds the positions, the transitions, the states and the symbols, and relations record the order on positions, the attributes of each transition (the state it applies in, the symbol it reads, the state it moves to, the symbol it writes, the direction of the move), the start and accepting states, the blank symbol, and the input written on the tape.

Positions serve both as tape cells and as time steps, so the time bound is the number of positions, by construction and with no arithmetic. A configuration is a state, a head position and a tape; a step applies a transition at the head, and the machine accepts when some run from an initial configuration reaches an accepting state in fewer steps than there are positions. Well-formedness – the order is linear, there is a position, the input is functional and the blank symbol is unique – is folded into the yes-instances, since a relation symbol is not a linear order by itself.

Machine acceptance, the decision problem so defined, is the machine side of the Cook–Levin theorem. That it is isomorphism-invariant, which makes it a decision problem, is the one claim of this module: the proof transports runs along the isomorphism and belongs to the proofs of this submission, so the bundled problem takes the invariance proof as a parameter. By proof irrelevance the problem does not depend on which proof is supplied, and every statement about it is made for an arbitrary one.