YES(?,O(n^1)) Problem: f(f(x)) -> f(c(f(x))) f(f(x)) -> f(d(f(x))) g(c(x)) -> x g(d(x)) -> x g(c(h(0()))) -> g(d(1())) g(c(1())) -> g(d(h(0()))) g(h(x)) -> g(x) Proof: Bounds Processor: bound: 1 enrichment: match automaton: final states: {7,6} transitions: g1(32) -> 33* g1(34) -> 35* g1(24) -> 25* g1(9) -> 10* g1(26) -> 27* g1(18) -> 19* d1(8) -> 9* h1(16) -> 17* 01() -> 16* 11() -> 8* f0(5) -> 6* f0(2) -> 6* f0(4) -> 6* f0(1) -> 6* f0(3) -> 6* c0(5) -> 1* c0(2) -> 1* c0(4) -> 1* c0(1) -> 1* c0(3) -> 1* d0(5) -> 2* d0(2) -> 2* d0(4) -> 2* d0(1) -> 2* d0(3) -> 2* g0(5) -> 7* g0(2) -> 7* g0(4) -> 7* g0(1) -> 7* g0(3) -> 7* h0(5) -> 3* h0(2) -> 3* h0(4) -> 3* h0(1) -> 3* h0(3) -> 3* 00() -> 4* 10() -> 5* 1 -> 25,33,32,7 2 -> 25,33,24,7 3 -> 25,33,34,7 4 -> 25,33,26,7 5 -> 25,33,18,7 8 -> 10* 10 -> 33,7 17 -> 8* 19 -> 35,7 25 -> 35,7 27 -> 35,7 33 -> 35,7 35 -> 7* problem: Qed