R

     ↳Dependency Pair Analysis

+'(s(x), y) -> +'(x, y)
++'(:(x, xs), ys) -> ++'(xs, ys)
SUM(:(x, :(y, xs))) -> SUM(:(+(x, y), xs))
SUM(:(x, :(y, xs))) -> +'(x, y)
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(:(x, :(y, ys)))
-'(s(x), s(y)) -> -'(x, y)
QUOT(s(x), s(y)) -> QUOT(-(x, y), s(y))
QUOT(s(x), s(y)) -> -'(x, y)
LENGTH(:(x, xs)) -> LENGTH(xs)
AVG(xs) -> QUOT(hd(sum(xs)), length(xs))
AVG(xs) -> HD(sum(xs))
AVG(xs) -> SUM(xs)
AVG(xs) -> LENGTH(xs)

   R

     ↳DPs

       →DP Problem 1

         ↳Polynomial Ordering

       →DP Problem 2

         ↳Polo

       →DP Problem 3

         ↳Polo

       →DP Problem 4

         ↳Polo

       →DP Problem 5

         ↳Polo

       →DP Problem 6

         ↳Polo

       →DP Problem 7

         ↳Remaining

+'(s(x), y) -> +'(x, y)

+(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))

+'(s(x), y) -> +'(x, y)

+(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))

POL(:(x1, x2))	=  1 + x1 + x2
POL(sum(x1))	=  x1
POL(-(x1, x2))	=  x1
POL(avg(x1))	=  x1
POL(0)	=  0
POL(hd(x1))	=  x1
POL(++(x1, x2))	=  x1 + x2
POL(nil)	=  0
POL(quot(x1, x2))	=  x1
POL(s(x1))	=  1 + x1
POL(+(x1, x2))	=  x1 + x2
POL(length(x1))	=  x1
POL(+'(x1, x2))	=  1 + x1 + x2

   R

     ↳DPs

       →DP Problem 1

         ↳Polo

           →DP Problem 8

             ↳Dependency Graph

       →DP Problem 2

         ↳Polo

       →DP Problem 3

         ↳Polo

       →DP Problem 4

         ↳Polo

       →DP Problem 5

         ↳Polo

       →DP Problem 6

         ↳Polo

       →DP Problem 7

         ↳Remaining

+(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))

   R

     ↳DPs

       →DP Problem 1

         ↳Polo

       →DP Problem 2

         ↳Polynomial Ordering

       →DP Problem 3

         ↳Polo

       →DP Problem 4

         ↳Polo

       →DP Problem 5

         ↳Polo

       →DP Problem 6

         ↳Polo

       →DP Problem 7

         ↳Remaining

++'(:(x, xs), ys) -> ++'(xs, ys)

+(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))

++'(:(x, xs), ys) -> ++'(xs, ys)

+(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))

POL(:(x1, x2))	=  1 + x1 + x2
POL(++'(x1, x2))	=  1 + x1 + x2
POL(sum(x1))	=  x1
POL(-(x1, x2))	=  x1
POL(avg(x1))	=  0
POL(0)	=  0
POL(hd(x1))	=  x1
POL(++(x1, x2))	=  x1 + x2
POL(nil)	=  0
POL(quot(x1, x2))	=  0
POL(s(x1))	=  x1
POL(+(x1, x2))	=  x2
POL(length(x1))	=  0

   R

     ↳DPs

       →DP Problem 1

         ↳Polo

       →DP Problem 2

         ↳Polo

           →DP Problem 9

             ↳Dependency Graph

       →DP Problem 3

         ↳Polo

       →DP Problem 4

         ↳Polo

       →DP Problem 5

         ↳Polo

       →DP Problem 6

         ↳Polo

       →DP Problem 7

         ↳Remaining

+(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))

   R

     ↳DPs

       →DP Problem 1

         ↳Polo

       →DP Problem 2

         ↳Polo

       →DP Problem 3

         ↳Polynomial Ordering

       →DP Problem 4

         ↳Polo

       →DP Problem 5

         ↳Polo

       →DP Problem 6

         ↳Polo

       →DP Problem 7

         ↳Remaining

-'(s(x), s(y)) -> -'(x, y)

+(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))

-'(s(x), s(y)) -> -'(x, y)

+(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))

POL(:(x1, x2))	=  1 + x1 + x2
POL(sum(x1))	=  x1
POL(-(x1, x2))	=  x1
POL(avg(x1))	=  x1
POL(0)	=  0
POL(-'(x1, x2))	=  1 + x1
POL(hd(x1))	=  x1
POL(++(x1, x2))	=  x1 + x2
POL(nil)	=  0
POL(quot(x1, x2))	=  x1
POL(s(x1))	=  1 + x1
POL(+(x1, x2))	=  x1 + x2
POL(length(x1))	=  x1

   R

     ↳DPs

       →DP Problem 1

         ↳Polo

       →DP Problem 2

         ↳Polo

       →DP Problem 3

         ↳Polo

           →DP Problem 10

             ↳Dependency Graph

       →DP Problem 4

         ↳Polo

       →DP Problem 5

         ↳Polo

       →DP Problem 6

         ↳Polo

       →DP Problem 7

         ↳Remaining

+(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))

   R

     ↳DPs

       →DP Problem 1

         ↳Polo

       →DP Problem 2

         ↳Polo

       →DP Problem 3

         ↳Polo

       →DP Problem 4

         ↳Polynomial Ordering

       →DP Problem 5

         ↳Polo

       →DP Problem 6

         ↳Polo

       →DP Problem 7

         ↳Remaining

