(GOAL COMPLEXITY) (STARTTERM CONSTRUCTOR-BASED) (STRATEGY INNERMOST) (STRATEGY INNERMOST) (VAR x y) (DATATYPES A = µX.< 0, s(X), zero, true, false >) (SIGNATURES minus :: [A x A] -> A quot :: [A x A] -> A plus :: [A x A] -> A id :: [A] -> A if :: [A x A x A] -> A not :: [A] -> A gt :: [A x A] -> A) (RULES minus(x,0()) -> x minus(s(x),s(y)) -> minus(x,y) quot(0(),s(y)) -> 0() quot(s(x),s(y)) -> s(quot(minus(x,y),s(y))) plus(s(x),s(y)) -> s(s(plus(if(gt(x,y),x,y) ,if(not(gt(x,y)),id(x),id(y))))) plus(s(x),x) -> plus(if(gt(x,x) ,id(x) ,id(x)) ,s(x)) plus(zero(),y) -> y plus(id(x),s(y)) -> s(plus(x ,if(gt(s(y),y),y,s(y)))) id(x) -> x if(true(),x,y) -> x if(false(),x,y) -> y not(x) -> if(x,false(),true()) gt(s(x),zero()) -> true() gt(zero(),y) -> false() gt(s(x),s(y)) -> gt(x,y))