pub fn ackermann_function_terminates() -> bool
Certified fact: the Ackermann function A(m, n) terminates for all m, n : ℕ.
Proof: The pair (m, n) decreases under the lexicographic order on ℕ × ℕ, which is well-founded. QED.