YES Problem: f(a(),x) -> f(g(x),x) h(g(x)) -> h(a()) g(h(x)) -> g(x) h(h(x)) -> x Proof: DP Processor: DPs: f#(a(),x) -> g#(x) f#(a(),x) -> f#(g(x),x) h#(g(x)) -> h#(a()) g#(h(x)) -> g#(x) TRS: f(a(),x) -> f(g(x),x) h(g(x)) -> h(a()) g(h(x)) -> g(x) h(h(x)) -> x Matrix Interpretation Processor: dim=2 interpretation: [h#](x0) = [0 1]x0 + [2], [g#](x0) = [1 1]x0, [f#](x0, x1) = [1 0]x0 + [1 2]x1, [0 1] [3] [h](x0) = [1 1]x0 + [0], [0] [g](x0) = [2], [1 0] [3] [f](x0, x1) = [2 1]x0 + [0], [1] [a] = [0] orientation: f#(a(),x) = [1 2]x + [1] >= [1 1]x = g#(x) f#(a(),x) = [1 2]x + [1] >= [1 2]x = f#(g(x),x) h#(g(x)) = [4] >= [2] = h#(a()) g#(h(x)) = [1 2]x + [3] >= [1 1]x = g#(x) [4] [3] f(a(),x) = [2] >= [2] = f(g(x),x) [5] [3] h(g(x)) = [2] >= [1] = h(a()) [0] [0] g(h(x)) = [2] >= [2] = g(x) [1 1] [3] h(h(x)) = [1 2]x + [3] >= x = x problem: DPs: TRS: f(a(),x) -> f(g(x),x) h(g(x)) -> h(a()) g(h(x)) -> g(x) h(h(x)) -> x Qed