Consider a setup configuration of the oblivious schedule machine built from a Boolean machine \(W\) with \(k\) work tapes and padding parameter \(a\), with input head at \(p\) and controller tapes \(\beta , \mu , \gamma \) with heads at \(b, u, g\). Applying a schedule action with next phase \(q'\), input-head move \(d \in \{ -1,0,+1\} \), and one (optional write, move) pair for each controller tape yields exactly the setup configuration with phase \(q'\), input head moved by \(d\) (clamped to \(\{ 0,\dots ,|x|+1\} \)), each controller tape updated by its optional write at the old head position, and each controller head shifted by its move; the first \(k\) work tapes and the output are untouched.

In a setup configuration on input \(x\) with input head at position \(p \in \{ 0,\dots ,|x|+1\} \), the symbol read from the input tape is blank when \(p = 0\), and otherwise it is the \((p-1)\)-st symbol of \(x\) (in \(0\)-indexed order), which is blank when \(p - 1 \ge |x|\).

In a setup configuration with controller tapes \(\beta , \mu , \gamma \) and heads at \(b, u, g\), the symbols read from the three controller tapes are \(\beta (b)\), \(\mu (u)\), and \(\gamma (g)\) respectively.

Suppose the oblivious schedule machine is in a setup configuration in the reset-scan phase with input head at an interior position \(j \le |x|\); the controller tapes and heads are arbitrary. Then after exactly \(j\) steps the machine is in the same setup configuration except that the input head is at the left boundary (position \(0\)): the phase, all tapes, and all work heads are unchanged.

From a setup configuration in the reset-start phase with input head at an arbitrary position \(p \in \{ 0,\dots ,|x|+1\} \), running exactly \(\max (p,1)+1\) steps of the oblivious schedule machine leads to the setup configuration in the copy-left phase with input head at position \(1\); all controller tapes and heads are unchanged. (The reset begins with a mandatory left move, so even the right blank boundary and the empty input reach the left boundary before the final right move.)

Updating the partial guide with \(j\) copied cells at cell \(j\) — writing the origin mark when \(j = 0\) and an interior mark otherwise — yields the partial guide with \(j+1\) copied cells.

For \(j \gt 0\), a cell of the partial guide with \(j\) copied cells carries the origin mark if and only if it is cell \(0\).

From a setup configuration in the copy-left phase with guide head at \(0\) and entirely blank guide tape, exactly two steps of the oblivious schedule machine write the virtual left boundary (an interior mark at guide cell \(-1\)) and reach the first-copy phase with guide head back at \(0\) over the partial guide with \(0\) copied cells; the input head, the budget and unary tapes, and their heads are unchanged. This holds for every input-head position, including the empty input.

Let \(j \le |x|\). From a setup configuration in the first-copy phase with input head at position \(1\) and guide head at \(0\) over the partial guide with \(0\) copied cells, exactly \(j\) steps lead to the copy phase for \(j\) copied symbols with input head at \(j+1\), guide head at \(j\), and guide tape the partial guide with \(j\) copied cells; the budget and unary tapes and heads are unchanged. In particular the input and guide heads make exactly the same number of right moves, and no data value influences a movement.

From a setup configuration in the copy phase for \(|x|\) copied symbols, with input head parked at the right boundary \(|x|+1\) (reading blank) and guide head at \(|x|\), a single step enters the copy-return phase, leaves both heads in place, and closes the copied zone by writing one more mark, producing the partial guide with \(|x|+1\) cells.

For all \(n, j \in \mathbb {N}\): from a setup configuration in the copy-return phase with guide head at \(j\) over the partial guide with \(n+1\) copied cells, exactly \(j+1\) steps reach the budget-start phase with guide head at the origin (cell \(0\)); all tapes and all other heads are unchanged.

Updating the unary tape with \(N\) markers at cell \(N+1\) with a unit marker yields the unary tape with \(N+1\) markers.

Let \(w\) be a bit word and consider its captured clock tape: the tape with the origin sentinel at cell \(0\), the \(i\)-th bit of \(w\) at cell \(i+1\) for \(0 \le i \lt |w|\), and blanks elsewhere. A cell of this tape carries the origin mark if and only if it is cell \(0\).

On the captured clock tape of a bit word \(w\) (origin sentinel at cell \(0\), the bits of \(w\) on cells \(1,\dots ,|w|\)), cell \(|w|+1\) is blank.

For every \(j \in \mathbb {N}\): from a setup configuration in the budget-back phase with budget head at cell \(j\) over the captured clock tape of a bit word \(w\), exactly \(j+1\) steps reach the sentinel at the origin and move right once, entering the first append phase with budget head at cell \(1\); all tapes and all other heads are unchanged.

