Consider the TRS R consisting of the rewrite rules

1: app(id,x) -> x
2: app(plus,0) -> id
3: app(app(plus,app(s,x)),y) -> app(s,app(app(plus,x),y))

There are 3 dependency pairs:

4: APP(app(plus,app(s,x)),y) -> APP(s,app(app(plus,x),y))
5: APP(app(plus,app(s,x)),y) -> APP(app(plus,x),y)
6: APP(app(plus,app(s,x)),y) -> APP(plus,x)

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

- Consider the SCC {5}.
By taking the polynomial interpretation
[0] = [id] = [plus] = [s] = 1
and [app](x,y) = [APP](x,y) = x + y + 1,
rule 3
is weakly decreasing and
the rules in {1,2,5}
are strictly decreasing.

Hence the TRS is terminating.