Let \(f\) be a function from binary strings to binary strings. If there exist a finite multi-tape Turing machine over the binary alphabet and a constant \(C\) such that the machine computes \(f\) within \(C\cdot (n+1)\) steps on every input of length \(n\), then \(f\) is polynomial-time computable.

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

Let \(p\) be a Boolean predicate on binary strings and \(f, g\) functions on binary strings. If the single-bit function \(x \mapsto [p(x)]\) and both \(f\) and \(g\) are polynomial-time computable, then so is the function mapping \(x\) to \(f(x)\) when \(p(x)\) holds and to \(g(x)\) otherwise.

Let \(p\) and \(q\) be Boolean predicates on binary strings. If the single-bit functions \(x \mapsto [p(x)]\) and \(x \mapsto [q(x)]\) are both polynomial-time computable, then so is \(x \mapsto [p(x) \wedge q(x)]\).

Let \(M\) and \(U\) be finite multi-tape Turing machines over the binary alphabet, let \(f, g\) be functions on binary strings and \(T_1, T_2 : \mathbb {N} \to \mathbb {N}\) time bounds. If \(M\) computes \(f\) within \(T_1\), and for every input \(x\) the machine \(U\) run on \(f(x)\) halts within \(T_2(|x|)\) steps with output \(g(x)\), then some finite machine computes \(g\) within time \(n \mapsto 2\, T_1(n) + T_2(n) + 2\).

For every binary string \(x\), the CNF formula decoded from \(x\) is satisfiable if and only if there exists a word \(u\) of length exactly \(|x| + 1\) such that the decoded formula evaluates to true under the assignment that reads variable \(v\) off the \(v\)-th bit of \(u\) (default false). [AB09, Theorem 2.10, membership]

If the certificate-split solver with parameters \((1,1)\), searching for a split of a total length \(N\), returns the value \(i\), then \(i + (i + 1) = N\).

If natural numbers \(i\) and \(N\) satisfy \(i + (i + 1) = N\), then the certificate-split solver with parameters \((1,1)\) on total length \(N\) succeeds and returns exactly \(i\); in particular this covers \(N = 1\), \(i = 0\).

For every CNF formula \(\varphi \), the Boolean width scan returns true if and only if \(\varphi \) has width at most \(3\), i.e. every clause of \(\varphi \) has at most three literals.

Let \(x\) and \(u\) be binary words with \(|u| = |x| + 1\). Then the verifier verdict on the concatenation \(x \mathbin {+\! \! +} u\) equals the conjunction of the (mode-guarded) width-three test of the formula decoded from \(x\) with the evaluation of that formula under the assignment read off \(u\).

A binary string \(x\) belongs to \(\mathrm{SAT}\) if and only if there exists a certificate \(u\) with \(|u| = |x| + 1\) such that the concatenation \(x \mathbin {+\! \! +} u\) belongs to the plain-mode verifier language.

A binary string \(x\) belongs to \(\mathrm{3SAT}\) if and only if there exists a certificate \(u\) with \(|u| = |x| + 1\) such that \(x \mathbin {+\! \! +} u\) belongs to the 3SAT-mode verifier language. The width condition depends only on the instance \(x\), so the same certificate as for \(\mathrm{SAT}\) suffices.

For every binary string \(x\), if the leading-ones scanner returns the count \(k\) and suffix \(s\), then \(x = 1^{k} \mathbin {+\! \! +} s\): the scanner partitions its input into the counted run of ones and the remaining suffix.

If the literal parser succeeds on a binary string \(x\), returning a literal \(\ell \) and a remainder \(r\), then \(x\) is exactly the serialization of \(\ell \) followed by \(r\).

If the fuel-indexed clause parser succeeds on a binary string \(x\), returning a clause \(C\) and a remainder \(r\), then \(x\) is exactly the serialization of \(C\) (including its terminator) followed by \(r\).

If the fuel-indexed formula parser succeeds on a binary string \(x\), returning a formula \(\varphi \) and a remainder \(r\), then \(x\) is exactly the serialization of \(\varphi \) — every clause marker and the final terminator — followed by \(r\).

If the exact-consumption CNF parser succeeds on a binary string \(x\), returning the formula \(\varphi \), then \(x\) equals the serialization of \(\varphi \).

