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(Y), s(U)) => minus#(Y, U)
      (2)  quot#(s(W), s(P)) => minus#(W, P)
      (3)  quot#(s(W), s(P)) => quot#(minus(W, P), s(P))
      (4)  le#(s(U1), s(V1)) => le#(U1, V1)
      (5)  app#(add(P1, X2), Y2) => app#(X2, Y2)
      (6)  low#(W2, add(V2, P2)) => le#(V2, W2)
      (7)  low#(W2, add(V2, P2)) => if_low#(le(V2, W2), W2, add(V2, P2))
      (8)  if_low#(true, Y3, add(X3, U3)) => low#(Y3, U3)
      (9)  if_low#(false, W3, add(V3, P3)) => low#(W3, P3)
      (10) high#(U4, add(Y4, V4)) => le#(Y4, U4)
      (11) high#(U4, add(Y4, V4)) => if_high#(le(Y4, U4), U4, add(Y4, V4))
      (12) if_high#(true, P4, add(W4, X5)) => high#(P4, X5)
      (13) if_high#(false, U5, add(Y5, V5)) => high#(U5, V5)
      (14) quicksort#(add(W5, P5)) => low#(W5, P5)
      (15) quicksort#(add(W5, P5)) => quicksort#(low(W5, P5))
      (16) quicksort#(add(W5, P5)) => high#(W5, P5)
      (17) quicksort#(add(W5, P5)) => quicksort#(high(W5, P5))
      (18) quicksort#(add(W5, P5)) => app#(quicksort(low(W5, P5)), add(W5, quicksort(high(W5, P5))))
      (19) map#(Z6, add(U6, V6)) => map#(Z6, V6)
      (20) filter#(J6, add(X7, Y7)) => filter2#(J6(X7), J6, X7, Y7)
      (21) filter2#(true, G7, V7, W7) => filter#(G7, W7)
      (22) filter2#(false, J7, X8, Y8) => filter#(J7, Y8)

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

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

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

  P3. (1) quot#(s(W), s(P)) => quot#(minus(W, P), s(P))

  P4. (1) le#(s(U1), s(V1)) => le#(U1, V1)

  P5. (1) app#(add(P1, X2), Y2) => app#(X2, Y2)

  P6. (1) low#(W2, add(V2, P2)) => if_low#(le(V2, W2), W2, add(V2, P2))
      (2) if_low#(true, Y3, add(X3, U3)) => low#(Y3, U3)
      (3) if_low#(false, W3, add(V3, P3)) => low#(W3, P3)

  P7. (1) high#(U4, add(Y4, V4)) => if_high#(le(Y4, U4), U4, add(Y4, V4))
      (2) if_high#(true, P4, add(W4, X5)) => high#(P4, X5)
      (3) if_high#(false, U5, add(Y5, V5)) => high#(U5, V5)

  P8. (1) quicksort#(add(W5, P5)) => quicksort#(low(W5, P5))
      (2) quicksort#(add(W5, P5)) => quicksort#(high(W5, P5))

  P9. (1) map#(Z6, add(U6, V6)) => map#(Z6, V6)

  P10. (1) filter#(J6, add(X7, Y7)) => filter2#(J6(X7), J6, X7, Y7)
       (2) filter2#(true, G7, V7, W7) => filter#(G7, W7)
       (3) filter2#(false, J7, X8, Y8) => filter#(J7, Y8)

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

We use the following projection function:

  nu(minus#) = 1

We thus have:

  (1) s(Y) |>| Y

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

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