For all natural numbers \(C\) and \(c\), the map \(n \mapsto n + C\, (n+1)^c\) on the natural numbers is strictly increasing.

Let \(C, c\) be natural numbers and let \(x, u, y, v\) be binary strings with \(|u| = C\, (|x|+1)^c\) and \(|v| = C\, (|y|+1)^c\). If the concatenations \(x\, u\) and \(y\, v\) are equal as strings, then \(x = y\) and \(u = v\).

For natural numbers \(C\), \(c\) and \(m\), the bounded search for a split position (which scans all \(n \le m\) for a solution of \(n + C\, (n+1)^c = m\)) returns no result if and only if no natural number \(n\) satisfies \(n + C\, (n+1)^c = m\).

For natural numbers \(C\), \(c\), \(m\) and \(n\) with \(n + C\, (n+1)^c = m\), the bounded search for a split position at length \(m\) succeeds and returns exactly \(n\).

Let \(N\) be a nondeterministic Turing machine over the binary alphabet, let \(C, c\) be natural numbers, and let \(x\) and \(u\) be binary strings with \(|u| = C\, (|x|+1)^c\). Then the concatenation \(x\, u\) belongs to the choice-word verifier language of \(N\) with parameters \(C, c\) if and only if the run of \(N\) on input \(x\) under choice word \(u\) has halted with output exactly the one-bit string \(1\).

Let \(N\) be a nondeterministic Turing machine over the binary alphabet and let \(C, c\) be natural numbers. If no natural number \(n\) satisfies \(n + C\, (n+1)^c = |y|\) for a binary string \(y\) (so the bounded split search fails at length \(|y|\)), then \(y\) does not belong to the choice-word verifier language of \(N\) with parameters \(C, c\).

Let \(N\) be a nondeterministic Turing machine over the binary alphabet, let \(x\) be an input string, and let \(t \le t'\) be step budgets such that every choice word of length \(t\) drives \(N\) on \(x\) into a halted configuration. Then \(N\) accepts \(x\) within \(t'\) steps if and only if \(N\) accepts \(x\) within \(t\) steps, where acceptance within a budget means that some choice word of exactly that length yields a halted run with output the one-bit string \(1\).

For all natural numbers \(a\), \(c\) and \(n\), the inequality \(a\, (n^c + 1) \le 2a\, (n+1)^c\) holds.

Let \(N\) be a nondeterministic Turing machine over the binary alphabet that decides a language \(L\) within time \(a\, (n^c+1)\) on inputs of length \(n\), meaning that every branch halts within the budget and acceptance characterizes membership. Then for every binary string \(x\): \(x \in L\) if and only if there is a binary string \(u\) with \(|u| = 2a\, (|x|+1)^c\) such that the concatenation \(x\, u\) lies in the choice-word verifier language of \(N\) with parameters \(2a\) and \(c\).

For every binary string \(w\) and every optional bit \(e\), updating the output summary of \(w\) by the emission \(e\) equals the output summary of \(w\) with the content of \(e\) appended.

For every binary string \(w\), the output summary of \(w\) equals the bit \(1\) if and only if \(w\) is exactly the one-bit string \(1\).

Let \(N\) be a nondeterministic Turing machine over the binary alphabet, let a configuration of \(N\) on input \(x\) carry a valid virtual boundary tag, and let \(u\) be a choice word with next unread index \(j \lt |u|\). Then one physical step of the simulation core of \(N\) transforms the embedded configuration into the embedding of the configuration obtained by one step of \(N\) under the choice bit at position \(j\), with choice index \(j+1\) and some valid updated boundary tag.

Let \(N\) be a nondeterministic Turing machine over the binary alphabet, let a configuration of \(N\) on input \(x\) carry a valid virtual boundary tag, and let \(u\) be a choice word with \(t \le |u|\). Then \(t\) physical steps of the simulation core of \(N\) carry the embedded configuration to the embedding of the run of \(N\) under the first \(t\) bits of \(u\), again with a valid boundary tag.

Let \(N\) be a nondeterministic Turing machine over the binary alphabet and consider the embedding of a configuration of \(N\) whose choice head stands at the blank after the complete choice word \(u\). One further step of the simulation core halts with output a single bit, and that bit is \(1\) exactly when the embedded source configuration has halted with output the one-bit string \(1\).

Let \(N\) be a nondeterministic Turing machine over the binary alphabet, let a configuration of \(N\) carry a valid virtual boundary tag, and let \(u\) be a choice word. From the prepared embedded configuration, the simulation core of \(N\) halts after exactly \(|u| + 1\) steps, and its output is the single bit recording whether the run of \(N\) under \(u\) from that configuration has halted with output the one-bit string \(1\).

For every nondeterministic Turing machine \(N\) over the binary alphabet and every input string \(x\), the initial configuration of \(N\) on \(x\) satisfies the virtual boundary-tag invariant with the interior tag value (its input head starts at position one, inside the window).

For all natural numbers \(C\), \(c\) and \(m\), the library split-search function and the local bounded split search return the same optional split position for the length equation \(n + C\, (n+1)^c = m\).

