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

  Signature: 0 :: d
             f :: a -> a
             g :: (b -> d -> e) -> b -> e -> f
             s :: c -> e

  Rules: f(X) -> X
         g(Z, U, s(V)) -> g(Z, U, Z(U, 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 UNION R_?, i, c), where:

  P1. (1) g#(Z, U, s(V)) => g#(Z, U, Z(U, 0))

***** No progress could be made on DP problem D1 = (P1, R UNION R_?, i, c).