YES

Problem:
 sum(0()) -> 0()
 sum(s(x)) -> +(sum(x),s(x))
 sum1(0()) -> 0()
 sum1(s(x)) -> s(+(sum1(x),+(x,x)))

Proof:
 DP Processor:
  DPs:
   sum#(s(x)) -> sum#(x)
   sum1#(s(x)) -> sum1#(x)
  TRS:
   sum(0()) -> 0()
   sum(s(x)) -> +(sum(x),s(x))
   sum1(0()) -> 0()
   sum1(s(x)) -> s(+(sum1(x),+(x,x)))
  Arctic Interpretation Processor:
   dimension: 1
   interpretation:
    [sum1#](x0) = 1x0,
    
    [sum#](x0) = 2x0,
    
    [sum1](x0) = 2x0 + 5,
    
    [+](x0, x1) = 0,
    
    [s](x0) = 4x0,
    
    [sum](x0) = 1,
    
    [0] = 0
   orientation:
    sum#(s(x)) = 6x >= 2x = sum#(x)
    
    sum1#(s(x)) = 5x >= 1x = sum1#(x)
    
    sum(0()) = 1 >= 0 = 0()
    
    sum(s(x)) = 1 >= 0 = +(sum(x),s(x))
    
    sum1(0()) = 5 >= 0 = 0()
    
    sum1(s(x)) = 6x + 5 >= 4 = s(+(sum1(x),+(x,x)))
   problem:
    DPs:
     
    TRS:
     sum(0()) -> 0()
     sum(s(x)) -> +(sum(x),s(x))
     sum1(0()) -> 0()
     sum1(s(x)) -> s(+(sum1(x),+(x,x)))
   Qed