1632
правки
Изменения
м
Дана упорядоченная пара Даны два конечных последовательностей списка <tex>(A = (a_1, \ldotsdots, a_n), </tex> и <tex>B = (b_1 ,\ldots dots ,b_n))</tex>, где <tex>a_i \in \Sigma ^*</tex> и <tex>b_i \in \Sigma ^*</tex> для всех <tex>i</tex>. Вопрос существования непустой последовательности индексов <tex>(i_1 , \ldotsdots, i_k)</tex>, удовлетворяющей условию <tex>a_{i_1} \ldots dots a_{i_k} = b_{i_1} \ldots dots b_{i_k}</tex>, где <tex>1 \leq leqslant i_j \leq leqslant n</tex> для каждого всех <tex>j</tex>, называется '''проблемой соответствий Поста (ПСП)'''. Такую последовательность индексов, в случае её существования, называют '''решением проблемы соответствий Поста'''.
Пусть даны последовательности Для списков <tex>aA</tex> и <tex>bB</tex> размера <tex>n</tex> из условия ПСП. Построим построим программу-полуразрешитель <tex>p</tex>, проверяющую все возможные решения: '''for ''' <tex>m = 1 .. \dots \infty</tex> for all '''foreach''' <tex>(i_1, i_2, \ldotsdots, i_m): 1 \leq leqslant i_j \leq leqslant n</tex> '''if ''' <tex>a_{i_1} \ldots dots a_{i_m} = b_{i_1} \ldots dots b_{i_m}</tex> '''return ''' ''true''
Выполним Из определения [[M-сводимость|m-сведениесведения]] множества пар из машины Тьюринга (МТ) <tex>M</tex> и строки <tex>w</tex>следует, где <tex>M(w)</tex> не зависает, к множеству решений что мы должны доказать равносильность наличия решения для построенных экземпляров МПСПи ПСП.
Назовём '''снимком''' состояния МТ строку вида <tex>c_1 c_2 \ldots c_k \#_p c_{k+1} \ldots c_t</tex>, где <tex>c_1 c_2 \ldots c_t</tex> — строка на ленте, за исключением бесконечных последовательностей пробелов слева и справа, <tex>p</tex> — текущее состояние автомата МТ, головка расположена справа от <tex>\#_pRightarrow</tex>. Построим последовательности таким образом, чтобы решение МПСП образовывало строку
где <tex>snap_i</tex> — снимки последовательных состояний МТ от стартового до конечного, <tex>snap_w_A = a_1 a_{n_i_2} \dots a_{-t}i_k}</tex> — последний снимок с <tex>t</tex> удалёнными символами. Оговоримся, что состояния <tex>no</tex> в автомате МТ не существует (его роль может выполнять сток), допуск происходит при попадании в состояние <tex>yes</tex>.
Сформируем последовательности <tex>a</tex> и <tex>b</tex> по МТ <tex>M</tex> и строке <tex>ww_B = b_1 b_{i_2} \dots b_{i_k}</tex>.
для всех символов <tex>c\# c_1 c_{i_2} \dots c_{i_k} = d_1 d_{i_2} \dots d_{i_k} \# </tex> алфавита ленты:.
а также<tex> c_0 c_{i_2} \dots c_{i_k} c_{n+1} = d_0 d_{i_2} \dots d_{i_k} d_{n+1} </tex>.
для всех правил <tex>M</tex> вида <tex>\delta (p, c) = \langle q, d, \leftarrow \rangle</tex> и для всех символов алфавита <tex>eLeftarrow</tex>:
для всех правил Пусть последовательность <tex>M</tex> вида <tex>\delta (p0, i_2, i_3, c) = \langle qdots, di_k, \rightarrow \ranglen + 1)</tex>:является решением ПСП. Иными словами,
для всех правил Если <tex>Mi_f</tex> вида — наименьший индекс, равный <tex>n+1</tex>, то <tex>c_0 c_{i_2} \dots c_{i_f}</tex>, <tex>d_0 d_{i_2} \delta dots d_{i_f}</tex> — префиксы исходных конкатенаций до первого символа <tex>\$</tex>, следовательно, равны между собой. Последовательность <tex>(p0, ci_{2} \dots, i_f) </tex> — также решение ПСП, причём первый индекс равен <tex>0</tex> и <tex>i_f = \langle qn + 1</tex>. Остальные индексы не превосходят <tex>n</tex>, dно и не равны <tex>0</tex>, иначе в левой части равенства образуется подстрока из двух <tex>\downarrow \rangle#</tex>подряд, а в правой её не может быть. Учитывая эти ограничения, перепишем получившееся равенство:
ЗаметимОставив из этих двух строк символы, стоящие на чётных позициях, что все элементы <tex>a</tex> и удалив с конца <tex>b</tex>, кроме первых, имеют одинаковую длину. Значит, строка, составленная из элементов <tex>a\$</tex>, всегда оказывается длиннее. Если представить процесс формирования решения МПСП как динамический, вторая строка вынуждена постоянно «догонять» первую. Более того, можно доказать по индукции, что если первая строка имеет видполучим
ито вторая будет равна
соответственно.а через несколько шагов они изменятся на
Задача — получить равные строки, если состояние <tex>\#_$ snap_1 \$ snap_2 \$ \dots \$ snap_n \$ snap_{yesn+1}\$</tex> достижимо. Для этого добавим в уже имеющиеся последовательности следующие элементы:
для всех символов <tex>c</tex> алфавита ленты:и
<tex>a_i = \#_{yes}</tex>, <tex>b_i = c \#_{yes}</tex>,соответственно.
а такжеТеперь стоит новая задача — получить равные строки, если состояние <tex>\#_{yes}</tex> достижимо. Для этого добавим в уже имеющиеся последовательности элементы по следующим правилам:
<tex>\$ snap_1 \$ snap_2 \$ \ldots \$ snap_n \$ snap_{n_{-1}} \$ snap_{n_{-2}} \$ \ldots \$ \#_{yes} \$ \$</tex>.и
Другими словами, «сравнять» строки возможно тогда и только тогда, когда автомат, принадлежащий <tex>M</tex>, допускает <tex>w</tex>. Таким образом, выполнено успешное m\$ snap_1 \$ snap_2 \$ \dots \$ snap_n \$ snap_{n_{-1}} \$ snap_{n_{-сведение множества пар из машины Тьюринга (МТ) <tex>M</tex> и строки <tex>w</tex>, где <tex>M(w)2}} \$ \dots \$ </tex> не зависает, к множеству решений МПСП.
}}И наконец, с помощью элементов из правила <tex>9</tex> сравняем строки.
Последовательности Списки <tex>A</tex> и <tex>B</tex> для строки <tex>ab</tex> будут сформированы следующим образом:
ПСП неразрешимаУниверсальный язык сводится к МПСП.
Выполним Из определения [[M-сводимость|m-сведениесведения]] множества решений следует, что мы должны доказать, что машина Тьюринга <tex>M</tex> допускает <tex>w</tex> тогда и только тогда, когда построенный экземпляр МПСП к множеству решений ПСПимеет решение.
Пусть даны последовательности <tex>a, b</tex> из условия МПСП. Обозначим как <tex>left(w, c)</tex> и <tex>right(w, c)</tex> строки, состоящие из символов <tex>w</tex>, разделённых <tex>c</tex>: <tex>left(w, c) = c w_1 c w_2 \ldots c w_k</tex>, <tex>right(w, c) = w_1 c w_2 c \dots w_k c</tex>.
Построим две новые последовательности <tex>a', b'</tex>:
* <tex>a'_1 = \$ right(a_1, \$)</tex>, <tex>b'_1 = left(b_1, \$)</tex>;
* <tex>\forall i = 1 .. n</tex>: <tex>a'_{i+1} = right(a_i, \$)</tex>, <tex>b'_{i+1} = left(b_i, \$)</tex>;
* <tex>a'_{n+2} = \#</tex>, <tex>b'_{n+2} = \$ \#</tex>,
где <tex>\$</tex>, <tex>\#</tex> — символы, не встречающиеся в словах исходных последовательностей.
{{Лемма
|id=lemma-
|statement=
Существование решения МПСП для <tex>a, b</tex> эквивалентно существованию решения ПСП для <tex>a', b'</tex>.
|proof=
Пусть Если <tex>w_a = a_1 a_{i_2} \ldots a_{i_k}w</tex>, допускается <tex>w_b = b_1 b_{i_2} \ldots b_{i_k}M</tex>, то можно проимитировать работу <tex>w_a = w_bM</tex>. Рассмотрим со входом <tex>w'_a = a'_1 a'_{i_2+1} \ldots a'_{i_k+1} a'_{n+2} = \$ right(a_1, \$) right(a_{i_2}, \$) \ldots right(a_{i_k}, \$) \#</tex>и, <tex>w'_b = b'_1 b'_{i_2+1} \ldots b'_{i_k+1} b'_{n+2} = left(b_1как показано в примере выше, \$) left(b_{i_2}, \$) \ldots left(b_{i_k}, \$) \$ \#</tex>. На чётных позициях в <tex>w'_a</tex> и <tex>w'_b</tex> стоят получить равные символы строки из элементов списков <tex>w_aA</tex> и <tex>w_b</tex>, а также <tex>\#</tex> (в конце); на нечётных — <tex>\$B</tex>. Следовательно, <tex>w'_a = w'_b</tex>, то То есть <tex>a'_1 a'_{i_2+1} \ldots a'_{i_k+1} a'_{n+2} = b'_1 b'_{i_2+1} \ldots b'_{i_k+1} b'_{n+2}</tex>найти решение МПСП.
В любом существующем решении ПСП для <tex>a'Поскольку все решения МПСП должны начинаться с первой пары, то длина соответствующих строк будет различаться, b'</tex> должны выполняться условия: * <tex>i_1 = 1</tex>и, так как только было сказано выше, если в паре первой строке никогда не будет символа <tex>(a'_1, b'_1)\#_{yes}</tex> первые символы совпадают;* последний индекс равен , то "сравнять" строки по длине не удастся. Значит, если МПСП имеет решение, то символ <tex>n+2\#_{yes}</tex>, так как только в паре рано или поздно появится. А значит и машина Тьюринга допустит <tex>(a'_{n+2}, b'_{n+2})w</tex> строки заканчиваются одинаковыми символами.
Пусть }}
<tex>a'_1 a'_{i_2} \ldots a'_{i_k} Теорема|statement= b'_1 b'_{i_2} \ldots b'_{i_k}</tex>ПСП не разрешима.|proof=Если <tex>i_f</tex> — наименьший индекс, равный <tex>n+2</tex>, то <tex>a'_1 a'_{i_2} \ldots a'_{i_f}</tex>, <tex>b'_1 b'_{i_2} \ldots b'_{i_f}</tex> — префиксы исходных конкатенаций до первого символа <tex>\#</tex>, следовательно, равны между собой. <tex>i_1Скомбинировав обе леммы, \ldots, i_f</tex> — также решение мы сведем универсальный язык к языку ПСП, причём <tex>i_1 = 1</tex>а так как универсальный язык неразрешим, <tex>i_f = n + 2</tex>. Остальные индексы не превосходят <tex>n+1</tex>, но то и не равны <tex>1</tex>, иначе в левой части равенства образуется подстрока из двух <tex>\$</tex> подряд, а в правой её не может бытьПСП — неразрешима. Учитывая эти ограничения, перепишем получившееся равенство:}}
<tex>\$ right(a_1, \$) right(a_{i_2-1}, \$) \ldots right(a_{i_{f-1}-1}, \$) \#</tex> <tex>=</tex> <tex>left(b_1, \$) left(b_{i_2= См. также ==* [[Неразрешимость исчисления предикатов первого порядка]]* [[Примеры неразрешимых задач: задача о выводе в полусистеме Туэ|Задача о выводе в полусистеме Туэ]]* [[Примеры неразрешимых задач: задача о замощении|Задача о замощении]]* [[Примеры неразрешимых задач: однозначность грамматики|Однозначность грамматики]]* [[Неразрешимость задачи об эквивалентности КС-1}, \$) \ldots left(b_{i_{f-1}-1}, \$) \$ \#</tex>.грамматик]]* [[Неразрешимость проблемы существования решения диофантова уравнения в целых числах]]
Оставив из этих двух строк символы== Источники информации ==* Хопкрофт Д., стоящие на чётных позицияхМотвани Р., Ульман Д. Введение в теорию автоматов, языков и удалив вычислений, 2-е изд. : Пер. с конца <tex>\#</tex>англ. — М.:Издательский дом «Вильямс», получим <tex>a_1 a_{i_22008. — С. 528. — ISBN 5-1} \ldots a_{i_{f8459-1}1347-1} = b_1 b_{i_2-1} \ldots b_{i_{f-1}-1}<0* [http://tex>en.}} По доказанному ранее, МПСП неразрешимаwikipedia. Тогда, вследствие теоремы для m-сведения, ПСП неразрешима.}}org/wiki/Post_correspondence_problem Wikipedia — Post correspondence problem]
== Литература ==[[Категория: Теория формальных языков]]* Джон Хопкрофт, Раджив Мотвани, Джеффри Ульман. Введение в теорию автоматов, языков и вычислений.[[Категория: Теория вычислимости]][[Категория: Примеры неразрешимых задач]]
rollbackEdits.php mass rollback
'''Проблема соответствий Поста''' (англ. ''Post correspondence problem'') — один из основных примеров неразрешимой задачи, использующийся для доказательства неразрешимости многих других задач.
{{Определение
|definition=
}}
== Примеры решений проблем соответствия Поста == === Пример 1 ==={{Определение|class="wikitable" style="text-align: center" |- !Номер элемента !<tex>1</tex> !<tex>2</tex> !<tex>3</tex> |- !<tex>A</tex> |<tex>01</tex> |<tex>1</tex> |<tex>011</tex> |- !<tex>B</tex> |<tex>101</tex> |<tex>11</tex> |<tex>01</tex> |definition=}Проблема Решение этой проблемы соответствий Постабудет являться последовательность индексов <tex>(3, 1, 3, для которой фиксирован элемент последовательности индексов 2)</tex>.Проверим это. <tex>i_1 sA = 011, 01, 011, 1</tex> <tex>sB = 01, 101, 01, 11</tex> Получаем то, называется '''модифицированной проблемой соответствий Поста что строки <tex>sA</tex> и <tex>sB</tex> равны, а значит последовательность индексов <tex>(МПСП3, 1, 3, 2)'''</tex> является решением этой проблемы соотвествий Поста. === Пример 2 ===Иногда возникает ситуация, когда решений конкретной проблемы соответствия Поста нет.{|class="wikitable" style="text-align: center" |- !Номер элемента !<tex>1</tex> !<tex>2</tex> !<tex>3</tex> |- !<tex>A</tex> |<tex>01</tex> |<tex>101</tex> |<tex>011</tex> |- !<tex>B</tex> |<tex>0</tex> |<tex>10</tex> |<tex>111</tex> |} Заметим, что если бы решение существовало оно должно было начинаться с индекса <tex>1</tex> или <tex>2</tex>.Но тогда строки получаемые из <tex>A</tex> всегда будут строго больше по длине, чем строки полученные из <tex>B</tex>, так как <tex> \mathrm{length}(A[i]) \geqslant \mathrm{length}(B[i])</tex> для всех <tex>i</tex>. Решения не существует. == Перечислимость языка ПСП ==
{{Теорема
|statement=
Язык пар последовательностей, для которых существует решение ПСП, [[Перечислимые языки | перечислим]].
|proof=
Таким образом, язык пар последовательностей, для которых существует решение ПСП, полуразрешим, а значит, перечислим.
}}
== Неразрешимость языка ПСП == {{Определение|definition=Проблема соответствий Поста, для которой фиксирован элемент последовательности индексов <tex>i_1 = 1</tex>, называется '''модифицированной проблемой соответствий Поста (МПСП)'''.}} Докажем [[Разрешимые (рекурсивные) языки|неразрешимость]] языка ПСП следующим образом. Докажем, что универсальный язык [[M-сводимость|сводится]] к языку МПСП, который в свою очередь сводится к языку ПСП. При этом отметим, что для унарного алфавита ПСП разрешима. === Cведение МПСП к ПСП === Пусть даны списки <tex>A</tex> и <tex>B</tex> из условия МПСП. Построим два новых списка <tex>C</tex> и <tex>D</tex> и рассмотрим ПСП для них. Для МПСП доказательство перечислимости имеющих решение пар аналогичноэтого введем два новых символа, которые не используются в словах из цепочек <tex>A</tex> и <tex>B</tex>. Пусть для определенности это будут символы <tex>\#</tex> и <tex>\$</tex>. Тогда сформируем два новых списка <tex>C, D</tex> по следующим правилам:* для всех <tex>i = 1 \dots n</tex> возьмем <tex>c_i</tex> равное слову <tex>a_i</tex> с символом <tex>\#</tex> после каждого его символа. Например, для <tex>a_i = 10zx</tex> положим <tex>c_i = 1\#0\#z\#x\#</tex>, но перебор индексов ведётся * для всех <tex>i = 1 \dots n</tex> возьмем <tex>d_i</tex> равное слову <tex>b_i</tex> с символом <tex>\#</tex> перед каждым его символом. Например, для <tex>b_i = 10zx</tex> положим <tex>d_i = \#1\#0\#z\#x</tex>,* <tex>c_0 = \#c_1</tex>,* <tex>d_0 = d_1</tex>,* <tex>c_{n+1} = \$</tex>,* <tex>i_2d_{n+1} = \#\$</tex>.
{{ТеоремаЛемма|id=lemma-
|statement=
МПСП неразрешимадля пары списков <tex>(A, B)</tex> сводится к ПСП для пары списков <tex>(C, D)</tex>.
|proof=
Пусть набор индексов <tex>\$ snap_1 \$ snap_2 \$ \ldots \$ snap_n \$ snap_{n_{-(1}} , i_2, \$ snap_{n_{-2}} \$ \ldots \$ \#_{yes} \$ \$dots, i_k)</tex> — решение МПСП из условия леммы. То есть <tex>w_A = w_B</tex>,где
Рассмотрев цепочки <tex>a_1 = \$' \#_{start} w \$ w_C</tex> и <tex>w_D</tex>c аналогичными индексами, заметим, что мы имеем почти равные цепочки с той лишь разницей, что первой не хватает символа <tex>b_1 = \$'#</tex>;в начале, а второй — в конце. Конкретно,
Изменив первый индекс с <tex>a_i = c1</tex> на <tex>0</tex>, решим проблему с символом <tex>b_i = c\#</tex>в начале. Добавив индекс <tex>n+1</tex> к набору,решим проблему с символом <tex>\#</tex> в конце.
Итого, если <tex>a_i = (1, i_2, \$dots, i_k)</tex>— решение исходной МПСП, то <tex>b_i = (0, i_2, \$dots, i_k, n+1)</tex>;— решение построенной по правилам выше ПСП.
В любом существующем решении ПСП для списков <tex>a_i C, D</tex> должны выполняться условия: * <tex>i_1 = \#_q e d0</tex>, так как только в паре <tex>b_i = e \#_p c(c_1, d_1)</tex> первые символы совпадают,* последний индекс равен <tex>n+1</tex>, так как только в паре <tex>(c_{n+1}, d_{n+1})</tex>;строки заканчиваются одинаковыми символами.
<tex>a_i = d c_0 c_{i_2} \#_q</tex>, <tex>b_i dots c_{i_k} c_{n+1} = d_0 d_{i_2} \#_p cdots d_{i_k} d_{n+1}</tex>;.
<tex>a_i = \#_q dc_1 c_{i_2} \dots c_{i_{f-1}}\$</tex>, <tex>b_i = </tex> <tex>d_1 d_{i_2} \dots d_{i_{f-1}} \#_p c\$</tex>.
<tex>a_1 a_{i_2} \$' snap_1 dots a_{i_{f-1}} = b_1 b_{i_2} \$ snap_2 \$ \ldots \$ snap_n \$dots b_{i_{f-1}}</tex>,.
Итого, если <tex>(0, i_2, \dots, i_k, n+1)</tex> — решение ПСП, то вторая будет равна<tex>(1, i_2, \dots, i_k)</tex> — решение исходной МПСП.}} === Сведение универсального языка к МПСП ==={{Определение|definition=Назовём '''снимком состояния [[Машина Тьюринга|МТ]]''' строку вида <tex>c_1 c_2 \dots c_k \#_p c_{k+1} \dots c_t</tex>, где <tex>c_1 c_2 \dots c_t</tex> — строка на ленте, за исключением бесконечных последовательностей пробелов слева и справа, <tex>p</tex> — текущее состояние автомата МТ, головка расположена справа от <tex>\#_p</tex>.}}Построим списки <tex>A</tex> и <tex>B</tex> таким образом, чтобы решение МПСП образовывало строку <tex>\$ snap_1 \$ snap_2 \$ \dots \$ snap_n \$ snap_{n_{-1}} \$ snap_{n_{-2}} \$ \dots \$ \#_{yes} \$ \$</tex>, где <tex>snap_i</tex> — снимки последовательных состояний МТ от стартового до конечного, <tex>snap_{n_{-t}}</tex> — последний снимок с <tex>t</tex> удалёнными символами, а <tex>\$</tex> — символ, не принадлежащий алфавиту ленты и алфавиту входных слов. Оговоримся, что отвергающего состояния <tex>no</tex> в автомате МТ не существует, а допуск происходит при попадании в состояние <tex>yes</tex>. Сформируем списки <tex>A</tex> и <tex>B</tex> по МТ <tex>M</tex> и входной строке <tex>w</tex>. Будем добавлять пары цепочек в эти списки по следующим правилам:
:1. <tex>a_1 = \$' snap_1 \#_{start} w \$ snap_2 </tex>, <tex>b_1 = \$ </tex>. По определению МПСП эта пара всегда будет первой в любом решении.:2. <tex>a_i = c</tex>, <tex>b_i = c</tex> для всех символов <tex>c</tex> алфавита ленты.:3. <tex>a_i = \ldots $</tex>, <tex>b_i = \$ snap_{n-1} </tex>.:4. <tex>a_i = \#_q e d</tex>, <tex>b_i = e \#_p c</tex> для всех правил <tex>M</tex> вида <tex>\delta (p, c) = \langle q, d, \leftarrow \rangle</tex> и для всех символов алфавита <tex>e</tex>.:5. <tex>a_i = d \#_q</tex>, <tex>b_i = \#_p c</tex> для всех правил <tex>M</tex> вида <tex>\delta (p, c) = \langle q, d, \rightarrow \rangle</tex>.:6. <tex>a_i = \#_q d</tex>, <tex>b_i = \$#_p c</tex> для всех правил <tex>M</tex>вида <tex>\delta (p,c) = \langle q, d, \downarrow \rangle</tex>.
Заметим, что все элементы <tex>A</tex> и <tex>B</tex>, кроме первых, имеют одинаковую длину. Значит, строка, составленная из элементов <tex>A</tex>, всегда оказывается длиннее. Если представить процесс формирования решения МПСП как динамический, то строка из элементов <tex>B</tex> вынуждена постоянно "догонять" первую. Более того, можно заметить, что вторая строка всегда будет отставать ровно на один снимок. Действительно, первая пара из списков <tex>A</tex> и <tex>B</tex> задает это отставание. Затем при помощи элементов из правил <tex>4</tex>, <tex>5</tex> и <tex>6</tex> мы имитируем переход машины Тьюринга, добавляя во вторую строку то состояние и положение головки, которые были до перехода, а через несколько шагов они примут видв первую строку - то состояние, положение головки и новый ленточный символ, которые стали после перехода. Нетрудно заметить, что тем самым строка составленная из элементов списка <tex>B</tex> будет соответствовать строке из элементов списка <tex>A</tex>, но с отставанием на один переход. Далее с помощью элементов из правил <tex>2</tex> и <tex>3</tex> мы допишем в обе строки одинаковые суффиксы текущего снимка, разделитель <tex>\$</tex> и префикс нового снимка до следующего перехода машины Тьюринга. Таким образом если первая строка равна
<tex>\$' snap_1 \$ snap_2 \$ \ldots dots \$ snap_n \$ snap_{n+1} \$</tex>,
<tex>\$' snap_1 \$ snap_2 \$ \ldots dots \$ snap_n snap_{n-1} \$</tex>,
<tex>a_i = \#_$ snap_1 \$ snap_2 \$ \dots \$ snap_{yesn-1}</tex>, <tex>b_i = \#_{yes} c$ snap_n \$</tex>,
:7. <tex>a_i = \#_{yes}</tex>, <tex>b_i = \#_{yes} c</tex>, для всех символов <tex>c</tex> алфавита ленты.:8. <tex>a_i = \#_{yes}</tex>, <tex>b_i = c \#_{yes}</tex>, для всех символов <tex>c</tex> алфавита ленты.:9. <tex>a_i = \$'</tex>, <tex>b_i = \#_{yes} \$ \$'</tex>.
Если состояние <tex>yes</tex> недостижимо, в первой строке никогда не будет символа <tex>\#_{yes}</tex>, и ни одним из новых элементов воспользоваться не удастся. Значит, строки всегда будут иметь различную длину.
Если же допускающее состояние встретится, то "съедая" по одному символу с помощью новых элементов правил <tex>7</tex> и <tex>8</tex> и копируя все остальные с помощью элементов из правил <tex>2</tex> и <tex>3</tex> можно будет привести обе строки к виду <tex>\$ snap_1 \$ snap_2 \$ \dots \$ snap_n \$ snap_{n_{-1}} \$ snap_{n_{-2}} \$ \dots \$ \#_{yes} \$</tex>
=== Пример ===
из <tex>yes</tex> переходов нет.
{|class="wikitable" style="text-align: center"
|-
! Номер элемента
! Последовательность a<tex>A</tex> ! Последовательность b<tex>B</tex>
|-
|1
|<tex>\$' \#_{start} ab \$</tex> |<tex>\$'</tex>
|-
|2
|align="center" | 1
|align="center" | 1
|<tex>\$' \#_{start} ab \$</tex> |<tex>\$'</tex>
|-
|align="center" | 2
|align="center" | 5
|<tex>\$' \#_{start} ab \$ b \#_{start}</tex> |<tex>\$' \#_{start} a</tex>
|-
|align="center" | 3
|align="center" | 3
|<tex>\$' \#_{start} ab \$ b \#_{start} b</tex> |<tex>\$' \#_{start} ab</tex>
|-
|align="center" | 4
|align="center" | 4
|<tex>\$' \#_{start} ab \$ b \#_{start} b\$</tex> |<tex>\$' \#_{start} ab \$</tex>
|-
|align="center" | 5
|align="center" | 3
|<tex>\$' \#_{start} ab \$ b \#_{start} b\$ b</tex> |<tex>\$' \#_{start} ab \$ b</tex>
|-
|align="center" | 6
|align="center" | 6
|<tex>\$' \#_{start} ab \$ b \#_{start} b\$ b \#_{yes} b</tex> |<tex>\$' \#_{start} ab \$ b \#_{start} b</tex>
|-
|align="center" | 7
|align="center" | 4
|<tex>\$' \#_{start} ab \$ b \#_{start} b\$ b \#_{yes} b \$</tex> |<tex>\$' \#_{start} ab \$ b \#_{start} b \$</tex>
|-
|align="center" | 8
|align="center" | 8
|<tex>\$' \#_{start} ab \$ b \#_{start} b\$ b \#_{yes} b \$ \#_{yes}</tex> |<tex>\$' \#_{start} ab \$ b \#_{start} b \$ b \#_{yes}</tex>
|-
|align="center" | 9
|align="center" | 3
|<tex>\$' \#_{start} ab \$ b \#_{start} b\$ b \#_{yes} b \$ \#_{yes} b</tex> |<tex>\$' \#_{start} ab \$ b \#_{start} b \$ b \#_{yes} b</tex>
|-
|align="center" | 10
|align="center" | 4
|<tex>\$' \#_{start} ab \$ b \#_{start} b\$ b \#_{yes} b \$ \#_{yes} b \$</tex> |<tex>\$' \#_{start} ab \$ b \#_{start} b \$ b \#_{yes} b \$</tex>
|-
|align="center" | 11
|align="center" | 10
|<tex>\$' \#_{start} ab \$ b \#_{start} b\$ b \#_{yes} b \$ \#_{yes} b \$ \#_{yes}</tex> |<tex>\$' \#_{start} ab \$ b \#_{start} b \$ b \#_{yes} b \$ \#_{yes} b</tex>
|-
|align="center" | 12
|align="center" | 4
|<tex>\$' \#_{start} ab \$ b \#_{start} b\$ b \#_{yes} b \$ \#_{yes} b \$ \#_{yes} \$</tex> |<tex>\$' \#_{start} ab \$ b \#_{start} b \$ b \#_{yes} b \$ \#_{yes} b \$</tex>
|-
|align="center" | 13
|align="center" | 11
|<tex>\$' \#_{start} ab \$ b \#_{start} b \$ b \#_{yes} b \$ \#_{yes} b \$ \#_{yes} \$ \$'</tex> |<tex>\$' \#_{start} ab \$ b \#_{start} b \$ b \#_{yes} b \$ \#_{yes} b \$ \#_{yes} \$ \$'</tex>
|}
{{ТеоремаЛемма
|statement=
|proof=
<tex>\Rightarrow</tex>
<tex>\Leftarrow</tex>