MAYBE
MAYBE
TRS:
 {
      minus(x, 0()) -> x,
  minus(s(x), s(y)) -> minus(x, y),
        double(0()) -> 0(),
       double(s(x)) -> s(s(double(x))),
      plus(s(x), x) -> plus(if(gt(x, x), id(x), id(x)), s(x)),
   plus(s(x), s(y)) ->
  s(s(plus(if(gt(x, y), x, y), if(not(gt(x, y)), id(x), id(y))))),
  plus(id(x), s(y)) -> s(plus(x, if(gt(s(y), y), y, s(y)))),
    plus(zero(), y) -> y,
   if(true(), x, y) -> x,
  if(false(), x, y) -> y,
     gt(s(x), s(y)) -> gt(x, y),
   gt(s(x), zero()) -> true(),
      gt(zero(), y) -> false(),
             not(x) -> if(x, false(), true()),
              id(x) -> x
 }
 DUP: We consider a duplicating system.
  Trs:
   {
        minus(x, 0()) -> x,
    minus(s(x), s(y)) -> minus(x, y),
          double(0()) -> 0(),
         double(s(x)) -> s(s(double(x))),
        plus(s(x), x) -> plus(if(gt(x, x), id(x), id(x)), s(x)),
     plus(s(x), s(y)) ->
    s(s(plus(if(gt(x, y), x, y), if(not(gt(x, y)), id(x), id(y))))),
    plus(id(x), s(y)) -> s(plus(x, if(gt(s(y), y), y, s(y)))),
      plus(zero(), y) -> y,
     if(true(), x, y) -> x,
    if(false(), x, y) -> y,
       gt(s(x), s(y)) -> gt(x, y),
     gt(s(x), zero()) -> true(),
        gt(zero(), y) -> false(),
               not(x) -> if(x, false(), true()),
                id(x) -> x
   }
  Fail