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