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

   
  

  Qed