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