(GOAL COMPLEXITY) (STARTTERM CONSTRUCTORBASED) (VAR x y ) (STRATEGY INNERMOST) (RULES +(0, y) -> y +(s(x), y) -> s(+(x, y)) +(s(x), y) -> +(x, s(y)) )