We consider universal computability of the LCTRS with only rule scheme Calc:

  Signature: cons    :: Int -> o -> o
             filter  :: Int -> o -> o
             if_1    :: Bool -> Int -> Int -> o -> o
             if_2    :: Bool -> Int -> Int -> o -> o
             isdiv   :: Int -> Int -> Bool
             isprime :: Int -> Bool
             mem     :: Int -> o -> Bool
             nats    :: Int -> Int -> o
             nil     :: o
             primes  :: Int -> o
             sieve   :: o -> o

  Rules: isprime(x) -> mem(x, primes(x)) | x = x
         mem(x, nil) -> false | x = x
         mem(x, cons(y, zs)) -> true | x = y
         mem(x, cons(y, zs)) -> mem(x, zs) | y > x
         mem(x, cons(y, zs)) -> mem(x, zs) | x > y
         primes(x) -> sieve(nats(2, x)) | x = x
         nats(x, y) -> nil | x > y
         nats(x, y) -> cons(x, nil) | x = y
         nats(x, y) -> cons(x, nats(x + 1, y)) | y > x
         sieve(nil) -> nil
         sieve(cons(x, ys)) -> cons(x, sieve(filter(x, ys))) | x = x
         filter(x, nil) -> nil | x = x
         filter(x, cons(y, zs)) -> if_1(isdiv(x, y), x, y, zs) | x = x /\ y = y
         if_1(true, x, y, zs) -> filter(x, zs) | x = x /\ y = y
         filter(x, cons(y, zs)) -> if_2(isdiv(x, y), x, y, zs) | x = x /\ y = y
         if_2(false, x, y, zs) -> cons(x, filter(x, zs)) | x = x /\ y = y
         isdiv(x, 0) -> true | x > 0
         isdiv(x, y) -> false | x > y /\ y > 0
         isdiv(x, y) -> isdiv(x, -x + y) | y >= x /\ x > 0
         isdiv(x, y) -> isdiv(x, -y) | 0 > y /\ x = x
         isdiv(x, y) -> isdiv(-x, y) | 0 > x /\ y = y

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

We start by computing the initial DP problem D1 = (P1, R UNION R_?, i, c), where:

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

***** We apply the Graph Processor on D1 = (P1, R UNION R_?, i, c).

We compute a graph approximation with the following edges:

  1:  5 6 
  2:  3 4 
  3:  3 4 
  4:  3 4 
  5:  7 
  6:  8 9 
  7:  7 
  8:  10 11 13 14 
  9:  8 9 
  10: 16 17 18 
  11: 12 
  12: 10 11 13 14 
  13: 16 17 18 
  14: 15 
  15: 10 11 13 14 
  16: 16 
  17: 16 18 
  18: 16 17 

There are 6 SCCs.

Processor output: { D2 = (P2, R UNION R_?, i, c) ; D3 = (P3, R UNION R_?, i, c) ; D4 = (P4, R UNION R_?, i, c) ; D5 = (P5, R UNION R_?, i, c) ; D6 = (P6, R UNION R_?, i, c) ; D7 = (P7, R UNION R_?, i, c) }, where:

  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 /\ x = x
      (2) isdiv#(x, y) => isdiv#(-x, y) | 0 > x /\ y = y

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

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

  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 D2 = (P2, R UNION R_?, i, c).

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.

Processor output: { }.

***** We apply the Integer Function Processor on D3 = (P3, R UNION R_?, i, c).

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.

Processor output: { }.

***** We apply the Integer Function Processor on D4 = (P4, R UNION R_?, i, c).

We use the following integer mapping:

  J(isdiv#) = 0 - arg_2

We thus have:

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

We may remove the strictly oriented DPs, which yields:

Processor output: { D8 = (P8, R UNION R_?, i, c) }, where:

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

***** We apply the Subterm Criterion Processor on D5 = (P5, R UNION R_?, i, c).

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.

Processor output: { D9 = (P9, R UNION R_?, i, c) }, where:

  P9. (1) if_1#(true, x, y, zs) => filter#(x, zs) | x = x /\ y = y
      (2) if_2#(false, x, y, zs) => filter#(x, zs) | x = x /\ y = y

***** We apply the Usable Rules Processor on D6 = (P6, R UNION R_?, i, c).

We obtain 10 usable rules (out of 21 rules in the input problem).

Processor output: { D10 = (P6, R2, i, c) }, where:

  R2. (1)  filter(x, nil) -> nil | x = x
      (2)  filter(x, cons(y, zs)) -> if_1(isdiv(x, y), x, y, zs) | x = x /\ y = y
      (3)  filter(x, cons(y, zs)) -> if_2(isdiv(x, y), x, y, zs) | x = x /\ y = y
      (4)  if_1(true, x, y, zs) -> filter(x, zs) | x = x /\ y = y
      (5)  if_2(false, x, y, zs) -> cons(x, filter(x, zs)) | x = x /\ y = y
      (6)  isdiv(x, 0) -> true | x > 0
      (7)  isdiv(x, y) -> false | x > y /\ y > 0
      (8)  isdiv(x, y) -> isdiv(x, -x + y) | y >= x /\ x > 0
      (9)  isdiv(x, y) -> isdiv(x, -y) | 0 > y /\ x = x
      (10) isdiv(x, y) -> isdiv(-x, y) | 0 > x /\ y = y

***** We apply the Subterm Criterion Processor on D7 = (P7, R UNION R_?, i, c).

We use the following projection function:

  nu(mem#) = 2

We thus have:

  (1) cons(y, zs) |>| zs
  (2) cons(y, zs) |>| zs

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

Processor output: { }.

***** We apply the Graph Processor on D8 = (P8, R UNION R_?, i, c).

We compute a graph approximation with the following edges:

  1:

As there are no SCCs, this DP problem is removed.

Processor output: { }.

***** We apply the Graph Processor on D9 = (P9, R UNION R_?, i, c).

We compute a graph approximation with the following edges:

  1:
  2:

As there are no SCCs, this DP problem is removed.

Processor output: { }.

***** No progress could be made on DP problem D10 = (P6, R2, i, c).