MAYBE
MAYBE
TRS:
 {
                activate(X) -> X,
           activate(n__0()) -> 0(),
      activate(n__isNat(X)) -> isNat(X),
  activate(n__plus(X1, X2)) -> plus(X1, X2),
          activate(n__s(X)) -> s(X),
               U11(tt(), N) -> activate(N),
                       s(X) -> n__s(X),
              plus(N, s(M)) -> U21(and(isNat(M), n__isNat(N)), M, N),
               plus(N, 0()) -> U11(isNat(N), N),
               plus(X1, X2) -> n__plus(X1, X2),
            U21(tt(), M, N) -> s(plus(activate(N), activate(M))),
               and(tt(), X) -> activate(X),
                   isNat(X) -> n__isNat(X),
              isNat(n__0()) -> tt(),
     isNat(n__plus(V1, V2)) ->
  and(isNat(activate(V1)), n__isNat(activate(V2))),
            isNat(n__s(V1)) -> isNat(activate(V1)),
                        0() -> n__0()
 }
 DUP: We consider a duplicating system.
  Trs:
   {
                  activate(X) -> X,
             activate(n__0()) -> 0(),
        activate(n__isNat(X)) -> isNat(X),
    activate(n__plus(X1, X2)) -> plus(X1, X2),
            activate(n__s(X)) -> s(X),
                 U11(tt(), N) -> activate(N),
                         s(X) -> n__s(X),
                plus(N, s(M)) -> U21(and(isNat(M), n__isNat(N)), M, N),
                 plus(N, 0()) -> U11(isNat(N), N),
                 plus(X1, X2) -> n__plus(X1, X2),
              U21(tt(), M, N) -> s(plus(activate(N), activate(M))),
                 and(tt(), X) -> activate(X),
                     isNat(X) -> n__isNat(X),
                isNat(n__0()) -> tt(),
       isNat(n__plus(V1, V2)) ->
    and(isNat(activate(V1)), n__isNat(activate(V2))),
              isNat(n__s(V1)) -> isNat(activate(V1)),
                          0() -> n__0()
   }
  Fail