[proofplan] We convert a nondeterministic space-bounded computation into reachability in its implicit configuration graph. The graph has exponentially many vertices in the space bound, but each vertex has an encoding of length $O(f(n))$, so deterministic reachability can be solved by Savitch's divide-and-conquer recursion while storing only one recursion stack. The recursion has depth $O(f(n))$ and each frame uses $O(f(n))$ space, giving total deterministic space $O(f(n)^2)$. [/proofplan]

[step:Encode the nondeterministic computation as an implicit configuration graph] Let $L \in \operatorname{NSPACE}(f(n))$. Then there is a nondeterministic Turing machine $M$ and a constant $c_0 \ge 1$ such that, on every input $x \in \{0,1\}^*$ of length $n$, every computation branch of $M$ uses at most $c_0 f(n)$ work-tape cells and halts with either acceptance or rejection. For this fixed input $x$, define the configuration graph $G_{M,x}$ as follows. A vertex is a complete instantaneous description of $M$ on input $x$ using at most $c_0 f(n)$ work-tape cells: it records the finite control state, the input-head position, the work-tape-head positions, and the work-tape contents. There is a directed edge from a configuration $C$ to a configuration $D$ exactly when one legal transition of $M$ can take $C$ to $D$. Because $M$ has fixed finite alphabets, a fixed finite set of states, and only $O(f(n))$ work-tape cells, there is a constant $c_1 \ge 1$, depending only on $M$, such that every configuration of $M$ on input length $n$ can be encoded by a binary string of length $m(n) := c_1 f(n)$. The hypothesis $f(n) \ge \lceil \log_2 n \rceil$ ensures that the input-head position, which needs $O(\log n)$ bits, is included within this bound. Hence the number of encoded configurations is at most $2^{m(n)} = 2^{c_1 f(n)}$. [/step]

[step:Add a single accepting sink so acceptance is one reachability question] Define an augmented directed graph $H_{M,x}$ by adding one formal vertex $q_{\mathrm{acc}}$ to $G_{M,x}$. We represent $q_{\mathrm{acc}}$ by one reserved binary string of length $m'(n) := c_2 f(n)$, where $c_2 \ge c_1$ is chosen large enough that all ordinary configurations and the reserved sink code have length $m'(n)$. The vertices of $H_{M,x}$ are the ordinary configurations of $M$ on $x$ together with $q_{\mathrm{acc}}$. The directed edges are the original one-step transition edges of $G_{M,x}$, together with one edge from each accepting configuration of $M$ to $q_{\mathrm{acc}}$. The vertex $q_{\mathrm{acc}}$ has no outgoing edges. Let $C_{\mathrm{start}}(x)$ denote the start configuration of $M$ on input $x$. Then $M$ accepts $x$ if and only if $q_{\mathrm{acc}}$ is reachable from $C_{\mathrm{start}}(x)$ in $H_{M,x}$. Indeed, an accepting branch of $M$ reaches an accepting configuration and then follows the added edge to $q_{\mathrm{acc}}$; conversely, the only incoming edges to $q_{\mathrm{acc}}$ come from accepting configurations. [/step]

[step:Define the deterministic reachability recursion]For encoded vertices $a,b \in \{0,1\}^{m'(n)}$ and an integer $\ell \ge 0$, define the predicate $R(a,b,\ell)$ to mean that there is a directed path in $H_{M,x}$ from $a$ to $b$ of length at most $\ell$. A deterministic procedure $\operatorname{Reach}(a,b,\ell)$ decides $R(a,b,\ell)$ recursively: If $\ell = 0$, it accepts exactly when $a=b$. If $\ell = 1$, it accepts exactly when $a=b$ or there is a directed edge from $a$ to $b$ in $H_{M,x}$. If $\ell \ge 2$, it enumerates all binary strings $z \in \{0,1\}^{m'(n)}$ and accepts if, for some such $z$, both $\operatorname{Reach}(a,z,\lfloor \ell/2 \rfloor)$ and $\operatorname{Reach}(z,b,\lceil \ell/2 \rceil)$ accept. The edge test used in the case $\ell = 1$ is deterministic and uses $O(f(n))$ space: it checks whether the two strings encode legal configurations related by one transition of $M$, or whether the first string encodes an accepting configuration and the second string is the reserved code for $q_{\mathrm{acc}}$.[/step]

