The Canto pairing function C from N x N into N is defined by C(x,y) = (1/2)
(x + y)(x + y + 1) + y. The first order theory of natural integers equippe
d with the Cantor. pairing functions is decidable. (C) 2000 Academie des sc
iences/Editions scientifiques ct medicales Elsevier SAS.