(STRATEGY
    INNERMOST)

(VAR
    x xs y z)
(DATATYPES
    A = µX.< 0, true, false, s(X), nil, cons(X, X), error, b, c >)
(SIGNATURES
    plus :: [A x A] -> A
    plusIter :: [A x A x A] -> A
    ifPlus :: [A x A x A x A] -> A
    le :: [A x A] -> A
    sum :: [A] -> A
    sumIter :: [A x A] -> A
    ifSum :: [A x A x A x A] -> A
    isempty :: [A] -> A
    head :: [A] -> A
    tail :: [A] -> A
    a :: [] -> A)
(RULES
    plus(x,y) -> plusIter(x,y,0())
    plusIter(x,y,z) -> ifPlus(le(x
                                ,z)
                             ,x
                             ,y
                             ,z)
    ifPlus(true(),x,y,z) -> y
    ifPlus(false(),x,y,z) ->
      plusIter(x,s(y),s(z))
    le(s(x),0()) -> false()
    le(0(),y) -> true()
    le(s(x),s(y)) -> le(x,y)
    sum(xs) -> sumIter(xs,0())
    sumIter(xs,x) ->
      ifSum(isempty(xs)
           ,xs
           ,x
           ,plus(x,head(xs)))
    ifSum(true(),xs,x,y) -> x
    ifSum(false(),xs,x,y) ->
      sumIter(tail(xs),y)
    isempty(nil()) -> true()
    isempty(cons(x,xs)) -> false()
    head(nil()) -> error()
    head(cons(x,xs)) -> x
    tail(nil()) -> nil()
    tail(cons(x,xs)) -> xs
    a() -> b()
    a() -> c())