TIMEOUT
MAYBE
Trs:
 {  -(s(x), s(y)) -> -(x, y),
        -(x, 0()) -> x,
    if(0(), y, z) -> y,
   if(s(x), y, z) -> z,
      double(0()) -> 0(),
     double(s(x)) -> s(s(double(x))),
        half(0()) -> 0(),
     half(s(0())) -> 0(),
    half(s(s(x))) -> s(half(x)),
  half(double(x)) -> x}
 Open