TRS:
 { -(0(), y) -> 0(),
   -(x, 0()) -> x,
  -(x, s(y)) -> if(greater(x, s(y)), s(-(x, p(s(y)))), 0()),
      p(0()) -> 0(),
     p(s(x)) -> x}
 Fail