MAYBE
MAYBE
TRS:
 {
                  U12(tt()) -> tt(),
              isNat(n__0()) -> tt(),
     isNat(n__plus(V1, V2)) -> U11(isNat(activate(V1)), activate(V2)),
            isNat(n__s(V1)) -> U21(isNat(activate(V1))),
        isNat(n__x(V1, V2)) -> U31(isNat(activate(V1)), activate(V2)),
                activate(X) -> X,
           activate(n__0()) -> 0(),
  activate(n__plus(X1, X2)) -> plus(activate(X1), activate(X2)),
          activate(n__s(X)) -> s(activate(X)),
     activate(n__x(X1, X2)) -> x(activate(X1), activate(X2)),
              U11(tt(), V2) -> U12(isNat(activate(V2))),
                  U21(tt()) -> tt(),
                  U32(tt()) -> tt(),
              U31(tt(), V2) -> U32(isNat(activate(V2))),
               U41(tt(), N) -> activate(N),
            U52(tt(), M, N) -> s(plus(activate(N), activate(M))),
            U51(tt(), M, N) ->
  U52(isNat(activate(N)), activate(M), activate(N)),
                       s(X) -> n__s(X),
              plus(N, s(M)) -> U51(isNat(M), M, N),
               plus(N, 0()) -> U41(isNat(N), N),
               plus(X1, X2) -> n__plus(X1, X2),
                        0() -> n__0(),
                  U61(tt()) -> 0(),
            U72(tt(), M, N) -> plus(x(activate(N), activate(M)), activate(N)),
            U71(tt(), M, N) ->
  U72(isNat(activate(N)), activate(M), activate(N)),
                 x(N, s(M)) -> U71(isNat(M), M, N),
                  x(N, 0()) -> U61(isNat(N)),
                  x(X1, X2) -> n__x(X1, X2)
 }
 DUP: We consider a duplicating system.
  Trs:
   {
                    U12(tt()) -> tt(),
                isNat(n__0()) -> tt(),
       isNat(n__plus(V1, V2)) -> U11(isNat(activate(V1)), activate(V2)),
              isNat(n__s(V1)) -> U21(isNat(activate(V1))),
          isNat(n__x(V1, V2)) -> U31(isNat(activate(V1)), activate(V2)),
                  activate(X) -> X,
             activate(n__0()) -> 0(),
    activate(n__plus(X1, X2)) -> plus(activate(X1), activate(X2)),
            activate(n__s(X)) -> s(activate(X)),
       activate(n__x(X1, X2)) -> x(activate(X1), activate(X2)),
                U11(tt(), V2) -> U12(isNat(activate(V2))),
                    U21(tt()) -> tt(),
                    U32(tt()) -> tt(),
                U31(tt(), V2) -> U32(isNat(activate(V2))),
                 U41(tt(), N) -> activate(N),
              U52(tt(), M, N) -> s(plus(activate(N), activate(M))),
              U51(tt(), M, N) ->
    U52(isNat(activate(N)), activate(M), activate(N)),
                         s(X) -> n__s(X),
                plus(N, s(M)) -> U51(isNat(M), M, N),
                 plus(N, 0()) -> U41(isNat(N), N),
                 plus(X1, X2) -> n__plus(X1, X2),
                          0() -> n__0(),
                    U61(tt()) -> 0(),
              U72(tt(), M, N) ->
    plus(x(activate(N), activate(M)), activate(N)),
              U71(tt(), M, N) ->
    U72(isNat(activate(N)), activate(M), activate(N)),
                   x(N, s(M)) -> U71(isNat(M), M, N),
                    x(N, 0()) -> U61(isNat(N)),
                    x(X1, X2) -> n__x(X1, X2)
   }
  Fail