We consider termination 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)) | x = x
         split(x, e) -> pair(e, e) | x = x
         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) | x = x
         if_3(pair(yl, yh), x, ys) -> app(qsort(yl), cons(x, qsort(yh))) | x = x

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)  app#(cons(x, ys), zs) => app#(ys, zs) | x = x
      (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) | x = x
      (7)  qsort#(ins(x, ys)) => if_3#(split(x, ys), x, ys) | x = x
      (8)  if_3#(pair(yl, yh), x, ys) => qsort#(yl) | x = x
      (9)  if_3#(pair(yl, yh), x, ys) => qsort#(yh) | x = x
      (10) if_3#(pair(yl, yh), x, ys) => app#(qsort(yl), cons(x, qsort(yh))) | x = x

***** 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 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, i, c) ; D3 = (P3, R, i, c) ; D4 = (P4, R, i, c) }, where:

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

  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) | x = x
      (2) if_3#(pair(yl, yh), x, ys) => qsort#(yl) | x = x
      (3) if_3#(pair(yl, yh), x, ys) => qsort#(yh) | x = x

***** We apply the Subterm Criterion Processor on D2 = (P2, R, i, 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, i, 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 Usable Rules Processor on D4 = (P4, R, i, c).

We obtain 5 usable rules (out of 10 rules in the input problem).

Processor output: { D5 = (P4, R2, i, c) }, where:

  R2. (1) if_1(pair(zl, zh), x, y, zs) -> pair(ins(y, zl), zh) | x > y
      (2) if_2(pair(zl, zh), x, y, zs) -> pair(zl, ins(y, zh)) | y >= x
      (3) split(x, e) -> pair(e, e) | x = x
      (4) split(x, ins(y, zs)) -> if_1(split(x, zs), x, y, zs) | x > y
      (5) split(x, ins(y, zs)) -> if_2(split(x, zs), x, y, zs) | y >= x

***** We apply the Reduction Pair [with HORPO] Processor on D5 = (P4, R2, i, c).

Constrained HORPO yields:

  qsort#(ins(x, ys)) (>) if_3#(split(x, ys), x, ys) | x = x
  if_3#(pair(yl, yh), x, ys) (>) qsort#(yl) | x = x
  if_3#(pair(yl, yh), x, ys) (>) qsort#(yh) | x = x
  if_1(pair(zl, zh), x, y, zs) (>=) pair(ins(y, zl), zh) | x > y
  if_2(pair(zl, zh), x, y, zs) (>=) pair(zl, ins(y, zh)) | y >= x
  split(x, e) (>=) pair(e, e) | x = x
  split(x, ins(y, zs)) (>=) if_1(split(x, zs), x, y, zs) | x > y
  split(x, ins(y, zs)) (>=) if_2(split(x, zs), x, y, zs) | y >= x

We do this using the following settings:

* Disregarded arguments:

  if_2  4 
  if_3# 3 
  split 1 

* Precedence and permutation:

    if_1    { 1 }   2 3 4
  = if_2    { 1 3 } _ _ 2
  = ins     { 2 }   1
  = split   { 2 }
  > if_3#   { 2 }   _ 1
  = pair    { 1 2 }
  = qsort#  { 1 }
  > e       { }

* Well-founded theory orderings:

  [>]_{Bool} = {(true,false)}
  [>]_{Int}  = {(x,y) | x > -1000 /\ x > y }

All dependency pairs were removed.

Processor output: { }.