The unary reader on Boolean strings — the partial function that consumes a maximal leading block of true bits together with the terminating false bit and returns the pair consisting of the block’s length and the unconsumed suffix, undefined when the string contains no false bit — is primitive recursive.

The two-argument operation taking a Boolean bit \(b\) and a natural number \(n\) to \(2n + b\), i.e. appending \(b\) as a new least-significant binary digit, is primitive recursive.

The function evaluating a Boolean string as a natural number written with the least-significant bit first (the fold of the bit-append operation \((b, n) \mapsto 2n + b\) over the string, starting from \(0\)) is primitive recursive.

The aligned pair parser is primitive recursive. This parser reads a Boolean string in aligned two-bit blocks: the blocks \(00\) and \(11\) contribute the data bits false and true, the first aligned block \(01\) acts as separator, and any other block (or a missing separator) is rejected; on success it returns the decoded first component together with the suffix following the separator.

The function assigning to each natural number the list of its binary digits, least-significant bit first (the number \(0\) having the empty digit list), is primitive recursive.

For every fixed test \(v\) on pairs of Booleans, the skipping reader that consumes the first two bits \(a, b\) of a Boolean string and returns the remaining suffix when \(v(a, b)\) holds — rejecting otherwise, and rejecting strings with fewer than two bits — is primitive recursive.

The two-argument skipping reader that, given a bound \(n\) and a Boolean string, consumes a unary-encoded index (a block of true bits closed by a false bit) and returns the unconsumed suffix precisely when the index is smaller than \(n\), is primitive recursive jointly in \(n\) and the string.

The two-argument skipping reader for a halt-or-successor field is primitive recursive jointly in the bound and the string. This reader consumes one tag bit; on a true tag it further consumes a unary index checked to be smaller than the bound, and on a false tag it returns the rest of the string unchanged.

The two-argument skipping reader for one five-field transition record is primitive recursive jointly in the state bound \(n\) and the string. The record consists of four two-bit fields — the first, third, and fourth checked against a reserved block, the second unconstrained — followed by a halt-or-successor field whose unary index must be smaller than \(n + 1\).

Let \(r\) be a partial reader on Boolean strings (returning either a suffix or failure), let \(n \in \mathbb {N}\), and let \(xs\) be a Boolean string. Applying \(r\) sequentially \(n\) times starting from \(xs\), threading each returned suffix into the next application and failing as soon as one application fails, gives the same result as the \(n\)-th iterate — evaluated at \(xs\) — of the total map on optional strings that feeds a present value to \(r\) and propagates failure.

Let \(A\) be a type with a primitive recursive coding, let \(r\) assign to each \(a \in A\) a partial reader on Boolean strings, primitive recursively jointly in \(a\) and the string, and let \(\mathrm{count} \colon A \to \mathbb {N}\) be primitive recursive. Then the function taking \(a\) and a string to the result of applying the reader \(r(a)\) sequentially \(\mathrm{count}(a)\) times is primitive recursive jointly in \(a\) and the string.

The Boolean-valued function testing whether every entry of a Boolean string is true is primitive recursive.

The erased machine-code parser is primitive recursive. On a Boolean string this parser recovers a state count \(n\) from the aligned doubled-bit region, rejects unless those bits are exactly the canonical binary expansion of \(n\), rejects when fewer than \(81(n+1)\) bits remain, skips a unary initial state below \(n + 1\) and then \(9(n+1)\) five-field transition records, and accepts precisely when the leftover suffix consists entirely of true bits, returning that suffix.

The two-argument function taking a Boolean string and a natural number \(n\) to the string with its first \(n\) entries removed is primitive recursive.

The two-argument function taking a Boolean string \(xs\) and a natural number \(n\) to the prefix of \(xs\) of length \(\left\lvert xs\right\rvert - n\) (truncated subtraction, so the empty string when \(n \ge \left\lvert xs\right\rvert \)) is primitive recursive.

The canonizing string function is primitive recursive. This function maps a Boolean string \(xs\) to the prefix consumed by the erased machine-code parser when that parser accepts (namely the first \(\left\lvert xs\right\rvert - s\) bits, where \(s\) is the length of the leftover all-true suffix), and to the fixed serialization of the trivial one-state halting machine when the parser rejects.

In the work-tape representation of a stack \(xs\), the cell at position \(-\left\lvert xs\right\rvert \) holds the embedded top symbol of \(xs\), and is blank when \(xs\) is empty.

The work-tape representation of the empty stack is the everywhere-blank tape.

Updating the work-tape representation of a stack \(xs\) by writing an embedded symbol \(a\) into the cell at position \(-\left\lvert xs\right\rvert - 1\) yields exactly the representation of the pushed stack with \(a\) prepended to \(xs\).

Updating the work-tape representation of a nonempty stack, with top symbol \(a\) above a tail \(xs\), by blanking its top cell (at position \(-(\left\lvert xs\right\rvert + 1)\)) yields exactly the representation of the popped stack \(xs\).

