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)) TDG 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)) graph: g#(h(x),y) -> g#(x,y) -> g#(h(x),y) -> g#(x,y) g#(h(x),y) -> g#(x,y) -> g#(h(x),y) -> f#(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) -> g#(x,y) f#(x,y) -> g#(x,y) -> g#(h(x),y) -> f#(x,y) CDG 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)) graph: g#(h(x),y) -> f#(x,y) -> f#(x,y) -> g#(x,y) SCC Processor: #sccs: 0 #rules: 0 #arcs: 1/9