(VAR X Z N Y X1 X2)
(RULES 
active(from(X)) -> mark(cons(X,from(s(X))))
active(2ndspos(0,Z)) -> mark(rnil)
active(2ndspos(s(N),cons(X,Z))) -> mark(2ndspos(s(N),cons2(X,Z)))
active(2ndspos(s(N),cons2(X,cons(Y,Z)))) -> mark(rcons(posrecip(Y),2ndsneg(N,Z)))
active(2ndsneg(0,Z)) -> mark(rnil)
active(2ndsneg(s(N),cons(X,Z))) -> mark(2ndsneg(s(N),cons2(X,Z)))
active(2ndsneg(s(N),cons2(X,cons(Y,Z)))) -> mark(rcons(negrecip(Y),2ndspos(N,Z)))
active(pi(X)) -> mark(2ndspos(X,from(0)))
active(plus(0,Y)) -> mark(Y)
active(plus(s(X),Y)) -> mark(s(plus(X,Y)))
active(times(0,Y)) -> mark(0)
active(times(s(X),Y)) -> mark(plus(Y,times(X,Y)))
active(square(X)) -> mark(times(X,X))
mark(from(X)) -> active(from(mark(X)))
mark(cons(X1,X2)) -> active(cons(mark(X1),X2))
mark(s(X)) -> active(s(mark(X)))
mark(2ndspos(X1,X2)) -> active(2ndspos(mark(X1),mark(X2)))
mark(0) -> active(0)
mark(rnil) -> active(rnil)
mark(cons2(X1,X2)) -> active(cons2(X1,mark(X2)))
mark(rcons(X1,X2)) -> active(rcons(mark(X1),mark(X2)))
mark(posrecip(X)) -> active(posrecip(mark(X)))
mark(2ndsneg(X1,X2)) -> active(2ndsneg(mark(X1),mark(X2)))
mark(negrecip(X)) -> active(negrecip(mark(X)))
mark(pi(X)) -> active(pi(mark(X)))
mark(plus(X1,X2)) -> active(plus(mark(X1),mark(X2)))
mark(times(X1,X2)) -> active(times(mark(X1),mark(X2)))
mark(square(X)) -> active(square(mark(X)))
from(mark(X)) -> from(X)
from(active(X)) -> from(X)
cons(mark(X1),X2) -> cons(X1,X2)
cons(X1,mark(X2)) -> cons(X1,X2)
cons(active(X1),X2) -> cons(X1,X2)
cons(X1,active(X2)) -> cons(X1,X2)
s(mark(X)) -> s(X)
s(active(X)) -> s(X)
2ndspos(mark(X1),X2) -> 2ndspos(X1,X2)
2ndspos(X1,mark(X2)) -> 2ndspos(X1,X2)
2ndspos(active(X1),X2) -> 2ndspos(X1,X2)
2ndspos(X1,active(X2)) -> 2ndspos(X1,X2)
cons2(mark(X1),X2) -> cons2(X1,X2)
cons2(X1,mark(X2)) -> cons2(X1,X2)
cons2(active(X1),X2) -> cons2(X1,X2)
cons2(X1,active(X2)) -> cons2(X1,X2)
rcons(mark(X1),X2) -> rcons(X1,X2)
rcons(X1,mark(X2)) -> rcons(X1,X2)
rcons(active(X1),X2) -> rcons(X1,X2)
rcons(X1,active(X2)) -> rcons(X1,X2)
posrecip(mark(X)) -> posrecip(X)
posrecip(active(X)) -> posrecip(X)
2ndsneg(mark(X1),X2) -> 2ndsneg(X1,X2)
2ndsneg(X1,mark(X2)) -> 2ndsneg(X1,X2)
2ndsneg(active(X1),X2) -> 2ndsneg(X1,X2)
2ndsneg(X1,active(X2)) -> 2ndsneg(X1,X2)
negrecip(mark(X)) -> negrecip(X)
negrecip(active(X)) -> negrecip(X)
pi(mark(X)) -> pi(X)
pi(active(X)) -> pi(X)
plus(mark(X1),X2) -> plus(X1,X2)
plus(X1,mark(X2)) -> plus(X1,X2)
plus(active(X1),X2) -> plus(X1,X2)
plus(X1,active(X2)) -> plus(X1,X2)
times(mark(X1),X2) -> times(X1,X2)
times(X1,mark(X2)) -> times(X1,X2)
times(active(X1),X2) -> times(X1,X2)
times(X1,active(X2)) -> times(X1,X2)
square(mark(X)) -> square(X)
square(active(X)) -> square(X)
)