*** 1 Progress [(O(1),O(n^1))] *** Considered Problem: Strict DP Rules: Strict TRS Rules: f(g(x)) -> g(g(f(x))) f(g(x)) -> g(g(g(x))) Weak DP Rules: Weak TRS Rules: Signature: {f/1} / {g/1} Obligation: Innermost basic terms: {f}/{g} Applied Processor: Bounds {initialAutomaton = minimal, enrichment = match} Proof: The problem is match-bounded by 1. The enriched problem is compatible with follwoing automaton. f_0(2) -> 1 f_1(2) -> 4 g_0(2) -> 2 g_1(2) -> 4 g_1(3) -> 1 g_1(3) -> 4 g_1(4) -> 3 *** 1.1 Progress [(O(1),O(1))] *** Considered Problem: Strict DP Rules: Strict TRS Rules: Weak DP Rules: Weak TRS Rules: f(g(x)) -> g(g(f(x))) f(g(x)) -> g(g(g(x))) Signature: {f/1} / {g/1} Obligation: Innermost basic terms: {f}/{g} Applied Processor: EmptyProcessor Proof: The problem is already closed. The intended complexity is O(1).