TRS:
 {               a__terms(N) -> cons(recip(a__sqr(mark(N))), terms(s(N))),
                 a__sqr(0()) -> 0(),
                a__sqr(s(X)) -> s(add(sqr(X), dbl(X))),
                 a__dbl(0()) -> 0(),
                a__dbl(s(X)) -> s(s(dbl(X))),
              a__add(0(), X) -> mark(X),
             a__add(s(X), Y) -> s(add(X, Y)),
            a__first(0(), X) -> nil(),
  a__first(s(X), cons(Y, Z)) -> cons(mark(Y), first(X, Z)),
              mark(terms(X)) -> a__terms(mark(X)),
                mark(sqr(X)) -> a__sqr(mark(X)),
           mark(add(X1, X2)) -> a__add(mark(X1), mark(X2)),
                mark(dbl(X)) -> a__dbl(mark(X)),
         mark(first(X1, X2)) -> a__first(mark(X1), mark(X2)),
          mark(cons(X1, X2)) -> cons(mark(X1), X2),
              mark(recip(X)) -> recip(mark(X)),
                  mark(s(X)) -> s(X),
                   mark(0()) -> 0(),
                 mark(nil()) -> nil(),
                 a__terms(X) -> terms(X),
                   a__sqr(X) -> sqr(X),
              a__add(X1, X2) -> add(X1, X2),
                   a__dbl(X) -> dbl(X),
            a__first(X1, X2) -> first(X1, X2)}
 Fail