(GOAL COMPLEXITY) (STARTTERM CONSTRUCTOR-BASED) (STRATEGY INNERMOST) (STRATEGY INNERMOST) (VAR x y z) (DATATYPES A = µX.< 0, s(X) >) (SIGNATURES minus :: [A x A] -> A double :: [A] -> A plus :: [A x A] -> A) (RULES minus(x,0()) -> x minus(s(x),s(y)) -> minus(x,y) double(0()) -> 0() double(s(x)) -> s(s(double(x))) plus(0(),y) -> y plus(s(x),y) -> s(plus(x,y)) plus(s(x),y) -> plus(x,s(y)) plus(s(x),y) -> s(plus(minus(x ,y) ,double(y))) plus(s(plus(x,y)),z) -> s(plus(plus(x,y),z)))