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