Abstract
Ackermann's function is defined in the usual way and a number of
its elementary properties are proved. Then, the primitive recursive
functions are defined inductively: as a predicate on the functions
that map lists of numbers to numbers. It is shown that every
primitive recursive function is strictly dominated by Ackermann's
function. The formalisation follows an earlier one by Nora Szasz.