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

  Signature: minus :: N -> N -> N
             s     :: N -> N
             z     :: N

  Rules: minus(z, X) -> z
         minus(Y, z) -> Y
         minus(s(U), s(V)) -> minus(U, V)
         minus(W, W) -> z

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) minus#(s(U), s(V)) => minus#(U, V)

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

We use the following projection function:

  nu(minus#) = 1

We thus have:

  (1) s(U) |>| U

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

Processor output: { }.