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)) EDG 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)) Matrix Interpretation Processor: dimension: 1 interpretation: [h#](x0, x1) = 1, [g#](x0, x1) = 0, [h](x0, x1) = 0, [g](x0, x1) = 0, [f](x0) = 0 orientation: h#(x,y) = 1 >= 0 = g#(x,f(y)) g(f(x),y) = 0 >= 0 = f(h(x,y)) h(x,y) = 0 >= 0 = g(x,f(y)) problem: DPs: TRS: g(f(x),y) -> f(h(x,y)) h(x,y) -> g(x,f(y)) Qed