Let \(N\) be a nondeterministic machine over the binary alphabet and let \(d\) be any configuration of the simulation core of \(N\). For every step count \(t\), running the pair-loader machine of \(N\) for \(t\) steps from the state-renamed copy of \(d\) yields exactly the state-renamed copy of the \(t\)-step run of the simulation core from \(d\).

Let \(N\) be a nondeterministic machine, let \(x\) and \(u\) be buffer words, and let \(j \le |u|\). From the loader configuration in the choice-rewind state with choice head at position \(j - 1\), exactly \(j + 1\) steps of the pair-loader machine reach the renamed embedding of the initial configuration of \(N\) on \(x\) prepared with choice word \(u\), preserving the physical input position.

Let \(N\) be a nondeterministic machine, let \(x\) and \(u\) be buffer words, and let \(j \le |x|\). From the loader configuration in the input-rewind state with input-buffer head at position \(j-1\) and choice head at the right end of \(u\), exactly \(j+1\) steps of the pair-loader machine reach the choice-rewind state with input-buffer head reset to zero and choice head at position \(|u| - 1\), with all tape contents preserved.

Let \(N\) be a nondeterministic machine and consider a loader configuration whose two buffer heads stand at the right blanks of the buffer words \(x\) and \(u\). Applying an action that optionally writes one bit at each of the two buffer heads (advancing a head exactly when it writes) produces the loader configuration whose buffers are \(x\) and \(u\) with the respective optional bits appended, with the physical input head moved by the action’s input move and all other tapes unchanged.

Let \(N\) be a nondeterministic machine and consider a loader configuration over a physical input \(y\) whose input head is at position \(i + 1\) with \(i \le |y|\). The symbol read from the physical input is the optional bit of \(y\) at index \(i\), which is blank exactly at the right boundary.

Let \(N\) be a nondeterministic machine, let \(y\) be a physical input with position index \(i \lt |y|\), and suppose the transition table of the pair-loader machine, applied in a loader state \(q\) to the bit of \(y\) at index \(i\), yields a right input move that optionally appends one bit to each buffer and enters a loader state \(q'\). Then one physical step from the loader configuration at position \(i+1\) with buffers \(x\) and \(u\) (heads at their right blanks) produces the loader configuration at position \(i+2\) in state \(q'\) with the appended buffers.

Let \(N\) be a nondeterministic machine and let the physical input \(y\) decompose as \(y = p\, r\) for words \(p\) and \(r\). From the suffix-copy loader state at position \(|p| + 1\) with buffers \(x\) and \(u\), exactly \(|r|\) steps of the pair-loader machine append \(r\) to the choice buffer, ending at the right boundary of \(y\) with the input buffer \(x\) unchanged and no physical output.

Let \(N\) be a nondeterministic machine and let \(x\) and \(u\) be the buffer words held by a loader configuration at the right boundary of the physical input \(y\). Exactly \(1 + (|x|+1) + (|u|+1)\) further steps of the pair-loader machine (one dispatch and the two buffer rewinds) reach the renamed embedding of the initial configuration of \(N\) on \(x\) prepared with choice word \(u\); no bits of the choice word are consumed by these administrative steps.

Let \(N\) be a nondeterministic machine and let the physical input decompose as \(y = p\, u\). Starting in the suffix-copy state at position \(|p|+1\) with input buffer \(x\) and empty choice buffer, after \(|u| + (1 + (|x|+1) + (|u|+1)) + (|u|+1)\) steps the pair-loader machine has halted, and its output is the single bit recording whether the run of \(N\) on \(x\) under choice word \(u\) has halted with output the one-bit string \(1\).

Let \(N\) be a nondeterministic machine and suppose the physical input has the form \(y = p\, b\, b\, r\) for a bit \(b\). From the initial parser state at position \(|p|+1\) with input buffer \(x\), exactly two steps of the pair-loader machine append \(b\) to the input buffer and move to position \(|p|+3\), leaving the choice buffer empty and the output silent.

Let \(N\) be a nondeterministic machine and suppose the physical input has the form \(y = p\, 0\, 1\, u\). From the initial parser state at position \(|p|+1\) with input buffer \(x\), exactly two steps of the pair-loader machine enter the suffix-copy state at position \(|p|+3\) without modifying either buffer or emitting output.

Let \(N\) be a nondeterministic machine and suppose the physical input has the form \(y = p\, e\) where \(e\) is the self-delimiting encoding of a pair \((x, u)\). From the initial parser state at position \(|p|+1\) with input buffer \(a\), exactly \(2|x| + 2\) steps of the pair-loader machine decode the doubled prefix and the separator, reaching the suffix-copy state at position \(|p| + 2|x| + 3\) with input buffer \(a\, x\) and the choice buffer still empty.

