YES(?,O(n^1))

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

Proof:
 RT Transformation Processor:
  strict:
   g(b()) -> f(b())
   f(a()) -> g(a())
   b() -> a()
  weak:
   
  Matrix Interpretation Processor:
   dimension: 1
   interpretation:
    [a] = 8,
    
    [f](x0) = x0 + 22,
    
    [g](x0) = x0 + 31,
    
    [b] = 13
   orientation:
    g(b()) = 44 >= 35 = f(b())
    
    f(a()) = 30 >= 39 = g(a())
    
    b() = 13 >= 8 = a()
   problem:
    strict:
     f(a()) -> g(a())
    weak:
     g(b()) -> f(b())
     b() -> a()
   Bounds Processor:
    bound: 1
    enrichment: match-rt
    automaton:
     final states: {5}
     transitions:
      g1(8) -> 9*
      a1() -> 8*
      f0(5) -> 5*
      a0() -> 5*
      g0(5) -> 5*
      b0() -> 5*
      9 -> 5*
    problem:
     strict:
      
     weak:
      f(a()) -> g(a())
      g(b()) -> f(b())
      b() -> a()
    Qed