Consider the TRS R consisting of the rewrite rules

1: div(0,y) -> 0
2: div(x,y) -> quot(x,y,y)
3: quot(0,s(y),z) -> 0
4: quot(s(x),s(y),z) -> quot(x,y,z)
5: quot(x,0,s(z)) -> s(div(x,s(z)))

There are 3 dependency pairs:

6: DIV(x,y) -> QUOT(x,y,y)
7: QUOT(s(x),s(y),z) -> QUOT(x,y,z)
8: QUOT(x,0,s(z)) -> DIV(x,s(z))

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

- Consider the SCC {6-8}.
There are no usable rules.
By taking the polynomial interpretation
[0] = 1,
[s](x) = x + 1,
[DIV](x,y) = x + y + 1
and [QUOT](x,y,z) = x + z + 1,
the rules in {6,8}
are weakly decreasing and
rule 7
is strictly decreasing.
There is one new SCC.

- Consider the SCC {6,8}.
By taking the polynomial interpretation
[s](x) = 0,
[0] = 1
and [DIV](x,y) = [QUOT](x,y,z) = x + y + 1,
rule 6
is weakly decreasing and
rule 8
is strictly decreasing.


Hence the TRS is terminating.