[proofplan] Take a deterministic decider for $L$ whose work-tape space is bounded by a constant multiple of $f(n)$. Construct a new deterministic machine that performs the same computation on the same input but interchanges the accepting and rejecting halting states. Determinism and total halting are preserved by this construction, and the simulation uses exactly the same work tapes up to fixed finite-control overhead. [/proofplan] [step:Choose a deterministic space-bounded decider for $L$] Since $L \in \operatorname{SPACE}(f(n))$, there exist a deterministic Turing machine $M$, constants $C > 0$ and $n_0 \in \mathbb{N}$, such that $M$ halts on every input $w \in \Sigma^*$, decides membership in $L$, and uses at most $C f(|w|)$ work-tape cells whenever $|w| \ge n_0$. Thus, for every $w \in \Sigma^*$, the machine $M$ accepts $w$ if and only if $w \in L$, and rejects $w$ if and only if $w \notin L$. [/step] [step:Construct the complement decider by reversing halting answers] Define a deterministic Turing machine $M'$ as follows. On input $w \in \Sigma^*$, the machine $M'$ simulates $M$ on the same input $w$ using the same work-tape configuration. If the simulated computation of $M$ enters an accepting halting state, then $M'$ enters a rejecting halting state. If the simulated computation of $M$ enters a rejecting halting state, then $M'$ enters an accepting halting state. Because $M$ is deterministic, each simulated configuration has a unique successor configuration, so $M'$ is deterministic. Because $M$ halts on every input, the simulation performed by $M'$ also reaches one of these two halting cases on every input. [guided] We build $M'$ by changing only the final answer of $M$, not the computation leading to that answer. Formally, on input $w \in \Sigma^*$, the machine $M'$ runs the same transition sequence that $M$ would run on $w$ until $M$ reaches a halting state. At that point, $M'$ reverses the outcome: an accepting halt of $M$ becomes a rejecting halt of $M'$, and a rejecting halt of $M$ becomes an accepting halt of $M'$. Why is this a legitimate deterministic machine? The original machine $M$ is deterministic, so from any configuration of $M$ there is at most one next configuration. The simulator $M'$ follows exactly that unique next configuration during the simulation phase, and its only additional rule is the fixed reversal of the final halting answer. Hence $M'$ also has at most one next move from each configuration. Why does $M'$ halt? The hypothesis says that $M$ is a decider, not merely a recognizer, so for every input $w \in \Sigma^*$ the computation of $M$ on $w$ eventually reaches either an accepting halting state or a rejecting halting state. Since $M'$ simulates that same computation until this halting state is reached, $M'$ also halts on every input. [/guided] [/step] [step:Verify that the new machine decides the complement language] Let $w \in \Sigma^*$ be arbitrary. If $w \in \overline{L}$, then $w \notin L$, so $M$ rejects $w$. By the construction of $M'$, the machine $M'$ accepts $w$. Conversely, if $M'$ accepts $w$, then the simulated computation of $M$ rejected $w$, so $w \notin L$, and therefore $w \in \overline{L}$. Hence $M'$ accepts exactly the strings in $\overline{L}$. [/step] [step:Check that the space bound is unchanged up to constant overhead] On input $w \in \Sigma^*$ with $|w| \ge n_0$, the simulation uses the same work-tape cells that $M$ uses on $w$, namely at most $C f(|w|)$ cells. The reversal of the final answer is encoded in the finite control of $M'$ and therefore adds no asymptotic work-tape space. Thus $M'$ uses $O(f(n))$ work-tape space on inputs of length $n$. Since $M'$ is a deterministic decider for $\overline{L}$ using $O(f(n))$ space, we conclude that $\overline{L} \in \operatorname{SPACE}(f(n))$. [/step]