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