Note there is a typo in the def of the predecessor function

"The following function generates from the pair (n, n − 1) (which is the argument p in the function) the pair (n + 1, n − 1):"

which should be

"The following function generates from the pair (n, n − 1) (which is the argument p in the function) the pair (n + 1, n):"