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

  Signature: 0   :: a
             rec :: (a -> b -> b) -> b -> a -> b
             s   :: a -> a

  Rules: rec(F, Y, 0) -> Y
         rec(G, V, s(W)) -> G(s(W), rec(G, V, W))

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) rec#(G, V, s(W)) => rec#(G, V, W)

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

We use the following projection function:

  nu(rec#) = 3

We thus have:

  (1) s(W) |>| W

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

Processor output: { }.