YES Problem: f(f(x)) -> g(f(x)) g(g(x)) -> f(x) Proof: DP Processor: DPs: f#(f(x)) -> g#(f(x)) g#(g(x)) -> f#(x) TRS: f(f(x)) -> g(f(x)) g(g(x)) -> f(x) Arctic Interpretation Processor: dimension: 1 usable rules: f(f(x)) -> g(f(x)) g(g(x)) -> f(x) interpretation: [g#](x0) = -11x0 + 0, [f#](x0) = x0 + -10, [g](x0) = 12x0 + 11, [f](x0) = 13x0 + 10 orientation: f#(f(x)) = 13x + 10 >= 2x + 0 = g#(f(x)) g#(g(x)) = 1x + 0 >= x + -10 = f#(x) f(f(x)) = 26x + 23 >= 25x + 22 = g(f(x)) g(g(x)) = 24x + 23 >= 13x + 10 = f(x) problem: DPs: TRS: f(f(x)) -> g(f(x)) g(g(x)) -> f(x) Qed