YES

Problem:
 U11(tt(),N) -> activate(N)
 U21(tt(),M,N) -> s(plus(activate(N),activate(M)))
 and(tt(),X) -> activate(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))
 plus(N,0()) -> U11(isNat(N),N)
 plus(N,s(M)) -> U21(and(isNat(M),n__isNat(N)),M,N)
 0() -> n__0()
 plus(X1,X2) -> n__plus(X1,X2)
 isNat(X) -> n__isNat(X)
 s(X) -> n__s(X)
 activate(n__0()) -> 0()
 activate(n__plus(X1,X2)) -> plus(X1,X2)
 activate(n__isNat(X)) -> isNat(X)
 activate(n__s(X)) -> s(X)
 activate(X) -> X

Proof:
 DP Processor:
  DPs:
   U11#(tt(),N) -> activate#(N)
   U21#(tt(),M,N) -> activate#(M)
   U21#(tt(),M,N) -> activate#(N)
   U21#(tt(),M,N) -> plus#(activate(N),activate(M))
   U21#(tt(),M,N) -> s#(plus(activate(N),activate(M)))
   and#(tt(),X) -> activate#(X)
   isNat#(n__plus(V1,V2)) -> activate#(V2)
   isNat#(n__plus(V1,V2)) -> 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__s(V1)) -> activate#(V1)
   isNat#(n__s(V1)) -> isNat#(activate(V1))
   plus#(N,0()) -> isNat#(N)
   plus#(N,0()) -> U11#(isNat(N),N)
   plus#(N,s(M)) -> isNat#(M)
   plus#(N,s(M)) -> and#(isNat(M),n__isNat(N))
   plus#(N,s(M)) -> U21#(and(isNat(M),n__isNat(N)),M,N)
   activate#(n__0()) -> 0#()
   activate#(n__plus(X1,X2)) -> plus#(X1,X2)
   activate#(n__isNat(X)) -> isNat#(X)
   activate#(n__s(X)) -> s#(X)
  TRS:
   U11(tt(),N) -> activate(N)
   U21(tt(),M,N) -> s(plus(activate(N),activate(M)))
   and(tt(),X) -> activate(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))
   plus(N,0()) -> U11(isNat(N),N)
   plus(N,s(M)) -> U21(and(isNat(M),n__isNat(N)),M,N)
   0() -> n__0()
   plus(X1,X2) -> n__plus(X1,X2)
   isNat(X) -> n__isNat(X)
   s(X) -> n__s(X)
   activate(n__0()) -> 0()
   activate(n__plus(X1,X2)) -> plus(X1,X2)
   activate(n__isNat(X)) -> isNat(X)
   activate(n__s(X)) -> s(X)
   activate(X) -> X
  TDG Processor:
   DPs:
    U11#(tt(),N) -> activate#(N)
    U21#(tt(),M,N) -> activate#(M)
    U21#(tt(),M,N) -> activate#(N)
    U21#(tt(),M,N) -> plus#(activate(N),activate(M))
    U21#(tt(),M,N) -> s#(plus(activate(N),activate(M)))
    and#(tt(),X) -> activate#(X)
    isNat#(n__plus(V1,V2)) -> activate#(V2)
    isNat#(n__plus(V1,V2)) -> 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__s(V1)) -> activate#(V1)
    isNat#(n__s(V1)) -> isNat#(activate(V1))
    plus#(N,0()) -> isNat#(N)
    plus#(N,0()) -> U11#(isNat(N),N)
    plus#(N,s(M)) -> isNat#(M)
    plus#(N,s(M)) -> and#(isNat(M),n__isNat(N))
    plus#(N,s(M)) -> U21#(and(isNat(M),n__isNat(N)),M,N)
    activate#(n__0()) -> 0#()
    activate#(n__plus(X1,X2)) -> plus#(X1,X2)
    activate#(n__isNat(X)) -> isNat#(X)
    activate#(n__s(X)) -> s#(X)
   TRS:
    U11(tt(),N) -> activate(N)
    U21(tt(),M,N) -> s(plus(activate(N),activate(M)))
    and(tt(),X) -> activate(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))
    plus(N,0()) -> U11(isNat(N),N)
    plus(N,s(M)) -> U21(and(isNat(M),n__isNat(N)),M,N)
    0() -> n__0()
    plus(X1,X2) -> n__plus(X1,X2)
    isNat(X) -> n__isNat(X)
    s(X) -> n__s(X)
    activate(n__0()) -> 0()
    activate(n__plus(X1,X2)) -> plus(X1,X2)
    activate(n__isNat(X)) -> isNat(X)
    activate(n__s(X)) -> s(X)
    activate(X) -> X
   graph:
    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__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__plus(V1,V2)) -> activate#(V1)
    isNat#(n__s(V1)) -> isNat#(activate(V1)) ->
    isNat#(n__plus(V1,V2)) -> activate#(V2)
    isNat#(n__s(V1)) -> activate#(V1) ->
    activate#(n__s(X)) -> s#(X)
    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__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)) -> 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)) -> 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)) -> and#(isNat(activate(V1)),n__isNat(activate(V2))) ->
    and#(tt(),X) -> activate#(X)
    isNat#(n__plus(V1,V2)) -> activate#(V2) ->
    activate#(n__s(X)) -> s#(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)) -> plus#(X1,X2)
    isNat#(n__plus(V1,V2)) -> activate#(V2) ->
    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__isNat(X)) -> isNat#(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#()
    and#(tt(),X) -> activate#(X) -> activate#(n__s(X)) -> s#(X)
    and#(tt(),X) -> activate#(X) -> activate#(n__isNat(X)) -> isNat#(X)
    and#(tt(),X) -> activate#(X) ->
    activate#(n__plus(X1,X2)) -> plus#(X1,X2)
    and#(tt(),X) -> activate#(X) -> 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)) -> 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__plus(V1,V2)) -> activate#(V1)
    plus#(N,0()) -> isNat#(N) ->
    isNat#(n__plus(V1,V2)) -> activate#(V2)
    plus#(N,0()) -> U11#(isNat(N),N) -> U11#(tt(),N) -> activate#(N)
    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)
    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__plus(V1,V2)) -> activate#(V1)
    plus#(N,s(M)) -> isNat#(M) ->
    isNat#(n__plus(V1,V2)) -> activate#(V2)
    plus#(N,s(M)) -> and#(isNat(M),n__isNat(N)) ->
    and#(tt(),X) -> activate#(X)
    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) -> plus#(activate(N),activate(M))
    plus#(N,s(M)) -> U21#(and(isNat(M),n__isNat(N)),M,N) ->
    U21#(tt(),M,N) -> activate#(N)
    plus#(N,s(M)) -> U21#(and(isNat(M),n__isNat(N)),M,N) ->
    U21#(tt(),M,N) -> activate#(M)
    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)
    U21#(tt(),M,N) -> activate#(N) -> activate#(n__s(X)) -> s#(X)
    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__0()) -> 0#()
    U21#(tt(),M,N) -> activate#(M) -> activate#(n__s(X)) -> s#(X)
    U21#(tt(),M,N) -> activate#(M) ->
    activate#(n__isNat(X)) -> isNat#(X)
    U21#(tt(),M,N) -> activate#(M) ->
    activate#(n__plus(X1,X2)) -> plus#(X1,X2)
    U21#(tt(),M,N) -> activate#(M) -> 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)) -> and#(isNat(activate(V1)),n__isNat(activate(V2)))
    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)) -> activate#(V1)
    activate#(n__isNat(X)) -> isNat#(X) ->
    isNat#(n__plus(V1,V2)) -> activate#(V2)
    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)
    U11#(tt(),N) -> activate#(N) -> activate#(n__s(X)) -> s#(X)
    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__0()) -> 0#()
   SCC Processor:
    #sccs: 1
    #rules: 18
    #arcs: 75/441
    DPs:
     isNat#(n__s(V1)) -> isNat#(activate(V1))
     isNat#(n__plus(V1,V2)) -> activate#(V2)
     activate#(n__plus(X1,X2)) -> plus#(X1,X2)
     plus#(N,0()) -> isNat#(N)
     isNat#(n__plus(V1,V2)) -> activate#(V1)
     activate#(n__isNat(X)) -> isNat#(X)
     isNat#(n__plus(V1,V2)) -> isNat#(activate(V1))
     isNat#(n__plus(V1,V2)) -> and#(isNat(activate(V1)),n__isNat(activate(V2)))
     and#(tt(),X) -> activate#(X)
     isNat#(n__s(V1)) -> activate#(V1)
     plus#(N,0()) -> U11#(isNat(N),N)
     U11#(tt(),N) -> activate#(N)
     plus#(N,s(M)) -> isNat#(M)
     plus#(N,s(M)) -> and#(isNat(M),n__isNat(N))
     plus#(N,s(M)) -> U21#(and(isNat(M),n__isNat(N)),M,N)
     U21#(tt(),M,N) -> activate#(M)
     U21#(tt(),M,N) -> activate#(N)
     U21#(tt(),M,N) -> plus#(activate(N),activate(M))
    TRS:
     U11(tt(),N) -> activate(N)
     U21(tt(),M,N) -> s(plus(activate(N),activate(M)))
     and(tt(),X) -> activate(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))
     plus(N,0()) -> U11(isNat(N),N)
     plus(N,s(M)) -> U21(and(isNat(M),n__isNat(N)),M,N)
     0() -> n__0()
     plus(X1,X2) -> n__plus(X1,X2)
     isNat(X) -> n__isNat(X)
     s(X) -> n__s(X)
     activate(n__0()) -> 0()
     activate(n__plus(X1,X2)) -> plus(X1,X2)
     activate(n__isNat(X)) -> isNat(X)
     activate(n__s(X)) -> s(X)
     activate(X) -> X
    KBO Processor:
     argument filtering:
      pi(tt) = []
      pi(U11) = [1]
      pi(activate) = [0]
      pi(U21) = [1,2]
      pi(plus) = [0,1]
      pi(s) = [0]
      pi(and) = [0,1]
      pi(n__0) = []
      pi(isNat) = 0
      pi(n__plus) = [0,1]
      pi(n__isNat) = 0
      pi(n__s) = [0]
      pi(0) = []
      pi(U11#) = 1
      pi(activate#) = 0
      pi(U21#) = [1,2]
      pi(plus#) = [0,1]
      pi(and#) = 1
      pi(isNat#) = 0
     usable rules:
      U11(tt(),N) -> activate(N)
      U21(tt(),M,N) -> s(plus(activate(N),activate(M)))
      and(tt(),X) -> activate(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))
      plus(N,0()) -> U11(isNat(N),N)
      plus(N,s(M)) -> U21(and(isNat(M),n__isNat(N)),M,N)
      0() -> n__0()
      plus(X1,X2) -> n__plus(X1,X2)
      isNat(X) -> n__isNat(X)
      s(X) -> n__s(X)
      activate(n__0()) -> 0()
      activate(n__plus(X1,X2)) -> plus(X1,X2)
      activate(n__isNat(X)) -> isNat(X)
      activate(n__s(X)) -> s(X)
      activate(X) -> X
     weight function:
      w0 = 1
      w(U11#) = w(0) = w(n__s) = w(n__0) = w(s) = w(U21) = w(U11) = w(
      tt) = 1
      w(isNat#) = w(and#) = w(plus#) = w(U21#) = w(activate#) = w(n__isNat) = w(
      n__plus) = w(isNat) = w(and) = w(plus) = w(activate) = 0
     precedence:
      activate > plus > U21# ~ 0 ~ U21 > n__plus ~ n__0 ~ s > isNat# ~ 
      and# ~ plus# ~ activate# ~ U11# ~ n__s ~ n__isNat ~ isNat ~ and ~ 
      U11 ~ tt
     problem:
      DPs:
       activate#(n__isNat(X)) -> isNat#(X)
       and#(tt(),X) -> activate#(X)
       U11#(tt(),N) -> activate#(N)
      TRS:
       U11(tt(),N) -> activate(N)
       U21(tt(),M,N) -> s(plus(activate(N),activate(M)))
       and(tt(),X) -> activate(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))
       plus(N,0()) -> U11(isNat(N),N)
       plus(N,s(M)) -> U21(and(isNat(M),n__isNat(N)),M,N)
       0() -> n__0()
       plus(X1,X2) -> n__plus(X1,X2)
       isNat(X) -> n__isNat(X)
       s(X) -> n__s(X)
       activate(n__0()) -> 0()
       activate(n__plus(X1,X2)) -> plus(X1,X2)
       activate(n__isNat(X)) -> isNat(X)
       activate(n__s(X)) -> s(X)
       activate(X) -> X
     Restore Modifier:
      DPs:
       activate#(n__isNat(X)) -> isNat#(X)
       and#(tt(),X) -> activate#(X)
       U11#(tt(),N) -> activate#(N)
      TRS:
       U11(tt(),N) -> activate(N)
       U21(tt(),M,N) -> s(plus(activate(N),activate(M)))
       and(tt(),X) -> activate(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))
       plus(N,0()) -> U11(isNat(N),N)
       plus(N,s(M)) -> U21(and(isNat(M),n__isNat(N)),M,N)
       0() -> n__0()
       plus(X1,X2) -> n__plus(X1,X2)
       isNat(X) -> n__isNat(X)
       s(X) -> n__s(X)
       activate(n__0()) -> 0()
       activate(n__plus(X1,X2)) -> plus(X1,X2)
       activate(n__isNat(X)) -> isNat(X)
       activate(n__s(X)) -> s(X)
       activate(X) -> X
      SCC Processor:
       #sccs: 0
       #rules: 0
       #arcs: 60/9