We consider termination of the LCSTRS with only rule scheme Calc:

  Signature: app :: o -> o -> o
             lam :: (o -> o) -> o

  Rules: app(lam(F), X) -> F(X)

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

No HORPO proof could be found.