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