(GOAL COMPLEXITY) (STARTTERM CONSTRUCTOR-BASED) (STRATEGY INNERMOST) (STRATEGY INNERMOST) (VAR x y z) (DATATYPES A = µX.< true, 0, false, s(X) >) (SIGNATURES cond1 :: [A x A x A x A] -> A cond2 :: [A x A x A x A] -> A cond3 :: [A x A x A x A] -> A gr :: [A x A] -> A add :: [A x A] -> A p :: [A] -> A) (RULES cond1(true(),x,y,z) -> cond2(gr(x,0()),x,y,z) cond2(true(),x,y,z) -> cond1(gr(add(x,y),z),p(x),y,z) cond2(false(),x,y,z) -> cond3(gr(y,0()),x,y,z) cond3(true(),x,y,z) -> cond1(gr(add(x,y),z),x,p(y),z) cond3(false(),x,y,z) -> cond1(gr(add(x,y),z),x,y,z) gr(0(),x) -> false() gr(s(x),0()) -> true() gr(s(x),s(y)) -> gr(x,y) add(0(),x) -> x add(s(x),y) -> s(add(x,y)) p(0()) -> 0() p(s(x)) -> x)