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) | x = x
         min(x, ins(y, zs)) -> if_1(min(y, zs), x, y, zs) | x = x /\ y = y
         if_1(pair(m, zh), x, y, zs) -> pair(x, ins(m, zh)) | m > x /\ y = y
         min(x, ins(y, zs)) -> if_2(min(y, zs), x, y, zs) | x = x /\ y = y
         if_2(pair(m, zh), x, y, zs) -> pair(m, ins(x, zh)) | x >= m /\ y = y
         msort(e) -> nil
         msort(ins(x, ys)) -> if_3(min(x, ys), x, ys) | x = x
         if_3(pair(m, zs), x, ys) -> cons(m, msort(zs)) | m = m /\ 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) min#(x, ins(y, zs)) => min#(y, zs) | x = x /\ y = y
      (2) min#(x, ins(y, zs)) => if_1#(min(y, zs), x, y, zs) | x = x /\ y = y
      (3) min#(x, ins(y, zs)) => min#(y, zs) | x = x /\ y = y
      (4) min#(x, ins(y, zs)) => if_2#(min(y, zs), x, y, zs) | x = x /\ y = y
      (5) msort#(ins(x, ys)) => min#(x, ys) | x = x
      (6) msort#(ins(x, ys)) => if_3#(min(x, ys), x, ys) | x = x
      (7) if_3#(pair(m, zs), x, ys) => msort#(zs) | m = m /\ 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 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, i, c) ; D3 = (P3, R, i, c) }, where:

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

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

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

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

Processor output: { D4 = (P3, R2, i, c) }, where:

  R2. (1) if_1(pair(m, zh), x, y, zs) -> pair(x, ins(m, zh)) | m > x /\ y = y
      (2) if_2(pair(m, zh), x, y, zs) -> pair(m, ins(x, zh)) | x >= m /\ y = y
      (3) min(x, e) -> pair(x, e) | x = x
      (4) min(x, ins(y, zs)) -> if_1(min(y, zs), x, y, zs) | x = x /\ y = y
      (5) min(x, ins(y, zs)) -> if_2(min(y, zs), x, y, zs) | x = x /\ y = y

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

Constrained HORPO yields:

  msort#(ins(x, ys)) (>) if_3#(min(x, ys), x, ys) | x = x
  if_3#(pair(m, zs), x, ys) (>) msort#(zs) | m = m /\ x = x
  if_1(pair(m, zh), x, y, zs) (>=) pair(x, ins(m, zh)) | m > x /\ y = y
  if_2(pair(m, zh), x, y, zs) (>=) pair(m, ins(x, zh)) | x >= m /\ y = y
  min(x, e) (>=) pair(x, e) | x = x
  min(x, ins(y, zs)) (>=) if_1(min(y, zs), x, y, zs) | x = x /\ y = y
  min(x, ins(y, zs)) (>=) if_2(min(y, zs), x, y, zs) | x = x /\ y = y

We do this using the following settings:

* Disregarded arguments:

  if_2  3 
  if_3# 2 

* Precedence and permutation:

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

* Well-founded theory orderings:

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

All dependency pairs were removed.

Processor output: { }.