we notice that since $\bound{3}$ is polynomial in the description of the OCN, then the size of each DFA for $\LangVia{\initialstate,c_0}{r}$ constructed as per \[lem:pump state DFA\] is polynomial in the OCN. Since the proof in \[lem:pump state DFA\] is constructive, we can obtain an explicit representation of these DFAs. Finally, given a DFA (or indeed, and NFA) over a singleton alphabet and $n$ written in binary, we can check whether $n$ is accepted in time $O(\log n)$ by repeated squaring of the transition matrix for the DFA [@MS1973]. We conclude with the following.

\[thm:singleton alphabet unary coNP\] The universality problem for singleton-alphabet one-counter nets with transitions encoded in unary is in , and is thus -complete.

##### Binary Encoding. {#binary-encoding. .unnumbered}

When the transitions are encoded in binary, $\bound{3}$ is potentially exponential in the encoding of the OCN. Thus, naively adapting the methods taken in the unary case (with basic optimization) will lead to a $\PSPACE$ algorithm for universality (using Savitch’s Theorem). As we now show, by taking a different approach, we can obtain an upper bound of $\SigmaTwo$, placing the problem in the second level of the polynomial hierarchy.

In order to obtain this bound, we essentially show 