YES Problem: f(x,y) -> h(x,y) f(x,y) -> h(y,x) h(x,x) -> x Proof: Bounds Processor: bound: 1 enrichment: roof automaton: final states: {3} transitions: f0(3,3) -> 3* h0(3,3) -> 3* h1(3,3) -> 3* problem: Qed