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

  Signature: 0         :: b
             add       :: b -> c -> c
             app       :: c -> c -> c
             false     :: a
             filter    :: (b -> a) -> c -> c
             filter2   :: a -> (b -> a) -> b -> c -> c
             high      :: b -> c -> c
             if_high   :: a -> b -> c -> c
             if_low    :: a -> b -> c -> c
             le        :: b -> b -> a
             low       :: b -> c -> c
             map       :: (b -> b) -> c -> c
             minus     :: b -> b -> b
             nil       :: c
             quicksort :: c -> c
             quot      :: b -> b -> b
             s         :: b -> b
             true      :: a

  Rules: minus(X, 0) -> X
         minus(s(Y), s(U)) -> minus(Y, U)
         quot(0, s(V)) -> 0
         quot(s(W), s(P)) -> s(quot(minus(W, P), s(P)))
         le(0, X1) -> true
         le(s(Y1), 0) -> false
         le(s(U1), s(V1)) -> le(U1, V1)
         app(nil, W1) -> W1
         app(add(P1, X2), Y2) -> add(P1, app(X2, Y2))
         low(U2, nil) -> nil
         low(W2, add(V2, P2)) -> if_low(le(V2, W2), W2, add(V2, P2))
         if_low(true, Y3, add(X3, U3)) -> add(X3, low(Y3, U3))
         if_low(false, W3, add(V3, P3)) -> low(W3, P3)
         high(X4, nil) -> nil
         high(U4, add(Y4, V4)) -> if_high(le(Y4, U4), U4, add(Y4, V4))
         if_high(true, P4, add(W4, X5)) -> high(P4, X5)
         if_high(false, U5, add(Y5, V5)) -> add(Y5, high(U5, V5))
         quicksort(nil) -> nil
         quicksort(add(W5, P5)) -> app(quicksort(low(W5, P5)), add(W5, quicksort(high(W5, P5))))
         map(F6, nil) -> nil
         map(Z6, add(U6, V6)) -> add(Z6(U6), map(Z6, V6))
         filter(I6, nil) -> nil
         filter(J6, add(X7, Y7)) -> filter2(J6(X7), J6, X7, Y7)
         filter2(true, G7, V7, W7) -> add(V7, filter(G7, W7))
         filter2(false, J7, X8, Y8) -> filter(J7, Y8)

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

We compute a graph approximation with the following edges:

  1:  1 
  2:  1 
  3:  2 3 
  4:  4 
  5:  5 
  6:  4 
  7:  8 9 
  8:  6 7 
  9:  6 7 
  10: 4 
  11: 12 13 
  12: 10 11 
  13: 10 11 
  14: 6 7 
  15: 14 15 16 17 18 
  16: 10 11 
  17: 14 15 16 17 18 
  18: 5 
  19: 19 
  20: 21 22 
  21: 20 
  22: 20 

There are 9 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) ; D6 = (P6, R UNION R_?, i, c) ; D7 = (P7, R UNION R_?, i, c) ; D8 = (P8, R UNION R_?, i, c) ; D9 = (P9, R UNION R_?, i, c) ; D10 = (P10, R UNION R_?, i, c) }, where:

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

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.

Processor output: { }.

***** No progress could be made on DP problem D3 = (P3, R UNION R_?, i, c).