YES(?,O(n^1))

Problem:
 f(1()) -> f(g(1()))
 f(f(x)) -> f(x)
 g(0()) -> g(f(0()))
 g(g(x)) -> g(x)

Proof:
 RT Transformation Processor:
  strict:
   f(1()) -> f(g(1()))
   f(f(x)) -> f(x)
   g(0()) -> g(f(0()))
   g(g(x)) -> g(x)
  weak:
   
  Matrix Interpretation Processor:
   dimension: 1
   interpretation:
    [0] = 8,
    
    [g](x0) = x0 + 1,
    
    [f](x0) = x0,
    
    [1] = 2
   orientation:
    f(1()) = 2 >= 3 = f(g(1()))
    
    f(f(x)) = x >= x = f(x)
    
    g(0()) = 9 >= 9 = g(f(0()))
    
    g(g(x)) = x + 2 >= x + 1 = g(x)
   problem:
    strict:
     f(1()) -> f(g(1()))
     f(f(x)) -> f(x)
     g(0()) -> g(f(0()))
    weak:
     g(g(x)) -> g(x)
   Matrix Interpretation Processor:
    dimension: 1
    interpretation:
     [0] = 17,
     
     [g](x0) = x0,
     
     [f](x0) = x0 + 5,
     
     [1] = 0
    orientation:
     f(1()) = 5 >= 5 = f(g(1()))
     
     f(f(x)) = x + 10 >= x + 5 = f(x)
     
     g(0()) = 17 >= 22 = g(f(0()))
     
     g(g(x)) = x >= x = g(x)
    problem:
     strict:
      f(1()) -> f(g(1()))
      g(0()) -> g(f(0()))
     weak:
      f(f(x)) -> f(x)
      g(g(x)) -> g(x)
    Bounds Processor:
     bound: 1
     enrichment: match-rt
     automaton:
      final states: {5}
      transitions:
       f1(15) -> 16*
       f1(19) -> 20*
       g1(16) -> 17*
       g1(18) -> 19*
       11() -> 18*
       01() -> 15*
       f0(5) -> 5*
       10() -> 5*
       g0(5) -> 5*
       00() -> 5*
       17 -> 5*
       20 -> 5*
     problem:
      strict:
       f(1()) -> f(g(1()))
      weak:
       g(0()) -> g(f(0()))
       f(f(x)) -> f(x)
       g(g(x)) -> g(x)
     Bounds Processor:
      bound: 1
      enrichment: match-rt
      automaton:
       final states: {5}
       transitions:
        f1(10) -> 11*
        f1(12) -> 13*
        g1(9) -> 10*
        g1(13) -> 14*
        11() -> 9*
        01() -> 12*
        f0(5) -> 5*
        10() -> 5*
        g0(5) -> 5*
        00() -> 5*
        11 -> 5*
        14 -> 5*
      problem:
       strict:
        
       weak:
        f(1()) -> f(g(1()))
        g(0()) -> g(f(0()))
        f(f(x)) -> f(x)
        g(g(x)) -> g(x)
      Qed