Consider the TRS R consisting of the rewrite rules

1: minus(x,0) -> x
2: minus(s(x),s(y)) -> minus(x,y)
3: quot(0,s(y)) -> 0
4: quot(s(x),s(y)) -> s(quot(minus(x,y),s(y)))
5: plus(0,y) -> y
5: plus(0,y) -> y
6: plus(s(x),y) -> s(plus(x,y))
6: plus(s(x),y) -> s(plus(x,y))
7: minus(minus(x,y),z) -> minus(x,plus(y,z))
8: app(nil,k) -> k
9: app(l,nil) -> l
10: app(cons(x,l),k) -> cons(x,app(l,k))
11: sum(cons(x,nil)) -> cons(x,nil)
12: sum(cons(x,cons(y,l))) -> sum(cons(plus(x,y),l))
13: sum(app(l,cons(x,cons(y,k)))) -> sum(app(l,sum(cons(x,cons(y,k)))))

There are 12 dependency pairs:

16: MINUS(s(x),s(y)) -> MINUS(x,y)
17: QUOT(s(x),s(y)) -> QUOT(minus(x,y),s(y))
18: QUOT(s(x),s(y)) -> MINUS(x,y)
19: MINUS(minus(x,y),z) -> MINUS(x,plus(y,z))
20: MINUS(minus(x,y),z) -> PLUS(y,z)
21: APP(cons(x,l),k) -> APP(l,k)
22: SUM(cons(x,cons(y,l))) -> SUM(cons(plus(x,y),l))
23: SUM(cons(x,cons(y,l))) -> PLUS(x,y)
24: SUM(app(l,cons(x,cons(y,k)))) -> SUM(app(l,sum(cons(x,cons(y,k)))))
25: SUM(app(l,cons(x,cons(y,k)))) -> APP(l,sum(cons(x,cons(y,k))))
26: SUM(app(l,cons(x,cons(y,k)))) -> SUM(cons(x,cons(y,k)))
27: PLUS(s(x),y) -> PLUS(x,y)

The approximated dependency graph contains 6 SCCs:
{21},
{27},
{16,19},
{17},
{22}
and {24}.

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

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

- Consider the SCC {16,19}.
The usable rules are {5,6}.
By taking the polynomial interpretation
[0] = 1,
[s](x) = x + 1
and [minus](x,y) = [MINUS](x,y) = [plus](x,y) = x + y + 1,
the rules in {6,19}
are weakly decreasing and
the rules in {5,16}
are strictly decreasing.
There is one new SCC.

- Consider the SCC {19}.
By taking the polynomial interpretation
[0] = 1,
[MINUS](x,y) = [s](x) = x + 1
and [minus](x,y) = [plus](x,y) = x + y + 1,
rule 6
is weakly decreasing and
the rules in {5,19}
are strictly decreasing.


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

- Consider the SCC {22}.
The usable rules are {5,6}.
By taking the polynomial interpretation
[0] = 1,
[s](x) = [SUM](x) = x + 1,
[plus](x,y) = x + y + 1
and [cons](x,y) = y + 1,
rule 6
is weakly decreasing and
the rules in {5,22}
are strictly decreasing.

- Consider the SCC {24}.
The usable rules are {5,6,8-13}.
By taking the polynomial interpretation
[nil] = 0,
[0] = [sum](x) = 1,
[s](x) = [SUM](x) = x + 1,
[app](x,y) = [plus](x,y) = x + y + 1
and [cons](x,y) = y + 1,
the rules in {6,10-13}
are weakly decreasing and
the rules in {5,8,9,24}
are strictly decreasing.

Hence the TRS is terminating.