(STRATEGY
    INNERMOST)

(VAR
    l l1 l2 l3 x y)
(DATATYPES
    A = µX.< true, false, 0, s(X), nil, cons(X, X) >)
(SIGNATURES
    if :: [A x A x A] -> A
    eq :: [A x A] -> A
    app :: [A x A] -> A
    mem :: [A x A] -> A
    ifmem :: [A x A x A] -> A
    inter :: [A x A] -> A
    ifinter :: [A x A x A x A] -> A)
(RULES
    if(true(),x,y) -> x
    if(false(),x,y) -> y
    eq(0(),0()) -> true()
    eq(0(),s(x)) -> false()
    eq(s(x),0()) -> false()
    eq(s(x),s(y)) -> eq(x,y)
    app(nil(),l) -> l
    app(cons(x,l1),l2) -> cons(x
                              ,app(l1,l2))
    app(app(l1,l2),l3) -> app(l1
                             ,app(l2,l3))
    mem(x,nil()) -> false()
    mem(x,cons(y,l)) -> ifmem(eq(x
                                ,y)
                             ,x
                             ,l)
    ifmem(true(),x,l) -> true()
    ifmem(false(),x,l) -> mem(x,l)
    inter(x,nil()) -> nil()
    inter(nil(),x) -> nil()
    inter(app(l1,l2),l3) ->
      app(inter(l1,l3),inter(l2,l3))
    inter(l1,app(l2,l3)) ->
      app(inter(l1,l2),inter(l1,l3))
    inter(cons(x,l1),l2) ->
      ifinter(mem(x,l2),x,l1,l2)
    inter(l1,cons(x,l2)) ->
      ifinter(mem(x,l1),x,l2,l1)
    ifinter(true(),x,l1,l2) ->
      cons(x,inter(l1,l2))
    ifinter(false(),x,l1,l2) ->
      inter(l1,l2))