YES

Problem:
 U11(tt(),M,N) -> U12(tt(),activate(M),activate(N))
 U12(tt(),M,N) -> s(plus(activate(N),activate(M)))
 U21(tt(),M,N) -> U22(tt(),activate(M),activate(N))
 U22(tt(),M,N) -> plus(x(activate(N),activate(M)),activate(N))
 plus(N,0()) -> N
 plus(N,s(M)) -> U11(tt(),M,N)
 x(N,0()) -> 0()
 x(N,s(M)) -> U21(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))
   U21#(tt(),M,N) -> activate#(N)
   U21#(tt(),M,N) -> activate#(M)
   U21#(tt(),M,N) -> U22#(tt(),activate(M),activate(N))
   U22#(tt(),M,N) -> activate#(M)
   U22#(tt(),M,N) -> activate#(N)
   U22#(tt(),M,N) -> x#(activate(N),activate(M))
   U22#(tt(),M,N) -> plus#(x(activate(N),activate(M)),activate(N))
   plus#(N,s(M)) -> U11#(tt(),M,N)
   x#(N,s(M)) -> U21#(tt(),M,N)
  TRS:
   U11(tt(),M,N) -> U12(tt(),activate(M),activate(N))
   U12(tt(),M,N) -> s(plus(activate(N),activate(M)))
   U21(tt(),M,N) -> U22(tt(),activate(M),activate(N))
   U22(tt(),M,N) -> plus(x(activate(N),activate(M)),activate(N))
   plus(N,0()) -> N
   plus(N,s(M)) -> U11(tt(),M,N)
   x(N,0()) -> 0()
   x(N,s(M)) -> U21(tt(),M,N)
   activate(X) -> X
  TDG 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))
    U21#(tt(),M,N) -> activate#(N)
    U21#(tt(),M,N) -> activate#(M)
    U21#(tt(),M,N) -> U22#(tt(),activate(M),activate(N))
    U22#(tt(),M,N) -> activate#(M)
    U22#(tt(),M,N) -> activate#(N)
    U22#(tt(),M,N) -> x#(activate(N),activate(M))
    U22#(tt(),M,N) -> plus#(x(activate(N),activate(M)),activate(N))
    plus#(N,s(M)) -> U11#(tt(),M,N)
    x#(N,s(M)) -> U21#(tt(),M,N)
   TRS:
    U11(tt(),M,N) -> U12(tt(),activate(M),activate(N))
    U12(tt(),M,N) -> s(plus(activate(N),activate(M)))
    U21(tt(),M,N) -> U22(tt(),activate(M),activate(N))
    U22(tt(),M,N) -> plus(x(activate(N),activate(M)),activate(N))
    plus(N,0()) -> N
    plus(N,s(M)) -> U11(tt(),M,N)
    x(N,0()) -> 0()
    x(N,s(M)) -> U21(tt(),M,N)
    activate(X) -> X
   graph:
    x#(N,s(M)) -> U21#(tt(),M,N) ->
    U21#(tt(),M,N) -> U22#(tt(),activate(M),activate(N))
    x#(N,s(M)) -> U21#(tt(),M,N) -> U21#(tt(),M,N) -> activate#(M)
    x#(N,s(M)) -> U21#(tt(),M,N) ->
    U21#(tt(),M,N) -> activate#(N)
    U22#(tt(),M,N) -> x#(activate(N),activate(M)) ->
    x#(N,s(M)) -> U21#(tt(),M,N)
    U22#(tt(),M,N) -> plus#(x(activate(N),activate(M)),activate(N)) ->
    plus#(N,s(M)) -> U11#(tt(),M,N)
    U21#(tt(),M,N) -> U22#(tt(),activate(M),activate(N)) ->
    U22#(tt(),M,N) -> plus#(x(activate(N),activate(M)),activate(N))
    U21#(tt(),M,N) -> U22#(tt(),activate(M),activate(N)) ->
    U22#(tt(),M,N) -> x#(activate(N),activate(M))
    U21#(tt(),M,N) -> U22#(tt(),activate(M),activate(N)) ->
    U22#(tt(),M,N) -> activate#(N)
    U21#(tt(),M,N) -> U22#(tt(),activate(M),activate(N)) ->
    U22#(tt(),M,N) -> activate#(M)
    plus#(N,s(M)) -> U11#(tt(),M,N) ->
    U11#(tt(),M,N) -> U12#(tt(),activate(M),activate(N))
    plus#(N,s(M)) -> U11#(tt(),M,N) ->
    U11#(tt(),M,N) -> activate#(M)
    plus#(N,s(M)) -> U11#(tt(),M,N) ->
    U11#(tt(),M,N) -> activate#(N)
    U12#(tt(),M,N) -> plus#(activate(N),activate(M)) ->
    plus#(N,s(M)) -> U11#(tt(),M,N)
    U11#(tt(),M,N) -> U12#(tt(),activate(M),activate(N)) ->
    U12#(tt(),M,N) -> plus#(activate(N),activate(M))
    U11#(tt(),M,N) -> U12#(tt(),activate(M),activate(N)) ->
    U12#(tt(),M,N) -> activate#(N)
    U11#(tt(),M,N) -> U12#(tt(),activate(M),activate(N)) -> U12#(tt(),M,N) -> activate#(M)
   SCC Processor:
    #sccs: 2
    #rules: 6
    #arcs: 16/225
    DPs:
     x#(N,s(M)) -> U21#(tt(),M,N)
     U21#(tt(),M,N) -> U22#(tt(),activate(M),activate(N))
     U22#(tt(),M,N) -> x#(activate(N),activate(M))
    TRS:
     U11(tt(),M,N) -> U12(tt(),activate(M),activate(N))
     U12(tt(),M,N) -> s(plus(activate(N),activate(M)))
     U21(tt(),M,N) -> U22(tt(),activate(M),activate(N))
     U22(tt(),M,N) -> plus(x(activate(N),activate(M)),activate(N))
     plus(N,0()) -> N
     plus(N,s(M)) -> U11(tt(),M,N)
     x(N,0()) -> 0()
     x(N,s(M)) -> U21(tt(),M,N)
     activate(X) -> X
    Usable Rule Processor:
     DPs:
      x#(N,s(M)) -> U21#(tt(),M,N)
      U21#(tt(),M,N) -> U22#(tt(),activate(M),activate(N))
      U22#(tt(),M,N) -> x#(activate(N),activate(M))
     TRS:
      activate(X) -> X
     Semantic Labeling Processor:
      dimension: 2
      usable rules:
       activate(X) -> X
      interpretation:
                 [0]
       [s](x0) = [0],
       
                        [0 1]     [1]
       [activate](x0) = [0 0]x0 + [1],
       
              [0]
       [tt] = [1]
       labeled:
       usable (for model):
       argument filtering:
        pi(tt) = []
        pi(activate) = [0]
        pi(s) = [0]
        pi(U21#) = [1]
        pi(U22#) = [1]
        pi(x#) = 1
      precedence:
       s > U21# > U22# > x# ~ activate ~ tt
      problem:
       DPs:
        
       TRS:
        activate(X) -> X
      Qed
    
    DPs:
     plus#(N,s(M)) -> U11#(tt(),M,N)
     U11#(tt(),M,N) -> U12#(tt(),activate(M),activate(N))
     U12#(tt(),M,N) -> plus#(activate(N),activate(M))
    TRS:
     U11(tt(),M,N) -> U12(tt(),activate(M),activate(N))
     U12(tt(),M,N) -> s(plus(activate(N),activate(M)))
     U21(tt(),M,N) -> U22(tt(),activate(M),activate(N))
     U22(tt(),M,N) -> plus(x(activate(N),activate(M)),activate(N))
     plus(N,0()) -> N
     plus(N,s(M)) -> U11(tt(),M,N)
     x(N,0()) -> 0()
     x(N,s(M)) -> U21(tt(),M,N)
     activate(X) -> X
    Usable Rule Processor:
     DPs:
      plus#(N,s(M)) -> U11#(tt(),M,N)
      U11#(tt(),M,N) -> U12#(tt(),activate(M),activate(N))
      U12#(tt(),M,N) -> plus#(activate(N),activate(M))
     TRS:
      activate(X) -> X
     Semantic Labeling Processor:
      dimension: 2
      usable rules:
       activate(X) -> X
      interpretation:
                 [0]
       [s](x0) = [0],
       
                        [0 1]     [1]
       [activate](x0) = [0 0]x0 + [1],
       
              [0]
       [tt] = [1]
       labeled:
       usable (for model):
       argument filtering:
        pi(tt) = []
        pi(activate) = [0]
        pi(s) = [0]
        pi(U11#) = [1]
        pi(U12#) = [1]
        pi(plus#) = 1
      precedence:
       s > U11# > U12# > plus# ~ activate ~ tt
      problem:
       DPs:
        
       TRS:
        activate(X) -> X
      Qed