special significance in analyzing universality.

\[def:pump states\] Let $\Pump\subseteq\states$ be the set of states that admit good cycles. For each such state $r$ fix a shortest good cycle $\gamma_r$.

Intuitively, a state $r$ is in if it has a cycle that can be taken with any counter value, any number of times. That is, it can be used to “pump” the length of the word. Another important property is that if a path never visits a state in then *all* its simple cycles must be negative. Indeed, any non-negative cycle must contain a non-negative simple cycle and any state at a nadir of such cycle must be in .

If however, a state in occurs along an accepting run, we can accept the same word using a run in a short linear form, as we now show.

[lemma]{}[unaryLPFpump]{} \[lem:linear form with pump state\] There exists a bound $\bound{1}\in\poly(|\states|,\norm{\transitions})$ such that, for every $n\in\N$, if $n$ is accepted by a run that visits a state $r\in \Pump$, then $n$ has an accepting run of the form $\eta_1\gamma_r^t\eta_2$ for paths $\eta_1,\eta_2$ of length at most $\bound{1}$.

Using \[lem:linear form of paths\], we split an accepting run on $n$ that visits $r$ to 