MAYBE
Time: 0.005156
TRS:
 {                  sqr s X -> s add(sqr X, dbl X),
                    sqr 0() -> 0(),
                    terms N -> cons(recip sqr N, n__terms s N),
                    terms X -> n__terms X,
                add(s X, Y) -> s add(X, Y),
                add(0(), X) -> X,
                    dbl s X -> s s dbl X,
                    dbl 0() -> 0(),
              first(X1, X2) -> n__first(X1, X2),
     first(s X, cons(Y, Z)) -> cons(Y, n__first(X, activate Z)),
              first(0(), X) -> nil(),
                 activate X -> X,
        activate n__terms X -> terms X,
  activate n__first(X1, X2) -> first(X1, X2)}
 DP:
  DP:
   {                  sqr# s X -> sqr# X,
                      sqr# s X -> add#(sqr X, dbl X),
                      sqr# s X -> dbl# X,
                      terms# N -> sqr# N,
                  add#(s X, Y) -> add#(X, Y),
                      dbl# s X -> dbl# X,
       first#(s X, cons(Y, Z)) -> activate# Z,
          activate# n__terms X -> terms# X,
    activate# n__first(X1, X2) -> first#(X1, X2)}
  TRS:
  {                  sqr s X -> s add(sqr X, dbl X),
                     sqr 0() -> 0(),
                     terms N -> cons(recip sqr N, n__terms s N),
                     terms X -> n__terms X,
                 add(s X, Y) -> s add(X, Y),
                 add(0(), X) -> X,
                     dbl s X -> s s dbl X,
                     dbl 0() -> 0(),
               first(X1, X2) -> n__first(X1, X2),
      first(s X, cons(Y, Z)) -> cons(Y, n__first(X, activate Z)),
               first(0(), X) -> nil(),
                  activate X -> X,
         activate n__terms X -> terms X,
   activate n__first(X1, X2) -> first(X1, X2)}
  EDG:
   {(activate# n__first(X1, X2) -> first#(X1, X2), first#(s X, cons(Y, Z)) -> activate# Z)
    (sqr# s X -> sqr# X, sqr# s X -> dbl# X)
    (sqr# s X -> sqr# X, sqr# s X -> add#(sqr X, dbl X))
    (sqr# s X -> sqr# X, sqr# s X -> sqr# X)
    (dbl# s X -> dbl# X, dbl# s X -> dbl# X)
    (first#(s X, cons(Y, Z)) -> activate# Z, activate# n__first(X1, X2) -> first#(X1, X2))
    (first#(s X, cons(Y, Z)) -> activate# Z, activate# n__terms X -> terms# X)
    (sqr# s X -> add#(sqr X, dbl X), add#(s X, Y) -> add#(X, Y))
    (activate# n__terms X -> terms# X, terms# N -> sqr# N)
    (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 -> sqr# X)
    (terms# N -> sqr# N, sqr# s X -> add#(sqr X, dbl X))
    (terms# N -> sqr# N, sqr# s X -> dbl# X)}
   EDG:
    {(activate# n__first(X1, X2) -> first#(X1, X2), first#(s X, cons(Y, Z)) -> activate# Z)
     (sqr# s X -> sqr# X, sqr# s X -> dbl# X)
     (sqr# s X -> sqr# X, sqr# s X -> add#(sqr X, dbl X))
     (sqr# s X -> sqr# X, sqr# s X -> sqr# X)
     (dbl# s X -> dbl# X, dbl# s X -> dbl# X)
     (first#(s X, cons(Y, Z)) -> activate# Z, activate# n__first(X1, X2) -> first#(X1, X2))
     (first#(s X, cons(Y, Z)) -> activate# Z, activate# n__terms X -> terms# X)
     (sqr# s X -> add#(sqr X, dbl X), add#(s X, Y) -> add#(X, Y))
     (activate# n__terms X -> terms# X, terms# N -> sqr# N)
     (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 -> sqr# X)
     (terms# N -> sqr# N, sqr# s X -> add#(sqr X, dbl X))
     (terms# N -> sqr# N, sqr# s X -> dbl# X)}
    EDG:
     {(activate# n__first(X1, X2) -> first#(X1, X2), first#(s X, cons(Y, Z)) -> activate# Z)
      (sqr# s X -> sqr# X, sqr# s X -> dbl# X)
      (sqr# s X -> sqr# X, sqr# s X -> add#(sqr X, dbl X))
      (sqr# s X -> sqr# X, sqr# s X -> sqr# X)
      (dbl# s X -> dbl# X, dbl# s X -> dbl# X)
      (first#(s X, cons(Y, Z)) -> activate# Z, activate# n__first(X1, X2) -> first#(X1, X2))
      (first#(s X, cons(Y, Z)) -> activate# Z, activate# n__terms X -> terms# X)
      (sqr# s X -> add#(sqr X, dbl X), add#(s X, Y) -> add#(X, Y))
      (activate# n__terms X -> terms# X, terms# N -> sqr# N)
      (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 -> sqr# X)
      (terms# N -> sqr# N, sqr# s X -> add#(sqr X, dbl X))
      (terms# N -> sqr# N, sqr# s X -> dbl# X)}
     STATUS:
      arrows: 0.827160
      SCCS (4):
       Scc:
        {   first#(s X, cons(Y, Z)) -> activate# Z,
         activate# n__first(X1, X2) -> first#(X1, X2)}
       Scc:
        {sqr# s X -> sqr# X}
       Scc:
        {dbl# s X -> dbl# X}
       Scc:
        {add#(s X, Y) -> add#(X, Y)}
       
       SCC (2):
        Strict:
         {   first#(s X, cons(Y, Z)) -> activate# Z,
          activate# n__first(X1, X2) -> first#(X1, X2)}
        Weak:
        {                  sqr s X -> s add(sqr X, dbl X),
                           sqr 0() -> 0(),
                           terms N -> cons(recip sqr N, n__terms s N),
                           terms X -> n__terms X,
                       add(s X, Y) -> s add(X, Y),
                       add(0(), X) -> X,
                           dbl s X -> s s dbl X,
                           dbl 0() -> 0(),
                     first(X1, X2) -> n__first(X1, X2),
            first(s X, cons(Y, Z)) -> cons(Y, n__first(X, activate Z)),
                     first(0(), X) -> nil(),
                        activate X -> X,
               activate n__terms X -> terms X,
         activate n__first(X1, X2) -> first(X1, X2)}
        Open
       
       
       SCC (1):
        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, n__terms s N),
                           terms X -> n__terms X,
                       add(s X, Y) -> s add(X, Y),
                       add(0(), X) -> X,
                           dbl s X -> s s dbl X,
                           dbl 0() -> 0(),
                     first(X1, X2) -> n__first(X1, X2),
            first(s X, cons(Y, Z)) -> cons(Y, n__first(X, activate Z)),
                     first(0(), X) -> nil(),
                        activate X -> X,
               activate n__terms X -> terms X,
         activate n__first(X1, X2) -> first(X1, X2)}
        Open
       
       SCC (1):
        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, n__terms s N),
                           terms X -> n__terms X,
                       add(s X, Y) -> s add(X, Y),
                       add(0(), X) -> X,
                           dbl s X -> s s dbl X,
                           dbl 0() -> 0(),
                     first(X1, X2) -> n__first(X1, X2),
            first(s X, cons(Y, Z)) -> cons(Y, n__first(X, activate Z)),
                     first(0(), X) -> nil(),
                        activate X -> X,
               activate n__terms X -> terms X,
         activate n__first(X1, X2) -> first(X1, X2)}
        Open
       
       SCC (1):
        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, n__terms s N),
                           terms X -> n__terms X,
                       add(s X, Y) -> s add(X, Y),
                       add(0(), X) -> X,
                           dbl s X -> s s dbl X,
                           dbl 0() -> 0(),
                     first(X1, X2) -> n__first(X1, X2),
            first(s X, cons(Y, Z)) -> cons(Y, n__first(X, activate Z)),
                     first(0(), X) -> nil(),
                        activate X -> X,
               activate n__terms X -> terms X,
         activate n__first(X1, X2) -> first(X1, X2)}
        Open