MAYBE
TRS:
 {              sqr(s(X)) -> s(add(sqr(X), dbl(X))),
                 sqr(0()) -> 0(),
                 terms(N) -> cons(recip(sqr(N)), terms(s(N))),
             add(s(X), Y) -> s(add(X, Y)),
              add(0(), X) -> X,
                dbl(s(X)) -> s(s(dbl(X))),
                 dbl(0()) -> 0(),
  first(s(X), cons(Y, Z)) -> cons(Y, first(X, Z)),
            first(0(), X) -> nil()}
 DP:
  Strict:
   {              sqr#(s(X)) -> sqr#(X),
                  sqr#(s(X)) -> add#(sqr(X), dbl(X)),
                  sqr#(s(X)) -> dbl#(X),
                   terms#(N) -> sqr#(N),
                   terms#(N) -> terms#(s(N)),
               add#(s(X), Y) -> add#(X, Y),
                  dbl#(s(X)) -> dbl#(X),
    first#(s(X), cons(Y, Z)) -> first#(X, Z)}
  Weak:
  {              sqr(s(X)) -> s(add(sqr(X), dbl(X))),
                  sqr(0()) -> 0(),
                  terms(N) -> cons(recip(sqr(N)), terms(s(N))),
              add(s(X), Y) -> s(add(X, Y)),
               add(0(), X) -> X,
                 dbl(s(X)) -> s(s(dbl(X))),
                  dbl(0()) -> 0(),
   first(s(X), cons(Y, Z)) -> cons(Y, first(X, Z)),
             first(0(), X) -> nil()}
  EDG:
   {(sqr#(s(X)) -> dbl#(X), dbl#(s(X)) -> dbl#(X))
    (add#(s(X), Y) -> add#(X, Y), add#(s(X), Y) -> add#(X, Y))
    (terms#(N) -> sqr#(N), sqr#(s(X)) -> dbl#(X))
    (terms#(N) -> sqr#(N), sqr#(s(X)) -> add#(sqr(X), dbl(X)))
    (terms#(N) -> sqr#(N), sqr#(s(X)) -> sqr#(X))
    (first#(s(X), cons(Y, Z)) -> first#(X, Z), first#(s(X), cons(Y, Z)) -> first#(X, Z))
    (sqr#(s(X)) -> add#(sqr(X), dbl(X)), add#(s(X), Y) -> add#(X, Y))
    (terms#(N) -> terms#(s(N)), terms#(N) -> sqr#(N))
    (terms#(N) -> terms#(s(N)), terms#(N) -> terms#(s(N)))
    (dbl#(s(X)) -> dbl#(X), dbl#(s(X)) -> dbl#(X))
    (sqr#(s(X)) -> sqr#(X), sqr#(s(X)) -> sqr#(X))
    (sqr#(s(X)) -> sqr#(X), sqr#(s(X)) -> add#(sqr(X), dbl(X)))
    (sqr#(s(X)) -> sqr#(X), sqr#(s(X)) -> dbl#(X))}
   SCCS:
    Scc:
     {first#(s(X), cons(Y, Z)) -> first#(X, Z)}
    Scc:
     {dbl#(s(X)) -> dbl#(X)}
    Scc:
     {add#(s(X), Y) -> add#(X, Y)}
    Scc:
     {terms#(N) -> terms#(s(N))}
    Scc:
     {sqr#(s(X)) -> sqr#(X)}
    SCC:
     Strict:
      {first#(s(X), cons(Y, Z)) -> first#(X, Z)}
     Weak:
     {              sqr(s(X)) -> s(add(sqr(X), dbl(X))),
                     sqr(0()) -> 0(),
                     terms(N) -> cons(recip(sqr(N)), terms(s(N))),
                 add(s(X), Y) -> s(add(X, Y)),
                  add(0(), X) -> X,
                    dbl(s(X)) -> s(s(dbl(X))),
                     dbl(0()) -> 0(),
      first(s(X), cons(Y, Z)) -> cons(Y, first(X, Z)),
                first(0(), X) -> nil()}
     SPSC:
      Simple Projection:
       pi(first#) = 0
      Strict:
       {}
      Qed
    SCC:
     Strict:
      {dbl#(s(X)) -> dbl#(X)}
     Weak:
     {              sqr(s(X)) -> s(add(sqr(X), dbl(X))),
                     sqr(0()) -> 0(),
                     terms(N) -> cons(recip(sqr(N)), terms(s(N))),
                 add(s(X), Y) -> s(add(X, Y)),
                  add(0(), X) -> X,
                    dbl(s(X)) -> s(s(dbl(X))),
                     dbl(0()) -> 0(),
      first(s(X), cons(Y, Z)) -> cons(Y, first(X, Z)),
                first(0(), X) -> nil()}
     SPSC:
      Simple Projection:
       pi(dbl#) = 0
      Strict:
       {}
      Qed
    SCC:
     Strict:
      {add#(s(X), Y) -> add#(X, Y)}
     Weak:
     {              sqr(s(X)) -> s(add(sqr(X), dbl(X))),
                     sqr(0()) -> 0(),
                     terms(N) -> cons(recip(sqr(N)), terms(s(N))),
                 add(s(X), Y) -> s(add(X, Y)),
                  add(0(), X) -> X,
                    dbl(s(X)) -> s(s(dbl(X))),
                     dbl(0()) -> 0(),
      first(s(X), cons(Y, Z)) -> cons(Y, first(X, Z)),
                first(0(), X) -> nil()}
     SPSC:
      Simple Projection:
       pi(add#) = 0
      Strict:
       {}
      Qed
    SCC:
     Strict:
      {terms#(N) -> terms#(s(N))}
     Weak:
     {              sqr(s(X)) -> s(add(sqr(X), dbl(X))),
                     sqr(0()) -> 0(),
                     terms(N) -> cons(recip(sqr(N)), terms(s(N))),
                 add(s(X), Y) -> s(add(X, Y)),
                  add(0(), X) -> X,
                    dbl(s(X)) -> s(s(dbl(X))),
                     dbl(0()) -> 0(),
      first(s(X), cons(Y, Z)) -> cons(Y, first(X, Z)),
                first(0(), X) -> nil()}
     Fail
    SCC:
     Strict:
      {sqr#(s(X)) -> sqr#(X)}
     Weak:
     {              sqr(s(X)) -> s(add(sqr(X), dbl(X))),
                     sqr(0()) -> 0(),
                     terms(N) -> cons(recip(sqr(N)), terms(s(N))),
                 add(s(X), Y) -> s(add(X, Y)),
                  add(0(), X) -> X,
                    dbl(s(X)) -> s(s(dbl(X))),
                     dbl(0()) -> 0(),
      first(s(X), cons(Y, Z)) -> cons(Y, first(X, Z)),
                first(0(), X) -> nil()}
     SPSC:
      Simple Projection:
       pi(sqr#) = 0
      Strict:
       {}
      Qed