(VAR
    l p x x_1 x_2 xs xs' y y_1 y_2 z)
(RULES
    #equal(x,y) -> #eq(x,y)
    eratos(::(x,xs)) -> ::(x,eratos(filter(x,xs)))
    eratos(nil) -> nil
    filter(p,nil) -> nil
    filter(p,::(x,xs)) -> filter'(#equal(#mod(x,p),#0), x, filter(p,xs))
    filter'(#true,x,xs) -> xs
    filter'(#false,x,xs) -> ::(x,xs)

    #mod(x,y) -> #sub(x,#mult(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))
    #positive(#0) ->= #0
    #positive(#s(x)) ->= #pos(#s(x))
    #positive(#pos(x)) ->= #pos(x)
    #positive(#neg(x)) ->= #neg(x)
    #negative(#0) ->= #0
    #negative(#s(x)) ->= #neg(#s(x))
    #negative(#pos(x)) ->= #neg(x)
    #negative(#neg(x)) ->= #pos(x)
    #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(#0,#s(y)) ->= #0
    #natdiv(#s(x),#0) ->= #divByZero
    #natdiv(#s(x),#s(y)) ->= #natdiv'(#divsub(x,y),#s(y))
    #natdiv'(#underflow,y) ->= #0
    #natdiv'(#0,y) ->= #s(#0)
    #natdiv'(#s(x),y) ->= #s(#natdiv(#s(x),y))
    #natdiv(#underflow,y) ->= #0
    #divsub(#0,#0) ->= #0
    #divsub(#0,#s(y)) ->= #underflow
    #divsub(#s(x),#0) ->= #s(x)
    #divsub(#s(x),#s(y)) ->= #divsub(x,y)
    #natmult(#0,y) ->= #0
    #natmult(#s(x),y) ->= #natadd(y,#natmult(x,y))
    #natadd(#0,y) ->= y
    #natadd(#s(x),y) ->= #s(#natadd(x,y))
    #natsub(#0,#0) ->= #0
    #natsub(#0,#s(y)) ->= #0
    #natsub(#s(x),#0) ->= #s(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)))
)