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,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: cons(X1,X2) -> n__cons(X1,X2)
14: activate(n__from(X)) -> from(X)
15: activate(n__cons(X1,X2)) -> cons(X1,X2)
16: activate(X) -> X

There are 15 dependency pairs:

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

The approximated dependency graph contains 3 SCCs:
{26},
{28}
and {19,22}.

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

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

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

Hence the TRS is terminating.