Mapping a stack name to its work-tape index and back returns the original stack name.

Mapping a work-tape index in \(\{ 0, 1, 2, 3\} \) to its stack name and back returns the original index.

In a bridge configuration with stack assignment \(st\), the symbol read on the work tape assigned to a stack name \(k\) is the embedded top of \(st(k)\), or blank when \(st(k)\) is empty.

Every configuration of a multi-tape machine is reachable from itself, in zero steps.

The one-step successor of any configuration of a multi-tape machine is reachable from it.

Reachability between configurations of a multi-tape machine on a fixed input is transitive: if \(b\) is reachable from \(a\) and \(d\) is reachable from \(b\), then \(d\) is reachable from \(a\).

Applying the idle action with a successor state \(q'\) to a bridge configuration changes only the control state to \(q'\), leaving the input head, all stacks, and the output unchanged.

Suppose that in a bridge configuration the stack assigned to a name \(k\) is nonempty, with top symbol \(a\) above a tail \(xs\). Then the one-tape action on the tape of \(k\) that blanks the current cell and moves that head one cell to the right, passing to a control state \(q'\), transforms the configuration into the bridge configuration with control state \(q'\) whose assignment replaces the stack at \(k\) by \(xs\), the input position and output unchanged.

Pushing a symbol \(a\) onto the stack named \(k\) is realized by two consecutive one-tape actions on the tape of \(k\): first move that head one cell to the left (writing nothing), then write the embedded symbol \(a\) without moving. Applied to a bridge configuration, this yields the bridge configuration whose assignment replaces the stack at \(k\) by \(a\) prepended to it, with the specified final control state and the input position and output unchanged.

The one-tape action on the tape of a stack name \(k\) that blanks the current cell and moves the head right precisely when the stack at \(k\) is nonempty transforms a bridge configuration into the bridge configuration whose stack at \(k\) is replaced by its tail (an empty stack remaining empty), with the input position and output unchanged.

If an optional statement \(q\) belongs to the finite statement support of the compiled program, then the optional execution control state determined by \(q\) and a register value \(v\) is precisely the execution state carrying \(q\) and \(v\).

One step of the bridging machine from a bridge configuration in a live control state is computed by applying the action that its transition table prescribes for that state, the symbol under the input head, and the symbols under the four work-tape heads.

The finite statement support of a compiled program is closed under immediate substatements: if a statement belongs to the support and another statement occurs as an immediate constituent of it, the latter also belongs to the support.

The halt marker belongs to the finite statement support of every compiled program.

Let \(c\) be a program in Mathlib’s partial-recursive language, \(q\) a stack-machine statement in the finite statement support of \(c\)’s compilation, \(v\) an optional register value, and \(st\) a stack assignment. Executing \(q\) on \(v\) and \(st\) in the stack-machine semantics produces a next optional label, register value, and stacks. From the bridge configuration in the execution state for \(q\) and \(v\) over \(st\), the bridging machine of \(c\) reaches, in finitely many steps, the bridge configuration in the optional execution state determined by the translation of that next label and by that register value, over those resulting stacks, with the input position and output unchanged.

For every optional label drawn from the label support of the compiled program with the halt label adjoined, the statement obtained by translating that label belongs to the finite statement support of the program.

Let \(c\) be a program in Mathlib’s partial-recursive language, and let \(a, b\) be configurations of the compiled stack machine such that \(b\) is reachable from \(a\) and the label of \(a\) lies in the label support of \(c\)’s compilation with the halt label adjoined. Then the label of \(b\) also lies in that support, and, for every fixed input head position and output string, the bridging machine of \(c\) reaches, from the bridge configuration associated with \(a\) (the optional execution state for \(a\)’s translated label and register value, over \(a\)’s stacks), the bridge configuration associated with \(b\).

The sentinel numeric code of every Boolean string is positive.

Mathlib’s stack encoding of the singleton list containing the sentinel numeric code of a Boolean string \(xs\) equals the stack word of \(xs\): the bits of \(xs\) as bit symbols, then the sentinel true-bit symbol, then the list terminator.

Performing the two-action push of a symbol \(a\) onto the stack named \(k\), where the second action additionally moves the input head in a direction \(d\), transforms a bridge configuration into the bridge configuration with \(a\) prepended to the stack at \(k\) and the input head moved by \(d\), the output unchanged.

Prepending a symbol to the main stack of the assignment that stores a word on the main stack (other stacks empty) yields the assignment storing the extended word.

Let \(c\) be a program in Mathlib’s partial-recursive language and \(x\) a Boolean input string. For every position \(j \le \left\lvert x\right\rvert \): from the bridge configuration of the bridging machine of \(c\) in the backward-reading state, with input head at position \(j\) and the main stack holding the stack word of the suffix of \(x\) from position \(j\) onward (other stacks empty, empty output), the machine reaches the configuration with the input head at the left endmarker whose main stack holds the stack word of all of \(x\) and whose control is the execution state at the translated initial statement of \(c\)’s compilation, with empty register.

