YES

Problem:
 +(0(),y) -> y
 +(s(x),y) -> s(+(x,y))
 ++(nil(),ys) -> ys
 ++(:(x,xs),ys) -> :(x,++(xs,ys))
 sum(:(x,nil())) -> :(x,nil())
 sum(:(x,:(y,xs))) -> sum(:(+(x,y),xs))
 sum(++(xs,:(x,:(y,ys)))) -> sum(++(xs,sum(:(x,:(y,ys)))))
 -(x,0()) -> x
 -(0(),s(y)) -> 0()
 -(s(x),s(y)) -> -(x,y)
 quot(0(),s(y)) -> 0()
 quot(s(x),s(y)) -> s(quot(-(x,y),s(y)))
 length(nil()) -> 0()
 length(:(x,xs)) -> s(length(xs))
 hd(:(x,xs)) -> x
 avg(xs) -> quot(hd(sum(xs)),length(xs))

Proof:
 DP Processor:
  DPs:
   +#(s(x),y) -> +#(x,y)
   ++#(:(x,xs),ys) -> ++#(xs,ys)
   sum#(:(x,:(y,xs))) -> +#(x,y)
   sum#(:(x,:(y,xs))) -> sum#(:(+(x,y),xs))
   sum#(++(xs,:(x,:(y,ys)))) -> sum#(:(x,:(y,ys)))
   sum#(++(xs,:(x,:(y,ys)))) -> ++#(xs,sum(:(x,:(y,ys))))
   sum#(++(xs,:(x,:(y,ys)))) -> sum#(++(xs,sum(:(x,:(y,ys)))))
   -#(s(x),s(y)) -> -#(x,y)
   quot#(s(x),s(y)) -> -#(x,y)
   quot#(s(x),s(y)) -> quot#(-(x,y),s(y))
   length#(:(x,xs)) -> length#(xs)
   avg#(xs) -> length#(xs)
   avg#(xs) -> sum#(xs)
   avg#(xs) -> hd#(sum(xs))
   avg#(xs) -> quot#(hd(sum(xs)),length(xs))
  TRS:
   +(0(),y) -> y
   +(s(x),y) -> s(+(x,y))
   ++(nil(),ys) -> ys
   ++(:(x,xs),ys) -> :(x,++(xs,ys))
   sum(:(x,nil())) -> :(x,nil())
   sum(:(x,:(y,xs))) -> sum(:(+(x,y),xs))
   sum(++(xs,:(x,:(y,ys)))) -> sum(++(xs,sum(:(x,:(y,ys)))))
   -(x,0()) -> x
   -(0(),s(y)) -> 0()
   -(s(x),s(y)) -> -(x,y)
   quot(0(),s(y)) -> 0()
   quot(s(x),s(y)) -> s(quot(-(x,y),s(y)))
   length(nil()) -> 0()
   length(:(x,xs)) -> s(length(xs))
   hd(:(x,xs)) -> x
   avg(xs) -> quot(hd(sum(xs)),length(xs))
  Matrix Interpretation Processor: dim=2
   
   interpretation:
    [avg#](x0) = [2 3]x0 + [3],
    
    [hd#](x0) = [0],
    
    [length#](x0) = [0 2]x0,
    
    [quot#](x0, x1) = [1 0]x0 + [1],
    
    [-#](x0, x1) = [1 0]x0 + [1],
    
    [sum#](x0) = [0 2]x0,
    
    [++#](x0, x1) = [0 1]x0 + [0 2]x1 + [1],
    
    [+#](x0, x1) = [2 2]x0 + [0 2]x1,
    
                [0 3]     [1]
    [avg](x0) = [2 2]x0 + [0],
    
               [0 2]     [1]
    [hd](x0) = [0 2]x0 + [3],
    
                   [0 1]  
    [length](x0) = [0 0]x0,
    
                     [1 0]     [0 1]  
    [quot](x0, x1) = [0 0]x0 + [1 0]x1,
    
                    
    [-](x0, x1) = x0,
    
                [0 0]  
    [sum](x0) = [0 1]x0,
    
                  [0 0]     [0 1]     [0]
    [:](x0, x1) = [1 1]x0 + [0 1]x1 + [1],
    
                   [0 2]     [2 2]  
    [++](x0, x1) = [0 1]x0 + [1 1]x1,
    
            [0]
    [nil] = [0],
    
                   [1]
    [s](x0) = x0 + [0],
    
                  [1 1]       
    [+](x0, x1) = [0 0]x0 + x1,
    
          [0]
    [0] = [0]
   orientation:
    +#(s(x),y) = [2 2]x + [0 2]y + [2] >= [2 2]x + [0 2]y = +#(x,y)
    
    ++#(:(x,xs),ys) = [1 1]x + [0 1]xs + [0 2]ys + [2] >= [0 1]xs + [0 2]ys + [1] = ++#(xs,ys)
    
    sum#(:(x,:(y,xs))) = [2 2]x + [0 2]xs + [2 2]y + [4] >= [2 2]x + [0 2]y = +#(x,y)
    
    sum#(:(x,:(y,xs))) = [2 2]x + [0 2]xs + [2 2]y + [4] >= [2 2]x + [0 2]xs + [2 2]y + [2] = sum#(:(+(x,y),xs))
    
    sum#(++(xs,:(x,:(y,ys)))) = [2 2]x + [0 2]xs + [4 4]y + [0 4]ys + [6] >= [2 2]x + [2 2]y + [0 2]ys + [4] = sum#(:(x,:(y,ys)))
    
    sum#(++(xs,:(x,:(y,ys)))) = [2 2]x + [0 2]xs + [4 4]y + [0 4]ys + [6] >= [2 2]x + [0 1]xs + [2 2]y + [0 2]ys + [5] = ++#(xs,sum(:(x,:(y,ys))))
    
    sum#(++(xs,:(x,:(y,ys)))) = [2 2]x + [0 2]xs + [4 4]y + [0 4]ys + [6] >= [2 2]x + [0 2]xs + [2 2]y + [0 2]ys + [4] = sum#(++(xs,sum(:(x,:(y,ys)))))
    
    -#(s(x),s(y)) = [1 0]x + [2] >= [1 0]x + [1] = -#(x,y)
    
    quot#(s(x),s(y)) = [1 0]x + [2] >= [1 0]x + [1] = -#(x,y)
    
    quot#(s(x),s(y)) = [1 0]x + [2] >= [1 0]x + [1] = quot#(-(x,y),s(y))
    
    length#(:(x,xs)) = [2 2]x + [0 2]xs + [2] >= [0 2]xs = length#(xs)
    
    avg#(xs) = [2 3]xs + [3] >= [0 2]xs = length#(xs)
    
    avg#(xs) = [2 3]xs + [3] >= [0 2]xs = sum#(xs)
    
    avg#(xs) = [2 3]xs + [3] >= [0] = hd#(sum(xs))
    
    avg#(xs) = [2 3]xs + [3] >= [0 2]xs + [2] = quot#(hd(sum(xs)),length(xs))
    
                         
    +(0(),y) = y >= y = y
    
                [1 1]        [1]    [1 1]        [1]            
    +(s(x),y) = [0 0]x + y + [0] >= [0 0]x + y + [0] = s(+(x,y))
    
                   [2 2]             
    ++(nil(),ys) = [1 1]ys >= ys = ys
    
                     [2 2]    [0 2]     [2 2]     [2]    [0 0]    [0 1]     [1 1]     [0]                 
    ++(:(x,xs),ys) = [1 1]x + [0 1]xs + [1 1]ys + [1] >= [1 1]x + [0 1]xs + [1 1]ys + [1] = :(x,++(xs,ys))
    
                      [0 0]    [0]    [0 0]    [0]             
    sum(:(x,nil())) = [1 1]x + [1] >= [1 1]x + [1] = :(x,nil())
    
                        [0 0]    [0 0]     [0 0]    [0]    [0 0]    [0 0]     [0 0]    [0]                    
    sum(:(x,:(y,xs))) = [1 1]x + [0 1]xs + [1 1]y + [2] >= [1 1]x + [0 1]xs + [1 1]y + [1] = sum(:(+(x,y),xs))
    
                               [0 0]    [0 0]     [0 0]    [0 0]     [0]    [0 0]    [0 0]     [0 0]    [0 0]     [0]                                
    sum(++(xs,:(x,:(y,ys)))) = [1 1]x + [0 1]xs + [2 2]y + [0 2]ys + [3] >= [1 1]x + [0 1]xs + [1 1]y + [0 1]ys + [2] = sum(++(xs,sum(:(x,:(y,ys)))))
    
                         
    -(x,0()) = x >= x = x
    
                  [0]    [0]      
    -(0(),s(y)) = [0] >= [0] = 0()
    
                       [1]              
    -(s(x),s(y)) = x + [0] >= x = -(x,y)
    
                     [0 1]    [0]    [0]      
    quot(0(),s(y)) = [1 0]y + [1] >= [0] = 0()
    
                      [1 0]    [0 1]    [1]    [1 0]    [0 1]    [1]                       
    quot(s(x),s(y)) = [0 0]x + [1 0]y + [1] >= [0 0]x + [1 0]y + [1] = s(quot(-(x,y),s(y)))
    
                    [0]    [0]      
    length(nil()) = [0] >= [0] = 0()
    
                      [1 1]    [0 1]     [1]    [0 1]     [1]                
    length(:(x,xs)) = [0 0]x + [0 0]xs + [0] >= [0 0]xs + [0] = s(length(xs))
    
                  [2 2]    [0 2]     [3]         
    hd(:(x,xs)) = [2 2]x + [0 2]xs + [5] >= x = x
    
              [0 3]     [1]    [0 2]     [1]                               
    avg(xs) = [2 2]xs + [0] >= [0 1]xs + [0] = quot(hd(sum(xs)),length(xs))
   problem:
    DPs:
     
    TRS:
     +(0(),y) -> y
     +(s(x),y) -> s(+(x,y))
     ++(nil(),ys) -> ys
     ++(:(x,xs),ys) -> :(x,++(xs,ys))
     sum(:(x,nil())) -> :(x,nil())
     sum(:(x,:(y,xs))) -> sum(:(+(x,y),xs))
     sum(++(xs,:(x,:(y,ys)))) -> sum(++(xs,sum(:(x,:(y,ys)))))
     -(x,0()) -> x
     -(0(),s(y)) -> 0()
     -(s(x),s(y)) -> -(x,y)
     quot(0(),s(y)) -> 0()
     quot(s(x),s(y)) -> s(quot(-(x,y),s(y)))
     length(nil()) -> 0()
     length(:(x,xs)) -> s(length(xs))
     hd(:(x,xs)) -> x
     avg(xs) -> quot(hd(sum(xs)),length(xs))
   Qed