Изменения

Так как <tex>U</tex> - универсальная, то найдется вычислимая всюду определенная <tex>h</tex> такая что <tex>\forall n, x</tex> <tex>V(n, x) = U(h(n), x)</tex>. <br >По доказанному найдется такое <tex>n_0</tex> что <tex>U_{n0} = U_{h(n0n_0)}</tex>. <br> Тогда <tex>V(n0n_0, x) = U(h(n0n_0), x) = U(n0n_0, x)</tex>. Взяв <tex>p=U_{n0n_0}</tex> получаем требуемое утверждение.}}Неформально теорема о рекурсии утверждает то что внутри программы можно использовать ее код. Это упрощает доказательство некоторых теорем.==Пример==Используя теорему о рекурсии приведем простое доказательство неразрешимости языка <tex>L=\{p|p(\epsilon)=\perp\}</tex>{{Утверждение|id=st2|statement= Язык <tex>L=\{p|p(\epsilon)=\perp\}</tex> неразрешим. |proof=Предположим обратное, тогда существует программа <tex>r</tex> разрещающая <tex>L</tex>.Рассмотрим следущую программу <code> p(x) if r(p) return 1 while true</code>Пусть <tex>p(\epsilon)=\perp</tex>. Тогда условие <tex>r(p)</tex> выполняется и <tex>p(\epsilon)=1</tex>. Противоречие. Если <tex>p(\epsilon) \ne \perp</tex>, то <tex>r(p)</tex> не выполняется и <tex>p(\epsilon)=\perp</tex>. Противоречие.