MAYBE

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))
     Open
     
     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))
     Open
     
     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))
     Open
     
     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))
     Open
     
     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))
     Open
     
     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))
     Open
     
     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))
     Open