*** 1 Progress [(O(1),O(n^1))] *** Considered Problem: Strict DP Rules: Strict TRS Rules: activate(X) -> X activate(n__f(X)) -> f(activate(X)) activate(n__h(X)) -> h(activate(X)) f(X) -> g(n__h(n__f(X))) f(X) -> n__f(X) h(X) -> n__h(X) Weak DP Rules: Weak TRS Rules: Signature: {activate/1,f/1,h/1} / {g/1,n__f/1,n__h/1} Obligation: Innermost basic terms: {activate,f,h}/{g,n__f,n__h} 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) -> 1 f_1(3) -> 1 f_1(3) -> 3 g_0(2) -> 1 g_0(2) -> 2 g_0(2) -> 3 g_1(4) -> 1 g_2(6) -> 1 g_2(6) -> 3 h_0(2) -> 1 h_1(3) -> 1 h_1(3) -> 3 n__f_0(2) -> 1 n__f_0(2) -> 2 n__f_0(2) -> 3 n__f_1(2) -> 1 n__f_1(2) -> 5 n__f_2(3) -> 1 n__f_2(3) -> 3 n__f_2(3) -> 7 n__h_0(2) -> 1 n__h_0(2) -> 2 n__h_0(2) -> 3 n__h_1(2) -> 1 n__h_1(5) -> 4 n__h_2(3) -> 1 n__h_2(3) -> 3 n__h_2(7) -> 6 2 -> 1 2 -> 3 *** 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(activate(X)) activate(n__h(X)) -> h(activate(X)) f(X) -> g(n__h(n__f(X))) f(X) -> n__f(X) h(X) -> n__h(X) Signature: {activate/1,f/1,h/1} / {g/1,n__f/1,n__h/1} Obligation: Innermost basic terms: {activate,f,h}/{g,n__f,n__h} Applied Processor: EmptyProcessor Proof: The problem is already closed. The intended complexity is O(1).