YES

Problem:
 U11(tt(),M,N) -> U12(tt(),activate(M),activate(N))
 U12(tt(),M,N) -> s(plus(activate(N),activate(M)))
 plus(N,0()) -> N
 plus(N,s(M)) -> U11(tt(),M,N)
 activate(X) -> X

Proof:
 DP Processor:
  DPs:
   U11#(tt(),M,N) -> activate#(N)
   U11#(tt(),M,N) -> activate#(M)
   U11#(tt(),M,N) -> U12#(tt(),activate(M),activate(N))
   U12#(tt(),M,N) -> activate#(M)
   U12#(tt(),M,N) -> activate#(N)
   U12#(tt(),M,N) -> plus#(activate(N),activate(M))
   plus#(N,s(M)) -> U11#(tt(),M,N)
  TRS:
   U11(tt(),M,N) -> U12(tt(),activate(M),activate(N))
   U12(tt(),M,N) -> s(plus(activate(N),activate(M)))
   plus(N,0()) -> N
   plus(N,s(M)) -> U11(tt(),M,N)
   activate(X) -> X
  Usable Rule Processor:
   DPs:
    U11#(tt(),M,N) -> activate#(N)
    U11#(tt(),M,N) -> activate#(M)
    U11#(tt(),M,N) -> U12#(tt(),activate(M),activate(N))
    U12#(tt(),M,N) -> activate#(M)
    U12#(tt(),M,N) -> activate#(N)
    U12#(tt(),M,N) -> plus#(activate(N),activate(M))
    plus#(N,s(M)) -> U11#(tt(),M,N)
   TRS:
    activate(X) -> X
   Arctic Interpretation Processor:
    dimension: 1
    usable rules:
     activate(X) -> X
    interpretation:
     [plus#](x0, x1) = x1,
     
     [U12#](x0, x1, x2) = x0 + 3x1 + 1,
     
     [activate#](x0) = 0,
     
     [U11#](x0, x1, x2) = 2x0 + 5x1 + 0,
     
     [s](x0) = 6x0 + 3,
     
     [activate](x0) = 1x0,
     
     [tt] = 0
    orientation:
     U11#(tt(),M,N) = 5M + 2 >= 0 = activate#(N)
     
     U11#(tt(),M,N) = 5M + 2 >= 0 = activate#(M)
     
     U11#(tt(),M,N) = 5M + 2 >= 4M + 1 = U12#(tt(),activate(M),activate(N))
     
     U12#(tt(),M,N) = 3M + 1 >= 0 = activate#(M)
     
     U12#(tt(),M,N) = 3M + 1 >= 0 = activate#(N)
     
     U12#(tt(),M,N) = 3M + 1 >= 1M = plus#(activate(N),activate(M))
     
     plus#(N,s(M)) = 6M + 3 >= 5M + 2 = U11#(tt(),M,N)
     
     activate(X) = 1X >= X = X
    problem:
     DPs:
      
     TRS:
      activate(X) -> X
    Qed