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