For every boolean word \(u\), the little-endian value of \(u\) is strictly less than \(2^{|u|}\).

For all \(w\) and \(i\), the width-\(w\) little-endian binary word of \(i\) has length exactly \(w\).

For every width \(w\), the width-\(w\) little-endian binary word of \(0\) is the all-false word of length \(w\).

If \(i \lt 2^w\), then the little-endian value of the width-\(w\) binary word of \(i\) equals \(i\).

Two boolean words of the same length with the same little-endian value are equal (trailing high-order false bits included).

Every boolean word \(u\) equals the width-\(|u|\) little-endian binary word of its own little-endian value.

For every boolean word \(u\): if the fixed-width increment of \(u\) succeeds with result \(v\), then \(|v| = |u|\) and the little-endian value of \(v\) is one more than that of \(u\); if it overflows, then the value of \(u\) plus one equals \(2^{|u|}\).

For \(i \lt 2^w\), the fixed-width increment of the width-\(w\) binary word of \(i\) equals the width-\(w\) word of \(i+1\) when \(i + 1 \lt 2^w\), and reports overflow otherwise. This includes width zero.

For every width \(w\) and every predicate \(p\) on boolean words: there exists a word \(u\) with \(|u| = w\) satisfying \(p\) if and only if there exists a rank \(i \lt 2^w\) such that \(p\) holds of the width-\(w\) binary word of \(i\).

Testing \(\mathrm{count}\) consecutive ranks starting at \(i\) against an acceptance function returns true if and only if some rank \(j\) with \(i \le j \lt i + \mathrm{count}\) accepts.

Let \(V\) be a language over the binary alphabet, \(x\) a string, and \(w\) a width. Testing all \(2^w\) ranks with the acceptance function “the indicator of \(V\) accepts \(x\) concatenated with the width-\(w\) binary word of the rank” returns true if and only if there exists \(u\) with \(|u| = w\) and \(x \mathbin {+\! \! +} u \in V\).

Let \(M\) be a finite multi-tape Turing machine over the binary alphabet, \(x\) an input, and let \(\mathrm{cfg}\) assign to each rank a configuration of \(M\) on \(x\). Suppose the configuration at rank \(i + \mathrm{count}\) is halted with single-bit output false, and that for each rank \(j\) with \(i \le j \lt i + \mathrm{count}\) the machine, within \(B\) steps from \(\mathrm{cfg}(j)\), either halts with single-bit output true (when rank \(j\) accepts) or reaches \(\mathrm{cfg}(j+1)\) (when it rejects). Then within \(\mathrm{count} \cdot B\) steps from \(\mathrm{cfg}(i)\) the machine halts with single-bit output equal to the disjunction of the acceptance bits over the ranks \(i \le j \lt i + \mathrm{count}\).

For all constants \(K, k \in \mathbb {N}\) there exist constants \(A, e \in \mathbb {N}\) such that \(2^{K (n+1)^k} \le A \cdot 2^{n^e}\) for every \(n\).

For all constants \(a, C, c, d \in \mathbb {N}\) there exist \(A, e \in \mathbb {N}\) such that for every \(n\),

For every boolean word \(s\), the fixed-width little-endian binary increment of \(s\) computed by the Turing-machine catalog’s counter equals the one computed by the certificate-enumeration counter: both return the same-length incremented word, or both fail exactly on overflow (including on the empty word).

For every boolean word \(s\), applying the fixed-width increment and falling back to \(s\) itself on overflow yields a word whose length is exactly \(|s|\).

For every width \(w\) and every \(i \lt 2^w\), iterating the stalled fixed-width increment (increment, keeping the word unchanged on overflow) \(i\) times from the all-false word of length \(w\) yields the width-\(w\) little-endian binary word of \(i\). Nothing is asserted at the terminal rank \(2^w\).

For every \(w\), the binary-digit list of \(2^w - 1\) is the all-true word of length \(w\).

Appending one possibly blank entry to a finite cell list changes the induced sparse tape at exactly the position just past the old list, where the new entry is written.

Let \(w\) be a finite list of possibly blank cells and \(b\) a possibly blank entry. Blanking position \(|w|\) of the sparse tape of \(w\) extended by \(b\) yields exactly the sparse tape of \(w\); this holds even when \(b\) is itself blank.

For every head move \(d\), encoding \(d\) as a tape symbol and decoding the inverse move yields exactly the negation of \(d\)’s integer head displacement.

