YES Problem: f(f(a())) -> f(g(n__f(n__a()))) f(X) -> n__f(X) a() -> n__a() activate(n__f(X)) -> f(activate(X)) activate(n__a()) -> a() activate(X) -> X Proof: DP Processor: DPs: f#(f(a())) -> f#(g(n__f(n__a()))) activate#(n__f(X)) -> activate#(X) activate#(n__f(X)) -> f#(activate(X)) activate#(n__a()) -> a#() TRS: f(f(a())) -> f(g(n__f(n__a()))) f(X) -> n__f(X) a() -> n__a() activate(n__f(X)) -> f(activate(X)) activate(n__a()) -> a() activate(X) -> X Matrix Interpretation Processor: dim=1 usable rules: f(f(a())) -> f(g(n__f(n__a()))) f(X) -> n__f(X) a() -> n__a() activate(n__f(X)) -> f(activate(X)) activate(n__a()) -> a() activate(X) -> X interpretation: [activate#](x0) = 4x0 + 5, [a#] = 0, [f#](x0) = 4x0 + 2, [activate](x0) = 2x0 + 4, [g](x0) = 0, [n__f](x0) = 2x0 + 4, [n__a] = 1, [f](x0) = 2x0 + 4, [a] = 1 orientation: f#(f(a())) = 26 >= 2 = f#(g(n__f(n__a()))) activate#(n__f(X)) = 8X + 21 >= 4X + 5 = activate#(X) activate#(n__f(X)) = 8X + 21 >= 8X + 18 = f#(activate(X)) activate#(n__a()) = 9 >= 0 = a#() f(f(a())) = 16 >= 4 = f(g(n__f(n__a()))) f(X) = 2X + 4 >= 2X + 4 = n__f(X) a() = 1 >= 1 = n__a() activate(n__f(X)) = 4X + 12 >= 4X + 12 = f(activate(X)) activate(n__a()) = 6 >= 1 = a() activate(X) = 2X + 4 >= X = X problem: DPs: TRS: f(f(a())) -> f(g(n__f(n__a()))) f(X) -> n__f(X) a() -> n__a() activate(n__f(X)) -> f(activate(X)) activate(n__a()) -> a() activate(X) -> X Qed