YES(?,O(n^1)) 3.98/1.27 YES(?,O(n^1)) 3.98/1.27 3.98/1.27 We are left with following problem, upon which TcT provides the 3.98/1.27 certificate YES(?,O(n^1)). 3.98/1.27 3.98/1.27 Strict Trs: 3.98/1.27 { f(a()) -> g(h(a())) 3.98/1.27 , h(g(x)) -> g(h(f(x))) 3.98/1.27 , k(x, h(x), a()) -> h(x) 3.98/1.27 , k(f(x), y, x) -> f(x) } 3.98/1.27 Obligation: 3.98/1.27 runtime complexity 3.98/1.27 Answer: 3.98/1.27 YES(?,O(n^1)) 3.98/1.27 3.98/1.27 The problem is match-bounded by 2. The enriched problem is 3.98/1.27 compatible with the following automaton. 3.98/1.27 { f_0(2) -> 1 3.98/1.27 , f_0(3) -> 1 3.98/1.27 , f_1(2) -> 9 3.98/1.27 , f_1(3) -> 9 3.98/1.27 , f_2(6) -> 11 3.98/1.27 , a_0() -> 2 3.98/1.27 , a_1() -> 7 3.98/1.27 , g_0(2) -> 3 3.98/1.27 , g_0(3) -> 3 3.98/1.27 , g_1(6) -> 1 3.98/1.27 , g_1(6) -> 9 3.98/1.27 , g_1(8) -> 4 3.98/1.27 , g_2(10) -> 8 3.98/1.27 , h_0(2) -> 4 3.98/1.27 , h_0(3) -> 4 3.98/1.27 , h_1(7) -> 6 3.98/1.27 , h_1(9) -> 8 3.98/1.27 , h_2(11) -> 10 3.98/1.27 , k_0(2, 2, 2) -> 5 3.98/1.27 , k_0(2, 2, 3) -> 5 3.98/1.27 , k_0(2, 3, 2) -> 5 3.98/1.27 , k_0(2, 3, 3) -> 5 3.98/1.27 , k_0(3, 2, 2) -> 5 3.98/1.27 , k_0(3, 2, 3) -> 5 3.98/1.27 , k_0(3, 3, 2) -> 5 3.98/1.27 , k_0(3, 3, 3) -> 5 } 3.98/1.27 3.98/1.27 Hurray, we answered YES(?,O(n^1)) 3.98/1.27 EOF