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))
  TDG 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))
   graph:
    avg#(xs) -> length#(xs) ->
    length#(:(x,xs)) -> length#(xs)
    avg#(xs) -> quot#(hd(sum(xs)),length(xs)) ->
    quot#(s(x),s(y)) -> quot#(-(x,y),s(y))
    avg#(xs) -> quot#(hd(sum(xs)),length(xs)) -> quot#(s(x),s(y)) -> -#(x,y)
    avg#(xs) -> sum#(xs) ->
    sum#(++(xs,:(x,:(y,ys)))) -> sum#(++(xs,sum(:(x,:(y,ys)))))
    avg#(xs) -> sum#(xs) ->
    sum#(++(xs,:(x,:(y,ys)))) -> ++#(xs,sum(:(x,:(y,ys))))
    avg#(xs) -> sum#(xs) -> sum#(++(xs,:(x,:(y,ys)))) -> sum#(:(x,:(y,ys)))
    avg#(xs) -> sum#(xs) -> sum#(:(x,:(y,xs))) -> sum#(:(+(x,y),xs))
    avg#(xs) -> sum#(xs) -> sum#(:(x,:(y,xs))) -> +#(x,y)
    length#(:(x,xs)) -> length#(xs) ->
    length#(:(x,xs)) -> length#(xs)
    quot#(s(x),s(y)) -> quot#(-(x,y),s(y)) ->
    quot#(s(x),s(y)) -> quot#(-(x,y),s(y))
    quot#(s(x),s(y)) -> quot#(-(x,y),s(y)) ->
    quot#(s(x),s(y)) -> -#(x,y)
    quot#(s(x),s(y)) -> -#(x,y) -> -#(s(x),s(y)) -> -#(x,y)
    -#(s(x),s(y)) -> -#(x,y) -> -#(s(x),s(y)) -> -#(x,y)
    sum#(:(x,:(y,xs))) -> sum#(:(+(x,y),xs)) ->
    sum#(++(xs,:(x,:(y,ys)))) -> sum#(++(xs,sum(:(x,:(y,ys)))))
    sum#(:(x,:(y,xs))) -> sum#(:(+(x,y),xs)) ->
    sum#(++(xs,:(x,:(y,ys)))) -> ++#(xs,sum(:(x,:(y,ys))))
    sum#(:(x,:(y,xs))) -> sum#(:(+(x,y),xs)) ->
    sum#(++(xs,:(x,:(y,ys)))) -> sum#(:(x,:(y,ys)))
    sum#(:(x,:(y,xs))) -> sum#(:(+(x,y),xs)) ->
    sum#(:(x,:(y,xs))) -> sum#(:(+(x,y),xs))
    sum#(:(x,:(y,xs))) -> sum#(:(+(x,y),xs)) ->
    sum#(:(x,:(y,xs))) -> +#(x,y)
    sum#(:(x,:(y,xs))) -> +#(x,y) ->
    +#(s(x),y) -> +#(x,y)
    sum#(++(xs,:(x,:(y,ys)))) -> sum#(:(x,:(y,ys))) ->
    sum#(++(xs,:(x,:(y,ys)))) -> sum#(++(xs,sum(:(x,:(y,ys)))))
    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#(:(x,:(y,ys))) ->
    sum#(++(xs,:(x,:(y,ys)))) -> sum#(:(x,:(y,ys)))
    sum#(++(xs,:(x,:(y,ys)))) -> sum#(:(x,:(y,ys))) ->
    sum#(:(x,:(y,xs))) -> sum#(:(+(x,y),xs))
    sum#(++(xs,:(x,:(y,ys)))) -> sum#(:(x,:(y,ys))) ->
    sum#(:(x,:(y,xs))) -> +#(x,y)
    sum#(++(xs,:(x,:(y,ys)))) -> sum#(++(xs,sum(:(x,:(y,ys))))) ->
    sum#(++(xs,:(x,:(y,ys)))) -> sum#(++(xs,sum(:(x,:(y,ys)))))
    sum#(++(xs,:(x,:(y,ys)))) -> sum#(++(xs,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))))) ->
    sum#(++(xs,:(x,:(y,ys)))) -> sum#(:(x,:(y,ys)))
    sum#(++(xs,:(x,:(y,ys)))) -> sum#(++(xs,sum(:(x,:(y,ys))))) ->
    sum#(:(x,:(y,xs))) -> sum#(:(+(x,y),xs))
    sum#(++(xs,:(x,:(y,ys)))) -> sum#(++(xs,sum(:(x,:(y,ys))))) ->
    sum#(:(x,:(y,xs))) -> +#(x,y)
    sum#(++(xs,:(x,:(y,ys)))) -> ++#(xs,sum(:(x,:(y,ys)))) ->
    ++#(:(x,xs),ys) -> ++#(xs,ys)
    ++#(:(x,xs),ys) -> ++#(xs,ys) -> ++#(:(x,xs),ys) -> ++#(xs,ys)
    +#(s(x),y) -> +#(x,y) -> +#(s(x),y) -> +#(x,y)
   EDG 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))
    graph:
     avg#(xs) -> length#(xs) ->
     length#(:(x,xs)) -> length#(xs)
     avg#(xs) -> quot#(hd(sum(xs)),length(xs)) ->
     quot#(s(x),s(y)) -> -#(x,y)
     avg#(xs) -> quot#(hd(sum(xs)),length(xs)) ->
     quot#(s(x),s(y)) -> quot#(-(x,y),s(y))
     avg#(xs) -> sum#(xs) -> sum#(:(x,:(y,xs))) -> +#(x,y)
     avg#(xs) -> sum#(xs) -> sum#(:(x,:(y,xs))) -> sum#(:(+(x,y),xs))
     avg#(xs) -> sum#(xs) -> sum#(++(xs,:(x,:(y,ys)))) -> sum#(:(x,:(y,ys)))
     avg#(xs) -> sum#(xs) ->
     sum#(++(xs,:(x,:(y,ys)))) -> ++#(xs,sum(:(x,:(y,ys))))
     avg#(xs) -> sum#(xs) ->
     sum#(++(xs,:(x,:(y,ys)))) -> sum#(++(xs,sum(:(x,:(y,ys)))))
     length#(:(x,xs)) -> length#(xs) ->
     length#(:(x,xs)) -> length#(xs)
     quot#(s(x),s(y)) -> quot#(-(x,y),s(y)) ->
     quot#(s(x),s(y)) -> -#(x,y)
     quot#(s(x),s(y)) -> quot#(-(x,y),s(y)) ->
     quot#(s(x),s(y)) -> quot#(-(x,y),s(y))
     quot#(s(x),s(y)) -> -#(x,y) -> -#(s(x),s(y)) -> -#(x,y)
     -#(s(x),s(y)) -> -#(x,y) -> -#(s(x),s(y)) -> -#(x,y)
     sum#(:(x,:(y,xs))) -> sum#(:(+(x,y),xs)) ->
     sum#(:(x,:(y,xs))) -> +#(x,y)
     sum#(:(x,:(y,xs))) -> sum#(:(+(x,y),xs)) ->
     sum#(:(x,:(y,xs))) -> sum#(:(+(x,y),xs))
     sum#(:(x,:(y,xs))) -> +#(x,y) ->
     +#(s(x),y) -> +#(x,y)
     sum#(++(xs,:(x,:(y,ys)))) -> sum#(:(x,:(y,ys))) ->
     sum#(:(x,:(y,xs))) -> +#(x,y)
     sum#(++(xs,:(x,:(y,ys)))) -> sum#(:(x,:(y,ys))) ->
     sum#(:(x,:(y,xs))) -> sum#(:(+(x,y),xs))
     sum#(++(xs,:(x,:(y,ys)))) -> sum#(++(xs,sum(:(x,:(y,ys))))) ->
     sum#(:(x,:(y,xs))) -> +#(x,y)
     sum#(++(xs,:(x,:(y,ys)))) -> sum#(++(xs,sum(:(x,:(y,ys))))) ->
     sum#(:(x,:(y,xs))) -> sum#(:(+(x,y),xs))
     sum#(++(xs,:(x,:(y,ys)))) -> sum#(++(xs,sum(:(x,:(y,ys))))) ->
     sum#(++(xs,:(x,:(y,ys)))) -> sum#(:(x,:(y,ys)))
     sum#(++(xs,:(x,:(y,ys)))) -> sum#(++(xs,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))))) ->
     sum#(++(xs,:(x,:(y,ys)))) -> sum#(++(xs,sum(:(x,:(y,ys)))))
     sum#(++(xs,:(x,:(y,ys)))) -> ++#(xs,sum(:(x,:(y,ys)))) ->
     ++#(:(x,xs),ys) -> ++#(xs,ys)
     ++#(:(x,xs),ys) -> ++#(xs,ys) -> ++#(:(x,xs),ys) -> ++#(xs,ys)
     +#(s(x),y) -> +#(x,y) -> +#(s(x),y) -> +#(x,y)
    SCC Processor:
     #sccs: 7
     #rules: 7
     #arcs: 26/225
     DPs:
      sum#(++(xs,:(x,:(y,ys)))) -> sum#(++(xs,sum(:(x,:(y,ys)))))
     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:
       [sum#](x0) = [2 0]x0 + [1],
       
                   [0 1]  
       [avg](x0) = [0 1]x0,
       
                  [2 2]  
       [hd](x0) = [1 1]x0,
       
                      [0 0]  
       [length](x0) = [0 1]x0,
       
                        [1 1]  
       [quot](x0, x1) = [0 0]x1,
       
                     [2 0]     [0 3]     [2]
       [-](x0, x1) = [0 1]x0 + [0 0]x1 + [2],
       
                   [1 0]     [0]
       [sum](x0) = [0 0]x0 + [1],
       
                     [1 1]          [0]
       [:](x0, x1) = [0 0]x0 + x1 + [1],
       
                      [3 0]     [2 1]  
       [++](x0, x1) = [2 2]x0 + [0 2]x1,
       
               [2]
       [nil] = [0],
       
                   
       [s](x0) = x0,
       
                     [1 0]       
       [+](x0, x1) = [0 0]x0 + x1,
       
             [0]
       [0] = [0]
      orientation:
       sum#(++(xs,:(x,:(y,ys)))) = [4 4]x + [6 0]xs + [4 4]y + [4 2]ys + [5] >= [4 4]x + [6 0]xs + [4 4]y + [4 0]ys + [3] = sum#(++(xs,sum(:(x,:(y,ys)))))
       
                            
       +(0(),y) = y >= y = y
       
                   [1 0]         [1 0]                 
       +(s(x),y) = [0 0]x + y >= [0 0]x + y = s(+(x,y))
       
                      [2 1]     [6]           
       ++(nil(),ys) = [0 2]ys + [4] >= ys = ys
       
                        [3 3]    [3 0]     [2 1]     [0]    [1 1]    [3 0]     [2 1]     [0]                 
       ++(:(x,xs),ys) = [2 2]x + [2 2]xs + [0 2]ys + [2] >= [0 0]x + [2 2]xs + [0 2]ys + [1] = :(x,++(xs,ys))
       
                         [1 1]    [2]    [1 1]    [2]             
       sum(:(x,nil())) = [0 0]x + [1] >= [0 0]x + [1] = :(x,nil())
       
                           [1 1]    [1 0]     [1 1]    [0]    [1 0]    [1 0]     [1 1]    [0]                    
       sum(:(x,:(y,xs))) = [0 0]x + [0 0]xs + [0 0]y + [1] >= [0 0]x + [0 0]xs + [0 0]y + [1] = sum(:(+(x,y),xs))
       
                                  [2 2]    [3 0]     [2 2]    [2 1]     [2]    [2 2]    [3 0]     [2 2]    [2 0]     [1]                                
       sum(++(xs,:(x,:(y,ys)))) = [0 0]x + [0 0]xs + [0 0]y + [0 0]ys + [1] >= [0 0]x + [0 0]xs + [0 0]y + [0 0]ys + [1] = sum(++(xs,sum(:(x,:(y,ys)))))
       
                  [2 0]    [2]         
       -(x,0()) = [0 1]x + [2] >= x = x
       
                     [0 3]    [2]    [0]      
       -(0(),s(y)) = [0 0]y + [2] >= [0] = 0()
       
                      [2 0]    [0 3]    [2]    [2 0]    [0 3]    [2]         
       -(s(x),s(y)) = [0 1]x + [0 0]y + [2] >= [0 1]x + [0 0]y + [2] = -(x,y)
       
                        [1 1]     [0]      
       quot(0(),s(y)) = [0 0]y >= [0] = 0()
       
                         [1 1]     [1 1]                        
       quot(s(x),s(y)) = [0 0]y >= [0 0]y = s(quot(-(x,y),s(y)))
       
                       [0]    [0]      
       length(nil()) = [0] >= [0] = 0()
       
                         [0 0]     [0]    [0 0]                  
       length(:(x,xs)) = [0 1]xs + [1] >= [0 1]xs = s(length(xs))
       
                     [2 2]    [2 2]     [2]         
       hd(:(x,xs)) = [1 1]x + [1 1]xs + [1] >= x = x
       
                 [0 1]      [0 1]                                 
       avg(xs) = [0 1]xs >= [0 0]xs = 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
     
     DPs:
      sum#(:(x,:(y,xs))) -> sum#(:(+(x,y),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))
     KBO Processor:
      argument filtering:
       pi(0) = []
       pi(+) = 1
       pi(s) = 0
       pi(nil) = []
       pi(++) = [0,1]
       pi(:) = [0,1]
       pi(sum) = 0
       pi(-) = [0]
       pi(quot) = []
       pi(length) = 0
       pi(hd) = 0
       pi(avg) = [0]
       pi(sum#) = 0
      weight function:
       w0 = 1
       w(sum#) = w(length) = w(quot) = w(:) = w(nil) = w(0) = 1
       w(avg) = w(hd) = w(-) = w(sum) = w(++) = w(s) = w(+) = 0
      precedence:
       avg ~ - ~ ++ ~ nil ~ + > quot > sum# ~ hd ~ length ~ sum ~ : ~ s ~ 0
      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
     
     DPs:
      +#(s(x),y) -> +#(x,y)
     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))
     KBO Processor:
      argument filtering:
       pi(0) = []
       pi(+) = [0,1]
       pi(s) = [0]
       pi(nil) = []
       pi(++) = [0,1]
       pi(:) = [0,1]
       pi(sum) = 0
       pi(-) = 0
       pi(quot) = 0
       pi(length) = [0]
       pi(hd) = 0
       pi(avg) = 0
       pi(+#) = 0
      weight function:
       w0 = 1
       w(+#) = w(hd) = w(length) = w(-) = w(:) = w(nil) = w(s) = w(0) = 1
       w(avg) = w(quot) = w(sum) = w(++) = w(+) = 0
      precedence:
       ++ ~ + > +# ~ avg ~ hd ~ length ~ quot ~ - ~ sum ~ : ~ nil ~ s ~ 0
      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
     
     DPs:
      ++#(:(x,xs),ys) -> ++#(xs,ys)
     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))
     KBO Processor:
      argument filtering:
       pi(0) = []
       pi(+) = 1
       pi(s) = 0
       pi(nil) = []
       pi(++) = [0,1]
       pi(:) = [0,1]
       pi(sum) = 0
       pi(-) = 0
       pi(quot) = 0
       pi(length) = []
       pi(hd) = 0
       pi(avg) = 0
       pi(++#) = [0,1]
      weight function:
       w0 = 1
       w(++#) = w(avg) = w(hd) = w(length) = w(quot) = w(-) = w(nil) = w(
       s) = w(0) = 1
       w(sum) = w(:) = w(++) = w(+) = 0
      precedence:
       ++# ~ length ~ ++ > avg ~ hd ~ quot ~ - ~ sum ~ : ~ nil ~ s ~ + ~ 0
      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
     
     DPs:
      quot#(s(x),s(y)) -> quot#(-(x,y),s(y))
     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))
     KBO Processor:
      argument filtering:
       pi(0) = []
       pi(+) = [0,1]
       pi(s) = [0]
       pi(nil) = []
       pi(++) = [0,1]
       pi(:) = [0,1]
       pi(sum) = 0
       pi(-) = 0
       pi(quot) = 0
       pi(length) = 0
       pi(hd) = 0
       pi(avg) = 0
       pi(quot#) = 0
      weight function:
       w0 = 1
       w(quot#) = w(hd) = w(sum) = w(:) = w(nil) = w(s) = w(0) = 1
       w(avg) = w(length) = w(quot) = w(-) = w(++) = w(+) = 0
      precedence:
       sum > ++ ~ + > nil > quot# ~ avg ~ hd ~ length ~ quot ~ - ~ : ~ s ~ 0
      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
     
     DPs:
      -#(s(x),s(y)) -> -#(x,y)
     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))
     KBO Processor:
      argument filtering:
       pi(0) = []
       pi(+) = [0,1]
       pi(s) = [0]
       pi(nil) = []
       pi(++) = [0,1]
       pi(:) = [0,1]
       pi(sum) = 0
       pi(-) = 0
       pi(quot) = 0
       pi(length) = 0
       pi(hd) = 0
       pi(avg) = 0
       pi(-#) = 1
      weight function:
       w0 = 1
       w(-#) = w(avg) = w(hd) = w(quot) = w(-) = w(sum) = w(:) = w(nil) = w(
       s) = w(0) = 1
       w(length) = w(++) = w(+) = 0
      precedence:
       sum > nil > ++ ~ + > -# ~ avg ~ hd ~ length ~ quot ~ - ~ : ~ s ~ 0
      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
     
     DPs:
      length#(:(x,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))
     KBO Processor:
      argument filtering:
       pi(0) = []
       pi(+) = [1]
       pi(s) = 0
       pi(nil) = []
       pi(++) = [0,1]
       pi(:) = [0,1]
       pi(sum) = 0
       pi(-) = 0
       pi(quot) = [1]
       pi(length) = []
       pi(hd) = 0
       pi(avg) = [0]
       pi(length#) = 0
      weight function:
       w0 = 1
       w(length#) = w(avg) = w(hd) = w(length) = w(-) = w(sum) = w(nil) = w(
       0) = 1
       w(quot) = w(:) = w(++) = w(s) = w(+) = 0
      precedence:
       avg ~ length ~ quot ~ ++ ~ nil ~ s ~ + > length# ~ hd ~ - ~ sum ~ : ~ 0
      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