Let \(N\) be a nondeterministic Turing machine over the binary alphabet and let \(x\) and \(u\) be binary strings. On the self-delimiting encoding of the pair \((x,u)\), the pair-loader machine of \(N\) halts from blank tapes within \(3(\ell + 1)\) steps, where \(\ell \) is the length of the encoded pair, and outputs the single bit recording whether the run of \(N\) on \(x\) under choice word \(u\) has halted with output the one-bit string \(1\).

For every nondeterministic Turing machine \(N\) over the binary alphabet, the pair-loader machine of \(N\) on the empty input halts within one step, and its output is the single bit \(0\).

For all natural numbers \(C, c\) and every binary string \(y\), the word emitted by the polynomial split emitter on \(y\) has length at most \(2|y| + 2\).

Let \(N\) be a nondeterministic Turing machine over the binary alphabet and let \(C, c\) be natural numbers. For every binary string \(y\), the pair-loader machine of \(N\), run on the word emitted by the polynomial split emitter for \(y\), halts within \(3(2|y|+3)\) steps, and its output is the indicator bit of membership of \(y\) in the choice-word verifier language of \(N\) with parameters \(C, c\).

For every nondeterministic Turing machine \(N\) over the binary alphabet and all natural numbers \(C\) and \(c\), the choice-word verifier language of \(N\) with parameters \(C, c\) belongs to the class \(\mathrm{P}\).

For every mask \(m\) and every choice word \(w\) with \(|w| = |m|\), the word selected from \(w\) along \(m\) has length equal to the number of \(1\) entries of \(m\).

Let \(m\) be a mask and let \(u\) be a binary string whose length equals the number of \(1\) entries of \(m\). Then there is a choice word \(w\) with \(|w| = |m|\) whose selection along \(m\) is exactly \(u\).

For every deterministic machine \(M\), configuration \(d\) and step count \(t\), the emission mask of the run of \(M\) from \(d\) over \(t\) steps has length exactly \(t\).

Let \(M\) be a deterministic machine, \(d\) a configuration and \(t\) a step count. The output length of \(d\) plus the number of \(1\) entries in the emission mask over \(t\) steps equals the output length of the configuration reached after \(t\) steps of \(M\) from \(d\).

Let \(M\) be a deterministic machine over the binary alphabet, \(d\) one of its configurations, \(u\) a captured word and \(b\) a choice bit. One nondeterministic step of the guessing-phase machine of \(M\) under \(b\) maps the invariant configuration for \((d, u)\) to the invariant configuration for the stepped configuration of \(M\), with \(b\) appended to the captured word exactly when \(M\) emits an output symbol at \(d\).

Let \(M\) be a deterministic machine over the binary alphabet, \(d\) a configuration, \(u\) a captured word and \(w\) a word of choice bits. Running the guessing-phase machine of \(M\) under \(w\) from the invariant configuration for \((d,u)\) yields the invariant configuration for the \(|w|\)-step run of \(M\) from \(d\), with the selection of \(w\) along the emission mask appended to the captured word.

For every deterministic machine \(M\) over the binary alphabet and every input \(x\), the blank-tape initial configuration of the guessing-phase machine of \(M\) on \(x\) equals the invariant configuration for the initial configuration of \(M\) on \(x\) with empty captured word.

Let \(M\) be a deterministic machine over the binary alphabet that computes an output \(v\) on input \(x\) within \(T\) steps. Then every choice word of length \(T\) drives the guessing-phase machine of \(M\) from its initial configuration on \(x\) to the invariant configuration for the \(T\)-step run of \(M\), with some captured word of length \(|v|\); and conversely, every word \(u\) with \(|u| = |v|\) is the captured word of that configuration for some choice word of length \(T\).

For all natural numbers \(C, c, K, r\) and \(n\), the bound \(K\, (n + C(n+1)^c + 1)^r \le K\, (C+1)^r\, 2^{\, r \cdot \max (1,c)} \cdot (n^{\, r \cdot \max (1,c)} + 1)\) holds.

Let \(L\) be a language over the binary alphabet and \(C, c\) natural numbers. If some nondeterministic machine decides \(L\) within time \(K\, (n + C(n+1)^c + 1)^r\) for some constants \(K\) and \(r\), then \(L\) belongs to \(\bigcup _{e} \mathrm{NTIME}(n^e + 1)\).

For all natural numbers \(C\) and \(c\) there exist a deterministic scheduler machine \(M\) and a constant \(A\) such that for every \(n\), on the unary input of length \(n\) and with \(T = A(n+1)^{c+1}\): every choice word of length \(T\) drives the guessing-phase machine of \(M\) to the completed \(T\)-step configuration while capturing some word of length exactly \(C(n+1)^c\), and every word of that length is captured by some choice word of length \(T\).

For every configuration \(d\) on an input \(x\), the input symbol read by the reinterpretation of \(d\) over the all-ones word of length \(|x|\) equals the symbol read by \(d\) with every non-blank bit replaced by \(1\).

For every tape action \(a\) and every configuration \(d\) on an input \(x\), reinterpreting the result of applying \(a\) to \(d\) over the all-ones word equals applying \(a\) to the reinterpretation of \(d\); input-head clamping depends only on the input length.

