YES Problem: f(g(x),y,y) -> g(f(x,x,y)) Proof: DP Processor: DPs: f#(g(x),y,y) -> f#(x,x,y) TRS: f(g(x),y,y) -> g(f(x,x,y)) Usable Rule Processor: DPs: f#(g(x),y,y) -> f#(x,x,y) TRS: f3(x,y) -> x f3(x,y) -> y Restore Modifier: DPs: f#(g(x),y,y) -> f#(x,x,y) TRS: f(g(x),y,y) -> g(f(x,x,y)) SCC Processor: #sccs: 1 #rules: 1 #arcs: 1/1 DPs: f#(g(x),y,y) -> f#(x,x,y) TRS: f(g(x),y,y) -> g(f(x,x,y)) Matrix Interpretation Processor: dimension: 1 interpretation: [f#](x0, x1, x2) = x0 + 1, [f](x0, x1, x2) = x0 + 1, [g](x0) = x0 + 1 orientation: f#(g(x),y,y) = x + 2 >= x + 1 = f#(x,x,y) f(g(x),y,y) = x + 2 >= x + 2 = g(f(x,x,y)) problem: DPs: TRS: f(g(x),y,y) -> g(f(x,x,y)) Qed