[proofplan]
We reduce the a priori infinite question "does there exist *some* word $w$ with $\hat{\delta}(q_0, w) = q$?" to a finite one by establishing a length bound: if any such word exists, there is one of length at most $|Q|$. The bound comes from the pigeonhole principle applied to the sequence of states visited along a word — any word longer than $|Q|$ must revisit a state, and that loop can be excised to produce a strictly shorter word reaching $q$. Once the length bound is in place, we exhibit an explicit finite algorithm: enumerate all words of length at most $|Q|$ and test each by iterating $\delta$. The number of such words is $\sum_{k=0}^{|Q|} |\Sigma|^k$, which is finite whenever $\Sigma$ is finite (as it is by definition of a finite automaton).
[/proofplan]
[step:Fix notation and state the decision problem]
Let $D = (Q, \Sigma, \delta, q_0, F)$ be a deterministic automaton with $|Q|$ finite and $\Sigma$ finite, and let $\hat{\delta}: Q \times \Sigma^* \to Q$ denote the extended transition function, defined recursively by $\hat{\delta}(p, \varepsilon) = p$ and $\hat{\delta}(p, aw) = \hat{\delta}(\delta(p, a), w)$ for $a \in \Sigma$, $w \in \Sigma^*$. Recall that $q \in Q$ is *accessible* iff there exists $w \in \Sigma^*$ with $\hat{\delta}(q_0, w) = q$. We must exhibit a terminating procedure that, given $D$ and $q$, outputs "yes" if $q$ is accessible and "no" otherwise.
[/step]
[step:Bound the length of a minimal accessing word by $|Q|$ using pigeonhole]
[claim:If $q$ is accessible then there exists $w \in \Sigma^*$ with $\hat{\delta}(q_0, w) = q$ and $|w| \le |Q|$]
Let $W := \{w \in \Sigma^* : \hat{\delta}(q_0, w) = q\}$. By hypothesis $W \ne \varnothing$, so $\min\{|w| : w \in W\}$ exists; pick $w^\star \in W$ of minimal length and write $|w^\star| = N$. We show $N \le |Q|$.
Write $w^\star = a_1 a_2 \cdots a_N$ with $a_i \in \Sigma$, and define the sequence of intermediate states
\begin{align*}
p_i := \hat{\delta}(q_0, a_1 \cdots a_i) \qquad (0 \le i \le N),
\end{align*}
so $p_0 = q_0$ and $p_N = q$. Suppose for contradiction that $N > |Q|$. Then the sequence $p_0, p_1, \dots, p_N$ has $N + 1 > |Q| + 1$ entries in the set $Q$ of cardinality $|Q|$, and by the pigeonhole principle there exist indices $0 \le i < j \le N$ with $p_i = p_j$. Define the pruned word
\begin{align*}
w^\circ := a_1 \cdots a_i \, a_{j+1} \cdots a_N \in \Sigma^*.
\end{align*}
Using the recursive identity $\hat{\delta}(r, uv) = \hat{\delta}(\hat{\delta}(r, u), v)$ (a routine induction on $|u|$) and the equality $p_i = p_j$,
\begin{align*}
\hat{\delta}(q_0, w^\circ)
&= \hat{\delta}(\hat{\delta}(q_0, a_1 \cdots a_i), a_{j+1} \cdots a_N) \\
&= \hat{\delta}(p_i, a_{j+1} \cdots a_N) \\
&= \hat{\delta}(p_j, a_{j+1} \cdots a_N) \\
&= p_N = q.
\end{align*}
So $w^\circ \in W$ with $|w^\circ| = N - (j - i) < N$, contradicting the minimality of $w^\star$. Hence $N \le |Q|$.
[/claim]
[/step]
[step:Reduce the decision problem to a finite search]
By the previous step, $q$ is accessible iff there exists $w \in \Sigma^*$ with $|w| \le |Q|$ and $\hat{\delta}(q_0, w) = q$. Define the finite search space
\begin{align*}
S := \bigcup_{k=0}^{|Q|} \Sigma^k, \qquad |S| = \sum_{k=0}^{|Q|} |\Sigma|^k < \infty,
\end{align*}
where finiteness uses that both $\Sigma$ and $|Q|$ are finite. The decision problem becomes: *does there exist $w \in S$ with $\hat{\delta}(q_0, w) = q$?*
[/step]
[step:Exhibit the decision algorithm and verify its correctness]
The algorithm proceeds as follows:
1. Enumerate the words of $S$ in some order (e.g., shortlex). This enumeration is finite and computable from $\Sigma$ and $|Q|$.
2. For each $w = a_1 \cdots a_k \in S$, compute $\hat{\delta}(q_0, w)$ by iterating $\delta$: set $r_0 := q_0$ and $r_i := \delta(r_{i-1}, a_i)$ for $1 \le i \le k$, and output $r_k$. This terminates after $k \le |Q|$ applications of $\delta$, each a single table lookup.
3. If at any stage $r_k = q$, halt and output "yes". If the enumeration of $S$ exhausts without a match, halt and output "no".
*Termination.* The algorithm performs at most $|S|$ iterations of the outer loop, and each iteration performs at most $|Q|$ transitions; the total number of elementary operations is bounded by $|Q| \cdot |S|$, which is finite.
*Correctness.* If the algorithm outputs "yes" on word $w$, then $\hat{\delta}(q_0, w) = q$, so $q$ is accessible. Conversely, if $q$ is accessible, the previous step produces some $w \in S$ with $\hat{\delta}(q_0, w) = q$; this $w$ is enumerated by the algorithm, which then outputs "yes". Consequently the algorithm outputs "no" exactly when no such $w \in S$ exists, i.e., when $q$ is not accessible.
This exhibits a finite, deterministic procedure that decides accessibility of $q$ in $D$, completing the proof.
[/step]
