Induction Ackermann function

Hello,

I have to prove by induction that the following Ackerman function that takes pairs always halts:

How should I go about proving that when the function halts, then it returns a natural number? I don't need this assumption to prove that the first two cases of the formula halt, but for the third one, which takes I think I need to know that the second value is positive, which I have no idea how to surmise this.

Re: Induction Ackerman function

You do nested inductions: the outer one on x and the inner one on y. The induction statement (and hypothesis) for x is that A(x - 1, y) terminates *for all y*. It is important that the universal quantifier on y is included in the induction statement.