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 Matrix Interpretation Processor: dim=1 interpretation: [g#](x0) = 0, [h#](x0) = 18, [d#](x0) = 11, [activate#](x0) = 6x0 + 16, [c#](x0) = 6x0 + 17, [f#](x0) = x0 + 20, [g](x0) = 0, [n__d](x0) = 0, [h](x0) = 0, [d](x0) = 0, [activate](x0) = 4x0, [c](x0) = 0, [n__g](x0) = 0, [n__f](x0) = 4x0 + 1, [f](x0) = 4x0 + 4 orientation: f#(f(X)) = 4X + 24 >= 23 = c#(n__f(n__g(n__f(X)))) c#(X) = 6X + 17 >= 6X + 16 = activate#(X) c#(X) = 6X + 17 >= 11 = d#(activate(X)) h#(X) = 18 >= 17 = c#(n__d(X)) activate#(n__f(X)) = 24X + 22 >= 6X + 16 = activate#(X) activate#(n__f(X)) = 24X + 22 >= 4X + 20 = f#(activate(X)) activate#(n__g(X)) = 16 >= 0 = g#(X) activate#(n__d(X)) = 16 >= 11 = d#(X) f(f(X)) = 16X + 20 >= 0 = c(n__f(n__g(n__f(X)))) c(X) = 0 >= 0 = d(activate(X)) h(X) = 0 >= 0 = c(n__d(X)) f(X) = 4X + 4 >= 4X + 1 = n__f(X) g(X) = 0 >= 0 = n__g(X) d(X) = 0 >= 0 = n__d(X) activate(n__f(X)) = 16X + 4 >= 16X + 4 = f(activate(X)) activate(n__g(X)) = 0 >= 0 = g(X) activate(n__d(X)) = 0 >= 0 = d(X) activate(X) = 4X >= X = X problem: DPs: 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 Qed