YES

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

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