YES(?,O(n^1)) Problem: p(f(f(x))) -> q(f(g(x))) p(g(g(x))) -> q(g(f(x))) q(f(f(x))) -> p(f(g(x))) q(g(g(x))) -> p(g(f(x))) Proof: Bounds Processor: bound: 1 enrichment: match automaton: final states: {4,3} transitions: p1(27) -> 28* g1(15) -> 16* g1(5) -> 6* g1(18) -> 19* f1(25) -> 26* f1(17) -> 18* f1(6) -> 7* q1(7) -> 8* p0(2) -> 3* p0(1) -> 3* f0(2) -> 1* f0(1) -> 1* q0(2) -> 4* q0(1) -> 4* g0(2) -> 2* g0(1) -> 2* 1 -> 25,15 2 -> 17,5 7 -> 27* 8 -> 3* 16 -> 6* 19 -> 7* 26 -> 18* 28 -> 4* problem: Qed