(STARTTERM
    CONSTRUCTOR-BASED)
(STRATEGY
    INNERMOST)

(VAR
    @l @l1 @l2 @x @x_1 @x_2 @xs @y @y_1 @y_2 @ys)
(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())
(COMMENT
    This TRS was automatically generated from the resource aware ML program 'duplicates.raml', c.f. http://raml.tcs.ifi.lmu.de/)