Consider the TRS R consisting of the rewrite rules

1: 0 + y -> y
2: s(x) + y -> s(x + y)
3: p(x) + y -> p(x + y)
4: minus(0) -> 0
5: minus(s(x)) -> p(minus(x))
6: minus(p(x)) -> s(minus(x))
7: 0 * y -> 0
8: s(x) * y -> (x * y) + y
9: p(x) * y -> (x * y) + minus(y)

There are 9 dependency pairs:

10: s(x) +# y -> x +# y
11: p(x) +# y -> x +# y
12: MINUS(s(x)) -> MINUS(x)
13: MINUS(p(x)) -> MINUS(x)
14: s(x) *# y -> (x * y) +# y
15: s(x) *# y -> x *# y
16: p(x) *# y -> (x * y) +# minus(y)
17: p(x) *# y -> x *# y
18: p(x) *# y -> MINUS(y)

The approximated dependency graph contains 3 SCCs:
{10,11},
{12,13}
and {15,17}.

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

- Consider the SCC {12,13}.
There are no usable rules.
By taking the polynomial interpretation
[MINUS](x) = [p](x) = [s](x) = x + 1,
the rules in {12,13}
are strictly decreasing.

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

Hence the TRS is terminating.