YES(?,O(n^3))

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

Proof:
 RT Transformation Processor:
  strict:
   a(b(a(x1))) -> a(b(b(a(x1))))
   b(b(b(x1))) -> b(b(x1))
  weak:
   
  Bounds Processor:
   bound: 1
   enrichment: match-rt
   automaton:
    final states: {3}
    transitions:
     a1(12) -> 13*
     a1(9) -> 10*
     b1(25) -> 26*
     b1(10) -> 11*
     b1(11) -> 12*
     a0(3) -> 3*
     b0(3) -> 3*
     3 -> 9*
     13 -> 10,25,3
     26 -> 11*
   problem:
    strict:
     b(b(b(x1))) -> b(b(x1))
    weak:
     a(b(a(x1))) -> a(b(b(a(x1))))
   Matrix Interpretation Processor:
    dimension: 3
    interpretation:
               [1 0 2]     [1]
     [b](x0) = [0 0 1]x0 + [0]
               [0 0 0]     [0],
     
               [1 2 0]     [3]
     [a](x0) = [0 0 0]x0 + [1]
               [0 0 0]     [2]
    orientation:
                   [1 0 2]     [3]    [1 0 2]     [2]           
     b(b(b(x1))) = [0 0 0]x1 + [0] >= [0 0 0]x1 + [0] = b(b(x1))
                   [0 0 0]     [0]    [0 0 0]     [0]           
     
                   [1 2 0]     [15]    [1 2 0]     [12]                 
     a(b(a(x1))) = [0 0 0]x1 + [1 ] >= [0 0 0]x1 + [1 ] = a(b(b(a(x1))))
                   [0 0 0]     [2 ]    [0 0 0]     [2 ]                 
    problem:
     strict:
      
     weak:
      b(b(b(x1))) -> b(b(x1))
      a(b(a(x1))) -> a(b(b(a(x1))))
    Qed