A machine has finitely many control states, a finite work alphabet with a blank symbol, a read-only binary input tape between distinct endmarkers, and one initially blank, semi-infinite work tape. Both heads start at position zero, which is the input's left endmarker and the work tape's leftmost cell. One transition reads the two scanned symbols, writes one work symbol, changes state, and moves each head by at most one cell. An outward move at a tape boundary leaves that head in place.

The finite transition table gives a finite set of possible actions for each state and pair of scanned symbols. A deterministic machine has at most one action in every such set. A configuration with no successor is terminal, and its control state supplies an accept/reject bit. Acceptance means that some computation branch reaches an accepting terminal configuration. A decider has a finite bound on the lengths of all branches for each input, and accepts exactly the strings in its language. This bound need not be computable or satisfy any specified time bound.

Only the work tape is charged as space. Bounding its head below $s$ at every reachable configuration bounds every visited cell to the prefix $0,\ldots,s-1$, including blank cells and cells later erased. The input head is confined to $|x|+2$ positions and cannot act as an unbounded free counter. The transition table sees neither head position nor the input length; it sees only the control state and scanned symbols.