(GOAL COMPLEXITY) (STARTTERM CONSTRUCTOR-BASED) (STRATEGY INNERMOST) (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())