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)  eq#(s(U), s(V)) => eq#(U, V)
      (2)  le#(s(X1), s(Y1)) => le#(X1, Y1)
      (3)  app#(add(V1, W1), P1) => app#(W1, P1)
      (4)  min#(add(U2, add(Y2, V2))) => le#(U2, Y2)
      (5)  min#(add(U2, add(Y2, V2))) => if_min#(le(U2, Y2), add(U2, add(Y2, V2)))
      (6)  if_min#(true, add(P2, add(W2, X3))) => min#(add(P2, X3))
      (7)  if_min#(false, add(U3, add(Y3, V3))) => min#(add(Y3, V3))
      (8)  rm#(X4, add(P3, Y4)) => eq#(X4, P3)
      (9)  rm#(X4, add(P3, Y4)) => if_rm#(eq(X4, P3), X4, add(P3, Y4))
      (10) if_rm#(true, V4, add(U4, W4)) => rm#(V4, W4)
      (11) if_rm#(false, X5, add(P4, Y5)) => rm#(X5, Y5)
      (12) minsort#(add(U5, V5), W5) => min#(add(U5, V5))
      (13) minsort#(add(U5, V5), W5) => eq#(U5, min(add(U5, V5)))
      (14) minsort#(add(U5, V5), W5) => if_minsort#(eq(U5, min(add(U5, V5))), add(U5, V5), W5)
      (15) if_minsort#(true, add(P5, X6), Y6) => rm#(P5, X6)
      (16) if_minsort#(true, add(P5, X6), Y6) => app#(rm(P5, X6), Y6)
      (17) if_minsort#(true, add(P5, X6), Y6) => minsort#(app(rm(P5, X6), Y6), nil)
      (18) if_minsort#(false, add(U6, V6), W6) => minsort#(V6, add(U6, W6))
      (19) map#(F7, add(Y7, U7)) => map#(F7, U7)
      (20) filter#(I7, add(P7, X8)) => filter2#(I7(P7), I7, P7, X8)
      (21) filter2#(true, Z8, U8, V8) => filter#(Z8, V8)
      (22) filter2#(false, I8, P8, X9) => filter#(I8, X9)

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

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

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

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

  P4. (1) app#(add(V1, W1), P1) => app#(W1, P1)

  P5. (1) min#(add(U2, add(Y2, V2))) => if_min#(le(U2, Y2), add(U2, add(Y2, V2)))
      (2) if_min#(true, add(P2, add(W2, X3))) => min#(add(P2, X3))
      (3) if_min#(false, add(U3, add(Y3, V3))) => min#(add(Y3, V3))

  P6. (1) rm#(X4, add(P3, Y4)) => if_rm#(eq(X4, P3), X4, add(P3, Y4))
      (2) if_rm#(true, V4, add(U4, W4)) => rm#(V4, W4)
      (3) if_rm#(false, X5, add(P4, Y5)) => rm#(X5, Y5)

  P7. (1) minsort#(add(U5, V5), W5) => if_minsort#(eq(U5, min(add(U5, V5))), add(U5, V5), W5)
      (2) if_minsort#(true, add(P5, X6), Y6) => minsort#(app(rm(P5, X6), Y6), nil)
      (3) if_minsort#(false, add(U6, V6), W6) => minsort#(V6, add(U6, W6))

  P8. (1) map#(F7, add(Y7, U7)) => map#(F7, U7)

  P9. (1) filter#(I7, add(P7, X8)) => filter2#(I7(P7), I7, P7, X8)
      (2) filter2#(true, Z8, U8, V8) => filter#(Z8, V8)
      (3) filter2#(false, I8, P8, X9) => filter#(I8, X9)

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

We use the following projection function:

  nu(eq#) = 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(app#) = 1

We thus have:

  (1) add(V1, W1) |>| W1

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

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