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,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: s(X) -> n__s(X)
16: activate(n__from(X)) -> from(activate(X))
17: activate(n__s(X)) -> s(activate(X))
18: activate(X) -> X

There are 19 dependency pairs:

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

The approximated dependency graph contains 4 SCCs:
{35,37},
{19,21,23,25},
{30}
and {32}.

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

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

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

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

Hence the TRS is terminating.