Consider the TRS R consisting of the rewrite rules

1: div(X,e) -> i(X)
2: i(div(X,Y)) -> div(Y,X)
3: div(div(X,Y),Z) -> div(Y,div(i(X),Z))

There are 5 dependency pairs:

4: DIV(X,e) -> I(X)
5: I(div(X,Y)) -> DIV(Y,X)
6: DIV(div(X,Y),Z) -> DIV(Y,div(i(X),Z))
7: DIV(div(X,Y),Z) -> DIV(i(X),Z)
8: DIV(div(X,Y),Z) -> I(X)

The approximated dependency graph contains one SCC:
{4-8}.

- Consider the SCC {4-8}.
By taking the polynomial interpretation
[e] = 1,
[i](x) = x,
[I](x) = x + 1
and [div](x,y) = [DIV](x,y) = x + y + 1,
the rules in {2,3,6}
are weakly decreasing and
the rules in {1,4,5,7,8}
are strictly decreasing.
There is one new SCC.

- Consider the SCC {6}.
By taking the polynomial interpretation
[e] = 1,
[i](x) = x,
[DIV](x,y) = x + 1
and [div](x,y) = x + y + 1,
the rules in {2,3}
are weakly decreasing and
the rules in {1,6}
are strictly decreasing.


Hence the TRS is terminating.