(VAR N X X1 X2 Y Z )
(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)
        
)