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)  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 P1.

Considering the 3 SCCs, this DP problem is split into the following new problems.

  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 P2.

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.

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

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.

***** We apply the Theory Arguments Processor on P4.

We use the following theory arguments function:

  if_3#  : [2]
  qsort# : []

This yields the following new DP problems:

  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 P5.