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