Consider the TRS R consisting of the rewrite rules

1: x - 0 -> x
2: s(x) - s(y) -> x - y
3: p(s(x)) -> x
4: f(s(x),y) -> f(p(s(x) - y),p(y - s(x)))
5: f(x,s(y)) -> f(p(x - s(y)),p(s(y) - x))

There are 11 dependency pairs:

6: s(x) -# s(y) -> x -# y
7: F(s(x),y) -> F(p(s(x) - y),p(y - s(x)))
8: F(s(x),y) -> P(s(x) - y)
9: F(s(x),y) -> s(x) -# y
10: F(s(x),y) -> P(y - s(x))
11: F(s(x),y) -> y -# s(x)
12: F(x,s(y)) -> F(p(x - s(y)),p(s(y) - x))
13: F(x,s(y)) -> P(x - s(y))
14: F(x,s(y)) -> x -# s(y)
15: F(x,s(y)) -> P(s(y) - x)
16: F(x,s(y)) -> s(y) -# x

The approximated dependency graph contains 2 SCCs:
{6}
and {7,12}.

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

- Consider the SCC {7,12}.
The usable rules are {1-3}.
By taking the polynomial interpretation
[0] = s,
[-](x,y) = [F](x,y) = x,
[s](x) = x + 1
and [p](x) = x - 1,
we obtain a quasi-model of the usable rules.
Furthermore, dependency pair 12
is weakly decreasing and
dependency pair 7
is strictly decreasing.
There is one new SCC.

- Consider the SCC {12}.
By taking the polynomial interpretation
[0] = s,
[-](x,y) = x,
[s](x) = x + 1,
[p](x) = x - 1
and [F](x,y) = y,
we obtain a quasi-model of the usable rules.
Furthermore, dependency pair 12
is strictly decreasing.


Hence the TRS is terminating.