YES Problem: f(x,x) -> a() f(g(x),y) -> f(x,y) Proof: Bounds Processor: bound: 1 enrichment: match automaton: final states: {4,2,1} transitions: f30() -> 3* a0() -> 4*,2,1 f0(3,3) -> 2* a1() -> 1,4*,2 problem: Qed