check that $n\notin \Lang{\initialstate,c_0}$, or (2) guess $\bound{3}^{|\states|}\le n\le 2\bound{3}^{|\states|}$ and check that $n\notin \LangVia{\initialstate,c_0}{r}$ for all $r\in \Pump$, which implies that $n\notin\?P$.

Note that even if the transitions are encoded in unary, $n$ still needs to be guessed in binary for part (2) (and also for part (1) if the encoding is binary). The complexity of the checks involved in both parts of the algorithm depend on the encoding of the transitions, and are handled separately in the following.

##### Unary Encoding. {#unary-encoding. .unnumbered}

If the transitions are encoded in unary, then $\bound{3}$ is polynomial in the size of the OCN. Consequently, we can check for $n<\bound{3}$ whether $n\in \Lang{\initialstate,c_0}$ by simulating the OCN for $n$ steps, while keeping track of the maximal run to each state. Indeed, due to the monotonicity of executability of OCN paths it suffices to remember, for each state $s$, the maximal possible counter-value $c$ so that $(s,c)$ is reachable via the current prefix, which must be a number $\le c_0 + n\cdot \norm{\transitions}$ or $-\infty$ (to represent that no configuration $(s,c)$ can be reached).

Next, in order to check whether $n\notin \LangVia{\initialstate,c_0}{r}$ for all $r\in \Pump$ for $\bound{3}^{|\states|}\le n\le 2\bound{3}^{|\states|}$ written in binary, 