Consider the TRS R consisting of the rewrite rule

1: app(app(app(compose,f),g),x) -> app(f,app(g,x))

There are 2 dependency pairs:

2: APP(app(app(compose,f),g),x) -> APP(f,app(g,x))
3: APP(app(app(compose,f),g),x) -> APP(g,x)

Consider the SCC {2,3}.
By taking the polynomial interpretation
[compose] = 1
and [app](x,y) = [APP](x,y) = x + y + 1,
the rules in {1-3}
are strictly decreasing.
Hence the TRS is terminating.