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