Consider the TRS R consisting of the rewrite rules

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

There are 4 dependency pairs:

6: QUOT(s(x),s(y),z) -> QUOT(x,y,z)
7: PLUS(s(x),y) -> PLUS(x,y)
8: QUOT(x,0,s(z)) -> QUOT(x,plus(z,s(0)),s(z))
9: QUOT(x,0,s(z)) -> PLUS(z,s(0))

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

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

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

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


Hence the TRS is terminating.