[guided]The point of the recursion is to avoid storing a whole path. A path of length at most $\ell$ from $a$ to $b$ exists exactly when there is some midpoint vertex $z$ such that the first part of the path goes from $a$ to $z$ in at most $\lfloor \ell/2 \rfloor$ steps and the second part goes from $z$ to $b$ in at most $\lceil \ell/2 \rceil$ steps. We define $R(a,b,\ell)$ formally as the assertion that $H_{M,x}$ contains a directed path from the encoded vertex $a$ to the encoded vertex $b$ of length at most $\ell$. The recursive procedure $\operatorname{Reach}(a,b,\ell)$ is designed to decide exactly this predicate. For $\ell = 0$, the only path of length at most $0$ is the empty path, so $R(a,b,0)$ holds exactly when $a=b$. For $\ell = 1$, a path of length at most $1$ is either the empty path or one directed edge. Thus $\operatorname{Reach}(a,b,1)$ accepts exactly when $a=b$ or when the deterministic edge predicate confirms that $a \to b$ is an edge of $H_{M,x}$. This edge predicate is space-bounded because it only compares two configurations and verifies one local transition rule of the fixed machine $M$. For $\ell \ge 2$, suppose first that there is a path from $a$ to $b$ of length at most $\ell$. Choose a vertex $z$ on that path after at most $\lfloor \ell/2 \rfloor$ edges; if the path is shorter, take $z$ to be the endpoint reached at that time or the final vertex once the path has ended. Then the initial segment gives a path from $a$ to $z$ of length at most $\lfloor \ell/2 \rfloor$, and the remaining segment gives a path from $z$ to $b$ of length at most $\lceil \ell/2 \rceil$. Hence both recursive calls accept for this $z$. Conversely, if for some encoded string $z$ both recursive calls accept, then there is a path from $a$ to $z$ of length at most $\lfloor \ell/2 \rfloor$ and a path from $z$ to $b$ of length at most $\lceil \ell/2 \rceil$. Concatenating these two directed paths gives a path from $a$ to $b$ of length at most $\lfloor \ell/2 \rfloor + \lceil \ell/2 \rceil = \ell$. Therefore the recursion decides $R(a,b,\ell)$.[/guided]

[step:Bound the space used by the recursion] Let $N(n) := 2^{m'(n)}$. Every vertex code, midpoint code, and counter value used by the recursion has length $O(f(n))$, since $\log_2 N(n) = m'(n) = c_2 f(n)$. One recursion frame stores the current vertices $a,b$, the current midpoint candidate $z$, the current length bound $\ell$, and a constant amount of control information. Thus one frame uses $O(f(n))$ space. At each recursive call, the length parameter is replaced by either $\lfloor \ell/2 \rfloor$ or $\lceil \ell/2 \rceil$. Starting from $\ell = N(n)$, the recursion depth is at most $\lceil \log_2 N(n) \rceil + 1 = c_2 f(n) + 1$. Therefore the recursion stack uses $O(f(n)) \cdot O(f(n)) = O(f(n)^2)$ space. The deterministic edge test uses only $O(f(n))$ additional space, which is absorbed by the same bound. [/step]

[step:Run the simulator and conclude the space inclusion] Because $f$ is space-constructible, the deterministic simulator can compute a work bound proportional to $f(n)$ and therefore can allocate and address the $m'(n) = c_2 f(n)$-bit configuration fields and the $O(f(n))$-bit counters used above. The simulator for $L$ on input $x$ computes the start configuration code $C_{\mathrm{start}}(x)$, the reserved accepting-sink code $q_{\mathrm{acc}}$, and runs $\operatorname{Reach}(C_{\mathrm{start}}(x), q_{\mathrm{acc}}, N(n))$. The graph $H_{M,x}$ has at most $N(n)$ vertices, because every ordinary configuration and the accepting sink is represented by a binary string of length $m'(n)$. If $q_{\mathrm{acc}}$ is reachable from $C_{\mathrm{start}}(x)$, then deleting repeated vertices from any directed path gives a simple directed path of length at most $N(n)-1$, hence of length at most $N(n)$. Thus the call with length bound $N(n)$ detects exactly the relevant reachability relation. If $M$ accepts $x$, then some accepting computation branch reaches an accepting configuration, and the added sink edge gives a path from $C_{\mathrm{start}}(x)$ to $q_{\mathrm{acc}}$. If the reachability procedure accepts, then such a path exists, and the last edge into $q_{\mathrm{acc}}$ must come from an accepting configuration of $M$, so $M$ has an accepting branch on $x$. Thus the deterministic simulator decides exactly $L$. By the space estimate above, it uses $O(f(n)^2)$ space. Since $L \in \operatorname{NSPACE}(f(n))$ was arbitrary, we obtain $\operatorname{NSPACE}(f(n)) \subseteq \operatorname{SPACE}(f(n)^2)$. [/step]