Proving an invariant in a recursion using mathematical induction

Given the following pseudocode for function AP(x, y: integer) which returns an integer,

function AP(x,y: integer):
if x = 0 then return y+1
else
if y = 0 then return AP(x-1,1)
else return AP(x-1, AP(x,y-1))


I need to prove, $\forall x (AP(x, y) > y)$.

I have tried solving it using mathematical induction,
Basis: $AP(0, y) = y + 1$
Inductive step: Assuming, $AP(n, y) > y$ and $y > 0$
Prove that $AP(n + 1, y) = AP(n, AP(n + 1, y - 1)) > y$

By unrolling recursion, I get relations like,
$AP(n + 1, y) > AP(n + 1, y - 1) > AP(n, 1)$,
but I am not sure how to proceed from here.

• Use double induction. That is do an induction proof inside of your induction step. Or do the whole thing by strong induction on lexicographic ordering of pairs of integers. – Jake Dec 23 '16 at 6:01