YES
TRS:
 {              activate(X) -> X,
           activate(n__0()) -> 0(),
      activate(n__isNat(X)) -> isNat(X),
  activate(n__plus(X1, X2)) -> plus(activate(X1), activate(X2)),
          activate(n__s(X)) -> s(activate(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()}
 DP:
  Strict:
   {         activate#(n__0()) -> 0#(),
        activate#(n__isNat(X)) -> isNat#(X),
    activate#(n__plus(X1, X2)) -> activate#(X1),
    activate#(n__plus(X1, X2)) -> activate#(X2),
    activate#(n__plus(X1, X2)) -> plus#(activate(X1), activate(X2)),
            activate#(n__s(X)) -> activate#(X),
            activate#(n__s(X)) -> s#(activate(X)),
                 U11#(tt(), N) -> activate#(N),
                plus#(N, s(M)) -> U21#(and(isNat(M), n__isNat(N)), M, N),
                plus#(N, s(M)) -> and#(isNat(M), n__isNat(N)),
                plus#(N, s(M)) -> isNat#(M),
                 plus#(N, 0()) -> U11#(isNat(N), N),
                 plus#(N, 0()) -> isNat#(N),
              U21#(tt(), M, N) -> activate#(N),
              U21#(tt(), M, N) -> activate#(M),
              U21#(tt(), M, N) -> s#(plus(activate(N), activate(M))),
              U21#(tt(), M, N) -> plus#(activate(N), activate(M)),
                 and#(tt(), X) -> activate#(X),
       isNat#(n__plus(V1, V2)) -> activate#(V1),
       isNat#(n__plus(V1, V2)) -> activate#(V2),
       isNat#(n__plus(V1, V2)) -> and#(isNat(activate(V1)), n__isNat(activate(V2))),
       isNat#(n__plus(V1, V2)) -> isNat#(activate(V1)),
              isNat#(n__s(V1)) -> activate#(V1),
              isNat#(n__s(V1)) -> isNat#(activate(V1))}
  Weak:
  {              activate(X) -> X,
            activate(n__0()) -> 0(),
       activate(n__isNat(X)) -> isNat(X),
   activate(n__plus(X1, X2)) -> plus(activate(X1), activate(X2)),
           activate(n__s(X)) -> s(activate(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()}
  EDG:
   {(isNat#(n__plus(V1, V2)) -> activate#(V1), activate#(n__s(X)) -> s#(activate(X)))
    (isNat#(n__plus(V1, V2)) -> activate#(V1), activate#(n__s(X)) -> activate#(X))
    (isNat#(n__plus(V1, V2)) -> activate#(V1), activate#(n__plus(X1, X2)) -> plus#(activate(X1), activate(X2)))
    (isNat#(n__plus(V1, V2)) -> activate#(V1), activate#(n__plus(X1, X2)) -> activate#(X2))
    (isNat#(n__plus(V1, V2)) -> activate#(V1), activate#(n__plus(X1, X2)) -> activate#(X1))
    (isNat#(n__plus(V1, V2)) -> activate#(V1), activate#(n__isNat(X)) -> isNat#(X))
    (isNat#(n__plus(V1, V2)) -> activate#(V1), activate#(n__0()) -> 0#())
    (activate#(n__isNat(X)) -> isNat#(X), isNat#(n__s(V1)) -> isNat#(activate(V1)))
    (activate#(n__isNat(X)) -> isNat#(X), isNat#(n__s(V1)) -> activate#(V1))
    (activate#(n__isNat(X)) -> isNat#(X), isNat#(n__plus(V1, V2)) -> isNat#(activate(V1)))
    (activate#(n__isNat(X)) -> isNat#(X), isNat#(n__plus(V1, V2)) -> and#(isNat(activate(V1)), n__isNat(activate(V2))))
    (activate#(n__isNat(X)) -> isNat#(X), isNat#(n__plus(V1, V2)) -> activate#(V2))
    (activate#(n__isNat(X)) -> isNat#(X), isNat#(n__plus(V1, V2)) -> activate#(V1))
    (and#(tt(), X) -> activate#(X), activate#(n__s(X)) -> s#(activate(X)))
    (and#(tt(), X) -> activate#(X), activate#(n__s(X)) -> activate#(X))
    (and#(tt(), X) -> activate#(X), activate#(n__plus(X1, X2)) -> plus#(activate(X1), activate(X2)))
    (and#(tt(), X) -> activate#(X), activate#(n__plus(X1, X2)) -> activate#(X2))
    (and#(tt(), X) -> activate#(X), activate#(n__plus(X1, X2)) -> activate#(X1))
    (and#(tt(), X) -> activate#(X), activate#(n__isNat(X)) -> isNat#(X))
    (and#(tt(), X) -> activate#(X), activate#(n__0()) -> 0#())
    (isNat#(n__plus(V1, V2)) -> isNat#(activate(V1)), isNat#(n__s(V1)) -> isNat#(activate(V1)))
    (isNat#(n__plus(V1, V2)) -> isNat#(activate(V1)), isNat#(n__s(V1)) -> activate#(V1))
    (isNat#(n__plus(V1, V2)) -> isNat#(activate(V1)), isNat#(n__plus(V1, V2)) -> isNat#(activate(V1)))
    (isNat#(n__plus(V1, V2)) -> isNat#(activate(V1)), isNat#(n__plus(V1, V2)) -> and#(isNat(activate(V1)), n__isNat(activate(V2))))
    (isNat#(n__plus(V1, V2)) -> isNat#(activate(V1)), isNat#(n__plus(V1, V2)) -> activate#(V2))
    (isNat#(n__plus(V1, V2)) -> isNat#(activate(V1)), isNat#(n__plus(V1, V2)) -> activate#(V1))
    (plus#(N, 0()) -> U11#(isNat(N), N), U11#(tt(), N) -> activate#(N))
    (U11#(tt(), N) -> activate#(N), activate#(n__s(X)) -> s#(activate(X)))
    (U11#(tt(), N) -> activate#(N), activate#(n__s(X)) -> activate#(X))
    (U11#(tt(), N) -> activate#(N), activate#(n__plus(X1, X2)) -> plus#(activate(X1), activate(X2)))
    (U11#(tt(), N) -> activate#(N), activate#(n__plus(X1, X2)) -> activate#(X2))
    (U11#(tt(), N) -> activate#(N), activate#(n__plus(X1, X2)) -> activate#(X1))
    (U11#(tt(), N) -> activate#(N), activate#(n__isNat(X)) -> isNat#(X))
    (U11#(tt(), N) -> activate#(N), activate#(n__0()) -> 0#())
    (U21#(tt(), M, N) -> activate#(N), activate#(n__s(X)) -> s#(activate(X)))
    (U21#(tt(), M, N) -> activate#(N), activate#(n__s(X)) -> activate#(X))
    (U21#(tt(), M, N) -> activate#(N), activate#(n__plus(X1, X2)) -> plus#(activate(X1), activate(X2)))
    (U21#(tt(), M, N) -> activate#(N), activate#(n__plus(X1, X2)) -> activate#(X2))
    (U21#(tt(), M, N) -> activate#(N), activate#(n__plus(X1, X2)) -> activate#(X1))
    (U21#(tt(), M, N) -> activate#(N), activate#(n__isNat(X)) -> isNat#(X))
    (U21#(tt(), M, N) -> activate#(N), activate#(n__0()) -> 0#())
    (plus#(N, s(M)) -> and#(isNat(M), n__isNat(N)), and#(tt(), X) -> activate#(X))
    (activate#(n__plus(X1, X2)) -> activate#(X2), activate#(n__s(X)) -> s#(activate(X)))
    (activate#(n__plus(X1, X2)) -> activate#(X2), activate#(n__s(X)) -> activate#(X))
    (activate#(n__plus(X1, X2)) -> activate#(X2), activate#(n__plus(X1, X2)) -> plus#(activate(X1), activate(X2)))
    (activate#(n__plus(X1, X2)) -> activate#(X2), activate#(n__plus(X1, X2)) -> activate#(X2))
    (activate#(n__plus(X1, X2)) -> activate#(X2), activate#(n__plus(X1, X2)) -> activate#(X1))
    (activate#(n__plus(X1, X2)) -> activate#(X2), activate#(n__isNat(X)) -> isNat#(X))
    (activate#(n__plus(X1, X2)) -> activate#(X2), activate#(n__0()) -> 0#())
    (plus#(N, s(M)) -> U21#(and(isNat(M), n__isNat(N)), M, N), U21#(tt(), M, N) -> plus#(activate(N), activate(M)))
    (plus#(N, s(M)) -> U21#(and(isNat(M), n__isNat(N)), M, N), U21#(tt(), M, N) -> s#(plus(activate(N), activate(M))))
    (plus#(N, s(M)) -> U21#(and(isNat(M), n__isNat(N)), M, N), U21#(tt(), M, N) -> activate#(M))
    (plus#(N, s(M)) -> U21#(and(isNat(M), n__isNat(N)), M, N), U21#(tt(), M, N) -> activate#(N))
    (activate#(n__plus(X1, X2)) -> activate#(X1), activate#(n__0()) -> 0#())
    (activate#(n__plus(X1, X2)) -> activate#(X1), activate#(n__isNat(X)) -> isNat#(X))
    (activate#(n__plus(X1, X2)) -> activate#(X1), activate#(n__plus(X1, X2)) -> activate#(X1))
    (activate#(n__plus(X1, X2)) -> activate#(X1), activate#(n__plus(X1, X2)) -> activate#(X2))
    (activate#(n__plus(X1, X2)) -> activate#(X1), activate#(n__plus(X1, X2)) -> plus#(activate(X1), activate(X2)))
    (activate#(n__plus(X1, X2)) -> activate#(X1), activate#(n__s(X)) -> activate#(X))
    (activate#(n__plus(X1, X2)) -> activate#(X1), activate#(n__s(X)) -> s#(activate(X)))
    (U21#(tt(), M, N) -> plus#(activate(N), activate(M)), plus#(N, s(M)) -> U21#(and(isNat(M), n__isNat(N)), M, N))
    (U21#(tt(), M, N) -> plus#(activate(N), activate(M)), plus#(N, s(M)) -> and#(isNat(M), n__isNat(N)))
    (U21#(tt(), M, N) -> plus#(activate(N), activate(M)), plus#(N, s(M)) -> isNat#(M))
    (U21#(tt(), M, N) -> plus#(activate(N), activate(M)), plus#(N, 0()) -> U11#(isNat(N), N))
    (U21#(tt(), M, N) -> plus#(activate(N), activate(M)), plus#(N, 0()) -> isNat#(N))
    (activate#(n__plus(X1, X2)) -> plus#(activate(X1), activate(X2)), plus#(N, s(M)) -> U21#(and(isNat(M), n__isNat(N)), M, N))
    (activate#(n__plus(X1, X2)) -> plus#(activate(X1), activate(X2)), plus#(N, s(M)) -> and#(isNat(M), n__isNat(N)))
    (activate#(n__plus(X1, X2)) -> plus#(activate(X1), activate(X2)), plus#(N, s(M)) -> isNat#(M))
    (activate#(n__plus(X1, X2)) -> plus#(activate(X1), activate(X2)), plus#(N, 0()) -> U11#(isNat(N), N))
    (activate#(n__plus(X1, X2)) -> plus#(activate(X1), activate(X2)), plus#(N, 0()) -> isNat#(N))
    (plus#(N, 0()) -> isNat#(N), isNat#(n__plus(V1, V2)) -> activate#(V1))
    (plus#(N, 0()) -> isNat#(N), isNat#(n__plus(V1, V2)) -> activate#(V2))
    (plus#(N, 0()) -> isNat#(N), isNat#(n__plus(V1, V2)) -> and#(isNat(activate(V1)), n__isNat(activate(V2))))
    (plus#(N, 0()) -> isNat#(N), isNat#(n__plus(V1, V2)) -> isNat#(activate(V1)))
    (plus#(N, 0()) -> isNat#(N), isNat#(n__s(V1)) -> activate#(V1))
    (plus#(N, 0()) -> isNat#(N), isNat#(n__s(V1)) -> isNat#(activate(V1)))
    (U21#(tt(), M, N) -> activate#(M), activate#(n__0()) -> 0#())
    (U21#(tt(), M, N) -> activate#(M), activate#(n__isNat(X)) -> isNat#(X))
    (U21#(tt(), M, N) -> activate#(M), activate#(n__plus(X1, X2)) -> activate#(X1))
    (U21#(tt(), M, N) -> activate#(M), activate#(n__plus(X1, X2)) -> activate#(X2))
    (U21#(tt(), M, N) -> activate#(M), activate#(n__plus(X1, X2)) -> plus#(activate(X1), activate(X2)))
    (U21#(tt(), M, N) -> activate#(M), activate#(n__s(X)) -> activate#(X))
    (U21#(tt(), M, N) -> activate#(M), activate#(n__s(X)) -> s#(activate(X)))
    (plus#(N, s(M)) -> isNat#(M), isNat#(n__plus(V1, V2)) -> activate#(V1))
    (plus#(N, s(M)) -> isNat#(M), isNat#(n__plus(V1, V2)) -> activate#(V2))
    (plus#(N, s(M)) -> isNat#(M), isNat#(n__plus(V1, V2)) -> and#(isNat(activate(V1)), n__isNat(activate(V2))))
    (plus#(N, s(M)) -> isNat#(M), isNat#(n__plus(V1, V2)) -> isNat#(activate(V1)))
    (plus#(N, s(M)) -> isNat#(M), isNat#(n__s(V1)) -> activate#(V1))
    (plus#(N, s(M)) -> isNat#(M), isNat#(n__s(V1)) -> isNat#(activate(V1)))
    (isNat#(n__s(V1)) -> isNat#(activate(V1)), isNat#(n__plus(V1, V2)) -> activate#(V1))
    (isNat#(n__s(V1)) -> isNat#(activate(V1)), isNat#(n__plus(V1, V2)) -> activate#(V2))
    (isNat#(n__s(V1)) -> isNat#(activate(V1)), isNat#(n__plus(V1, V2)) -> and#(isNat(activate(V1)), n__isNat(activate(V2))))
    (isNat#(n__s(V1)) -> isNat#(activate(V1)), isNat#(n__plus(V1, V2)) -> isNat#(activate(V1)))
    (isNat#(n__s(V1)) -> isNat#(activate(V1)), isNat#(n__s(V1)) -> activate#(V1))
    (isNat#(n__s(V1)) -> isNat#(activate(V1)), isNat#(n__s(V1)) -> isNat#(activate(V1)))
    (isNat#(n__plus(V1, V2)) -> and#(isNat(activate(V1)), n__isNat(activate(V2))), and#(tt(), X) -> activate#(X))
    (activate#(n__s(X)) -> activate#(X), activate#(n__0()) -> 0#())
    (activate#(n__s(X)) -> activate#(X), activate#(n__isNat(X)) -> isNat#(X))
    (activate#(n__s(X)) -> activate#(X), activate#(n__plus(X1, X2)) -> activate#(X1))
    (activate#(n__s(X)) -> activate#(X), activate#(n__plus(X1, X2)) -> activate#(X2))
    (activate#(n__s(X)) -> activate#(X), activate#(n__plus(X1, X2)) -> plus#(activate(X1), activate(X2)))
    (activate#(n__s(X)) -> activate#(X), activate#(n__s(X)) -> activate#(X))
    (activate#(n__s(X)) -> activate#(X), activate#(n__s(X)) -> s#(activate(X)))
    (isNat#(n__s(V1)) -> activate#(V1), activate#(n__0()) -> 0#())
    (isNat#(n__s(V1)) -> activate#(V1), activate#(n__isNat(X)) -> isNat#(X))
    (isNat#(n__s(V1)) -> activate#(V1), activate#(n__plus(X1, X2)) -> activate#(X1))
    (isNat#(n__s(V1)) -> activate#(V1), activate#(n__plus(X1, X2)) -> activate#(X2))
    (isNat#(n__s(V1)) -> activate#(V1), activate#(n__plus(X1, X2)) -> plus#(activate(X1), activate(X2)))
    (isNat#(n__s(V1)) -> activate#(V1), activate#(n__s(X)) -> activate#(X))
    (isNat#(n__s(V1)) -> activate#(V1), activate#(n__s(X)) -> s#(activate(X)))
    (isNat#(n__plus(V1, V2)) -> activate#(V2), activate#(n__0()) -> 0#())
    (isNat#(n__plus(V1, V2)) -> activate#(V2), activate#(n__isNat(X)) -> isNat#(X))
    (isNat#(n__plus(V1, V2)) -> activate#(V2), activate#(n__plus(X1, X2)) -> activate#(X1))
    (isNat#(n__plus(V1, V2)) -> activate#(V2), activate#(n__plus(X1, X2)) -> activate#(X2))
    (isNat#(n__plus(V1, V2)) -> activate#(V2), activate#(n__plus(X1, X2)) -> plus#(activate(X1), activate(X2)))
    (isNat#(n__plus(V1, V2)) -> activate#(V2), activate#(n__s(X)) -> activate#(X))
    (isNat#(n__plus(V1, V2)) -> activate#(V2), activate#(n__s(X)) -> s#(activate(X)))}
   SCCS:
    Scc:
     {    activate#(n__isNat(X)) -> isNat#(X),
      activate#(n__plus(X1, X2)) -> activate#(X1),
      activate#(n__plus(X1, X2)) -> activate#(X2),
      activate#(n__plus(X1, X2)) -> plus#(activate(X1), activate(X2)),
              activate#(n__s(X)) -> activate#(X),
                   U11#(tt(), N) -> activate#(N),
                  plus#(N, s(M)) -> U21#(and(isNat(M), n__isNat(N)), M, N),
                  plus#(N, s(M)) -> and#(isNat(M), n__isNat(N)),
                  plus#(N, s(M)) -> isNat#(M),
                   plus#(N, 0()) -> U11#(isNat(N), N),
                   plus#(N, 0()) -> isNat#(N),
                U21#(tt(), M, N) -> activate#(N),
                U21#(tt(), M, N) -> activate#(M),
                U21#(tt(), M, N) -> plus#(activate(N), activate(M)),
                   and#(tt(), X) -> activate#(X),
         isNat#(n__plus(V1, V2)) -> activate#(V1),
         isNat#(n__plus(V1, V2)) -> activate#(V2),
         isNat#(n__plus(V1, V2)) -> and#(isNat(activate(V1)), n__isNat(activate(V2))),
         isNat#(n__plus(V1, V2)) -> isNat#(activate(V1)),
                isNat#(n__s(V1)) -> activate#(V1),
                isNat#(n__s(V1)) -> isNat#(activate(V1))}
    SCC:
     Strict:
      {    activate#(n__isNat(X)) -> isNat#(X),
       activate#(n__plus(X1, X2)) -> activate#(X1),
       activate#(n__plus(X1, X2)) -> activate#(X2),
       activate#(n__plus(X1, X2)) -> plus#(activate(X1), activate(X2)),
               activate#(n__s(X)) -> activate#(X),
                    U11#(tt(), N) -> activate#(N),
                   plus#(N, s(M)) -> U21#(and(isNat(M), n__isNat(N)), M, N),
                   plus#(N, s(M)) -> and#(isNat(M), n__isNat(N)),
                   plus#(N, s(M)) -> isNat#(M),
                    plus#(N, 0()) -> U11#(isNat(N), N),
                    plus#(N, 0()) -> isNat#(N),
                 U21#(tt(), M, N) -> activate#(N),
                 U21#(tt(), M, N) -> activate#(M),
                 U21#(tt(), M, N) -> plus#(activate(N), activate(M)),
                    and#(tt(), X) -> activate#(X),
          isNat#(n__plus(V1, V2)) -> activate#(V1),
          isNat#(n__plus(V1, V2)) -> activate#(V2),
          isNat#(n__plus(V1, V2)) -> and#(isNat(activate(V1)), n__isNat(activate(V2))),
          isNat#(n__plus(V1, V2)) -> isNat#(activate(V1)),
                 isNat#(n__s(V1)) -> activate#(V1),
                 isNat#(n__s(V1)) -> isNat#(activate(V1))}
     Weak:
     {              activate(X) -> X,
               activate(n__0()) -> 0(),
          activate(n__isNat(X)) -> isNat(X),
      activate(n__plus(X1, X2)) -> plus(activate(X1), activate(X2)),
              activate(n__s(X)) -> s(activate(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()}
     POLY:
      Argument Filtering:
       pi(0) = [], pi(n__s) = [0], pi(n__plus) = [0,1], pi(n__isNat) = 0, pi(n__0) = [], pi(isNat#) = 0, pi(isNat) = 0, pi(and#) = 1, pi(and) = 1, pi(U21#) = [1,2], pi(U21) = [1,2], pi(plus#) = [0,1], pi(plus) = [0,1], pi(s) = [0], pi(tt) = [], pi(U11#) = 1, pi(U11) = 1, pi(activate#) = 0, pi(activate) = 0
      Usable Rules:
       {}
      Interpretation:
       [U21#](x0, x1) = x0 + x1,
       [plus#](x0, x1) = x0 + x1,
       [n__plus](x0, x1) = x0 + x1,
       [n__s](x0) = x0 + 1,
       [s](x0) = x0 + 1,
       [0] = 0
      Strict:
       {    activate#(n__isNat(X)) -> isNat#(X),
        activate#(n__plus(X1, X2)) -> activate#(X1),
        activate#(n__plus(X1, X2)) -> activate#(X2),
        activate#(n__plus(X1, X2)) -> plus#(activate(X1), activate(X2)),
                     U11#(tt(), N) -> activate#(N),
                     plus#(N, 0()) -> U11#(isNat(N), N),
                     plus#(N, 0()) -> isNat#(N),
                  U21#(tt(), M, N) -> activate#(N),
                  U21#(tt(), M, N) -> activate#(M),
                  U21#(tt(), M, N) -> plus#(activate(N), activate(M)),
                     and#(tt(), X) -> activate#(X),
           isNat#(n__plus(V1, V2)) -> activate#(V1),
           isNat#(n__plus(V1, V2)) -> activate#(V2),
           isNat#(n__plus(V1, V2)) -> and#(isNat(activate(V1)), n__isNat(activate(V2))),
           isNat#(n__plus(V1, V2)) -> isNat#(activate(V1))}
      Weak:
       {              activate(X) -> X,
                 activate(n__0()) -> 0(),
            activate(n__isNat(X)) -> isNat(X),
        activate(n__plus(X1, X2)) -> plus(activate(X1), activate(X2)),
                activate(n__s(X)) -> s(activate(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()}
      EDG:
       {(and#(tt(), X) -> activate#(X), activate#(n__plus(X1, X2)) -> plus#(activate(X1), activate(X2)))
        (and#(tt(), X) -> activate#(X), activate#(n__plus(X1, X2)) -> activate#(X2))
        (and#(tt(), X) -> activate#(X), activate#(n__plus(X1, X2)) -> activate#(X1))
        (and#(tt(), X) -> activate#(X), activate#(n__isNat(X)) -> isNat#(X))
        (isNat#(n__plus(V1, V2)) -> and#(isNat(activate(V1)), n__isNat(activate(V2))), and#(tt(), X) -> activate#(X))
        (activate#(n__plus(X1, X2)) -> plus#(activate(X1), activate(X2)), plus#(N, 0()) -> isNat#(N))
        (activate#(n__plus(X1, X2)) -> plus#(activate(X1), activate(X2)), plus#(N, 0()) -> U11#(isNat(N), N))
        (U11#(tt(), N) -> activate#(N), activate#(n__plus(X1, X2)) -> plus#(activate(X1), activate(X2)))
        (U11#(tt(), N) -> activate#(N), activate#(n__plus(X1, X2)) -> activate#(X2))
        (U11#(tt(), N) -> activate#(N), activate#(n__plus(X1, X2)) -> activate#(X1))
        (U11#(tt(), N) -> activate#(N), activate#(n__isNat(X)) -> isNat#(X))
        (U21#(tt(), M, N) -> activate#(N), activate#(n__plus(X1, X2)) -> plus#(activate(X1), activate(X2)))
        (U21#(tt(), M, N) -> activate#(N), activate#(n__plus(X1, X2)) -> activate#(X2))
        (U21#(tt(), M, N) -> activate#(N), activate#(n__plus(X1, X2)) -> activate#(X1))
        (U21#(tt(), M, N) -> activate#(N), activate#(n__isNat(X)) -> isNat#(X))
        (isNat#(n__plus(V1, V2)) -> isNat#(activate(V1)), isNat#(n__plus(V1, V2)) -> isNat#(activate(V1)))
        (isNat#(n__plus(V1, V2)) -> isNat#(activate(V1)), isNat#(n__plus(V1, V2)) -> and#(isNat(activate(V1)), n__isNat(activate(V2))))
        (isNat#(n__plus(V1, V2)) -> isNat#(activate(V1)), isNat#(n__plus(V1, V2)) -> activate#(V2))
        (isNat#(n__plus(V1, V2)) -> isNat#(activate(V1)), isNat#(n__plus(V1, V2)) -> activate#(V1))
        (U21#(tt(), M, N) -> activate#(M), activate#(n__plus(X1, X2)) -> plus#(activate(X1), activate(X2)))
        (U21#(tt(), M, N) -> activate#(M), activate#(n__plus(X1, X2)) -> activate#(X2))
        (U21#(tt(), M, N) -> activate#(M), activate#(n__plus(X1, X2)) -> activate#(X1))
        (U21#(tt(), M, N) -> activate#(M), activate#(n__isNat(X)) -> isNat#(X))
        (isNat#(n__plus(V1, V2)) -> activate#(V2), activate#(n__isNat(X)) -> isNat#(X))
        (isNat#(n__plus(V1, V2)) -> activate#(V2), activate#(n__plus(X1, X2)) -> activate#(X1))
        (isNat#(n__plus(V1, V2)) -> activate#(V2), activate#(n__plus(X1, X2)) -> activate#(X2))
        (isNat#(n__plus(V1, V2)) -> activate#(V2), activate#(n__plus(X1, X2)) -> plus#(activate(X1), activate(X2)))
        (activate#(n__plus(X1, X2)) -> activate#(X2), activate#(n__isNat(X)) -> isNat#(X))
        (activate#(n__plus(X1, X2)) -> activate#(X2), activate#(n__plus(X1, X2)) -> activate#(X1))
        (activate#(n__plus(X1, X2)) -> activate#(X2), activate#(n__plus(X1, X2)) -> activate#(X2))
        (activate#(n__plus(X1, X2)) -> activate#(X2), activate#(n__plus(X1, X2)) -> plus#(activate(X1), activate(X2)))
        (isNat#(n__plus(V1, V2)) -> activate#(V1), activate#(n__isNat(X)) -> isNat#(X))
        (isNat#(n__plus(V1, V2)) -> activate#(V1), activate#(n__plus(X1, X2)) -> activate#(X1))
        (isNat#(n__plus(V1, V2)) -> activate#(V1), activate#(n__plus(X1, X2)) -> activate#(X2))
        (isNat#(n__plus(V1, V2)) -> activate#(V1), activate#(n__plus(X1, X2)) -> plus#(activate(X1), activate(X2)))
        (plus#(N, 0()) -> isNat#(N), isNat#(n__plus(V1, V2)) -> activate#(V1))
        (plus#(N, 0()) -> isNat#(N), isNat#(n__plus(V1, V2)) -> activate#(V2))
        (plus#(N, 0()) -> isNat#(N), isNat#(n__plus(V1, V2)) -> and#(isNat(activate(V1)), n__isNat(activate(V2))))
        (plus#(N, 0()) -> isNat#(N), isNat#(n__plus(V1, V2)) -> isNat#(activate(V1)))
        (U21#(tt(), M, N) -> plus#(activate(N), activate(M)), plus#(N, 0()) -> U11#(isNat(N), N))
        (U21#(tt(), M, N) -> plus#(activate(N), activate(M)), plus#(N, 0()) -> isNat#(N))
        (activate#(n__plus(X1, X2)) -> activate#(X1), activate#(n__isNat(X)) -> isNat#(X))
        (activate#(n__plus(X1, X2)) -> activate#(X1), activate#(n__plus(X1, X2)) -> activate#(X1))
        (activate#(n__plus(X1, X2)) -> activate#(X1), activate#(n__plus(X1, X2)) -> activate#(X2))
        (activate#(n__plus(X1, X2)) -> activate#(X1), activate#(n__plus(X1, X2)) -> plus#(activate(X1), activate(X2)))
        (plus#(N, 0()) -> U11#(isNat(N), N), U11#(tt(), N) -> activate#(N))
        (activate#(n__isNat(X)) -> isNat#(X), isNat#(n__plus(V1, V2)) -> activate#(V1))
        (activate#(n__isNat(X)) -> isNat#(X), isNat#(n__plus(V1, V2)) -> activate#(V2))
        (activate#(n__isNat(X)) -> isNat#(X), isNat#(n__plus(V1, V2)) -> and#(isNat(activate(V1)), n__isNat(activate(V2))))
        (activate#(n__isNat(X)) -> isNat#(X), isNat#(n__plus(V1, V2)) -> isNat#(activate(V1)))}
       SCCS:
        Scc:
         {    activate#(n__isNat(X)) -> isNat#(X),
          activate#(n__plus(X1, X2)) -> activate#(X1),
          activate#(n__plus(X1, X2)) -> activate#(X2),
          activate#(n__plus(X1, X2)) -> plus#(activate(X1), activate(X2)),
                       U11#(tt(), N) -> activate#(N),
                       plus#(N, 0()) -> U11#(isNat(N), N),
                       plus#(N, 0()) -> isNat#(N),
                       and#(tt(), X) -> activate#(X),
             isNat#(n__plus(V1, V2)) -> activate#(V1),
             isNat#(n__plus(V1, V2)) -> activate#(V2),
             isNat#(n__plus(V1, V2)) -> and#(isNat(activate(V1)), n__isNat(activate(V2))),
             isNat#(n__plus(V1, V2)) -> isNat#(activate(V1))}
        SCC:
         Strict:
          {    activate#(n__isNat(X)) -> isNat#(X),
           activate#(n__plus(X1, X2)) -> activate#(X1),
           activate#(n__plus(X1, X2)) -> activate#(X2),
           activate#(n__plus(X1, X2)) -> plus#(activate(X1), activate(X2)),
                        U11#(tt(), N) -> activate#(N),
                        plus#(N, 0()) -> U11#(isNat(N), N),
                        plus#(N, 0()) -> isNat#(N),
                        and#(tt(), X) -> activate#(X),
              isNat#(n__plus(V1, V2)) -> activate#(V1),
              isNat#(n__plus(V1, V2)) -> activate#(V2),
              isNat#(n__plus(V1, V2)) -> and#(isNat(activate(V1)), n__isNat(activate(V2))),
              isNat#(n__plus(V1, V2)) -> isNat#(activate(V1))}
         Weak:
         {              activate(X) -> X,
                   activate(n__0()) -> 0(),
              activate(n__isNat(X)) -> isNat(X),
          activate(n__plus(X1, X2)) -> plus(activate(X1), activate(X2)),
                  activate(n__s(X)) -> s(activate(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()}
         POLY:
          Argument Filtering:
           pi(0) = [], pi(n__s) = 0, pi(n__plus) = [0,1], pi(n__isNat) = 0, pi(n__0) = [], pi(isNat#) = 0, pi(isNat) = 0, pi(and#) = 1, pi(and) = 1, pi(U21) = [1,2], pi(plus#) = [0,1], pi(plus) = [0,1], pi(s) = 0, pi(tt) = [], pi(U11#) = 1, pi(U11) = [1], pi(activate#) = 0, pi(activate) = 0
          Usable Rules:
           {}
          Interpretation:
           [plus#](x0, x1) = x0 + x1,
           [n__plus](x0, x1) = x0 + x1,
           [0] = 1
          Strict:
           {    activate#(n__isNat(X)) -> isNat#(X),
            activate#(n__plus(X1, X2)) -> activate#(X1),
            activate#(n__plus(X1, X2)) -> activate#(X2),
            activate#(n__plus(X1, X2)) -> plus#(activate(X1), activate(X2)),
                         U11#(tt(), N) -> activate#(N),
                         and#(tt(), X) -> activate#(X),
               isNat#(n__plus(V1, V2)) -> activate#(V1),
               isNat#(n__plus(V1, V2)) -> activate#(V2),
               isNat#(n__plus(V1, V2)) -> and#(isNat(activate(V1)), n__isNat(activate(V2))),
               isNat#(n__plus(V1, V2)) -> isNat#(activate(V1))}
          Weak:
           {              activate(X) -> X,
                     activate(n__0()) -> 0(),
                activate(n__isNat(X)) -> isNat(X),
            activate(n__plus(X1, X2)) -> plus(activate(X1), activate(X2)),
                    activate(n__s(X)) -> s(activate(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()}
          EDG:
           {(activate#(n__isNat(X)) -> isNat#(X), isNat#(n__plus(V1, V2)) -> isNat#(activate(V1)))
            (activate#(n__isNat(X)) -> isNat#(X), isNat#(n__plus(V1, V2)) -> and#(isNat(activate(V1)), n__isNat(activate(V2))))
            (activate#(n__isNat(X)) -> isNat#(X), isNat#(n__plus(V1, V2)) -> activate#(V2))
            (activate#(n__isNat(X)) -> isNat#(X), isNat#(n__plus(V1, V2)) -> activate#(V1))
            (isNat#(n__plus(V1, V2)) -> activate#(V1), activate#(n__plus(X1, X2)) -> plus#(activate(X1), activate(X2)))
            (isNat#(n__plus(V1, V2)) -> activate#(V1), activate#(n__plus(X1, X2)) -> activate#(X2))
            (isNat#(n__plus(V1, V2)) -> activate#(V1), activate#(n__plus(X1, X2)) -> activate#(X1))
            (isNat#(n__plus(V1, V2)) -> activate#(V1), activate#(n__isNat(X)) -> isNat#(X))
            (isNat#(n__plus(V1, V2)) -> and#(isNat(activate(V1)), n__isNat(activate(V2))), and#(tt(), X) -> activate#(X))
            (activate#(n__plus(X1, X2)) -> activate#(X1), activate#(n__plus(X1, X2)) -> plus#(activate(X1), activate(X2)))
            (activate#(n__plus(X1, X2)) -> activate#(X1), activate#(n__plus(X1, X2)) -> activate#(X2))
            (activate#(n__plus(X1, X2)) -> activate#(X1), activate#(n__plus(X1, X2)) -> activate#(X1))
            (activate#(n__plus(X1, X2)) -> activate#(X1), activate#(n__isNat(X)) -> isNat#(X))
            (activate#(n__plus(X1, X2)) -> activate#(X2), activate#(n__plus(X1, X2)) -> plus#(activate(X1), activate(X2)))
            (activate#(n__plus(X1, X2)) -> activate#(X2), activate#(n__plus(X1, X2)) -> activate#(X2))
            (activate#(n__plus(X1, X2)) -> activate#(X2), activate#(n__plus(X1, X2)) -> activate#(X1))
            (activate#(n__plus(X1, X2)) -> activate#(X2), activate#(n__isNat(X)) -> isNat#(X))
            (isNat#(n__plus(V1, V2)) -> isNat#(activate(V1)), isNat#(n__plus(V1, V2)) -> activate#(V1))
            (isNat#(n__plus(V1, V2)) -> isNat#(activate(V1)), isNat#(n__plus(V1, V2)) -> activate#(V2))
            (isNat#(n__plus(V1, V2)) -> isNat#(activate(V1)), isNat#(n__plus(V1, V2)) -> and#(isNat(activate(V1)), n__isNat(activate(V2))))
            (isNat#(n__plus(V1, V2)) -> isNat#(activate(V1)), isNat#(n__plus(V1, V2)) -> isNat#(activate(V1)))
            (isNat#(n__plus(V1, V2)) -> activate#(V2), activate#(n__isNat(X)) -> isNat#(X))
            (isNat#(n__plus(V1, V2)) -> activate#(V2), activate#(n__plus(X1, X2)) -> activate#(X1))
            (isNat#(n__plus(V1, V2)) -> activate#(V2), activate#(n__plus(X1, X2)) -> activate#(X2))
            (isNat#(n__plus(V1, V2)) -> activate#(V2), activate#(n__plus(X1, X2)) -> plus#(activate(X1), activate(X2)))
            (and#(tt(), X) -> activate#(X), activate#(n__isNat(X)) -> isNat#(X))
            (and#(tt(), X) -> activate#(X), activate#(n__plus(X1, X2)) -> activate#(X1))
            (and#(tt(), X) -> activate#(X), activate#(n__plus(X1, X2)) -> activate#(X2))
            (and#(tt(), X) -> activate#(X), activate#(n__plus(X1, X2)) -> plus#(activate(X1), activate(X2)))
            (U11#(tt(), N) -> activate#(N), activate#(n__isNat(X)) -> isNat#(X))
            (U11#(tt(), N) -> activate#(N), activate#(n__plus(X1, X2)) -> activate#(X1))
            (U11#(tt(), N) -> activate#(N), activate#(n__plus(X1, X2)) -> activate#(X2))
            (U11#(tt(), N) -> activate#(N), activate#(n__plus(X1, X2)) -> plus#(activate(X1), activate(X2)))}
           SCCS:
            Scc:
             {    activate#(n__isNat(X)) -> isNat#(X),
              activate#(n__plus(X1, X2)) -> activate#(X1),
              activate#(n__plus(X1, X2)) -> activate#(X2),
                           and#(tt(), X) -> activate#(X),
                 isNat#(n__plus(V1, V2)) -> activate#(V1),
                 isNat#(n__plus(V1, V2)) -> activate#(V2),
                 isNat#(n__plus(V1, V2)) -> and#(isNat(activate(V1)), n__isNat(activate(V2))),
                 isNat#(n__plus(V1, V2)) -> isNat#(activate(V1))}
            SCC:
             Strict:
              {    activate#(n__isNat(X)) -> isNat#(X),
               activate#(n__plus(X1, X2)) -> activate#(X1),
               activate#(n__plus(X1, X2)) -> activate#(X2),
                            and#(tt(), X) -> activate#(X),
                  isNat#(n__plus(V1, V2)) -> activate#(V1),
                  isNat#(n__plus(V1, V2)) -> activate#(V2),
                  isNat#(n__plus(V1, V2)) -> and#(isNat(activate(V1)), n__isNat(activate(V2))),
                  isNat#(n__plus(V1, V2)) -> isNat#(activate(V1))}
             Weak:
             {              activate(X) -> X,
                       activate(n__0()) -> 0(),
                  activate(n__isNat(X)) -> isNat(X),
              activate(n__plus(X1, X2)) -> plus(activate(X1), activate(X2)),
                      activate(n__s(X)) -> s(activate(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()}
             POLY:
              Argument Filtering:
               pi(0) = [], pi(n__s) = 0, pi(n__plus) = [0,1], pi(n__isNat) = 0, pi(n__0) = [], pi(isNat#) = [0], pi(isNat) = 0, pi(and#) = [1], pi(and) = 1, pi(U21) = [1,2], pi(plus) = [0,1], pi(s) = 0, pi(tt) = [], pi(U11) = 1, pi(activate#) = [0], pi(activate) = 0
              Usable Rules:
               {}
              Interpretation:
               [and#](x0) = x0 + 1,
               [isNat#](x0) = x0 + 1,
               [activate#](x0) = x0 + 1,
               [n__plus](x0, x1) = x0 + x1 + 1
              Strict:
               {activate#(n__isNat(X)) -> isNat#(X),
                         and#(tt(), X) -> activate#(X)}
              Weak:
               {              activate(X) -> X,
                         activate(n__0()) -> 0(),
                    activate(n__isNat(X)) -> isNat(X),
                activate(n__plus(X1, X2)) -> plus(activate(X1), activate(X2)),
                        activate(n__s(X)) -> s(activate(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()}
              EDG:
               {(and#(tt(), X) -> activate#(X), activate#(n__isNat(X)) -> isNat#(X))}
               SCCS:
                
                Qed