Consider the TRS R consisting of the rewrite rules

1: plus(0,Y) -> Y
2: plus(s(X),Y) -> s(plus(X,Y))
3: min(X,0) -> X
4: min(s(X),s(Y)) -> min(X,Y)
5: min(min(X,Y),Z) -> min(X,plus(Y,Z))
6: quot(0,s(Y)) -> 0
7: quot(s(X),s(Y)) -> s(quot(min(X,Y),s(Y)))

There are 6 dependency pairs:

8: PLUS(s(X),Y) -> PLUS(X,Y)
9: MIN(s(X),s(Y)) -> MIN(X,Y)
10: MIN(min(X,Y),Z) -> MIN(X,plus(Y,Z))
11: MIN(min(X,Y),Z) -> PLUS(Y,Z)
12: QUOT(s(X),s(Y)) -> QUOT(min(X,Y),s(Y))
13: QUOT(s(X),s(Y)) -> MIN(X,Y)

The approximated dependency graph contains 3 SCCs:
{8},
{9,10}
and {12}.

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

- Consider the SCC {9,10}.
The usable rules are {1,2}.
By taking the polynomial interpretation
[0] = [Z] = 1,
[s](x) = x + 1
and [min](x,y) = [MIN](x,y) = [plus](x,y) = x + y + 1,
the rules in {2,10}
are weakly decreasing and
the rules in {1,9}
are strictly decreasing.
There is one new SCC.

- Consider the SCC {10}.
By taking the polynomial interpretation
[0] = [Z] = 1,
[MIN](x,y) = [s](x) = x + 1
and [min](x,y) = [plus](x,y) = x + y + 1,
rule 2
is weakly decreasing and
the rules in {1,10}
are strictly decreasing.


- Consider the SCC {12}.
The usable rules are {1-5}.
By taking the polynomial interpretation
[0] = [Z] = 1,
[min](x,y) = x,
[s](x) = x + 1
and [plus](x,y) = [QUOT](x,y) = x + y + 1,
the rules in {2,3,5}
are weakly decreasing and
the rules in {1,4,12}
are strictly decreasing.

Hence the TRS is terminating.