YES Problem: f(f(X)) -> c(n__f(g(n__f(X)))) c(X) -> d(activate(X)) h(X) -> c(n__d(X)) f(X) -> n__f(X) d(X) -> n__d(X) activate(n__f(X)) -> f(X) activate(n__d(X)) -> d(X) activate(X) -> X Proof: DP Processor: DPs: f#(f(X)) -> c#(n__f(g(n__f(X)))) c#(X) -> activate#(X) c#(X) -> d#(activate(X)) h#(X) -> c#(n__d(X)) activate#(n__f(X)) -> f#(X) activate#(n__d(X)) -> d#(X) TRS: f(f(X)) -> c(n__f(g(n__f(X)))) c(X) -> d(activate(X)) h(X) -> c(n__d(X)) f(X) -> n__f(X) d(X) -> n__d(X) activate(n__f(X)) -> f(X) activate(n__d(X)) -> d(X) activate(X) -> X Arctic Interpretation Processor: dimension: 1 interpretation: [h#](x0) = 4x0 + 7, [d#](x0) = 0, [activate#](x0) = 1x0 + 1, [c#](x0) = 2x0 + 4, [f#](x0) = 2x0 + 4, [n__d](x0) = x0, [h](x0) = 12x0 + 12, [d](x0) = 1x0, [activate](x0) = 3x0 + 0, [c](x0) = 8x0 + 8, [g](x0) = 1, [n__f](x0) = 5x0 + 12, [f](x0) = 7x0 + 14 orientation: f#(f(X)) = 9X + 16 >= 14 = c#(n__f(g(n__f(X)))) c#(X) = 2X + 4 >= 1X + 1 = activate#(X) c#(X) = 2X + 4 >= 0 = d#(activate(X)) h#(X) = 4X + 7 >= 2X + 4 = c#(n__d(X)) activate#(n__f(X)) = 6X + 13 >= 2X + 4 = f#(X) activate#(n__d(X)) = 1X + 1 >= 0 = d#(X) f(f(X)) = 14X + 21 >= 20 = c(n__f(g(n__f(X)))) c(X) = 8X + 8 >= 4X + 1 = d(activate(X)) h(X) = 12X + 12 >= 8X + 8 = c(n__d(X)) f(X) = 7X + 14 >= 5X + 12 = n__f(X) d(X) = 1X >= X = n__d(X) activate(n__f(X)) = 8X + 15 >= 7X + 14 = f(X) activate(n__d(X)) = 3X + 0 >= 1X = d(X) activate(X) = 3X + 0 >= X = X problem: DPs: TRS: f(f(X)) -> c(n__f(g(n__f(X)))) c(X) -> d(activate(X)) h(X) -> c(n__d(X)) f(X) -> n__f(X) d(X) -> n__d(X) activate(n__f(X)) -> f(X) activate(n__d(X)) -> d(X) activate(X) -> X Qed