The system is accessible function passing by a sort ordering that equates all sorts.

We start by computing the following initial DP problem:

  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 P1.

Considering the 2 SCCs, this DP problem is split into the following new problems.

  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 P2.

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.

***** We apply the Theory Arguments Processor on P3.

We use the following theory arguments function:

  if_3#  : [2]
  msort# : []

This yields the following new DP problems:

  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 P4.