MAYBE
MAYBE
TRS:
 {
   cond(true(), x, y) -> s(0()),
  cond(false(), x, y) -> double(log(x, square(s(s(y))))),
       le(s(u), s(v)) -> le(u, v),
        le(s(u), 0()) -> false(),
           le(0(), v) -> true(),
      log(x, s(s(y))) -> cond(le(x, s(s(y))), x, y),
         double(s(x)) -> s(s(double(x))),
          double(0()) -> 0(),
         square(s(x)) -> s(plus(square(x), double(x))),
          square(0()) -> 0(),
        plus(n, s(m)) -> s(plus(n, m)),
         plus(n, 0()) -> n
 }
 DUP: We consider a duplicating system.
  Trs:
   {
     cond(true(), x, y) -> s(0()),
    cond(false(), x, y) -> double(log(x, square(s(s(y))))),
         le(s(u), s(v)) -> le(u, v),
          le(s(u), 0()) -> false(),
             le(0(), v) -> true(),
        log(x, s(s(y))) -> cond(le(x, s(s(y))), x, y),
           double(s(x)) -> s(s(double(x))),
            double(0()) -> 0(),
           square(s(x)) -> s(plus(square(x), double(x))),
            square(0()) -> 0(),
          plus(n, s(m)) -> s(plus(n, m)),
           plus(n, 0()) -> n
   }
  Fail