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.