MAYBE
MAYBE
TRS:
 {
  f(a(), s(x), y) -> f(b(), y, s(x)),
   f(a(), 0(), y) -> y,
     f(b(), y, x) -> f(a(), half(x), exp(y)),
         tower(x) -> f(a(), x, s(0())),
    half(s(s(x))) -> s(half(x)),
     half(s(0())) -> half(0()),
        half(0()) -> double(0()),
        exp(s(x)) -> double(exp(x)),
         exp(0()) -> s(0()),
     double(s(x)) -> s(s(double(x))),
      double(0()) -> 0()
 }
 DUP: We consider a non-duplicating system.
  Trs:
   {
    f(a(), s(x), y) -> f(b(), y, s(x)),
     f(a(), 0(), y) -> y,
       f(b(), y, x) -> f(a(), half(x), exp(y)),
           tower(x) -> f(a(), x, s(0())),
      half(s(s(x))) -> s(half(x)),
       half(s(0())) -> half(0()),
          half(0()) -> double(0()),
          exp(s(x)) -> double(exp(x)),
           exp(0()) -> s(0()),
       double(s(x)) -> s(s(double(x))),
        double(0()) -> 0()
   }
  Fail