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