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) h#(Y, e(X)) => d#(Y, X) (2) h#(Y, e(X)) => h#(c(Y), d(Y, X)) (3) d#(P, g(V, W)) => d#(P, W) (4) d#(P, g(V, W)) => g#(e(V), d(P, W)) (5) d#(c(U1), g(g(X1, Y1), 0)) => g#(X1, Y1) (6) d#(c(U1), g(g(X1, Y1), 0)) => d#(c(U1), g(X1, Y1)) (7) d#(c(U1), g(g(X1, Y1), 0)) => g#(X1, Y1) (8) d#(c(U1), g(g(X1, Y1), 0)) => d#(U1, g(X1, Y1)) (9) d#(c(U1), g(g(X1, Y1), 0)) => g#(d(c(U1), g(X1, Y1)), d(U1, g(X1, Y1))) (10) g#(e(V1), e(W1)) => g#(V1, W1) (11) map#(F2, cons(Y2, U2)) => map#(F2, U2) (12) filter#(I2, cons(P2, X3)) => filter2#(I2(P2), I2, P2, X3) (13) filter2#(true, Z3, U3, V3) => filter#(Z3, V3) (14) filter2#(false, I3, P3, X4) => filter#(I3, X4) ***** We apply the Graph Processor on P1. Considering the 5 SCCs, this DP problem is split into the following new problems. P2. (1) g#(e(V1), e(W1)) => g#(V1, W1) P3. (1) d#(P, g(V, W)) => d#(P, W) (2) d#(c(U1), g(g(X1, Y1), 0)) => d#(c(U1), g(X1, Y1)) (3) d#(c(U1), g(g(X1, Y1), 0)) => d#(U1, g(X1, Y1)) P4. (1) h#(Y, e(X)) => h#(c(Y), d(Y, X)) P5. (1) map#(F2, cons(Y2, U2)) => map#(F2, U2) P6. (1) filter#(I2, cons(P2, X3)) => filter2#(I2(P2), I2, P2, X3) (2) filter2#(true, Z3, U3, V3) => filter#(Z3, V3) (3) filter2#(false, I3, P3, X4) => filter#(I3, X4) ***** We apply the Subterm Criterion Processor on P2. We use the following projection function: nu(g#) = 1 We thus have: (1) e(V1) |>| V1 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(d#) = 1 We thus have: (1) P |>=| P (2) c(U1) |>=| c(U1) (3) c(U1) |>| U1 We may remove the strictly oriented DPs, which yields: P7. (1) d#(P, g(V, W)) => d#(P, W) (2) d#(c(U1), g(g(X1, Y1), 0)) => d#(c(U1), g(X1, Y1)) ***** No progress could be made on DP problem P4.