YES
TRS:
 {                 a__sqr(X) -> sqr(X),
                a__sqr(s(X)) -> s(add(sqr(X), dbl(X))),
                 a__sqr(0()) -> 0(),
          mark(cons(X1, X2)) -> cons(mark(X1), X2),
              mark(recip(X)) -> recip(mark(X)),
              mark(terms(X)) -> a__terms(mark(X)),
                  mark(s(X)) -> s(X),
                   mark(0()) -> 0(),
           mark(add(X1, X2)) -> a__add(mark(X1), mark(X2)),
                mark(sqr(X)) -> a__sqr(mark(X)),
                mark(dbl(X)) -> a__dbl(mark(X)),
                 mark(nil()) -> nil(),
         mark(first(X1, X2)) -> a__first(mark(X1), mark(X2)),
                 a__terms(N) -> cons(recip(a__sqr(mark(N))), terms(s(N))),
                 a__terms(X) -> terms(X),
                   a__dbl(X) -> dbl(X),
                a__dbl(s(X)) -> s(s(dbl(X))),
                 a__dbl(0()) -> 0(),
              a__add(X1, X2) -> add(X1, X2),
             a__add(s(X), Y) -> s(add(X, Y)),
              a__add(0(), X) -> mark(X),
            a__first(X1, X2) -> first(X1, X2),
  a__first(s(X), cons(Y, Z)) -> cons(mark(Y), first(X, Z)),
            a__first(0(), X) -> nil()}
 DP:
  Strict:
   {        mark#(cons(X1, X2)) -> mark#(X1),
                mark#(recip(X)) -> mark#(X),
                mark#(terms(X)) -> mark#(X),
                mark#(terms(X)) -> a__terms#(mark(X)),
             mark#(add(X1, X2)) -> mark#(X1),
             mark#(add(X1, X2)) -> mark#(X2),
             mark#(add(X1, X2)) -> a__add#(mark(X1), mark(X2)),
                  mark#(sqr(X)) -> a__sqr#(mark(X)),
                  mark#(sqr(X)) -> mark#(X),
                  mark#(dbl(X)) -> mark#(X),
                  mark#(dbl(X)) -> a__dbl#(mark(X)),
           mark#(first(X1, X2)) -> mark#(X1),
           mark#(first(X1, X2)) -> mark#(X2),
           mark#(first(X1, X2)) -> a__first#(mark(X1), mark(X2)),
                   a__terms#(N) -> a__sqr#(mark(N)),
                   a__terms#(N) -> mark#(N),
                a__add#(0(), X) -> mark#(X),
    a__first#(s(X), cons(Y, Z)) -> mark#(Y)}
  Weak:
  {                 a__sqr(X) -> sqr(X),
                 a__sqr(s(X)) -> s(add(sqr(X), dbl(X))),
                  a__sqr(0()) -> 0(),
           mark(cons(X1, X2)) -> cons(mark(X1), X2),
               mark(recip(X)) -> recip(mark(X)),
               mark(terms(X)) -> a__terms(mark(X)),
                   mark(s(X)) -> s(X),
                    mark(0()) -> 0(),
            mark(add(X1, X2)) -> a__add(mark(X1), mark(X2)),
                 mark(sqr(X)) -> a__sqr(mark(X)),
                 mark(dbl(X)) -> a__dbl(mark(X)),
                  mark(nil()) -> nil(),
          mark(first(X1, X2)) -> a__first(mark(X1), mark(X2)),
                  a__terms(N) -> cons(recip(a__sqr(mark(N))), terms(s(N))),
                  a__terms(X) -> terms(X),
                    a__dbl(X) -> dbl(X),
                 a__dbl(s(X)) -> s(s(dbl(X))),
                  a__dbl(0()) -> 0(),
               a__add(X1, X2) -> add(X1, X2),
              a__add(s(X), Y) -> s(add(X, Y)),
               a__add(0(), X) -> mark(X),
             a__first(X1, X2) -> first(X1, X2),
   a__first(s(X), cons(Y, Z)) -> cons(mark(Y), first(X, Z)),
             a__first(0(), X) -> nil()}
  EDG:
   {
    (mark#(add(X1, X2)) -> mark#(X1), mark#(first(X1, X2)) -> a__first#(mark(X1), mark(X2)))
    (mark#(add(X1, X2)) -> mark#(X1), mark#(first(X1, X2)) -> mark#(X2))
    (mark#(add(X1, X2)) -> mark#(X1), mark#(first(X1, X2)) -> mark#(X1))
    (mark#(add(X1, X2)) -> mark#(X1), mark#(dbl(X)) -> a__dbl#(mark(X)))
    (mark#(add(X1, X2)) -> mark#(X1), mark#(dbl(X)) -> mark#(X))
    (mark#(add(X1, X2)) -> mark#(X1), mark#(sqr(X)) -> mark#(X))
    (mark#(add(X1, X2)) -> mark#(X1), mark#(sqr(X)) -> a__sqr#(mark(X)))
    (mark#(add(X1, X2)) -> mark#(X1), mark#(add(X1, X2)) -> a__add#(mark(X1), mark(X2)))
    (mark#(add(X1, X2)) -> mark#(X1), mark#(add(X1, X2)) -> mark#(X2))
    (mark#(add(X1, X2)) -> mark#(X1), mark#(add(X1, X2)) -> mark#(X1))
    (mark#(add(X1, X2)) -> mark#(X1), mark#(terms(X)) -> a__terms#(mark(X)))
    (mark#(add(X1, X2)) -> mark#(X1), mark#(terms(X)) -> mark#(X))
    (mark#(add(X1, X2)) -> mark#(X1), mark#(recip(X)) -> mark#(X))
    (mark#(add(X1, X2)) -> mark#(X1), mark#(cons(X1, X2)) -> mark#(X1))
    (mark#(terms(X)) -> a__terms#(mark(X)), a__terms#(N) -> mark#(N))
    (mark#(terms(X)) -> a__terms#(mark(X)), a__terms#(N) -> a__sqr#(mark(N)))
    (a__first#(s(X), cons(Y, Z)) -> mark#(Y), mark#(first(X1, X2)) -> a__first#(mark(X1), mark(X2)))
    (a__first#(s(X), cons(Y, Z)) -> mark#(Y), mark#(first(X1, X2)) -> mark#(X2))
    (a__first#(s(X), cons(Y, Z)) -> mark#(Y), mark#(first(X1, X2)) -> mark#(X1))
    (a__first#(s(X), cons(Y, Z)) -> mark#(Y), mark#(dbl(X)) -> a__dbl#(mark(X)))
    (a__first#(s(X), cons(Y, Z)) -> mark#(Y), mark#(dbl(X)) -> mark#(X))
    (a__first#(s(X), cons(Y, Z)) -> mark#(Y), mark#(sqr(X)) -> mark#(X))
    (a__first#(s(X), cons(Y, Z)) -> mark#(Y), mark#(sqr(X)) -> a__sqr#(mark(X)))
    (a__first#(s(X), cons(Y, Z)) -> mark#(Y), mark#(add(X1, X2)) -> a__add#(mark(X1), mark(X2)))
    (a__first#(s(X), cons(Y, Z)) -> mark#(Y), mark#(add(X1, X2)) -> mark#(X2))
    (a__first#(s(X), cons(Y, Z)) -> mark#(Y), mark#(add(X1, X2)) -> mark#(X1))
    (a__first#(s(X), cons(Y, Z)) -> mark#(Y), mark#(terms(X)) -> a__terms#(mark(X)))
    (a__first#(s(X), cons(Y, Z)) -> mark#(Y), mark#(terms(X)) -> mark#(X))
    (a__first#(s(X), cons(Y, Z)) -> mark#(Y), mark#(recip(X)) -> mark#(X))
    (a__first#(s(X), cons(Y, Z)) -> mark#(Y), mark#(cons(X1, X2)) -> mark#(X1))
    (mark#(first(X1, X2)) -> a__first#(mark(X1), mark(X2)), a__first#(s(X), cons(Y, Z)) -> mark#(Y))
    (mark#(terms(X)) -> mark#(X), mark#(first(X1, X2)) -> a__first#(mark(X1), mark(X2)))
    (mark#(terms(X)) -> mark#(X), mark#(first(X1, X2)) -> mark#(X2))
    (mark#(terms(X)) -> mark#(X), mark#(first(X1, X2)) -> mark#(X1))
    (mark#(terms(X)) -> mark#(X), mark#(dbl(X)) -> a__dbl#(mark(X)))
    (mark#(terms(X)) -> mark#(X), mark#(dbl(X)) -> mark#(X))
    (mark#(terms(X)) -> mark#(X), mark#(sqr(X)) -> mark#(X))
    (mark#(terms(X)) -> mark#(X), mark#(sqr(X)) -> a__sqr#(mark(X)))
    (mark#(terms(X)) -> mark#(X), mark#(add(X1, X2)) -> a__add#(mark(X1), mark(X2)))
    (mark#(terms(X)) -> mark#(X), mark#(add(X1, X2)) -> mark#(X2))
    (mark#(terms(X)) -> mark#(X), mark#(add(X1, X2)) -> mark#(X1))
    (mark#(terms(X)) -> mark#(X), mark#(terms(X)) -> a__terms#(mark(X)))
    (mark#(terms(X)) -> mark#(X), mark#(terms(X)) -> mark#(X))
    (mark#(terms(X)) -> mark#(X), mark#(recip(X)) -> mark#(X))
    (mark#(terms(X)) -> mark#(X), mark#(cons(X1, X2)) -> mark#(X1))
    (mark#(dbl(X)) -> mark#(X), mark#(first(X1, X2)) -> a__first#(mark(X1), mark(X2)))
    (mark#(dbl(X)) -> mark#(X), mark#(first(X1, X2)) -> mark#(X2))
    (mark#(dbl(X)) -> mark#(X), mark#(first(X1, X2)) -> mark#(X1))
    (mark#(dbl(X)) -> mark#(X), mark#(dbl(X)) -> a__dbl#(mark(X)))
    (mark#(dbl(X)) -> mark#(X), mark#(dbl(X)) -> mark#(X))
    (mark#(dbl(X)) -> mark#(X), mark#(sqr(X)) -> mark#(X))
    (mark#(dbl(X)) -> mark#(X), mark#(sqr(X)) -> a__sqr#(mark(X)))
    (mark#(dbl(X)) -> mark#(X), mark#(add(X1, X2)) -> a__add#(mark(X1), mark(X2)))
    (mark#(dbl(X)) -> mark#(X), mark#(add(X1, X2)) -> mark#(X2))
    (mark#(dbl(X)) -> mark#(X), mark#(add(X1, X2)) -> mark#(X1))
    (mark#(dbl(X)) -> mark#(X), mark#(terms(X)) -> a__terms#(mark(X)))
    (mark#(dbl(X)) -> mark#(X), mark#(terms(X)) -> mark#(X))
    (mark#(dbl(X)) -> mark#(X), mark#(recip(X)) -> mark#(X))
    (mark#(dbl(X)) -> mark#(X), mark#(cons(X1, X2)) -> mark#(X1))
    (a__terms#(N) -> mark#(N), mark#(first(X1, X2)) -> a__first#(mark(X1), mark(X2)))
    (a__terms#(N) -> mark#(N), mark#(first(X1, X2)) -> mark#(X2))
    (a__terms#(N) -> mark#(N), mark#(first(X1, X2)) -> mark#(X1))
    (a__terms#(N) -> mark#(N), mark#(dbl(X)) -> a__dbl#(mark(X)))
    (a__terms#(N) -> mark#(N), mark#(dbl(X)) -> mark#(X))
    (a__terms#(N) -> mark#(N), mark#(sqr(X)) -> mark#(X))
    (a__terms#(N) -> mark#(N), mark#(sqr(X)) -> a__sqr#(mark(X)))
    (a__terms#(N) -> mark#(N), mark#(add(X1, X2)) -> a__add#(mark(X1), mark(X2)))
    (a__terms#(N) -> mark#(N), mark#(add(X1, X2)) -> mark#(X2))
    (a__terms#(N) -> mark#(N), mark#(add(X1, X2)) -> mark#(X1))
    (a__terms#(N) -> mark#(N), mark#(terms(X)) -> a__terms#(mark(X)))
    (a__terms#(N) -> mark#(N), mark#(terms(X)) -> mark#(X))
    (a__terms#(N) -> mark#(N), mark#(recip(X)) -> mark#(X))
    (a__terms#(N) -> mark#(N), mark#(cons(X1, X2)) -> mark#(X1))
    (mark#(first(X1, X2)) -> mark#(X2), mark#(first(X1, X2)) -> a__first#(mark(X1), mark(X2)))
    (mark#(first(X1, X2)) -> mark#(X2), mark#(first(X1, X2)) -> mark#(X2))
    (mark#(first(X1, X2)) -> mark#(X2), mark#(first(X1, X2)) -> mark#(X1))
    (mark#(first(X1, X2)) -> mark#(X2), mark#(dbl(X)) -> a__dbl#(mark(X)))
    (mark#(first(X1, X2)) -> mark#(X2), mark#(dbl(X)) -> mark#(X))
    (mark#(first(X1, X2)) -> mark#(X2), mark#(sqr(X)) -> mark#(X))
    (mark#(first(X1, X2)) -> mark#(X2), mark#(sqr(X)) -> a__sqr#(mark(X)))
    (mark#(first(X1, X2)) -> mark#(X2), mark#(add(X1, X2)) -> a__add#(mark(X1), mark(X2)))
    (mark#(first(X1, X2)) -> mark#(X2), mark#(add(X1, X2)) -> mark#(X2))
    (mark#(first(X1, X2)) -> mark#(X2), mark#(add(X1, X2)) -> mark#(X1))
    (mark#(first(X1, X2)) -> mark#(X2), mark#(terms(X)) -> a__terms#(mark(X)))
    (mark#(first(X1, X2)) -> mark#(X2), mark#(terms(X)) -> mark#(X))
    (mark#(first(X1, X2)) -> mark#(X2), mark#(recip(X)) -> mark#(X))
    (mark#(first(X1, X2)) -> mark#(X2), mark#(cons(X1, X2)) -> mark#(X1))
    (mark#(add(X1, X2)) -> mark#(X2), mark#(cons(X1, X2)) -> mark#(X1))
    (mark#(add(X1, X2)) -> mark#(X2), mark#(recip(X)) -> mark#(X))
    (mark#(add(X1, X2)) -> mark#(X2), mark#(terms(X)) -> mark#(X))
    (mark#(add(X1, X2)) -> mark#(X2), mark#(terms(X)) -> a__terms#(mark(X)))
    (mark#(add(X1, X2)) -> mark#(X2), mark#(add(X1, X2)) -> mark#(X1))
    (mark#(add(X1, X2)) -> mark#(X2), mark#(add(X1, X2)) -> mark#(X2))
    (mark#(add(X1, X2)) -> mark#(X2), mark#(add(X1, X2)) -> a__add#(mark(X1), mark(X2)))
    (mark#(add(X1, X2)) -> mark#(X2), mark#(sqr(X)) -> a__sqr#(mark(X)))
    (mark#(add(X1, X2)) -> mark#(X2), mark#(sqr(X)) -> mark#(X))
    (mark#(add(X1, X2)) -> mark#(X2), mark#(dbl(X)) -> mark#(X))
    (mark#(add(X1, X2)) -> mark#(X2), mark#(dbl(X)) -> a__dbl#(mark(X)))
    (mark#(add(X1, X2)) -> mark#(X2), mark#(first(X1, X2)) -> mark#(X1))
    (mark#(add(X1, X2)) -> mark#(X2), mark#(first(X1, X2)) -> mark#(X2))
    (mark#(add(X1, X2)) -> mark#(X2), mark#(first(X1, X2)) -> a__first#(mark(X1), mark(X2)))
    (a__add#(0(), X) -> mark#(X), mark#(cons(X1, X2)) -> mark#(X1))
    (a__add#(0(), X) -> mark#(X), mark#(recip(X)) -> mark#(X))
    (a__add#(0(), X) -> mark#(X), mark#(terms(X)) -> mark#(X))
    (a__add#(0(), X) -> mark#(X), mark#(terms(X)) -> a__terms#(mark(X)))
    (a__add#(0(), X) -> mark#(X), mark#(add(X1, X2)) -> mark#(X1))
    (a__add#(0(), X) -> mark#(X), mark#(add(X1, X2)) -> mark#(X2))
    (a__add#(0(), X) -> mark#(X), mark#(add(X1, X2)) -> a__add#(mark(X1), mark(X2)))
    (a__add#(0(), X) -> mark#(X), mark#(sqr(X)) -> a__sqr#(mark(X)))
    (a__add#(0(), X) -> mark#(X), mark#(sqr(X)) -> mark#(X))
    (a__add#(0(), X) -> mark#(X), mark#(dbl(X)) -> mark#(X))
    (a__add#(0(), X) -> mark#(X), mark#(dbl(X)) -> a__dbl#(mark(X)))
    (a__add#(0(), X) -> mark#(X), mark#(first(X1, X2)) -> mark#(X1))
    (a__add#(0(), X) -> mark#(X), mark#(first(X1, X2)) -> mark#(X2))
    (a__add#(0(), X) -> mark#(X), mark#(first(X1, X2)) -> a__first#(mark(X1), mark(X2)))
    (mark#(sqr(X)) -> mark#(X), mark#(cons(X1, X2)) -> mark#(X1))
    (mark#(sqr(X)) -> mark#(X), mark#(recip(X)) -> mark#(X))
    (mark#(sqr(X)) -> mark#(X), mark#(terms(X)) -> mark#(X))
    (mark#(sqr(X)) -> mark#(X), mark#(terms(X)) -> a__terms#(mark(X)))
    (mark#(sqr(X)) -> mark#(X), mark#(add(X1, X2)) -> mark#(X1))
    (mark#(sqr(X)) -> mark#(X), mark#(add(X1, X2)) -> mark#(X2))
    (mark#(sqr(X)) -> mark#(X), mark#(add(X1, X2)) -> a__add#(mark(X1), mark(X2)))
    (mark#(sqr(X)) -> mark#(X), mark#(sqr(X)) -> a__sqr#(mark(X)))
    (mark#(sqr(X)) -> mark#(X), mark#(sqr(X)) -> mark#(X))
    (mark#(sqr(X)) -> mark#(X), mark#(dbl(X)) -> mark#(X))
    (mark#(sqr(X)) -> mark#(X), mark#(dbl(X)) -> a__dbl#(mark(X)))
    (mark#(sqr(X)) -> mark#(X), mark#(first(X1, X2)) -> mark#(X1))
    (mark#(sqr(X)) -> mark#(X), mark#(first(X1, X2)) -> mark#(X2))
    (mark#(sqr(X)) -> mark#(X), mark#(first(X1, X2)) -> a__first#(mark(X1), mark(X2)))
    (mark#(recip(X)) -> mark#(X), mark#(cons(X1, X2)) -> mark#(X1))
    (mark#(recip(X)) -> mark#(X), mark#(recip(X)) -> mark#(X))
    (mark#(recip(X)) -> mark#(X), mark#(terms(X)) -> mark#(X))
    (mark#(recip(X)) -> mark#(X), mark#(terms(X)) -> a__terms#(mark(X)))
    (mark#(recip(X)) -> mark#(X), mark#(add(X1, X2)) -> mark#(X1))
    (mark#(recip(X)) -> mark#(X), mark#(add(X1, X2)) -> mark#(X2))
    (mark#(recip(X)) -> mark#(X), mark#(add(X1, X2)) -> a__add#(mark(X1), mark(X2)))
    (mark#(recip(X)) -> mark#(X), mark#(sqr(X)) -> a__sqr#(mark(X)))
    (mark#(recip(X)) -> mark#(X), mark#(sqr(X)) -> mark#(X))
    (mark#(recip(X)) -> mark#(X), mark#(dbl(X)) -> mark#(X))
    (mark#(recip(X)) -> mark#(X), mark#(dbl(X)) -> a__dbl#(mark(X)))
    (mark#(recip(X)) -> mark#(X), mark#(first(X1, X2)) -> mark#(X1))
    (mark#(recip(X)) -> mark#(X), mark#(first(X1, X2)) -> mark#(X2))
    (mark#(recip(X)) -> mark#(X), mark#(first(X1, X2)) -> a__first#(mark(X1), mark(X2)))
    (mark#(add(X1, X2)) -> a__add#(mark(X1), mark(X2)), a__add#(0(), X) -> mark#(X))
    (mark#(first(X1, X2)) -> mark#(X1), mark#(cons(X1, X2)) -> mark#(X1))
    (mark#(first(X1, X2)) -> mark#(X1), mark#(recip(X)) -> mark#(X))
    (mark#(first(X1, X2)) -> mark#(X1), mark#(terms(X)) -> mark#(X))
    (mark#(first(X1, X2)) -> mark#(X1), mark#(terms(X)) -> a__terms#(mark(X)))
    (mark#(first(X1, X2)) -> mark#(X1), mark#(add(X1, X2)) -> mark#(X1))
    (mark#(first(X1, X2)) -> mark#(X1), mark#(add(X1, X2)) -> mark#(X2))
    (mark#(first(X1, X2)) -> mark#(X1), mark#(add(X1, X2)) -> a__add#(mark(X1), mark(X2)))
    (mark#(first(X1, X2)) -> mark#(X1), mark#(sqr(X)) -> a__sqr#(mark(X)))
    (mark#(first(X1, X2)) -> mark#(X1), mark#(sqr(X)) -> mark#(X))
    (mark#(first(X1, X2)) -> mark#(X1), mark#(dbl(X)) -> mark#(X))
    (mark#(first(X1, X2)) -> mark#(X1), mark#(dbl(X)) -> a__dbl#(mark(X)))
    (mark#(first(X1, X2)) -> mark#(X1), mark#(first(X1, X2)) -> mark#(X1))
    (mark#(first(X1, X2)) -> mark#(X1), mark#(first(X1, X2)) -> mark#(X2))
    (mark#(first(X1, X2)) -> mark#(X1), mark#(first(X1, X2)) -> a__first#(mark(X1), mark(X2)))
    (mark#(cons(X1, X2)) -> mark#(X1), mark#(cons(X1, X2)) -> mark#(X1))
    (mark#(cons(X1, X2)) -> mark#(X1), mark#(recip(X)) -> mark#(X))
    (mark#(cons(X1, X2)) -> mark#(X1), mark#(terms(X)) -> mark#(X))
    (mark#(cons(X1, X2)) -> mark#(X1), mark#(terms(X)) -> a__terms#(mark(X)))
    (mark#(cons(X1, X2)) -> mark#(X1), mark#(add(X1, X2)) -> mark#(X1))
    (mark#(cons(X1, X2)) -> mark#(X1), mark#(add(X1, X2)) -> mark#(X2))
    (mark#(cons(X1, X2)) -> mark#(X1), mark#(add(X1, X2)) -> a__add#(mark(X1), mark(X2)))
    (mark#(cons(X1, X2)) -> mark#(X1), mark#(sqr(X)) -> a__sqr#(mark(X)))
    (mark#(cons(X1, X2)) -> mark#(X1), mark#(sqr(X)) -> mark#(X))
    (mark#(cons(X1, X2)) -> mark#(X1), mark#(dbl(X)) -> mark#(X))
    (mark#(cons(X1, X2)) -> mark#(X1), mark#(dbl(X)) -> a__dbl#(mark(X)))
    (mark#(cons(X1, X2)) -> mark#(X1), mark#(first(X1, X2)) -> mark#(X1))
    (mark#(cons(X1, X2)) -> mark#(X1), mark#(first(X1, X2)) -> mark#(X2))
    (mark#(cons(X1, X2)) -> mark#(X1), mark#(first(X1, X2)) -> a__first#(mark(X1), mark(X2)))
   }
   SCCS:
    Scc:
     {        mark#(cons(X1, X2)) -> mark#(X1),
                  mark#(recip(X)) -> mark#(X),
                  mark#(terms(X)) -> mark#(X),
                  mark#(terms(X)) -> a__terms#(mark(X)),
               mark#(add(X1, X2)) -> mark#(X1),
               mark#(add(X1, X2)) -> mark#(X2),
               mark#(add(X1, X2)) -> a__add#(mark(X1), mark(X2)),
                    mark#(sqr(X)) -> mark#(X),
                    mark#(dbl(X)) -> mark#(X),
             mark#(first(X1, X2)) -> mark#(X1),
             mark#(first(X1, X2)) -> mark#(X2),
             mark#(first(X1, X2)) -> a__first#(mark(X1), mark(X2)),
                     a__terms#(N) -> mark#(N),
                  a__add#(0(), X) -> mark#(X),
      a__first#(s(X), cons(Y, Z)) -> mark#(Y)}
    SCC:
     Strict:
      {        mark#(cons(X1, X2)) -> mark#(X1),
                   mark#(recip(X)) -> mark#(X),
                   mark#(terms(X)) -> mark#(X),
                   mark#(terms(X)) -> a__terms#(mark(X)),
                mark#(add(X1, X2)) -> mark#(X1),
                mark#(add(X1, X2)) -> mark#(X2),
                mark#(add(X1, X2)) -> a__add#(mark(X1), mark(X2)),
                     mark#(sqr(X)) -> mark#(X),
                     mark#(dbl(X)) -> mark#(X),
              mark#(first(X1, X2)) -> mark#(X1),
              mark#(first(X1, X2)) -> mark#(X2),
              mark#(first(X1, X2)) -> a__first#(mark(X1), mark(X2)),
                      a__terms#(N) -> mark#(N),
                   a__add#(0(), X) -> mark#(X),
       a__first#(s(X), cons(Y, Z)) -> mark#(Y)}
     Weak:
     {                 a__sqr(X) -> sqr(X),
                    a__sqr(s(X)) -> s(add(sqr(X), dbl(X))),
                     a__sqr(0()) -> 0(),
              mark(cons(X1, X2)) -> cons(mark(X1), X2),
                  mark(recip(X)) -> recip(mark(X)),
                  mark(terms(X)) -> a__terms(mark(X)),
                      mark(s(X)) -> s(X),
                       mark(0()) -> 0(),
               mark(add(X1, X2)) -> a__add(mark(X1), mark(X2)),
                    mark(sqr(X)) -> a__sqr(mark(X)),
                    mark(dbl(X)) -> a__dbl(mark(X)),
                     mark(nil()) -> nil(),
             mark(first(X1, X2)) -> a__first(mark(X1), mark(X2)),
                     a__terms(N) -> cons(recip(a__sqr(mark(N))), terms(s(N))),
                     a__terms(X) -> terms(X),
                       a__dbl(X) -> dbl(X),
                    a__dbl(s(X)) -> s(s(dbl(X))),
                     a__dbl(0()) -> 0(),
                  a__add(X1, X2) -> add(X1, X2),
                 a__add(s(X), Y) -> s(add(X, Y)),
                  a__add(0(), X) -> mark(X),
                a__first(X1, X2) -> first(X1, X2),
      a__first(s(X), cons(Y, Z)) -> cons(mark(Y), first(X, Z)),
                a__first(0(), X) -> nil()}
     POLY:
      Argument Filtering:
       pi(first) = [0,1], pi(a__first#) = 1, pi(a__first) = [0,1], pi(nil) = [], pi(a__add#) = 1, pi(a__add) = [0,1], pi(a__dbl) = 0, pi(dbl) = 0, pi(sqr) = 0, pi(add) = [0,1], pi(0) = [], pi(a__terms#) = 0, pi(a__terms) = 0, pi(s) = [], pi(terms) = 0, pi(mark#) = 0, pi(mark) = 0, pi(a__sqr) = 0, pi(recip) = 0, pi(cons) = 0
      Usable Rules:
       {}
      Interpretation:
       [first](x0, x1) = x0 + x1,
       [add](x0, x1) = x0 + x1 + 1
      Strict:
       {        mark#(cons(X1, X2)) -> mark#(X1),
                    mark#(recip(X)) -> mark#(X),
                    mark#(terms(X)) -> mark#(X),
                    mark#(terms(X)) -> a__terms#(mark(X)),
                      mark#(sqr(X)) -> mark#(X),
                      mark#(dbl(X)) -> mark#(X),
               mark#(first(X1, X2)) -> mark#(X1),
               mark#(first(X1, X2)) -> mark#(X2),
               mark#(first(X1, X2)) -> a__first#(mark(X1), mark(X2)),
                       a__terms#(N) -> mark#(N),
                    a__add#(0(), X) -> mark#(X),
        a__first#(s(X), cons(Y, Z)) -> mark#(Y)}
      Weak:
       {                 a__sqr(X) -> sqr(X),
                      a__sqr(s(X)) -> s(add(sqr(X), dbl(X))),
                       a__sqr(0()) -> 0(),
                mark(cons(X1, X2)) -> cons(mark(X1), X2),
                    mark(recip(X)) -> recip(mark(X)),
                    mark(terms(X)) -> a__terms(mark(X)),
                        mark(s(X)) -> s(X),
                         mark(0()) -> 0(),
                 mark(add(X1, X2)) -> a__add(mark(X1), mark(X2)),
                      mark(sqr(X)) -> a__sqr(mark(X)),
                      mark(dbl(X)) -> a__dbl(mark(X)),
                       mark(nil()) -> nil(),
               mark(first(X1, X2)) -> a__first(mark(X1), mark(X2)),
                       a__terms(N) -> cons(recip(a__sqr(mark(N))), terms(s(N))),
                       a__terms(X) -> terms(X),
                         a__dbl(X) -> dbl(X),
                      a__dbl(s(X)) -> s(s(dbl(X))),
                       a__dbl(0()) -> 0(),
                    a__add(X1, X2) -> add(X1, X2),
                   a__add(s(X), Y) -> s(add(X, Y)),
                    a__add(0(), X) -> mark(X),
                  a__first(X1, X2) -> first(X1, X2),
        a__first(s(X), cons(Y, Z)) -> cons(mark(Y), first(X, Z)),
                  a__first(0(), X) -> nil()}
      EDG:
       {(mark#(first(X1, X2)) -> mark#(X1), mark#(first(X1, X2)) -> a__first#(mark(X1), mark(X2)))
        (mark#(first(X1, X2)) -> mark#(X1), mark#(first(X1, X2)) -> mark#(X2))
        (mark#(first(X1, X2)) -> mark#(X1), mark#(first(X1, X2)) -> mark#(X1))
        (mark#(first(X1, X2)) -> mark#(X1), mark#(dbl(X)) -> mark#(X))
        (mark#(first(X1, X2)) -> mark#(X1), mark#(sqr(X)) -> mark#(X))
        (mark#(first(X1, X2)) -> mark#(X1), mark#(terms(X)) -> a__terms#(mark(X)))
        (mark#(first(X1, X2)) -> mark#(X1), mark#(terms(X)) -> mark#(X))
        (mark#(first(X1, X2)) -> mark#(X1), mark#(recip(X)) -> mark#(X))
        (mark#(first(X1, X2)) -> mark#(X1), mark#(cons(X1, X2)) -> mark#(X1))
        (mark#(first(X1, X2)) -> a__first#(mark(X1), mark(X2)), a__first#(s(X), cons(Y, Z)) -> mark#(Y))
        (mark#(first(X1, X2)) -> mark#(X2), mark#(first(X1, X2)) -> a__first#(mark(X1), mark(X2)))
        (mark#(first(X1, X2)) -> mark#(X2), mark#(first(X1, X2)) -> mark#(X2))
        (mark#(first(X1, X2)) -> mark#(X2), mark#(first(X1, X2)) -> mark#(X1))
        (mark#(first(X1, X2)) -> mark#(X2), mark#(dbl(X)) -> mark#(X))
        (mark#(first(X1, X2)) -> mark#(X2), mark#(sqr(X)) -> mark#(X))
        (mark#(first(X1, X2)) -> mark#(X2), mark#(terms(X)) -> a__terms#(mark(X)))
        (mark#(first(X1, X2)) -> mark#(X2), mark#(terms(X)) -> mark#(X))
        (mark#(first(X1, X2)) -> mark#(X2), mark#(recip(X)) -> mark#(X))
        (mark#(first(X1, X2)) -> mark#(X2), mark#(cons(X1, X2)) -> mark#(X1))
        (mark#(terms(X)) -> mark#(X), mark#(first(X1, X2)) -> a__first#(mark(X1), mark(X2)))
        (mark#(terms(X)) -> mark#(X), mark#(first(X1, X2)) -> mark#(X2))
        (mark#(terms(X)) -> mark#(X), mark#(first(X1, X2)) -> mark#(X1))
        (mark#(terms(X)) -> mark#(X), mark#(dbl(X)) -> mark#(X))
        (mark#(terms(X)) -> mark#(X), mark#(sqr(X)) -> mark#(X))
        (mark#(terms(X)) -> mark#(X), mark#(terms(X)) -> a__terms#(mark(X)))
        (mark#(terms(X)) -> mark#(X), mark#(terms(X)) -> mark#(X))
        (mark#(terms(X)) -> mark#(X), mark#(recip(X)) -> mark#(X))
        (mark#(terms(X)) -> mark#(X), mark#(cons(X1, X2)) -> mark#(X1))
        (mark#(dbl(X)) -> mark#(X), mark#(first(X1, X2)) -> a__first#(mark(X1), mark(X2)))
        (mark#(dbl(X)) -> mark#(X), mark#(first(X1, X2)) -> mark#(X2))
        (mark#(dbl(X)) -> mark#(X), mark#(first(X1, X2)) -> mark#(X1))
        (mark#(dbl(X)) -> mark#(X), mark#(dbl(X)) -> mark#(X))
        (mark#(dbl(X)) -> mark#(X), mark#(sqr(X)) -> mark#(X))
        (mark#(dbl(X)) -> mark#(X), mark#(terms(X)) -> a__terms#(mark(X)))
        (mark#(dbl(X)) -> mark#(X), mark#(terms(X)) -> mark#(X))
        (mark#(dbl(X)) -> mark#(X), mark#(recip(X)) -> mark#(X))
        (mark#(dbl(X)) -> mark#(X), mark#(cons(X1, X2)) -> mark#(X1))
        (mark#(terms(X)) -> a__terms#(mark(X)), a__terms#(N) -> mark#(N))
        (a__add#(0(), X) -> mark#(X), mark#(cons(X1, X2)) -> mark#(X1))
        (a__add#(0(), X) -> mark#(X), mark#(recip(X)) -> mark#(X))
        (a__add#(0(), X) -> mark#(X), mark#(terms(X)) -> mark#(X))
        (a__add#(0(), X) -> mark#(X), mark#(terms(X)) -> a__terms#(mark(X)))
        (a__add#(0(), X) -> mark#(X), mark#(sqr(X)) -> mark#(X))
        (a__add#(0(), X) -> mark#(X), mark#(dbl(X)) -> mark#(X))
        (a__add#(0(), X) -> mark#(X), mark#(first(X1, X2)) -> mark#(X1))
        (a__add#(0(), X) -> mark#(X), mark#(first(X1, X2)) -> mark#(X2))
        (a__add#(0(), X) -> mark#(X), mark#(first(X1, X2)) -> a__first#(mark(X1), mark(X2)))
        (mark#(sqr(X)) -> mark#(X), mark#(cons(X1, X2)) -> mark#(X1))
        (mark#(sqr(X)) -> mark#(X), mark#(recip(X)) -> mark#(X))
        (mark#(sqr(X)) -> mark#(X), mark#(terms(X)) -> mark#(X))
        (mark#(sqr(X)) -> mark#(X), mark#(terms(X)) -> a__terms#(mark(X)))
        (mark#(sqr(X)) -> mark#(X), mark#(sqr(X)) -> mark#(X))
        (mark#(sqr(X)) -> mark#(X), mark#(dbl(X)) -> mark#(X))
        (mark#(sqr(X)) -> mark#(X), mark#(first(X1, X2)) -> mark#(X1))
        (mark#(sqr(X)) -> mark#(X), mark#(first(X1, X2)) -> mark#(X2))
        (mark#(sqr(X)) -> mark#(X), mark#(first(X1, X2)) -> a__first#(mark(X1), mark(X2)))
        (mark#(recip(X)) -> mark#(X), mark#(cons(X1, X2)) -> mark#(X1))
        (mark#(recip(X)) -> mark#(X), mark#(recip(X)) -> mark#(X))
        (mark#(recip(X)) -> mark#(X), mark#(terms(X)) -> mark#(X))
        (mark#(recip(X)) -> mark#(X), mark#(terms(X)) -> a__terms#(mark(X)))
        (mark#(recip(X)) -> mark#(X), mark#(sqr(X)) -> mark#(X))
        (mark#(recip(X)) -> mark#(X), mark#(dbl(X)) -> mark#(X))
        (mark#(recip(X)) -> mark#(X), mark#(first(X1, X2)) -> mark#(X1))
        (mark#(recip(X)) -> mark#(X), mark#(first(X1, X2)) -> mark#(X2))
        (mark#(recip(X)) -> mark#(X), mark#(first(X1, X2)) -> a__first#(mark(X1), mark(X2)))
        (a__first#(s(X), cons(Y, Z)) -> mark#(Y), mark#(cons(X1, X2)) -> mark#(X1))
        (a__first#(s(X), cons(Y, Z)) -> mark#(Y), mark#(recip(X)) -> mark#(X))
        (a__first#(s(X), cons(Y, Z)) -> mark#(Y), mark#(terms(X)) -> mark#(X))
        (a__first#(s(X), cons(Y, Z)) -> mark#(Y), mark#(terms(X)) -> a__terms#(mark(X)))
        (a__first#(s(X), cons(Y, Z)) -> mark#(Y), mark#(sqr(X)) -> mark#(X))
        (a__first#(s(X), cons(Y, Z)) -> mark#(Y), mark#(dbl(X)) -> mark#(X))
        (a__first#(s(X), cons(Y, Z)) -> mark#(Y), mark#(first(X1, X2)) -> mark#(X1))
        (a__first#(s(X), cons(Y, Z)) -> mark#(Y), mark#(first(X1, X2)) -> mark#(X2))
        (a__first#(s(X), cons(Y, Z)) -> mark#(Y), mark#(first(X1, X2)) -> a__first#(mark(X1), mark(X2)))
        (a__terms#(N) -> mark#(N), mark#(cons(X1, X2)) -> mark#(X1))
        (a__terms#(N) -> mark#(N), mark#(recip(X)) -> mark#(X))
        (a__terms#(N) -> mark#(N), mark#(terms(X)) -> mark#(X))
        (a__terms#(N) -> mark#(N), mark#(terms(X)) -> a__terms#(mark(X)))
        (a__terms#(N) -> mark#(N), mark#(sqr(X)) -> mark#(X))
        (a__terms#(N) -> mark#(N), mark#(dbl(X)) -> mark#(X))
        (a__terms#(N) -> mark#(N), mark#(first(X1, X2)) -> mark#(X1))
        (a__terms#(N) -> mark#(N), mark#(first(X1, X2)) -> mark#(X2))
        (a__terms#(N) -> mark#(N), mark#(first(X1, X2)) -> a__first#(mark(X1), mark(X2)))
        (mark#(cons(X1, X2)) -> mark#(X1), mark#(cons(X1, X2)) -> mark#(X1))
        (mark#(cons(X1, X2)) -> mark#(X1), mark#(recip(X)) -> mark#(X))
        (mark#(cons(X1, X2)) -> mark#(X1), mark#(terms(X)) -> mark#(X))
        (mark#(cons(X1, X2)) -> mark#(X1), mark#(terms(X)) -> a__terms#(mark(X)))
        (mark#(cons(X1, X2)) -> mark#(X1), mark#(sqr(X)) -> mark#(X))
        (mark#(cons(X1, X2)) -> mark#(X1), mark#(dbl(X)) -> mark#(X))
        (mark#(cons(X1, X2)) -> mark#(X1), mark#(first(X1, X2)) -> mark#(X1))
        (mark#(cons(X1, X2)) -> mark#(X1), mark#(first(X1, X2)) -> mark#(X2))
        (mark#(cons(X1, X2)) -> mark#(X1), mark#(first(X1, X2)) -> a__first#(mark(X1), mark(X2)))}
       SCCS:
        Scc:
         {        mark#(cons(X1, X2)) -> mark#(X1),
                      mark#(recip(X)) -> mark#(X),
                      mark#(terms(X)) -> mark#(X),
                      mark#(terms(X)) -> a__terms#(mark(X)),
                        mark#(sqr(X)) -> mark#(X),
                        mark#(dbl(X)) -> mark#(X),
                 mark#(first(X1, X2)) -> mark#(X1),
                 mark#(first(X1, X2)) -> mark#(X2),
                 mark#(first(X1, X2)) -> a__first#(mark(X1), mark(X2)),
                         a__terms#(N) -> mark#(N),
          a__first#(s(X), cons(Y, Z)) -> mark#(Y)}
        SCC:
         Strict:
          {        mark#(cons(X1, X2)) -> mark#(X1),
                       mark#(recip(X)) -> mark#(X),
                       mark#(terms(X)) -> mark#(X),
                       mark#(terms(X)) -> a__terms#(mark(X)),
                         mark#(sqr(X)) -> mark#(X),
                         mark#(dbl(X)) -> mark#(X),
                  mark#(first(X1, X2)) -> mark#(X1),
                  mark#(first(X1, X2)) -> mark#(X2),
                  mark#(first(X1, X2)) -> a__first#(mark(X1), mark(X2)),
                          a__terms#(N) -> mark#(N),
           a__first#(s(X), cons(Y, Z)) -> mark#(Y)}
         Weak:
         {                 a__sqr(X) -> sqr(X),
                        a__sqr(s(X)) -> s(add(sqr(X), dbl(X))),
                         a__sqr(0()) -> 0(),
                  mark(cons(X1, X2)) -> cons(mark(X1), X2),
                      mark(recip(X)) -> recip(mark(X)),
                      mark(terms(X)) -> a__terms(mark(X)),
                          mark(s(X)) -> s(X),
                           mark(0()) -> 0(),
                   mark(add(X1, X2)) -> a__add(mark(X1), mark(X2)),
                        mark(sqr(X)) -> a__sqr(mark(X)),
                        mark(dbl(X)) -> a__dbl(mark(X)),
                         mark(nil()) -> nil(),
                 mark(first(X1, X2)) -> a__first(mark(X1), mark(X2)),
                         a__terms(N) -> cons(recip(a__sqr(mark(N))), terms(s(N))),
                         a__terms(X) -> terms(X),
                           a__dbl(X) -> dbl(X),
                        a__dbl(s(X)) -> s(s(dbl(X))),
                         a__dbl(0()) -> 0(),
                      a__add(X1, X2) -> add(X1, X2),
                     a__add(s(X), Y) -> s(add(X, Y)),
                      a__add(0(), X) -> mark(X),
                    a__first(X1, X2) -> first(X1, X2),
          a__first(s(X), cons(Y, Z)) -> cons(mark(Y), first(X, Z)),
                    a__first(0(), X) -> nil()}
         POLY:
          Argument Filtering:
           pi(first) = [0,1], pi(a__first#) = 1, pi(a__first) = [0,1], pi(nil) = [], pi(a__add) = 1, pi(a__dbl) = 0, pi(dbl) = 0, pi(sqr) = 0, pi(add) = 1, pi(0) = [], pi(a__terms#) = [0], pi(a__terms) = [0], pi(s) = [], pi(terms) = [0], pi(mark#) = 0, pi(mark) = 0, pi(a__sqr) = 0, pi(recip) = 0, pi(cons) = 0
          Usable Rules:
           {}
          Interpretation:
           [a__terms#](x0) = x0 + 1,
           [first](x0, x1) = x0 + x1,
           [terms](x0) = x0 + 1
          Strict:
           {        mark#(cons(X1, X2)) -> mark#(X1),
                        mark#(recip(X)) -> mark#(X),
                        mark#(terms(X)) -> a__terms#(mark(X)),
                          mark#(sqr(X)) -> mark#(X),
                          mark#(dbl(X)) -> mark#(X),
                   mark#(first(X1, X2)) -> mark#(X1),
                   mark#(first(X1, X2)) -> mark#(X2),
                   mark#(first(X1, X2)) -> a__first#(mark(X1), mark(X2)),
            a__first#(s(X), cons(Y, Z)) -> mark#(Y)}
          Weak:
           {                 a__sqr(X) -> sqr(X),
                          a__sqr(s(X)) -> s(add(sqr(X), dbl(X))),
                           a__sqr(0()) -> 0(),
                    mark(cons(X1, X2)) -> cons(mark(X1), X2),
                        mark(recip(X)) -> recip(mark(X)),
                        mark(terms(X)) -> a__terms(mark(X)),
                            mark(s(X)) -> s(X),
                             mark(0()) -> 0(),
                     mark(add(X1, X2)) -> a__add(mark(X1), mark(X2)),
                          mark(sqr(X)) -> a__sqr(mark(X)),
                          mark(dbl(X)) -> a__dbl(mark(X)),
                           mark(nil()) -> nil(),
                   mark(first(X1, X2)) -> a__first(mark(X1), mark(X2)),
                           a__terms(N) -> cons(recip(a__sqr(mark(N))), terms(s(N))),
                           a__terms(X) -> terms(X),
                             a__dbl(X) -> dbl(X),
                          a__dbl(s(X)) -> s(s(dbl(X))),
                           a__dbl(0()) -> 0(),
                        a__add(X1, X2) -> add(X1, X2),
                       a__add(s(X), Y) -> s(add(X, Y)),
                        a__add(0(), X) -> mark(X),
                      a__first(X1, X2) -> first(X1, X2),
            a__first(s(X), cons(Y, Z)) -> cons(mark(Y), first(X, Z)),
                      a__first(0(), X) -> nil()}
          EDG:
           {(mark#(first(X1, X2)) -> mark#(X1), mark#(first(X1, X2)) -> a__first#(mark(X1), mark(X2)))
            (mark#(first(X1, X2)) -> mark#(X1), mark#(first(X1, X2)) -> mark#(X2))
            (mark#(first(X1, X2)) -> mark#(X1), mark#(first(X1, X2)) -> mark#(X1))
            (mark#(first(X1, X2)) -> mark#(X1), mark#(dbl(X)) -> mark#(X))
            (mark#(first(X1, X2)) -> mark#(X1), mark#(sqr(X)) -> mark#(X))
            (mark#(first(X1, X2)) -> mark#(X1), mark#(terms(X)) -> a__terms#(mark(X)))
            (mark#(first(X1, X2)) -> mark#(X1), mark#(recip(X)) -> mark#(X))
            (mark#(first(X1, X2)) -> mark#(X1), mark#(cons(X1, X2)) -> mark#(X1))
            (mark#(sqr(X)) -> mark#(X), mark#(first(X1, X2)) -> a__first#(mark(X1), mark(X2)))
            (mark#(sqr(X)) -> mark#(X), mark#(first(X1, X2)) -> mark#(X2))
            (mark#(sqr(X)) -> mark#(X), mark#(first(X1, X2)) -> mark#(X1))
            (mark#(sqr(X)) -> mark#(X), mark#(dbl(X)) -> mark#(X))
            (mark#(sqr(X)) -> mark#(X), mark#(sqr(X)) -> mark#(X))
            (mark#(sqr(X)) -> mark#(X), mark#(terms(X)) -> a__terms#(mark(X)))
            (mark#(sqr(X)) -> mark#(X), mark#(recip(X)) -> mark#(X))
            (mark#(sqr(X)) -> mark#(X), mark#(cons(X1, X2)) -> mark#(X1))
            (a__first#(s(X), cons(Y, Z)) -> mark#(Y), mark#(first(X1, X2)) -> a__first#(mark(X1), mark(X2)))
            (a__first#(s(X), cons(Y, Z)) -> mark#(Y), mark#(first(X1, X2)) -> mark#(X2))
            (a__first#(s(X), cons(Y, Z)) -> mark#(Y), mark#(first(X1, X2)) -> mark#(X1))
            (a__first#(s(X), cons(Y, Z)) -> mark#(Y), mark#(dbl(X)) -> mark#(X))
            (a__first#(s(X), cons(Y, Z)) -> mark#(Y), mark#(sqr(X)) -> mark#(X))
            (a__first#(s(X), cons(Y, Z)) -> mark#(Y), mark#(terms(X)) -> a__terms#(mark(X)))
            (a__first#(s(X), cons(Y, Z)) -> mark#(Y), mark#(recip(X)) -> mark#(X))
            (a__first#(s(X), cons(Y, Z)) -> mark#(Y), mark#(cons(X1, X2)) -> mark#(X1))
            (mark#(first(X1, X2)) -> a__first#(mark(X1), mark(X2)), a__first#(s(X), cons(Y, Z)) -> mark#(Y))
            (mark#(first(X1, X2)) -> mark#(X2), mark#(cons(X1, X2)) -> mark#(X1))
            (mark#(first(X1, X2)) -> mark#(X2), mark#(recip(X)) -> mark#(X))
            (mark#(first(X1, X2)) -> mark#(X2), mark#(terms(X)) -> a__terms#(mark(X)))
            (mark#(first(X1, X2)) -> mark#(X2), mark#(sqr(X)) -> mark#(X))
            (mark#(first(X1, X2)) -> mark#(X2), mark#(dbl(X)) -> mark#(X))
            (mark#(first(X1, X2)) -> mark#(X2), mark#(first(X1, X2)) -> mark#(X1))
            (mark#(first(X1, X2)) -> mark#(X2), mark#(first(X1, X2)) -> mark#(X2))
            (mark#(first(X1, X2)) -> mark#(X2), mark#(first(X1, X2)) -> a__first#(mark(X1), mark(X2)))
            (mark#(dbl(X)) -> mark#(X), mark#(cons(X1, X2)) -> mark#(X1))
            (mark#(dbl(X)) -> mark#(X), mark#(recip(X)) -> mark#(X))
            (mark#(dbl(X)) -> mark#(X), mark#(terms(X)) -> a__terms#(mark(X)))
            (mark#(dbl(X)) -> mark#(X), mark#(sqr(X)) -> mark#(X))
            (mark#(dbl(X)) -> mark#(X), mark#(dbl(X)) -> mark#(X))
            (mark#(dbl(X)) -> mark#(X), mark#(first(X1, X2)) -> mark#(X1))
            (mark#(dbl(X)) -> mark#(X), mark#(first(X1, X2)) -> mark#(X2))
            (mark#(dbl(X)) -> mark#(X), mark#(first(X1, X2)) -> a__first#(mark(X1), mark(X2)))
            (mark#(recip(X)) -> mark#(X), mark#(cons(X1, X2)) -> mark#(X1))
            (mark#(recip(X)) -> mark#(X), mark#(recip(X)) -> mark#(X))
            (mark#(recip(X)) -> mark#(X), mark#(terms(X)) -> a__terms#(mark(X)))
            (mark#(recip(X)) -> mark#(X), mark#(sqr(X)) -> mark#(X))
            (mark#(recip(X)) -> mark#(X), mark#(dbl(X)) -> mark#(X))
            (mark#(recip(X)) -> mark#(X), mark#(first(X1, X2)) -> mark#(X1))
            (mark#(recip(X)) -> mark#(X), mark#(first(X1, X2)) -> mark#(X2))
            (mark#(recip(X)) -> mark#(X), mark#(first(X1, X2)) -> a__first#(mark(X1), mark(X2)))
            (mark#(cons(X1, X2)) -> mark#(X1), mark#(cons(X1, X2)) -> mark#(X1))
            (mark#(cons(X1, X2)) -> mark#(X1), mark#(recip(X)) -> mark#(X))
            (mark#(cons(X1, X2)) -> mark#(X1), mark#(terms(X)) -> a__terms#(mark(X)))
            (mark#(cons(X1, X2)) -> mark#(X1), mark#(sqr(X)) -> mark#(X))
            (mark#(cons(X1, X2)) -> mark#(X1), mark#(dbl(X)) -> mark#(X))
            (mark#(cons(X1, X2)) -> mark#(X1), mark#(first(X1, X2)) -> mark#(X1))
            (mark#(cons(X1, X2)) -> mark#(X1), mark#(first(X1, X2)) -> mark#(X2))
            (mark#(cons(X1, X2)) -> mark#(X1), mark#(first(X1, X2)) -> a__first#(mark(X1), mark(X2)))}
           SCCS:
            Scc:
             {        mark#(cons(X1, X2)) -> mark#(X1),
                          mark#(recip(X)) -> mark#(X),
                            mark#(sqr(X)) -> mark#(X),
                            mark#(dbl(X)) -> mark#(X),
                     mark#(first(X1, X2)) -> mark#(X1),
                     mark#(first(X1, X2)) -> mark#(X2),
                     mark#(first(X1, X2)) -> a__first#(mark(X1), mark(X2)),
              a__first#(s(X), cons(Y, Z)) -> mark#(Y)}
            SCC:
             Strict:
              {        mark#(cons(X1, X2)) -> mark#(X1),
                           mark#(recip(X)) -> mark#(X),
                             mark#(sqr(X)) -> mark#(X),
                             mark#(dbl(X)) -> mark#(X),
                      mark#(first(X1, X2)) -> mark#(X1),
                      mark#(first(X1, X2)) -> mark#(X2),
                      mark#(first(X1, X2)) -> a__first#(mark(X1), mark(X2)),
               a__first#(s(X), cons(Y, Z)) -> mark#(Y)}
             Weak:
             {                 a__sqr(X) -> sqr(X),
                            a__sqr(s(X)) -> s(add(sqr(X), dbl(X))),
                             a__sqr(0()) -> 0(),
                      mark(cons(X1, X2)) -> cons(mark(X1), X2),
                          mark(recip(X)) -> recip(mark(X)),
                          mark(terms(X)) -> a__terms(mark(X)),
                              mark(s(X)) -> s(X),
                               mark(0()) -> 0(),
                       mark(add(X1, X2)) -> a__add(mark(X1), mark(X2)),
                            mark(sqr(X)) -> a__sqr(mark(X)),
                            mark(dbl(X)) -> a__dbl(mark(X)),
                             mark(nil()) -> nil(),
                     mark(first(X1, X2)) -> a__first(mark(X1), mark(X2)),
                             a__terms(N) -> cons(recip(a__sqr(mark(N))), terms(s(N))),
                             a__terms(X) -> terms(X),
                               a__dbl(X) -> dbl(X),
                            a__dbl(s(X)) -> s(s(dbl(X))),
                             a__dbl(0()) -> 0(),
                          a__add(X1, X2) -> add(X1, X2),
                         a__add(s(X), Y) -> s(add(X, Y)),
                          a__add(0(), X) -> mark(X),
                        a__first(X1, X2) -> first(X1, X2),
              a__first(s(X), cons(Y, Z)) -> cons(mark(Y), first(X, Z)),
                        a__first(0(), X) -> nil()}
             POLY:
              Argument Filtering:
               pi(first) = [0,1], pi(a__first#) = 1, pi(a__first) = [0,1], pi(nil) = [], pi(a__add) = 1, pi(a__dbl) = [0], pi(dbl) = [0], pi(sqr) = 0, pi(add) = 1, pi(0) = [], pi(a__terms) = 0, pi(s) = [], pi(terms) = 0, pi(mark#) = 0, pi(mark) = 0, pi(a__sqr) = 0, pi(recip) = 0, pi(cons) = 0
              Usable Rules:
               {}
              Interpretation:
               [first](x0, x1) = x0 + x1,
               [dbl](x0) = x0 + 1
              Strict:
               {        mark#(cons(X1, X2)) -> mark#(X1),
                            mark#(recip(X)) -> mark#(X),
                              mark#(sqr(X)) -> mark#(X),
                       mark#(first(X1, X2)) -> mark#(X1),
                       mark#(first(X1, X2)) -> mark#(X2),
                       mark#(first(X1, X2)) -> a__first#(mark(X1), mark(X2)),
                a__first#(s(X), cons(Y, Z)) -> mark#(Y)}
              Weak:
               {                 a__sqr(X) -> sqr(X),
                              a__sqr(s(X)) -> s(add(sqr(X), dbl(X))),
                               a__sqr(0()) -> 0(),
                        mark(cons(X1, X2)) -> cons(mark(X1), X2),
                            mark(recip(X)) -> recip(mark(X)),
                            mark(terms(X)) -> a__terms(mark(X)),
                                mark(s(X)) -> s(X),
                                 mark(0()) -> 0(),
                         mark(add(X1, X2)) -> a__add(mark(X1), mark(X2)),
                              mark(sqr(X)) -> a__sqr(mark(X)),
                              mark(dbl(X)) -> a__dbl(mark(X)),
                               mark(nil()) -> nil(),
                       mark(first(X1, X2)) -> a__first(mark(X1), mark(X2)),
                               a__terms(N) -> cons(recip(a__sqr(mark(N))), terms(s(N))),
                               a__terms(X) -> terms(X),
                                 a__dbl(X) -> dbl(X),
                              a__dbl(s(X)) -> s(s(dbl(X))),
                               a__dbl(0()) -> 0(),
                            a__add(X1, X2) -> add(X1, X2),
                           a__add(s(X), Y) -> s(add(X, Y)),
                            a__add(0(), X) -> mark(X),
                          a__first(X1, X2) -> first(X1, X2),
                a__first(s(X), cons(Y, Z)) -> cons(mark(Y), first(X, Z)),
                          a__first(0(), X) -> nil()}
              EDG:
               {(mark#(first(X1, X2)) -> a__first#(mark(X1), mark(X2)), a__first#(s(X), cons(Y, Z)) -> mark#(Y))
                (mark#(first(X1, X2)) -> mark#(X1), mark#(first(X1, X2)) -> a__first#(mark(X1), mark(X2)))
                (mark#(first(X1, X2)) -> mark#(X1), mark#(first(X1, X2)) -> mark#(X2))
                (mark#(first(X1, X2)) -> mark#(X1), mark#(first(X1, X2)) -> mark#(X1))
                (mark#(first(X1, X2)) -> mark#(X1), mark#(sqr(X)) -> mark#(X))
                (mark#(first(X1, X2)) -> mark#(X1), mark#(recip(X)) -> mark#(X))
                (mark#(first(X1, X2)) -> mark#(X1), mark#(cons(X1, X2)) -> mark#(X1))
                (mark#(recip(X)) -> mark#(X), mark#(first(X1, X2)) -> a__first#(mark(X1), mark(X2)))
                (mark#(recip(X)) -> mark#(X), mark#(first(X1, X2)) -> mark#(X2))
                (mark#(recip(X)) -> mark#(X), mark#(first(X1, X2)) -> mark#(X1))
                (mark#(recip(X)) -> mark#(X), mark#(sqr(X)) -> mark#(X))
                (mark#(recip(X)) -> mark#(X), mark#(recip(X)) -> mark#(X))
                (mark#(recip(X)) -> mark#(X), mark#(cons(X1, X2)) -> mark#(X1))
                (mark#(sqr(X)) -> mark#(X), mark#(cons(X1, X2)) -> mark#(X1))
                (mark#(sqr(X)) -> mark#(X), mark#(recip(X)) -> mark#(X))
                (mark#(sqr(X)) -> mark#(X), mark#(sqr(X)) -> mark#(X))
                (mark#(sqr(X)) -> mark#(X), mark#(first(X1, X2)) -> mark#(X1))
                (mark#(sqr(X)) -> mark#(X), mark#(first(X1, X2)) -> mark#(X2))
                (mark#(sqr(X)) -> mark#(X), mark#(first(X1, X2)) -> a__first#(mark(X1), mark(X2)))
                (a__first#(s(X), cons(Y, Z)) -> mark#(Y), mark#(cons(X1, X2)) -> mark#(X1))
                (a__first#(s(X), cons(Y, Z)) -> mark#(Y), mark#(recip(X)) -> mark#(X))
                (a__first#(s(X), cons(Y, Z)) -> mark#(Y), mark#(sqr(X)) -> mark#(X))
                (a__first#(s(X), cons(Y, Z)) -> mark#(Y), mark#(first(X1, X2)) -> mark#(X1))
                (a__first#(s(X), cons(Y, Z)) -> mark#(Y), mark#(first(X1, X2)) -> mark#(X2))
                (a__first#(s(X), cons(Y, Z)) -> mark#(Y), mark#(first(X1, X2)) -> a__first#(mark(X1), mark(X2)))
                (mark#(cons(X1, X2)) -> mark#(X1), mark#(cons(X1, X2)) -> mark#(X1))
                (mark#(cons(X1, X2)) -> mark#(X1), mark#(recip(X)) -> mark#(X))
                (mark#(cons(X1, X2)) -> mark#(X1), mark#(sqr(X)) -> mark#(X))
                (mark#(cons(X1, X2)) -> mark#(X1), mark#(first(X1, X2)) -> mark#(X1))
                (mark#(cons(X1, X2)) -> mark#(X1), mark#(first(X1, X2)) -> mark#(X2))
                (mark#(cons(X1, X2)) -> mark#(X1), mark#(first(X1, X2)) -> a__first#(mark(X1), mark(X2)))
                (mark#(first(X1, X2)) -> mark#(X2), mark#(cons(X1, X2)) -> mark#(X1))
                (mark#(first(X1, X2)) -> mark#(X2), mark#(recip(X)) -> mark#(X))
                (mark#(first(X1, X2)) -> mark#(X2), mark#(sqr(X)) -> mark#(X))
                (mark#(first(X1, X2)) -> mark#(X2), mark#(first(X1, X2)) -> mark#(X1))
                (mark#(first(X1, X2)) -> mark#(X2), mark#(first(X1, X2)) -> mark#(X2))
                (mark#(first(X1, X2)) -> mark#(X2), mark#(first(X1, X2)) -> a__first#(mark(X1), mark(X2)))}
               SCCS:
                Scc:
                 {        mark#(cons(X1, X2)) -> mark#(X1),
                              mark#(recip(X)) -> mark#(X),
                                mark#(sqr(X)) -> mark#(X),
                         mark#(first(X1, X2)) -> mark#(X1),
                         mark#(first(X1, X2)) -> mark#(X2),
                         mark#(first(X1, X2)) -> a__first#(mark(X1), mark(X2)),
                  a__first#(s(X), cons(Y, Z)) -> mark#(Y)}
                SCC:
                 Strict:
                  {        mark#(cons(X1, X2)) -> mark#(X1),
                               mark#(recip(X)) -> mark#(X),
                                 mark#(sqr(X)) -> mark#(X),
                          mark#(first(X1, X2)) -> mark#(X1),
                          mark#(first(X1, X2)) -> mark#(X2),
                          mark#(first(X1, X2)) -> a__first#(mark(X1), mark(X2)),
                   a__first#(s(X), cons(Y, Z)) -> mark#(Y)}
                 Weak:
                 {                 a__sqr(X) -> sqr(X),
                                a__sqr(s(X)) -> s(add(sqr(X), dbl(X))),
                                 a__sqr(0()) -> 0(),
                          mark(cons(X1, X2)) -> cons(mark(X1), X2),
                              mark(recip(X)) -> recip(mark(X)),
                              mark(terms(X)) -> a__terms(mark(X)),
                                  mark(s(X)) -> s(X),
                                   mark(0()) -> 0(),
                           mark(add(X1, X2)) -> a__add(mark(X1), mark(X2)),
                                mark(sqr(X)) -> a__sqr(mark(X)),
                                mark(dbl(X)) -> a__dbl(mark(X)),
                                 mark(nil()) -> nil(),
                         mark(first(X1, X2)) -> a__first(mark(X1), mark(X2)),
                                 a__terms(N) -> cons(recip(a__sqr(mark(N))), terms(s(N))),
                                 a__terms(X) -> terms(X),
                                   a__dbl(X) -> dbl(X),
                                a__dbl(s(X)) -> s(s(dbl(X))),
                                 a__dbl(0()) -> 0(),
                              a__add(X1, X2) -> add(X1, X2),
                             a__add(s(X), Y) -> s(add(X, Y)),
                              a__add(0(), X) -> mark(X),
                            a__first(X1, X2) -> first(X1, X2),
                  a__first(s(X), cons(Y, Z)) -> cons(mark(Y), first(X, Z)),
                            a__first(0(), X) -> nil()}
                 POLY:
                  Argument Filtering:
                   pi(first) = [0,1], pi(a__first#) = 1, pi(a__first) = [0,1], pi(nil) = [], pi(a__add) = 1, pi(a__dbl) = [], pi(dbl) = [], pi(sqr) = 0, pi(add) = 1, pi(0) = [], pi(a__terms) = [0], pi(s) = [], pi(terms) = [0], pi(mark#) = 0, pi(mark) = 0, pi(a__sqr) = 0, pi(recip) = [0], pi(cons) = 0
                  Usable Rules:
                   {}
                  Interpretation:
                   [first](x0, x1) = x0 + x1,
                   [recip](x0) = x0 + 1
                  Strict:
                   {        mark#(cons(X1, X2)) -> mark#(X1),
                                  mark#(sqr(X)) -> mark#(X),
                           mark#(first(X1, X2)) -> mark#(X1),
                           mark#(first(X1, X2)) -> mark#(X2),
                           mark#(first(X1, X2)) -> a__first#(mark(X1), mark(X2)),
                    a__first#(s(X), cons(Y, Z)) -> mark#(Y)}
                  Weak:
                   {                 a__sqr(X) -> sqr(X),
                                  a__sqr(s(X)) -> s(add(sqr(X), dbl(X))),
                                   a__sqr(0()) -> 0(),
                            mark(cons(X1, X2)) -> cons(mark(X1), X2),
                                mark(recip(X)) -> recip(mark(X)),
                                mark(terms(X)) -> a__terms(mark(X)),
                                    mark(s(X)) -> s(X),
                                     mark(0()) -> 0(),
                             mark(add(X1, X2)) -> a__add(mark(X1), mark(X2)),
                                  mark(sqr(X)) -> a__sqr(mark(X)),
                                  mark(dbl(X)) -> a__dbl(mark(X)),
                                   mark(nil()) -> nil(),
                           mark(first(X1, X2)) -> a__first(mark(X1), mark(X2)),
                                   a__terms(N) -> cons(recip(a__sqr(mark(N))), terms(s(N))),
                                   a__terms(X) -> terms(X),
                                     a__dbl(X) -> dbl(X),
                                  a__dbl(s(X)) -> s(s(dbl(X))),
                                   a__dbl(0()) -> 0(),
                                a__add(X1, X2) -> add(X1, X2),
                               a__add(s(X), Y) -> s(add(X, Y)),
                                a__add(0(), X) -> mark(X),
                              a__first(X1, X2) -> first(X1, X2),
                    a__first(s(X), cons(Y, Z)) -> cons(mark(Y), first(X, Z)),
                              a__first(0(), X) -> nil()}
                  EDG:
                   {(mark#(first(X1, X2)) -> mark#(X1), mark#(first(X1, X2)) -> a__first#(mark(X1), mark(X2)))
                    (mark#(first(X1, X2)) -> mark#(X1), mark#(first(X1, X2)) -> mark#(X2))
                    (mark#(first(X1, X2)) -> mark#(X1), mark#(first(X1, X2)) -> mark#(X1))
                    (mark#(first(X1, X2)) -> mark#(X1), mark#(sqr(X)) -> mark#(X))
                    (mark#(first(X1, X2)) -> mark#(X1), mark#(cons(X1, X2)) -> mark#(X1))
                    (mark#(first(X1, X2)) -> mark#(X2), mark#(first(X1, X2)) -> a__first#(mark(X1), mark(X2)))
                    (mark#(first(X1, X2)) -> mark#(X2), mark#(first(X1, X2)) -> mark#(X2))
                    (mark#(first(X1, X2)) -> mark#(X2), mark#(first(X1, X2)) -> mark#(X1))
                    (mark#(first(X1, X2)) -> mark#(X2), mark#(sqr(X)) -> mark#(X))
                    (mark#(first(X1, X2)) -> mark#(X2), mark#(cons(X1, X2)) -> mark#(X1))
                    (mark#(sqr(X)) -> mark#(X), mark#(first(X1, X2)) -> a__first#(mark(X1), mark(X2)))
                    (mark#(sqr(X)) -> mark#(X), mark#(first(X1, X2)) -> mark#(X2))
                    (mark#(sqr(X)) -> mark#(X), mark#(first(X1, X2)) -> mark#(X1))
                    (mark#(sqr(X)) -> mark#(X), mark#(sqr(X)) -> mark#(X))
                    (mark#(sqr(X)) -> mark#(X), mark#(cons(X1, X2)) -> mark#(X1))
                    (mark#(first(X1, X2)) -> a__first#(mark(X1), mark(X2)), a__first#(s(X), cons(Y, Z)) -> mark#(Y))
                    (a__first#(s(X), cons(Y, Z)) -> mark#(Y), mark#(cons(X1, X2)) -> mark#(X1))
                    (a__first#(s(X), cons(Y, Z)) -> mark#(Y), mark#(sqr(X)) -> mark#(X))
                    (a__first#(s(X), cons(Y, Z)) -> mark#(Y), mark#(first(X1, X2)) -> mark#(X1))
                    (a__first#(s(X), cons(Y, Z)) -> mark#(Y), mark#(first(X1, X2)) -> mark#(X2))
                    (a__first#(s(X), cons(Y, Z)) -> mark#(Y), mark#(first(X1, X2)) -> a__first#(mark(X1), mark(X2)))
                    (mark#(cons(X1, X2)) -> mark#(X1), mark#(cons(X1, X2)) -> mark#(X1))
                    (mark#(cons(X1, X2)) -> mark#(X1), mark#(sqr(X)) -> mark#(X))
                    (mark#(cons(X1, X2)) -> mark#(X1), mark#(first(X1, X2)) -> mark#(X1))
                    (mark#(cons(X1, X2)) -> mark#(X1), mark#(first(X1, X2)) -> mark#(X2))
                    (mark#(cons(X1, X2)) -> mark#(X1), mark#(first(X1, X2)) -> a__first#(mark(X1), mark(X2)))}
                   SCCS:
                    Scc:
                     {        mark#(cons(X1, X2)) -> mark#(X1),
                                    mark#(sqr(X)) -> mark#(X),
                             mark#(first(X1, X2)) -> mark#(X1),
                             mark#(first(X1, X2)) -> mark#(X2),
                             mark#(first(X1, X2)) -> a__first#(mark(X1), mark(X2)),
                      a__first#(s(X), cons(Y, Z)) -> mark#(Y)}
                    SCC:
                     Strict:
                      {        mark#(cons(X1, X2)) -> mark#(X1),
                                     mark#(sqr(X)) -> mark#(X),
                              mark#(first(X1, X2)) -> mark#(X1),
                              mark#(first(X1, X2)) -> mark#(X2),
                              mark#(first(X1, X2)) -> a__first#(mark(X1), mark(X2)),
                       a__first#(s(X), cons(Y, Z)) -> mark#(Y)}
                     Weak:
                     {                 a__sqr(X) -> sqr(X),
                                    a__sqr(s(X)) -> s(add(sqr(X), dbl(X))),
                                     a__sqr(0()) -> 0(),
                              mark(cons(X1, X2)) -> cons(mark(X1), X2),
                                  mark(recip(X)) -> recip(mark(X)),
                                  mark(terms(X)) -> a__terms(mark(X)),
                                      mark(s(X)) -> s(X),
                                       mark(0()) -> 0(),
                               mark(add(X1, X2)) -> a__add(mark(X1), mark(X2)),
                                    mark(sqr(X)) -> a__sqr(mark(X)),
                                    mark(dbl(X)) -> a__dbl(mark(X)),
                                     mark(nil()) -> nil(),
                             mark(first(X1, X2)) -> a__first(mark(X1), mark(X2)),
                                     a__terms(N) -> cons(recip(a__sqr(mark(N))), terms(s(N))),
                                     a__terms(X) -> terms(X),
                                       a__dbl(X) -> dbl(X),
                                    a__dbl(s(X)) -> s(s(dbl(X))),
                                     a__dbl(0()) -> 0(),
                                  a__add(X1, X2) -> add(X1, X2),
                                 a__add(s(X), Y) -> s(add(X, Y)),
                                  a__add(0(), X) -> mark(X),
                                a__first(X1, X2) -> first(X1, X2),
                      a__first(s(X), cons(Y, Z)) -> cons(mark(Y), first(X, Z)),
                                a__first(0(), X) -> nil()}
                     POLY:
                      Argument Filtering:
                       pi(first) = [0,1], pi(a__first#) = [0,1], pi(a__first) = [0,1], pi(nil) = [], pi(a__add) = [0,1], pi(a__dbl) = 0, pi(dbl) = 0, pi(sqr) = 0, pi(add) = [0,1], pi(0) = [], pi(a__terms) = [], pi(s) = [], pi(terms) = [], pi(mark#) = [0], pi(mark) = 0, pi(a__sqr) = 0, pi(recip) = [], pi(cons) = [0]
                      Usable Rules:
                       {}
                      Interpretation:
                       [a__first#](x0, x1) = x0 + x1,
                       [mark#](x0) = x0 + 1,
                       [first](x0, x1) = x0 + x1 + 1,
                       [cons](x0) = x0 + 1,
                       [s] = 1
                      Strict:
                       {mark#(sqr(X)) -> mark#(X)}
                      Weak:
                       {                 a__sqr(X) -> sqr(X),
                                      a__sqr(s(X)) -> s(add(sqr(X), dbl(X))),
                                       a__sqr(0()) -> 0(),
                                mark(cons(X1, X2)) -> cons(mark(X1), X2),
                                    mark(recip(X)) -> recip(mark(X)),
                                    mark(terms(X)) -> a__terms(mark(X)),
                                        mark(s(X)) -> s(X),
                                         mark(0()) -> 0(),
                                 mark(add(X1, X2)) -> a__add(mark(X1), mark(X2)),
                                      mark(sqr(X)) -> a__sqr(mark(X)),
                                      mark(dbl(X)) -> a__dbl(mark(X)),
                                       mark(nil()) -> nil(),
                               mark(first(X1, X2)) -> a__first(mark(X1), mark(X2)),
                                       a__terms(N) -> cons(recip(a__sqr(mark(N))), terms(s(N))),
                                       a__terms(X) -> terms(X),
                                         a__dbl(X) -> dbl(X),
                                      a__dbl(s(X)) -> s(s(dbl(X))),
                                       a__dbl(0()) -> 0(),
                                    a__add(X1, X2) -> add(X1, X2),
                                   a__add(s(X), Y) -> s(add(X, Y)),
                                    a__add(0(), X) -> mark(X),
                                  a__first(X1, X2) -> first(X1, X2),
                        a__first(s(X), cons(Y, Z)) -> cons(mark(Y), first(X, Z)),
                                  a__first(0(), X) -> nil()}
                      EDG:
                       {(mark#(sqr(X)) -> mark#(X), mark#(sqr(X)) -> mark#(X))}
                       SCCS:
                        Scc:
                         {mark#(sqr(X)) -> mark#(X)}
                        SCC:
                         Strict:
                          {mark#(sqr(X)) -> mark#(X)}
                         Weak:
                         {                 a__sqr(X) -> sqr(X),
                                        a__sqr(s(X)) -> s(add(sqr(X), dbl(X))),
                                         a__sqr(0()) -> 0(),
                                  mark(cons(X1, X2)) -> cons(mark(X1), X2),
                                      mark(recip(X)) -> recip(mark(X)),
                                      mark(terms(X)) -> a__terms(mark(X)),
                                          mark(s(X)) -> s(X),
                                           mark(0()) -> 0(),
                                   mark(add(X1, X2)) -> a__add(mark(X1), mark(X2)),
                                        mark(sqr(X)) -> a__sqr(mark(X)),
                                        mark(dbl(X)) -> a__dbl(mark(X)),
                                         mark(nil()) -> nil(),
                                 mark(first(X1, X2)) -> a__first(mark(X1), mark(X2)),
                                         a__terms(N) -> cons(recip(a__sqr(mark(N))), terms(s(N))),
                                         a__terms(X) -> terms(X),
                                           a__dbl(X) -> dbl(X),
                                        a__dbl(s(X)) -> s(s(dbl(X))),
                                         a__dbl(0()) -> 0(),
                                      a__add(X1, X2) -> add(X1, X2),
                                     a__add(s(X), Y) -> s(add(X, Y)),
                                      a__add(0(), X) -> mark(X),
                                    a__first(X1, X2) -> first(X1, X2),
                          a__first(s(X), cons(Y, Z)) -> cons(mark(Y), first(X, Z)),
                                    a__first(0(), X) -> nil()}
                         SPSC:
                          Simple Projection:
                           pi(mark#) = 0
                          Strict:
                           {}
                          Qed