 Primitive recursive pairing function

A pairing function whose forward map and two inverse coordinate functions are primitive recursive functions. For example, the Cantor pairing function $⟨x,y⟩=(x+y)(x+y+1)/2+y$ has such inverses: find the diagonal index by bounded minimization over integers at most the encoded value, then recover $x,y$ by subtraction. It enables finite tuples to be decoded within a primitive recursive construction.