For every scanner position \(q\), bit \(b\), and binary string \(x\): the string \(b :: x\) lies in the residual grammar of \(q\) if and only if \(x\) lies in the residual grammar of the position reached from \(q\) on reading \(b\).

The empty string lies in the residual grammar of a scanner position \(q\) if and only if \(q\) is the exact-end position.

For every scanner position \(q\) and binary string \(x\): \(x\) lies in the residual grammar of \(q\) if and only if folding the grammar transition over \(x\) starting at \(q\) ends in the exact-end position.

For every binary string \(x\), the Boolean syntax scan of \(x\) returns true exactly when the exact-consumption CNF parser succeeds on \(x\). This holds on every string, including the empty input, unfinished literals, and strings with trailing garbage.

Let a one-way scanner read input \(x\) in state \(q\) at position \(i \lt |x|\). One machine step moves silently to the state obtained by applying the transition to the \(i\)-th input bit, with the head advanced to position \(i+1\).

Let the input decompose as \(x = p \mathbin {+\! \! +} r\). Started in any state \(q\) at position \(|p|\), the one-way scanner halts after exactly \(|r| + 1\) steps with output the single bit obtained by applying the accepting predicate to the fold of the transition over \(r\) from \(q\); no earlier step emits.

Let \(S\) be a finite set with transition function \(\delta : S \times \{ 0,1\} \to S\), start state \(s_0 \in S\), and accepting predicate \(\alpha \) on \(S\). On every input \(x\) of length \(n\), the one-way scanner built from these data halts within \(n + 1\) steps, and its output is the single bit \(\alpha (\delta ^*(s_0, x))\), where \(\delta ^*(s_0, x)\) is the state reached by folding \(\delta \) over \(x\) from \(s_0\).

The single-bit function returning the Boolean result of the complete CNF syntax scan is polynomial-time computable; the witnessing machine is a one-way finite-state scanner, and the result concerns every input string, not merely serialized formulas.

In the canonical evaluation configuration at input position \(i\) on input \(w\), the symbol read by the input head is the optional \(i\)-th entry of \(w\); it does not depend on the saved extractor bank.

Let \(u\) be a certificate word and \(j \in \mathbb {Z}\). In every canonical evaluation configuration with certificate \(u\) and certificate head at offset \(j\), the symbol read by the last work head is the cell of the buffer tape of \(u\) at offset \(j\), that is, the \(j\)-th bit of \(u\) when \(0 \le j \lt |u|\) and the blank otherwise.

Applying a non-emitting administrative evaluator action to a canonical evaluation configuration yields the canonical configuration with the prescribed new control state, the input position moved as stated, and the certificate head displaced by the stated amount; the saved extractor bank and the empty output are preserved.

Let \(w\) be an input and \(i \lt |w|\). From a canonical evaluation configuration at input position \(i\) in a semantic state with phase \(q\), accumulator bits \(a\) and \(c\), and the skip flag set, one evaluator step yields the canonical configuration at position \(i + 1\) in the same phase with the same accumulator bits and the skip flag cleared; the certificate head, the saved bank, and the empty output are unchanged.

Suppose the evaluator’s transition at a semantic state on the current input bit is the administrative action moving right, displacing the certificate head by \(d\), and entering a new semantic state with the skip flag set. Then two machine steps — the semantic transition followed by its silent skip — consume the doubled input bit: the input position advances by two, the certificate head by \(d\), and the control reaches the new semantic state with the skip flag cleared. The certificate head moves only on the first of the two physical transitions.

Let \(q\) be an evaluator control state whose transition moves the certificate head left while its cell is occupied and otherwise steps right into a destination state. For every \(n \le |u|\), starting from the canonical configuration with certificate head at offset \(n - 1\), exactly \(n + 1\) steps return the head to offset \(0\) in the destination state, preserving all native input and output fields.

For every binary string \(x\), the doubled word has length exactly \(2\, |x|\).

Suppose the evaluator’s input contains, at the current position, the doubling of a unary run \(1^n\). In the index phase, exactly \(2n\) steps consume the doubled run, advancing the input position by \(2n\) and the certificate head by \(n\), leaving the phase and both accumulator bits unchanged. (The first one of a literal is consumed by the clause phase, so this scan counts the variable index itself.)

