[proofplan] We count the data needed to specify a configuration of $M$ on an input $x$ of length $n$. The control state contributes a constant factor; the input-head positions contribute a polynomial factor in $n$; and the work-tape contents and work-tape head positions contribute an exponential factor in $s(n)$. Since $s(n) \geq \log_2 n$, every polynomial factor in $n$ is absorbed into $2^{O(s(n))}$, and multiplying the finitely many factors gives the desired bound. [/proofplan] [step:Fix the machine-dependent constants that describe configurations] Let $Q$ be the finite set of internal states of $M$, and let $q := |Q|$. Let $a \in \mathbb{N}$ be the number of input tapes of $M$, and let $b \in \mathbb{N}$ be the number of work tapes of $M$. Let $\Gamma$ denote a finite alphabet containing every symbol that can appear on any work tape of $M$, and let $\gamma := |\Gamma|$. If the model already uses a common work-tape alphabet, this is that alphabet; if different work tapes have different finite alphabets, $\Gamma$ is their finite union. For an input $x$ of length $n$, a configuration of $M$ on $x$ is determined by the following finite data: one state in $Q$, one input-head position on each input tape, one work-head position on each work tape, and the contents of every work-tape cell used by the computation. Since $M$ is fixed, the numbers $q$, $a$, $b$, and $\gamma$ are constants independent of $x$, $n$, and $s(n)$. [/step] [step:Bound the number of choices for input-head positions] Each input head has at most $n+2$ possible positions, allowing the $n$ input cells and the two endmarker positions. Therefore the total number of input-head position choices is at most $(n+2)^a$. Since $n \geq 2$, we have $n+2 \leq 2n$. Using $s(n) \geq \log_2 n$, we obtain $(n+2)^a \leq (2n)^a = 2^a n^a = 2^a 2^{a \log_2 n} \leq 2^a 2^{a s(n)}$. Because $s(n) \geq \log_2 n \geq 1$, the factor $2^a$ is also bounded by $2^{a s(n)}$. Hence $(n+2)^a \leq 2^{2a s(n)}$. [guided] We now isolate the only part of the configuration count that depends directly on the input length $n$: the input-head locations. For each input tape, the head can be on one of the $n$ input symbols or on one of the two endmarker positions, so there are at most $n+2$ choices per input tape. Since $M$ has exactly $a$ input tapes, the total number of choices is at most $(n+2)^a$. The goal is to express this polynomial factor as an exponential in the space bound $s(n)$. The hypothesis $s(n) \geq \log_2 n$ is precisely what permits this absorption. Since $n \geq 2$, we have $n+2 \leq 2n$, and therefore $(n+2)^a \leq (2n)^a$. Expanding the right-hand side gives $(2n)^a = 2^a n^a = 2^a 2^{a\log_2 n}$. Using $\log_2 n \leq s(n)$, we get $2^a 2^{a\log_2 n} \leq 2^a 2^{a s(n)}$. Finally, since $n \geq 2$, the assumption $s(n) \geq \log_2 n$ implies $s(n) \geq 1$, so $2^a \leq 2^{a s(n)}$. Combining these inequalities yields $(n+2)^a \leq 2^{2a s(n)}$. Thus the polynomial input-head contribution is bounded by an exponential whose exponent is linear in $s(n)$. [/guided] [/step] [step:Bound the number of choices for work-tape heads and contents] We use the standard space-bounded configuration convention that the recorded work-tape window on each tape consists of the cells ever used by the computation, together with at most one adjacent boundary cell when the model records the next unused cell. Since $M$ uses space $s(n)$, this window has length at most $s(n)+1$ on each work tape. Thus each work-tape head has at most $s(n)+1$ possible relevant positions, and the total number of work-head position choices is therefore at most $(s(n)+1)^b$. Since $s(n) \geq 1$, we have $s(n)+1 \leq 2^{s(n)+1} \leq 2^{2s(n)}$, and hence $(s(n)+1)^b \leq 2^{2b s(n)}$. The contents of all work tapes are determined by assigning a symbol of $\Gamma$ to each used work-tape cell. Across the $b$ work tapes, there are at most $b s(n)$ used cells, so the number of possible work-tape contents is at most $\gamma^{b s(n)} = 2^{b(\log_2 \gamma)s(n)}$. [/step] [step:Multiply the factors and absorb constants into one exponent] Combining the choices for the internal state, input-head positions, work-head positions, and work-tape contents, the number of configurations in $G_{M,x}$ is at most $q \cdot 2^{2a s(n)} \cdot 2^{2b s(n)} \cdot 2^{b(\log_2 \gamma)s(n)}$. Since $q \geq 1$ is constant and $s(n) \geq 1$, we have $q \leq 2^{(\log_2 q)s(n)}$, with the convention that $\log_2 1 = 0$. Define the machine-dependent constant $c > 0$ by $c := \max\{1, \log_2 q + 2a + 2b + b\log_2 \gamma\}$. Then $q \cdot 2^{2a s(n)} \cdot 2^{2b s(n)} \cdot 2^{b(\log_2 \gamma)s(n)} \leq 2^{c s(n)}$. The constant $c$ depends only on the fixed machine $M$. Hence, for every input $x$ of length $n \geq 2$, the number of vertices in $G_{M,x}$ is at most $2^{c s(n)}$, as required. [/step]