MAYBE
MAYBE
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
 }
 DUP: We consider a non-duplicating system.
  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
   }
  Fail