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