YES Problem: f(f(X)) -> c(n__f(n__g(n__f(X)))) c(X) -> d(activate(X)) h(X) -> c(n__d(X)) f(X) -> n__f(X) g(X) -> n__g(X) d(X) -> n__d(X) activate(n__f(X)) -> f(activate(X)) activate(n__g(X)) -> g(X) activate(n__d(X)) -> d(X) activate(X) -> X Proof: DP Processor: DPs: f#(f(X)) -> c#(n__f(n__g(n__f(X)))) c#(X) -> activate#(X) c#(X) -> d#(activate(X)) h#(X) -> c#(n__d(X)) activate#(n__f(X)) -> activate#(X) activate#(n__f(X)) -> f#(activate(X)) activate#(n__g(X)) -> g#(X) activate#(n__d(X)) -> d#(X) TRS: f(f(X)) -> c(n__f(n__g(n__f(X)))) c(X) -> d(activate(X)) h(X) -> c(n__d(X)) f(X) -> n__f(X) g(X) -> n__g(X) d(X) -> n__d(X) activate(n__f(X)) -> f(activate(X)) activate(n__g(X)) -> g(X) activate(n__d(X)) -> d(X) activate(X) -> X Usable Rule Processor: DPs: f#(f(X)) -> c#(n__f(n__g(n__f(X)))) c#(X) -> activate#(X) c#(X) -> d#(activate(X)) h#(X) -> c#(n__d(X)) activate#(n__f(X)) -> activate#(X) activate#(n__f(X)) -> f#(activate(X)) activate#(n__g(X)) -> g#(X) activate#(n__d(X)) -> d#(X) TRS: activate(n__f(X)) -> f(activate(X)) activate(n__g(X)) -> g(X) activate(n__d(X)) -> d(X) activate(X) -> X f(f(X)) -> c(n__f(n__g(n__f(X)))) f(X) -> n__f(X) c(X) -> d(activate(X)) d(X) -> n__d(X) g(X) -> n__g(X) Matrix Interpretation Processor: dim=1 interpretation: [g#](x0) = 0, [h#](x0) = 16x0 + 17, [d#](x0) = 0, [activate#](x0) = 12x0 + 1, [c#](x0) = 16x0 + 16, [f#](x0) = 6x0 + 3, [g](x0) = 0, [n__d](x0) = 0, [d](x0) = 0, [activate](x0) = 8x0, [c](x0) = 16x0, [n__g](x0) = 0, [n__f](x0) = 4x0 + 2, [f](x0) = 4x0 + 9 orientation: f#(f(X)) = 24X + 57 >= 48 = c#(n__f(n__g(n__f(X)))) c#(X) = 16X + 16 >= 12X + 1 = activate#(X) c#(X) = 16X + 16 >= 0 = d#(activate(X)) h#(X) = 16X + 17 >= 16 = c#(n__d(X)) activate#(n__f(X)) = 48X + 25 >= 12X + 1 = activate#(X) activate#(n__f(X)) = 48X + 25 >= 48X + 3 = f#(activate(X)) activate#(n__g(X)) = 1 >= 0 = g#(X) activate#(n__d(X)) = 1 >= 0 = d#(X) activate(n__f(X)) = 32X + 16 >= 32X + 9 = f(activate(X)) activate(n__g(X)) = 0 >= 0 = g(X) activate(n__d(X)) = 0 >= 0 = d(X) activate(X) = 8X >= X = X f(f(X)) = 16X + 45 >= 32 = c(n__f(n__g(n__f(X)))) f(X) = 4X + 9 >= 4X + 2 = n__f(X) c(X) = 16X >= 0 = d(activate(X)) d(X) = 0 >= 0 = n__d(X) g(X) = 0 >= 0 = n__g(X) problem: DPs: TRS: activate(n__f(X)) -> f(activate(X)) activate(n__g(X)) -> g(X) activate(n__d(X)) -> d(X) activate(X) -> X f(f(X)) -> c(n__f(n__g(n__f(X)))) f(X) -> n__f(X) c(X) -> d(activate(X)) d(X) -> n__d(X) g(X) -> n__g(X) Qed