TRS:
 {    +(0(), y) -> y,
     +(s(x), y) -> s(+(x, y)),
      -(0(), y) -> 0(),
      -(x, 0()) -> x,
  -(s(x), s(y)) -> -(x, y)}
 POP*:
  Precedence:
  + > s
  empty
  
Normal:
   pi(-) = [1,2], pi(+) = [1,2]
  
Safe:
   pi(s) = [1]
  
Predicative System:
   {      +(0(),y;) -> y,
        +(s(;x),y;) -> s(;+(x,y;)),
          -(0(),y;) -> 0(),
          -(x,0();) -> x,
    -(s(;x),s(;y);) -> -(x,y;)}
  Qed