Здесь используется рекурсивный вызов функции A. Чтобы доказать,
что для любых x, y, z эта программа вычислит A(z, x, y) за конечное
время, достаточно показать, что в ходе своей работы функция A вы-
зывает сама себя конечное число раз. Предположим противное. Тогда
существует бесконечная цепь рекурсивных вызовов функции A. Пусть
(z
0
, x, y
0
), (z
1
, x, y
1
), . . . — последовательность параметров, с которыми
функция A вызывает себя вдоль этой бесконечной цепи. Тогда для лю-
бого i ∈ N либо z
i+1
< z
i
, либо z
i+1
= z
i
и y
i+1
< y
i
. Так как z
i
не уве-
личивается, то для некоторого i
0
∈ N z
i
= z
i
0
для всех i > i
0
. Но тогда
y
i
0
> y
i
0
+1
> . . . — бесконечная строго убывающая последовательность
натуральных чисел. Противоречие. ¤
Лемма 6 Для всех z, y, y
1
, y
2
∈ N справедливы следующие соотношения:
1. A(z + 2, 2, 0) = 1, A(z + 2, 2, 1) = 2, A(z + 2, 2, 2) = 4;
2. A(z + 2, 2, y) > 2
y
;
3. A(z, 2, y + 1) > A(z, 2, y);
4. A(z + 2, 2, y + 3) > A(z + 1, 2, y + 3);
5. A(z + 2, 2, y + 3) > A(z + 1, 2, y + 4);
6. A(z + 2, 2, y
1
+ y
2
+ 3) 6 A(z + 4, 2, max{y
1
, y
2
} + 3).
Доказательство. (1). Индукция по z. Для z = 0 утверждение спра-
ведливо, так как A(2, 2, y) = 2
y
для всех y. Теперь для произвольного z
A(z+3, 2, 0) = 1 по определению, A(z+3, 2, 1) = A(z +2, 2, A(z +3, 2, 0)) =
A(z +2, 2, 1) = 2 и A(z +3, 2, 2) = A(z +2, 2, A(z +3, 2, 1)) = A(z +2, 2, 2) =
4.
(2) Докажем индукцией по z, что для любого y A(z + 2, 2, y) > 2
y
.
При z = 0 имеем равенство A(2, 2, y) = 2
y
. Пусть теперь для z это верно;
покажем, что это верно для z + 1, используя индукцию по y. При y = 0
имеем A(z + 3, 2, 0) = 1 = 2
0
. Теперь A(z + 3, 2, y + 1) = A(z + 2, 2, A(z +
3, 2, y)) > 2
A(z+3,2,y)
> 2
2
y
> 2
y+1
. Здесь мы использовали неравенство
2
y
> y, которое справедливо для всех y ∈ N и легко доказывается при
помощи индукции.
(3) При z = 0 , 1, 2 неравенство очевидно, так как A(0, 2, y) = 2 + y,
A(1, 2, y) = 2y и A(2, 2, y) = 2
y
. Пусть z > 3. По предыдущему A(z, 2, y +
1) = A(z − 1, 2, A(z, 2, y)) > 2
A(z,2,y)
> A(z, 2, y).
116