Let \(M\) be a deterministic machine over the binary alphabet and \(d\) a configuration on an input \(x\). The unary reinterpretation of one step of the input-normalized variant of \(M\) at \(d\) equals one native step of \(M\) at the unary reinterpretation of \(d\), including the absorbing halted case.

Let \(M\) be a deterministic machine over the binary alphabet, \(d\) a configuration on an input \(x\), and \(t\) a step count. The unary reinterpretation of the \(t\)-step run of the input-normalized variant of \(M\) from \(d\) equals the \(t\)-step run of \(M\) from the reinterpretation of \(d\).

For every deterministic machine \(M\) over the binary alphabet and every input \(x\), the reinterpretation of the initial configuration of the input-normalized variant of \(M\) on \(x\) equals the initial configuration of \(M\) on the all-ones word of length \(|x|\).

Let \(M\) be a deterministic machine over the binary alphabet, \(d\) a configuration and \(t\) a step count. The emission mask of the input-normalized variant of \(M\) over \(t\) steps from \(d\) equals the emission mask of \(M\) over \(t\) steps from the unary reinterpretation of \(d\).

Let \(M\) be a deterministic machine over the binary alphabet and suppose \(M\) computes an output \(v\) within \(t\) steps on the all-ones input of length \(|x|\). Then the input-normalized variant of \(M\) computes \(v\) within \(t\) steps on the input \(x\) itself.

Let \(M\) be a deterministic machine over the binary alphabet such that for every \(n\), on the all-ones input of length \(n\), \(M\) computes a word \(f(n)\) within \(T(n)\) steps. Then there is a function \(\tau \) with \(\tau (n) \le T(n)\) for all \(n\) such that on every input \(x\), the input-normalized variant of \(M\) computes \(f(|x|)\) within \(\tau (|x|)\) steps and is still live at every time before \(\tau (|x|)\).

Let \(S\) and \(V\) be deterministic machines and let \(q\) be any control state of the reverse host built from \(S\) and \(V\) that is not a live guessing state. For every input symbol and every tuple of work-tape symbols, the two transition tables of the host agree at \(q\).

Let \(S, V\) be deterministic machines, \(d\) a non-halted scheduler configuration on an input \(x\), \(u\) a guessed word and \(b\) a choice bit. One step of the reverse host under \(b\) maps the guessing-phase configuration for \((d,u)\) to the guessing-phase configuration for the stepped configuration of the input-normalized variant of \(S\), with \(b\) appended to the guessed word exactly when that machine emits at \(d\).

Let \(S, V\) be deterministic machines, \(d\) a scheduler configuration on an input \(x\), \(u\) a guessed word, and \(w\) a word of choice bits such that the input-normalized scheduler is still live at every time before \(|w|\). Running the reverse host under \(w\) from the guessing-phase configuration for \((d,u)\) gives the guessing-phase configuration for the \(|w|\)-step scheduler run, with the selection of \(w\) along the scheduler emission mask appended to the guessed word.

Let \(S, V\) be deterministic machines and \(x\) an input with position index \(i \lt |x|\). For every choice bit, one step of the reverse host from the copy-state loader configuration holding the first \(i\) bits of \(x\) appends the bit of \(x\) at index \(i\) to the assembly buffer and advances the input head by one.

Let \(S, V\) be deterministic machines, \(x\) an input, and \(w\) any word of choice bits with \(i + |w| \le |x|\). Running the reverse host under \(w\) from the copy-state loader configuration holding the first \(i\) bits of \(x\) yields the copy-state configuration holding the first \(i + |w|\) bits, one bit copied per step regardless of the choices.

Let \(S, V\) be deterministic machines and \(x\) an input. From the rewind-state loader configuration with input head at the left blank and assembly buffer exactly \(x\), one host step (for any choice bit) yields the guessing-phase configuration for the initial configuration of the input-normalized scheduler on \(x\) with empty guessed word.

Let \(S, V\) be deterministic machines and \(x\) an input with \(j \lt |x|\). For any choice bit, one host step from the rewind-state loader configuration with input head at position \(j+1\) and assembly buffer \(x\) moves the input head to position \(j\), leaving all tapes unchanged.

Let \(S, V\) be deterministic machines, \(x\) an input, \(j \le |x|\), and \(w\) any word of choice bits with \(|w| = j + 1\). Running the reverse host under \(w\) from the rewind-state loader configuration with input head at position \(j\) and assembly buffer \(x\) reaches the guessing-phase configuration for the initial normalized-scheduler configuration on \(x\) with empty guessed word.

For all deterministic machines \(S, V\) and every input \(x\), the blank-tape initial configuration of the reverse host built from \(S\) and \(V\) equals the copy-state loader configuration with empty assembly buffer, input head at position one and assembly head at zero.

Let \(S, V\) be deterministic machines and \(x\) an input. For any choice bit, one host step from the copy-state loader configuration at the right input blank with assembly buffer \(x\) yields the rewind-state configuration with the input head moved left to position \(|x|\).

