The Ackermann function is well-defined.

This is easily proved by lexicographic induction on $\mathbb N\times \mathbb N$. But perhaps not easily formulated -- I can only think of this awkward formulation: For every $x,y$ there is a unique function on the initial segment determined by $(x,y)$ satisfying the Ackermann recursion.