YES
Time: 0.034232
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}
 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}
  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}
  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)
    (sqr# s X -> add#(sqr X, dbl X), add#(s X, Y) -> add#(X, Y))
    (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)}
   STATUS:
    arrows: 0.722222
    SCCS (3):
     Scc:
      {sqr# s X -> sqr# X}
     Scc:
      {dbl# s X -> dbl# X}
     Scc:
      {add#(s X, Y) -> add#(X, Y)}
     
     
     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}
      POLY:
       Mode: weak, max_in=1, output_bits=-1, dnum=1, ur=true
       Interpretation:
        [add](x0, x1) = 0,
        
        [first](x0, x1) = x0 + 1,
        
        [cons](x0) = 0,
        
        [recip](x0) = 0,
        
        [sqr](x0) = x0 + 1,
        
        [terms](x0) = 0,
        
        [s](x0) = x0 + 1,
        
        [dbl](x0) = x0 + 1,
        
        [0] = 1,
        
        [nil] = 0,
        
        [sqr#](x0) = x0
       Strict:
        sqr# s X -> sqr# X
        1 + 1X >= 0 + 1X
       Weak:
        first(s X, cons Y) -> cons Y
        2 + 1X + 0Y >= 0 + 0Y
        first(0(), X) -> nil()
        2 + 0X >= 0
        dbl s X -> s s dbl X
        2 + 1X >= 3 + 1X
        dbl 0() -> 0()
        2 >= 1
        add(s X, Y) -> s add(X, Y)
        0 + 0X + 0Y >= 1 + 0X + 0Y
        add(0(), X) -> X
        0 + 0X >= 1X
        terms N -> cons recip sqr N
        0 + 0N >= 0 + 0N
        sqr s X -> s add(sqr X, dbl X)
        2 + 1X >= 1 + 0X
        sqr 0() -> 0()
        2 >= 1
      Qed
    
    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}
     POLY:
      Mode: weak, max_in=1, output_bits=-1, dnum=1, ur=true
      Interpretation:
       [add](x0, x1) = 0,
       
       [first](x0, x1) = x0 + 1,
       
       [cons](x0) = 0,
       
       [recip](x0) = 0,
       
       [sqr](x0) = x0 + 1,
       
       [terms](x0) = 0,
       
       [s](x0) = x0 + 1,
       
       [dbl](x0) = x0 + 1,
       
       [0] = 1,
       
       [nil] = 0,
       
       [dbl#](x0) = x0
      Strict:
       dbl# s X -> dbl# X
       1 + 1X >= 0 + 1X
      Weak:
       first(s X, cons Y) -> cons Y
       2 + 1X + 0Y >= 0 + 0Y
       first(0(), X) -> nil()
       2 + 0X >= 0
       dbl s X -> s s dbl X
       2 + 1X >= 3 + 1X
       dbl 0() -> 0()
       2 >= 1
       add(s X, Y) -> s add(X, Y)
       0 + 0X + 0Y >= 1 + 0X + 0Y
       add(0(), X) -> X
       0 + 0X >= 1X
       terms N -> cons recip sqr N
       0 + 0N >= 0 + 0N
       sqr s X -> s add(sqr X, dbl X)
       2 + 1X >= 1 + 0X
       sqr 0() -> 0()
       2 >= 1
     Qed
    
    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}
     POLY:
      Mode: weak, max_in=1, output_bits=-1, dnum=1, ur=true
      Interpretation:
       [add](x0, x1) = 0,
       
       [first](x0, x1) = x0 + 1,
       
       [cons](x0) = 0,
       
       [recip](x0) = 0,
       
       [sqr](x0) = x0 + 1,
       
       [terms](x0) = 0,
       
       [s](x0) = x0 + 1,
       
       [dbl](x0) = x0 + 1,
       
       [0] = 1,
       
       [nil] = 0,
       
       [add#](x0, x1) = x0
      Strict:
       add#(s X, Y) -> add#(X, Y)
       1 + 1X + 0Y >= 0 + 1X + 0Y
      Weak:
       first(s X, cons Y) -> cons Y
       2 + 1X + 0Y >= 0 + 0Y
       first(0(), X) -> nil()
       2 + 0X >= 0
       dbl s X -> s s dbl X
       2 + 1X >= 3 + 1X
       dbl 0() -> 0()
       2 >= 1
       add(s X, Y) -> s add(X, Y)
       0 + 0X + 0Y >= 1 + 0X + 0Y
       add(0(), X) -> X
       0 + 0X >= 1X
       terms N -> cons recip sqr N
       0 + 0N >= 0 + 0N
       sqr s X -> s add(sqr X, dbl X)
       2 + 1X >= 1 + 0X
       sqr 0() -> 0()
       2 >= 1
     Qed