YES
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:
   Strict:
    { double#(s(x)) -> double#(x),
     half#(s(s(x))) -> half#(x),
     -#(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)}
   EDG:
    {(double#(s(x)) -> double#(x), double#(s(x)) -> double#(x))
     (half#(s(s(x))) -> half#(x), half#(s(s(x))) -> half#(x))
     (-#(s(x), s(y)) -> -#(x, y), -#(s(x), s(y)) -> -#(x, y))}
    SCCS:
     Scc:
      {-#(s(x), s(y)) -> -#(x, y)}
     Scc:
      {half#(s(s(x))) -> half#(x)}
     Scc:
      {double#(s(x)) -> double#(x)}
     SCC:
      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(-#) = 0
       Strict:
        {}
       Qed
     SCC:
      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:
      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