YES(?,O(n^1)) 22.19/12.59 YES(?,O(n^1)) 22.19/12.59 22.19/12.59 We are left with following problem, upon which TcT provides the 22.19/12.59 certificate YES(?,O(n^1)). 22.19/12.59 22.19/12.59 Strict Trs: 22.19/12.59 { f(X) -> n__f(X) 22.19/12.59 , f(f(a())) -> c(n__f(g(f(a())))) 22.19/12.59 , activate(X) -> X 22.19/12.59 , activate(n__f(X)) -> f(X) } 22.19/12.59 Obligation: 22.19/12.59 derivational complexity 22.19/12.59 Answer: 22.19/12.59 YES(?,O(n^1)) 22.19/12.59 22.19/12.59 The problem is match-bounded by 2. The enriched problem is 22.19/12.59 compatible with the following automaton. 22.19/12.59 { f_0(1) -> 1 22.19/12.59 , f_0(1) -> 6 22.19/12.59 , f_0(2) -> 1 22.19/12.59 , f_0(2) -> 6 22.19/12.59 , f_0(3) -> 1 22.19/12.59 , f_0(3) -> 6 22.19/12.59 , f_0(4) -> 1 22.19/12.59 , f_0(4) -> 6 22.19/12.59 , f_0(5) -> 1 22.19/12.59 , f_0(5) -> 6 22.19/12.59 , f_0(6) -> 1 22.19/12.59 , f_0(6) -> 6 22.19/12.59 , f_1(1) -> 6 22.19/12.59 , f_1(2) -> 6 22.19/12.59 , f_1(3) -> 6 22.19/12.59 , f_1(4) -> 6 22.19/12.59 , f_1(5) -> 6 22.19/12.59 , f_1(6) -> 6 22.19/12.59 , f_1(10) -> 9 22.19/12.59 , a_0() -> 2 22.19/12.59 , a_0() -> 6 22.19/12.59 , a_1() -> 10 22.19/12.59 , c_0(1) -> 3 22.19/12.59 , c_0(1) -> 6 22.19/12.59 , c_0(2) -> 3 22.19/12.59 , c_0(2) -> 6 22.19/12.59 , c_0(3) -> 3 22.19/12.59 , c_0(3) -> 6 22.19/12.59 , c_0(4) -> 3 22.19/12.59 , c_0(4) -> 6 22.19/12.59 , c_0(5) -> 3 22.19/12.59 , c_0(5) -> 6 22.19/12.59 , c_0(6) -> 3 22.19/12.59 , c_0(6) -> 6 22.19/12.59 , c_1(7) -> 1 22.19/12.59 , c_1(7) -> 6 22.19/12.59 , n__f_0(1) -> 4 22.19/12.59 , n__f_0(1) -> 6 22.19/12.59 , n__f_0(2) -> 4 22.19/12.59 , n__f_0(2) -> 6 22.19/12.59 , n__f_0(3) -> 4 22.19/12.59 , n__f_0(3) -> 6 22.19/12.59 , n__f_0(4) -> 4 22.19/12.59 , n__f_0(4) -> 6 22.19/12.59 , n__f_0(5) -> 4 22.19/12.59 , n__f_0(5) -> 6 22.19/12.59 , n__f_0(6) -> 4 22.19/12.59 , n__f_0(6) -> 6 22.19/12.59 , n__f_1(1) -> 1 22.19/12.59 , n__f_1(1) -> 6 22.19/12.59 , n__f_1(2) -> 1 22.19/12.59 , n__f_1(2) -> 6 22.19/12.59 , n__f_1(3) -> 1 22.19/12.59 , n__f_1(3) -> 6 22.19/12.59 , n__f_1(4) -> 1 22.19/12.59 , n__f_1(4) -> 6 22.19/12.59 , n__f_1(5) -> 1 22.19/12.59 , n__f_1(5) -> 6 22.19/12.59 , n__f_1(6) -> 1 22.19/12.59 , n__f_1(6) -> 6 22.19/12.59 , n__f_1(8) -> 7 22.19/12.59 , n__f_2(1) -> 6 22.19/12.59 , n__f_2(2) -> 6 22.19/12.59 , n__f_2(3) -> 6 22.19/12.59 , n__f_2(4) -> 6 22.19/12.59 , n__f_2(5) -> 6 22.19/12.59 , n__f_2(6) -> 6 22.19/12.59 , n__f_2(10) -> 9 22.19/12.59 , g_0(1) -> 5 22.19/12.59 , g_0(1) -> 6 22.19/12.59 , g_0(2) -> 5 22.19/12.59 , g_0(2) -> 6 22.19/12.59 , g_0(3) -> 5 22.19/12.59 , g_0(3) -> 6 22.19/12.59 , g_0(4) -> 5 22.19/12.59 , g_0(4) -> 6 22.19/12.59 , g_0(5) -> 5 22.19/12.59 , g_0(5) -> 6 22.19/12.59 , g_0(6) -> 5 22.19/12.59 , g_0(6) -> 6 22.19/12.59 , g_1(9) -> 8 22.19/12.59 , activate_0(1) -> 6 22.19/12.59 , activate_0(2) -> 6 22.19/12.59 , activate_0(3) -> 6 22.19/12.59 , activate_0(4) -> 6 22.19/12.59 , activate_0(5) -> 6 22.19/12.59 , activate_0(6) -> 6 } 22.19/12.59 22.19/12.59 Hurray, we answered YES(?,O(n^1)) 22.34/12.61 EOF