(STRATEGY
    INNERMOST)

(VAR
    @l @l1 @l2 @x @x_1 @x_2 @xs @y
    @y_1 @y_2 @ys)
(DATATYPES
    A = µX.< ::(X, X), nil, #false, #true, #0, #neg(X), #pos(X), #s(X) >)
(SIGNATURES
    #equal :: [A x A] -> A
    and :: [A x A] -> A
    eq :: [A x A] -> A
    eq#1 :: [A x A] -> A
    eq#2 :: [A] -> A
    eq#3 :: [A x A x A] -> A
    nub :: [A] -> A
    nub#1 :: [A] -> A
    remove :: [A x A] -> A
    remove#1 :: [A x A] -> A
    remove#2 :: [A x A x A x A] -> A
    #and :: [A x A] -> A
    #eq :: [A x A] -> A)
(RULES
    #equal(@x,@y) -> #eq(@x,@y)
    and(@x,@y) -> #and(@x,@y)
    eq(@l1,@l2) -> eq#1(@l1,@l2)
    eq#1(::(@x,@xs),@l2) -> eq#3(@l2
                                ,@x
                                ,@xs)
    eq#1(nil(),@l2) -> eq#2(@l2)
    eq#2(::(@y,@ys)) -> #false()
    eq#2(nil()) -> #true()
    eq#3(::(@y,@ys),@x,@xs) ->
      and(#equal(@x,@y),eq(@xs,@ys))
    eq#3(nil(),@x,@xs) -> #false()
    nub(@l) -> nub#1(@l)
    nub#1(::(@x,@xs)) -> ::(@x
                           ,nub(remove(@x,@xs)))
    nub#1(nil()) -> nil()
    remove(@x,@l) -> remove#1(@l,@x)
    remove#1(::(@y,@ys),@x) ->
      remove#2(eq(@x,@y),@x,@y,@ys)
    remove#1(nil(),@x) -> nil()
    remove#2(#false(),@x,@y,@ys) ->
      ::(@y,remove(@x,@ys))
    remove#2(#true(),@x,@y,@ys) ->
      remove(@x,@ys)
    #and(#false(),#false()) ->=
      #false()
    #and(#false(),#true()) ->=
      #false()
    #and(#true(),#false()) ->=
      #false()
    #and(#true(),#true()) ->=
      #true()
    #eq(#0(),#0()) ->= #true()
    #eq(#0(),#neg(@y)) ->= #false()
    #eq(#0(),#pos(@y)) ->= #false()
    #eq(#0(),#s(@y)) ->= #false()
    #eq(#neg(@x),#0()) ->= #false()
    #eq(#neg(@x),#neg(@y)) ->=
      #eq(@x,@y)
    #eq(#neg(@x),#pos(@y)) ->=
      #false()
    #eq(#pos(@x),#0()) ->= #false()
    #eq(#pos(@x),#neg(@y)) ->=
      #false()
    #eq(#pos(@x),#pos(@y)) ->=
      #eq(@x,@y)
    #eq(#s(@x),#0()) ->= #false()
    #eq(#s(@x),#s(@y)) ->= #eq(@x
                              ,@y)
    #eq(::(@x_1,@x_2)
       ,::(@y_1,@y_2)) ->=
      #and(#eq(@x_1,@y_1)
          ,#eq(@x_2,@y_2))
    #eq(::(@x_1,@x_2),nil()) ->=
      #false()
    #eq(nil(),::(@y_1,@y_2)) ->=
      #false()
    #eq(nil(),nil()) ->= #true())