For any configuration \(c\) with history \(h\) and any action \(a\) of the source machine: applying the logged version of \(a\) to the logged configuration of \(c\) with history \(h\) yields the logged configuration of \(a\) applied to \(c\), with history \(h\) extended by the single entry recording the overwritten symbols and head moves of \(a\). This includes halting and output-emitting actions.

For every finite machine \(M\), start configuration \(c_0\) (possibly prepared, not necessarily initial), and time \(t\): running the logging machine of \(M\) for \(t\) steps from the logged configuration of \(c_0\) with empty history yields the logged configuration of \(M\)’s time-\(t\) configuration together with the history of the first \(t\) steps. In particular the source’s input, output, and halting time are unchanged by the instrumentation.

For any configuration \(c\), action \(a\), and work-tape index \(i\): writing the symbol that was under head \(i\) in \(c\), at \(c\)’s head position, into tape \(i\) after \(a\) has been applied restores tape \(i\) exactly to its contents in \(c\). This covers no-write actions and writes of the blank symbol.

For every \(n\), blanking cell \(n\) of the buffer tape holding \(n + 1\) consecutive true marks yields the buffer tape holding \(n\) consecutive true marks.

Let \(c\) be a source configuration, \(a\) an action, \(h\) a history list, and \(p\) an input-head position. One step of the restoration machine from the checkpoint at \(p\) for the configuration obtained by applying \(a\) to \(c\), whose history is \(h\) extended by the entry recording \(a\) (the symbols under the work heads of \(c\) and the head moves of \(a\)), equals the mid-restoration configuration for \(c\), \(a\), \(h\) and \(p\): the recorded head moves are reversed, the overwritten symbols are retained in finite control, and the cells of that history entry are erased.

Let \(c\) be a source configuration, \(a\) an action, \(h\) a history list, and \(p\) an input-head position. One step of the restoration machine from the mid-restoration configuration for \(c\), \(a\), \(h\) and \(p\) equals the checkpoint configuration for \(c\) and \(h\) at \(p\): the retained old symbols are written back, restoring the source tapes to their contents in \(c\), and the history heads move back onto the last entry of \(h\).

With no history left, one silent step of the restoration machine from the checkpoint for a source configuration \(c\) with empty history returns the history heads to zero and halts, reaching the completed restoration configuration for \(c\). This also covers a source run of zero steps.

Let \(M\) be a finite machine that is live (not halted) at every time before \(t\) when run from \(c_0\). Then the restoration machine, started at the checkpoint for \(M\)’s time-\(t\) configuration with the \(t\)-step history, reaches the completed restoration configuration of \(c_0\) — original work tapes and head positions, blank history — in exactly \(2t + 1\) steps, preserving any supplied input-head position.

If a machine’s run from \(c_0\) is halted at time \(T\), then there is a time \(t \le T\) at which it halts for the first time: the machine is live at every time before \(t\), and its configuration at time \(t\) equals its configuration at time \(T\).

If a source machine \(M\) is live for \(t\) steps from a configuration \(c_0\), then the clean wrapper of \(M\), run for \(t\) steps from the captured logged start of \(c_0\), reaches the captured logged configuration of \(M\)’s time-\(t\) configuration with the \(t\)-step history; any halting emission of \(M\) is retained on the capture tape.

If the source configuration \(c\) is halted, then one silent step of the clean wrapper from the captured logged configuration of \(c\) with history \(h\) parks every history head on the last entry and enters the captured restoration phase at the checkpoint for \(c\) and \(h\), retaining \(c\)’s output on the capture tape.

If the source \(M\) is live for \(t\) steps from \(c_0\), then within \(2t + 1\) steps the clean wrapper’s captured restoration, started at the checkpoint of the time-\(t\) configuration with its history, reaches the administrative configuration in which the original source work fields of \(c_0\) are restored, the time-\(t\) output is retained on the last tape, and the capture head stands at the end of that word.

