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