YES
Time: 0.007900
TRS:
 {  activate X -> X,
  and(tt(), X) -> activate X,
  plus(N, 0()) -> N,
  plus(N, s M) -> s plus(N, M),
     x(N, 0()) -> 0(),
     x(N, s M) -> plus(x(N, M), N)}
 DP:
  DP:
   {and#(tt(), X) -> activate# X,
    plus#(N, s M) -> plus#(N, M),
       x#(N, s M) -> plus#(x(N, M), N),
       x#(N, s M) -> x#(N, M)}
  TRS:
  {  activate X -> X,
   and(tt(), X) -> activate X,
   plus(N, 0()) -> N,
   plus(N, s M) -> s plus(N, M),
      x(N, 0()) -> 0(),
      x(N, s M) -> plus(x(N, M), N)}
  UR:
   {plus(N, 0()) -> N,
    plus(N, s M) -> s plus(N, M),
       x(N, 0()) -> 0(),
       x(N, s M) -> plus(x(N, M), N),
         a(x, y) -> x,
         a(x, y) -> y}
   EDG:
    {(x#(N, s M) -> plus#(x(N, M), N), plus#(N, s M) -> plus#(N, M))
     (x#(N, s M) -> x#(N, M), x#(N, s M) -> x#(N, M))
     (x#(N, s M) -> x#(N, M), x#(N, s M) -> plus#(x(N, M), N))
     (plus#(N, s M) -> plus#(N, M), plus#(N, s M) -> plus#(N, M))}
    STATUS:
     arrows: 0.750000
     SCCS (2):
      Scc:
       {x#(N, s M) -> x#(N, M)}
      Scc:
       {plus#(N, s M) -> plus#(N, M)}
      
      SCC (1):
       Strict:
        {x#(N, s M) -> x#(N, M)}
       Weak:
       {  activate X -> X,
        and(tt(), X) -> activate X,
        plus(N, 0()) -> N,
        plus(N, s M) -> s plus(N, M),
           x(N, 0()) -> 0(),
           x(N, s M) -> plus(x(N, M), N)}
       POLY:
        Mode: weak, max_in=1, output_bits=-1, dnum=1, ur=true
        Interpretation:
         [and](x0, x1) = 0,
         
         [plus](x0, x1) = x0 + 1,
         
         [x](x0, x1) = x0 + 1,
         
         [activate](x0) = 0,
         
         [s](x0) = x0 + 1,
         
         [tt] = 0,
         
         [0] = 1,
         
         [x#](x0, x1) = x0 + 1
        Strict:
         x#(N, s M) -> x#(N, M)
         2 + 0N + 1M >= 1 + 0N + 1M
        Weak:
         x(N, s M) -> plus(x(N, M), N)
         2 + 0N + 1M >= 1 + 1N + 0M
         x(N, 0()) -> 0()
         2 + 0N >= 1
         plus(N, s M) -> s plus(N, M)
         2 + 0N + 1M >= 2 + 0N + 1M
         plus(N, 0()) -> N
         2 + 0N >= 1N
         and(tt(), X) -> activate X
         0 + 0X >= 0 + 0X
         activate X -> X
         0 + 0X >= 1X
       Qed
     
     SCC (1):
      Strict:
       {plus#(N, s M) -> plus#(N, M)}
      Weak:
      {  activate X -> X,
       and(tt(), X) -> activate X,
       plus(N, 0()) -> N,
       plus(N, s M) -> s plus(N, M),
          x(N, 0()) -> 0(),
          x(N, s M) -> plus(x(N, M), N)}
      POLY:
       Mode: weak, max_in=1, output_bits=-1, dnum=1, ur=true
       Interpretation:
        [and](x0, x1) = 0,
        
        [plus](x0, x1) = x0 + 1,
        
        [x](x0, x1) = x0 + 1,
        
        [activate](x0) = 0,
        
        [s](x0) = x0 + 1,
        
        [tt] = 0,
        
        [0] = 1,
        
        [plus#](x0, x1) = x0 + 1
       Strict:
        plus#(N, s M) -> plus#(N, M)
        2 + 0N + 1M >= 1 + 0N + 1M
       Weak:
        x(N, s M) -> plus(x(N, M), N)
        2 + 0N + 1M >= 1 + 1N + 0M
        x(N, 0()) -> 0()
        2 + 0N >= 1
        plus(N, s M) -> s plus(N, M)
        2 + 0N + 1M >= 2 + 0N + 1M
        plus(N, 0()) -> N
        2 + 0N >= 1N
        and(tt(), X) -> activate X
        0 + 0X >= 0 + 0X
        activate X -> X
        0 + 0X >= 1X
      Qed