Consider the TRS R consisting of the rewrite rules

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

There are 20 dependency pairs:

19: FROM(X) -> CONS(X,n__from(n__s(X)))
20: 2ndspos#(s(N),cons(X,n__cons(Y,Z))) -> ACTIVATE(Y)
21: 2ndspos#(s(N),cons(X,n__cons(Y,Z))) -> 2ndsneg#(N,activate(Z))
22: 2ndspos#(s(N),cons(X,n__cons(Y,Z))) -> ACTIVATE(Z)
23: 2ndsneg#(s(N),cons(X,n__cons(Y,Z))) -> ACTIVATE(Y)
24: 2ndsneg#(s(N),cons(X,n__cons(Y,Z))) -> 2ndspos#(N,activate(Z))
25: 2ndsneg#(s(N),cons(X,n__cons(Y,Z))) -> ACTIVATE(Z)
26: PI(X) -> 2ndspos#(X,from(0))
27: PI(X) -> FROM(0)
28: PLUS(s(X),Y) -> S(plus(X,Y))
29: PLUS(s(X),Y) -> PLUS(X,Y)
30: TIMES(s(X),Y) -> PLUS(Y,times(X,Y))
31: TIMES(s(X),Y) -> TIMES(X,Y)
32: SQUARE(X) -> TIMES(X,X)
33: ACTIVATE(n__from(X)) -> FROM(activate(X))
34: ACTIVATE(n__from(X)) -> ACTIVATE(X)
35: ACTIVATE(n__s(X)) -> S(activate(X))
36: ACTIVATE(n__s(X)) -> ACTIVATE(X)
37: ACTIVATE(n__cons(X1,X2)) -> CONS(activate(X1),X2)
38: ACTIVATE(n__cons(X1,X2)) -> ACTIVATE(X1)

The approximated dependency graph contains 4 SCCs:
{34,36,38},
{21,24},
{29}
and {31}.

- Consider the SCC {34,36,38}.
There are no usable rules.
By taking the polynomial interpretation
[ACTIVATE](x) = [n__from](x) = [n__s](x) = x + 1
and [n__cons](x,y) = x + y + 1,
the rules in {34,36,38}
are strictly decreasing.

- Consider the SCC {21,24}.
The usable rules are {1,12-18}.
By taking the polynomial interpretation
[2ndsneg#](x,y) = [2ndspos#](x,y) = [activate](x) = [cons](x,y) = [from](x) = [n__cons](x,y) = [n__from](x) = [n__s](x) = [s](x) = x + 1,
the rules in {1,12-17}
are weakly decreasing and
the rules in {18,21,24}
are strictly decreasing.

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

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

Hence the TRS is terminating.