Изменения

Назовём '''снимком''' состояния МТ строку вида <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>\#_p</tex> соответствует положению головки. Построим последовательности таким образом, чтобы решение МПСП образовывало строку

где <tex>snap_i</tex> — снимки последовательных состояний МТ от стартового до конечного, <tex>snap_{n_{-t}}</tex> — последний снимок с <tex>t</tex> удалёнными символами строки. Оговоримся, что состояния <tex>no</tex> в автомате МТ не существует (его роль может выполнять сток), допуск происходит при попадании в состояние <tex>yes</tex>.

<tex>a_1 = \$ ' \#_{start} w \$ </tex>, <tex>b_1 = \$'</tex>;

для всех символов <tex>c</tex> алфавита ленты (за исключением пробела):

Такие последовательности позволяют сформировать строки Заметим, что все элементы <tex>a</tex> и <tex>b</tex>, кроме первых, имеют одинаковую длину. Значит, строка, составленная из элементов <tex>a</tex>, всегда оказывается длиннее. Если представить процесс формирования решения МПСП как динамический, вторая строка вынуждена постоянно «догонять» первую. Более того, можно доказать по индукции, что если первая строка имеет вид <tex>\$ ' snap_1 \$ snap_2 \$ \ldots \$ snap_n \$</tex> (из <tex>a</tex>) и , то вторая будет равна <tex>\$ ' snap_1 \$ snap_2 \$ \ldots \$ snap_{n-1} \$</tex> (из , а через несколько шагов они примут вид <tex>b\$' snap_1 \$ snap_2 \$ \ldots \$ snap_n \$ snap_{n+1} \$</tex>)  и только их, но решения МПСП быть не может, так как все члены последовательностей, кроме первого, имеют равную длину, и строка, составленная из элементов  <tex>a\$' snap_1 \$ snap_2 \$ \ldots \$ snap_n \$</tex>, всегда оказывается длиннее соответственно.

для всех символов <tex>c</tex> алфавита ленты (за исключением пробела):

<tex>a_i = \$'</tex>, <tex>b_i = \#_{yes} \$ \$'</tex>.

С помощью Если состояние <tex>yes</tex> недостижимо, в первой строке никогда не будет символа <tex>\#_{yes}</tex>, и ни одним из новых элементов можно привести обе воспользоваться не удастся. Значит, строки к виду всегда будут иметь различную длину.

Если же допускающее состояние встретится, с помощью новых элементов можно будет привести обе строки к виду  <tex>\$ snap_1 \$ snap_2 \$ \ldots \$ snap_n \$ snap_{n_{-1}} \$ snap_{n_{-2}} \$ \ldots \$ \#_{yes} \$ \$</tex>,.

но только тогда, когда в <tex>snap_n</tex> содержится <tex>\#_{yes}</tex>; другими Другими словами, «сравнять» строки возможно тогда и только тогда, когда автомат, принадлежащий <tex>M</tex>, допускает <tex>w</tex>. Таким образом, выполнено успешное m-сведение множества пар из машины Тьюринга (МТ) <tex>M</tex> и строки <tex>w</tex>, где <tex>M(w)</tex> не зависает, к множеству решений МПСП.

|<tex>\$ ' \#_{start} ab \$</tex> |<tex>\$'</tex>

|<tex>\$'</tex> |<tex>\#_{yes} \$ \$'</tex>

|<tex>\$ ' \#_{start} ab \$</tex> |<tex>\$'</tex>

|<tex>\$ ' \#_{start} ab \$ b \#_{start}</tex> |<tex>\$ ' \#_{start} a</tex>

|<tex>\$ ' \#_{start} ab \$ b \#_{start} b</tex> |<tex>\$ ' \#_{start} ab</tex>

|<tex>\$ ' \#_{start} ab \$ b \#_{start} b\$</tex> |<tex>\$ ' \#_{start} ab \$</tex>

|<tex>\$ ' \#_{start} ab \$ b \#_{start} b\$ b</tex> |<tex>\$ ' \#_{start} ab \$ b</tex>

|<tex>\$ ' \#_{start} ab \$ b \#_{start} b\$ b \#_{yes} b</tex> |<tex>\$ ' \#_{start} ab \$ b \#_{start} b</tex>

|<tex>\$ ' \#_{start} ab \$ b \#_{start} b\$ b \#_{yes} b \$</tex> |<tex>\$ ' \#_{start} ab \$ b \#_{start} b \$</tex>

|<tex>\$ ' \#_{start} ab \$ b \#_{start} b\$ b \#_{yes} b \$ \#_{yes}</tex> |<tex>\$ ' \#_{start} ab \$ b \#_{start} b \$ b \#_{yes}</tex>

|<tex>\$ ' \#_{start} ab \$ b \#_{start} b\$ b \#_{yes} b \$ \#_{yes} b</tex> |<tex>\$ ' \#_{start} ab \$ b \#_{start} b \$ b \#_{yes} b</tex>

|<tex>\$ ' \#_{start} ab \$ b \#_{start} b\$ b \#_{yes} b \$ \#_{yes} b \$</tex> |<tex>\$ ' \#_{start} ab \$ b \#_{start} b \$ b \#_{yes} b \$</tex>

|<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>

|<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>

|<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>