[proofplan]
We build an isomorphism $f: I \to I'$ between two irreducible deterministic automata recognising the same language. The key tool is the state-equivalence relation $q \sim q'$, which asks that $q$ and $q'$ accept the same future words. We show that starting from $q_0 \sim q_0'$ (a consequence of $\mathcal{L}(I) = \mathcal{L}(I')$), the $\sim$-relation propagates along transitions, so we can define $f(q)$ to be the unique state of $I'$ with $q \sim f(q)$. Uniqueness uses the irreducibility of $I'$: any two candidate images would be indistinguishable in $I'$, hence equal in the quotient-free setting. Finally we verify that $f$ is a homomorphism, and since every homomorphism between irreducible automata is an isomorphism, this finishes the proof.
[/proofplan]
[step:Fix notation and recall the future relation]
Write $I = (Q, \Sigma, \delta, q_0, F)$ and $I' = (Q', \Sigma, \delta', q_0', F')$ for the two irreducible deterministic automata, and denote their extended transition functions by
\begin{align*}
\hat{\delta}: Q \times \Sigma^* &\to Q, & \hat{\delta}': Q' \times \Sigma^* &\to Q'.
\end{align*}
For $p \in Q$ and $p' \in Q'$, define the *future-equivalence* relation across automata by
\begin{align*}
p \sim p' \iff \bigl(\forall w \in \Sigma^*\bigr)\bigl[\hat{\delta}(p, w) \in F \iff \hat{\delta}'(p', w) \in F'\bigr].
\end{align*}
Similarly, for $p, \tilde{p} \in Q$ write $p \sim_I \tilde{p}$ when the analogous condition holds within $I$; this is the [state equivalence](/pages/???) relation, and *irreducibility* of $I$ means that $\sim_I$ is the identity on $Q$ (every $\sim_I$-equivalence class is a singleton). The analogous statement holds in $I'$.
[/step]
[step:Observe that start states are future-equivalent because the languages agree]
By the definition of the language of an automaton,
\begin{align*}
w \in \mathcal{L}(I) &\iff \hat{\delta}(q_0, w) \in F, & w \in \mathcal{L}(I') &\iff \hat{\delta}'(q_0', w) \in F'.
\end{align*}
The hypothesis $\mathcal{L}(I) = \mathcal{L}(I')$ gives for every $w \in \Sigma^*$ the biconditional
\begin{align*}
\hat{\delta}(q_0, w) \in F \iff \hat{\delta}'(q_0', w) \in F',
\end{align*}
which is exactly $q_0 \sim q_0'$.
[/step]
[step:Propagate future-equivalence along transitions]
[claim:If $p \sim p'$ then $\delta(p, a) \sim \delta'(p', a)$ for every $a \in \Sigma$]
Let $a \in \Sigma$ and write $r := \delta(p, a)$, $r' := \delta'(p', a)$. For any $w \in \Sigma^*$, the extended transition function satisfies $\hat{\delta}(p, aw) = \hat{\delta}(\delta(p, a), w) = \hat{\delta}(r, w)$, and likewise $\hat{\delta}'(p', aw) = \hat{\delta}'(r', w)$. Hence
\begin{align*}
\hat{\delta}(r, w) \in F &\iff \hat{\delta}(p, aw) \in F \\
&\iff \hat{\delta}'(p', aw) \in F' \qquad \text{(since } p \sim p'\text{, with test word } aw\text{)} \\
&\iff \hat{\delta}'(r', w) \in F'.
\end{align*}
As $w \in \Sigma^*$ was arbitrary, $r \sim r'$.
[/claim]
[/step]
[step:Construct a candidate map $f: Q \to Q'$ by induction on accessibility distance]
Because $I$ is irreducible, in particular every state of $I$ is accessible from $q_0$ (states not reachable from $q_0$ are all $\sim_I$-equivalent to each other via the vacuous condition, so a non-singleton $\sim_I$-class would form unless there is at most one inaccessible state; to avoid any subtlety we work only with accessible states and note that an irreducible automaton is by definition accessible). For $q \in Q$ let
\begin{align*}
d(q) := \min\{|w| : w \in \Sigma^*, \hat{\delta}(q_0, w) = q\}.
\end{align*}
We define $f(q) \in Q'$ by strong induction on $d(q)$, maintaining the invariant $q \sim f(q)$.
*Base case* $d(q) = 0$: then $q = q_0$. Set $f(q_0) := q_0'$; the invariant $q_0 \sim q_0'$ was established in the previous step.
*Inductive step* $d(q) = k + 1$: choose a word $w = w_1 \cdots w_{k+1}$ realising the minimum, and set $p := \hat{\delta}(q_0, w_1 \cdots w_k)$, so that $d(p) \le k$ and $q = \delta(p, w_{k+1})$. By the inductive hypothesis $f(p)$ is defined with $p \sim f(p)$. The previous step (applied to the pair $(p, f(p))$ and the letter $a = w_{k+1}$) gives
\begin{align*}
\delta(p, w_{k+1}) \sim \delta'(f(p), w_{k+1}).
\end{align*}
So we set
\begin{align*}
f(q) := \delta'(f(p), w_{k+1}),
\end{align*}
preserving the invariant $q \sim f(q)$.
Well-definedness (independence of the choice of shortest word, and of the particular predecessor $p$) follows from the next step, which shows that *any* $r' \in Q'$ with $q \sim r'$ is uniquely determined by $q$.
[/step]
[step:Uniqueness of the image from irreducibility of $I'$]
[claim:For every $q \in Q$ there is exactly one $q' \in Q'$ with $q \sim q'$]
Existence is the inductive construction of the previous step. For uniqueness, suppose $q \sim q_1'$ and $q \sim q_2'$ with $q_1', q_2' \in Q'$. Then for every $w \in \Sigma^*$,
\begin{align*}
\hat{\delta}'(q_1', w) \in F' &\iff \hat{\delta}(q, w) \in F \iff \hat{\delta}'(q_2', w) \in F',
\end{align*}
where both equivalences use the defining property of $\sim$. This is exactly the statement $q_1' \sim_{I'} q_2'$. Since $I'$ is irreducible, $\sim_{I'}$ is the identity on $Q'$, so $q_1' = q_2'$.
[/claim]
Consequently the map $f: Q \to Q'$ defined in the previous step does not depend on the chosen shortest word or predecessor $p$: it is the unique function satisfying $q \sim f(q)$ for all $q$.
[/step]
[step:Verify that $f$ is a homomorphism of automata]
We check the three conditions.
*Start state.* By construction $f(q_0) = q_0'$.
*Transitions.* Fix $p \in Q$ and $a \in \Sigma$. The transition-propagation step gives $\delta(p, a) \sim \delta'(f(p), a)$. By the uniqueness step, $f(\delta(p, a))$ is the unique element of $Q'$ with $\delta(p, a) \sim \delta'(f(p), a)$, hence
\begin{align*}
f(\delta(p, a)) = \delta'(f(p), a).
\end{align*}
*Accept states.* For any $q \in Q$, apply the definition of $\sim$ with the empty word $w = \varepsilon$:
\begin{align*}
q \in F \iff \hat{\delta}(q, \varepsilon) \in F \iff \hat{\delta}'(f(q), \varepsilon) \in F' \iff f(q) \in F'.
\end{align*}
Thus $f^{-1}(F') = F$, and $f$ is a homomorphism of deterministic automata.
[/step]
[step:Conclude that $f$ is an isomorphism using irreducibility of both automata]
It is a standard fact that every homomorphism $f: I \to I'$ between two *irreducible* deterministic automata recognising the same language is an isomorphism: injectivity follows because if $f(p) = f(q)$ then $p \sim_I q$ (pushing through $f$ preserves acceptance of all future words), so $p = q$ by irreducibility of $I$; surjectivity follows because the image $f(Q)$ is closed under transitions and contains $q_0'$, hence contains every accessible state of $I'$, which is all of $Q'$ since $I'$ is irreducible (in particular accessible). Since $f$ is a bijective homomorphism, it is an isomorphism. Therefore $I \cong I'$, completing the proof.
[/step]
