MAYBE
Trs:
 {                  sqr(0()) -> 0(),
                   sqr(s(X)) -> s(add(sqr(X), dbl(X))),
                 add(0(), X) -> X,
                add(s(X), Y) -> s(add(X, Y)),
                    dbl(0()) -> 0(),
                   dbl(s(X)) -> s(s(dbl(X))),
                   half(0()) -> 0(),
                half(s(0())) -> 0(),
               half(s(s(X))) -> s(half(X)),
                half(dbl(X)) -> X,
                    terms(N) -> cons(recip(sqr(N)), n__terms(s(N))),
                    terms(X) -> n__terms(X),
               first(0(), X) -> nil(),
     first(s(X), cons(Y, Z)) -> cons(Y, n__first(X, activate(Z))),
               first(X1, X2) -> n__first(X1, X2),
       activate(n__terms(X)) -> terms(X),
  activate(n__first(X1, X2)) -> first(X1, X2),
                 activate(X) -> X}
 Comment:
  We consider a duplicating trs.
  FAIL:
   Open