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 TDG 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 graph: h#(X) -> c#(n__d(X)) -> c#(X) -> d#(activate(X)) h#(X) -> c#(n__d(X)) -> c#(X) -> activate#(X) activate#(n__f(X)) -> activate#(X) -> activate#(n__d(X)) -> d#(X) activate#(n__f(X)) -> activate#(X) -> activate#(n__g(X)) -> g#(X) activate#(n__f(X)) -> activate#(X) -> activate#(n__f(X)) -> f#(activate(X)) activate#(n__f(X)) -> activate#(X) -> activate#(n__f(X)) -> activate#(X) activate#(n__f(X)) -> f#(activate(X)) -> f#(f(X)) -> c#(n__f(n__g(n__f(X)))) c#(X) -> activate#(X) -> activate#(n__d(X)) -> d#(X) c#(X) -> activate#(X) -> activate#(n__g(X)) -> g#(X) c#(X) -> activate#(X) -> activate#(n__f(X)) -> f#(activate(X)) c#(X) -> activate#(X) -> activate#(n__f(X)) -> activate#(X) f#(f(X)) -> c#(n__f(n__g(n__f(X)))) -> c#(X) -> d#(activate(X)) f#(f(X)) -> c#(n__f(n__g(n__f(X)))) -> c#(X) -> activate#(X) CDG 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 graph: h#(X) -> c#(n__d(X)) -> c#(X) -> activate#(X) h#(X) -> c#(n__d(X)) -> c#(X) -> d#(activate(X)) activate#(n__f(X)) -> activate#(X) -> activate#(n__f(X)) -> activate#(X) activate#(n__f(X)) -> activate#(X) -> activate#(n__f(X)) -> f#(activate(X)) activate#(n__f(X)) -> activate#(X) -> activate#(n__g(X)) -> g#(X) activate#(n__f(X)) -> f#(activate(X)) -> f#(f(X)) -> c#(n__f(n__g(n__f(X)))) c#(X) -> activate#(X) -> activate#(n__f(X)) -> activate#(X) c#(X) -> activate#(X) -> activate#(n__f(X)) -> f#(activate(X)) c#(X) -> activate#(X) -> activate#(n__g(X)) -> g#(X) f#(f(X)) -> c#(n__f(n__g(n__f(X)))) -> c#(X) -> activate#(X) f#(f(X)) -> c#(n__f(n__g(n__f(X)))) -> c#(X) -> d#(activate(X)) SCC Processor: #sccs: 1 #rules: 4 #arcs: 11/64 DPs: c#(X) -> activate#(X) activate#(n__f(X)) -> f#(activate(X)) f#(f(X)) -> c#(n__f(n__g(n__f(X)))) activate#(n__f(X)) -> activate#(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 Arctic Interpretation Processor: dimension: 1 interpretation: [activate#](x0) = x0, [c#](x0) = x0, [f#](x0) = 4x0, [g](x0) = x0, [n__d](x0) = x0, [h](x0) = 3x0 + 2, [d](x0) = x0, [activate](x0) = x0, [c](x0) = x0, [n__g](x0) = x0, [n__f](x0) = 4x0, [f](x0) = 4x0 orientation: c#(X) = X >= X = activate#(X) activate#(n__f(X)) = 4X >= 4X = f#(activate(X)) f#(f(X)) = 8X >= 8X = c#(n__f(n__g(n__f(X)))) activate#(n__f(X)) = 4X >= X = activate#(X) f(f(X)) = 8X >= 8X = c(n__f(n__g(n__f(X)))) c(X) = X >= X = d(activate(X)) h(X) = 3X + 2 >= X = c(n__d(X)) f(X) = 4X >= 4X = n__f(X) g(X) = X >= X = n__g(X) d(X) = X >= X = n__d(X) activate(n__f(X)) = 4X >= 4X = f(activate(X)) activate(n__g(X)) = X >= X = g(X) activate(n__d(X)) = X >= X = d(X) activate(X) = X >= X = X problem: DPs: c#(X) -> activate#(X) activate#(n__f(X)) -> f#(activate(X)) f#(f(X)) -> c#(n__f(n__g(n__f(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 EDG Processor: DPs: c#(X) -> activate#(X) activate#(n__f(X)) -> f#(activate(X)) f#(f(X)) -> c#(n__f(n__g(n__f(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 graph: activate#(n__f(X)) -> f#(activate(X)) -> f#(f(X)) -> c#(n__f(n__g(n__f(X)))) c#(X) -> activate#(X) -> activate#(n__f(X)) -> f#(activate(X)) f#(f(X)) -> c#(n__f(n__g(n__f(X)))) -> c#(X) -> activate#(X) Arctic Interpretation Processor: dimension: 1 interpretation: [activate#](x0) = 6x0 + 0, [c#](x0) = 6x0 + 0, [f#](x0) = 8x0 + 0, [g](x0) = 1, [n__d](x0) = x0, [h](x0) = 10x0 + 0, [d](x0) = x0 + 0, [activate](x0) = x0 + 0, [c](x0) = 1x0 + 0, [n__g](x0) = 1, [n__f](x0) = 2x0 + 2, [f](x0) = 2x0 + 2 orientation: c#(X) = 6X + 0 >= 6X + 0 = activate#(X) activate#(n__f(X)) = 8X + 8 >= 8X + 8 = f#(activate(X)) f#(f(X)) = 10X + 10 >= 9 = c#(n__f(n__g(n__f(X)))) f(f(X)) = 4X + 4 >= 4 = c(n__f(n__g(n__f(X)))) c(X) = 1X + 0 >= X + 0 = d(activate(X)) h(X) = 10X + 0 >= 1X + 0 = c(n__d(X)) f(X) = 2X + 2 >= 2X + 2 = n__f(X) g(X) = 1 >= 1 = n__g(X) d(X) = X + 0 >= X = n__d(X) activate(n__f(X)) = 2X + 2 >= 2X + 2 = f(activate(X)) activate(n__g(X)) = 1 >= 1 = g(X) activate(n__d(X)) = X + 0 >= X + 0 = d(X) activate(X) = X + 0 >= X = X problem: DPs: c#(X) -> activate#(X) activate#(n__f(X)) -> f#(activate(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 EDG Processor: DPs: c#(X) -> activate#(X) activate#(n__f(X)) -> f#(activate(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 graph: c#(X) -> activate#(X) -> activate#(n__f(X)) -> f#(activate(X)) CDG Processor: DPs: c#(X) -> activate#(X) activate#(n__f(X)) -> f#(activate(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 graph: Qed