Savitch simulation into read-only-input deterministic work space

On input $x$, encode a configuration by its state, input-head position, work contents, and work-head positions. There are only polynomially many syntactically possible encodings, by the same finite product count used in [L2]. Choose $r=O(\log (n+2))$ with $2^r$ at least that number.

Define $R(C,D,0)$ to test whether $C=D$ or $C\to D$ is one legal transition, and define $R(C,D,j+1)$ by enumerating every configuration $E$ and accepting exactly if both $R(C,E,j)$ and $R(E,D,j)$ hold. Induction on $j$ shows that it decides reachability by a path of length at most $2^j$.

A recursion frame stores $C,D,E$ and $j$, each using $O(\log (n+2))$ work bits; there are $r+1=O(\log (n+2))$ frames. Adjacency is recomputed from $M$ and the read-only input, never stored as a graph.

Enumerate accepting configurations $D$ and run $R(C_{\mathrm{s}\mathrm{t}\mathrm{a}\mathrm{r}\mathrm{t}},D,r)$. By step 2.1 this accepts exactly when $M$ has an accepting branch, and by step 3.1 it uses $O({\log }^2(n+2))$ charged work space.