, the transition from $q$ goes to a forever accepting state ($heaven$), and if $a=$, it goes to the state of $\A$ that corresponds to the line $l_i$. This is the “command-checker gadget” of $\A$.

Counting cheats are more challenging to verify, as OCNs cannot branch according to a counter value. We consider separately “positive cheats” and “negative cheats”. The former stands for the case that the input letter is (or ) while the value of $x$ (or $y$) in the legal run of $\M$ should be positive. The latter stands for the case that the input letter is (or ) while the value of $x$ (or $y$) in the legal run of $\M$ should be $0$.

Positive cheats can be verified by directly simulating the respective counter of $\M$ using the counter in $\A$ (states $q_3$ and $q_5$ in \[fig:A\]). Once the cheat occurs, $\A$ can return to $q_0$ with a penalty of $-1$, and since the counter in $\M$ is positive, we are guaranteed that the counter in $\A$ did not decrease since leaving $q_0$, allowing $\A$ to continue the run.

For verifying a negative cheat, we simulate the counting of $\M$ by an “opposite-counting” in $\A$ (states 