The system is accessible function passing by a sort ordering that equates all sorts.

We start by computing the following initial DP problem:

  P1. (1)  isprime#(x) => primes#(x)
      (2)  isprime#(x) => mem#(x, primes(x))
      (3)  mem#(x, cons(y, zs)) => mem#(x, zs) | y > x
      (4)  mem#(x, cons(y, zs)) => mem#(x, zs) | x > y
      (5)  primes#(x) => nats#(2, x)
      (6)  primes#(x) => sieve#(nats(2, x))
      (7)  nats#(x, y) => nats#(x + 1, y) | y > x
      (8)  sieve#(cons(x, ys)) => filter#(x, ys)
      (9)  sieve#(cons(x, ys)) => sieve#(filter(x, ys))
      (10) filter#(x, cons(y, zs)) => isdiv#(x, y)
      (11) filter#(x, cons(y, zs)) => if_1#(isdiv(x, y), x, y, zs)
      (12) if_1#(true, x, y, zs) => filter#(x, zs)
      (13) filter#(x, cons(y, zs)) => isdiv#(x, y)
      (14) filter#(x, cons(y, zs)) => if_2#(isdiv(x, y), x, y, zs)
      (15) if_2#(false, x, y, zs) => filter#(x, zs)
      (16) isdiv#(x, y) => isdiv#(x, -x + y) | y >= x /\ x > 0
      (17) isdiv#(x, y) => isdiv#(x, -y) | 0 > y
      (18) isdiv#(x, y) => isdiv#(-x, y) | 0 > x

***** We apply the Graph Processor on P1.

Considering the 6 SCCs, this DP problem is split into the following new problems.

  P2. (1) nats#(x, y) => nats#(x + 1, y) | y > x

  P3. (1) isdiv#(x, y) => isdiv#(x, -x + y) | y >= x /\ x > 0

  P4. (1) isdiv#(x, y) => isdiv#(x, -y) | 0 > y
      (2) isdiv#(x, y) => isdiv#(-x, y) | 0 > x

  P5. (1) filter#(x, cons(y, zs)) => if_1#(isdiv(x, y), x, y, zs)
      (2) if_1#(true, x, y, zs) => filter#(x, zs)
      (3) filter#(x, cons(y, zs)) => if_2#(isdiv(x, y), x, y, zs)
      (4) if_2#(false, x, y, zs) => filter#(x, zs)

  P6. (1) sieve#(cons(x, ys)) => sieve#(filter(x, ys))

  P7. (1) mem#(x, cons(y, zs)) => mem#(x, zs) | y > x
      (2) mem#(x, cons(y, zs)) => mem#(x, zs) | x > y

***** We apply the Integer Function Processor on P2.

We use the following integer mapping:

  J(nats#) = arg_2 - arg_1

We thus have:

  (1) y > x |= y - x > y - (x + 1) (and y - x >= 0)

All DPs are strictly oriented, and may be removed.  Hence, this DP problem is finite.

***** We apply the Integer Function Processor on P3.

We use the following integer mapping:

  J(isdiv#) = arg_2

We thus have:

  (1) y >= x /\ x > 0 |= y > -x + y (and y >= 0)

All DPs are strictly oriented, and may be removed.  Hence, this DP problem is finite.

***** We apply the Theory Arguments Processor on P4.

We use the following theory arguments function:

  sieve# : []

This yields the following new DP problems:

  P8. (1) isdiv#(x, y) => isdiv#(x, -y) | 0 > y
      (2) isdiv#(x, y) => isdiv#(-x, y) | 0 > x { x, y }

  P9. (1) isdiv#(x, y) => isdiv#(-x, y) | 0 > x

***** We apply the Subterm Criterion Processor on P5.

We use the following projection function:

  nu(filter#) = 2
  nu(if_1#)   = 4
  nu(if_2#)   = 4

We thus have:

  (1) cons(y, zs) |>|  zs
  (2) zs          |>=| zs
  (3) cons(y, zs) |>|  zs
  (4) zs          |>=| zs

We may remove the strictly oriented DPs, which yields:

  P10. (1) if_1#(true, x, y, zs) => filter#(x, zs)
       (2) if_2#(false, x, y, zs) => filter#(x, zs)

***** No progress could be made on DP problem P6.