(GOAL COMPLEXITY)
(STARTTERM CONSTRUCTOR-BASED)
(STRATEGY INNERMOST)
(STRATEGY
    INNERMOST)

(VAR
    X Y Z)
(DATATYPES
    A = µX.< s(X), 0, cons(X, X), true, false, divides(X, X) >)
(SIGNATURES
    primes :: [] -> A
    from :: [A] -> A
    head :: [A] -> A
    tail :: [A] -> A
    if :: [A x A x A] -> A
    filter :: [A x A] -> A
    sieve :: [A] -> A)
(RULES
    primes() ->
      sieve(from(s(s(0()))))
    from(X) -> cons(X,from(s(X)))
    head(cons(X,Y)) -> X
    tail(cons(X,Y)) -> Y
    if(true(),X,Y) -> X
    if(false(),X,Y) -> Y
    filter(s(s(X)),cons(Y,Z)) ->
      if(divides(s(s(X)),Y)
        ,filter(s(s(X)),Z)
        ,cons(Y,filter(X,sieve(Y))))
    sieve(cons(X,Y)) -> cons(X
                            ,filter(X,sieve(Y))))