YES(?,O(n^1))

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

Proof:
 Matrix Interpretation Processor:
  dimension: 1
  interpretation:
   [b](x0) = x0 + 7,
   
   [a](x0) = x0 + 11
  orientation:
   a(a(x1)) = x1 + 22 >= x1 + 21 = b(b(b(x1)))
   
   b(b(b(b(b(x1))))) = x1 + 35 >= x1 + 33 = a(a(a(x1)))
  problem:
   
  Qed