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