YES Problem: f(x,y) -> h(x,y) f(x,y) -> h(y,x) h(x,x) -> x Proof: DP Processor: DPs: f#(x,y) -> h#(x,y) f#(x,y) -> h#(y,x) TRS: f(x,y) -> h(x,y) f(x,y) -> h(y,x) h(x,x) -> x Usable Rule Processor: DPs: f#(x,y) -> h#(x,y) f#(x,y) -> h#(y,x) TRS: Arctic Interpretation Processor: dimension: 1 usable rules: interpretation: [h#](x0, x1) = 8, [f#](x0, x1) = -8x0 + x1 + 9 orientation: f#(x,y) = -8x + y + 9 >= 8 = h#(x,y) f#(x,y) = -8x + y + 9 >= 8 = h#(y,x) problem: DPs: TRS: Qed