From a setup configuration in the budget-start phase with budget head at cell \(|w|+1\) (one cell beyond the captured clock tape of the bit word \(w\)), exactly \(|w|+2\) steps reach the first append phase with budget head at cell \(1\); the cost depends only on the width of \(w\), not on its bits, and all tapes and all other heads are unchanged.

Let \(j \le a+1\), where \(a\) is the padding parameter. From a setup configuration in append phase \(0\) with unary head at cell \(N+1\) over the unary tape with \(N\) markers, exactly \(j\) steps reach append phase \(j\) with unary head at cell \(N+j+1\) over the unary tape with \(N+j\) markers; each step writes exactly one unit marker, and all other tapes and heads are unchanged.

From a setup configuration in append phase \(0\) with unary head at cell \(N+1\) over the unary tape with \(N\) markers, exactly \(a+2\) steps append exactly \(a+1\) unit markers and enter the borrow phase with incoming borrow set: the unary head is then at cell \(N+(a+1)+1\) over the unary tape with \(N+a+1\) markers, and all other tapes and heads are unchanged.

Present a tape as a zipper with frontier \(z \in \mathbb {Z}\), a list \(l\) of the (possibly blank) cells to the left of \(z\) listed nearest-first, and a list of the cells at and to the right of \(z\). If the right list decomposes as \(w \mathbin {+\! \! +} r\), then the same tape is presented by the zipper with frontier \(z + |w|\), left list \(\mathrm{reverse}(w) \mathbin {+\! \! +} l\), and right list \(r\).

For every bit word \(w\), the captured clock tape of \(w\) (origin sentinel at cell \(0\), the bits of \(w\) on cells \(1,\dots ,|w|\), blanks elsewhere) equals the zipper tape with frontier at cell \(1\), left list consisting of the single origin sentinel, and right list the bits of \(w\), each encoded as a budget-bit symbol.

For every bit word \(w\), the zipper tape with frontier \(1+|w|\), empty right list, and left list consisting of the reversed encoded bits of \(w\) followed by the origin sentinel equals the captured clock tape of \(w\).

Take a setup configuration and focus its budget lane: replace the state by \(q'\), the budget tape by the zipper tape with frontier \(z\), left list \(l\), and right list \(r\), and move the budget head to \(z\), keeping every other tape and head. The result is again a setup configuration, with the same base configuration, input head, unary and guide data, state \(q'\), budget head \(z\), and budget tape given by that zipper.

Let \(w\) be a bit word and \(c\) a Boolean incoming borrow, and recall the fixed-width borrow pass: it processes all of \(w\), subtracting the incoming borrow from its little-endian value while preserving its length, and returns an outgoing borrow flag together with the rewritten word. From a setup configuration in the borrow phase with flag \(c\) and budget head at cell \(1\) over the captured clock tape of \(w\), exactly \(|w|\) steps reach the borrow phase whose flag is the outgoing borrow, with budget head at \(1+|w|\) over the captured clock tape of the rewritten word; all other tapes and heads, and the parked input head, remain fixed.

From a setup configuration in the borrow phase with flag \(c\) and budget head at cell \(|w|+1\) (the blank cell after the captured clock tape of the bit word \(w\)), one step keeps every tape and head fixed and moves to the unary-start phase when \(c\) is true (the budget underflowed, i.e. is exhausted) and back to the budget-start phase otherwise.

One complete round of the budget controller — full rewind, append block of \(a+1\) unary markers, fixed-width borrow pass, and end test — costs exactly \(2|w| + (a+1) + 4\) steps, independently of the bits of the budget word \(w\). Starting in the budget-start phase with budget head at \(|w|+1\) over the captured clock tape of \(w\) and unary head at \(N+1\) over the unary tape with \(N\) markers, the round ends with the captured clock tape of the borrowed word (incoming borrow set), the unary tape with \(N + a + 1\) markers, and phase unary-start or budget-start according to the borrow’s underflow flag.

Let \(w\) be a bit word of little-endian value \(v\) and let \(N \in \mathbb {N}\). From a setup configuration in the budget-start phase with budget head at \(|w|+1\) over the captured clock tape of \(w\) and unary head at \(N+1\) over the unary tape with \(N\) markers, exactly \((v+1)\, \bigl(2|w| + (a+1) + 4\bigr)\) steps reach the unary-start phase with unary head at \(N + (a+1)(v+1) + 1\) over the unary tape with \(N + (a+1)(v+1)\) markers, the budget tape being the captured clock tape of some bit word \(w'\) with \(|w'| = |w|\) (the word keeps its full width as its high bits become zero); the guide tape and head and the input head are unchanged.

A cell of the unary tape with \(N\) markers carries the origin mark if and only if it is cell \(0\).

For every \(j \lt N\), cell \(j+1\) of the unary tape with \(N\) markers carries a unit marker.

Cell \(N+1\) of the unary tape with \(N\) markers is blank.

