(VAR x x' xs y ys ) (STRATEGY INNERMOST) (RULES overlap(Cons(x,xs),ys) -> overlap[Ite][True][Ite](member(x,ys),Cons(x,xs),ys) overlap(Nil,ys) -> False member(x',Cons(x,xs)) -> member[Ite][True][Ite](!EQ(x,x'),x',Cons(x,xs)) member(x,Nil) -> False notEmpty(Cons(x,xs)) -> True notEmpty(Nil) -> False goal(xs,ys) -> overlap(xs,ys) !EQ(S(x),S(y)) ->= !EQ(x,y) !EQ(0,S(y)) ->= False !EQ(S(x),0) ->= False !EQ(0,0) ->= True overlap[Ite][True][Ite](False,Cons(x,xs),ys) ->= overlap(xs,ys) member[Ite][True][Ite](False,x',Cons(x,xs)) ->= member(x',xs) overlap[Ite][True][Ite](True,xs,ys) ->= True member[Ite][True][Ite](True,x,xs) ->= True )