Suppose the evaluator’s input contains, at the current position, the doubling of a serialized literal \((v, b)\) with \(v \lt |u|\) for the certificate \(u\). Starting in the clause phase with clause bit \(c\), exactly \(3v + 8\) steps process the literal: the input advances by \(2(v + 3)\), the certificate head walks to position \(v\), the polarity is compared with the \(v\)-th certificate bit, the clause bit becomes \(c \vee (u_v = b)\), and the certificate head returns to \(0\).

Let \(u\) be the certificate word on the evaluator’s last tape and \(C\) a clause all of whose variable indices are below \(|u|\), with serialization \(\mathrm{ser}(C)\). Suppose the evaluator’s input is a word \(p\), followed by the doubling of \(\mathrm{ser}(C)\), followed by a word \(r\). Started at input position \(|p|\) in the clause phase with formula bit \(a\), clause bit \(c\), and certificate head at \(0\), there is a number \(t \le 3\, |\mathrm{ser}(C)|\) of steps after which the evaluator is in the formula phase with formula bit \(a \wedge (c \vee C(u))\), where \(C(u)\) is the truth value of \(C\) under the assignment read off \(u\), with the clause bit reset, input position \(|p| + 2\, |\mathrm{ser}(C)|\), and certificate head at \(0\). No output bit is emitted by this pass, even for an empty or false clause.

Let \(u\) be the certificate word on the evaluator’s last tape and \(\varphi \) a CNF formula all of whose variable indices are below \(|u|\), with serialization \(\mathrm{ser}(\varphi )\). Suppose the evaluator’s input is a word \(p\), followed by the doubling of \(\mathrm{ser}(\varphi )\), followed by a word \(r\). Started at input position \(|p|\) in the formula phase with formula bit \(a\), clause bit false, and certificate head at \(0\), there is a number \(t \le 3\, |\mathrm{ser}(\varphi )|\) of steps after which the evaluator is halted and its output is the single bit \(a \wedge \varphi (u)\), where \(\varphi (u)\) is the truth value of \(\varphi \) under the assignment read off \(u\); only the final formula terminator emits.

Let a finite multi-tape machine \(M\) compute output \(y\) on input \(x\) within \(T\) steps. Then there is a time \(t \le T\) such that \(M\) is still live at every time before \(t\), halts exactly at time \(t\), and its output at time \(t\) is \(y\): the first halting transition can be selected while retaining the final emission.

Let the extractor machine \(M\) compute the certificate \(u\) on input \(w\) within \(T\) steps. Then within \(T + |w| + |u| + 5\) steps from its initial configuration, the evaluator built over \(M\) reaches the canonical evaluation configuration: some saved bank of \(M\), the certificate \(u\) on the last tape with head at \(0\), the input head at \(0\), formula phase with formula bit true, and empty output.

There exist a single finite machine \(E\) and a constant \(A\) such that for every CNF formula \(\varphi \) and every certificate word \(u\) covering all variables of \(\varphi \) (each literal index below \(|u|\)), the machine \(E\), run on the pair encoding of the serialization of \(\varphi \) with \(u\), halts within \(A \cdot (\ell + 1)\) steps — \(\ell \) the length of that paired input — and outputs the single bit giving the truth value of \(\varphi \) under the assignment read off \(u\).

Let \(\varphi \) be a CNF formula, \(C\) a clause of \(\varphi \), and \(\ell \) a literal of \(C\). Then the variable index of \(\ell \) is strictly below the variable bound of \(\varphi \) (the maximum over all occurring indices \(v\) of \(v + 1\)).

For every binary string \(z\) there exist a CNF formula \(\varphi \) and a word \(u\) such that the safe evaluator request on \(z\) is exactly the pair encoding of the serialization of \(\varphi \) with \(u\), every variable index occurring in \(\varphi \) is below \(|u|\), and the truth value of \(\varphi \) under the assignment read off \(u\) equals the safe evaluation value of \(z\). This holds also on failed splits and failed parses.

The following four functions on binary strings are polynomial-time computable: the single-bit split-validity test, the instance projection, the single-bit syntax scan of the projected instance, and the safe evaluator request assembly.

The single-bit function sending a binary string \(z\) to its safe evaluation value is polynomial-time computable: the uniform evaluator is applied only on safe requests, which are certified serializations with covering certificates.

The single-bit function computing the plain-mode (SAT) verifier verdict on a binary string is polynomial-time computable: failed splits are rejected, failed parses take the accepting fallback branch, and all remaining inputs go through the safe evaluation pipeline.

