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 Usable rules with respect to an argument wiltering [with HORPO] Processor on D4 = (P3, R2, i, c).

Constrained HORPO yields:

  msort#1(ins2(x, ys)) (>) if_3#3(min2(x, ys), x, ys) | x = x
  if_3#3(pair2(m, zs), x, ys) (>) msort#1(zs) | m = m /\ x = x
  if_14(pair2(m, zh), x, y, zs) (>=) pair2(x, ins2(m, zh)) | m > x /\ y = y
  if_24(pair2(m, zh), x, y, zs) (>=) pair2(m, ins2(x, zh)) | x >= m /\ y = y
  min2(x, e0) (>=) pair2(x, e0) | x = x
  min2(x, ins2(y, zs)) (>=) if_14(min2(y, zs), x, y, zs) | x = x /\ y = y
  min2(x, ins2(y, zs)) (>=) if_24(min2(y, zs), x, y, zs) | x = x /\ y = y

We do this using the following settings:

* Disregarded arguments:

  if_3#3 2 
  min2   1 

* Precedence and permutation:

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

* Well-founded theory orderings:

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

Processor output: { }.