Consider the TRS R consisting of the rewrite rule

1: app(app(apply,f),x) -> app(f,x)

There is one dependency pair:

2: APP(app(apply,f),x) -> APP(f,x)

The approximated dependency graph contains one SCC:
{2}.

- Consider the SCC {2}.
There are no usable rules.
By taking the polynomial interpretation
[apply] = 1
and [app](x,y) = [APP](x,y) = x + y + 1,
rule 2
is strictly decreasing.

Hence the TRS is terminating.