YES Problem: g(h(g(x))) -> g(x) g(g(x)) -> g(h(g(x))) h(h(x)) -> h(f(h(x),x)) Proof: DP Processor: DPs: g#(g(x)) -> h#(g(x)) g#(g(x)) -> g#(h(g(x))) h#(h(x)) -> h#(f(h(x),x)) TRS: g(h(g(x))) -> g(x) g(g(x)) -> g(h(g(x))) h(h(x)) -> h(f(h(x),x)) Matrix Interpretation Processor: dim=1 interpretation: [h#](x0) = 4x0, [g#](x0) = 4x0 + 6, [f](x0, x1) = 2, [h](x0) = 4, [g](x0) = 6 orientation: g#(g(x)) = 30 >= 24 = h#(g(x)) g#(g(x)) = 30 >= 22 = g#(h(g(x))) h#(h(x)) = 16 >= 8 = h#(f(h(x),x)) g(h(g(x))) = 6 >= 6 = g(x) g(g(x)) = 6 >= 6 = g(h(g(x))) h(h(x)) = 4 >= 4 = h(f(h(x),x)) problem: DPs: TRS: g(h(g(x))) -> g(x) g(g(x)) -> g(h(g(x))) h(h(x)) -> h(f(h(x),x)) Qed