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))
         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, i, 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, 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)

  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, 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 Theory Arguments Processor on D4 = (P4, R, i, c).

We use the following theory arguments function:

  if_3#  : [2]
  qsort# : []

Processor output: { D5 = (P5, R, i, c) ; D6 = (P6, R, i, 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 = x
      (3) if_3#(pair(yl, yh), x, ys) => qsort#(yh) | x = x

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

***** We apply the Usable Rules Processor on D5 = (P5, R, i, c).

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

Processor output: { D7 = (P5, 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)
      (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 Graph Processor on D6 = (P6, R, i, c).

We compute a graph approximation with the following edges:

  1:
  2:

As there are no SCCs, this DP problem is removed.

Processor output: { }.

***** We apply the Usable rules with respect to HORPO Processor on D7 = (P5, R2, i, c).

Constrained HORPO yields:

  qsort#1(ins2(x, ys)) (>) if_3#3(split2(x, ys), x, ys)
  if_3#3(pair2(yl, yh), x, ys) (>) qsort#1(yl) | x = x
  if_3#3(pair2(yl, yh), x, ys) (>) qsort#1(yh) | x = x
  if_14(pair2(zl, zh), x, y, zs) (>=) pair2(ins2(y, zl), zh) | x > y
  if_24(pair2(zl, zh), x, y, zs) (>=) pair2(zl, ins2(y, zh)) | y >= x
  split2(x, e0) (>=) pair2(e0, e0)
  split2(x, ins2(y, zs)) (>=) if_14(split2(x, zs), x, y, zs) | x > y
  split2(x, ins2(y, zs)) (>=) if_24(split2(x, zs), x, y, zs) | y >= x

We do this using the following settings:

* Disregarded arguments:

  if_14 4 
  if_24 3 

* Precedence and permutation:

    e0       { }
  = if_14    { 1 }     _ 2 _ 3
  = if_24    { 1 }     _ 4 _ 2
  = ins2     { 1 2 }
  = split2   { 2 }     1
  > pair2    { 1 }     2
  > if_3#3   { 1 2 3 }
  = qsort#1  { 1 }

* Well-founded theory orderings:

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

Processor output: { }.