TRS:
 {           p(0()) -> 0(),
            p(s(X)) -> X,
        leq(0(), Y) -> true(),
     leq(s(X), 0()) -> false(),
    leq(s(X), s(Y)) -> leq(X, Y),
   if(true(), X, Y) -> X,
  if(false(), X, Y) -> Y,
         diff(X, Y) -> if(leq(X, Y), 0(), s(diff(p(X), Y)))}
 Fail