YES Problem: f(x,g(x)) -> x f(x,h(y)) -> f(h(x),y) Proof: DP Processor: DPs: f#(x,h(y)) -> f#(h(x),y) TRS: f(x,g(x)) -> x f(x,h(y)) -> f(h(x),y) Arctic Interpretation Processor: dimension: 1 interpretation: [f#](x0, x1) = 2x1, [h](x0) = 2x0, [f](x0, x1) = x1, [g](x0) = 2x0 + 6 orientation: f#(x,h(y)) = 4y >= 2y = f#(h(x),y) f(x,g(x)) = 2x + 6 >= x = x f(x,h(y)) = 2y >= y = f(h(x),y) problem: DPs: TRS: f(x,g(x)) -> x f(x,h(y)) -> f(h(x),y) Qed