*** 1 Progress [(O(1),O(n^1))] *** Considered Problem: Strict DP Rules: Strict TRS Rules: activate(X) -> X activate(n__f(X1,X2)) -> f(activate(X1),X2) activate(n__g(X)) -> g(activate(X)) f(X1,X2) -> n__f(X1,X2) f(g(X),Y) -> f(X,n__f(n__g(X),activate(Y))) g(X) -> n__g(X) Weak DP Rules: Weak TRS Rules: Signature: {activate/1,f/2,g/1} / {n__f/2,n__g/1} Obligation: Innermost basic terms: {activate,f,g}/{n__f,n__g} Applied Processor: InnermostRuleRemoval Proof: Arguments of following rules are not normal-forms. f(g(X),Y) -> f(X,n__f(n__g(X),activate(Y))) All above mentioned rules can be savely removed. *** 1.1 Progress [(O(1),O(n^1))] *** Considered Problem: Strict DP Rules: Strict TRS Rules: activate(X) -> X activate(n__f(X1,X2)) -> f(activate(X1),X2) activate(n__g(X)) -> g(activate(X)) f(X1,X2) -> n__f(X1,X2) g(X) -> n__g(X) Weak DP Rules: Weak TRS Rules: Signature: {activate/1,f/2,g/1} / {n__f/2,n__g/1} Obligation: Innermost basic terms: {activate,f,g}/{n__f,n__g} Applied Processor: Bounds {initialAutomaton = minimal, enrichment = match} Proof: The problem is match-bounded by 2. The enriched problem is compatible with follwoing automaton. activate_0(2) -> 1 activate_1(2) -> 3 f_0(2,2) -> 1 f_1(3,2) -> 1 f_1(3,2) -> 3 g_0(2) -> 1 g_1(3) -> 1 g_1(3) -> 3 n__f_0(2,2) -> 1 n__f_0(2,2) -> 2 n__f_0(2,2) -> 3 n__f_1(2,2) -> 1 n__f_2(3,2) -> 1 n__f_2(3,2) -> 3 n__g_0(2) -> 1 n__g_0(2) -> 2 n__g_0(2) -> 3 n__g_1(2) -> 1 n__g_2(3) -> 1 n__g_2(3) -> 3 2 -> 1 2 -> 3 *** 1.1.1 Progress [(O(1),O(1))] *** Considered Problem: Strict DP Rules: Strict TRS Rules: Weak DP Rules: Weak TRS Rules: activate(X) -> X activate(n__f(X1,X2)) -> f(activate(X1),X2) activate(n__g(X)) -> g(activate(X)) f(X1,X2) -> n__f(X1,X2) g(X) -> n__g(X) Signature: {activate/1,f/2,g/1} / {n__f/2,n__g/1} Obligation: Innermost basic terms: {activate,f,g}/{n__f,n__g} Applied Processor: EmptyProcessor Proof: The problem is already closed. The intended complexity is O(1).