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

  Signature: 0 :: nat
             1 :: nat
             f :: nat -> (nat -> nat) -> nat

  Rules: f(0, F) -> F(f(F(1), F))

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) f#(0, F) => f#(F(1), F)

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