We consider universal computability of the STRS with no additional rule schemes:

  Signature: *        :: a -> a -> a
             +        :: a -> a -> a
             -        :: a -> a -> a
             0        :: a
             1        :: a
             2        :: a
             D        :: a -> a
             cons     :: c -> d -> d
             constant :: a
             div      :: a -> a -> a
             false    :: b
             filter   :: (c -> b) -> d -> d
             filter2  :: b -> (c -> b) -> c -> d -> d
             ln       :: a -> a
             map      :: (c -> c) -> d -> d
             minus    :: a -> a
             nil      :: d
             pow      :: a -> a -> a
             t        :: a
             true     :: b

  Rules: D(t) -> 1
         D(constant) -> 0
         D(+(X, Y)) -> +(D(X), D(Y))
         D(*(U, V)) -> +(*(V, D(U)), *(U, D(V)))
         D(-(W, P)) -> -(D(W), D(P))
         D(minus(X1)) -> minus(D(X1))
         D(div(Y1, U1)) -> -(div(D(Y1), U1), div(*(Y1, D(U1)), pow(U1, 2)))
         D(ln(V1)) -> div(D(V1), V1)
         D(pow(W1, P1)) -> +(*(*(P1, pow(W1, -(P1, 1))), D(W1)), *(*(pow(W1, P1), ln(W1)), D(P1)))
         map(F2, nil) -> nil
         map(Z2, cons(U2, V2)) -> cons(Z2(U2), map(Z2, V2))
         filter(I2, nil) -> nil
         filter(J2, cons(X3, Y3)) -> filter2(J2(X3), J2, X3, Y3)
         filter2(true, G3, V3, W3) -> cons(V3, filter(G3, W3))
         filter2(false, J3, X4, Y4) -> filter(J3, Y4)

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)  D#(+(X, Y)) => D#(X)
      (2)  D#(+(X, Y)) => D#(Y)
      (3)  D#(*(U, V)) => D#(U)
      (4)  D#(*(U, V)) => D#(V)
      (5)  D#(-(W, P)) => D#(W)
      (6)  D#(-(W, P)) => D#(P)
      (7)  D#(minus(X1)) => D#(X1)
      (8)  D#(div(Y1, U1)) => D#(Y1)
      (9)  D#(div(Y1, U1)) => D#(U1)
      (10) D#(ln(V1)) => D#(V1)
      (11) D#(pow(W1, P1)) => D#(W1)
      (12) D#(pow(W1, P1)) => D#(P1)
      (13) map#(Z2, cons(U2, V2)) => map#(Z2, V2)
      (14) filter#(J2, cons(X3, Y3)) => filter2#(J2(X3), J2, X3, Y3)
      (15) filter2#(true, G3, V3, W3) => filter#(G3, W3)
      (16) filter2#(false, J3, X4, Y4) => filter#(J3, Y4)

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

We compute a graph approximation with the following edges:

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

There are 3 SCCs.

Processor output: { D2 = (P2, R UNION R_?, i, c) ; D3 = (P3, R UNION R_?, i, c) ; D4 = (P4, R UNION R_?, i, c) }, where:

  P2. (1)  D#(+(X, Y)) => D#(X)
      (2)  D#(+(X, Y)) => D#(Y)
      (3)  D#(*(U, V)) => D#(U)
      (4)  D#(*(U, V)) => D#(V)
      (5)  D#(-(W, P)) => D#(W)
      (6)  D#(-(W, P)) => D#(P)
      (7)  D#(minus(X1)) => D#(X1)
      (8)  D#(div(Y1, U1)) => D#(Y1)
      (9)  D#(div(Y1, U1)) => D#(U1)
      (10) D#(ln(V1)) => D#(V1)
      (11) D#(pow(W1, P1)) => D#(W1)
      (12) D#(pow(W1, P1)) => D#(P1)

  P3. (1) map#(Z2, cons(U2, V2)) => map#(Z2, V2)

  P4. (1) filter#(J2, cons(X3, Y3)) => filter2#(J2(X3), J2, X3, Y3)
      (2) filter2#(true, G3, V3, W3) => filter#(G3, W3)
      (3) filter2#(false, J3, X4, Y4) => filter#(J3, Y4)

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

We use the following projection function:

  nu(D#) = 1

We thus have:

  (1)  +(X, Y)     |>| X
  (2)  +(X, Y)     |>| Y
  (3)  *(U, V)     |>| U
  (4)  *(U, V)     |>| V
  (5)  -(W, P)     |>| W
  (6)  -(W, P)     |>| P
  (7)  minus(X1)   |>| X1
  (8)  div(Y1, U1) |>| Y1
  (9)  div(Y1, U1) |>| U1
  (10) ln(V1)      |>| V1
  (11) pow(W1, P1) |>| W1
  (12) pow(W1, P1) |>| P1

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

Processor output: { }.

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

We use the following projection function:

  nu(map#) = 2

We thus have:

  (1) cons(U2, V2) |>| V2

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

Processor output: { }.

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

We use the following projection function:

  nu(filter#)  = 2
  nu(filter2#) = 4

We thus have:

  (1) cons(X3, Y3) |>|  Y3
  (2) W3           |>=| W3
  (3) Y4           |>=| Y4

We may remove the strictly oriented DPs.

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

  P5. (1) filter2#(true, G3, V3, W3) => filter#(G3, W3)
      (2) filter2#(false, J3, X4, Y4) => filter#(J3, Y4)

***** We apply the Graph Processor on D5 = (P5, 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: { }.