the form $\pi_1,r,\pi_2$ where $\pi_1$ and $\pi_2$ are in linear form. Then, we successively shorten $\pi_1$ and $\pi_2$ by eliminating simple cycles along them, and instead pumping the non-negative cycle $\gamma_r$. Some careful accounting is needed so that the length of the path is maintained, and so that it remains executable.

We now characterize the regular language $\LangVia{\initialstate,c_0}{r}$ using a DFA of bounded size.

[lemma]{}[unaryPumpDFA]{} \[lem:pump state DFA\] There exists a bound $\bound{2}\in\poly(\norm{\transitions}\cdot\card{\states})$ such that, for every $r\in \Pump$, there exists a DFA that accepts $\LangVia{\initialstate,c_0}{r}$ and is of size at most $\bound{2}$.

Define $\PS\eqdef\bigcup_{r\in \Pump} \LangVia{\initialstate,c_0}{r}$. Notice that $\PS\subseteq \Lang{\initialstate,c_0}$ and that $\Lang{\initialstate,c_0}\setminus \PS$ must be finite. Indeed, if $w\in \Lang{\initialstate,c_0}\setminus \PS$ then it can only be accepted by runs with *only* negative cycles, of which there are finitely many. In particular, if $\N\setminus \PS$ is infinite, then $\Lang{\initialstate,c_0}\neq \N$.

Using the bounds from \[lem:pump state DFA\], we have the following.

[lemma]{}[unaryWitnessBound]{} \[lem:singleton alphabet witness bound\] There exists $\bound{3}\in\poly(\norm{\transitions},\card{\states})$ such that $\Lang{\initialstate,c_0}\neq \N$ if, and only if, there exists $n\in \N$ such that either $n<\bound{2}$ and $n\notin \Lang{\initialstate,c_0}$, or $\bound{3}^{|\states|}\le n\le 2\bound{3}^{|\states|}$ and $n\notin \PS$.

suggests the following algorithmic scheme for deciding non-universality: non-deterministically either (1) guess $n<\bound{3}$, and 