YES(?,O(n^1))

Problem:
 g(c(x1)) -> g(f(c(x1)))
 g(f(c(x1))) -> g(f(f(c(x1))))
 g(g(x1)) -> g(f(g(x1)))
 f(f(g(x1))) -> g(f(x1))

Proof:
 Bounds Processor:
  bound: 2
  enrichment: match
  automaton:
   final states: {3,2}
   transitions:
    g1(6) -> 7*
    f1(5) -> 6*
    c1(4) -> 5*
    g2(20) -> 21*
    g0(1) -> 2*
    f2(19) -> 20*
    f2(18) -> 19*
    c0(1) -> 1*
    c2(17) -> 18*
    f0(1) -> 3*
    1 -> 4*
    4 -> 17*
    7 -> 2*
    21 -> 7,2
  problem:
   
  Qed