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