We consider universal computability of the LCTRS with only rule scheme Calc:

  Signature: app   :: o -> o -> o
             cons  :: Int -> o -> o
             e     :: o
             if_1  :: o -> Int -> Int -> o -> o
             if_2  :: o -> Int -> Int -> o -> o
             if_3  :: o -> Int -> o -> o
             ins   :: Int -> o -> o
             nil   :: o
             pair  :: o -> o -> o
             qsort :: o -> o
             split :: Int -> o -> o

  Rules: app(nil, zs) -> zs
         app(cons(x, ys), zs) -> cons(x, app(ys, zs))
         split(x, e) -> pair(e, e)
         split(x, ins(y, zs)) -> if_1(split(x, zs), x, y, zs) | x > y
         if_1(pair(zl, zh), x, y, zs) -> pair(ins(y, zl), zh) | x > y
         split(x, ins(y, zs)) -> if_2(split(x, zs), x, y, zs) | y >= x
         if_2(pair(zl, zh), x, y, zs) -> pair(zl, ins(y, zh)) | y >= x
         qsort(e) -> nil
         qsort(ins(x, ys)) -> if_3(split(x, ys), x, ys)
         if_3(pair(yl, yh), x, ys) -> app(qsort(yl), cons(x, qsort(yh)))

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_?, f, c), where:

  P1. (1)  app#(cons(x, ys), zs) => app#(ys, zs)
      (2)  split#(x, ins(y, zs)) => split#(x, zs) | x > y
      (3)  split#(x, ins(y, zs)) => if_1#(split(x, zs), x, y, zs) | x > y
      (4)  split#(x, ins(y, zs)) => split#(x, zs) | y >= x
      (5)  split#(x, ins(y, zs)) => if_2#(split(x, zs), x, y, zs) | y >= x
      (6)  qsort#(ins(x, ys)) => split#(x, ys)
      (7)  qsort#(ins(x, ys)) => if_3#(split(x, ys), x, ys)
      (8)  if_3#(pair(yl, yh), x, ys) => qsort#(yl)
      (9)  if_3#(pair(yl, yh), x, ys) => qsort#(yh)
      (10) if_3#(pair(yl, yh), x, ys) => app#(qsort(yl), cons(x, qsort(yh)))

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

We compute a graph approximation with the following edges:

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

There are 3 SCCs.

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

  P2. (1) app#(cons(x, ys), zs) => app#(ys, zs)

  P3. (1) split#(x, ins(y, zs)) => split#(x, zs) | x > y
      (2) split#(x, ins(y, zs)) => split#(x, zs) | y >= x

  P4. (1) qsort#(ins(x, ys)) => if_3#(split(x, ys), x, ys)
      (2) if_3#(pair(yl, yh), x, ys) => qsort#(yl)
      (3) if_3#(pair(yl, yh), x, ys) => qsort#(yh)

***** We apply the Subterm Criterion Processor on D2 = (P2, R UNION R_?, f, c).

We use the following projection function:

  nu(app#) = 1

We thus have:

  (1) cons(x, ys) |>| ys

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_?, f, c).

We use the following projection function:

  nu(split#) = 2

We thus have:

  (1) ins(y, zs) |>| zs
  (2) ins(y, zs) |>| zs

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

Processor output: { }.

***** We apply the Theory Arguments Processor on D4 = (P4, R UNION R_?, f, c).

We use the following theory arguments function:

  if_3#  : [2]
  qsort# : []

Processor output: { D5 = (P5, R UNION R_?, f, c) ; D6 = (P6, R UNION R_?, f, c) }, where:

  P5. (1) qsort#(ins(x, ys)) => if_3#(split(x, ys), x, ys)
      (2) if_3#(pair(yl, yh), x, ys) => qsort#(yl) { x }
      (3) if_3#(pair(yl, yh), x, ys) => qsort#(yh) { x }

  P6. (1) if_3#(pair(yl, yh), x, ys) => qsort#(yl)
      (2) if_3#(pair(yl, yh), x, ys) => qsort#(yh)

***** No progress could be made on DP problem D5 = (P5, R UNION R_?, f, c).