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)  sort#(G, H, cons(W, P)) => sort#(G, H, P)
      (2)  sort#(G, H, cons(W, P)) => insert#(G, H, sort(G, H, P), W)
      (3)  insert#(H1, I1, cons(P1, Y2), X2) => insert#(H1, I1, Y2, I1(P1, X2))
      (4)  max#(s(W2), s(P2)) => max#(W2, P2)
      (5)  min#(s(U3), s(V3)) => min#(U3, V3)
      (6)  asort#(W3) => min#(X{24}, X{25})
      (7)  asort#(W3) => max#(X{26}, X{27})
      (8)  asort#(W3) => sort#(min, max, W3)
      (9)  dsort#(P3) => max#(X{28}, X{29})
      (10) dsort#(P3) => min#(X{30}, X{31})
      (11) dsort#(P3) => sort#(max, min, P3)

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

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

  P2. (1) insert#(H1, I1, cons(P1, Y2), X2) => insert#(H1, I1, Y2, I1(P1, X2))

  P3. (1) sort#(G, H, cons(W, P)) => sort#(G, H, P)

  P4. (1) max#(s(W2), s(P2)) => max#(W2, P2)

  P5. (1) min#(s(U3), s(V3)) => min#(U3, V3)

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

We use the following projection function:

  nu(insert#) = 3

We thus have:

  (1) cons(P1, Y2) |>| Y2

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(sort#) = 3

We thus have:

  (1) cons(W, P) |>| P

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

We thus have:

  (1) s(W2) |>| W2

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

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

We use the following projection function:

  nu(min#) = 1

We thus have:

  (1) s(U3) |>| U3

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