For every \(j \in \mathbb {N}\) and either rewind variant: from a setup configuration in the corresponding unary rewind phase with unary head at cell \(j\) over the unary tape with \(N\) markers, exactly \(j+1\) steps reach the successor phase — the start-center phase for the final rewind, the first rightward layout phase otherwise — with unary head at cell \(1\); no tape is written and all other heads are unchanged.

From a setup configuration in the unary-start phase with unary head at cell \(N+1\) over the unary tape with \(N\) markers, exactly \(N+2\) steps rewind the entire newly constructed unary segment and reach the first rightward layout phase with unary head at cell \(1\); all tapes and all other heads are unchanged.

Filling zero cells of a guide tape, in either direction, leaves the tape unchanged.

If a guide tape carries the origin mark exactly at cell \(0\), then for every \(j\) and either direction, its \(j\)-cell filled version also carries the origin mark exactly at cell \(0\).

Updating the \(j\)-cell filled version of a guide tape at cell \(j\) (rightward) respectively \(-j\) (leftward) with the corresponding guide mark yields the \((j+1)\)-cell filled version.

Consider a setup configuration in layout phase \(i \in \{ 0,1,2\} \) of either direction, and suppose the unary tape reads a unit marker at the unary head and the guide tape reads the origin mark at the guide head exactly when that head is at cell \(0\). Then one step moves to layout phase \(i+1 \bmod 3\), writes the guide mark at the guide head, moves the guide head one cell in the chosen direction, and advances the unary head by one exactly when \(i = 2\); everything else is unchanged. Thus the controller spends three guide cells per unary marker.

Let \(\gamma \) be a guide tape carrying the origin mark exactly at cell \(0\), and suppose the unary tape reads a unit marker at the unary head. Then one step from layout phase \(i\) (of either direction) with guide head at \(\pm j\) over the \(j\)-cell filled version of \(\gamma \) leads to layout phase \(i+1 \bmod 3\) with guide head at \(\pm (j+1)\) over the \((j+1)\)-cell filled version, incrementing the unary head exactly when \(i = 2\).

For every \(j \in \mathbb {N}\), the cyclic successor on \(\{ 0,1,2\} \) of \(j \bmod 3\) is \((j+1) \bmod 3\). Hence the finite allocation phase is the remainder modulo three of the number of guide cells already written.

Let \(\gamma \) be a guide tape carrying the origin mark exactly at cell \(0\), and let \(j \le 3B\). From layout phase \(0\) (of either direction) with unary head at cell \(1\) over the unary tape with \(B\) markers and guide head at cell \(0\) over \(\gamma \), exactly \(j\) steps lead to layout phase \(j \bmod 3\) with unary head at \(\lfloor j/3 \rfloor + 1\), guide head at \(\pm j\), and guide tape the \(j\)-cell filled version of \(\gamma \): the elapsed time equals the number of written guide cells, and the unary head moves once every three cells.

From layout phase \(0\) (of either direction) with unary head at cell \(B+1\) — the blank cell terminating the unary tape with \(B\) markers — and guide head at cell \(g\), one step writes an interior mark at guide cell \(g\), moves the guide head one further cell outward, keeps the unary head in place, and enters the right-edge or left-edge phase according to the direction.

If \(n + 1 \le R\), then filling \(R\) cells rightward starting from the partial guide with \(n+1\) copied cells yields exactly the partial guide with \(R\) cells: only the positive prefix is overwritten.

A cell of the right guide of radius \(R\) carries the origin mark if and only if it is cell \(0\); the right-boundary write cannot alter the origin.

Let \(R \gt 0\). Starting from the right guide of radius \(R\), filling \(R\) cells leftward and then writing an interior mark at cell \(-R\) and the left outer boundary marker at cell \(-R-1\) produces the completed guide of radius \(R\): origin mark at \(0\), interior marks at all \(z\) with \(0 \lt |z| \le R\), boundary markers at \(\pm (R+1)\), and blanks elsewhere.

From a setup configuration in the right-edge phase with unary head at cell \(B+1\) over the unary tape with \(B\) markers and guide head at cell \(R+1\) over the partial guide with \(R+1\) copied cells, one step writes the right outer boundary marker at guide cell \(R+1\), moves the unary and guide heads one cell left (to \(B\) and \(R\)), and enters the first layout-return phase; the resulting guide tape is the right guide of radius \(R\).

Suppose a setup configuration is in layout-return phase \(i \in \{ 0,1,2\} \) and the unary tape does not read the origin sentinel at the unary head. Then one step moves to layout-return phase \(i+1 \bmod 3\), moves the guide head one cell left, decrements the unary head exactly when \(i = 2\), and writes nothing on any tape.

