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(h(0()))) -> g(d(1())) g(c(1())) -> g(d(h(0()))) g(h(x)) -> g(x) Proof: DP Processor: DPs: f#(f(x)) -> f#(c(f(x))) f#(f(x)) -> f#(d(f(x))) g#(c(h(0()))) -> g#(d(1())) g#(c(1())) -> g#(d(h(0()))) g#(h(x)) -> g#(x) 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(h(0()))) -> g(d(1())) g(c(1())) -> g(d(h(0()))) g(h(x)) -> g(x) Arctic Interpretation Processor: dimension: 1 interpretation: [g#](x0) = x0 + -16, [f#](x0) = 4x0 + 0, [1] = 4, [h](x0) = 2x0 + 1, [0] = 2, [g](x0) = 5x0 + 0, [d](x0) = -4x0 + 0, [c](x0) = -3x0 + 0, [f](x0) = 1x0 + 2 orientation: f#(f(x)) = 5x + 6 >= 2x + 4 = f#(c(f(x))) f#(f(x)) = 5x + 6 >= 1x + 4 = f#(d(f(x))) g#(c(h(0()))) = 1 >= 0 = g#(d(1())) g#(c(1())) = 1 >= 0 = g#(d(h(0()))) g#(h(x)) = 2x + 1 >= x + -16 = g#(x) f(f(x)) = 2x + 3 >= -1x + 2 = f(c(f(x))) f(f(x)) = 2x + 3 >= -2x + 2 = f(d(f(x))) g(c(x)) = 2x + 5 >= x = x g(d(x)) = 1x + 5 >= x = x g(c(h(0()))) = 6 >= 5 = g(d(1())) g(c(1())) = 6 >= 5 = g(d(h(0()))) g(h(x)) = 7x + 6 >= 5x + 0 = g(x) 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(h(0()))) -> g(d(1())) g(c(1())) -> g(d(h(0()))) g(h(x)) -> g(x) Qed