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)  minus#(s(U), s(V)) => minus#(U, V)
      (2)  le#(s(X1), s(Y1)) => le#(X1, Y1)
      (3)  perfectp#(s(X2)) => f#(X2, s(0), s(X2), s(X2))
      (4)  f#(s(Y3), 0, U3, X3) => minus#(U3, s(Y3))
      (5)  f#(s(Y3), 0, U3, X3) => f#(Y3, X3, minus(U3, s(Y3)), X3)
      (6)  f#(s(W3), s(P3), X4, V3) => le#(W3, P3)
      (7)  f#(s(W3), s(P3), X4, V3) => minus#(P3, W3)
      (8)  f#(s(W3), s(P3), X4, V3) => f#(s(W3), minus(P3, W3), X4, V3)
      (9)  f#(s(W3), s(P3), X4, V3) => f#(W3, V3, X4, V3)
      (10) f#(s(W3), s(P3), X4, V3) => if#(le(W3, P3), f(s(W3), minus(P3, W3), X4, V3), f(W3, V3, X4, V3))
      (11) map#(G4, cons(V4, W4)) => map#(G4, W4)
      (12) filter#(F5, cons(Y5, U5)) => filter2#(F5(Y5), F5, Y5, U5)
      (13) filter2#(true, H5, W5, P5) => filter#(H5, P5)
      (14) filter2#(false, F6, Y6, U6) => filter#(F6, U6)

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

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

  P2. (1) minus#(s(U), s(V)) => minus#(U, V)

  P3. (1) le#(s(X1), s(Y1)) => le#(X1, Y1)

  P4. (1) f#(s(Y3), 0, U3, X3) => f#(Y3, X3, minus(U3, s(Y3)), X3)
      (2) f#(s(W3), s(P3), X4, V3) => f#(s(W3), minus(P3, W3), X4, V3)
      (3) f#(s(W3), s(P3), X4, V3) => f#(W3, V3, X4, V3)

  P5. (1) map#(G4, cons(V4, W4)) => map#(G4, W4)

  P6. (1) filter#(F5, cons(Y5, U5)) => filter2#(F5(Y5), F5, Y5, U5)
      (2) filter2#(true, H5, W5, P5) => filter#(H5, P5)
      (3) filter2#(false, F6, Y6, U6) => filter#(F6, U6)

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

We use the following projection function:

  nu(minus#) = 1

We thus have:

  (1) s(U) |>| U

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(le#) = 1

We thus have:

  (1) s(X1) |>| X1

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(f#) = 1

We thus have:

  (1) s(Y3) |>|  Y3
  (2) s(W3) |>=| s(W3)
  (3) s(W3) |>|  W3

We may remove the strictly oriented DPs, which yields:

  P7. (1) f#(s(W3), s(P3), X4, V3) => f#(s(W3), minus(P3, W3), X4, V3)

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

We use the following projection function:

  nu(map#) = 2

We thus have:

  (1) cons(V4, W4) |>| W4

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

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

We use the following projection function:

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

We thus have:

  (1) cons(Y5, U5) |>|  U5
  (2) P5           |>=| P5
  (3) U6           |>=| U6

We may remove the strictly oriented DPs, which yields:

  P8. (1) filter2#(true, H5, W5, P5) => filter#(H5, P5)
      (2) filter2#(false, F6, Y6, U6) => filter#(F6, U6)

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