(STRATEGY
    INNERMOST)

(VAR
    x x' xs y ys)
(DATATYPES
    A = µX.< Cons(X, X), Nil, False, True, S(X), 0 >)
(SIGNATURES
    overlap :: [A x A] -> A
    member :: [A x A] -> A
    notEmpty :: [A] -> A
    goal :: [A x A] -> A
    !EQ :: [A x A] -> A
    overlap[Ite][True][Ite] :: [A x A x A] -> A
    member[Ite][True][Ite] :: [A x A x A] -> A)
(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())