[proofplan] We decide the indistinguishability relation $q \sim q'$ by a constructive algorithm — the table-filling algorithm — which marks pairs that are *distinguishable* and leaves the remaining pairs as exactly those with $q \sim q'$. The table is indexed by unordered pairs $\{q, q'\}$ with $q \ne q'$, and each entry is either empty or holds a concrete distinguishing word. Initialisation fills pairs separated by acceptance status with the empty word. Iteration propagates distinguishability backwards along transitions: if $(\delta(q, a), \delta(q', a))$ has a distinguishing word $w$, then $(q, q')$ has the distinguishing word $aw$. Termination is guaranteed because only finitely many pairs exist. Correctness splits into soundness (every filled entry holds a genuine distinguisher, by induction on the time of filling) and completeness (every distinguishable pair eventually gets filled, proved by induction on the length of a shortest distinguishing word). [/proofplan]

[step:Fix notation and recall the indistinguishability relation] Let $D = (Q, \Sigma, \delta, q_0, F)$ be a deterministic automaton with $Q$ and $\Sigma$ finite, and let $\hat{\delta}: Q \times \Sigma^* \to Q$ be the extended transition function. For $q, q' \in Q$, the [indistinguishability relation](/pages/???) is \begin{align*} q \sim q' \iff \bigl(\forall w \in \Sigma^*\bigr)\bigl[\hat{\delta}(q, w) \in F \iff \hat{\delta}'(q', w) \in F\bigr], \end{align*} and a word $w \in \Sigma^*$ *distinguishes* $q$ from $q'$ iff exactly one of $\hat{\delta}(q, w), \hat{\delta}(q', w)$ lies in $F$. Thus $q \not\sim q'$ iff there exists some distinguishing word. [/step]

[step:Set up the table as a function on unordered pairs] Let \begin{align*} P := \{\{q, q'\} : q, q' \in Q, q \ne q'\}, \end{align*} a finite set with $|P| = \binom{|Q|}{2}$. The *table* is a partial function \begin{align*} A: P &\rightharpoonup \Sigma^*, \\ \{q, q'\} &\mapsto A_{q, q'} \text{ (a word, if assigned)}. \end{align*} We write $A_{q, q'} = \bot$ when $\{q, q'\}$ is unassigned ("empty"). The algorithm builds $A$ in two phases (initialisation, then a loop of iteration passes) and we shall prove: after termination, $A_{q, q'} \ne \bot$ iff $q \not\sim q'$, and in that case $A_{q, q'}$ is a word distinguishing $q$ from $q'$. [/step]

