We consider universal computability 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 UNION 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 UNION 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 UNION R_?, f, c) ; D3 = (P3, R UNION 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 UNION 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 UNION R_?, f, c).

We use the following theory arguments function:

  if_3#  : [2]
  msort# : []

Processor output: { D4 = (P4, R UNION R_?, f, c) ; D5 = (P5, R UNION 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)

***** No progress could be made on DP problem D4 = (P4, R UNION R_?, f, c).