We consider termination of the STRS with no additional rule schemes:

  Signature: 0               :: a
             ascending_sort  :: b -> b
             cons            :: a -> b -> b
             descending_sort :: b -> b
             insert          :: (a -> a -> a) -> (a -> a -> a) -> b -> a -> b
             max             :: a -> a -> a
             min             :: a -> a -> a
             nil             :: b
             s               :: a -> a
             sort            :: (a -> a -> a) -> (a -> a -> a) -> b -> b

  Rules: max(0, X) -> X
         max(Y, 0) -> Y
         max(s(U), s(V)) -> max(U, V)
         min(0, W) -> 0
         min(P, 0) -> 0
         min(s(X1), s(Y1)) -> min(X1, Y1)
         insert(G1, H1, nil, W1) -> cons(W1, nil)
         insert(J1, F2, cons(Y2, U2), V2) -> cons(J1(V2, Y2), insert(J1, F2, U2, F2(V2, Y2)))
         sort(I2, J2, nil) -> nil
         sort(F3, Z3, cons(U3, V3)) -> insert(F3, Z3, sort(F3, Z3, V3), U3)
         ascending_sort(W3) -> sort(min, max, W3)
         descending_sort(P3) -> sort(max, min, P3)

The system is accessible function passing by a sort ordering that equates all sorts.

We start by computing the initial DP problem D1 = (P1, R, i, c), where:

  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#(fresh1, fresh2)
      (7)  ascending_sort#(W3) => max#(fresh1, fresh2)
      (8)  ascending_sort#(W3) => sort#(min, max, W3)
      (9)  descending_sort#(P3) => max#(fresh1, fresh2)
      (10) descending_sort#(P3) => min#(fresh1, fresh2)
      (11) descending_sort#(P3) => sort#(max, min, P3)

***** We apply the Graph Processor on D1 = (P1, R, i, c).

We compute a graph approximation with the following edges:

  1:  1 
  2:  2 
  3:  3 
  4:  4 5 
  5:  3 
  6:  2 
  7:  1 
  8:  4 5 
  9:  1 
  10: 2 
  11: 4 5 

There are 4 SCCs.

Processor output: { D2 = (P2, R, i, c) ; D3 = (P3, R, i, c) ; D4 = (P4, R, i, c) ; D5 = (P5, R, i, c) }, where:

  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 D2 = (P2, R, i, c).

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.

Processor output: { }.

***** We apply the Subterm Criterion Processor on D3 = (P3, R, i, c).

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.

Processor output: { }.

***** We apply the Subterm Criterion Processor on D4 = (P4, R, i, c).

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.

Processor output: { }.

***** We apply the Subterm Criterion Processor on D5 = (P5, R, i, c).

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.

Processor output: { }.