The stack assignment storing the empty word on the main stack has all four stacks empty.

Evaluating the assignment that stores a word \(xs\) on the main stack at the stack name enumerated by an index \(i \in \{ 0, 1, 2, 3\} \) yields \(xs\) when \(i = 0\) (the main stack) and the empty stack otherwise.

Let \(c\) be a program in Mathlib’s partial-recursive language and \(x\) a Boolean input string. For every \(j \le \left\lvert x\right\rvert \), running the bridging machine of \(c\) for exactly \(j\) steps from its initial configuration on the embedded input \(x\) yields the bridge configuration in the scanning state with the input head at position \(j + 1\) (positions are shifted by one, position \(0\) being the left endmarker), all stacks empty, and empty output.

From the bridge configuration of the bridging machine in the scanning state at the right endmarker of the embedded Boolean input \(x\) (all stacks empty, empty output), exactly three steps lead to the backward-reading state with the input head at position \(\left\lvert x\right\rvert \) and the main stack holding just the sentinel true-bit symbol on top of the list terminator, the other stacks empty and the output empty.

From its initial configuration on the embedded Boolean input \(x\), the bridging machine of a partial-recursive program \(c\) reaches the bridge configuration at input position \(0\) whose main stack holds the full stack word of \(x\) (other stacks empty, empty output), in the execution state at the translated initial statement of \(c\)’s compilation, with empty register.

Suppose that in a bridge configuration the stack at a name \(k\) is nonempty, with top symbol \(a\) above a tail \(xs\). The one-tape pop action on the tape of \(k\) (blank the current cell, move right), extended with the emission of an optional output symbol \(e\), produces the bridge configuration whose stack at \(k\) is \(xs\) and whose output is extended by \(e\), the input position unchanged.

Suppose the bridging machine is in the emitting state with an optional pending bit, and the main stack begins with the bit symbol embedding a Boolean \(b\). Then a single step pops that symbol, appends the pending bit (if present, embedded into the bridge alphabet) to the output, and continues in the emitting state with pending bit \(b\); the input position and the other stacks are unchanged.

Suppose that in a bridge configuration of the bridging machine the main stack holds the stack word of a Boolean string \(xs\) and the control is the emitting state with an optional pending bit. Then the machine reaches the halted configuration whose main stack retains only the list terminator (the other stacks unchanged) and whose output is extended by the pending bit, if present, followed by the bits of \(xs\), all embedded into the bridge alphabet; the trailing sentinel bit of the stack word is consumed without being emitted.

Let \(c\) be a program in Mathlib’s partial-recursive language and \(f\) a total function on Boolean strings such that, for every string \(x\), evaluating \(c\) on the singleton list containing the sentinel numeric code of \(x\) yields exactly the singleton list containing the sentinel numeric code of \(f(x)\). Then for every \(x\) there exists a time \(t\) such that the bridging machine of \(c\), run on the embedded input \(x\), halts within \(t\) steps with the embedded string \(f(x)\) on its output tape.

Let \(c\) be a program in Mathlib’s partial-recursive language and \(f\) a function on Boolean strings such that evaluating \(c\) on the singleton list holding the sentinel numeric code of each string \(x\) yields exactly the singleton list holding the code of \(f(x)\). Then there exist a finite Turing machine over the two-letter Boolean alphabet and a time bound \(T \colon \mathbb {N}\to \mathbb {N}\) such that the machine computes \(f\), halting within \(T(\left\lvert x\right\rvert )\) steps on every input \(x\).

The binary expansion, least-significant bit first, of the sentinel numeric code of a Boolean string \(xs\) is exactly \(xs\) followed by a single true bit.

Applying the sentinel decoding to the sentinel numeric code of any Boolean string returns that string.

The sentinel numeric coding of Boolean strings — the number whose binary digits are the string’s bits followed by one true bit — is primitive recursive.

The decoding of sentinel numeric codes — the binary expansion with its most significant digit removed — is primitive recursive.

Every primitive recursive function \(f\) on Boolean strings is computed by an actual machine: there exist a finite Turing machine over the two-letter Boolean alphabet and a time bound \(T \colon \mathbb {N}\to \mathbb {N}\) such that on every input \(x\) the machine halts within \(T(\left\lvert x\right\rvert )\) steps with \(f(x)\) on its output tape. No growth or effectivity condition is imposed on \(T\).

There exist a finite Turing machine over the two-letter Boolean alphabet and a time bound \(T \colon \mathbb {N}\to \mathbb {N}\) such that on every Boolean string the machine halts within \(T\) of the input’s length, outputting the fixed serialization of the one-work-tape binary machine that the string decodes to (malformed strings decoding to the trivial one-state halting machine).