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)  max#(s(U), s(V)) => max#(U, V)
      (2)  min#(s(X1), s(Y1)) => min#(X1, Y1)
      (3)  insert#(J1, F2, cons(Y2, U2), V2) => insert#(J1, F2, U2, F2(V2, Y2))
      (4)  sort#(F3, Z3, cons(U3, V3)) => sort#(F3, Z3, V3)
      (5)  sort#(F3, Z3, cons(U3, V3)) => insert#(F3, Z3, sort(F3, Z3, V3), U3)
      (6)  ascending_sort#(W3) => min#(X{24}, X{25})
      (7)  ascending_sort#(W3) => max#(X{26}, X{27})
      (8)  ascending_sort#(W3) => sort#(min, max, W3)
      (9)  descending_sort#(P3) => max#(X{28}, X{29})
      (10) descending_sort#(P3) => min#(X{30}, X{31})
      (11) descending_sort#(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) max#(s(U), s(V)) => max#(U, V)

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

  P4. (1) insert#(J1, F2, cons(Y2, U2), V2) => insert#(J1, F2, U2, F2(V2, Y2))

  P5. (1) sort#(F3, Z3, cons(U3, V3)) => sort#(F3, Z3, V3)

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

We use the following projection function:

  nu(max#) = 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(min#) = 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(insert#) = 3

We thus have:

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

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

We thus have:

  (1) cons(U3, V3) |>| V3

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