[edflsafoiewq]

> (not always)

Doesn't this work: consider the call graph of all possible argument lists (with an edge A->B if f(A) calls f(B)). If the function terminates, there are no cycles, so this is a DAG, which puts a partial order on the set of argument lists which strictly decreases with each call.

[jlokier]

You may find the Collatz conjecture interesting: https://en.wikipedia.org/wiki/Collatz_conjecture

It's an easy to understand loop, which can be written as a recursive function of one argument.

Even though the possible arguments are just the natural numbers, nobody knows how to identify a suitable ordering relation which decreases with each call.

[viewfromafar]

(I need sleep, Ackermann is actually very easy to show as decreasing using lexicographic order).

Yeah, if you know that the recursive function always terminates, then you know that each recursive call makes the set of remaining steps strictly smaller.

When you want to prove termination, then it is exactly what you need to show (that the remaining work does get smaller, no cycles).