The embedded NTM follows the same run on every choice sequence; its uniform time bound is the largest halting time over the finitely many inputs of each length. Monotonicity is transitivity of \(O\).

Every head moves at most one cell per step and a decider in time \(f\) halts within \(f(|x|)\) steps, so every reachable configuration of the same machine is within decision space \(f(|x|)\). The nondeterministic statements compose this with Lemma 201.

Run the decider, rewind the output head to the verdict cell, and flip the bit. The rewind costs one extra cell, so the new machine decides the complement in space \(f + 1\); the delicate point is that the space predicate constrains every reachable configuration, not only the last.

Unfold the union and replace the asymptotic bound by a dominating polynomial. The iteration lemma, Savitch’s theorem, and the \(\mathsf{PP} \subseteq \mathsf{PSPACE}\) and \(\mathsf{PH} \subseteq \mathsf{PSPACE}\) machines enter \(\mathsf{PSPACE}\) through the converse direction.

The finite-state scanner of Theorem 105 has no work tapes, never moves its input head past the first blank after the input, and never moves its output head past the verdict cell, so it decides the language in space \(0\). Its output head never moves left, so it is also a transducer, as membership in \(\mathsf{L}\) requires. For the other models, CSLib first shows that the language is regular.

For a one-way output tape the written prefix cannot influence future execution, so a halting run cannot repeat a reduced snapshot.

The same machine runs within the reduced-snapshot bound, which is polynomial for logarithmic space. The same argument places every language of \(\mathsf{L}\) in \(\bigcup _k \mathsf{DTISP}(n^k, \log n) \subseteq \mathsf{SC}\), with the same machine as witness; that corollary is not yet stated in the library.

Every configuration of the run is windowed, so distinct configurations of the run have distinct codes, and a deterministic halting run visits no configuration twice before it halts. The halting time is therefore below the number of codes, and the same machine decides the language in exponential time.

A log-space machine has polynomially many configuration codes inside its window, so breadth-first search saturates within polynomially many rounds.

The worklist search over encoded configurations is programmed in Cobham’s function algebra and run for polynomially many rounds, and the verdict function gives membership in \(\mathsf{P}\). The \(\mathsf{coNL}\) case follows because \(\mathsf{P}\) is closed under complement; it does not use the Immerman–Szelepcsényi theorem.

A subset of a finite set that is at least as large is the whole set; the codes are the fixed-width configuration codes of Definition 207.

Complement both sides of the inclusion.

Apply the hypothesis to the machine and bounds supplied by Lemma 211; the decided set is exactly the complement.

It remains to build the counting machine required by Proposition 215: a nondeterministic log-space machine that guesses the certificate of Lemma 213 entry by entry, with three nested bounded loops (rounds, codes of a round, steps of a walk) over a constant number of logarithmically wide registers. The planned route builds it deterministically over a guess tape and converts it to an NTM. The statement \(\mathsf{NL} \subseteq \mathsf{coNL}\) is recorded as the proposition NLSubsetCoNL.

The machine stores only the current state and a binary iteration counter of polynomially many bits, applies \(G\) in place until the done flag appears, and publishes the verdict after one more application. This is the polynomial-space counterpart of the iteration lemma for \(\mathsf{FP}\) in Cobham’s algebra.

A walk longer than the number of codes repeats a configuration, and the loop can be cut out; halving splits a walk at its midpoint. For (3), membership is reachability of an accepting configuration, and the configuration codes number at most \(2\) to a polynomial.

Savitch’s recursion is written as a stack machine whose single step is a polynomial-time function, built in Cobham’s algebra, on a polynomially long encoded stack; the midpoint enumeration ranges over every string of the configuration-code width. The step is iterated \(2^{\mathrm{poly}}\) times by Lemma 217. The reverse inclusion is the embedding of DTMs into NTMs. No bound of the form \(O(S^2)\) is extracted.

The formalized theorem is only the polynomial-union corollary. The parametric form needs the recursion to run in space \(O(S^2)\) with \(S\) computed in space \(O(S)\), rather than through a polynomial-time step function.

Depth-first evaluation with a stack of at most \(d(|x|)\) frames, each holding a node, a child cursor and an accumulator. One step of the walk is polynomial time, so Lemma 217 applies. Instances: Savitch’s theorem (an \(\vee \) over midpoints of an \(\wedge \) of two subcalls), \(\mathsf{IP} \subseteq \mathsf{PSPACE}\) (maximum over prover replies, sum over verifier messages), \(\mathsf{PH} \subseteq \mathsf{PSPACE}\) (\(\vee \) and \(\wedge \) over witnesses), \(\mathsf{PP} \subseteq \mathsf{PSPACE}\) (a sum over choice sequences), \(\mathsf{TQBF} \in \mathsf{PSPACE}\), and \(\mathsf{NP} \cup \mathsf{coNP} \subseteq \mathsf{PSPACE}\), which is not yet stated. Today Savitch’s theorem and \(\mathsf{IP} \subseteq \mathsf{PSPACE}\) each program their own stack walk on Lemma 217, and \(\mathsf{PH} \subseteq \mathsf{PSPACE}\) and \(\mathsf{PP} \subseteq \mathsf{PSPACE}\) assemble dedicated machines; one generic theorem would subsume all four.

Structural induction on the formula.

Each quantifier is a binary node of a game tree of depth at most the formula size.

Hardness: express “\(c\) reaches \(c'\) within \(2^i\) steps” by a formula that quantifies universally over the pair of halves, so its size is linear in \(i\) rather than exponential, over a formula for one step between configuration codes.

\(\mathsf{AP} \subseteq \mathsf{PSPACE}\) is an instance of game-tree evaluation; \(\mathsf{PSPACE} \subseteq \mathsf{AP}\) follows by evaluating TQBF alternately, or directly by alternating Savitch’s midpoint recursion.

Diagonalize against machines with a space-bounded universal simulation, reusing the diagonal-machine infrastructure of the time hierarchy theorem.

Closure of nondeterministic space under complement, by inductive counting, makes the diagonal argument go through.

(1) is induction along the reachable configurations. For (2), the run halts within \(b\) steps, so every reachable configuration is at most \(b\) steps from its start, and each step moves each head by at most one cell. For (4), the time component is Theorem 17; the first phase is covered by the contract of \(M_1\), and the normalized start of \(M_2\) and everything after it by the contract of \(M_2\).

The recomputation argument: simulate the machine for \(g\), keeping the position of its virtual input head in a binary counter, and whenever it reads bit \(j\) of \(f(x)\), rerun the machine for \(f\) from the start, discarding output until position \(j\). By \(\mathsf{FL} \subseteq \mathsf{FP}\), \(|f(x)|\) is polynomial, so the counters need \(O(\log n)\) bits. Under the library’s convention the virtual input head may travel one cell past \(f(x)\) for free and is charged beyond that.

Transitivity and closure of \(\mathsf{L}\) are Theorem 234; closure of \(\mathsf{NL}\) is the same recomputation with a nondeterministic outer machine.

The reduction writes out the configuration graph of the log-space machine on the given input, one adjacency bit at a time.

Each register becomes a binary work tape, input access becomes a seek driven by a counter, and loops become binary counters, reusing the Hoare-style binary-counter subroutines and the space-aware contracts of Lemma 233. The counting machine of Theorem 216 and the tableau serializer would then be written as programs.