(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 p :: [A] -> A div :: [A x A] -> A plus :: [A x A] -> A) (RULES minus(x,0()) -> x minus(0(),y) -> 0() minus(s(x),s(y)) -> minus(p(s(x)),p(s(y))) minus(x,plus(y,z)) -> minus(minus(x,y),z) p(s(s(x))) -> s(p(s(x))) p(0()) -> s(s(0())) div(s(x),s(y)) -> s(div(minus(x ,y) ,s(y))) div(plus(x,y),z) -> plus(div(x ,z) ,div(y,z)) plus(0(),y) -> y plus(s(x),y) -> s(plus(y ,minus(s(x),s(0())))))