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))
  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))
    Usable Rule Processor:
     DPs:
      sum#(++(xs,:(x,:(y,ys)))) -> sum#(++(xs,sum(:(x,:(y,ys)))))
     TRS:
      sum(:(x,:(y,xs))) -> sum(:(+(x,y),xs))
      sum(:(x,nil())) -> :(x,nil())
      +(0(),y) -> y
      +(s(x),y) -> s(+(x,y))
      ++(nil(),ys) -> ys
      ++(:(x,xs),ys) -> :(x,++(xs,ys))
     Bounds Processor:
      bound: 0
      enrichment: match-dp
      automaton:
       final states: {9}
       transitions:
        sum{#,0}(13) -> 9*
        ++0(3,1) -> 3*
        ++0(3,3) -> 3*
        ++0(3,5) -> 3*
        ++0(3,7) -> 3*
        ++0(4,2) -> 3*
        ++0(4,4) -> 3*
        ++0(4,6) -> 3*
        ++0(5,1) -> 3*
        ++0(5,3) -> 3*
        ++0(5,5) -> 3*
        ++0(5,7) -> 3*
        ++0(6,2) -> 3*
        ++0(1,2) -> 3*
        ++0(6,4) -> 3*
        ++0(1,4) -> 3*
        ++0(6,6) -> 3*
        ++0(1,6) -> 3*
        ++0(7,1) -> 3*
        ++0(2,1) -> 3*
        ++0(7,3) -> 3*
        ++0(2,3) -> 3*
        ++0(7,5) -> 3*
        ++0(2,5) -> 3*
        ++0(7,7) -> 3*
        ++0(2,7) -> 3*
        ++0(3,2) -> 3*
        ++0(3,4) -> 3*
        ++0(3,6) -> 3*
        ++0(8,12) -> 13*
        ++0(4,1) -> 3*
        ++0(4,3) -> 3*
        ++0(4,5) -> 3*
        ++0(4,7) -> 3*
        ++0(5,2) -> 3*
        ++0(5,4) -> 3*
        ++0(5,6) -> 3*
        ++0(6,1) -> 3*
        ++0(1,1) -> 3*
        ++0(6,3) -> 3*
        ++0(1,3) -> 3*
        ++0(6,5) -> 3*
        ++0(1,5) -> 3*
        ++0(6,7) -> 3*
        ++0(1,7) -> 3*
        ++0(7,2) -> 3*
        ++0(2,2) -> 3*
        ++0(7,4) -> 3*
        ++0(2,4) -> 3*
        ++0(7,6) -> 3*
        ++0(2,6) -> 3*
        :0(3,1) -> 2*
        :0(3,3) -> 2*
        :0(3,5) -> 1,2
        :0(3,7) -> 2*
        :0(3,13) -> 13*
        :0(4,2) -> 2*
        :0(4,4) -> 2*
        :0(14,8) -> 11*
        :0(4,6) -> 2*
        :0(5,1) -> 2*
        :0(5,3) -> 2*
        :0(5,5) -> 1,2
        :0(5,7) -> 2*
        :0(6,2) -> 2*
        :0(1,2) -> 2*
        :0(6,4) -> 2*
        :0(1,4) -> 2*
        :0(6,6) -> 2*
        :0(1,6) -> 2*
        :0(7,1) -> 2*
        :0(2,1) -> 2*
        :0(7,3) -> 2*
        :0(2,3) -> 2*
        :0(7,5) -> 1,2
        :0(2,5) -> 1,2
        :0(7,7) -> 2*
        :0(2,7) -> 2*
        :0(3,2) -> 2*
        :0(3,4) -> 2*
        :0(3,6) -> 2*
        :0(8,8) -> 10*
        :0(8,10) -> 11*
        :0(4,1) -> 2*
        :0(14,5) -> 12,13
        :0(4,3) -> 2*
        :0(4,5) -> 1,2
        :0(4,7) -> 2*
        :0(5,2) -> 2*
        :0(5,4) -> 2*
        :0(5,6) -> 2*
        :0(6,1) -> 2*
        :0(1,1) -> 2*
        :0(6,3) -> 2*
        :0(1,3) -> 2*
        :0(6,5) -> 1,2
        :0(1,5) -> 1,2
        :0(6,7) -> 2*
        :0(1,7) -> 2*
        :0(7,2) -> 2*
        :0(2,2) -> 2*
        :0(7,4) -> 2*
        :0(2,4) -> 2*
        :0(7,6) -> 2*
        :0(2,6) -> 2*
        sum0(5) -> 1*
        sum0(7) -> 1*
        sum0(2) -> 1*
        sum0(4) -> 1*
        sum0(11) -> 12*
        sum0(6) -> 1*
        sum0(1) -> 1*
        sum0(3) -> 1*
        +0(3,1) -> 4*
        +0(3,3) -> 4*
        +0(3,5) -> 4*
        +0(3,7) -> 4*
        +0(4,2) -> 4*
        +0(4,4) -> 4*
        +0(4,6) -> 4*
        +0(5,1) -> 4*
        +0(5,3) -> 4*
        +0(5,5) -> 4*
        +0(5,7) -> 4*
        +0(6,2) -> 4*
        +0(1,2) -> 4*
        +0(6,4) -> 4*
        +0(1,4) -> 4*
        +0(6,6) -> 4*
        +0(1,6) -> 4*
        +0(7,1) -> 4*
        +0(2,1) -> 4*
        +0(7,3) -> 4*
        +0(2,3) -> 4*
        +0(7,5) -> 4*
        +0(2,5) -> 4*
        +0(7,7) -> 4*
        +0(2,7) -> 4*
        +0(3,2) -> 4*
        +0(3,4) -> 4*
        +0(3,6) -> 4*
        +0(8,8) -> 14*
        +0(14,3) -> 14*
        +0(4,1) -> 4*
        +0(4,3) -> 4*
        +0(4,5) -> 4*
        +0(4,7) -> 4*
        +0(5,2) -> 4*
        +0(5,4) -> 4*
        +0(5,6) -> 4*
        +0(6,1) -> 4*
        +0(1,1) -> 4*
        +0(6,3) -> 4*
        +0(1,3) -> 4*
        +0(6,5) -> 4*
        +0(1,5) -> 4*
        +0(6,7) -> 4*
        +0(1,7) -> 4*
        +0(7,2) -> 4*
        +0(2,2) -> 4*
        +0(7,4) -> 4*
        +0(2,4) -> 4*
        +0(7,6) -> 4*
        +0(2,6) -> 4*
        nil0() -> 5*
        00() -> 6*
        s0(5) -> 7*
        s0(7) -> 7*
        s0(2) -> 7*
        s0(14) -> 14*
        s0(4) -> 7*
        s0(6) -> 7*
        s0(1) -> 7*
        s0(3) -> 7*
        1 -> 4,8
        2 -> 4,8
        3 -> 4,8
        4 -> 3,8
        5 -> 4,8
        6 -> 3,4,8
        7 -> 4,8
        8 -> 14*
        12 -> 13*
      problem:
       DPs:
        
       TRS:
        sum(:(x,:(y,xs))) -> sum(:(+(x,y),xs))
        sum(:(x,nil())) -> :(x,nil())
        +(0(),y) -> y
        +(s(x),y) -> s(+(x,y))
        ++(nil(),ys) -> ys
        ++(:(x,xs),ys) -> :(x,++(xs,ys))
      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))
    Matrix Interpretation Processor:
     dimension: 1
     interpretation:
      [sum#](x0) = x0,
      
      [avg](x0) = 0,
      
      [hd](x0) = x0 + 1,
      
      [length](x0) = 0,
      
      [quot](x0, x1) = 0,
      
      [-](x0, x1) = x0,
      
      [sum](x0) = x0,
      
      [:](x0, x1) = x0 + x1 + 1,
      
      [++](x0, x1) = x0 + x1,
      
      [nil] = 0,
      
      [s](x0) = x0,
      
      [+](x0, x1) = x0 + x1,
      
      [0] = 0
     orientation:
      sum#(:(x,:(y,xs))) = x + xs + y + 2 >= x + xs + y + 1 = sum#(:(+(x,y),xs))
      
      +(0(),y) = y >= y = y
      
      +(s(x),y) = x + y >= x + y = s(+(x,y))
      
      ++(nil(),ys) = ys >= ys = ys
      
      ++(:(x,xs),ys) = x + xs + ys + 1 >= x + xs + ys + 1 = :(x,++(xs,ys))
      
      sum(:(x,nil())) = x + 1 >= x + 1 = :(x,nil())
      
      sum(:(x,:(y,xs))) = x + xs + y + 2 >= x + xs + y + 1 = sum(:(+(x,y),xs))
      
      sum(++(xs,:(x,:(y,ys)))) = x + xs + y + ys + 2 >= x + xs + y + ys + 2 = sum(++(xs,sum(:(x,:(y,ys)))))
      
      -(x,0()) = x >= x = x
      
      -(0(),s(y)) = 0 >= 0 = 0()
      
      -(s(x),s(y)) = x >= x = -(x,y)
      
      quot(0(),s(y)) = 0 >= 0 = 0()
      
      quot(s(x),s(y)) = 0 >= 0 = s(quot(-(x,y),s(y)))
      
      length(nil()) = 0 >= 0 = 0()
      
      length(:(x,xs)) = 0 >= 0 = s(length(xs))
      
      hd(:(x,xs)) = x + xs + 2 >= x = x
      
      avg(xs) = 0 >= 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
    
    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))
    Subterm Criterion Processor:
     simple projection:
      pi(+#) = 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))
    Subterm Criterion Processor:
     simple projection:
      pi(++#) = 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))
    Matrix Interpretation Processor:
     dimension: 1
     interpretation:
      [quot#](x0, x1) = x0,
      
      [avg](x0) = x0 + 1,
      
      [hd](x0) = x0,
      
      [length](x0) = x0,
      
      [quot](x0, x1) = x0,
      
      [-](x0, x1) = x0,
      
      [sum](x0) = x0,
      
      [:](x0, x1) = x0 + x1 + 1,
      
      [++](x0, x1) = x0 + x1 + 1,
      
      [nil] = 0,
      
      [s](x0) = x0 + 1,
      
      [+](x0, x1) = x0 + x1 + 1,
      
      [0] = 0
     orientation:
      quot#(s(x),s(y)) = x + 1 >= x = quot#(-(x,y),s(y))
      
      +(0(),y) = y + 1 >= y = y
      
      +(s(x),y) = x + y + 2 >= x + y + 2 = s(+(x,y))
      
      ++(nil(),ys) = ys + 1 >= ys = ys
      
      ++(:(x,xs),ys) = x + xs + ys + 2 >= x + xs + ys + 2 = :(x,++(xs,ys))
      
      sum(:(x,nil())) = x + 1 >= x + 1 = :(x,nil())
      
      sum(:(x,:(y,xs))) = x + xs + y + 2 >= x + xs + y + 2 = sum(:(+(x,y),xs))
      
      sum(++(xs,:(x,:(y,ys)))) = x + xs + y + ys + 3 >= x + xs + y + ys + 3 = sum(++(xs,sum(:(x,:(y,ys)))))
      
      -(x,0()) = x >= x = x
      
      -(0(),s(y)) = 0 >= 0 = 0()
      
      -(s(x),s(y)) = x + 1 >= x = -(x,y)
      
      quot(0(),s(y)) = 0 >= 0 = 0()
      
      quot(s(x),s(y)) = x + 1 >= x + 1 = s(quot(-(x,y),s(y)))
      
      length(nil()) = 0 >= 0 = 0()
      
      length(:(x,xs)) = x + xs + 1 >= xs + 1 = s(length(xs))
      
      hd(:(x,xs)) = x + xs + 1 >= x = x
      
      avg(xs) = xs + 1 >= 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:
     -#(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))
    Subterm Criterion Processor:
     simple projection:
      pi(-#) = 1
     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))
    Subterm Criterion Processor:
     simple projection:
      pi(length#) = 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