MAYBE
MAYBE
TRS:
 {
            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,
  times(x, plus(y, s(z))) ->
  plus(times(x, plus(y, times(s(z), 0()))), times(x, s(z))),
           times(x, s(y)) -> plus(times(x, y), x),
            times(x, 0()) -> 0(),
         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:
   {
              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,
    times(x, plus(y, s(z))) ->
    plus(times(x, plus(y, times(s(z), 0()))), times(x, s(z))),
             times(x, s(y)) -> plus(times(x, y), x),
              times(x, 0()) -> 0(),
           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