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)  sort#(l) => st#(0, l)
      (2)  st#(n, l) => stNat#(n >= 0, n, l)
      (3)  stNat#(true, n, l) => member#(n, l)
      (4)  stNat#(true, n, l) => cond1#(member(n, l), n, l)
      (5)  cond1#(true, n, l) => st#(n + 1, l)
      (6)  cond1#(false, n, l) => max#(l)
      (7)  cond1#(false, n, l) => cond2#(n > max(l), n, l)
      (8)  cond2#(false, n, l) => st#(n + 1, l)
      (9)  member#(n, cons(m, l)) => member#(n, l)
      (10) max#(cons(u, l)) => max#(l)
      (11) max#(cons(u, l)) => max#(l)
      (12) max#(cons(u, l)) => if#(u > max(l), u, max(l))

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

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

  P2. (1) member#(n, cons(m, l)) => member#(n, l)

  P3. (1) max#(cons(u, l)) => max#(l)
      (2) max#(cons(u, l)) => max#(l)

  P4. (1) st#(n, l) => stNat#(n >= 0, n, l)
      (2) stNat#(true, n, l) => cond1#(member(n, l), n, l)
      (3) cond1#(true, n, l) => st#(n + 1, l)

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

We use the following projection function:

  nu(member#) = 2

We thus have:

  (1) cons(m, l) |>| l

All DPs are strictly oriented, and may be removed.  Hence, this DP problem is finite.

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

We use the following projection function:

  nu(max#) = 1

We thus have:

  (1) cons(u, l) |>| l
  (2) cons(u, l) |>| l

All DPs are strictly oriented, and may be removed.  Hence, this DP problem is finite.

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

We use the following theory arguments function:

  cond1# : [2]
  st#    : [1]
  stNat# : [1, 2]

This yields the following new DP problems:

  P5. (1) st#(n, l) => stNat#(n >= 0, n, l)
      (2) stNat#(true, n, l) => cond1#(member(n, l), n, l) { n }
      (3) cond1#(true, n, l) => st#(n + 1, l) { n }

  P6. (1) stNat#(true, n, l) => cond1#(member(n, l), n, l)
      (2) cond1#(true, n, l) => st#(n + 1, l)

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

We use the following theory arguments function:

  cond1# : [2]
  st#    : [1]
  stNat# : [1, 2]

This yields the following new DP problems:

  P7. (1) st#(n, l) => stNat#(n >= 0, n, l) { n }
      (2) stNat#(true, n, l) => cond1#(member(n, l), n, l) { n }
      (3) cond1#(true, n, l) => st#(n + 1, l) { n }

  P8. (1) st#(n, l) => stNat#(n >= 0, n, l)

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

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

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