YES
TRS:
 {a(b(a(x))) -> b(a(b(x)))}
 DP:
  Strict:
   {a#(b(a(x))) -> a#(b(x))}
  Weak:
  {a(b(a(x))) -> b(a(b(x)))}
  EDG:
   {(a#(b(a(x))) -> a#(b(x)), a#(b(a(x))) -> a#(b(x)))}
   SCCS:
    Scc:
     {a#(b(a(x))) -> a#(b(x))}
    SCC:
     Strict:
      {a#(b(a(x))) -> a#(b(x))}
     Weak:
     {a(b(a(x))) -> b(a(b(x)))}
     POLY:
      Argument Filtering:
       pi(a#) = 0, pi(a) = [0], pi(b) = 0
      Usable Rules:
       {}
      Interpretation:
       [a](x0) = x0 + 1
      Strict:
       {}
      Weak:
       {a(b(a(x))) -> b(a(b(x)))}
      Qed