Изменения

Пусть <tex>A_{1}</tex> и <tex>A_{2}</tex> — детерминированные конечные автоматы, соответствующие языкам задающие языки <tex>L_{1}</tex> и <tex>L_{2}</tex> над одним алфавитом <tex>\Sigma</tex>, соответственно. Совпадение языков на языке конечных автоматов ('''эквивалентность''' задающих их автоматов) означает, что любое слово, допустимое одним автоматом, допускается и другим. Назовём состояния <tex>p_{1} \in </tex> из <tex>A_{1}</tex> и <tex>p_{2} \in </tex> из <tex>A_{2}</tex> '''различимыми''', если существует строка <tex>w</tex> из символов <tex>\Sigma</tex>, для которой выполняется

где <tex>s_{1}</tex>, <tex>s_{2}</tex> — стартовые состояния, <tex>t_{1}</tex>, <tex>t_{2}</tex> — допускающие состояния, <tex>u_{1}</tex>, <tex>u_{2}</tex> — недопускающие.

Все состояния, из которых не достигаются допускающие, не влияют на множество слов, допускаемых автоматами; назовём их '''бесполезными'''. Введём '''сток''' <ref>Другое название стока - «дьявольское состояние».</ref> — специальное недопускающее состояние, переходы по всем символам из которого ведут в него самого. Все переходы исходного автомата, которые отсутствовали или вели в бесполезные состояния, направим в сток.

Пусть такой пары не существует. Возьмём произвольное слово <tex>w</tex> длины <tex>n</tex> и выпишем последовательность пар состояний <tex>\langle u_{i}, v_{i} \rangle</tex>: <tex>u_{0} = s_{1}, v_{0} = s_{2}</tex> и <tex>\forall i = 1 .. n</tex> справедливо <tex>\delta_{1} (u_{i-1}, sw[i-1]) = u_{i}, \delta_{2} (v_{i-1}, sw[i-1]) = v_{i}</tex>. Так как пара <tex>\langle u_{0}, v_{0} \rangle</tex> была в очереди, каждая из последующих пар в процессе алгоритма также побывала в очереди, значит, <tex>eq</tex> для них возвращает <tex>true</tex>. По предположению, или оба состояния <tex>\langle u_{n}, v_{n} \rangle</tex> допускающие в своих автоматах, или оба недопускающие. Таким образом, строка <tex>w</tex> или входит в оба языка, или не входит ни в один.