We consider termination of the LCTRS with only rule scheme Calc:

  Signature: 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
             min   :: Int -> o -> o
             msort :: o -> o
             nil   :: o
             pair  :: Int -> o -> o

  Rules: min(x, e) -> pair(x, e)
         min(x, ins(y, zs)) -> if_1(min(y, zs), x, y, zs)
         if_1(pair(m, zh), x, y, zs) -> pair(x, ins(m, zh)) | m > x
         min(x, ins(y, zs)) -> if_2(min(y, zs), x, y, zs)
         if_2(pair(m, zh), x, y, zs) -> pair(m, ins(x, zh)) | x >= m
         msort(e) -> nil
         msort(ins(x, ys)) -> if_3(min(x, ys), x, ys)
         if_3(pair(m, zs), x, ys) -> cons(m, msort(zs))

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

  P1. (1) min#(x, ins(y, zs)) => min#(y, zs)
      (2) min#(x, ins(y, zs)) => if_1#(min(y, zs), x, y, zs)
      (3) min#(x, ins(y, zs)) => min#(y, zs)
      (4) min#(x, ins(y, zs)) => if_2#(min(y, zs), x, y, zs)
      (5) msort#(ins(x, ys)) => min#(x, ys)
      (6) msort#(ins(x, ys)) => if_3#(min(x, ys), x, ys)
      (7) if_3#(pair(m, zs), x, ys) => msort#(zs)

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

We compute a graph approximation with the following edges:

  1: 1 2 3 4 
  2:
  3: 1 2 3 4 
  4:
  5: 1 2 3 4 
  6: 7 
  7: 5 6 

There are 2 SCCs.

Processor output: { D2 = (P2, R, f, c) ; D3 = (P3, R, f, c) }, where:

  P2. (1) min#(x, ins(y, zs)) => min#(y, zs)
      (2) min#(x, ins(y, zs)) => min#(y, zs)

  P3. (1) msort#(ins(x, ys)) => if_3#(min(x, ys), x, ys)
      (2) if_3#(pair(m, zs), x, ys) => msort#(zs)

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

We use the following projection function:

  nu(min#) = 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 D3 = (P3, R, f, c).

We use the following theory arguments function:

  if_3#  : [2]
  msort# : []

Processor output: { D4 = (P4, R, f, c) ; D5 = (P5, R, f, c) }, where:

  P4. (1) msort#(ins(x, ys)) => if_3#(min(x, ys), x, ys)
      (2) if_3#(pair(m, zs), x, ys) => msort#(zs) { x }

  P5. (1) if_3#(pair(m, zs), x, ys) => msort#(zs)

***** We apply the Reduction Pair [with HORPO] Processor on D4 = (P4, R, f, c).

Constrained HORPO yields:

  msort#(ins(x, ys)) (>) if_3#(min(x, ys), x, ys)
  if_3#(pair(m, zs), x, ys) (>) msort#(zs) { x }
  min(x, e) (>=) pair(x, e)
  min(x, ins(y, zs)) (>=) if_1(min(y, zs), x, y, zs)
  if_1(pair(m, zh), x, y, zs) (>=) pair(x, ins(m, zh)) | m > x
  min(x, ins(y, zs)) (>=) if_2(min(y, zs), x, y, zs)
  if_2(pair(m, zh), x, y, zs) (>=) pair(m, ins(x, zh)) | x >= m
  msort(e) (>=) nil
  msort(ins(x, ys)) (>=) if_3(min(x, ys), x, ys)
  if_3(pair(m, zs), x, ys) (>=) cons(m, msort(zs))

We do this using the following settings:

* Disregarded arguments:

  cons 1 
  if_1 2 
  if_2 2 
  if_3 3 

* Precedence and permutation:

    if_1    { 1 }   _ 3 _ 4
  = if_2    { 1 }   _ 3 _ 4
  = ins     { 1 2 }
  = min     { 2 }   1
  > e       { }
  = if_3    { 1 }   _ 2
  = nil     { }
  > cons    { }     2
  = pair    { 2 }   1
  > if_3#   { 1 2 } _ 3
  = msort#  { 1 }
  = msort   { 1 }

* Well-founded theory orderings:

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

All dependency pairs were removed.

Processor output: { }.

***** We apply the Graph Processor on D5 = (P5, R, f, c).

We compute a graph approximation with the following edges:

  1:

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

Processor output: { }.