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) 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 P1. Considering the 3 SCCs, this DP problem is split into the following new problems. 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 P2. 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. ***** We apply the Subterm Criterion Processor on P3. 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. ***** We apply the Subterm Criterion Processor on P4. 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, which yields: 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 P5. As there are no SCCs, this DP problem is removed.