Let \(S, V\) be deterministic machines, \(x\) an input, and \(w\) any word of choice bits with \(|w| = 2|x| + 2\). Running the reverse host under \(w\) from its blank-tape initial configuration on \(x\) reaches the guessing-phase configuration for the initial configuration of the input-normalized scheduler on \(x\) with empty guessed word; all startup choices are ignored.

Let \(M\) be a deterministic machine, \(d\) one of its configurations, and \(u, v\) captured words. If the guessing-phase invariant configurations for \((d,u)\) and \((d,v)\) are equal, then \(u = v\).

Let \(S, V\) be deterministic machines and suppose the input-normalized scheduler on an input \(x\) computes an output \(v\) within \(T\) steps while remaining live at all earlier times. Then every choice word of length \(T\) drives the reverse host from the start-of-guessing configuration to the completed-scheduler guessing configuration with some guessed word of length \(|v|\), and every word of length \(|v|\) arises this way from some choice word of length \(T\).

Let \(S, V\) be deterministic machines, \(d\) a non-halted verifier configuration on an assembled word \(y\) carrying a valid virtual boundary tag, and fix frozen scheduler data and a physical position. For every choice bit, one host step maps the verifier-phase configuration for \(d\) to the verifier-phase configuration for the stepped verifier, with some valid updated tag; reads come from the assembly buffer and every emission of \(V\) is captured, including one on a halting transition.

Let \(S, V\) be deterministic machines, \(d\) a verifier configuration with a valid boundary tag, and \(w\) a choice word such that the verifier is live at every time before \(|w|\). Running the host under \(w\) from the verifier-phase configuration for \(d\) yields the verifier-phase configuration for the \(|w|\)-step verifier run, with a valid tag; the choices are ignored.

Let \(S, V\) be deterministic machines and \(d\) a halted verifier configuration. For any choice bit, one host step from the verifier-phase configuration for \(d\) halts the host and emits the single bit recording whether the complete output of \(d\) is exactly the one-bit string \(1\).

Let \(S, V\) be deterministic machines, \(d\) a halted scheduler configuration on an input \(x\), and \(u\) a guessed word. For any choice bit, one host step from the guessing-phase configuration for \((d,u)\) yields the assembly-rewind configuration holding the assembled word \(x\, u\) with assembly head at its last cell.

Let \(S, V\) be deterministic machines, \(d\) a scheduler configuration, \(y\) an assembled word and \(j \lt |y|\). For any choice bit, one host step from the assembly-rewind configuration with head at cell \(j\) moves the head to cell \(j - 1\), preserving \(y\) and the scheduler bank.

Let \(S, V\) be deterministic machines, \(d\) a scheduler configuration and \(y\) an assembled word. For any choice bit, one host step from the assembly-rewind configuration with head at cell \(-1\) yields the verifier-phase configuration for the initial configuration of \(V\) on \(y\), with interior boundary tag, blank verifier tapes and empty captured output.

Let \(S, V\) be deterministic machines, \(d\) a scheduler configuration, \(y\) an assembled word, \(j \le |y|\), and \(w\) any choice word with \(|w| = j + 1\). Running the host under \(w\) from the assembly-rewind configuration with head at cell \(j - 1\) reaches the verifier-phase configuration for the initial configuration of \(V\) on \(y\).

Let \(S, V\) be deterministic machines, \(d\) a halted scheduler configuration on an input \(x\), \(u\) a guessed word, and \(w\) any choice word with \(|w| = |x\, u| + 2\). Running the host under \(w\) from the guessing-phase configuration for \((d,u)\) installs the verifier-phase configuration for the initial configuration of \(V\) on the assembled word \(x\, u\).

Let \(S, V\) be deterministic machines and suppose \(V\) computes the single-bit output \(b\) on a word \(y\) within \(T\) steps. For every choice word \(w\) with \(|w| = T + 1\), running the host under \(w\) from the verifier-phase start on \(y\) halts with output exactly the one-bit string \(b\).

Let \(S, V\) be deterministic machines, \(d\) a halted scheduler configuration on an input \(x\), \(u\) a guessed word, and suppose \(V\) computes the single-bit output \(b\) on \(x\, u\) within \(T\) steps. Then for every choice word \(w\) with \(|w| = |x\, u| + 2 + (T+1)\), running the host under \(w\) from the guessing-phase configuration for \((d,u)\) halts with output exactly the one-bit string \(b\).

Let \(S\) and \(M\) be deterministic machines, \(V\) a language, and suppose the input-normalized scheduler on an input \(x\) computes a word \(v\) within \(T\) steps while live earlier, and that \(M\) decides \(V\) within time \(A(m+1)^d\) on inputs of length \(m\). Set \(H = 2|x| + 2 + T + (|x| + |v| + 2 + (A\, (|x|+|v|+1)^d + 1))\). Then every choice word of length \(H\) makes the reverse host built from \(S\) and \(M\) halt with output the indicator bit of \(x\, u \in V\) for some guessed word \(u\) of length \(|v|\); and conversely, for every \(u\) of length \(|v|\) some choice word of length \(H\) produces a halted run with output the indicator bit of \(x\, u \in V\).

