MAYBE
Time: 0.017310
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# ++(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# ++(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# :(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# ++(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)) -> +#(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))}
    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))}
     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))}
      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)}
          Open
         
         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)}
          Open
         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)}
          Open
         
         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)}
          Open
         
         
         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)}
          Open
         
         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)}
          Open
         
         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)}
          Open