YES Problem: p(f(f(x))) -> q(f(g(x))) p(g(g(x))) -> q(g(f(x))) q(f(f(x))) -> p(f(g(x))) q(g(g(x))) -> p(g(f(x))) Proof: DP Processor: DPs: p#(f(f(x))) -> q#(f(g(x))) p#(g(g(x))) -> q#(g(f(x))) q#(f(f(x))) -> p#(f(g(x))) q#(g(g(x))) -> p#(g(f(x))) TRS: p(f(f(x))) -> q(f(g(x))) p(g(g(x))) -> q(g(f(x))) q(f(f(x))) -> p(f(g(x))) q(g(g(x))) -> p(g(f(x))) Arctic Interpretation Processor: dimension: 2 interpretation: [q#](x0) = [-& 0 ]x0 + [0], [p#](x0) = [-& 0 ]x0 + [0], [-& 0 ] [0] [q](x0) = [-& 0 ]x0 + [0], [0 2 ] [3] [g](x0) = [0 -&]x0 + [2], [-& 0 ] [0] [p](x0) = [-& 0 ]x0 + [0], [-& 0 ] [0] [f](x0) = [1 2 ]x0 + [3] orientation: p#(f(f(x))) = [3 4]x + [5] >= [2 3]x + [4] = q#(f(g(x))) p#(g(g(x))) = [0 2]x + [3] >= [-& 0 ]x + [2] = q#(g(f(x))) q#(f(f(x))) = [3 4]x + [5] >= [2 3]x + [4] = p#(f(g(x))) q#(g(g(x))) = [0 2]x + [3] >= [-& 0 ]x + [2] = p#(g(f(x))) [3 4] [5] [2 3] [4] p(f(f(x))) = [3 4]x + [5] >= [2 3]x + [4] = q(f(g(x))) [0 2] [3] [-& 0 ] [2] p(g(g(x))) = [0 2]x + [3] >= [-& 0 ]x + [2] = q(g(f(x))) [3 4] [5] [2 3] [4] q(f(f(x))) = [3 4]x + [5] >= [2 3]x + [4] = p(f(g(x))) [0 2] [3] [-& 0 ] [2] q(g(g(x))) = [0 2]x + [3] >= [-& 0 ]x + [2] = p(g(f(x))) problem: DPs: TRS: p(f(f(x))) -> q(f(g(x))) p(g(g(x))) -> q(g(f(x))) q(f(f(x))) -> p(f(g(x))) q(g(g(x))) -> p(g(f(x))) Qed