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

  Signature: cons    :: nat -> list -> list
             iterate :: (nat -> nat) -> nat -> list
             nil     :: list
             suc     :: nat -> nat
             zero    :: nat

  Rules: iterate(f, x) -> cons(x, iterate(f, f(x)))

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) iterate#(f, x) => iterate#(f, f(x))

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