(COMMENT sum([x1,..,xn]) computes x1 + + xn problems: - plus terminates by bounded increase - sum uses destructors and plus inside recursive call - not confluent ) (VAR x y z xs) (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 )