MAYBE
Time: 0.002454
TRS:
 {           sqr 0() -> 0(),
             sqr s X -> s add(sqr X, dbl X),
             terms N -> cons recip sqr N,
         add(0(), X) -> X,
         add(s X, Y) -> s add(X, Y),
             dbl 0() -> 0(),
             dbl s X -> s s dbl X,
       first(0(), X) -> nil(),
  first(s X, cons Y) -> cons Y,
            half 0() -> 0(),
          half s 0() -> 0(),
          half s s X -> s half X,
          half dbl X -> X}
 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,
     half# s s X -> half# X}
  TRS:
  {           sqr 0() -> 0(),
              sqr s X -> s add(sqr X, dbl X),
              terms N -> cons recip sqr N,
          add(0(), X) -> X,
          add(s X, Y) -> s add(X, Y),
              dbl 0() -> 0(),
              dbl s X -> s s dbl X,
        first(0(), X) -> nil(),
   first(s X, cons Y) -> cons Y,
             half 0() -> 0(),
           half s 0() -> 0(),
           half s s X -> s half X,
           half dbl X -> X}
  UR:
   {    sqr 0() -> 0(),
        sqr s X -> s add(sqr X, dbl X),
    add(0(), X) -> X,
    add(s X, Y) -> s add(X, Y),
        dbl 0() -> 0(),
        dbl s X -> s s dbl X}
   EDG:
    {(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)
     (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)
     (add#(s X, Y) -> add#(X, Y), add#(s X, Y) -> add#(X, Y))
     (half# s s X -> half# X, half# s s X -> half# X)
     (sqr# s X -> dbl# X, dbl# s X -> dbl# X)
     (sqr# s X -> add#(sqr X, dbl X), add#(s X, Y) -> add#(X, Y))}
    STATUS:
     arrows: 0.775510
     SCCS (4):
      Scc:
       {half# s s X -> half# X}
      Scc:
       {sqr# s X -> sqr# X}
      Scc:
       {dbl# s X -> dbl# X}
      Scc:
       {add#(s X, Y) -> add#(X, Y)}
      
      
      SCC (1):
       Strict:
        {half# s s X -> half# X}
       Weak:
       {           sqr 0() -> 0(),
                   sqr s X -> s add(sqr X, dbl X),
                   terms N -> cons recip sqr N,
               add(0(), X) -> X,
               add(s X, Y) -> s add(X, Y),
                   dbl 0() -> 0(),
                   dbl s X -> s s dbl X,
             first(0(), X) -> nil(),
        first(s X, cons Y) -> cons Y,
                  half 0() -> 0(),
                half s 0() -> 0(),
                half s s X -> s half X,
                half dbl X -> X}
       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,
               add(0(), X) -> X,
               add(s X, Y) -> s add(X, Y),
                   dbl 0() -> 0(),
                   dbl s X -> s s dbl X,
             first(0(), X) -> nil(),
        first(s X, cons Y) -> cons Y,
                  half 0() -> 0(),
                half s 0() -> 0(),
                half s s X -> s half X,
                half dbl X -> X}
       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,
               add(0(), X) -> X,
               add(s X, Y) -> s add(X, Y),
                   dbl 0() -> 0(),
                   dbl s X -> s s dbl X,
             first(0(), X) -> nil(),
        first(s X, cons Y) -> cons Y,
                  half 0() -> 0(),
                half s 0() -> 0(),
                half s s X -> s half X,
                half dbl X -> X}
       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,
               add(0(), X) -> X,
               add(s X, Y) -> s add(X, Y),
                   dbl 0() -> 0(),
                   dbl s X -> s s dbl X,
             first(0(), X) -> nil(),
        first(s X, cons Y) -> cons Y,
                  half 0() -> 0(),
                half s 0() -> 0(),
                half s s X -> s half X,
                half dbl X -> X}
       Open