(VAR N X X1 X2 Y Z )
(RULES 
        terms(N) -> cons(recip(sqr(N)), n__terms(n__s(N)))
        sqr(0) -> 0
        sqr(s(X)) -> s(n__add(n__sqr(activate(X)), n__dbl(activate(X))))
        dbl(0) -> 0
        dbl(s(X)) -> s(n__s(n__dbl(activate(X))))
        add(0, X) -> X
        add(s(X), Y) -> s(n__add(activate(X), Y))
        first(0, X) -> nil
        first(s(X), cons(Y, Z)) -> cons(Y, n__first(activate(X), activate(Z)))
        terms(X) -> n__terms(X)
        s(X) -> n__s(X)
        add(X1, X2) -> n__add(X1, X2)
        sqr(X) -> n__sqr(X)
        dbl(X) -> n__dbl(X)
        first(X1, X2) -> n__first(X1, X2)
        activate(n__terms(X)) -> terms(activate(X))
        activate(n__s(X)) -> s(X)
        activate(n__add(X1, X2)) -> add(activate(X1), activate(X2))
        activate(n__sqr(X)) -> sqr(activate(X))
        activate(n__dbl(X)) -> dbl(activate(X))
        activate(n__first(X1, X2)) -> first(activate(X1), activate(X2))
        activate(X) -> X
        
)