For either mode flag: if the single-bit function computing the verifier verdict is polynomial-time computable, then the corresponding verifier language belongs to the class \(\mathrm{P}\).

For every \(n \in \mathbb {N}\), every counter value \(c\), and every flag \(g\), folding the width-pass transition over the unary run \(1^n\) from the index position with counter \(c\) and flag \(g\) returns exactly the same state: index bits change neither the position, nor the counter, nor the flag.

Let \(\ell \) be a literal, \(c \in \{ 0,1,2,3\} \) a counter value, and \(g\) a Boolean flag. Folding the width-pass transition over the serialization of \(\ell \), from the clause position with counter \(c\) and flag \(g\), returns the clause position with counter \(\min (c + 1, 3)\) and flag \(g \wedge [c \lt 3]\), independently of the variable index and polarity of \(\ell \).

Let \(C\) be a clause, \(c \in \{ 0,1,2,3\} \) a counter value, and \(g\) a Boolean flag. Folding the width-pass transition over the serialization of \(C\), from the clause position with counter \(c\) and flag \(g\), returns the formula position with counter \(0\) and flag \(g \wedge [c + |C| \le 3]\), where \(|C|\) counts literal occurrences including repetitions.

Folding the width-pass transition over the serialization of a CNF formula \(\varphi \) from the initial state ends at the exact-end position with counter zero and the goodness flag conjoined with the Boolean width-three test of \(\varphi \); every clause is checked and the empty formula passes vacuously.

For every CNF formula \(\varphi \), the width scan of the serialization of \(\varphi \) equals the Boolean width-three test of \(\varphi \), which is true exactly when every clause of \(\varphi \) has at most three literal occurrences.

The single-bit width-scan function is polynomial-time computable, realized by a one-way finite-state scanner with no work tapes and time exactly \(n + 1\).

The single-bit function computing the 3SAT-mode verifier verdict on a binary string is polynomial-time computable: the machine validates the entire syntax before running the width pass, and runs the evaluation pass only after width success; split failure rejects, while syntax failure accepts the empty fallback.

Let \(C\) be a clause and \(a, b\) two truth assignments that agree on the variable index of every literal occurring in \(C\). Then \(C\) evaluates identically under \(a\) and under \(b\).

For every head literal, remaining clause, and starting cursor \(n\), the cursor returned by the chain construction is at least \(n\): the fresh-variable allocator never moves backwards.

Every clause of the formula emitted by the chain construction has at most three literals.

Let \(a\) be a truth assignment satisfying the formula emitted by the chain construction on a head literal, remaining clause, and cursor. Then \(a\) satisfies the original clause (head followed by the remaining literals). No freshness hypothesis is needed in this direction.

