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

We use the following theory arguments function:

  if_3#  : [2]
  msort# : []

Processor output: { D4 = (P4, R, i, c) ; D5 = (P5, R, i, 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 = x

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

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

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

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

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

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

We compute a graph approximation with the following edges:

  1:

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

Processor output: { }.

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

Constrained HORPO yields:

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

We do this using the following settings:

* Disregarded arguments:

  if_14 2 
  if_24 2 

* Precedence and permutation:

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

* Well-founded theory orderings:

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

Processor output: { }.