(STRATEGY
    INNERMOST)

(VAR
    @l @p @x @x_1 @x_2 @xs @xs' @y
    @y_1 @y_2)
(DATATYPES
    A = µX.< ::(X, X), nil, #0, #false, #true, #neg(X), #s(X), #pos(X), #divByZero >)
(SIGNATURES
    #equal :: [A x A] -> A
    * :: [A x A] -> A
    - :: [A x A] -> A
    div :: [A x A] -> A
    eratos :: [A] -> A
    eratos#1 :: [A] -> A
    filter :: [A x A] -> A
    filter#1 :: [A x A] -> A
    filter#2 :: [A x A x A] -> A
    filter#3 :: [A x A x A] -> A
    mod :: [A x A] -> A
    #add :: [A x A] -> A
    #and :: [A x A] -> A
    #div :: [A x A] -> A
    #eq :: [A x A] -> A
    #mult :: [A x A] -> A
    #natdiv :: [A x A] -> A
    #natmult :: [A x A] -> A
    #natsub :: [A x A] -> A
    #pred :: [A] -> A
    #sub :: [A x A] -> A
    #succ :: [A] -> A)
(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))))