YES(?,O(n^1))

Problem:
 f(a()) -> f(b())
 g(b()) -> g(a())

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