YES

Problem:
 a(b(a(x))) -> b(a(b(x)))

Proof:
 DP Processor:
  DPs:
   a#(b(a(x))) -> a#(b(x))
  TRS:
   a(b(a(x))) -> b(a(b(x)))
  Usable Rule Processor:
   DPs:
    a#(b(a(x))) -> a#(b(x))
   TRS:
    
   Arctic Interpretation Processor:
    dimension: 2
    usable rules:
     
    interpretation:
     [a#](x0) = [-4 1 ]x0 + [0],
     
               [-& 2 ]     [1 ]
     [b](x0) = [2  1 ]x0 + [-4],
     
               [-& -1]     [1 ]
     [a](x0) = [2  3 ]x0 + [-2]
    orientation:
     a#(b(a(x))) = [4 5]x + [4] >= [3 2]x + [0] = a#(b(x))
    problem:
     DPs:
      
     TRS:
      
    Qed