For all natural numbers \(C, c, B, A, d, n\) and \(T\) with \(T \le B(n+1)^{c+1}\), the total \(2n + 2 + T + (n + C(n+1)^c + 2 + (A\, (n + C(n+1)^c + 1)^d + 1))\) is at most \((B + A + 5)\, (n + C(n+1)^c + 1)^{c+d+1}\).

Let \(L\) be a language over the binary alphabet such that \(x \in L\) exactly when some binary string \(u\) with \(|u| = C\, (|x|+1)^c\) has \(x\, u \in V\), and let \(M\) be a deterministic machine deciding the verifier language \(V\) within time \(A(m+1)^d\). Then there are constants \(K, r\) and a nondeterministic machine deciding \(L\) within time \(K\, (n + C(n+1)^c + 1)^r\).

For all natural numbers \(C\) and \(c\), the map \(n \mapsto n + C \cdot 2^{(n+1)^c}\) on the natural numbers is strictly increasing.

Let \(C, c\) be natural numbers and \(x, u, y, v\) binary strings with \(|u| = C\cdot 2^{(|x|+1)^c}\) and \(|v| = C \cdot 2^{(|y|+1)^c}\). If \(x\, u = y\, v\) as strings, then \(x = y\) and \(u = v\).

For natural numbers \(C, c, m, n\): if the exponential split search at length \(m\) returns \(n\), then \(n \le m\) and \(n + C \cdot 2^{(n+1)^c} = m\).

For natural numbers \(C, c\) and \(m\), the exponential split search at length \(m\) fails if and only if no natural number \(n\) satisfies \(n + C \cdot 2^{(n+1)^c} = m\).

Let \(N\) be a nondeterministic Turing machine over the binary alphabet, \(C, c\) natural numbers, and \(x, u\) binary strings with \(|u| = C \cdot 2^{(|x|+1)^c}\). Then \(x\, u\) lies in the exponential choice-word verifier language of \(N\) with parameters \(C, c\) if and only if the run of \(N\) on \(x\) under \(u\) has halted with output the one-bit string \(1\).

Let \(N\) be a nondeterministic Turing machine and \(C, c\) natural numbers. If the exponential split search fails at the length of a string \(y\), then \(y\) is not in the exponential choice-word verifier language of \(N\) with parameters \(C, c\).

For all natural numbers \(a, c\) and \(n\), the inequality \(a \cdot 2^{n^c} \le a \cdot 2^{(n+1)^c}\) holds.

Let \(N\) be a nondeterministic Turing machine deciding a language \(L\) within time \(a \cdot 2^{n^c}\) on inputs of length \(n\). For every binary string \(x\): \(x \in L\) if and only if there is a string \(u\) with \(|u| = a \cdot 2^{(|x|+1)^c}\) such that \(x\, u\) lies in the exponential choice-word verifier language of \(N\) with parameters \(a, c\).

For natural numbers \(C \ne 0\) and \(p\), the little-endian binary expansion of \(C \cdot 2^p\) equals \(p\) zero bits followed by the binary expansion of \(C\).

For all natural numbers \(C, c, n, m\) with \(n \le m\), the binary expansion of \(C \cdot 2^{(n+1)^c}\) has length at most \((m+1)^c\) plus the length of the binary expansion of \(C\).

For every fixed word \(w\), every input \(x\) and every \(t \le |x|\): after \(t\) steps from the initial configuration, the zero-prefixing emitter for \(w\) is still in its scanner state, its input head is at position \(t + 1\), and its output so far is \(t\) zero bits.

For every fixed word \(w\) and every input \(x\), the zero-prefixing emitter for \(w\) halts within \(|x| + |w| + 2\) steps, and its complete output is the word of \(|x|\) zero bits followed by \(w\).

For every fixed word \(w\), the zero-prefixing emitter computes, on each input \(x\), the word of \(|x|\) zero bits followed by \(w\); its running time is at most the monotone linear budget \((|w|+2)(n+1)\) on inputs of length \(n\).

For all natural numbers \(C\) and \(c\) there exist a deterministic machine and a constant \(A\) computing, on every input \(x\), the little-endian binary expansion of \(C \cdot 2^{(|x|+1)^c}\) within \(A\, (|x|+1)^{c+1}\) steps.

For all natural numbers \(C, c\) and every binary string \(y\), the word emitted by the exponential split emitter on \(y\) has length at most \(2|y| + 2\).

Let \(N\) be a nondeterministic Turing machine and \(C, c\) natural numbers. For every binary string \(y\), the pair-loader machine of \(N\), run on the word emitted by the exponential split emitter for \(y\), halts within \(3(2|y|+3)\) steps, and its output is the indicator bit of membership of \(y\) in the exponential choice-word verifier language of \(N\).

Let \(N\) be a nondeterministic Turing machine and \(C, c\) natural numbers. If some deterministic machine computes the exponential split-emitter function within time \(A(n+1)^{r+1}\) for constants \(A, r\), then the exponential choice-word verifier language of \(N\) with parameters \(C, c\) belongs to \(\mathrm{P}\).

