Consider the TRS R consisting of the rewrite rules

1: from(X) -> cons(X,n__from(s(X)))
2: 2ndspos(0,Z) -> rnil
3: 2ndspos(s(N),cons(X,Z)) -> 2ndspos(s(N),cons2(X,activate(Z)))
4: 2ndspos(s(N),cons2(X,cons(Y,Z))) -> rcons(posrecip(Y),2ndsneg(N,activate(Z)))
5: 2ndsneg(0,Z) -> rnil
6: 2ndsneg(s(N),cons(X,Z)) -> 2ndsneg(s(N),cons2(X,activate(Z)))
7: 2ndsneg(s(N),cons2(X,cons(Y,Z))) -> rcons(negrecip(Y),2ndspos(N,activate(Z)))
8: pi(X) -> 2ndspos(X,from(0))
9: plus(0,Y) -> Y
10: plus(s(X),Y) -> s(plus(X,Y))
11: times(0,Y) -> 0
12: times(s(X),Y) -> plus(Y,times(X,Y))
13: square(X) -> times(X,X)
14: from(X) -> n__from(X)
15: activate(n__from(X)) -> from(X)
16: activate(X) -> X

There are 15 dependency pairs:

17: 2ndspos#(s(N),cons(X,Z)) -> 2ndspos#(s(N),cons2(X,activate(Z)))
18: 2ndspos#(s(N),cons(X,Z)) -> ACTIVATE(Z)
19: 2ndspos#(s(N),cons2(X,cons(Y,Z))) -> 2ndsneg#(N,activate(Z))
20: 2ndspos#(s(N),cons2(X,cons(Y,Z))) -> ACTIVATE(Z)
21: 2ndsneg#(s(N),cons(X,Z)) -> 2ndsneg#(s(N),cons2(X,activate(Z)))
22: 2ndsneg#(s(N),cons(X,Z)) -> ACTIVATE(Z)
23: 2ndsneg#(s(N),cons2(X,cons(Y,Z))) -> 2ndspos#(N,activate(Z))
24: 2ndsneg#(s(N),cons2(X,cons(Y,Z))) -> ACTIVATE(Z)
25: PI(X) -> 2ndspos#(X,from(0))
26: PI(X) -> FROM(0)
27: PLUS(s(X),Y) -> PLUS(X,Y)
28: TIMES(s(X),Y) -> PLUS(Y,times(X,Y))
29: TIMES(s(X),Y) -> TIMES(X,Y)
30: SQUARE(X) -> TIMES(X,X)
31: ACTIVATE(n__from(X)) -> FROM(X)

The approximated dependency graph contains 3 SCCs:
{27},
{29}
and {17,19,21,23}.

- 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 {29}.
There are no usable rules.
By taking the polynomial interpretation
[s](x) = x + 1
and [TIMES](x,y) = x + y + 1,
rule 29
is strictly decreasing.

- Consider the SCC {17,19,21,23}.
The usable rules are {1,14-16}.
By taking the polynomial interpretation
[n__from](x) = x,
[2ndsneg#](x,y) = [2ndspos#](x,y) = [activate](x) = [from](x) = [s](x) = x + 1,
[cons2](x,y) = x + y + 1
and [cons](x,y) = y,
the rules in {1,15,17,21}
are weakly decreasing and
the rules in {14,16,19,23}
are strictly decreasing.

Hence the TRS is terminating.