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) perfectp#(s(X)) => f#(X, s(0), s(X), s(X))
      (2) f#(s(Y1), 0, U1, X1) => f#(Y1, X1, minus(U1, s(Y1)), X1)
      (3) f#(s(W1), s(P1), X2, V1) => f#(s(W1), minus(P1, W1), X2, V1)
      (4) f#(s(W1), s(P1), X2, V1) => f#(W1, V1, X2, V1)
      (5) map#(G2, cons(V2, W2)) => map#(G2, W2)
      (6) filter#(F3, cons(Y3, U3)) => filter2#(F3(Y3), F3, Y3, U3)
      (7) filter2#(true, H3, W3, P3) => filter#(H3, P3)
      (8) filter2#(false, F4, Y4, U4) => filter#(F4, U4)

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

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

  P2. (1) f#(s(Y1), 0, U1, X1) => f#(Y1, X1, minus(U1, s(Y1)), X1)
      (2) f#(s(W1), s(P1), X2, V1) => f#(W1, V1, X2, V1)

  P3. (1) map#(G2, cons(V2, W2)) => map#(G2, W2)

  P4. (1) filter#(F3, cons(Y3, U3)) => filter2#(F3(Y3), F3, Y3, U3)
      (2) filter2#(true, H3, W3, P3) => filter#(H3, P3)
      (3) filter2#(false, F4, Y4, U4) => filter#(F4, U4)

***** We apply the Subterm Criterion Processor on P2.

We use the following projection function:

  nu(f#) = 1

We thus have:

  (1) s(Y1) |>| Y1
  (2) s(W1) |>| W1

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(V2, W2) |>| W2

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(Y3, U3) |>|  U3
  (2) P3           |>=| P3
  (3) U4           |>=| U4

We may remove the strictly oriented DPs, which yields:

  P5. (1) filter2#(true, H3, W3, P3) => filter#(H3, P3)
      (2) filter2#(false, F4, Y4, U4) => filter#(F4, U4)

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

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