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

  Signature: dom  :: N -> N -> N -> N
             eval :: N -> N -> N
             fun  :: (N -> N) -> N -> N -> N
             o    :: N
             s    :: N -> N

  Rules: eval(fun(F, X, Y), Z) -> F(dom(X, Y, Z))
         dom(s(X), s(Y), s(Z)) -> s(dom(X, Y, Z))
         dom(o, s(Y), s(Z)) -> s(dom(o, Y, Z))
         dom(X, Y, o) -> X
         dom(o, o, Z) -> o

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

No HORPO proof could be found.