For all words \(w\) and \(s\) with \(|s| \le |w| + 1\), the state produced by one search round still has length at most \(|w| + 1\).

For every word \(w\) and every \(i \le |w| + 1\), iterating the search round \(i\) times from the empty state yields the all-ones word of length \(i\).

Let \(p\) and \(q\) be Boolean predicates that agree on every element of a given list. Then the first element of the list satisfying \(p\) equals the first element satisfying \(q\).

For all natural numbers \(C, c\) and every word \(w\), searching the indices \(i \le |w|\) for the first round state (the \(i\)-fold iterate from the empty state) that passes the round test returns exactly the result of the exponential split search at length \(|w|\).

For natural numbers \(C, c\) and a word \(w\): taking the first accepted index of the bounded orbit search and emitting the encoded pair of the corresponding prefix and suffix of \(w\) (or the empty word when the search is exhausted) yields exactly the word of the exponential split emitter on \(w\).

For all natural numbers \(b, A, r\) and \(n\), the product \(b\, (A(n+1)^{r+1} + 1)(n+2)\) is at most \(2b(A+1)\, (n+1)^{r+2}\).

Fix natural numbers \(C, c\) and suppose a deterministic loop-body machine with a designated anchor state satisfies two timed contracts within \(A(|w|+1)^{r+1}\) steps on every input \(w\): a startup contract that first reaches the anchor with clean scratch, and a round contract that, from any anchored search state, either halts with the encoded pair payload when the round test accepts, or returns to the anchor with the stepped search state. Then some deterministic machine computes the exponential split-emitter function within \(B(n+1)^{r+2}\) steps for a constant \(B\).

For all binary strings \(u, v\) and every index \(j\), the length-\((j+1)\) prefixes of \(u\) and \(v\) agree if and only if their length-\(j\) prefixes agree and their optional bits at index \(j\) agree, a missing bit counting as different from any present bit.

The map sending a natural number to its little-endian binary expansion is injective: two numbers with the same bit list are equal.

For every binary word \(u\), the borrow position of \(u\) is at most \(|u|\).

For every binary word \(u\), the word part of the fixed-width decrement of \(u\) has the same length as \(u\), whether or not the decrement succeeds.

For every natural number \(n\), the little-endian value of the binary expansion of \(n\) equals \(n\).

For every binary word \(u\): if the fixed-width decrement of \(u\) succeeds, the value of the resulting word plus one equals the value of \(u\); if it fails, the value of \(u\) is zero.

For all binary words \(p\) and \(s\), reading the buffer tape holding \(p\, s\) at cell \(|p|\) returns the first bit of \(s\), or blank when \(s\) is empty.

