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: h1(3,3) -> 3* f0(3,3) -> 3* problem: Qed