Изменения
→Теорема Успенского-Райса
Предположим, что <tex>A</tex> разрешимо и нетривиально, <tex>p_A</tex> {{---}} программа, разрешающая <tex>A</tex>.
Не умаляя общности, можно считать, что <tex>\varnothing \notin A</tex> (в противном случае перейдём к <tex> \mathrm {RE} \setminus A</tex>, которое также будет разрешимым и нетривиальным, так как <tex> \mathrm {RE} \setminus A</tex> и <tex> \mathrm {RE} \setminus A</tex> ).
Поскольку <tex>A</tex> непусто, то найдётся перечислимый язык <tex>X \in A</tex>. Пусть <tex>p_X</tex> {{---}} полуразрешитель <tex>X</tex>.
