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)) Subterm Criterion Processor: simple projection: pi(g#) = 0 pi(h#) = 0 problem: DPs: h#(x,y) -> g#(x,f(y)) TRS: g(f(x),y) -> f(h(x,y)) h(x,y) -> g(x,f(y)) SCC Processor: #sccs: 0 #rules: 0 #arcs: 2/1