YES Problem: h(f(x,y)) -> f(f(a(),h(h(y))),x) Proof: DP Processor: DPs: h#(f(x,y)) -> h#(y) h#(f(x,y)) -> h#(h(y)) TRS: h(f(x,y)) -> f(f(a(),h(h(y))),x) Matrix Interpretation Processor: dim=2 usable rules: h(f(x,y)) -> f(f(a(),h(h(y))),x) interpretation: [h#](x0) = [2 0]x0, [0] [a] = [0], [0 1] [h](x0) = [3 0]x0, [0 0] [1 1] [1] [f](x0, x1) = [1 1]x0 + [0 0]x1 + [1] orientation: h#(f(x,y)) = [2 2]y + [2] >= [2 0]y = h#(y) h#(f(x,y)) = [2 2]y + [2] >= [0 2]y = h#(h(y)) [1 1] [0 0] [1] [1 1] [0 0] [1] h(f(x,y)) = [0 0]x + [3 3]y + [3] >= [0 0]x + [3 3]y + [3] = f(f(a(),h(h(y))),x) problem: DPs: TRS: h(f(x,y)) -> f(f(a(),h(h(y))),x) Qed