We consider universal computability of the STRS with no additional rule schemes:

  Signature: 0      :: a
             asort  :: b -> b
             cons   :: a -> b -> b
             dsort  :: 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: sort(F, Z, nil) -> nil
         sort(G, H, cons(W, P)) -> insert(G, H, sort(G, H, P), W)
         insert(F1, Z1, nil, U1) -> cons(U1, nil)
         insert(H1, I1, cons(P1, Y2), X2) -> cons(H1(P1, X2), insert(H1, I1, Y2, I1(P1, X2)))
         max(0, U2) -> U2
         max(V2, 0) -> V2
         max(s(W2), s(P2)) -> max(W2, P2)
         min(0, X3) -> 0
         min(Y3, 0) -> 0
         min(s(U3), s(V3)) -> min(U3, V3)
         asort(W3) -> sort(min, max, W3)
         dsort(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 UNION R_?, i, c), where:

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

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

We compute a graph approximation with the following edges:

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

There are 4 SCCs.

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

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

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.

Processor output: { }.

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

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.

Processor output: { }.

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

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.

Processor output: { }.

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

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.

Processor output: { }.