(GOAL COMPLEXITY) (STARTTERM CONSTRUCTOR-BASED) (STRATEGY INNERMOST) (STRATEGY INNERMOST) (VAR h i u v x y) (DATATYPES A = µX.< 0, true, s(X), false, empty, edge(X, X, X) >) (SIGNATURES eq :: [A x A] -> A or :: [A x A] -> A union :: [A x A] -> A reach :: [A x A x A x A] -> A if_reach_1 :: [A x A x A x A x A] -> A if_reach_2 :: [A x A x A x A x A] -> A) (RULES eq(0(),0()) -> true() eq(0(),s(x)) -> false() eq(s(x),0()) -> false() eq(s(x),s(y)) -> eq(x,y) or(true(),y) -> true() or(false(),y) -> y union(empty(),h) -> h union(edge(x,y,i),h) -> edge(x ,y ,union(i,h)) reach(x,y,empty(),h) -> false() reach(x,y,edge(u,v,i),h) -> if_reach_1(eq(x,u) ,x ,y ,edge(u,v,i) ,h) if_reach_1(true() ,x ,y ,edge(u,v,i) ,h) -> if_reach_2(eq(y,v) ,x ,y ,edge(u,v,i) ,h) if_reach_2(true() ,x ,y ,edge(u,v,i) ,h) -> true() if_reach_2(false() ,x ,y ,edge(u,v,i) ,h) -> or(reach(x,y,i,h) ,reach(v,y,union(i,h),empty())) if_reach_1(false() ,x ,y ,edge(u,v,i) ,h) -> reach(x,y,i,edge(u,v,h)))