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.
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.
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.