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