YES Problem: f(a()) -> b() f(c()) -> d() f(g(x,y)) -> g(f(x),f(y)) f(h(x,y)) -> g(h(y,f(x)),h(x,f(y))) g(x,x) -> h(e(),x) Proof: DP Processor: DPs: f#(g(x,y)) -> f#(y) f#(g(x,y)) -> f#(x) f#(g(x,y)) -> g#(f(x),f(y)) f#(h(x,y)) -> f#(y) f#(h(x,y)) -> f#(x) f#(h(x,y)) -> g#(h(y,f(x)),h(x,f(y))) TRS: f(a()) -> b() f(c()) -> d() f(g(x,y)) -> g(f(x),f(y)) f(h(x,y)) -> g(h(y,f(x)),h(x,f(y))) g(x,x) -> h(e(),x) Arctic Interpretation Processor: dimension: 1 usable rules: interpretation: [g#](x0, x1) = 0, [f#](x0) = x0, [e] = 0, [h](x0, x1) = 6x0 + 1x1 + 1, [g](x0, x1) = 1x0 + 1x1 + 5, [d] = 0, [c] = 4, [b] = 0, [f](x0) = x0 + 5, [a] = 6 orientation: f#(g(x,y)) = 1x + 1y + 5 >= y = f#(y) f#(g(x,y)) = 1x + 1y + 5 >= x = f#(x) f#(g(x,y)) = 1x + 1y + 5 >= 0 = g#(f(x),f(y)) f#(h(x,y)) = 6x + 1y + 1 >= y = f#(y) f#(h(x,y)) = 6x + 1y + 1 >= x = f#(x) f#(h(x,y)) = 6x + 1y + 1 >= 0 = g#(h(y,f(x)),h(x,f(y))) f(a()) = 6 >= 0 = b() f(c()) = 5 >= 0 = d() f(g(x,y)) = 1x + 1y + 5 >= 1x + 1y + 6 = g(f(x),f(y)) f(h(x,y)) = 6x + 1y + 5 >= 7x + 7y + 7 = g(h(y,f(x)),h(x,f(y))) g(x,x) = 1x + 5 >= 1x + 6 = h(e(),x) problem: DPs: TRS: f(a()) -> b() f(c()) -> d() f(g(x,y)) -> g(f(x),f(y)) f(h(x,y)) -> g(h(y,f(x)),h(x,f(y))) g(x,x) -> h(e(),x) Qed