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) fold#(G, V, cons(W, P)) => fold#(G, V, P)
      (2) plus#(s(Y1), U1) => plus#(Y1, U1)
      (3) times#(s(W1), P1) => times#(W1, P1)
      (4) times#(s(W1), P1) => plus#(times(W1, P1), P1)
      (5) sum#(X{12}) => fold#(add, 0, X{12})
      (6) prod#(X{13}) => fold#(mul, s(0), X{13})

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

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

  P2. (1) fold#(G, V, cons(W, P)) => fold#(G, V, P)

  P3. (1) plus#(s(Y1), U1) => plus#(Y1, U1)

  P4. (1) times#(s(W1), P1) => times#(W1, P1)

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

We use the following projection function:

  nu(fold#) = 3

We thus have:

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

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(Y1) |>| Y1

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

We thus have:

  (1) s(W1) |>| W1

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