For all binary words \(p\) and \(s\) and all bits \(b, b'\), overwriting cell \(|p|\) of the buffer tape holding \(p\, b\, s\) with the bit \(b'\) yields exactly the buffer tape holding \(p\, b'\, s\).

For every emitted prefix, every input and position, and every counter word split as \(p\, s\): one step of the countdown emitter in the borrow state with work head at cell \(|p|\) clears a leading \(1\) of \(s\) and turns to rewind with success, converts a leading \(0\) of \(s\) to \(1\) and advances, or, at the blank end of the word, turns to rewind with failure; in each case the width is preserved and nothing is emitted.

For every counter word \(u\) and every prefix \(p\): starting in the borrow state with work head at cell \(|p|\) over the word \(p\, u\), exactly \(\beta + 1\) steps of the countdown emitter, where \(\beta \) is the borrow position of \(u\), reach the rewind state carrying the success flag of the decrement of \(u\), with the work tape now holding \(p\) followed by the decremented word.

For every counter word \(u\), every flag \(b\) and every \(j \le |u|\): from the rewind state with work head at cell \(j-1\), exactly \(j+1\) steps of the countdown emitter reach the round-return state carrying \(b\), with head at cell zero and the counter unchanged.

For every counter word \(u\): a full borrow-and-rewind round of the countdown emitter from cell zero costs \(2\beta + 2 \le 2|u| + 2\) steps, where \(\beta \) is the borrow position of \(u\), and ends at cell zero in the round-return state carrying the success flag, with the counter replaced by its fixed-width decrement and no output emitted.

For every input, head position and counter word \(u\) of value \(n\), and every already-emitted word: within \((n+1)(2|u|+3)\) steps from the borrow state at cell zero, the countdown emitter halts with output equal to the already-emitted word followed by exactly \(n\) ones.

For every input \(x\) and every index \(i \lt |x|\), one step of the countdown emitter from the copy configuration holding the first \(i\) bits of \(x\) appends the bit at index \(i\) to the work tape and advances both heads, emitting nothing.

For every input \(x\) and every \(i \le |x|\), the \(i\)-step run of the countdown emitter from its blank-tape initial configuration is the copy configuration holding the first \(i\) bits of \(x\) with input head at position \(i+1\).

For every input position, every counter word \(u\) and every \(j \le |u|\): from the startup-rewind configuration with work head at cell \(j-1\), exactly \(j+1\) steps of the countdown emitter reach the borrow state at cell zero with counter \(u\) and empty output.

For every input \(x\), the \((2|x| + 2)\)-step run of the countdown emitter from its blank-tape initial configuration is the borrow-state configuration at cell zero with the full input \(x\) as counter, input head at the right boundary and empty output.

For every binary input \(x\), the countdown emitter computes the all-ones word whose length is the little-endian value \(v\) of \(x\), within \(2|x| + 2 + (v+1)(2|x|+3)\) steps.

For all natural numbers \(C\) and \(c\) there exist a deterministic machine \(S\) and a constant \(B\) such that on every input \(x\), \(S\) outputs the all-ones word of length \(C \cdot 2^{(|x|+1)^c}\) within \(B\, (|x| + C\cdot 2^{(|x|+1)^c} + 1)^{c+2}\) steps.

For all natural numbers \(Q, B, r, A, d, n\) and \(T\) with \(T \le B(n+Q+1)^r\): the total \(2n + 2 + T + (n + Q + 2 + (A(n+Q+1)^d + 1))\) is at most \((B+A+5)(n+Q+1)^{r+d+1}\).

Let \(L\) be a language over the binary alphabet such that \(x \in L\) exactly when some binary string \(u\) with \(|u| = C \cdot 2^{(|x|+1)^c}\) has \(x\, u \in V\), and let \(M\) be a deterministic machine deciding the verifier language \(V\) within \(A(m+1)^d\). Then there are constants \(K, r\) and a nondeterministic machine deciding \(L\) within \(K\, (n + C\cdot 2^{(n+1)^c} + 1)^r\).

For all natural numbers \(K\) and \(k\) there exist constants \(A\) and \(e\) such that \(2^{K(n+1)^k} \le A \cdot 2^{n^e}\) for every natural number \(n\).

For all natural numbers \(C, c, K, r\) there exist constants \(A\) and \(e\) with \(K\, (n + C\cdot 2^{(n+1)^c} + 1)^r \le A \cdot 2^{n^e}\) for every natural number \(n\).

Let \(L\) be a language over the binary alphabet and \(C, c\) natural numbers. If some nondeterministic machine decides \(L\) within time \(K(n + C\cdot 2^{(n+1)^c} + 1)^r\) for constants \(K, r\), then \(L\) belongs to \(\bigcup _e \mathrm{NTIME}(2^{n^e})\).

Let \(f\) be a function on binary strings. If some deterministic machine computes \(f\) within a budget \(a(n+1)\) on inputs of length \(n\), for a constant \(a\), then \(f\) is polynomial-time computable.

For every fixed binary word \(w\), the constant function sending every input to \(w\) is polynomial-time computable.

Let \(p\) be a Boolean test whose single-bit indicator is polynomial-time computable, and let \(f\) and \(g\) be polynomial-time computable functions on binary strings. Then the function that returns \(f(x)\) when \(p(x)\) holds and \(g(x)\) otherwise is polynomial-time computable.

Let \(g\) be a polynomial-time computable function on binary strings. Then the function that decodes its input as a pair \((a,b)\) and re-encodes the pair \((a, g(b))\), returning the empty word on malformed input, is polynomial-time computable.

Let \(f\) and \(g\) be polynomial-time computable functions on binary strings. Then the function sending \(x\) to the self-delimiting encoding of the pair \((f(x), g(x))\) is polynomial-time computable.

Let \(F\) and \(G\) be deterministic machines, and suppose \(F\) computes \(y\) from \(x\) within \(s\) steps and \(G\) computes \(z\) from \(y\) within \(t\) steps. Then the buffered composition of \(F\) and \(G\) computes \(z\) from \(x\) within \(s + |y| + 2 + t\) steps.

Suppose the comparator input has the form \(y = p\, b\, b\, r\) for a bit \(b\) and words \(p, r\). From the parser state at position \(|p|+1\) with decoded word \(u\), exactly two steps of the pair comparator append \(b\) to the work tape and move to position \(|p|+3\), emitting nothing.

Suppose the comparator input has the form \(y = p\, 0\, 1\, v\) for words \(p, v\). From the parser state at position \(|p|+1\) with decoded word \(u\), exactly two steps of the pair comparator enter the rewind state at position \(|p|+3\), with the work tape and output untouched and the work head moved one cell left.

Suppose the comparator input has the form \(y = p\, e\) where \(e\) is the self-delimiting encoding of a pair \((u, v)\). From the parser state at position \(|p|+1\) with decoded word \(a\), exactly \(2|u|+2\) steps of the pair comparator reach the rewind state at position \(|p|+2|u|+3\) with decoded word \(a\, u\).

For every input, every decoded word \(u\), every position and every \(j \le |u|\): from the rewind state with work head at cell \(j - 1\), exactly \(j+1\) steps of the pair comparator reach the comparison state with work head at cell zero and all data unchanged.