Изменения
→Теорема Успенского-Райса
Предположим, что <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>\varnothing </tex> и <tex> \mathrm {RE} \setminus A</tex> != <tex>\mathrm {RE} ) </tex>. Исключение пустого множества нам нужно чтобы различать <tex> X</tex> и пустое (при построении функции <tex>L(g_{i,x}))</tex>).
Поскольку <tex>A</tex> непусто, то найдётся перечислимый язык <tex>X \in A</tex>. Пусть <tex>p_X</tex> {{---}} полуразрешитель <tex>X</tex>.