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

  Signature: bar :: (o -> o) -> o
             foo :: o -> o

  Rules: foo(bar(F)) -> F(bar(F))

The system does not satisfy the preconditions to apply static dependency pairs: it is not accessible function passing.

No HORPO proof could be found.