MAYBE
MAYBE
TRS:
 {
                      0() -> n__0(),
         minus(n__0(), Y) -> 0(),
  minus(n__s(X), n__s(Y)) -> minus(activate(X), activate(Y)),
              activate(X) -> X,
         activate(n__0()) -> 0(),
        activate(n__s(X)) -> s(X),
           geq(X, n__0()) -> true(),
     geq(n__0(), n__s(Y)) -> false(),
    geq(n__s(X), n__s(Y)) -> geq(activate(X), activate(Y)),
        div(0(), n__s(Y)) -> 0(),
       div(s(X), n__s(Y)) ->
  if(
    geq(X, activate(Y)), n__s(div(minus(X, activate(Y)), n__s(activate(Y)))),
    n__0()
  ),
         if(true(), X, Y) -> activate(X),
        if(false(), X, Y) -> activate(Y),
                     s(X) -> n__s(X)
 }
 DUP: We consider a duplicating system.
  Trs:
   {
                        0() -> n__0(),
           minus(n__0(), Y) -> 0(),
    minus(n__s(X), n__s(Y)) -> minus(activate(X), activate(Y)),
                activate(X) -> X,
           activate(n__0()) -> 0(),
          activate(n__s(X)) -> s(X),
             geq(X, n__0()) -> true(),
       geq(n__0(), n__s(Y)) -> false(),
      geq(n__s(X), n__s(Y)) -> geq(activate(X), activate(Y)),
          div(0(), n__s(Y)) -> 0(),
         div(s(X), n__s(Y)) ->
    if(
      geq(X, activate(Y)),
      n__s(div(minus(X, activate(Y)), n__s(activate(Y)))), n__0()
    ),
           if(true(), X, Y) -> activate(X),
          if(false(), X, Y) -> activate(Y),
                       s(X) -> n__s(X)
   }
  Fail