Lexicographic ordering arguments

This is the Ackermann function:

$$\begin{align} & A(0, n) = n + 1 \\ & A(m + 1, 0) = A(m, n) \\ & A(m + 1, n + 1) = A(m, A(m + 1, n)) \end{align}$$

Arguably the most interesting property of this function, is that it's total, but not primitive recursive. How do we know this function terminates then? Notice that \(A\) terminates when \(m\) reaches \(0,\) so we have to show that \(m\) reaches \(0,\) regardless of what \(m\) and \(n\) are. To this end, notice that either \(m\) decreases, or \(m\) remains the same and \(n\) decreases. Whenever \(n\) reaches \(0,\) \(m\) decreases, and so eventually \(m\) must reach \(0,\) causing \(A\) to terminate.

This is a particular instance of a lexicographic ordering argument. This type of argument can prove any primitive recursive function terminates, as well as some other functions like \(A.\)