Let \(P\) be a counter program on a binary input \(x\), let \(\ell , \ell '\) be labels, \(\ell ''\) a label or the halted state, \(\rho , \rho ', \rho ''\) register vectors and \(p, p', p''\) input positions. Suppose that from label \(\ell \) with registers \(\rho \) and \(p\) symbols read, \(P\) reaches label \(\ell '\) with registers \(\rho '\) and \(p'\) symbols read within \(b\) steps while appending \(e\) to whatever output was printed before, and that from \((\ell ', \rho ', p')\) it reaches \((\ell '', \rho '', p'')\) within \(b'\) steps while appending \(e'\). Then from \((\ell , \rho , p)\) it reaches \((\ell '', \rho '', p'')\) within \(b + b'\) steps while appending the concatenation \(e\, e'\).

Let \(P\) be a counter program on a binary input \(x\) and let \(b \le b'\). If from label \(\ell \) with registers \(\rho \) and \(p\) input symbols read, \(P\) reaches \(\ell '\) (a label or the halted state) with registers \(\rho '\) and \(p'\) symbols read within \(b\) steps while appending \(e\) to its output, then it does so within \(b'\) steps as well.

Let \(P\) be a counter program on a binary input \(x\). Suppose that from label \(\ell \) with registers \(\rho \) and \(p\) input symbols read, \(P\) reaches \(\ell '\) (a label or the halted state) with registers \(\rho '\) and \(p'\) symbols read within \(b\) steps while appending \(e\) to its output, and that \(\rho = \sigma \), \(\rho ' = \sigma '\), \(p = q\), \(p' = q'\), \(e = e'\) and \(b \le b'\). Then from label \(\ell \) with registers \(\sigma \) and \(q\) symbols read, \(P\) reaches \(\ell '\) with registers \(\sigma '\) and \(q'\) symbols read within \(b'\) steps while appending \(e'\).

Let \(P\) be a counter program on a binary input \(x\), let \(\ell \) be a label, \(\ell '\) a label or the halted state, \(\rho , \rho '\) register vectors, \(p, p'\) input positions and \(e\) a bit string. If for every output \(o\) one step of \(P\) on \(x\) maps the state with label \(\ell \), registers \(\rho \), \(p\) symbols read and output \(o\) to the state with label \(\ell '\), registers \(\rho '\), \(p'\) symbols read and output \(o\, e\), then from \((\ell , \rho , p)\) the program reaches \((\ell ', \rho ', p')\) within one step while appending \(e\) to its output.

Let \(P\) be a counter program on a binary input \(x\) and \(\ell \) a label whose instruction is \(\mathsf{halt}\). Then for all registers \(\rho \) and input positions \(p\), from label \(\ell \) with registers \(\rho \) and \(p\) symbols read the program reaches the halted state, with registers still \(\rho \) and still \(p\) symbols read, within one step and without printing anything.

Let \(P\) be a counter program on a binary input \(x\) and \(\ell \) a label whose instruction is \(\mathsf{goto}\ \ell '\). Then for all registers \(\rho \) and input positions \(p\), from label \(\ell \) with registers \(\rho \) and \(p\) symbols read the program reaches label \(\ell '\) with registers \(\rho \) and \(p\) symbols read within one step, without printing anything.

Let \(P\) be a counter program on a binary input \(x\) and \(\ell \) a label whose instruction is \(\mathsf{out}(b, \ell ')\), “print the bit \(b\), then go to \(\ell '\)”. Then for all registers \(\rho \) and input positions \(p\), from label \(\ell \) with registers \(\rho \) and \(p\) symbols read the program reaches label \(\ell '\) with registers \(\rho \) and \(p\) symbols read within one step, appending the single bit \(b\) to its output.

Let \(P\) be a counter program on a binary input \(x\), \(r\) a register and \(\ell \) a label whose instruction is \(\mathsf{inc}(r, \ell ')\). Then for all registers \(\rho \) and input positions \(p\), from label \(\ell \) with registers \(\rho \) and \(p\) symbols read the program reaches label \(\ell '\) within one step, printing nothing, with \(p\) symbols read and registers \(\rho \) except that register \(r\) now holds \(\rho (r) + 1\).

Let \(P\) be a counter program on a binary input \(x\), \(r\) a register and \(\ell \) a label whose instruction is \(\mathsf{dec}(r, \ell ')\). Then for all registers \(\rho \) and input positions \(p\), from label \(\ell \) with registers \(\rho \) and \(p\) symbols read the program reaches label \(\ell '\) within one step, printing nothing, with \(p\) symbols read and registers \(\rho \) except that register \(r\) now holds \(\max (\rho (r) - 1, 0)\).

Let \(P\) be a counter program on a binary input \(x\), \(r\) a register and \(\ell \) a label whose instruction is \(\mathsf{jz}(r, \ell _0, \ell _1)\), “go to \(\ell _0\) if register \(r\) is zero, else to \(\ell _1\)”. If the registers \(\rho \) satisfy \(\rho (r) = 0\), then for every input position \(p\), from label \(\ell \) with registers \(\rho \) and \(p\) symbols read the program reaches label \(\ell _0\) with registers \(\rho \) and \(p\) symbols read within one step, printing nothing.

Let \(P\) be a counter program on a binary input \(x\), \(r\) a register and \(\ell \) a label whose instruction is \(\mathsf{jz}(r, \ell _0, \ell _1)\), “go to \(\ell _0\) if register \(r\) is zero, else to \(\ell _1\)”. If the registers \(\rho \) satisfy \(\rho (r) \ne 0\), then for every input position \(p\), from label \(\ell \) with registers \(\rho \) and \(p\) symbols read the program reaches label \(\ell _1\) with registers \(\rho \) and \(p\) symbols read within one step, printing nothing.

Let \(P\) be a counter program on a binary input \(x\), \(r\) a register and \(\ell \) a label whose instruction is \(\mathsf{pr}(r, \ell ')\), “print the value of register \(r\) in unary, then go to \(\ell '\)”. Then for all registers \(\rho \) and input positions \(p\), from label \(\ell \) with registers \(\rho \) and \(p\) symbols read the program reaches label \(\ell '\) with registers \(\rho \) and \(p\) symbols read within one step, appending the string \(1^{\rho (r)}\) of \(\rho (r)\) ones to its output.

Let \(P\) be a counter program on a binary input \(x\) and \(\ell \) a label whose instruction is \(\mathsf{rd}(\ell _e, \ell _0, \ell _1)\), “read the next input symbol and go to \(\ell _e\), \(\ell _0\) or \(\ell _1\) according as the input has ended, the symbol is \(0\), or it is \(1\)”. If \(x\) has no symbol at (zero-based) position \(p\), i.e. \(p \ge |x|\), then for all registers \(\rho \), from label \(\ell \) with registers \(\rho \) and \(p\) symbols read the program reaches label \(\ell _e\) with registers \(\rho \) and still \(p\) symbols read within one step, printing nothing.

Let \(P\) be a counter program on a binary input \(x\) and \(\ell \) a label whose instruction is \(\mathsf{rd}(\ell _e, \ell _0, \ell _1)\), “read the next input symbol and go to \(\ell _e\), \(\ell _0\) or \(\ell _1\) according as the input has ended, the symbol is \(0\), or it is \(1\)”. If the symbol of \(x\) at (zero-based) position \(p\) is \(0\), then for all registers \(\rho \), from label \(\ell \) with registers \(\rho \) and \(p\) symbols read the program reaches label \(\ell _0\) with registers \(\rho \) and \(p + 1\) symbols read within one step, printing nothing.

Let \(P\) be a counter program on a binary input \(x\) and \(\ell \) a label whose instruction is \(\mathsf{rd}(\ell _e, \ell _0, \ell _1)\), “read the next input symbol and go to \(\ell _e\), \(\ell _0\) or \(\ell _1\) according as the input has ended, the symbol is \(0\), or it is \(1\)”. If the symbol of \(x\) at (zero-based) position \(p\) is \(1\), then for all registers \(\rho \), from label \(\ell \) with registers \(\rho \) and \(p\) symbols read the program reaches label \(\ell _1\) with registers \(\rho \) and \(p + 1\) symbols read within one step, printing nothing.

Let \(P\) be a counter program on a binary input \(x\), \(r\) a register, and \(h, d, c, z\) labels such that the instruction at \(h\) is \(\mathsf{jz}(r, z, d)\) (go to \(z\) if register \(r\) is zero, else to \(d\)) and the instruction at \(d\) is \(\mathsf{dec}(r, c)\). Let \(K, b \in \mathbb {N}\), and for each \(j \in \mathbb {N}\) let \(\sigma _j\) be a register vector, \(p_j\) an input position and \(e_j\) a bit string, with \(\sigma _j(r) = K - j\) for all \(j \le K\). Suppose that for every \(j \lt K\), from label \(c\) with registers \(\sigma _j\) modified so that register \(r\) holds \(K - j - 1\), and \(p_j\) symbols read, \(P\) reaches label \(h\) with registers \(\sigma _{j+1}\) and \(p_{j+1}\) symbols read within \(b\) steps while appending \(e_j\) to its output. Then from label \(h\) with registers \(\sigma _0\) and \(p_0\) symbols read, \(P\) reaches label \(z\) with registers \(\sigma _K\) and \(p_K\) symbols read within \(K(b+2)+1\) steps while appending the concatenation \(e_0 e_1 \cdots e_{K-1}\).

Let \(P\) be a counter program on a binary input \(x\), let \(\tau = (m_0, \dots , m_{n-1})\) be a list of micro-operations, each either “print a bit \(b\)” or “print register \(r\) in unary”, and let \(\lambda : \mathbb {N} \to \Lambda \) and \(\nu \in \Lambda \) be labels. Suppose that for each \(i \lt n\) the instruction of \(P\) at \(\lambda (i)\) performs \(m_i\) and then goes to \(\lambda (i+1)\), and the instruction at \(\lambda (n)\) is \(\mathsf{goto}\ \nu \). Then for all registers \(\rho \) and input positions \(p\), from label \(\lambda (0)\) with registers \(\rho \) and \(p\) symbols read the program reaches label \(\nu \) with registers \(\rho \) and \(p\) symbols read within \(n + 1\) steps, appending \(w_0 w_1 \cdots w_{n-1}\) to its output, where \(w_i\) is \(b\) if \(m_i\) prints the bit \(b\) and \(w_i = 1^{\rho (r)}\) if \(m_i\) prints register \(r\).

Let \(\rho : \{ 0,\dots ,R-1\} \to \mathbb {N}\) be register values and \((L, c)\) a linear expression with \(L = (r_1, \dots , r_k)\). Concatenating the strings printed under \(\rho \) by the micro-operations \(\mathsf{pr}(r_1), \dots , \mathsf{pr}(r_k)\) followed by \(c\) copies of \(\mathsf{out}(1)\), where \(\mathsf{pr}(r)\) prints \(1^{\rho (r)}\) and \(\mathsf{out}(1)\) prints \(1\), gives exactly the unary string \(1^{v}\) with \(v = \rho (r_1) + \dots + \rho (r_k) + c\).

For any register values \(\rho \) and any bit string \(w = w_1 \cdots w_n\), concatenating the strings printed under \(\rho \) by the micro-operations \(\mathsf{out}(w_1), \dots , \mathsf{out}(w_n)\), where \(\mathsf{out}(b)\) prints the single bit \(b\), gives back \(w\).

Let \(P\) be a counter program over \(R\) registers with a finite label set \(\Lambda \), let \(\ell _0 \in \Lambda \), let \(x\) be a binary input, and let \(M\) be the multi-tape Turing machine compiled from \(P\) with start label \(\ell _0\), which keeps each register on its own work tape in unary. For an abstract state \(s\) (label or halted, registers \(\rho _s\), number \(\mathrm{pos}(s)\) of input symbols read, output so far) let \(\mathrm{enc}(s)\) be the configuration of \(M\) in the control state for the label of \(s\) (or halted), with the input head on the next unread symbol, work tape \(r\) holding \(1^{\rho _s(r)}\) with its head on cell \(\rho _s(r)\), and output equal to that of \(s\). Let \(B \in \mathbb {N}\). Then for every \(t \in \mathbb {N}\) and every abstract state \(s\) with \(\mathrm{pos}(s) \le |x|\) and \(\rho _s(r) + t \le B\) for every register \(r\), there is \(t' \le t(2B+3)\) such that running \(M\) for \(t'\) steps from \(\mathrm{enc}(s)\) yields \(\mathrm{enc}(s_t)\), where \(s_t\) is the state reached by \(t\) steps of \(P\) on \(x\) from \(s\).

Let \(P\) be a counter program over \(R\) registers with a finite label set \(\Lambda \) and start label \(\ell _0\), let \(x\) be a binary input and \(t \in \mathbb {N}\). Suppose that \(t\) steps of \(P\) on \(x\), started from the initial state (label \(\ell _0\), all registers \(0\), nothing read, empty output), reach a halted state, and let \(y\) be its output. Then the multi-tape Turing machine compiled from \(P\) with start label \(\ell _0\), which keeps each register on its own work tape in unary, computes \(y\) on input \(x\) in time \(t(2t+3)\): after \(t(2t+3)\) steps from its initial configuration on \(x\) it is halted with output \(y\).

Let \(P\) be a counter program on a binary input \(x\), let \(s\) be an abstract state of \(P\) in which \(\mathrm{pos}(s)\) input symbols have been read, and let \(t \in \mathbb {N}\). Then after \(t\) steps of \(P\) on \(x\) from \(s\) the number of input symbols read is at most \(\mathrm{pos}(s) + t\).

Let \(P\) be a counter program on a binary input \(x\) and \(s\) an abstract state of \(P\) with output \(o\). Then there is a bit string \(e\) such that the output after one step of \(P\) on \(x\) from \(s\) is \(o\, e\).

Let \(P\) be a counter program on a binary input \(x\), \(s\) an abstract state of \(P\) with output \(o\), and \(t \in \mathbb {N}\). Then there is a bit string \(e\) such that the output after \(t\) steps of \(P\) on \(x\) from \(s\) is \(o\, e\).

Let \(P\) be a counter program on a binary input \(x\), \(K \in \mathbb {N}\), and \(s\) an abstract state of \(P\) with output \(o\) in which every register holds at most \(K\). Then the output after one step of \(P\) on \(x\) from \(s\) has length at most \(|o| + K + 1\).

Let \(P\) be a counter program on a binary input \(x\), \(\ell _0\) a label and \(t \in \mathbb {N}\). Starting from the initial state at \(\ell _0\) (all registers \(0\), nothing read, empty output), the output after \(t\) steps of \(P\) on \(x\) has length at most \(t(t+1)\).