YES Problem: f(f(a())) -> c(n__f(n__g(n__f(n__a())))) f(X) -> n__f(X) g(X) -> n__g(X) a() -> n__a() activate(n__f(X)) -> f(activate(X)) activate(n__g(X)) -> g(activate(X)) activate(n__a()) -> a() activate(X) -> X Proof: DP Processor: DPs: activate#(n__f(X)) -> activate#(X) activate#(n__f(X)) -> f#(activate(X)) activate#(n__g(X)) -> activate#(X) activate#(n__g(X)) -> g#(activate(X)) activate#(n__a()) -> a#() TRS: f(f(a())) -> c(n__f(n__g(n__f(n__a())))) f(X) -> n__f(X) g(X) -> n__g(X) a() -> n__a() activate(n__f(X)) -> f(activate(X)) activate(n__g(X)) -> g(activate(X)) activate(n__a()) -> a() activate(X) -> X Arctic Interpretation Processor: dimension: 1 usable rules: interpretation: [activate#](x0) = 2x0, [a#] = 0, [g#](x0) = 0, [f#](x0) = 0, [activate](x0) = 0, [g](x0) = 1x0 + 2, [c](x0) = x0 + 1, [n__g](x0) = 4x0 + 1, [n__f](x0) = 1x0 + 2, [n__a] = 0, [f](x0) = x0 + 1, [a] = 1 orientation: activate#(n__f(X)) = 3X + 4 >= 2X = activate#(X) activate#(n__f(X)) = 3X + 4 >= 0 = f#(activate(X)) activate#(n__g(X)) = 6X + 3 >= 2X = activate#(X) activate#(n__g(X)) = 6X + 3 >= 0 = g#(activate(X)) activate#(n__a()) = 2 >= 0 = a#() f(f(a())) = 1 >= 7 = c(n__f(n__g(n__f(n__a())))) f(X) = X + 1 >= 1X + 2 = n__f(X) g(X) = 1X + 2 >= 4X + 1 = n__g(X) a() = 1 >= 0 = n__a() activate(n__f(X)) = 0 >= 1 = f(activate(X)) activate(n__g(X)) = 0 >= 2 = g(activate(X)) activate(n__a()) = 0 >= 1 = a() activate(X) = 0 >= X = X problem: DPs: TRS: f(f(a())) -> c(n__f(n__g(n__f(n__a())))) f(X) -> n__f(X) g(X) -> n__g(X) a() -> n__a() activate(n__f(X)) -> f(activate(X)) activate(n__g(X)) -> g(activate(X)) activate(n__a()) -> a() activate(X) -> X Qed