Let a clause with head literal, a second literal \(b\), and a tail have all its variable indices below \(n\), and let \(a\) be an assignment satisfying it. Then there is an assignment \(a'\) agreeing with \(a\) below \(n\) such that \(a'\) satisfies both the link clause \([\mathrm{head},\, b,\, (n,\mathrm{true})]\) and the continuation clause headed by \((n,\mathrm{false})\) followed by the tail; the fresh value \(a'(n)\) is the truth of the tail under \(a\).

Let a clause (head plus remaining literals) have all variable indices below \(n\), and let \(a\) be an assignment satisfying it. Then there is an assignment \(a'\) agreeing with \(a\) on all indices below \(n\) that satisfies the formula emitted by the chain construction at cursor \(n\).

If every variable index of the input clause (head plus remaining literals) is below the starting cursor \(n\), then every variable index occurring in the formula emitted by the chain construction is below the returned cursor.

For every clause \(C\) and cursor \(n\), the cursor returned by splitting \(C\) at \(n\) is at least \(n\); this includes the empty clause.

For every clause \(C\) and cursor \(n\), every clause of the formula obtained by splitting \(C\) at \(n\) has at most three literals.

If every variable index of a clause \(C\) is below the cursor \(n\), then every variable index occurring in the formula obtained by splitting \(C\) at \(n\) is below the returned cursor.

Every truth assignment satisfying the formula obtained by splitting a clause \(C\) at some cursor also satisfies \(C\) itself.

Let a clause \(C\) have all variable indices below \(n\) and let \(a\) be an assignment satisfying \(C\). Then some assignment agreeing with \(a\) below \(n\) satisfies the formula obtained by splitting \(C\) at \(n\).

If every variable index occurring in a CNF formula \(\varphi \) is strictly below \(n\), then the variable bound of \(\varphi \) (the maximum of \(v + 1\) over occurring indices \(v\)) is at most \(n\).

For every CNF formula \(\varphi \) and cursor \(n\), the formula produced by the threaded clause transform of \(\varphi \) at \(n\) has width at most three.

Every truth assignment satisfying the threaded clause transform of a CNF formula \(\varphi \) also satisfies \(\varphi \) itself, with the same assignment.

Let a CNF formula \(\varphi \) have all variable indices below \(n\), and let \(a\) be an assignment satisfying \(\varphi \). Then some assignment agreeing with \(a\) on all indices below \(n\) satisfies the threaded clause transform of \(\varphi \) at cursor \(n\).

For every CNF formula \(\varphi \), the clause-splitting transform of \(\varphi \) is satisfiable if and only if \(\varphi \) is satisfiable. [AB09, Lemma 2.14]

For every binary string \(x\) — with no well-formedness hypothesis — \(x\) belongs to \(\mathrm{SAT}\) if and only if the image of \(x\) under the string-level reduction belongs to \(\mathrm{3SAT}\).

If the exact CNF parser fails on a binary string \(x\), then the string-level reduction maps \(x\) to the serialization of the (unchanged) empty formula.

For every clause \(C\), the serialization of \(C\) has length at least \(|C| + 1\), where \(|C|\) counts literal occurrences: there is room for every literal and the terminator.

Let \(x\) be an input and \(i \le |x|\). In every canonical reduction frame on input \(x\) at input position \(i\), the symbol read by the input head is the \(i\)-th bit of \(x\) when \(i \lt |x|\), and the blank when \(i = |x|\).

The unary counter tape of length \(n\) holds a one at every nonnegative offset \(j \lt n\) and a blank at every offset \(j \ge n\): its occupied cells are exactly its unary prefix.

The unary counter tape of any length is blank at offset \(-1\).

Let \(n, j \in \mathbb {N}\) with \(j \le n\). Writing a one at offset \(j\) of the unary counter tape of length \(n\) yields the unary counter tape of length \(\max (n, j + 1)\): writing within the current prefix preserves it, while writing its right blank extends the length by one.

Applying a two-tape reduction action to a canonical reduction frame yields the canonical frame whose input position, counter tape, buffer tape, both head offsets, and appended output are exactly as prescribed by the action’s components; this frame-level calculus is shared by the maximum pass and the streaming serializer.

If the transducer’s transition at the current state, input symbol, and work symbols is a silent action with no writes, then one machine step from the canonical reduction frame changes only the control state and the three head positions, as prescribed; the counter length, buffer, and output are unchanged.

Running the clause-splitting transducer for exactly one step from any configuration coincides with applying its single-step transition.

Let \(q\) be a transducer state whose transition moves the counter head left while its cell is occupied and otherwise steps right into a destination state. For every \(r \le n\), starting from the canonical frame with counter length \(n\) and counter head at offset \(r - 1\), exactly \(r + 1\) silent transitions reach the destination state with the counter head at \(0\); input position, buffer, and output are untouched.

Suppose the input contains a unary run \(1^v\) at the current position and the transducer is in its index-scanning state with counter length \(n\) and counter head at \(j \le n\). Then exactly \(v\) steps consume the run, advancing the input by \(v\), moving the counter head to \(j + v\), and extending the counter length to \(\max (n,\, j + v)\).

Suppose the input contains a serialized literal \((v,\mathrm{pol})\) at the current position and the transducer is in its clause-level maximum state with counter length \(n\) and counter head at \(0\). Then exactly \(2v + 5\) transitions consume the literal, record the counter length \(\max (n,\, v + 1)\), restore the counter head to \(0\), and return to the same state with the input advanced by \(v + 3\).

For lists of natural numbers \(a\) and \(b\), folding the maximum (with base \(0\)) over the concatenation \(a \mathbin {+\! \! +} b\) equals the maximum of the two separate folds.

The variable bound of a formula with first clause \(C\) and remaining clauses \(\varphi \) equals the maximum of the clause variable maximum of \(C\) with the variable bound of \(\varphi \).

Let \(C\) be a clause with serialization \(\mathrm{ser}(C)\), and let \(m_C\) be the maximum of \(v + 1\) over the literals \((v, b)\) of \(C\) (or \(0\) if \(C\) is empty). Suppose the input is \(x = p \mathbin {+\! \! +} \mathrm{ser}(C) \mathbin {+\! \! +} r\), and the transducer is in its clause-level maximum state at input position \(|p|\), with counter length \(n\), counter head at \(0\), and arbitrary buffer, buffer head, and output. Then there is a number \(t \le 2\, |\mathrm{ser}(C)|\) of silent steps after which the transducer is in formula-level maximum control at input position \(|p| + |\mathrm{ser}(C)|\), with counter length \(\max (n, m_C)\), counter head back at \(0\), and buffer, buffer head, and output unchanged.

Let \(\varphi \) be a CNF formula with serialization \(\mathrm{ser}(\varphi )\) and its variable bound \(N(\varphi )\) (one more than the largest variable index occurring in \(\varphi \), or \(0\) if no variable occurs). Suppose the input is \(x = p \mathbin {+\! \! +} \mathrm{ser}(\varphi ) \mathbin {+\! \! +} r\), and the transducer is in formula-level maximum control at input position \(|p|\), with counter length \(n\), counter head at \(0\), and arbitrary buffer, buffer head, and output. Then there is a number \(t \le 2\, |\mathrm{ser}(\varphi )|\) of silent steps after which the transducer is at its rewind seam at input position \(|p| + |\mathrm{ser}(\varphi )| - 1\), with counter length \(\max (n, N(\varphi ))\), counter head at \(0\), and buffer, buffer head, and output unchanged.

The literal buffer holding the empty word with cut \(0\) is the all-blank tape updated with the permanent marker at offset \(-1\).

For every input \(x\), the first two steps of the clause-splitting transducer from its initial configuration on \(x\) are silent and yield the canonical frame in the maximum-pass entry state with input head at \(0\), empty counter, the empty marked buffer (blank except for the permanent marker at offset \(-1\)), both work heads at \(0\), and empty output.

Let \(\varphi \) be a CNF formula with serialization \(\mathrm{ser}(\varphi )\) and its variable bound \(N(\varphi )\) (one more than the largest variable index occurring in \(\varphi \), or \(0\) if no variable occurs). There is a time \(t \le 3\, |\mathrm{ser}(\varphi )| + 5\) at which the clause-splitting transducer, started on \(\mathrm{ser}(\varphi )\), is in its streaming entry state with exactly \(1^{N(\varphi )}\) on the counter tape, the buffer empty apart from its permanent marker, the input head back at \(0\), both work heads at \(0\), and empty output.

For every literal \(\ell \) and remainder word \(r\), the literal parser applied to the serialization of \(\ell \) followed by \(r\) succeeds and returns exactly \((\ell , r)\).

Running \(m + n\) streaming rounds from a state equals running \(m\) rounds, then \(n\) further rounds from the intermediate state, with the two output words concatenated.

For every input \(x\), every \(k \in \mathbb {N}\), and every seam state in the finished phase, running \(k\) streaming rounds returns the same state and the empty output: padding after the formula terminator contributes no further output.

For literals \(a, b\), a clause tail \(C\), and a cursor \(j\): concatenating a clause marker with the serialization of each clause of the chain construction on \(a\), \(b :: C\), \(j\) yields exactly one marker followed by the serializations of \(a\) and \(b\) and the pending tail output of \(C\) at \(j\); moreover the chain’s returned cursor equals the tail’s final cursor.

For every clause \(C\) and cursor \(j\): concatenating a clause marker with the serialization of each clause of the split of \(C\) at \(j\) yields exactly one marker followed by the emitted clause body of \(C\) at \(j\), and the split’s returned cursor equals the body’s final cursor. This includes the empty clause and all clauses of width at most three.

Let the input be \(p \mathbin {+\! \! +} 0 :: r\) and the seam state have consumed \(|p|\) bits in a non-finished phase \(q\). The round emits \([0]\), consumes one bit, and moves to the finished phase when \(q\) was the formula phase and back to the formula phase otherwise.

Let the input be \(p \mathbin {+\! \! +} 1 :: r\) and the seam state have consumed \(|p|\) bits in the formula phase. The round emits \([1]\), consumes one bit, and moves to the first-literal phase.

Let the input be \(p\) followed by a serialized literal \(\ell \) and a remainder \(r\), and let the seam state have consumed \(|p|\) bits in a literal phase (neither formula nor finished). If the phase is the tail phase and \(r\) starts with a clause bit \(1\), the round allocates the fresh cursor \(j\): it emits the positive link \((j,\mathrm{true})\), two markers, the negative literal \((j,\mathrm{false})\), and \(\ell \), incrementing the cursor; otherwise it emits \(\ell \) verbatim and advances the phase. In both cases the consumed length advances by the serialized literal length, so no literal buffer survives a round boundary.

Let the input contain a serialized clause tail \(C\) at the consumed position, with the seam in the tail phase at cursor \(j\). Then exactly \(|C| + 1\) rounds — one per remaining literal plus one for the clause terminator — consume the serialized tail, emit exactly the pending tail output of \(C\) at \(j\), return to the formula phase, and leave the cursor at the tail’s final value.

Let the input contain a serialized clause \(C\) at the consumed position, with the seam in the first-literal phase at cursor \(j\). Then exactly \(|C| + 1\) rounds consume the serialized clause, emit exactly the emitted clause body of \(C\) at \(j\), return to the formula phase, and leave the cursor at the body’s final value.

Let the input contain the serialization of a formula \(\varphi \) at the consumed position, with the seam in the formula phase at cursor \(j\). Then exactly the round count of \(\varphi \) many rounds consume the serialized formula, emit exactly the serialization of the threaded clause transform of \(\varphi \) at \(j\), reach the finished phase, and leave the cursor at the transform’s final value.

For every CNF formula \(\varphi \), the round count of \(\varphi \) is at most the length of the serialization of \(\varphi \): every non-finished round consumes at least one input bit, including for empty clauses and the empty formula.

Let \(\varphi \) be a CNF formula with serialization \(\mathrm{ser}(\varphi )\) and its variable bound \(N(\varphi )\) (one more than the largest variable index occurring in \(\varphi \), or \(0\) if no variable occurs). Running \(|\mathrm{ser}(\varphi )| + 1\) streaming rounds on input \(\mathrm{ser}(\varphi )\), starting from the formula phase with fresh cursor \(N(\varphi )\) and nothing consumed, emits a word equal to the serialization of the clause-splitting transform of \(\varphi \): the semantic schedule finishes within the budget and all remaining rounds are empty.

For every input \(x\), round count \(k\), and seam state \(s\), the output of \(k\) streaming rounds equals the concatenation over \(i \lt k\) of the chunk emitted by the round applied to the \(i\)-fold iterate of the next-state map on \(s\) — the range-indexed form required by the emitting-loop contract.

For every seam state \(s\), decoding the encoded seam word of \(s\) returns exactly \(s\): the fresh cursor, the consumed length, and the phase are all recovered.

For every seam state with fresh cursor \(f\), consumed length \(c\), and phase \(q \in \{ 0, \dots , 4\} \), the encoded seam word has length exactly \(2f + 2c + q + 4\); in particular it is linear in the two unary counters.

If a seam state satisfies the length invariant on an input \(x\), then so does the state after one streaming round — including on malformed local inputs, where finished and failure cases preserve the counters.

If a seam state satisfies the length invariant on an input \(x\), then its fresh cursor is at most \(2\, |x|\) and its encoded seam word has length at most \(6\, |x| + 8\).

For every input string \(x\), the startup seam state of \(x\) satisfies the length invariant on \(x\); this holds both for the valid and for the fallback startup state.

Any positive number of streaming rounds from the right-boundary fallback state emits exactly the single bit \(0\): no prefix of the malformed string is emitted, including on trailing-data failures.

For every binary string \(x\), running \(|x| + 1\) streaming rounds from the startup seam state of \(x\) emits exactly the image of \(x\) under the string-level SAT-to-3SAT reduction. This is an exact output identity on every string, prior to any machine-computability claim.

For every input string \(x\), the encoded startup seam word of \(x\) satisfies the encoded loop invariant.

If a word satisfies the encoded loop invariant on an input \(x\), then so does its image under the encoded next-state function.

For every input \(x\), seam state \(s\), and \(k\), the \(k\)-fold iterate of the encoded next-state function on the encoded word of \(s\) equals the encoded word of the \(k\)-fold iterate of the structured round map on \(s\).

For every binary string \(x\), concatenating over \(i \lt |x| + 1\) the chunks produced by the encoded chunk function at the \(i\)-fold iterate of the encoded next-state function on the encoded startup word equals the image of \(x\) under the string-level SAT-to-3SAT reduction — exactly the expression returned by the emitting-loop constructor with round budget \(R(n) = n\).

Let \(M\) be a finite machine, \(x\) an input, and \(i \le |x|\). In every canonical pairing configuration over \(M\) on input \(x\) at input position \(i\), the symbol read by the input head is the \(i\)-th bit of \(x\) when \(i \lt |x|\), and the blank when \(i = |x|\).

Let \(M\) be a finite machine, \(u\) a captured word, and \(j \in \mathbb {Z}\). In every canonical pairing configuration over \(M\) with captured word \(u\) and capture head at offset \(j\), the symbol under the last work head is the cell of the buffer tape of \(u\) at \(j\), that is, the \(j\)-th bit of \(u\) when \(0 \le j \lt |u|\) and the blank otherwise.

Applying a pairing administrative action to a canonical pairing configuration changes only the control state, the two displayed head positions, and the output (appending the optionally emitted bit); the saved source bank and the captured word are preserved.

For every \(n \le |u|\): from the canonical pairing configuration in the capture-rewind state with the capture head at offset \(n - 1\) and empty output, exactly \(n + 1\) steps return the head to the origin and enter the replay state, with all other fields unchanged.

Let the source machine \(M\) compute the word \(u\) on input \(x\) within \(T\) steps. Then within \(T + |x| + |u| + 5\) steps from its initial configuration, the pairing machine over \(M\) reaches the canonical pairing configuration at the replay entry: some saved bank of \(M\), the captured word \(u\) with head at the origin, the input head at the origin, and all startup output suppressed.

Let the captured word decompose as \(u = p \mathbin {+\! \! +} r\) with the capture head at offset \(|p|\) in the replay state. Then exactly \(2\, |r| + 2\) steps emit the doubling of \(r\) followed by the separator \(01\), move the capture head to \(|u|\), and enter the native-copy state; the source bank and the native input head remain fixed.

Let the native input decompose as \(x = p \mathbin {+\! \! +} r\) with the pairing machine in its native-copy state at input position \(|p|\). Then exactly \(|r| + 1\) steps emit every bit of \(r\) and halt on the right blank, leaving all work tapes and the capture head unchanged.

Let the machine \(M\) compute a function \(f\) within time \(T\). Then the pairing machine over \(M\) computes the function \(x \mapsto \mathrm{pair}(f(x), x)\) within time \(n \mapsto 4\, T(n) + 2n + 8\): retaining a computed result next to its original input has a uniform overhead, the capture output length being paid by the source time.

If a function \(f\) on binary strings is polynomial-time computable, then so is the function \(x \mapsto \mathrm{pair}(f(x), x)\) pairing the computed value with the original input.

If a function \(g\) on binary strings is polynomial-time computable, then so is the function that decodes its input as a pair \((a, b)\), returns the pair encoding of \(a\) with \(g(b)\), and returns the empty word when the input is not a valid pair encoding.

If \(f\) and \(g\) are polynomial-time computable functions on binary strings, then so is \(x \mapsto \mathrm{pair}(f(x), g(x))\): independently computed fields can be paired without losing the original input needed by the second computation.

If \(f\) and \(g\) are polynomial-time computable functions on binary strings, then so is \(x \mapsto f(x) \mathbin {+\! \! +} g(x)\).

Let the input decompose as \(x = p \mathbin {+\! \! +} r\). From any state \(q\) at position \(|p|\) with emitted prefix \(o\), the word-transducer machine halts after exactly \(|r| + 1\) steps with output \(o\) followed by the transducer semantics applied to \(q\) and \(r\).

For every finite state set with transition, per-bit emission, final emission, and start state, the associated word-transducer function on binary strings is polynomial-time computable, with the exact time bound \(n + 1\).

The function replacing every bit of its input by \(1\) — computing the exact unary representation of the input length — is polynomial-time computable.

The function removing the first bit of a binary string (returning the empty word on the empty string) is polynomial-time computable, as a two-state finite transduction.

The function extracting at most the first bit of a binary string (the length-one prefix) is polynomial-time computable, as a two-state finite transduction.