YES(?,O(n^1)) Problem: f(x,x) -> a() f(g(x),y) -> f(x,y) Proof: Bounds Processor: bound: 2 enrichment: match automaton: final states: {5,4} transitions: f1(4,4) -> 4* f1(5,5) -> 4* f1(4,5) -> 4* f1(5,4) -> 4* a2() -> 4* g0(5) -> 5* g0(4) -> 5* problem: Qed