On solving the equivalence problem for a sub-class of primitive recursive functions

In the paper we constructively define the sub-class P of primitive recursive functions which can be defined from the base functions 0, s, x+y and x-y,and closed under composition. We show that the equivalence problem for P is solvable by reducing the function definitions according to a Church-Rosser Noetherian term rewriting system and testing the resulting irreducible terms for identity. Finally, we define an effective mapping from primitive recursive definitions to the definitions of the class P.