(STRATEGY
    INNERMOST)

(VAR
    x xs y ys)
(DATATYPES
    A = µX.< 0, s(X), nil, :(X, X) >)
(SIGNATURES
    + :: [A x A] -> A
    ++ :: [A x A] -> A
    sum :: [A] -> A
    - :: [A x A] -> A
    quot :: [A x A] -> A
    length :: [A] -> A
    hd :: [A] -> A
    avg :: [A] -> A)
(RULES
    +(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)))