We consider termination of the STRS with no additional rule schemes:

  Signature: 0     :: c
             add   :: a -> c -> c
             cons  :: a -> b -> b
             fold  :: (a -> c -> c) -> c -> b -> c
             mul   :: a -> c -> c
             nil   :: b
             plus  :: c -> c -> c
             prod  :: b -> c
             s     :: c -> c
             sum   :: b -> c
             times :: c -> c -> c

  Rules: fold(F, Y, nil) -> Y
         fold(G, V, cons(W, P)) -> G(W, fold(G, V, P))
         plus(0, X1) -> X1
         plus(s(Y1), U1) -> s(plus(Y1, U1))
         times(0, V1) -> 0
         times(s(W1), P1) -> plus(times(W1, P1), P1)
         sum -> fold(add, 0)
         prod -> fold(mul, s(0))

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

We start by computing the initial DP problem D1 = (P1, R, i, c), where:

  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#(arg1) => fold#(add, 0, arg1)
      (6) prod#(arg1) => fold#(mul, s(0), arg1)

***** We apply the Graph Processor on D1 = (P1, R, i, c).

We compute a graph approximation with the following edges:

  1: 1 
  2: 2 
  3: 3 4 
  4: 2 
  5: 1 
  6: 1 

There are 3 SCCs.

Processor output: { D2 = (P2, R, i, c) ; D3 = (P3, R, i, c) ; D4 = (P4, R, i, c) }, where:

  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 D2 = (P2, R, i, c).

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.

Processor output: { }.

***** We apply the Subterm Criterion Processor on D3 = (P3, R, i, c).

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.

Processor output: { }.

***** We apply the Subterm Criterion Processor on D4 = (P4, R, i, c).

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.

Processor output: { }.