YES(?,O(n^1))

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

Proof:
 RT Transformation Processor:
  strict:
   g(x,a(),b()) -> g(b(),b(),a())
  weak:
   
  Bounds Processor:
   bound: 1
   enrichment: match-rt
   automaton:
    final states: {3,2,1}
    transitions:
     g1(6,6,5) -> 1*
     b1() -> 6*
     a1() -> 5*
     g0(1,1,1) -> 1*
     g0(1,3,1) -> 1*
     g0(1,2,3) -> 1*
     g0(2,2,1) -> 1*
     g0(2,1,3) -> 1*
     g0(2,3,3) -> 1*
     g0(3,1,1) -> 1*
     g0(1,1,2) -> 1*
     g0(3,3,1) -> 1*
     g0(1,3,2) -> 1*
     g0(3,2,3) -> 1*
     g0(2,2,2) -> 1*
     g0(3,1,2) -> 1*
     g0(3,3,2) -> 1*
     g0(1,2,1) -> 1*
     g0(1,1,3) -> 1*
     g0(1,3,3) -> 1*
     g0(2,1,1) -> 1*
     g0(2,3,1) -> 1*
     g0(2,2,3) -> 1*
     g0(3,2,1) -> 1*
     g0(1,2,2) -> 1*
     g0(3,1,3) -> 1*
     g0(3,3,3) -> 1*
     g0(2,1,2) -> 1*
     g0(2,3,2) -> 1*
     g0(3,2,2) -> 1*
     a0() -> 2*
     b0() -> 3*
   problem:
    strict:
     
    weak:
     g(x,a(),b()) -> g(b(),b(),a())
   Qed