172 Complexity — Simulation
172.1 Overview
This module provides generic building blocks from which larger machine constructions are assembled: fixed-word emission chains that write a word to the output one symbol per step and then halt; control actions that only move the input head and change state, together with a rewind-to-start scan of the input head; disjoint tape-block extensions that run a machine on the left or right block of a larger machine in exact lockstep; the branch union of two machines selected by a Boolean; a normalization identity for work-tape writes; and a buffered sequential simulator that runs a first machine into a middle buffer tape, rewinds that buffer, and then serves the buffered word as the virtual input of a second machine, with boundary clamping realized by a Boolean arrival tag.
172.2 Declarations
Let \(a\) be a one-step action of a multi-tape Turing machine with \(k\) work tapes, let \(c\) be a configuration of such a machine, and let \(i\) be one of the \(k\) work-tape indices. After applying \(a\) to \(c\), the content of the \(i\)-th work tape equals the old content updated at the cell under the \(i\)-th work head, where the new cell value is the symbol that \(a\) proposes to write there and, when \(a\) declines to write on that tape, the symbol previously scanned: an explicit blank write erases the cell, while no write at all copies the scanned symbol back unchanged. No finiteness or liveness hypothesis is required.
Given a Boolean word \(w\), a map \(e\) from \(\{ 0,\dots ,\left\lvert w\right\rvert \} \) into the states of a machine with \(k\) work tapes over the Boolean alphabet, and an index \(i \in \{ 0,\dots ,\left\lvert w\right\rvert \} \), the one-step action that, when \(i \lt \left\lvert w\right\rvert \), appends the \(i\)-th symbol of \(w\) (zero-indexed) to the output and passes to state \(e(i+1)\), and otherwise emits nothing and halts. In both cases the input head and all work tapes are left untouched.
Let \(M\) be a multi-tape Turing machine with \(k\) work tapes over the Boolean alphabet running on some input \(x\), let \(w\) be a Boolean word, and let \(e\) be a map from \(\{ 0,\dots ,\left\lvert w\right\rvert \} \) into the states of \(M\) such that from each state \(e(i)\), regardless of the symbols read, the transition of \(M\) is the emission action for \(w\) at index \(i\): while \(i \lt \left\lvert w\right\rvert \) it appends the \(i\)-th symbol of \(w\) to the output and passes to \(e(i+1)\), and at \(i = \left\lvert w\right\rvert \) it halts, in both cases leaving the input head and all work tapes fixed. If a configuration \(c\) is in state \(e(0)\), then for every \(t \le \left\lvert w\right\rvert \), after \(t\) steps from \(c\) the machine is in state \(e(t)\) and its output is the output of \(c\) followed by the first \(t\) symbols of \(w\).
Let \(M\) be a multi-tape Turing machine with \(k\) work tapes over the Boolean alphabet running on some input \(x\), let \(w\) be a Boolean word, and let \(e\) be a map from \(\{ 0,\dots ,\left\lvert w\right\rvert \} \) into the states of \(M\) such that from each state \(e(i)\), regardless of the symbols read, the transition of \(M\) is the emission action for \(w\) at index \(i\) (append the \(i\)-th symbol of \(w\) and pass to \(e(i+1)\) while \(i \lt \left\lvert w\right\rvert \), halt at \(i = \left\lvert w\right\rvert \), never moving the input head or touching a work tape). If a configuration \(c\) is in state \(e(0)\), then after exactly \(\left\lvert w\right\rvert + 1\) steps from \(c\) the machine has halted and its output is the output of \(c\) followed by all of \(w\).
For a movement \(m \in \{ -1, 0, +1\} \) and an optional successor state \(q\), the one-step action of a machine with \(k\) work tapes over the Boolean alphabet that moves the input head by \(m\) (subject to clamping at the two boundary blanks), writes nothing on any work tape, moves no work head, emits no output, and passes to \(q\), halting when \(q\) is absent.
Let \(c\) be a configuration of a multi-tape Turing machine over the Boolean alphabet on input \(x\), and let \(i \le \left\lvert x\right\rvert \) be a natural number such that the input head of \(c\) sits at position \(i + 1\), in the convention where position \(0\) is the left boundary blank and position \(j\) with \(1 \le j \le \left\lvert x\right\rvert \) scans the \(j\)-th input symbol. Then the symbol scanned on the input tape is the optional \(i\)-th entry of \(x\) (zero-indexed): the symbol \(x_i\) when \(i \lt \left\lvert x\right\rvert \), and the right boundary blank when \(i = \left\lvert x\right\rvert \).
Given natural numbers \(k\) and \(l\), a state renaming \(f : S \to S'\), and a one-step action \(a\) of a machine with \(k\) work tapes over the Boolean alphabet, the action of a machine with \(k + l\) work tapes that performs \(a\) on the first \(k\) work tapes, writes nothing and moves no head on the last \(l\) tapes, keeps the input-head movement and the emitted output of \(a\), and renames the successor state along \(f\), preserving halting.
Given natural numbers \(k\) and \(l\), a state renaming \(f : S \to S'\), and a one-step action \(a\) of a machine with \(l\) work tapes over the Boolean alphabet, the action of a machine with \(k + l\) work tapes that performs \(a\) on the last \(l\) work tapes, writes nothing and moves no head on the first \(k\) tapes, keeps the input-head movement and the emitted output of \(a\), and renames the successor state along \(f\), preserving halting.
Given a state renaming \(f : S \to S'\), a configuration \(c\) of a machine with \(k\) work tapes over the Boolean alphabet on input \(x\), and arbitrary contents and head positions for \(l\) further tapes, the configuration of a machine with \(k + l\) work tapes on the same input whose state is that of \(c\) renamed along \(f\) (halted exactly when \(c\) is halted), whose input head and output agree with those of \(c\), whose first \(k\) work tapes and heads are those of \(c\), and whose last \(l\) work tapes carry the given inactive contents and head positions.
Given a state renaming \(f : S \to S'\), a configuration \(c\) of a machine with \(l\) work tapes over the Boolean alphabet on input \(x\), and arbitrary contents and head positions for \(k\) further tapes, the configuration of a machine with \(k + l\) work tapes on the same input whose state is that of \(c\) renamed along \(f\) (halted exactly when \(c\) is halted), whose input head and output agree with those of \(c\), whose last \(l\) work tapes and heads are those of \(c\), and whose first \(k\) work tapes carry the given inactive contents and head positions, for instance data left behind by an earlier phase.
Let \(f : S \to S'\) be a state renaming, \(a\) a one-step action of a machine with \(k\) work tapes over the Boolean alphabet, \(c\) a configuration of such a machine on input \(x\), and fix contents and head positions for \(l\) inactive extra tapes. Applying the left-block extension of \(a\) along \(f\) to the left-block embedding of \(c\) with the given inactive data yields the left-block embedding, with the same inactive data, of the result of applying \(a\) to \(c\).
Let \(f : S \to S'\) be a state renaming, \(a\) a one-step action of a machine with \(l\) work tapes over the Boolean alphabet, \(c\) a configuration of such a machine on input \(x\), and fix contents and head positions for \(k\) inactive extra tapes. Applying the right-block extension of \(a\) along \(f\) to the right-block embedding of \(c\) with the given inactive data yields the right-block embedding, with the same inactive data, of the result of applying \(a\) to \(c\).
Let \(M\) be a machine with \(k\) work tapes and \(M'\) a machine with \(k + l\) work tapes, both over the Boolean alphabet, and let \(f\) be a map from the states of \(M\) to the states of \(M'\) such that on every renamed state \(f(q)\), for every scanned input symbol and every tuple of scanned work symbols, the transition of \(M'\) is the left-block extension along \(f\) of the transition of \(M\) from \(q\) on that input symbol and the symbols scanned on the first \(k\) tapes. Then for every configuration \(c\) of \(M\) on input \(x\) and all inactive contents and head positions for the last \(l\) tapes, one step of \(M'\) from the left-block embedding of \(c\) equals the left-block embedding of one step of \(M\) from \(c\); in particular a halted embedded configuration stays halted.
Let \(M\) be a machine with \(l\) work tapes and \(M'\) a machine with \(k + l\) work tapes, both over the Boolean alphabet, and let \(f\) be a map from the states of \(M\) to the states of \(M'\) such that on every renamed state \(f(q)\), for every scanned input symbol and every tuple of scanned work symbols, the transition of \(M'\) is the right-block extension along \(f\) of the transition of \(M\) from \(q\) on that input symbol and the symbols scanned on the last \(l\) tapes. Then for every configuration \(c\) of \(M\) on input \(x\) and all inactive contents and head positions for the first \(k\) tapes — which may hold arbitrary data from an earlier phase — one step of \(M'\) from the right-block embedding of \(c\) equals the right-block embedding of one step of \(M\) from \(c\).
Let \(M\) be a machine with \(k\) work tapes and \(M'\) a machine with \(k + l\) work tapes, both over the Boolean alphabet, and let \(f\) be a map from the states of \(M\) to the states of \(M'\) such that on every renamed state, for all scanned symbols, the transition of \(M'\) is the left-block extension along \(f\) of the corresponding transition of \(M\) read off the first \(k\) tapes. Then for every configuration \(c\) of \(M\) on input \(x\), all inactive contents and head positions for the last \(l\) tapes, and every number of steps \(t\), running \(M'\) for \(t\) steps from the left-block embedding of \(c\) equals the left-block embedding of the run of \(M\) for \(t\) steps from \(c\).
Let \(M\) be a machine with \(l\) work tapes and \(M'\) a machine with \(k + l\) work tapes, both over the Boolean alphabet, and let \(f\) be a map from the states of \(M\) to the states of \(M'\) such that on every renamed state, for all scanned symbols, the transition of \(M'\) is the right-block extension along \(f\) of the corresponding transition of \(M\) read off the last \(l\) tapes. Then for every configuration \(c\) of \(M\) on input \(x\), all inactive contents and head positions for the first \(k\) tapes, and every number of steps \(t\), running \(M'\) for \(t\) steps from the right-block embedding of \(c\) equals the right-block embedding of the run of \(M\) for \(t\) steps from \(c\), with the inactive left-block data preserved throughout.
Given two Turing machines \(M_1\) and \(M_2\) over the Boolean alphabet with finitely many states, and a Boolean \(b\), the machine whose work tapes are the disjoint union of the tapes of \(M_1\) and \(M_2\), whose state type is the disjoint union of their state types, whose transitions run \(M_1\) on the left tape block from left states and \(M_2\) on the right tape block from right states, and whose initial state is the initial state of \(M_1\) when \(b\) is true and of \(M_2\) when \(b\) is false. Only the initial state depends on \(b\); the transition table does not.
Let \(M_1\) and \(M_2\) be Turing machines over the Boolean alphabet with finitely many states, let \(b\) be a Boolean, let \(x\) and \(w\) be Boolean words, and let \(t\) be a natural number. The branch union of \(M_1\) and \(M_2\) selected by \(b\) halts on input \(x\) within \(t\) steps with output \(w\) if and only if the selected machine — \(M_1\) when \(b\) is true, \(M_2\) when \(b\) is false — halts on input \(x\) within \(t\) steps with output \(w\).
Let \(c\) be a configuration of a machine with \(k\) work tapes over the Boolean alphabet on input \(x\), let \(m \in \{ -1, 0, +1\} \) be a movement, and let \(q\) be an optional state. Applying the control action for \(m\) and \(q\) to \(c\) yields the configuration that agrees with \(c\) on all work-tape contents, work-head positions, and output, whose state is \(q\), and whose input head is that of \(c\) moved by \(m\) with clamping at the two boundary blanks.
Let \(p \in \{ 0,\dots ,n+1\} \) be an input-head position for an input of length \(n\). The clamped left move sends \(p\) to the position whose value is \(p - 1\) in truncated natural subtraction; in particular the left boundary position \(0\) is fixed.
Let \(M\) be a multi-tape Turing machine over the Boolean alphabet on input \(x\), let \(s\) be a scanning state, and let \(d\) be an optional dispatch state, such that regardless of the work symbols read: in state \(s\) scanning an input symbol, \(M\) moves the input head left and stays in \(s\); in state \(s\) scanning a blank, \(M\) moves the input head right and passes to \(d\); and neither transition touches a work tape or the output. Then from any configuration \(c\) in state \(s\) whose input-head position \(p\) satisfies \(p \le \left\lvert x\right\rvert \), running \(M\) for exactly \(p + 1\) steps yields the configuration that agrees with \(c\) in every component except that its state is \(d\) and its input head is at position \(1\), the position scanning the first input symbol.
Let \(M\) be a multi-tape Turing machine over the Boolean alphabet on input \(x\), with a start state \(r\), a scanning state \(s\), and an optional dispatch state \(d\), such that regardless of the symbols read: from \(r\) the machine always moves the input head left and enters \(s\); from \(s\) it moves left and stays in \(s\) when an input symbol is scanned, and moves right and passes to \(d\) when a blank is scanned; and none of these transitions touches a work tape or the output. Then from any configuration \(c\) in state \(r\) there exists a number of steps \(t\) such that after \(t\) steps the configuration agrees with \(c\) in every component except that its state is \(d\) and its input head is at position \(1\). This holds even when \(x\) is empty or the input head of \(c\) starts at a boundary blank.
Given a family of values indexed by \(\{ 0,\dots ,k-1\} \) (the left block), a single value (the buffer), and a family of values indexed by \(\{ 0,\dots ,l-1\} \) (the right block), the family indexed by the \(k + (1 + l)\) tape indices that returns the left values on the first \(k\) indices, the buffer value on the next index, and the right values on the last \(l\) indices.
Let \(a\) be a family of values on \(k\) indices, \(b\) a single value, and \(c\) a family of values on \(l\) indices. Evaluating their three-block assembly at the \(i\)-th index of the left block returns \(a(i)\).
Let \(a\) be a family of values on \(k\) indices, \(b\) a single value, and \(c\) a family of values on \(l\) indices. Evaluating their three-block assembly at the middle buffer index returns \(b\).
Let \(a\) be a family of values on \(k\) indices, \(b\) a single value, and \(c\) a family of values on \(l\) indices. Evaluating their three-block assembly at the \(i\)-th index of the right block returns \(c(i)\).
For a Boolean word \(w\), the work-tape content over the integer cells that stores \(w\) contiguously from cell zero: cell \(z\) holds the \(z\)-th symbol of \(w\) (zero-indexed) when \(0 \le z \lt \left\lvert w\right\rvert \), and is blank at every other integer cell.
The buffer tape storing the empty word is blank at every integer cell.
Let \(w\) be a Boolean word and \(i\) a natural number. Cell \(i\) of the buffer tape storing \(w\) holds the optional \(i\)-th entry of \(w\): the symbol \(w_i\) when \(i \lt \left\lvert w\right\rvert \) and a blank otherwise. In particular cell \(\left\lvert w\right\rvert \) is the blank immediately to the right of the stored word.
For every Boolean word \(w\), cell \(-1\) of the buffer tape storing \(w\) is blank; this includes the case of the empty word.
Let \(w\) be a Boolean word and \(b\) a Boolean symbol. The buffer tape storing \(w\) followed by the single symbol \(b\) equals the buffer tape storing \(w\) updated at cell \(\left\lvert w\right\rvert \) to hold \(b\): exactly the cell that was the old right blank changes, and every other integer cell is unaffected.
For a position \(p \in \{ 0,\dots ,n+1\} \) of a virtual input head over an input of length \(n\) and a Boolean tag \(b\), the predicate asserting that \(b\) correctly marks the boundaries: if \(p = 0\) then \(b\) is false, and if \(p = n + 1\) then \(b\) is true. At interior positions both tag values are admissible.
Given a Boolean boundary tag \(b\), an optional scanned symbol, and a requested movement \(m \in \{ -1, 0, +1\} \), the movement actually performed by a buffer head simulating an input head: when the scanned symbol is blank and the requested movement points outward — left with tag false, marking the left boundary, or right with tag true, marking the right boundary — the head stays put; in every other case it moves by \(m\).
Given a Boolean tag \(b\) and a performed movement \(m \in \{ -1, 0, +1\} \), the tag after the move: false after a left move, true after a right move, and \(b\) itself after a stationary move, so that a suppressed outward move retains its boundary tag and repeated outward attempts remain clamped.
Let \(c\) be a configuration of a machine with \(k\) work tapes over the Boolean alphabet whose input is the word \(w\), and let \(p \in \{ 0,\dots ,\left\lvert w\right\rvert +1\} \) be its input-head position. Cell \(p - 1\) of the buffer tape storing \(w\) holds exactly the symbol scanned by the input head of \(c\): the corresponding input symbol at interior positions, and a blank at the two boundary positions.
Let \(c\) be a configuration of a machine over the Boolean alphabet on input \(w\), let \(p \in \{ 0,\dots ,\left\lvert w\right\rvert +1\} \) be its input-head position, let \(b\) be a Boolean tag valid for \(p\) (forced false at the left boundary \(p = 0\) and true at the right boundary \(p = \left\lvert w\right\rvert + 1\)), and let \(m \in \{ -1, 0, +1\} \) be a requested movement. Write \(p'\) for the result of the native clamped move of \(p\) by \(m\). Then, as integers, \(p - 1\) plus the virtual movement determined by \(b\), the scanned input symbol of \(c\), and \(m\) equals \(p' - 1\); and the updated tag — false after a left move, true after a right move, unchanged when stationary — is again valid for \(p'\). This holds for every word \(w\), including the empty word.
Given machines \(M_1\) and \(M_2\) over the Boolean alphabet with finitely many states, having \(k_1\) and \(k_2\) work tapes respectively, the machine with \(k_1 + (1 + k_2)\) work tapes that operates in phases. In the first phase it simulates \(M_1\) on the left tape block, diverting every symbol that \(M_1\) would output onto the middle buffer tape instead of the real output; the simulated halt of \(M_1\) leads to a live administrative rewind state, in which the buffer head scans left until it reaches the blank preceding the stored word. It then moves right and dispatches into the second phase, a simulation of \(M_2\) on the right tape block in which the input reads of \(M_2\) are served from the buffer, with movements clamped at the boundary blanks of the stored word by a Boolean arrival tag carried in the state. Only the second phase emits symbols to the real output or halts.
Given machines \(M_1\) and \(M_2\) over the Boolean alphabet with finitely many states and a configuration \(c\) of \(M_1\) on input \(x\), the configuration of the buffered sequential composition of \(M_1\) and \(M_2\) on input \(x\) whose state is the first-phase image of the state of \(c\) (a live administrative state even when \(c\) has halted), whose input head agrees with \(c\), whose left tape block carries the work tapes and heads of \(c\), whose middle buffer tape stores the output of \(c\) contiguously with the buffer head on the blank immediately to its right, whose right tape block is blank with heads at the origin, and whose real output is empty.
For all machines \(M_1\) and \(M_2\) over the Boolean alphabet with finitely many states and every input \(x\), the initial configuration of the buffered sequential composition of \(M_1\) and \(M_2\) on \(x\) equals the first-phase embedding of the initial configuration of \(M_1\) on \(x\), in which the buffer stores the empty word.
Let \(M_1\) and \(M_2\) be machines over the Boolean alphabet with finitely many states, and let \(c\) be a configuration of \(M_1\) on input \(x\) that has not halted. One step of the buffered sequential composition of \(M_1\) and \(M_2\) from the first-phase embedding of \(c\) equals the first-phase embedding of one step of \(M_1\) from \(c\). In particular a symbol emitted by \(M_1\) on that step — including on its halting transition — lands on the buffer with the buffer head advancing past it, the real output stays empty, and a simulated halt of \(M_1\) leaves the composite in a live administrative state.
Let \(M_1\) and \(M_2\) be machines over the Boolean alphabet with finitely many states, let \(c\) be a configuration of \(M_1\) on input \(x\), and let \(t\) be a number of steps such that the run of \(M_1\) from \(c\) has not halted at any time strictly before \(t\). Then running the buffered sequential composition of \(M_1\) and \(M_2\) for \(t\) steps from the first-phase embedding of \(c\) yields the first-phase embedding of the run of \(M_1\) for \(t\) steps from \(c\). The time \(t\) itself may be the first halting time of \(M_1\).
Given machines \(M_1\) and \(M_2\) over the Boolean alphabet with finitely many states, a configuration \(c\) of \(M_2\) on a virtual input \(y\), a Boolean tag \(b\), a position \(p \in \{ 0,\dots ,\left\lvert x\right\rvert +1\} \) of the physical input head over the real input \(x\), and arbitrary contents and head positions for the left tape block of \(M_1\), the configuration of the buffered sequential composition of \(M_1\) and \(M_2\) on input \(x\) whose state is the second-phase image of the state of \(c\) paired with \(b\) (halted exactly when \(c\) is halted), whose physical input head is parked at \(p\), whose left block carries the given inactive data, whose middle buffer stores \(y\) with the buffer head at the virtual input-head position of \(c\) minus one, whose right block carries the work tapes and heads of \(c\), and whose real output is the output of \(c\).
Let \(M_1\) and \(M_2\) be machines over the Boolean alphabet with finitely many states, let \(c\) be a configuration of \(M_2\) on a virtual input \(y\), and let \(b\) be a Boolean tag valid for the virtual input-head position of \(c\) (forced false at the left boundary and true at the right boundary). Fix a position \(p\) of the physical input head over the real input \(x\) and arbitrary inactive contents and head positions for the left tape block. Then there exists a tag \(b'\), valid for the input-head position reached after one step of \(M_2\) from \(c\), such that one step of the buffered sequential composition of \(M_1\) and \(M_2\) from the second-phase embedding of \(c\) with tag \(b\) equals the second-phase embedding of one step of \(M_2\) from \(c\) with tag \(b'\), keeping \(p\) and the inactive data unchanged. The halted case is included: a halted \(c\) stays halted on both sides.
Let \(M_1\) and \(M_2\) be machines over the Boolean alphabet with finitely many states, let \(c\) be a configuration of \(M_2\) on a virtual input \(y\), and let \(b\) be a Boolean tag valid for the virtual input-head position of \(c\). Fix a position \(p\) of the physical input head over the real input \(x\), arbitrary inactive contents and head positions for the left tape block, and a number of steps \(t\). Then there exists a tag \(b'\), valid for the input-head position of the run of \(M_2\) for \(t\) steps from \(c\), such that running the buffered sequential composition of \(M_1\) and \(M_2\) for \(t\) steps from the second-phase embedding of \(c\) with tag \(b\) equals the second-phase embedding of that run with tag \(b'\), keeping \(p\) and the inactive data unchanged. Completed outputs and absorbing halting are thereby preserved.
Given machines \(M_1\) and \(M_2\) over the Boolean alphabet with finitely many states, a Boolean word \(y\) stored on the buffer, a position \(p \in \{ 0,\dots ,\left\lvert x\right\rvert +1\} \) of the physical input head over the real input \(x\), arbitrary contents and head positions for the left tape block, and a natural number \(j\), the configuration of the buffered sequential composition of \(M_1\) and \(M_2\) on input \(x\) in the live administrative scan state, with the physical input head parked at \(p\), the left block carrying the given inactive data, the buffer storing \(y\) with its head at cell \(j - 1\), the right block blank with heads at the origin, and empty real output. The scan state is live even when \(j = 0\).
Let \(M_1\) and \(M_2\) be machines over the Boolean alphabet with finitely many states, let \(y\) be a Boolean word stored on the buffer, let \(p\) be a position of the physical input head over the real input \(x\), and fix arbitrary inactive contents and head positions for the left tape block. For every \(j \le \left\lvert y\right\rvert \), running the buffered sequential composition of \(M_1\) and \(M_2\) for exactly \(j + 1\) steps from the rewind-scan configuration with buffer head at cell \(j - 1\) yields the second-phase embedding of the initial configuration of \(M_2\) on virtual input \(y\), with arrival tag true, physical position \(p\), and the same inactive data. This includes the case of an empty word \(y\).
Let \(M_1\) and \(M_2\) be machines over the Boolean alphabet with finitely many states, and let \(c\) be a halted configuration of \(M_1\) on input \(x\) with output \(w\). Running the buffered sequential composition of \(M_1\) and \(M_2\) for exactly \(\left\lvert w\right\rvert + 2\) steps from the first-phase embedding of \(c\) yields the second-phase embedding of the initial configuration of \(M_2\) on virtual input \(w\), with arrival tag true, the physical input head parked where \(c\) left it, and the work tapes and head positions of \(c\) retained as inactive left-block data. The real output remains empty throughout.
Let \(M_1\) and \(M_2\) be machines over the Boolean alphabet with finitely many states, and suppose that \(M_1\), on input \(x\), halts within \(t_1\) steps with output \(y\). Then there exist a step count \(a \le t_1 + \left\lvert y\right\rvert + 2\), a position \(p\) of the physical input head over \(x\), and contents and head positions for the left tape block, such that running the buffered sequential composition of \(M_1\) and \(M_2\) for \(a\) steps from its initial configuration on \(x\) yields the second-phase embedding of the initial configuration of \(M_2\) on virtual input \(y\), with arrival tag true, physical position \(p\), and that inactive left-block data.
172.3 Additional declarations
Let \(M\) be a multi-tape Turing machine with \(k\) work tapes over the Boolean alphabet on input \(x\), with a start state \(r\), a scanning state \(s\), and an optional dispatch state \(d\), such that regardless of the symbols read: from \(r\) the machine always moves the input head left (clamped at the left boundary blank) and enters \(s\); from \(s\) it moves left and stays in \(s\) when an input symbol is scanned, and moves right and passes to \(d\) when a blank is scanned; and none of these transitions touches a work tape, a work head, or the output. Let \(c\) be a configuration of \(M\) in state \(r\) whose input head is at position \(p \in \{ 0,\dots ,\left\lvert x\right\rvert +1\} \), where position \(0\) is the left boundary blank. Then there exists \(t \le p + 2\) such that running \(M\) for \(t\) steps from \(c\) yields the configuration that agrees with \(c\) in every component except that its state is \(d\) and its input head is at position \(1\).