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

  Signature: cons    :: a -> b -> b
             iterate :: (a -> a) -> a -> b

  Rules: iterate(F, Y) -> cons(Y, iterate(F, F(Y)))

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) iterate#(F, Y) => iterate#(F, F(Y))

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