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