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