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 Usable Rule 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: activate(n__f(X)) -> f(X) activate(n__d(X)) -> d(X) activate(X) -> X f(f(X)) -> c(n__f(g(n__f(X)))) f(X) -> n__f(X) c(X) -> d(activate(X)) d(X) -> n__d(X) Arctic Interpretation Processor: dimension: 1 usable rules: activate(n__f(X)) -> f(X) activate(n__d(X)) -> d(X) activate(X) -> X f(f(X)) -> c(n__f(g(n__f(X)))) f(X) -> n__f(X) c(X) -> d(activate(X)) d(X) -> n__d(X) interpretation: [h#](x0) = 1x0 + 12, [d#](x0) = -13x0 + 0, [activate#](x0) = 2x0 + -16, [c#](x0) = 3x0 + 1, [f#](x0) = x0, [n__d](x0) = -11x0 + 8, [d](x0) = -7x0 + 9, [activate](x0) = 13x0 + 3, [c](x0) = 8x0 + 10, [g](x0) = x0 + -16, [n__f](x0) = x0, [f](x0) = 10x0 + 2 orientation: f#(f(X)) = 10X + 2 >= 3X + 1 = c#(n__f(g(n__f(X)))) c#(X) = 3X + 1 >= 2X + -16 = activate#(X) c#(X) = 3X + 1 >= X + 0 = d#(activate(X)) h#(X) = 1X + 12 >= -8X + 11 = c#(n__d(X)) activate#(n__f(X)) = 2X + -16 >= X = f#(X) activate#(n__d(X)) = -9X + 10 >= -13X + 0 = d#(X) activate(n__f(X)) = 13X + 3 >= 10X + 2 = f(X) activate(n__d(X)) = 2X + 21 >= -7X + 9 = d(X) activate(X) = 13X + 3 >= X = X f(f(X)) = 20X + 12 >= 8X + 10 = c(n__f(g(n__f(X)))) f(X) = 10X + 2 >= X = n__f(X) c(X) = 8X + 10 >= 6X + 9 = d(activate(X)) d(X) = -7X + 9 >= -11X + 8 = n__d(X) problem: DPs: TRS: activate(n__f(X)) -> f(X) activate(n__d(X)) -> d(X) activate(X) -> X f(f(X)) -> c(n__f(g(n__f(X)))) f(X) -> n__f(X) c(X) -> d(activate(X)) d(X) -> n__d(X) Qed