The system is accessible function passing by a sort ordering with b = c ≻ a.

We start by computing the following initial DP problem:

  P1. (1) map#(Z, cons(U, V)) => map#(Z, V)
      (2) sum#(cons(W, P)) => sum#(P)
      (3) sum#(cons(W, P)) => plus#(W, sum(P))
      (4) size#(node(X1, Y1)) => size#(X{11})
      (5) size#(node(X1, Y1)) => map#(size, Y1)
      (6) size#(node(X1, Y1)) => sum#(map(size, Y1))
      (7) plus#(s(V1), W1) => plus#(V1, W1)

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

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

  P2. (1) map#(Z, cons(U, V)) => map#(Z, V)

  P3. (1) plus#(s(V1), W1) => plus#(V1, W1)

  P4. (1) sum#(cons(W, P)) => sum#(P)

  P5. (1) size#(node(X1, Y1)) => size#(X{11})

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

We use the following projection function:

  nu(map#) = 2

We thus have:

  (1) cons(U, V) |>| V

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(plus#) = 1

We thus have:

  (1) s(V1) |>| V1

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

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

We use the following projection function:

  nu(sum#) = 1

We thus have:

  (1) cons(W, P) |>| P

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

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