For a deterministic automaton, the next state is determined uniquely by the current state and the current input. Hence, the transition relation can be written as a conjunction of equivalences of the form next(s) <-> phi(s,i) where the next state is determined by the current state s and the current input i. That also holds for a boolean encoding. The automaton above has two states. Let's encode it with a single boolean state variable q that is initially false. The transition relation will then be
next(q) <-> q | !a
Note that either we are already in the state where q holds (and then q does also hold next), or we need input !a to switch to that state.
