We consider universal computability of the MSTRS with no additional rule schemes:

  Signature: 0    :: Nat
             app  :: List -> List -> List
             cons :: Nat -> List -> List
             nil  :: List
             s    :: Nat -> Nat

  Rules: app(nil, ys) -> ys
         app(cons(x, xs), ys) -> cons(x, app(xs, ys))

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 UNION R_?, i, c), where:

  P1. (1) app#(cons(x, xs), ys) => app#(xs, ys)

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

We use the following projection function:

  nu(app#) = 1

We thus have:

  (1) cons(x, xs) |>| xs

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

Processor output: { }.