*** 1 Progress [(O(1),O(n^1))] *** Considered Problem: Strict DP Rules: Strict TRS Rules: activate(X) -> X activate(n__f(X)) -> f(X) f(X) -> n__f(X) f(f(a())) -> c(n__f(g(f(a())))) Weak DP Rules: Weak TRS Rules: Signature: {activate/1,f/1} / {a/0,c/1,g/1,n__f/1} Obligation: Full basic terms: {activate,f}/{a,c,g,n__f} Applied Processor: Bounds {initialAutomaton = minimal, enrichment = match} Proof: The problem is match-bounded by 2. The enriched problem is compatible with follwoing automaton. a_0() -> 1 a_0() -> 2 activate_0(2) -> 1 c_0(2) -> 1 c_0(2) -> 2 f_0(2) -> 1 f_1(2) -> 1 g_0(2) -> 1 g_0(2) -> 2 n__f_0(2) -> 1 n__f_0(2) -> 2 n__f_1(2) -> 1 n__f_2(2) -> 1 2 -> 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(X)) -> f(X) f(X) -> n__f(X) f(f(a())) -> c(n__f(g(f(a())))) Signature: {activate/1,f/1} / {a/0,c/1,g/1,n__f/1} Obligation: Full basic terms: {activate,f}/{a,c,g,n__f} Applied Processor: EmptyProcessor Proof: The problem is already closed. The intended complexity is O(1).