The ints being a total ordered set is why the example will terminate. Change that to a float, where -0,0,+0 don't have a successor and it could be problematic.

The ints being a total ordered set is why the example will terminate. Change that to a float, where -0,0,+0 don't have a successor and it could be problematic. Effectively the example was an existential quantifier, but will universal quantification, termination analysis would be less optimistic. While it doesn't cover special cases like Ackerman functions, the time complexity is fairly easy to build intuition about with loops being forms of recusion for me. While is Turning complete or a general recursive functions For loops are primitive recursive functions The reason c make choices it made as an example is shown in this paper. For those who haven't seen it. https://people.csail.mit.edu/meyer/meyer-ritchie.pdf https://people.csail.mit.edu/meyer/meyer-ritchie.pdf