YES
Time: 0.633266
TRS:
 {                 +(0(), y) -> y,
                   +(s x, y) -> s +(x, y),
               ++(nil(), ys) -> ys,
            ++(:(x, xs), ys) -> :(x, ++(xs, ys)),
  sum ++(xs, :(x, :(y, ys))) -> sum ++(xs, sum :(x, :(y, ys))),
             sum :(x, nil()) -> :(x, nil()),
          sum :(x, :(y, xs)) -> sum :(+(x, y), xs),
                   -(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)}
 DP:
  DP:
   {                 +#(s x, y) -> +#(x, y),
              ++#(:(x, xs), ys) -> ++#(xs, 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# :(x, :(y, xs)) -> +#(x, y),
            sum# :(x, :(y, xs)) -> sum# :(+(x, y), xs),
                   -#(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 -> sum# xs,
                        avg# xs -> quot#(hd sum xs, length xs),
                        avg# xs -> length# xs,
                        avg# xs -> hd# sum xs}
  TRS:
  {                 +(0(), y) -> y,
                    +(s x, y) -> s +(x, y),
                ++(nil(), ys) -> ys,
             ++(:(x, xs), ys) -> :(x, ++(xs, ys)),
   sum ++(xs, :(x, :(y, ys))) -> sum ++(xs, sum :(x, :(y, ys))),
              sum :(x, nil()) -> :(x, nil()),
           sum :(x, :(y, xs)) -> sum :(+(x, y), xs),
                    -(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)}
  UR:
   {                 +(0(), y) -> y,
                     +(s x, y) -> s +(x, y),
                 ++(nil(), ys) -> ys,
              ++(:(x, xs), ys) -> :(x, ++(xs, ys)),
    sum ++(xs, :(x, :(y, ys))) -> sum ++(xs, sum :(x, :(y, ys))),
               sum :(x, nil()) -> :(x, nil()),
            sum :(x, :(y, xs)) -> sum :(+(x, y), xs),
                     -(x, 0()) -> x,
                   -(0(), s y) -> 0(),
                   -(s x, s y) -> -(x, y),
                  length nil() -> 0(),
               length :(x, xs) -> s length xs,
                   hd :(x, xs) -> x,
                       a(z, w) -> z,
                       a(z, w) -> w}
   EDG:
    {(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))
     (+#(s x, y) -> +#(x, y), +#(s x, y) -> +#(x, y))
     (-#(s x, s y) -> -#(x, y), -#(s x, s y) -> -#(x, y))
     (length# :(x, xs) -> length# xs, length# :(x, xs) -> length# xs)
     (avg# xs -> length# xs, length# :(x, xs) -> length# xs)
     (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# :(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# ++(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))) -> 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)) -> +#(x, y))
     (sum# ++(xs, :(x, :(y, ys))) -> sum# ++(xs, sum :(x, :(y, ys))), sum# :(x, :(y, xs)) -> sum# :(+(x, y), xs))
     (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))))
     (avg# xs -> sum# xs, sum# ++(xs, :(x, :(y, ys))) -> sum# :(x, :(y, ys)))
     (avg# xs -> sum# xs, sum# :(x, :(y, xs)) -> +#(x, y))
     (avg# xs -> sum# xs, sum# :(x, :(y, xs)) -> sum# :(+(x, y), xs))
     (quot#(s x, s y) -> -#(x, y), -#(s x, s y) -> -#(x, y))
     (sum# :(x, :(y, xs)) -> +#(x, y), +#(s x, y) -> +#(x, y))
     (++#(:(x, xs), ys) -> ++#(xs, ys), ++#(:(x, xs), ys) -> ++#(xs, ys))
     (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))
     (sum# ++(xs, :(x, :(y, ys))) -> ++#(xs, sum :(x, :(y, ys))), ++#(:(x, xs), ys) -> ++#(xs, ys))}
    STATUS:
     arrows: 0.884444
     SCCS (7):
      Scc:
       {sum# ++(xs, :(x, :(y, ys))) -> sum# ++(xs, sum :(x, :(y, ys)))}
      Scc:
       {sum# :(x, :(y, xs)) -> sum# :(+(x, y), xs)}
      Scc:
       {length# :(x, xs) -> length# xs}
      Scc:
       {+#(s x, y) -> +#(x, y)}
      Scc:
       {quot#(s x, s y) -> quot#(-(x, y), s y)}
      Scc:
       {-#(s x, s y) -> -#(x, y)}
      Scc:
       {++#(:(x, xs), ys) -> ++#(xs, ys)}
      
      
      
      SCC (1):
       Strict:
        {sum# ++(xs, :(x, :(y, ys))) -> sum# ++(xs, sum :(x, :(y, ys)))}
       Weak:
       {                 +(0(), y) -> y,
                         +(s x, y) -> s +(x, y),
                     ++(nil(), ys) -> ys,
                  ++(:(x, xs), ys) -> :(x, ++(xs, ys)),
        sum ++(xs, :(x, :(y, ys))) -> sum ++(xs, sum :(x, :(y, ys))),
                   sum :(x, nil()) -> :(x, nil()),
                sum :(x, :(y, xs)) -> sum :(+(x, y), xs),
                         -(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)}
       POLY:
        Mode: weak, max_in=1, output_bits=-1, dnum=1, ur=true
        Interpretation:
         [+](x0, x1) = x0 + 1,
         
         [++](x0, x1) = x0 + x1 + 1,
         
         [:](x0, x1) = x0 + 1,
         
         [-](x0, x1) = x0 + 1,
         
         [quot](x0, x1) = x0 + 1,
         
         [s](x0) = x0 + 1,
         
         [sum](x0) = 1,
         
         [length](x0) = 0,
         
         [hd](x0) = 0,
         
         [avg](x0) = 0,
         
         [0] = 1,
         
         [nil] = 0,
         
         [sum#](x0) = x0
        Strict:
         sum# ++(xs, :(x, :(y, ys))) -> sum# ++(xs, sum :(x, :(y, ys)))
         3 + 0y + 0x + 1ys + 1xs >= 2 + 0y + 0x + 0ys + 1xs
        Weak:
         avg xs -> quot(hd sum xs, length xs)
         0 + 0xs >= 1 + 0xs
         hd :(x, xs) -> x
         0 + 0x + 0xs >= 1x
         length :(x, xs) -> s length xs
         0 + 0x + 0xs >= 1 + 0xs
         length nil() -> 0()
         0 >= 1
         quot(s x, s y) -> s quot(-(x, y), s y)
         2 + 1y + 0x >= 3 + 1y + 0x
         quot(0(), s y) -> 0()
         2 + 1y >= 1
         -(s x, s y) -> -(x, y)
         2 + 1y + 0x >= 1 + 1y + 0x
         -(0(), s y) -> 0()
         2 + 1y >= 1
         -(x, 0()) -> x
         2 + 0x >= 1x
         sum :(x, :(y, xs)) -> sum :(+(x, y), xs)
         1 + 0y + 0x + 0xs >= 1 + 0y + 0x + 0xs
         sum :(x, nil()) -> :(x, nil())
         1 + 0x >= 1 + 0x
         sum ++(xs, :(x, :(y, ys))) -> sum ++(xs, sum :(x, :(y, ys)))
         1 + 0y + 0x + 0ys + 0xs >= 1 + 0y + 0x + 0ys + 0xs
         ++(:(x, xs), ys) -> :(x, ++(xs, ys))
         2 + 0x + 1ys + 1xs >= 2 + 0x + 1ys + 1xs
         ++(nil(), ys) -> ys
         1 + 1ys >= 1ys
         +(s x, y) -> s +(x, y)
         2 + 0y + 1x >= 2 + 0y + 1x
         +(0(), y) -> y
         2 + 0y >= 1y
       Qed
     
     SCC (1):
      Strict:
       {sum# :(x, :(y, xs)) -> sum# :(+(x, y), xs)}
      Weak:
      {                 +(0(), y) -> y,
                        +(s x, y) -> s +(x, y),
                    ++(nil(), ys) -> ys,
                 ++(:(x, xs), ys) -> :(x, ++(xs, ys)),
       sum ++(xs, :(x, :(y, ys))) -> sum ++(xs, sum :(x, :(y, ys))),
                  sum :(x, nil()) -> :(x, nil()),
               sum :(x, :(y, xs)) -> sum :(+(x, y), xs),
                        -(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)}
      POLY:
       Mode: weak, max_in=1, output_bits=-1, dnum=1, ur=true
       Interpretation:
        [+](x0, x1) = x0 + 1,
        
        [++](x0, x1) = x0 + 1,
        
        [:](x0, x1) = x0 + 1,
        
        [-](x0, x1) = x0 + 1,
        
        [quot](x0, x1) = x0 + 1,
        
        [s](x0) = x0 + 1,
        
        [sum](x0) = 0,
        
        [length](x0) = 0,
        
        [hd](x0) = 0,
        
        [avg](x0) = 0,
        
        [0] = 1,
        
        [nil] = 1,
        
        [sum#](x0) = x0
       Strict:
        sum# :(x, :(y, xs)) -> sum# :(+(x, y), xs)
        2 + 0y + 0x + 1xs >= 1 + 0y + 0x + 1xs
       Weak:
        avg xs -> quot(hd sum xs, length xs)
        0 + 0xs >= 1 + 0xs
        hd :(x, xs) -> x
        0 + 0x + 0xs >= 1x
        length :(x, xs) -> s length xs
        0 + 0x + 0xs >= 1 + 0xs
        length nil() -> 0()
        0 >= 1
        quot(s x, s y) -> s quot(-(x, y), s y)
        2 + 1y + 0x >= 3 + 1y + 0x
        quot(0(), s y) -> 0()
        2 + 1y >= 1
        -(s x, s y) -> -(x, y)
        2 + 1y + 0x >= 1 + 1y + 0x
        -(0(), s y) -> 0()
        2 + 1y >= 1
        -(x, 0()) -> x
        2 + 0x >= 1x
        sum :(x, :(y, xs)) -> sum :(+(x, y), xs)
        0 + 0y + 0x + 0xs >= 0 + 0y + 0x + 0xs
        sum :(x, nil()) -> :(x, nil())
        0 + 0x >= 2 + 0x
        sum ++(xs, :(x, :(y, ys))) -> sum ++(xs, sum :(x, :(y, ys)))
        0 + 0y + 0x + 0ys + 0xs >= 0 + 0y + 0x + 0ys + 0xs
        ++(:(x, xs), ys) -> :(x, ++(xs, ys))
        2 + 0x + 0ys + 1xs >= 2 + 0x + 0ys + 1xs
        ++(nil(), ys) -> ys
        2 + 0ys >= 1ys
        +(s x, y) -> s +(x, y)
        2 + 0y + 1x >= 2 + 0y + 1x
        +(0(), y) -> y
        2 + 0y >= 1y
      Qed
     SCC (1):
      Strict:
       {length# :(x, xs) -> length# xs}
      Weak:
      {                 +(0(), y) -> y,
                        +(s x, y) -> s +(x, y),
                    ++(nil(), ys) -> ys,
                 ++(:(x, xs), ys) -> :(x, ++(xs, ys)),
       sum ++(xs, :(x, :(y, ys))) -> sum ++(xs, sum :(x, :(y, ys))),
                  sum :(x, nil()) -> :(x, nil()),
               sum :(x, :(y, xs)) -> sum :(+(x, y), xs),
                        -(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)}
      POLY:
       Mode: weak, max_in=1, output_bits=-1, dnum=1, ur=true
       Interpretation:
        [+](x0, x1) = x0 + 1,
        
        [++](x0, x1) = x0 + 1,
        
        [:](x0, x1) = x0 + 1,
        
        [-](x0, x1) = x0 + 1,
        
        [quot](x0, x1) = x0 + x1,
        
        [s](x0) = x0 + 1,
        
        [sum](x0) = 0,
        
        [length](x0) = 0,
        
        [hd](x0) = x0 + 1,
        
        [avg](x0) = 0,
        
        [0] = 1,
        
        [nil] = 1,
        
        [length#](x0) = x0 + 1
       Strict:
        length# :(x, xs) -> length# xs
        2 + 0x + 1xs >= 1 + 1xs
       Weak:
        avg xs -> quot(hd sum xs, length xs)
        0 + 0xs >= 1 + 0xs
        hd :(x, xs) -> x
        2 + 0x + 1xs >= 1x
        length :(x, xs) -> s length xs
        0 + 0x + 0xs >= 1 + 0xs
        length nil() -> 0()
        0 >= 1
        quot(s x, s y) -> s quot(-(x, y), s y)
        2 + 1y + 1x >= 3 + 2y + 0x
        quot(0(), s y) -> 0()
        2 + 1y >= 1
        -(s x, s y) -> -(x, y)
        2 + 1y + 0x >= 1 + 1y + 0x
        -(0(), s y) -> 0()
        2 + 1y >= 1
        -(x, 0()) -> x
        2 + 0x >= 1x
        sum :(x, :(y, xs)) -> sum :(+(x, y), xs)
        0 + 0y + 0x + 0xs >= 0 + 0y + 0x + 0xs
        sum :(x, nil()) -> :(x, nil())
        0 + 0x >= 2 + 0x
        sum ++(xs, :(x, :(y, ys))) -> sum ++(xs, sum :(x, :(y, ys)))
        0 + 0y + 0x + 0ys + 0xs >= 0 + 0y + 0x + 0ys + 0xs
        ++(:(x, xs), ys) -> :(x, ++(xs, ys))
        2 + 0x + 0ys + 1xs >= 2 + 0x + 0ys + 1xs
        ++(nil(), ys) -> ys
        2 + 0ys >= 1ys
        +(s x, y) -> s +(x, y)
        2 + 0y + 1x >= 2 + 0y + 1x
        +(0(), y) -> y
        2 + 0y >= 1y
      Qed
    
    SCC (1):
     Strict:
      {+#(s x, y) -> +#(x, y)}
     Weak:
     {                 +(0(), y) -> y,
                       +(s x, y) -> s +(x, y),
                   ++(nil(), ys) -> ys,
                ++(:(x, xs), ys) -> :(x, ++(xs, ys)),
      sum ++(xs, :(x, :(y, ys))) -> sum ++(xs, sum :(x, :(y, ys))),
                 sum :(x, nil()) -> :(x, nil()),
              sum :(x, :(y, xs)) -> sum :(+(x, y), xs),
                       -(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)}
     POLY:
      Mode: weak, max_in=1, output_bits=-1, dnum=1, ur=true
      Interpretation:
       [+](x0, x1) = x0 + 1,
       
       [++](x0, x1) = x0 + 1,
       
       [:](x0, x1) = x0 + 1,
       
       [-](x0, x1) = x0 + 1,
       
       [quot](x0, x1) = x0 + x1,
       
       [s](x0) = x0 + 1,
       
       [sum](x0) = 0,
       
       [length](x0) = 0,
       
       [hd](x0) = x0 + 1,
       
       [avg](x0) = 0,
       
       [0] = 1,
       
       [nil] = 1,
       
       [+#](x0, x1) = x0 + 1
      Strict:
       +#(s x, y) -> +#(x, y)
       2 + 0y + 1x >= 1 + 0y + 1x
      Weak:
       avg xs -> quot(hd sum xs, length xs)
       0 + 0xs >= 1 + 0xs
       hd :(x, xs) -> x
       2 + 0x + 1xs >= 1x
       length :(x, xs) -> s length xs
       0 + 0x + 0xs >= 1 + 0xs
       length nil() -> 0()
       0 >= 1
       quot(s x, s y) -> s quot(-(x, y), s y)
       2 + 1y + 1x >= 3 + 2y + 0x
       quot(0(), s y) -> 0()
       2 + 1y >= 1
       -(s x, s y) -> -(x, y)
       2 + 1y + 0x >= 1 + 1y + 0x
       -(0(), s y) -> 0()
       2 + 1y >= 1
       -(x, 0()) -> x
       2 + 0x >= 1x
       sum :(x, :(y, xs)) -> sum :(+(x, y), xs)
       0 + 0y + 0x + 0xs >= 0 + 0y + 0x + 0xs
       sum :(x, nil()) -> :(x, nil())
       0 + 0x >= 2 + 0x
       sum ++(xs, :(x, :(y, ys))) -> sum ++(xs, sum :(x, :(y, ys)))
       0 + 0y + 0x + 0ys + 0xs >= 0 + 0y + 0x + 0ys + 0xs
       ++(:(x, xs), ys) -> :(x, ++(xs, ys))
       2 + 0x + 0ys + 1xs >= 2 + 0x + 0ys + 1xs
       ++(nil(), ys) -> ys
       2 + 0ys >= 1ys
       +(s x, y) -> s +(x, y)
       2 + 0y + 1x >= 2 + 0y + 1x
       +(0(), y) -> y
       2 + 0y >= 1y
     Qed
    
    
    SCC (1):
     Strict:
      {quot#(s x, s y) -> quot#(-(x, y), s y)}
     Weak:
     {                 +(0(), y) -> y,
                       +(s x, y) -> s +(x, y),
                   ++(nil(), ys) -> ys,
                ++(:(x, xs), ys) -> :(x, ++(xs, ys)),
      sum ++(xs, :(x, :(y, ys))) -> sum ++(xs, sum :(x, :(y, ys))),
                 sum :(x, nil()) -> :(x, nil()),
              sum :(x, :(y, xs)) -> sum :(+(x, y), xs),
                       -(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)}
     POLY:
      Mode: weak, max_in=1, output_bits=-1, dnum=1, ur=true
      Interpretation:
       [+](x0, x1) = x0 + 1,
       
       [++](x0, x1) = x0 + 1,
       
       [:](x0, x1) = x0 + 1,
       
       [-](x0, x1) = x0,
       
       [quot](x0, x1) = x0 + 1,
       
       [s](x0) = x0 + 1,
       
       [sum](x0) = 0,
       
       [length](x0) = x0 + 1,
       
       [hd](x0) = 0,
       
       [avg](x0) = 0,
       
       [0] = 1,
       
       [nil] = 1,
       
       [quot#](x0, x1) = x0 + 1
      Strict:
       quot#(s x, s y) -> quot#(-(x, y), s y)
       2 + 0y + 1x >= 1 + 0y + 1x
      Weak:
       avg xs -> quot(hd sum xs, length xs)
       0 + 0xs >= 2 + 1xs
       hd :(x, xs) -> x
       0 + 0x + 0xs >= 1x
       length :(x, xs) -> s length xs
       2 + 0x + 1xs >= 2 + 1xs
       length nil() -> 0()
       2 >= 1
       quot(s x, s y) -> s quot(-(x, y), s y)
       2 + 1y + 0x >= 3 + 1y + 0x
       quot(0(), s y) -> 0()
       2 + 1y >= 1
       -(s x, s y) -> -(x, y)
       1 + 0y + 1x >= 0 + 0y + 1x
       -(0(), s y) -> 0()
       1 + 0y >= 1
       -(x, 0()) -> x
       0 + 1x >= 1x
       sum :(x, :(y, xs)) -> sum :(+(x, y), xs)
       0 + 0y + 0x + 0xs >= 0 + 0y + 0x + 0xs
       sum :(x, nil()) -> :(x, nil())
       0 + 0x >= 2 + 0x
       sum ++(xs, :(x, :(y, ys))) -> sum ++(xs, sum :(x, :(y, ys)))
       0 + 0y + 0x + 0ys + 0xs >= 0 + 0y + 0x + 0ys + 0xs
       ++(:(x, xs), ys) -> :(x, ++(xs, ys))
       2 + 0x + 0ys + 1xs >= 2 + 0x + 0ys + 1xs
       ++(nil(), ys) -> ys
       2 + 0ys >= 1ys
       +(s x, y) -> s +(x, y)
       2 + 0y + 1x >= 2 + 0y + 1x
       +(0(), y) -> y
       2 + 0y >= 1y
     Qed
   
   SCC (1):
    Strict:
     {-#(s x, s y) -> -#(x, y)}
    Weak:
    {                 +(0(), y) -> y,
                      +(s x, y) -> s +(x, y),
                  ++(nil(), ys) -> ys,
               ++(:(x, xs), ys) -> :(x, ++(xs, ys)),
     sum ++(xs, :(x, :(y, ys))) -> sum ++(xs, sum :(x, :(y, ys))),
                sum :(x, nil()) -> :(x, nil()),
             sum :(x, :(y, xs)) -> sum :(+(x, y), xs),
                      -(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)}
    POLY:
     Mode: weak, max_in=1, output_bits=-1, dnum=1, ur=true
     Interpretation:
      [+](x0, x1) = x0 + 1,
      
      [++](x0, x1) = x0 + 1,
      
      [:](x0, x1) = x0 + 1,
      
      [-](x0, x1) = x0 + 1,
      
      [quot](x0, x1) = x0 + 1,
      
      [s](x0) = x0 + 1,
      
      [sum](x0) = 0,
      
      [length](x0) = x0 + 1,
      
      [hd](x0) = x0 + 1,
      
      [avg](x0) = 0,
      
      [0] = 1,
      
      [nil] = 1,
      
      [-#](x0, x1) = x0 + 1
     Strict:
      -#(s x, s y) -> -#(x, y)
      2 + 0y + 1x >= 1 + 0y + 1x
     Weak:
      avg xs -> quot(hd sum xs, length xs)
      0 + 0xs >= 2 + 1xs
      hd :(x, xs) -> x
      2 + 0x + 1xs >= 1x
      length :(x, xs) -> s length xs
      2 + 0x + 1xs >= 2 + 1xs
      length nil() -> 0()
      2 >= 1
      quot(s x, s y) -> s quot(-(x, y), s y)
      2 + 1y + 0x >= 3 + 1y + 0x
      quot(0(), s y) -> 0()
      2 + 1y >= 1
      -(s x, s y) -> -(x, y)
      2 + 1y + 0x >= 1 + 1y + 0x
      -(0(), s y) -> 0()
      2 + 1y >= 1
      -(x, 0()) -> x
      2 + 0x >= 1x
      sum :(x, :(y, xs)) -> sum :(+(x, y), xs)
      0 + 0y + 0x + 0xs >= 0 + 0y + 0x + 0xs
      sum :(x, nil()) -> :(x, nil())
      0 + 0x >= 2 + 0x
      sum ++(xs, :(x, :(y, ys))) -> sum ++(xs, sum :(x, :(y, ys)))
      0 + 0y + 0x + 0ys + 0xs >= 0 + 0y + 0x + 0ys + 0xs
      ++(:(x, xs), ys) -> :(x, ++(xs, ys))
      2 + 0x + 0ys + 1xs >= 2 + 0x + 0ys + 1xs
      ++(nil(), ys) -> ys
      2 + 0ys >= 1ys
      +(s x, y) -> s +(x, y)
      2 + 0y + 1x >= 2 + 0y + 1x
      +(0(), y) -> y
      2 + 0y >= 1y
    Qed
   
   SCC (1):
    Strict:
     {++#(:(x, xs), ys) -> ++#(xs, ys)}
    Weak:
    {                 +(0(), y) -> y,
                      +(s x, y) -> s +(x, y),
                  ++(nil(), ys) -> ys,
               ++(:(x, xs), ys) -> :(x, ++(xs, ys)),
     sum ++(xs, :(x, :(y, ys))) -> sum ++(xs, sum :(x, :(y, ys))),
                sum :(x, nil()) -> :(x, nil()),
             sum :(x, :(y, xs)) -> sum :(+(x, y), xs),
                      -(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)}
    POLY:
     Mode: weak, max_in=1, output_bits=-1, dnum=1, ur=true
     Interpretation:
      [+](x0, x1) = x0 + 1,
      
      [++](x0, x1) = x0 + 1,
      
      [:](x0, x1) = x0 + 1,
      
      [-](x0, x1) = x0 + 1,
      
      [quot](x0, x1) = x0 + x1,
      
      [s](x0) = x0 + 1,
      
      [sum](x0) = 0,
      
      [length](x0) = 0,
      
      [hd](x0) = x0 + 1,
      
      [avg](x0) = 0,
      
      [0] = 1,
      
      [nil] = 1,
      
      [++#](x0, x1) = x0 + 1
     Strict:
      ++#(:(x, xs), ys) -> ++#(xs, ys)
      2 + 0x + 0ys + 1xs >= 1 + 0ys + 1xs
     Weak:
      avg xs -> quot(hd sum xs, length xs)
      0 + 0xs >= 1 + 0xs
      hd :(x, xs) -> x
      2 + 0x + 1xs >= 1x
      length :(x, xs) -> s length xs
      0 + 0x + 0xs >= 1 + 0xs
      length nil() -> 0()
      0 >= 1
      quot(s x, s y) -> s quot(-(x, y), s y)
      2 + 1y + 1x >= 3 + 2y + 0x
      quot(0(), s y) -> 0()
      2 + 1y >= 1
      -(s x, s y) -> -(x, y)
      2 + 1y + 0x >= 1 + 1y + 0x
      -(0(), s y) -> 0()
      2 + 1y >= 1
      -(x, 0()) -> x
      2 + 0x >= 1x
      sum :(x, :(y, xs)) -> sum :(+(x, y), xs)
      0 + 0y + 0x + 0xs >= 0 + 0y + 0x + 0xs
      sum :(x, nil()) -> :(x, nil())
      0 + 0x >= 2 + 0x
      sum ++(xs, :(x, :(y, ys))) -> sum ++(xs, sum :(x, :(y, ys)))
      0 + 0y + 0x + 0ys + 0xs >= 0 + 0y + 0x + 0ys + 0xs
      ++(:(x, xs), ys) -> :(x, ++(xs, ys))
      2 + 0x + 0ys + 1xs >= 2 + 0x + 0ys + 1xs
      ++(nil(), ys) -> ys
      2 + 0ys >= 1ys
      +(s x, y) -> s +(x, y)
      2 + 0y + 1x >= 2 + 0y + 1x
      +(0(), y) -> y
      2 + 0y >= 1y
    Qed