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) :#(:(:(:(C, Y), U), V), X) => :#(Y, V)
      (2) :#(:(:(:(C, Y), U), V), X) => :#(Y, U)
      (3) :#(:(:(:(C, Y), U), V), X) => :#(:(Y, U), V)
      (4) :#(:(:(:(C, Y), U), V), X) => :#(:(:(Y, U), V), X)
      (5) :#(:(:(:(C, Y), U), V), X) => :#(:(Y, V), :(:(:(Y, U), V), X))
      (6) map#(J, cons(X1, Y1)) => map#(J, Y1)
      (7) filter#(H1, cons(W1, P1)) => filter2#(H1(W1), H1, W1, P1)
      (8) filter2#(true, F2, Y2, U2) => filter#(F2, U2)
      (9) filter2#(false, H2, W2, P2) => filter#(H2, P2)

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

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

  P2. (1) :#(:(:(:(C, Y), U), V), X) => :#(Y, V)
      (2) :#(:(:(:(C, Y), U), V), X) => :#(Y, U)
      (3) :#(:(:(:(C, Y), U), V), X) => :#(:(Y, U), V)
      (4) :#(:(:(:(C, Y), U), V), X) => :#(:(:(Y, U), V), X)
      (5) :#(:(:(:(C, Y), U), V), X) => :#(:(Y, V), :(:(:(Y, U), V), X))

  P3. (1) map#(J, cons(X1, Y1)) => map#(J, Y1)

  P4. (1) filter#(H1, cons(W1, P1)) => filter2#(H1(W1), H1, W1, P1)
      (2) filter2#(true, F2, Y2, U2) => filter#(F2, U2)
      (3) filter2#(false, H2, W2, P2) => filter#(H2, P2)

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