LENGTH(:(x, xs)) -> LENGTH(xs)

+(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))

LENGTH(:(x, xs)) -> LENGTH(xs)

+(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))

POL(:(x1, x2))	=  1 + x1 + x2
POL(sum(x1))	=  x1
POL(-(x1, x2))	=  x1
POL(avg(x1))	=  0
POL(0)	=  0
POL(hd(x1))	=  x1
POL(++(x1, x2))	=  x1 + x2
POL(nil)	=  0
POL(quot(x1, x2))	=  0
POL(s(x1))	=  x1
POL(+(x1, x2))	=  x2
POL(LENGTH(x1))	=  1 + x1
POL(length(x1))	=  0

   R

     ↳DPs

       →DP Problem 1

         ↳Polo

       →DP Problem 2

         ↳Polo

       →DP Problem 3

         ↳Polo

       →DP Problem 4

         ↳Polo

           →DP Problem 11

             ↳Dependency Graph

       →DP Problem 5

         ↳Polo

       →DP Problem 6

         ↳Polo

       →DP Problem 7

         ↳Remaining

+(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))

   R

     ↳DPs

       →DP Problem 1

         ↳Polo

       →DP Problem 2

         ↳Polo

       →DP Problem 3

         ↳Polo

       →DP Problem 4

         ↳Polo

       →DP Problem 5

         ↳Polynomial Ordering

       →DP Problem 6

         ↳Polo

       →DP Problem 7

         ↳Remaining

SUM(:(x, :(y, xs))) -> SUM(:(+(x, y), xs))

+(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))

SUM(:(x, :(y, xs))) -> SUM(:(+(x, y), xs))

+(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))

POL(:(x1, x2))	=  1 + x1 + x2
POL(sum(x1))	=  x1
POL(-(x1, x2))	=  x1
POL(avg(x1))	=  0
POL(0)	=  0
POL(SUM(x1))	=  1 + x1
POL(hd(x1))	=  x1
POL(++(x1, x2))	=  x1 + x2
POL(nil)	=  0
POL(quot(x1, x2))	=  0
POL(s(x1))	=  x1
POL(+(x1, x2))	=  x2
POL(length(x1))	=  0

   R

     ↳DPs

       →DP Problem 1

         ↳Polo

       →DP Problem 2

         ↳Polo

       →DP Problem 3

         ↳Polo

       →DP Problem 4

         ↳Polo

       →DP Problem 5

         ↳Polo

           →DP Problem 12

             ↳Dependency Graph

       →DP Problem 6

         ↳Polo

       →DP Problem 7

         ↳Remaining

+(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))

   R

     ↳DPs

       →DP Problem 1

         ↳Polo

       →DP Problem 2

         ↳Polo

       →DP Problem 3

         ↳Polo

       →DP Problem 4

         ↳Polo

       →DP Problem 5

         ↳Polo

       →DP Problem 6

         ↳Polynomial Ordering

       →DP Problem 7

         ↳Remaining

QUOT(s(x), s(y)) -> QUOT(-(x, y), s(y))

+(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))

QUOT(s(x), s(y)) -> QUOT(-(x, y), s(y))

+(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))

POL(:(x1, x2))	=  1 + x1 + x2
POL(sum(x1))	=  x1
POL(-(x1, x2))	=  x1
POL(avg(x1))	=  x1
POL(QUOT(x1, x2))	=  1 + x1 + x2
POL(0)	=  0
POL(hd(x1))	=  x1
POL(++(x1, x2))	=  x1 + x2
POL(nil)	=  0
POL(quot(x1, x2))	=  x1
POL(s(x1))	=  1 + x1
POL(+(x1, x2))	=  x1 + x2
POL(length(x1))	=  x1

   R

     ↳DPs

       →DP Problem 1

         ↳Polo

       →DP Problem 2

         ↳Polo

       →DP Problem 3

         ↳Polo

       →DP Problem 4

         ↳Polo

       →DP Problem 5

         ↳Polo

       →DP Problem 6

         ↳Polo

           →DP Problem 13

             ↳Dependency Graph

       →DP Problem 7

         ↳Remaining

+(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))

   R

     ↳DPs

       →DP Problem 1

         ↳Polo

       →DP Problem 2

         ↳Polo

       →DP Problem 3

         ↳Polo

       →DP Problem 4

         ↳Polo

       →DP Problem 5

         ↳Polo

       →DP Problem 6

         ↳Polo

       →DP Problem 7

         ↳Remaining Obligation(s)

SUM(++(xs, :(x, :(y, ys)))) -> SUM(++(xs, sum(:(x, :(y, ys)))))

+(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))