[step:Run the initialisation phase: fill pairs separated by acceptance with $\varepsilon$] Start with $A_{q, q'} = \bot$ for every $\{q, q'\} \in P$. For each $\{q, q'\} \in P$ with exactly one of $q, q'$ in $F$, set $A_{q, q'} := \varepsilon$. *Correctness of initialisation.* If exactly one of $q, q'$ lies in $F$, then $\hat{\delta}(q, \varepsilon) = q$ and $\hat{\delta}(q', \varepsilon) = q'$, so exactly one lies in $F$ and $\varepsilon$ genuinely distinguishes them. [/step]

[step:Run the iteration phase and show it terminates] A *pass* consists of the following operation: for each $\{q, q'\} \in P$ currently with $A_{q, q'} = \bot$, and each $a \in \Sigma$, inspect the pair $\{\delta(q, a), \delta(q', a)\}$. - If $\delta(q, a) = \delta(q', a)$, do nothing (the pair lies on the diagonal and has no table entry). - Else if $A_{\delta(q, a), \delta(q', a)} = w \ne \bot$, set $A_{q, q'} := aw$ and move to the next pair. - Else (the child pair is empty), try the next $a$. Repeat passes until some pass completes without filling any new entry; then halt. *Termination.* Each pass either fills at least one previously-empty entry or leaves the table unchanged; in the former case the number of empty entries strictly decreases, and since $|P|$ is finite this can happen at most $|P| < \infty$ times. Hence a pass with no new fills must occur, and the algorithm halts after at most $|P| + 1$ passes. Each pass inspects at most $|P| \cdot |\Sigma|$ (pair, letter)-combinations, each an $O(1)$ table lookup, so the total cost is $O(|P|^2 \cdot |\Sigma|)$, which is finite. [/step]

[step:Soundness — every filled entry is a genuine distinguishing word] [claim:For every $\{q, q'\} \in P$, if $A_{q, q'} = w \ne \bot$ at termination, then $w$ distinguishes $q$ from $q'$] We prove this by induction on the time step $t$ at which the entry was filled (counting initialisation as $t = 0$ and the $k$-th iteration pass as time $t = k$). *Base* $t = 0$: at initialisation, $A_{q, q'}$ is set to $\varepsilon$ only when exactly one of $q, q'$ lies in $F$, and $\varepsilon$ distinguishes them as observed above. *Inductive step* $t \ge 1$: the entry $A_{q, q'} = aw$ was set because $\delta(q, a) \ne \delta(q', a)$ and $A_{\delta(q, a), \delta(q', a)} = w$ at some earlier time $t' < t$. By the inductive hypothesis, $w$ distinguishes $\delta(q, a)$ from $\delta(q', a)$, i.e., exactly one of $\hat{\delta}(\delta(q, a), w), \hat{\delta}(\delta(q', a), w)$ lies in $F$. Using the recursion $\hat{\delta}(r, av) = \hat{\delta}(\delta(r, a), v)$, \begin{align*} \hat{\delta}(q, aw) &= \hat{\delta}(\delta(q, a), w), \\ \hat{\delta}(q', aw) &= \hat{\delta}(\delta(q', a), w), \end{align*} so exactly one of $\hat{\delta}(q, aw), \hat{\delta}(q', aw)$ lies in $F$. Hence $aw$ distinguishes $q$ from $q'$. [/claim] In particular, if $A_{q, q'} \ne \bot$ at termination, then $q \not\sim q'$. [/step]

[step:Completeness — every distinguishable pair gets filled] [claim:For every $\{q, q'\} \in P$ with $q \not\sim q'$, the algorithm fills $A_{q, q'}$ before termination] Suppose $q \not\sim q'$ and fix a *shortest* word $w$ distinguishing $q$ from $q'$. We prove by strong induction on $|w|$ that $A_{q, q'}$ is filled. *Base* $|w| = 0$: then $w = \varepsilon$ and by definition of distinguishing, exactly one of $q, q'$ lies in $F$. Initialisation sets $A_{q, q'} := \varepsilon$ immediately, so the entry is filled at time $t = 0$. *Inductive step* $|w| \ge 1$: write $w = av$ with $a \in \Sigma$ and $v \in \Sigma^*$, $|v| = |w| - 1$. From $\hat{\delta}(q, w) = \hat{\delta}(\delta(q, a), v)$ and $\hat{\delta}(q', w) = \hat{\delta}(\delta(q', a), v)$, together with the hypothesis that $w$ distinguishes $q$ from $q'$, we conclude that $v$ distinguishes $\delta(q, a)$ from $\delta(q', a)$. In particular $\delta(q, a) \ne \delta(q', a)$ (else the deterministic transition would send $q$ and $q'$ to the same state after reading $a$, and $v$ could not distinguish them). Moreover $v$ is a distinguishing word of length $|w| - 1$, so $\{\delta(q, a), \delta(q', a)\}$ is distinguishable, and any *shortest* distinguishing word for this pair has length at most $|v| < |w|$. By the strong inductive hypothesis, $A_{\delta(q, a), \delta(q', a)}$ is filled at some termination time $t'$. Now suppose for contradiction that $A_{q, q'} = \bot$ at termination. Consider the pass immediately after $A_{\delta(q, a), \delta(q', a)}$ is filled (if the child was filled at initialisation, consider the first iteration pass). During that pass, the algorithm inspects $\{q, q'\}$ (because it is still empty) and the letter $a$, finds $A_{\delta(q, a), \delta(q', a)} \ne \bot$, and sets $A_{q, q'}$ to $a$ concatenated with that child word. This contradicts the assumption $A_{q, q'} = \bot$ at termination. Hence $A_{q, q'}$ is filled. [/claim] [/step]

[step:Conclude the decision procedure] Combining the previous two steps, after the algorithm halts, \begin{align*} A_{q, q'} \ne \bot \iff q \not\sim q' \qquad (\{q, q'\} \in P), \end{align*} and when non-empty the entry holds a concrete distinguishing word. To decide $q \sim q'$ for a given input pair, run the algorithm and inspect $A_{q, q'}$: output "yes, $q \sim q'$" iff the entry is empty, and otherwise output "no, with distinguisher $A_{q, q'}$". The algorithm terminates in finite time by the termination step. Hence indistinguishability is decidable. [/step]