For any displacements \(m, d\) and control states \(q, q'\), applying the two-head administrative action with displacements \(m, d\) and next state \(q'\) to an administrative configuration of the clean wrapper in state \(q\) yields the administrative configuration with the same tapes, retained word and empty output, in state \(q'\), with the native input head moved by \(m\) and the capture head moved by \(d\).

Consider a machine with a start state whose transition unconditionally steps the input head left into a scanning state, and a scanning state that keeps stepping left over input symbols and exits right into a destination state at the left blank. Then from any configuration in the start state there is a number of steps, at most the current input position plus \(2\), after which the configuration equals the original one with control transferred to the destination state and the input head at cell one.

For every \(j \le |y|\): from the administrative configuration of the clean wrapper with retained word \(y\) and capture head just left of cell \(j\), exactly \(j + 1\) steps return the capture head to zero without erasing \(y\), advancing control to the final administrative state.

If a machine \(M\) halts within \(T\) steps from configuration \(c_0\) on input \(x\) with output \(y\), then within \(3T + |x| + |y| + 8\) steps the clean wrapper of \(M\), started at the captured logged start of \(c_0\), halts in the administrative configuration with \(c_0\)’s work fields restored, all histories blank, \(y\) retained on the last tape, the input head at cell one, the capture head at zero, and no physical output.

Suppose the input \(x\) decomposes as \(\mathit{pre} \mathbin {+\! \! +} \mathit{rest}\), and let \(s\) be a candidate word. After exactly \(|\mathit{rest}| + 1\) steps from the input-phase configuration of the assembly machine with the input head on the first symbol of \(\mathit{rest}\), candidate \(s\) with its head at zero, and output \(\mathit{pre}\), the machine is in the candidate phase with the input head at the right boundary, the candidate tape and its head at zero unchanged, and output \(x\).

Suppose the candidate word \(s\) decomposes as \(\mathit{pre} \mathbin {+\! \! +} \mathit{rest}\), and let \(\mathit{out}\) be a word and \(p\) an input-head position. After exactly \(|\mathit{rest}| + 1\) steps from the candidate-phase configuration of the assembly machine with input head at \(p\), candidate head at position \(|\mathit{pre}|\), and output \(\mathit{out} \mathbin {+\! \! +} \mathit{pre}\), the machine is halted with the candidate tape unchanged, its head at position \(|s|\), the input head still at \(p\), and output \(\mathit{out} \mathbin {+\! \! +} s\); an empty remainder takes the single final step.

For all binary words \(x\) and \(s\), the assembly machine started in its input phase on input \(x\), with \(s\) on its work tape and all heads at their starting positions, is halted after exactly \(|x| + |s| + 2\) steps with output \(x \mathbin {+\! \! +} s\), its input head at the right boundary, the candidate tape unchanged, and the candidate head at position \(|s|\).

Let \(M_1, M_2\) be finite machines, and let \(c_0\) be a configuration of \(M_1\) on input \(x\) (not necessarily initial) from which \(M_1\) halts within \(T_1\) steps with output \(y\); suppose \(M_2\) computes \(z\) from input \(y\) within \(T_2\) steps. Then the buffered composition of \(M_1\) and \(M_2\), started at its first-phase configuration for \(c_0\), halts within \(T_1 + |y| + 2 + T_2\) steps with output \(z\).

For any verifier machine \(MV\), words \(x, s\), and assembly phase: the buffered composition’s first-phase configuration over the assembly machine prepared with candidate \(s\) equals the canonical configuration in which control sits in the chosen assembly phase, tape zero carries \(s\), and all other tapes (composition buffer and verifier work) are blank.

If a machine \(MV\) decides a language \(V\) within time \(T_v\), then from the canonical candidate seam with candidate \(s\) on input \(x\), the buffered composition of the assembly machine with \(MV\) halts within \(T_v(|x| + |s|) + 2(|x| + |s|) + 4\) steps, with single-bit output the indicator of \(x \mathbin {+\! \! +} s \in V\).

Suppose a host machine’s transitions on embedded states are the halt-redirected transitions of a source machine, and the source is live at every time before \(t\) when run from \(c_0\). Then the host’s \(t\)-step run from the redirected configuration of \(c_0\) equals the redirected configuration of the source’s time-\(t\) configuration; in particular at the first halt the host lands in the return state with the source’s final writes and output.

Applying the padded version of an action to the padded version of a configuration equals the padding of the result of applying the original action; the added high tapes remain blank.

Let \(k \le K\) and suppose a host machine’s transitions on embedded states are the padded transitions of a \(k\)-tape source machine, reading only the first \(k\) tapes. Then for every configuration \(c\) of the source and every time \(t\), the host’s run from the padded configuration of \(c\) equals the padding of the source’s run.

Suppose a machine \(I\) computes, within time \(j(n+1)\) on inputs of length \(n\), the output word of the fixed-width binary increment (the successor word, or the empty word on overflow). Then from the candidate seam in the candidate phase with candidate \(s\) on input \(x\), the buffered composition of the assembly machine with \(I\) halts within \((j+3)(|s|+1)\) steps and outputs the increment result of \(s\), which is empty exactly on overflow.

For \(0 \lt k \le K\): padding the canonical configuration whose only nonblank tape is tape zero carrying a word \(s\) from a \(k\)-tape bank to a \(K\)-tape bank yields the canonical configuration with \(s\) on tape zero of the larger bank, all added tapes blank and parked at zero.

Padding the initial (all-blank-work) configuration of a \(k\)-tape machine yields the canonical configuration with an empty tape-zero word on the larger bank; this holds even when the source machine has no work tapes.

Writing a bit at position \(|\mathit{pre}|\) of the buffer tape holding \(\mathit{pre} \mathbin {+\! \! +} \mathit{old}\) yields the buffer tape holding \(\mathit{pre}\), then that bit, then the tail of \(\mathit{old}\) with its first cell dropped; this includes the case of an empty \(\mathit{old}\).

For every \(p\), every bit \(b\), and every boolean word \(\mathit{rest}\), blanking position \(p\) of the sparse tape consisting of \(p\) blank cells followed by the symbols of the word \(b\) then \(\mathit{rest}\) yields the sparse tape of \(p + 1\) blank cells followed by the symbols of \(\mathit{rest}\).

Let \(L \gt 0\), and consider a two-ended configuration on \(L + 1\) work tapes whose tape zero holds \(u\) and whose last tape holds \(v\), with common head position \(h\). Applying the two-ended action with optional writes \(a\), \(b\), displacement \(d\) and next state \(q'\) yields the two-ended configuration in state \(q'\) whose tape zero is \(u\) with cell \(h\) overwritten by \(a\) (if \(a\) writes), whose last tape is \(v\) with cell \(h\) overwritten by \(b\) (if \(b\) writes), and whose common head position is \(h + d\); the input head and the empty output are unchanged.

The sparse tape induced by a list of \(n\) blank entries is blank at every position.

The sparse tape induced by lifting every symbol of a boolean word into a nonblank cell equals the standard buffer tape of that word.

Consider a machine with at least two work tapes whose copy state, at a two-ended configuration, overwrites the tape-zero cell with \(f\) applied to the captured symbol, blanks the captured cell, and advances both heads, exiting left into a rewind state at the captured right blank. Starting with tape zero holding \(\mathit{pre} \mathbin {+\! \! +} \mathit{old}\), the capture tape holding \(\mathit{rest}\) beyond \(|\mathit{pre}|\) already-erased cells, and both heads at \(|\mathit{pre}|\): after \(|\mathit{rest}| + 1\) steps the machine is in the rewind state, tape zero holds \(\mathit{pre}\), then \(f\) mapped over \(\mathit{rest}\), then the remainder of \(\mathit{old}\) beyond position \(|\mathit{rest}|\), the capture tape is blank, and both heads stand at \(|\mathit{pre}| + |\mathit{rest}| - 1\).

Consider a machine whose rewind state moves both endpoint heads left while the tape-zero cell is nonblank and exits right into an arrival state at the left blank. For every word \(w\) on tape zero and every \(j \le |w|\): from common head position \(j - 1\), exactly \(j + 1\) steps reach the arrival state with both heads at zero, preserving \(w\) and the blank capture tape.

For a machine with copy and rewind states as in the two preceding scans: if the captured word \(v\) is at least as long as the old tape-zero word, then from a two-ended configuration with both heads at zero, exactly \(2|v| + 2\) steps replace tape zero entirely by \(f\) mapped over \(v\), blank the capture tape, and return both heads to zero in the arrival state.

For a machine \(B\) with at least one work tape: the logged configuration, with empty history, of the canonical seam carrying a word \(s\) on tape zero equals the canonical seam of the logging machine’s larger tape bank, the added tapes being blank and stationary.

Appending one tape holding a word \(y\) to a bank of \(L\) tapes whose only nonblank tape is tape zero holding \(s\) yields exactly the two-ended tape layout: tape zero \(s\), last tape \(y\), all intervening tapes blank.

For a machine \(B\) with at least one work tape: the clean wrapper’s captured entry configuration at the prepared seam carrying \(s\) on tape zero equals the two-ended administrative configuration with tape zero \(s\), blank capture, and both endpoint heads at zero.

For a machine \(B\) with at least one work tape: the clean wrapper’s completed administrative configuration over the prepared seam carrying \(s\), with retained output \(y\), equals the two-ended configuration with tape zero \(s\), capture tape \(y\), and both endpoint heads at zero.

Let \(B\) be a source machine with at least one work tape that, started in state \(q\) at the seam carrying candidate \(s\) on input \(x\), halts within \(T\) steps with output \(y\). Then the enumerator body, from the two-ended configuration embedding the clean call of \(q\) in a given mode, reaches within \(3T + |x| + |y| + 8\) steps the two-ended configuration in that mode’s administrative continuation state, with candidate \(s\) preserved, \(y\) on the capture tape, all scratch blank, both endpoint heads at zero, and empty physical output.

The two-ended administrative configuration with tape zero holding \(s\), blank capture tape, and both endpoint heads at zero equals the canonical seam configuration carrying \(s\) on tape zero.

Let \(B\) be a source machine with at least one work tape that, started at the empty seam on input \(x\), halts within \(T\) steps emitting \(w\) consecutive true marks. Then within \(3T + |x| + 3w + 10\) steps from its initial configuration on \(x\), the enumerator body reaches the anchor state over the canonical seam carrying the all-false candidate of width \(w\).

For every input \(x\) and candidate word \(s\), one step of the active enumerator body from the anchor state over the canonical seam carrying \(s\) on tape zero yields the two-ended configuration that enters the verification call (the source’s verifier entry state in verification mode), with tape zero \(s\), a blank capture tape, and both endpoint heads at zero; the step writes nothing, moves no head, and emits nothing.

For every candidate word \(s\), after one step of the enumerator body (active or stopped) from the two-ended configuration in the verdict state with tape zero \(s\) and the captured word consisting of a single true bit, the machine is halted and its output is exactly the single bit true.

For every candidate word \(s\), one step of the enumerator body (active or stopped) from the two-ended configuration in the verdict state with tape zero \(s\) and a captured single false bit yields the two-ended configuration that enters the increment call (the source’s increment entry state in increment mode), with tape zero \(s\), the captured verdict erased so that the capture tape is blank, and both endpoint heads at zero.

For every boolean word \(s\), exactly one of the following holds for the fixed-width increment’s output word: it is empty (overflow) and the stalled step leaves \(s\) unchanged; or it is nonempty, has length exactly \(|s|\), and the stalled step equals it.

One step of the enumerator body from the increment-check state, at the two-ended configuration with candidate \(s\) and captured increment result \(v\), preserves all tapes and transfers control to the anchor when \(v\) is empty (overflow) and to the result-copy state otherwise.

Let \(B\) be a source machine with at least one work tape that, started in the increment entry state at the seam with candidate \(s\), halts within \(T\) steps emitting the fixed-width increment’s output word. Then the enumerator body, from the two-ended configuration embedding the increment call, reaches within \(3T + |x| + 3|s| + 11\) steps the anchor over the seam carrying the stalled increment of \(s\): the successor word of the same width, or \(s\) itself on overflow.

Let \(B\) be a source machine with at least one work tape whose verification call on candidate \(s\) (from the verifier entry state at the seam) halts within \(T_v\) steps with single-bit output \(b\), and whose increment call halts within \(T_i\) steps emitting the fixed-width increment output. Then from the configuration just after departure, within \(3T_v + 3T_i + 2|x| + 3|s| + 21\) steps the enumerator body either halts with output true (when \(b\) is true) or reaches the anchor over the seam carrying the stalled increment of \(s\) (when \(b\) is false).

If a control state’s transition is the silent stationary self-loop, then from any configuration in that state, a run of any length leaves the configuration unchanged.

If two transition tables agree at every control state other than a designated anchor state, then their runs from a common configuration coincide for every duration during which the second machine’s run has not yet visited the anchor.

Let two transition tables agree away from an anchor state, which the second (stopped) table turns into a silent self-loop. If the stopped run from \(c\) stands at the anchor at time \(T\), then there is a time \(t \le T\) such that the active run never visits the anchor before \(t\) and its time-\(t\) configuration equals the stopped run’s time-\(T\) configuration.

Let two transition tables agree away from an anchor state, which the second (stopped) table turns into a silent self-loop. If the stopped run from \(c\) is halted at time \(T\), then the active run from \(c\) equals the stopped run at time \(T\), and the active run never visits the anchor at any time up to \(T\).

The active and stopped variants of the enumerator body have identical transitions at every control state other than the anchor; their tape counts and finite state sets coincide.

Let \(B\) be a source machine with at least one work tape that, from the empty seam on input \(x\), halts within \(T\) steps emitting \(w\) true marks. Then within \(3T + |x| + 3w + 10\) steps the active enumerator body reaches the anchor over the all-false width-\(w\) candidate seam, without visiting the anchor at any earlier time.

Let \(B\) be a source machine with at least one work tape whose verification call on candidate \(s\) halts within \(T_v\) steps with single-bit verdict \(b\), and whose increment call halts within \(T_i\) steps emitting the fixed-width increment output. Then there is a time \(t\) with \(0 \lt t \le 3T_v + 3T_i + 2|x| + 3|s| + 22\) such that the active enumerator body, started at the anchor over the seam with candidate \(s\), does not visit the anchor at any strictly intermediate positive time, and at time \(t\) either halts with output true (when \(b\) is true) or stands at the anchor over the seam carrying the stalled increment of \(s\) (when \(b\) is false).

Suppose a host machine simulates a source machine with at least one work tape by padded transitions on an initial tape block. If the source, started in state \(q\) at the seam carrying \(s\), is halted at time \(T\) with output \(y\), then the host, started in the embedded state at its own seam carrying \(s\), is halted at time \(T\) with the same output \(y\).

Suppose a host machine simulates a source machine by padded transitions on an initial tape block. If the source computes \(y\) from input \(x\) within \(T\) steps, then the host, started in the embedded initial state at the empty seam on \(x\), is halted at time \(T\) with output \(y\); this holds even for a source with no work tapes.

Fix constants \(C, c\), a budget function \(G\), a language \(V\) over the binary alphabet, and a finite machine (the body) with a designated anchor state satisfying: (i) from its initial configuration on any input \(x\) it reaches, within \(G(|x|)\) steps and with no earlier anchor visit, the anchor over the seam carrying the all-false candidate of width \(w = C(|x|+1)^c\); and (ii) from the anchor over any candidate \(s\) of width \(w\), within some positive time at most \(G(|x|)\) and with no interior anchor visit, it halts with output true when \(x \mathbin {+\! \! +} s \in V\) and otherwise returns to the anchor over the stalled fixed-width increment of \(s\). Then there exist a constant \(b\) and a machine \(E\) such that for every input \(x\) there is a rank-indexed family of configurations with: \(E\) reaches the rank-\(0\) configuration from its initial configuration within \(b(G(|x|) + (|x|+1)^{c+1} + 1)\) steps; the rank-\(2^w\) configuration is halted with single-bit output false; and from each rank \(i \lt 2^w\), within the same budget, \(E\) either halts with output true (when \(x\) concatenated with the width-\(w\) binary word of \(i\) lies in \(V\)) or reaches rank \(i + 1\).

For every \(C \neq 0\) and every \(p\), the binary-digit list of \(C \cdot 2^p\) consists of \(p\) false bits followed by the binary digits of \(C\).

For every \(t \le |x|\): after \(t\) steps on input \(x\), the shift machine is still in its scanning state, its input head stands at position \(t + 1\), and its output so far is exactly \(t\) false bits.

For every suffix word \(w\) and every input \(x\), the shift machine for \(w\) halts on input \(x\) within \(|x| + |w| + 2\) steps, and its output is \(|x|\) false bits followed by \(w\).

For every word \(w\), the shift machine for \(w\) computes the function mapping each input \(x\) to \(0^{|x|} \mathbin {+\! \! +} w\) within time \((|w| + 2)(n + 1)\) on inputs of length \(n\); this time bound is monotone and linear in \(n\).

For all constants \(C, c\) there exist a finite machine and a constant \(A\) such that the machine computes, from each input \(x\), the binary-digit list of \(C \cdot 2^{(|x|+1)^c}\) within time \(A (|x| + 1)^{c+1}\).

For every \(i \lt |x|\), one step of the decider wrapper in its copy phase, with the first \(i\) input bits already on tape zero, appends the \((i+1)\)-st input bit to tape zero and advances both the input head and the tape-zero head by one.

For every \(i \le |x|\), running the decider wrapper for \(i\) steps from its initial configuration on \(x\) reaches the copy-phase configuration with the first \(i\) input bits on tape zero and both active heads just past them.

For every \(j \le |x|\): from the rewind-phase configuration of the decider wrapper with the full copy of \(x\) on tape zero and both active heads just left of cell \(j\), exactly \(j + 1\) steps reach the dispatch seam — the dispatch state over \(x\) on tape zero with all heads at the origin. This includes the empty input.

Let \(C\) be a finite machine with at least one work tape and designated entry and exit states, and let \(x\) be an input. After exactly \(2|x| + 2\) steps from its initial configuration on \(x\), the decider wrapper of \(C\) is in the dispatch seam configuration: the dispatch state, \(x\) on tape zero, every other work tape blank, and all heads at their starting positions.

As long as the inner machine’s run from a configuration has not reached the designated exit state, the decider wrapper’s run from the state-renamed copy of that configuration coincides, under the renaming, with the inner machine’s run.

Suppose the inner machine, started in its entry state at the seam carrying \(x\) on tape zero, first reaches the exit state at a positive time \(t\) (no visit at any earlier positive time), in the canonical configuration carrying a word \(y\) on tape zero. Then the decider wrapper, from its dispatch seam, reaches the renamed exit configuration in exactly \(t\) steps; this covers the case where the entry and exit states coincide.

Suppose the inner machine, started in its entry state at the seam carrying \(x\), first returns to the exit state at a positive time \(t\) with the singleton word \([b]\) on tape zero. Then the decider wrapper computes the output \([b]\) from input \(x\) within \(2|x| + 2 + t + 1\) steps, with no earlier emission.

If a finite machine \(M\) decides a language \(L\) over the binary alphabet within time \(T\), then there exist a finite machine \(R\) and a constant \(B\) such that \(R\) decides \(L\) within time \(B\, (T(n) + n + 2)\).

If a machine \(F\) computes \(y\) from \(x\) within \(s\) steps and a machine \(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.

After the nonempty guard has been passed, the guarded machine’s run from any state-renamed configuration of \(M\) coincides, under the renaming, with \(M\)’s own run.

For every finite machine \(M\), the nonempty-input guard of \(M\), run on the empty input, is halted after one step with output exactly the single bit false.

If \(x\) is nonempty and \(M\) computes \(y\) from \(x\) within \(t\) steps, then the guarded machine computes \(y\) from \(x\) within \(t + 1\) steps.

For all constants \(C, c\), the map \(n \mapsto n + C \cdot 2^{(n+1)^c}\) on the natural numbers is strictly increasing; in particular the exponential split of a padded length, when it exists, is unique. This includes coefficient zero and degree zero.

If the exponential-split search on \((C, c, m)\) returns \(n\), then \(n \le m\) and \(n + C \cdot 2^{(n+1)^c} = m\).

The exponential-split search on \((C, c, m)\) fails if and only if no natural number \(n\) satisfies \(n + C \cdot 2^{(n+1)^c} = m\).

If \(n + C \cdot 2^{(n+1)^c} = m\), then the exponential-split search on \((C, c, m)\) returns exactly \(n\).

For every positive coefficient \(C\) and every degree \(c\), the exponential-split search on \((C, c, 0)\) returns the failure value, so length zero admits no exponential split.

For every word \(y\), the emitted split word for \(y\) has length at most \(2|y| + 2\), including on malformed (unsplittable) inputs.

For all constants \(C, c\) there exist a finite machine and a constant \(A\) computing the split-word function (the paired prefix/suffix encoding, or the empty failure word) within time \(A (n + 1)^{c+2}\) on inputs of length \(n\).

If \(|u| = 2^{(|x|+1)^c}\), then the concatenation \(x \mathbin {+\! \! +} u\) belongs to the padding verifier of \(L\) at degree \(c\) if and only if \(x \in L\).

If the exponential-split search with coefficient one returns \(n\) on a length \(m\), then \(a \cdot 2^{n^c} \le a \cdot m\) for every constant \(a\), including degree zero.

If some finite machine decides a language \(L\) over the binary alphabet within time \(a \cdot 2^{n^c}\), then the padding verifier of \(L\) at degree \(c\) belongs to \(\mathrm{P}\).