Let \(j \le 3B\). From layout-return phase \(0\) with unary head at cell \(B\) over the unary tape with \(B\) markers and guide head at cell \(3B\) (over an arbitrary guide tape), exactly \(j\) steps lead to layout-return phase \(j \bmod 3\) with unary head at \(B - \lfloor j/3 \rfloor \) and guide head at \(3B - j\); no tape is written and all guide marks are unchanged.

From layout-return phase \(0\) with unary head at cell \(B\) over the unary tape with \(B\) markers and guide head at cell \(3B\) (over an arbitrary guide tape), exactly \(3B+1\) steps reach the origin and enter the first leftward layout phase with unary head at cell \(1\) and guide head at cell \(0\); no tape is written.

Let \(n + 1 \le B\). From the first rightward layout phase with unary head at cell \(1\) over the unary tape with \(B\) markers and guide head at cell \(0\) over the partial guide with \(n+1\) copied cells, exactly \(3B + 2\) steps reach radius \(3B\), install the right outer boundary marker, and enter the first layout-return phase with unary head at \(B\), guide head at \(3B\), and guide tape the right guide of radius \(3B\).

Let \(B \gt 0\). From the first leftward layout phase with unary head at cell \(1\) over the unary tape with \(B\) markers and guide head at cell \(0\) over the right guide of radius \(3B\), exactly \(3B + 2\) steps complete the fixed guide and enter the unary-reset phase with unary head at \(B\), guide head at the left outer boundary \(-3B - 1\), and guide tape the completed guide of radius \(3B\).

For every \(j \in \mathbb {N}\): from a setup configuration in the start-center phase with guide head at cell \(-j\) over the completed guide of radius \(R\), exactly \(j+1\) steps reach the origin and enter the macrostep-check phase with guide head at cell \(0\); all tapes and all other heads are unchanged.

Let \(n + 1 \le B\). From a setup configuration in the unary-start phase with unary head at cell \(B+1\) over the unary tape with \(B\) markers and guide head at cell \(0\) over the partial guide with \(n+1\) copied cells, exactly \(14B + 10\) steps produce the completed guide of radius \(3B\) and enter the macrostep-check phase with unary head at cell \(1\) and guide head at cell \(0\); the budget tape and head and the parked input head are unchanged.

From a setup configuration in the copy-left phase with input head at position \(1\), guide head at cell \(0\), and entirely blank guide tape, exactly \(2|x| + 4\) steps — covering both virtual boundary cells and the return to the origin — reach the budget-start phase with input head parked at position \(|x|+1\), guide head at cell \(0\), and guide tape the partial guide with \(|x|+1\) copied cells; the budget and unary tapes and heads are unchanged, and the native input stays parked from then on.

The captured clock tape of the empty bit word equals the unary tape with zero markers: both consist of the origin sentinel at cell \(0\) and blanks everywhere else.

Let \(c\) be a configuration of the \(k\)-tape Boolean machine \(W\) on a Boolean input that has halted (its state is the halting state). Then the clock-stage embedding of \(c\) into the oblivious schedule machine — which keeps the work block of \(c\) and captures its entire output word on the budget tape — is itself a setup configuration: base the embedded configuration itself, phase reset-start, the embedded input-head position, budget head at cell \(m+1\) over the captured clock tape of the output word of \(c\) (where \(m\) is that word’s length), unary head at cell \(1\) over the unary tape with zero markers, and guide head at cell \(0\) over the blank tape.

Modifying a setup configuration by changing only its phase to \(q'\) and its unary and guide head positions to \(u'\) and \(g'\) — keeping every tape, the budget head, and the input head fixed — again yields a setup configuration with the same remaining data.

From a setup configuration in the macrostep-check phase with unary head at cell \(1\) over the unary tape with \(B\) markers and guide head at cell \(0\) over the completed guide of radius \(3B\), exactly \(B\, \bigl(6\, (3B) + 8\bigr) + 1\) steps execute one full sweep per unary marker and reach the halted configuration with unary head at cell \(B+1\) and guide head at cell \(0\); every tape, the budget head, and the input head are unchanged.

Let \(w\) be a bit word of little-endian value \(v\), and suppose the input satisfies \(|x| + 1 \le (a+1)(v+1)\), where \(a\) is the padding parameter. Consider a setup configuration in the reset-start phase with input head at an arbitrary position \(p\), budget head at cell \(|w|+1\) over the captured clock tape of \(w\), unary head at cell \(1\) over the unary tape with zero markers, and guide head at cell \(0\) over the blank guide tape. Then there is a bit word \(w'\) with \(|w'| = |w|\) such that after exactly

steps the machine is in the macrostep-check phase with input head parked at position \(|x|+1\), budget head at cell \(|w|+1\) over the captured clock tape of \(w'\), unary head at cell \(1\) over the unary tape with \((a+1)(v+1)\) markers, and guide head at cell \(0\) over the completed guide of radius \(3\, (a+1)(v+1)\): the binary counter retains its full width throughout.