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) max#(cons(x, cons(y, xs))) => if1#(x >= y, x, y, xs)
      (2) if1#(true, x, y, xs) => max#(cons(x, xs))
      (3) if1#(false, x, y, xs) => max#(cons(y, xs))
      (4) del#(x, cons(y, xs)) => if2#(x = y, x, y, xs)
      (5) if2#(false, x, y, xs) => del#(x, xs)
      (6) sort#(cons(x, xs)) => max#(cons(x, xs))
      (7) sort#(cons(x, xs)) => max#(cons(x, xs))
      (8) sort#(cons(x, xs)) => del#(max(cons(x, xs)), cons(x, xs))
      (9) sort#(cons(x, xs)) => sort#(del(max(cons(x, xs)), cons(x, xs)))

***** We apply the Graph Processor on P1.

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

  P2. (1) max#(cons(x, cons(y, xs))) => if1#(x >= y, x, y, xs)
      (2) if1#(true, x, y, xs) => max#(cons(x, xs))
      (3) if1#(false, x, y, xs) => max#(cons(y, xs))

  P3. (1) del#(x, cons(y, xs)) => if2#(x = y, x, y, xs)
      (2) if2#(false, x, y, xs) => del#(x, xs)

  P4. (1) sort#(cons(x, xs)) => sort#(del(max(cons(x, xs)), cons(x, xs)))

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

We use the following theory arguments function:

  sort# : []

This yields the following new DP problems:

  P5. (1) max#(cons(x, cons(y, xs))) => if1#(x >= y, x, y, xs)
      (2) if1#(true, x, y, xs) => max#(cons(x, xs)) { x, y }
      (3) if1#(false, x, y, xs) => max#(cons(y, xs)) { x, y }

  P6. (1) if1#(true, x, y, xs) => max#(cons(x, xs))
      (2) if1#(false, x, y, xs) => max#(cons(y, xs))

***** We apply the Subterm Criterion Processor on P3.

We use the following projection function:

  nu(del#) = 2
  nu(if2#) = 4

We thus have:

  (1) cons(y, xs) |>|  xs
  (2) xs          |>=| xs

We may remove the strictly oriented DPs, which yields:

  P7. (1) if2#(false, x, y, xs) => del#(x, xs)

***** No progress could be made on DP problem P4.