Consider the TRS R consisting of the rewrite rules

1: app(app(plus,0),y) -> y
2: app(app(plus,app(s,x)),y) -> app(s,app(app(plus,x),y))
3: app(app(app(curry,f),x),y) -> app(app(f,x),y)
4: add -> app(curry,plus)

There are 6 dependency pairs:

5: APP(app(plus,app(s,x)),y) -> APP(s,app(app(plus,x),y))
6: APP(app(plus,app(s,x)),y) -> APP(app(plus,x),y)
7: APP(app(plus,app(s,x)),y) -> APP(plus,x)
8: APP(app(app(curry,f),x),y) -> APP(app(f,x),y)
9: APP(app(app(curry,f),x),y) -> APP(f,x)
10: ADD -> APP(curry,plus)

The approximated dependency graph contains one SCC:
{6,8,9}.

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

Hence the TRS is terminating.