| (1) | $Q \neq \emptyset$ is a D17: Finite set (of states) |
| (2) | $\Sigma \neq \emptyset$ is a D17: Finite set (the input alphabet) |
| (3) | $\delta : Q \times \Sigma \to Q$ (the word transition function) |
| (4) | $q_0 \in Q$ (the initial state) |
| (5) | $F \subseteq Q$ is a D2115: Nonempty set (of final or halting or accepting states) |