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>(A, B)</tex> сводится к ПСП для которых существует решение ПСПпары списков <tex>(C, перечислимD)</tex>.
Пусть даны последовательности Из определения [[M-сводимость|m-сведения]] следует, что мы должны доказать равносильность наличия решения для построенных экземпляров МПСП и ПСП. <tex>a\Rightarrow</tex> и Пусть набор индексов <tex>b(1, i_2, \dots, i_k)</tex> размера — решение МПСП из условия леммы. То есть <tex>nw_A = w_B</tex> из условия ПСП. Построим программу-полуразрешитель , где <tex>pw_A = a_1 a_{i_2} \dots a_{i_k}</tex>, проверяющую все возможные решения: for <tex>m w_B = 1 .. b_1 b_{i_2} \inftydots b_{i_k}</tex>. for all Рассмотрев цепочки <tex>w_C</tex>(i_1и <tex>w_D</tex> c аналогичными индексами, заметим, i_2что мы имеем почти равные цепочки с той лишь разницей, что первой не хватает символа <tex>\ldots#</tex> в начале, i_m): а второй — в конце. Конкретно, <tex>\# c_1 c_{i_2} \dots c_{i_k} = d_1 d_{i_2} \dots d_{i_k} \# </tex>. Изменив первый индекс с <tex>1 </tex> на <tex>0</tex>, решим проблему с символом <tex>\leq i_j #</tex> в начале. Добавив индекс <tex>n+1</tex> к набору, решим проблему с символом <tex>\leq n#</tex>в конце. if <tex>a_c_0 c_{i_1i_2} \ldots a_dots c_{i_mi_k} c_{n+1} = b_d_0 d_{i_1i_2} \ldots b_dots d_{i_mi_k} d_{n+1}</tex>. return trueТаким образомИтого, язык пар последовательностейесли <tex>(1, i_2, \dots, i_k)</tex> — решение исходной МПСП, для которых существует то <tex>(0, i_2, \dots, i_k, n+1)</tex> — решение построенной по правилам выше ПСП. <tex>\Leftarrow</tex> В любом существующем решении ПСП для списков <tex>C, полуразрешимD</tex> должны выполняться условия: * <tex>i_1 = 0</tex>, так как только в паре <tex>(c_1, а значитd_1)</tex> первые символы совпадают, перечислим.* последний индекс равен <tex>n+1</tex>, так как только в паре <tex>(c_{n+1}, d_{n+1})</tex> строки заканчиваются одинаковыми символами.
Для МПСП доказательство перечислимости имеющих решение пар аналогично, но перебор индексов ведётся с Пусть последовательность <tex>(0, i_2, i_3, \dots, i_k, n + 1)</tex>является решением ПСП.Иными словами,
Назовём '''снимком''' состояния МТ строку вида Если <tex>c_1 c_2 i_f</tex> — наименьший индекс, равный <tex>n+1</tex>, то <tex>c_0 c_{i_2} \ldots c_k dots c_{i_f}</tex>, <tex>d_0 d_{i_2} \#_p c_dots d_{k+1i_f} </tex> — префиксы исходных конкатенаций до первого символа <tex>\ldots c_t$</tex>, где следовательно, равны между собой. Последовательность <tex>c_1 c_2 (0, i_{2} \ldots c_tdots, i_f)</tex> — строка на ленте без учёта пробеловтакже решение ПСП, причём первый индекс равен <tex>p0</tex> и <tex>i_f = n + 1</tex>. Остальные индексы не превосходят <tex>n</tex>, но и не равны <tex>0</tex> — текущее состояние автомата МТ, иначе в левой части равенства образуется подстрока из двух <tex>\#_p</tex> соответствует положению головкиподряд, а в правой её не может быть. Построим последовательности таким образомУчитывая эти ограничения, чтобы решение МПСП образовывало строкуперепишем получившееся равенство:
где <tex>snap_i</tex> — снимки последовательных состояний МТ от стартового до конечногоОставив из этих двух строк символы, стоящие на чётных позициях, <tex>snap_{n_{-t}}</tex> — последний снимок и удалив с конца <tex>t</tex> удалёнными символами строки. Оговоримся, что состояния <tex>no\$</tex> в автомате МТ не существует (его роль может выполнять сток), допуск происходит при попадании в состояние <tex>yes</tex>.получим
Сформируем последовательности <tex>a</tex> и <tex>b</tex> по МТ <tex>M</tex> и строке <tex>wa_1 a_{i_2} \dots a_{i_{f-1}} = b_1 b_{i_2} \dots b_{i_{f-1}}</tex>.
для всех символов <tex>c</tex> алфавита ленты (за исключением пробела):
<tex>a_i = c</tex>, <tex>b_i = c</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>Msnap_i</tex> вида — снимки последовательных состояний МТ от стартового до конечного, <tex>snap_{n_{-t}}</tex> — последний снимок с <tex>\delta (pt</tex> удалёнными символами, c) = а <tex>\langle q$</tex> — символ, dне принадлежащий алфавиту ленты и алфавиту входных слов. Оговоримся, \leftarrow \rangleчто отвергающего состояния <tex>no</tex> и для всех символов алфавита в автомате МТ не существует, а допуск происходит при попадании в состояние <tex>eyes</tex>:.
для всех правил <tex>M</tex> вида <tex>\delta (p, c) = $ snap_1 \$ snap_2 \$ \langle q, d, dots \downarrow $ snap_n \rangle$</tex>:,
<tex>a_i = \#_q d</tex>, <tex>b_i = \#_p c</tex>.то вторая будет равна
Такие последовательности позволяют сформировать строки <tex>\$ snap_1 \$ snap_2 \$ \ldots \$ snap_n \$</tex> (из <tex>a</tex>) и <tex>\$ snap_1 \$ snap_2 \$ \ldots dots \$ snap_{n-1} \$</tex> (из <tex>b</tex>) и только их, но решения МПСП быть не может, так как все члены последовательностей, кроме первого, имеют равную длину, и строка, составленная из элементов <tex>a</tex>, всегда оказывается длиннее.
Задача — получить равные строки, если состояние <tex>\#_{yes}</tex> достижимо. Для этого добавим в уже имеющиеся последовательности следующие элементы:а через несколько шагов они изменятся на
для всех символов <tex>c\$ snap_1 \$ snap_2 \$ \dots \$ snap_n \$ snap_{n+1} \$</tex> алфавита ленты (за исключением пробела):
<tex>a_i = \#_{yes}</tex>, <tex>b_i = \#_{yes} c</tex>,и
а такжесоответственно.
<tex>a_i = \$</tex>Теперь стоит новая задача — получить равные строки, если состояние <tex>b_i = \#_{yes} \$ \$</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>snap_n7</tex> содержится и <tex>\#_{yes}8</tex>; другими словами, только тогда, когда автомат, принадлежащий <tex>M</tex>, допускает <tex>w</tex>. Таким образом, выполнено успешное m-сведение множества пар и копируя все остальные с помощью элементов из машины Тьюринга (МТ) правил <tex>M2</tex> и строки <tex>w3</tex>, где <tex>M(w)</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> — символы, не встречающиеся в словах исходных последовательностей.
{{Утверждение
|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>. Оставив из этих двух строк символы, стоящие на чётных позициях, и удалив с конца <tex>\#</tex>, получим
<tex>a_1 a_{i_2-1} \ldots a_{i_{f-1}-1} = b_1 b_{i_2= См. также ==* [[Неразрешимость исчисления предикатов первого порядка]]* [[Примеры неразрешимых задач: задача о выводе в полусистеме Туэ|Задача о выводе в полусистеме Туэ]]* [[Примеры неразрешимых задач: задача о замощении|Задача о замощении]]* [[Примеры неразрешимых задач: однозначность грамматики|Однозначность грамматики]]* [[Неразрешимость задачи об эквивалентности КС-1} \ldots b_{i_{f-1}-1}</tex>.грамматик]]}}* [[Неразрешимость проблемы существования решения диофантова уравнения в целых числах]]
По доказанному ранее== Источники информации ==* Хопкрофт Д., Мотвани Р., МПСП неразрешимаУльман Д. ТогдаВведение в теорию автоматов, языков и вычислений, вследствие теоремы для m2-сведенияе изд. : Пер. с англ. — М.:Издательский дом «Вильямс», ПСП неразрешима2008. — С. 528.— ISBN 5-8459-1347-0}}* [http://en.wikipedia.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>
|}
Решение этой проблемы соответствий Поста будет являться последовательность индексов <tex>(3, 1, 3, 2)</tex>.
Проверим это.
<tex>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=
Для списков <tex>A</tex> и <tex>B</tex> размера <tex>n</tex> из условия ПСП построим программу-полуразрешитель <tex>p</tex>, проверяющую все возможные решения:
'''for''' <tex>m = 1 \dots \infty</tex>
'''foreach''' <tex>(i_1, i_2, \dots, i_m): 1 \leqslant i_j \leqslant n</tex>
'''if''' <tex>a_{i_1} \dots a_{i_m} = b_{i_1} \dots b_{i_m}</tex>
'''return''' ''true''
Таким образом, язык пар последовательностей, для которых существует решение ПСП, полуразрешим, а значит, перечислим.
}}
== Неразрешимость языка ПСП ==
{{Определение
}}
Докажем [[Разрешимые (рекурсивные) языки|неразрешимость]] языка ПСП следующим образом. Докажем, что универсальный язык [[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>d_{Утверждениеn+1} = \#\$</tex>. {{Лемма|id=lemma-
|statement=
|proof=
<tex>c_0 c_{i_2} \dots c_{Теорема|statementi_k} c_{n+1} =МПСП неразрешима.|proof=Выполним [[M-сводимость|m-сведение]] множества пар из машины Тьюринга (МТ) <tex>M</tex> и строки <tex>w</tex>, где <tex>M(w)d_0 d_{i_2} \dots d_{i_k} d_{n+1}</tex> не зависает, к множеству решений МПСП.
<tex>\$ snap_1 \$ snap_2 \$ \ldots \$ snap_n # c_1 c_{i_2} \$ snap_dots c_{n_i_{f-1}} \$ snap_</tex> <tex>=</tex> <tex>d_1 d_{n_i_2} \dots d_{i_{f-21}} \$ \ldots \$ \#_{yes} \$ \$</tex>,.
Итого, если <tex>a_1 = (0, i_2, \$ \#_{start} w \$ dots, i_k, n+1)</tex>— решение ПСП, то <tex>b_1 = (1, i_2, \$dots, i_k)</tex>;— решение исходной МПСП.}}
<tex>a_i = \$</tex>, <tex>b_i = snap_1 \$ snap_2 \$ \dots \$ snap_n \$ snap_{n_{-1}} \$ snap_{n_{-2}} \$ \dots \$ \#_{yes} \$ \$</tex>;,
Сформируем списки <tex>a_i = \#_q e dA</tex>, и <tex>b_i = e \#_p cB</tex>;по МТ <tex>M</tex> и входной строке <tex>w</tex>. Будем добавлять пары цепочек в эти списки по следующим правилам:
:1. <tex>a_1 = \$ \#_{start} w \$ </tex>, <tex>b_1 = \$</tex>. По определению МПСП эта пара всегда будет первой в любом решении.:2. <tex>a_i = c</tex>, <tex>b_i = c</tex> для всех символов <tex>c</tex> алфавита ленты.:3. <tex>a_i = \$</tex>, <tex>b_i = \$</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>a_i = d \#_qи <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>b_i = \#_p c$</tex>;и префикс нового снимка до следующего перехода машины Тьюринга. Таким образом если первая строка равна
<tex>a_i = \#_$ snap_1 \$ snap_2 \$ \dots \$ snap_{yesn-1}</tex>, <tex>b_i = c \#_{yes}$ snap_n \$</tex>,
Если состояние <tex>yes</tex> недостижимо, в первой строке никогда не будет символа <tex>\$ snap_1 \$ snap_2 \$ \ldots \$ snap_n \$ snap_{n_{-1}} \$ snap_{n_{-2}} \$ \ldots \$ \#_{yes} \$ \$</tex>,и ни одним из новых элементов воспользоваться не удастся. Значит, строки всегда будут иметь различную длину.
<tex>\$ snap_1 \$ snap_2 \$ \dots \$ snap_n \$ snap_{n_{-1}}\$ snap_{n_{-2}} \$ \dots \$ \#_{yes} \$</tex> и <tex>\$ snap_1 \$ snap_2 \$ \dots \$ snap_n \$ snap_{n_{-1}} \$ snap_{n_{-2}} \$ \dots \$ </tex>. И наконец, с помощью элементов из правила <tex>9</tex> сравняем строки.
=== Пример ===
из <tex>yes</tex> переходов нет.
{|class="wikitable" style="text-align: center"
|-
! Номер элемента
! Последовательность a<tex>A</tex> ! Последовательность b<tex>B</tex>
|-
|1
|-
|11
|<tex>\$'</tex> |<tex>\#_{yes} \$ \$'</tex>
|}
Решение МПСП будет иметь следующий вид:
{|class="wikitable" style="text-align: center"
|-
! Шаг
! Вторая строка
|-
|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>
