YES Problem: g(f(x),y) -> f(h(x,y)) h(x,y) -> g(x,f(y)) Proof: DP Processor: DPs: g#(f(x),y) -> h#(x,y) h#(x,y) -> g#(x,f(y)) TRS: g(f(x),y) -> f(h(x,y)) h(x,y) -> g(x,f(y)) TDG Processor: DPs: g#(f(x),y) -> h#(x,y) h#(x,y) -> g#(x,f(y)) TRS: g(f(x),y) -> f(h(x,y)) h(x,y) -> g(x,f(y)) graph: h#(x,y) -> g#(x,f(y)) -> g#(f(x),y) -> h#(x,y) g#(f(x),y) -> h#(x,y) -> h#(x,y) -> g#(x,f(y)) CDG Processor: DPs: g#(f(x),y) -> h#(x,y) h#(x,y) -> g#(x,f(y)) TRS: g(f(x),y) -> f(h(x,y)) h(x,y) -> g(x,f(y)) graph: g#(f(x),y) -> h#(x,y) -> h#(x,y) -> g#(x,f(y)) SCC Processor: #sccs: 0 #rules: 0 #arcs: 1/4