(STARTTERM
    CONSTRUCTOR-BASED)
(STRATEGY
    INNERMOST)

(VAR
    @l @p @x @x_1 @x_2 @xs @xs' @y @y_1 @y_2)
(RULES
    #equal(@x,@y) -> #eq(@x,@y)
    *(@x,@y) -> #mult(@x,@y)
    -(@x,@y) -> #sub(@x,@y)
    div(@x,@y) -> #div(@x,@y)
    eratos(@l) -> eratos#1(@l)
    eratos#1(::(@x,@xs)) -> ::(@x,eratos(filter(@x,@xs)))
    eratos#1(nil()) -> nil()
    filter(@p,@l) -> filter#1(@l,@p)
    filter#1(::(@x,@xs),@p) -> filter#2(filter(@p,@xs),@p,@x)
    filter#1(nil(),@p) -> nil()
    filter#2(@xs',@p,@x) -> filter#3(#equal(mod(@x,@p),#0()),@x,@xs')
    filter#3(#false(),@x,@xs') -> ::(@x,@xs')
    filter#3(#true(),@x,@xs') -> @xs'
    mod(@x,@y) -> -(@x,*(@y,div(@x,@y)))
    #add(#0(),@y) ->= @y
    #add(#neg(#s(#0())),@y) ->= #pred(@y)
    #add(#neg(#s(#s(@x))),@y) ->= #pred(#add(#pos(#s(@x)),@y))
    #add(#pos(#s(#0())),@y) ->= #succ(@y)
    #add(#pos(#s(#s(@x))),@y) ->= #succ(#add(#pos(#s(@x)),@y))
    #and(#false(),#false()) ->= #false()
    #and(#false(),#true()) ->= #false()
    #and(#true(),#false()) ->= #false()
    #and(#true(),#true()) ->= #true()
    #div(#0(),#0()) ->= #divByZero()
    #div(#0(),#neg(@y)) ->= #0()
    #div(#0(),#pos(@y)) ->= #0()
    #div(#neg(@x),#0()) ->= #divByZero()
    #div(#neg(@x),#neg(@y)) ->= #positive(#natdiv(@x,@y))
    #div(#neg(@x),#pos(@y)) ->= #negative(#natdiv(@x,@y))
    #div(#pos(@x),#0()) ->= #divByZero()
    #div(#pos(@x),#neg(@y)) ->= #negative(#natdiv(@x,@y))
    #div(#pos(@x),#pos(@y)) ->= #positive(#natdiv(@x,@y))
    #divsub(#0(),#0()) ->= #0()
    #divsub(#0(),#s(@y)) ->= #underflow()
    #divsub(#s(@x),#0()) ->= #s(@x)
    #divsub(#s(@x),#s(@y)) ->= #divsub(@x,@y)
    #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()
    #mult(#0(),#0()) ->= #0()
    #mult(#0(),#neg(@y)) ->= #0()
    #mult(#0(),#pos(@y)) ->= #0()
    #mult(#neg(@x),#0()) ->= #0()
    #mult(#neg(@x),#neg(@y)) ->= #pos(#natmult(@x,@y))
    #mult(#neg(@x),#pos(@y)) ->= #neg(#natmult(@x,@y))
    #mult(#pos(@x),#0()) ->= #0()
    #mult(#pos(@x),#neg(@y)) ->= #neg(#natmult(@x,@y))
    #mult(#pos(@x),#pos(@y)) ->= #pos(#natmult(@x,@y))
    #natadd(#0(),@y) ->= @y
    #natadd(#s(@x),@y) ->= #s(#natadd(@x,@y))
    #natdiv(#0(),#0()) ->= #divByZero()
    #natdiv(#0(),#s(@y)) ->= #0()
    #natdiv(#s(@x),#0()) ->= #divByZero()
    #natdiv(#s(@x),#s(@y)) ->= #natdiv'(#divsub(@x,@y),#s(@y))
    #natdiv'(#0(),@y) ->= #s(#0())
    #natdiv'(#s(@x),@y) ->= #s(#natdiv(#s(@x),@y))
    #natdiv'(#underflow(),@y) ->= #0()
    #natmult(#0(),@y) ->= #0()
    #natmult(#s(@x),@y) ->= #natadd(@y,#natmult(@x,@y))
    #natsub(@x,#0()) ->= @x
    #natsub(#s(@x),#s(@y)) ->= #natsub(@x,@y)
    #negative(#0()) ->= #0()
    #negative(#neg(@x)) ->= #pos(@x)
    #negative(#pos(@x)) ->= #neg(@x)
    #negative(#s(@x)) ->= #neg(#s(@x))
    #positive(#0()) ->= #0()
    #positive(#neg(@x)) ->= #neg(@x)
    #positive(#pos(@x)) ->= #pos(@x)
    #positive(#s(@x)) ->= #pos(#s(@x))
    #pred(#0()) ->= #neg(#s(#0()))
    #pred(#neg(#s(@x))) ->= #neg(#s(#s(@x)))
    #pred(#pos(#s(#0()))) ->= #0()
    #pred(#pos(#s(#s(@x)))) ->= #pos(#s(@x))
    #sub(@x,#0()) ->= @x
    #sub(@x,#neg(@y)) ->= #add(@x,#pos(@y))
    #sub(@x,#pos(@y)) ->= #add(@x,#neg(@y))
    #succ(#0()) ->= #pos(#s(#0()))
    #succ(#neg(#s(#0()))) ->= #0()
    #succ(#neg(#s(#s(@x)))) ->= #neg(#s(@x))
    #succ(#pos(#s(@x))) ->= #pos(#s(#s(@x))))
(COMMENT
    This TRS was automatically generated from the resource aware ML program 'eratosthenes.raml', c.f. http://raml.tcs.ifi.lmu.de/)