(STRATEGY
    INNERMOST)

(VAR
    M N X X1 X2 X3 Y)
(DATATYPES
    A = µX.< 0, mark(X), zprimes, ok(X) >)
(SIGNATURES
    active :: [A] -> A
    filter :: [A x A x A] -> A
    cons :: [A x A] -> A
    s :: [A] -> A
    sieve :: [A] -> A
    nats :: [A] -> A
    proper :: [A] -> A
    top :: [A] -> A)
(RULES
    active(filter(cons(X,Y)
                 ,0()
                 ,M)) -> mark(cons(0()
                                  ,filter(Y,M,M)))
    active(filter(cons(X,Y)
                 ,s(N)
                 ,M)) -> mark(cons(X
                                  ,filter(Y,N,M)))
    active(sieve(cons(0(),Y))) ->
      mark(cons(0(),sieve(Y)))
    active(sieve(cons(s(N),Y))) ->
      mark(cons(s(N)
               ,sieve(filter(Y,N,N))))
    active(nats(N)) -> mark(cons(N
                                ,nats(s(N))))
    active(zprimes()) ->
      mark(sieve(nats(s(s(0())))))
    active(filter(X1,X2,X3)) ->
      filter(active(X1),X2,X3)
    active(filter(X1,X2,X3)) ->
      filter(X1,active(X2),X3)
    active(filter(X1,X2,X3)) ->
      filter(X1,X2,active(X3))
    active(cons(X1,X2)) ->
      cons(active(X1),X2)
    active(s(X)) -> s(active(X))
    active(sieve(X)) ->
      sieve(active(X))
    active(nats(X)) ->
      nats(active(X))
    filter(mark(X1),X2,X3) ->
      mark(filter(X1,X2,X3))
    filter(X1,mark(X2),X3) ->
      mark(filter(X1,X2,X3))
    filter(X1,X2,mark(X3)) ->
      mark(filter(X1,X2,X3))
    cons(mark(X1),X2) ->
      mark(cons(X1,X2))
    s(mark(X)) -> mark(s(X))
    sieve(mark(X)) -> mark(sieve(X))
    nats(mark(X)) -> mark(nats(X))
    proper(filter(X1,X2,X3)) ->
      filter(proper(X1)
            ,proper(X2)
            ,proper(X3))
    proper(cons(X1,X2)) ->
      cons(proper(X1),proper(X2))
    proper(0()) -> ok(0())
    proper(s(X)) -> s(proper(X))
    proper(sieve(X)) ->
      sieve(proper(X))
    proper(nats(X)) ->
      nats(proper(X))
    proper(zprimes()) ->
      ok(zprimes())
    filter(ok(X1),ok(X2),ok(X3)) ->
      ok(filter(X1,X2,X3))
    cons(ok(X1),ok(X2)) ->
      ok(cons(X1,X2))
    s(ok(X)) -> ok(s(X))
    sieve(ok(X)) -> ok(sieve(X))
    nats(ok(X)) -> ok(nats(X))
    top(mark(X)) -> top(proper(X))
    top(ok(X)) -> top(active(X)))