(VAR @l @p @x @x_1 @x_2 @xs @xs' @y @y_1 @y_2 )
(STRATEGY INNERMOST)
(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,*(@x,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)) ->= #pos(#natdiv(@x,@y))
        #div(#neg(@x),#pos(@y)) ->= #neg(#natdiv(@x,@y))
        #div(#pos(@x),#0) ->= #divByZero
        #div(#pos(@x),#neg(@y)) ->= #neg(#natdiv(@x,@y))
        #div(#pos(@x),#pos(@y)) ->= #pos(#natdiv(@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))
        #natdiv(#0,#0) ->= #divByZero
        #natdiv(#s(@x),#s(@y)) ->= #s(#natdiv(#natsub(@x,@y),#s(@y)))
        #natmult(#0,@y) ->= #0
        #natmult(#s(@x),@y) ->= #add(#pos(@y),#natmult(@x,@y))
        #natsub(@x,#0) ->= @x
        #natsub(#s(@x),#s(@y)) ->= #natsub(@x,@y)
        #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)))
)