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