Consider the TRS R consisting of the rewrite rules

1: from(X) -> cons(X,n__from(n__s(X)))
2: sel(0,cons(X,XS)) -> X
3: sel(s(N),cons(X,XS)) -> sel(N,activate(XS))
4: minus(X,0) -> 0
5: minus(s(X),s(Y)) -> minus(X,Y)
6: quot(0,s(Y)) -> 0
7: quot(s(X),s(Y)) -> s(quot(minus(X,Y),s(Y)))
8: zWquot(XS,nil) -> nil
9: zWquot(nil,XS) -> nil
10: zWquot(cons(X,XS),cons(Y,YS)) -> cons(quot(X,Y),n__zWquot(activate(XS),activate(YS)))
11: from(X) -> n__from(X)
12: s(X) -> n__s(X)
13: zWquot(X1,X2) -> n__zWquot(X1,X2)
14: activate(n__from(X)) -> from(activate(X))
15: activate(n__s(X)) -> s(activate(X))
16: activate(n__zWquot(X1,X2)) -> zWquot(activate(X1),activate(X2))
17: activate(X) -> X

There are 16 dependency pairs:

18: SEL(s(N),cons(X,XS)) -> SEL(N,activate(XS))
19: SEL(s(N),cons(X,XS)) -> ACTIVATE(XS)
20: MINUS(s(X),s(Y)) -> MINUS(X,Y)
21: QUOT(s(X),s(Y)) -> S(quot(minus(X,Y),s(Y)))
22: QUOT(s(X),s(Y)) -> QUOT(minus(X,Y),s(Y))
23: QUOT(s(X),s(Y)) -> MINUS(X,Y)
24: ZWQUOT(cons(X,XS),cons(Y,YS)) -> QUOT(X,Y)
25: ZWQUOT(cons(X,XS),cons(Y,YS)) -> ACTIVATE(XS)
26: ZWQUOT(cons(X,XS),cons(Y,YS)) -> ACTIVATE(YS)
27: ACTIVATE(n__from(X)) -> FROM(activate(X))
28: ACTIVATE(n__from(X)) -> ACTIVATE(X)
29: ACTIVATE(n__s(X)) -> S(activate(X))
30: ACTIVATE(n__s(X)) -> ACTIVATE(X)
31: ACTIVATE(n__zWquot(X1,X2)) -> ZWQUOT(activate(X1),activate(X2))
32: ACTIVATE(n__zWquot(X1,X2)) -> ACTIVATE(X1)
33: ACTIVATE(n__zWquot(X1,X2)) -> ACTIVATE(X2)

The approximated dependency graph contains 4 SCCs:
{20},
{22},
{25,26,28,30-33}
and {18}.

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

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

- Consider the SCC {25,26,28,30-33}.
The usable rules are {1,4-17}.
By taking the polynomial interpretation
[0] = [nil] = 1,
[activate](x) = [n__s](x) = [s](x) = x,
[ACTIVATE](x) = [from](x) = [n__from](x) = x + 1,
[minus](x,y) = [n__zWquot](x,y) = [zWquot](x,y) = [ZWQUOT](x,y) = x + y + 1,
[cons](x,y) = y
and [quot](x,y) = y + 1,
the rules in {1,5-7,10-17,25,26,30}
are weakly decreasing and
the rules in {4,8,9,28,31-33}
are strictly decreasing.
There is one new SCC.

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


- Consider the SCC {18}.
The usable rules are {1,4-17}.
By taking the polynomial interpretation
[0] = 0,
[nil] = 1,
[activate](x) = [minus](x,y) = x,
[cons](x,y) = [from](x) = [n__from](x) = [n__s](x) = [s](x) = [SEL](x,y) = x + 1
and [n__zWquot](x,y) = [quot](x,y) = [zWquot](x,y) = x + y + 1,
the rules in {1,4,7,11-17}
are weakly decreasing and
the rules in {5,6,8-10,18}
are strictly decreasing.

Hence the TRS is terminating.