YES
Time: 0.001362
TRS:
 {   sqr 0() -> 0(),
     sqr s x -> +(sqr x, s double x),
     sqr s x -> s +(sqr x, double x),
   +(x, 0()) -> x,
   +(x, s y) -> s +(x, y),
  double 0() -> 0(),
  double s x -> s s double x}
 DP:
  DP:
   {   sqr# s x -> sqr# x,
       sqr# s x -> +#(sqr x, s double x),
       sqr# s x -> +#(sqr x, double x),
       sqr# s x -> double# x,
     +#(x, s y) -> +#(x, y),
    double# s x -> double# x}
  TRS:
  {   sqr 0() -> 0(),
      sqr s x -> +(sqr x, s double x),
      sqr s x -> s +(sqr x, double x),
    +(x, 0()) -> x,
    +(x, s y) -> s +(x, y),
   double 0() -> 0(),
   double s x -> s s double x}
  EDG:
   {(sqr# s x -> +#(sqr x, s double x), +#(x, s y) -> +#(x, y))
    (sqr# s x -> sqr# x, sqr# s x -> double# x)
    (sqr# s x -> sqr# x, sqr# s x -> +#(sqr x, double x))
    (sqr# s x -> sqr# x, sqr# s x -> +#(sqr x, s double x))
    (sqr# s x -> sqr# x, sqr# s x -> sqr# x)
    (double# s x -> double# x, double# s x -> double# x)
    (sqr# s x -> double# x, double# s x -> double# x)
    (sqr# s x -> +#(sqr x, double x), +#(x, s y) -> +#(x, y))
    (+#(x, s y) -> +#(x, y), +#(x, s y) -> +#(x, y))}
   SCCS (3):
    Scc:
     {double# s x -> double# x}
    Scc:
     {+#(x, s y) -> +#(x, y)}
    Scc:
     {sqr# s x -> sqr# x}
    SCC (1):
     Strict:
      {double# s x -> double# x}
     Weak:
     {   sqr 0() -> 0(),
         sqr s x -> +(sqr x, s double x),
         sqr s x -> s +(sqr x, double x),
       +(x, 0()) -> x,
       +(x, s y) -> s +(x, y),
      double 0() -> 0(),
      double s x -> s s double x}
     SPSC:
      Simple Projection:
       pi(double#) = 0
      Strict:
       {}
      Qed
    SCC (1):
     Strict:
      {+#(x, s y) -> +#(x, y)}
     Weak:
     {   sqr 0() -> 0(),
         sqr s x -> +(sqr x, s double x),
         sqr s x -> s +(sqr x, double x),
       +(x, 0()) -> x,
       +(x, s y) -> s +(x, y),
      double 0() -> 0(),
      double s x -> s s double x}
     SPSC:
      Simple Projection:
       pi(+#) = 1
      Strict:
       {}
      Qed
    SCC (1):
     Strict:
      {sqr# s x -> sqr# x}
     Weak:
     {   sqr 0() -> 0(),
         sqr s x -> +(sqr x, s double x),
         sqr s x -> s +(sqr x, double x),
       +(x, 0()) -> x,
       +(x, s y) -> s +(x, y),
      double 0() -> 0(),
      double s x -> s s double x}
     SPSC:
      Simple Projection:
       pi(sqr#) = 0
      Strict:
       {}
      Qed