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

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):"