YES(?,O(n^1)) 4.08/1.13 YES(?,O(n^1)) 4.08/1.13 4.08/1.13 We are left with following problem, upon which TcT provides the 4.08/1.13 certificate YES(?,O(n^1)). 4.08/1.13 4.08/1.13 Strict Trs: 4.08/1.13 { f(f(X)) -> f(a(b(f(X)))) 4.08/1.13 , f(a(g(X))) -> b(X) 4.08/1.13 , b(X) -> a(X) } 4.08/1.13 Obligation: 4.08/1.13 innermost runtime complexity 4.08/1.13 Answer: 4.08/1.13 YES(?,O(n^1)) 4.08/1.13 4.08/1.13 The problem is match-bounded by 2. The enriched problem is 4.08/1.13 compatible with the following automaton. 4.08/1.13 { f_0(2) -> 1 4.08/1.13 , f_0(4) -> 1 4.08/1.13 , a_0(2) -> 2 4.08/1.13 , a_0(4) -> 2 4.08/1.13 , a_1(2) -> 3 4.08/1.13 , a_1(4) -> 3 4.08/1.13 , a_2(2) -> 1 4.08/1.13 , a_2(4) -> 1 4.08/1.13 , b_0(2) -> 3 4.08/1.13 , b_0(4) -> 3 4.08/1.13 , b_1(2) -> 1 4.08/1.13 , b_1(4) -> 1 4.08/1.13 , g_0(2) -> 4 4.08/1.13 , g_0(4) -> 4 } 4.08/1.13 4.08/1.13 Hurray, we answered YES(?,O(n^1)) 4.08/1.14 EOF