Статья 430

Очевидно, эта область определяется теми представимыми и для которых число также представило. Значит, если представило, то выполнение непременно закончится, и притом в состоянии, обеспечивающем истинность утверждения. Отсюда ясно, что утверждение представило следует ввести в предусловие, если мы хотим все-таки получить истинное утверждение о тотальной правильности.
В силу приведенных выше рассуждений, истинность данного утверждения доказана. В условиях невозможности определить при помощи компьютера операцию возведения в степень для любых и это не такое уж плохое достижение.
Обсуждая понятия, связанные с доказательством правильности программ, мы совсем не касались вопроса об эффективности использования машинных ресурсов - времени и памяти. Это не случайно, поскольку правильность и эффективность - независимые свойства программ.