Savitch's theorem

Reachability within $2^k$ steps can be tested by enumerating a midpoint and recursively testing two half-paths. Configurations have $O(s)$ bits and recursion depth $O(s)$, yielding deterministic space $O(s^2)$. The space-bound discovery by exit reachability permits this simulation without assuming that the supplied function $s$ is constructible.