Consider the TRS R consisting of the rewrite rules

1: exp(x,0) -> s(0)
2: exp(x,s(y)) -> x * exp(x,y)
3: 0 * y -> 0
4: s(x) * y -> y + (x * y)
5: 0 - y -> 0
6: x - 0 -> x
7: s(x) - s(y) -> x - y

There are 4 dependency pairs:

8: EXP(x,s(y)) -> x *# exp(x,y)
9: EXP(x,s(y)) -> EXP(x,y)
10: s(x) *# y -> x *# y
11: s(x) -# s(y) -> x -# y

The approximated dependency graph contains 3 SCCs:
{10},
{11}
and {9}.

- Consider the SCC {10}.
There are no usable rules.
By taking the polynomial interpretation
[s](x) = x + 1
and [*#](x,y) = x + y + 1,
rule 10
is strictly decreasing.

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

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

Hence the TRS is terminating.