YES(?,O(n^1)) 3.44/1.45 YES(?,O(n^1)) 3.44/1.45 3.44/1.45 We are left with following problem, upon which TcT provides the 3.44/1.45 certificate YES(?,O(n^1)). 3.44/1.45 3.44/1.45 Strict Trs: 3.44/1.45 { f(X) -> n__f(X) 3.44/1.45 , f(f(X)) -> c(n__f(g(n__f(X)))) 3.44/1.45 , c(X) -> d(activate(X)) 3.44/1.45 , d(X) -> n__d(X) 3.44/1.45 , activate(X) -> X 3.44/1.45 , activate(n__f(X)) -> f(X) 3.44/1.45 , activate(n__d(X)) -> d(X) 3.44/1.45 , h(X) -> c(n__d(X)) } 3.44/1.45 Obligation: 3.44/1.45 derivational complexity 3.44/1.45 Answer: 3.44/1.45 YES(?,O(n^1)) 3.44/1.45 3.44/1.45 The problem is match-bounded by 4. The enriched problem is 3.44/1.45 compatible with the following automaton. 3.44/1.45 { f_0(1) -> 1 3.44/1.45 , f_0(1) -> 4 3.44/1.45 , f_0(1) -> 5 3.44/1.45 , f_1(1) -> 1 3.44/1.45 , f_1(1) -> 4 3.44/1.45 , f_1(1) -> 5 3.44/1.45 , f_2(1) -> 4 3.44/1.45 , f_2(1) -> 5 3.44/1.45 , f_2(3) -> 5 3.44/1.45 , f_3(1) -> 5 3.44/1.45 , f_3(7) -> 8 3.44/1.45 , c_0(1) -> 1 3.44/1.45 , c_0(1) -> 4 3.44/1.45 , c_0(1) -> 5 3.44/1.45 , c_1(2) -> 1 3.44/1.45 , c_1(2) -> 4 3.44/1.45 , c_1(2) -> 5 3.44/1.45 , c_1(4) -> 1 3.44/1.45 , c_1(4) -> 4 3.44/1.45 , c_1(4) -> 5 3.44/1.45 , c_2(6) -> 1 3.44/1.45 , c_2(6) -> 4 3.44/1.45 , c_2(6) -> 5 3.44/1.45 , n__f_0(1) -> 1 3.44/1.45 , n__f_0(1) -> 4 3.44/1.45 , n__f_0(1) -> 5 3.44/1.45 , n__f_1(1) -> 1 3.44/1.45 , n__f_1(1) -> 4 3.44/1.45 , n__f_1(1) -> 5 3.44/1.45 , n__f_1(3) -> 2 3.44/1.45 , n__f_1(3) -> 5 3.44/1.45 , n__f_2(1) -> 1 3.44/1.45 , n__f_2(1) -> 4 3.44/1.45 , n__f_2(1) -> 5 3.44/1.45 , n__f_2(7) -> 6 3.44/1.45 , n__f_2(7) -> 8 3.44/1.45 , n__f_3(1) -> 4 3.44/1.45 , n__f_3(1) -> 5 3.44/1.45 , n__f_3(3) -> 5 3.44/1.45 , n__f_4(1) -> 5 3.44/1.45 , n__f_4(7) -> 8 3.44/1.45 , g_0(1) -> 1 3.44/1.45 , g_0(1) -> 4 3.44/1.45 , g_0(1) -> 5 3.44/1.45 , g_1(1) -> 3 3.44/1.45 , g_2(4) -> 7 3.44/1.45 , d_0(1) -> 1 3.44/1.45 , d_0(1) -> 4 3.44/1.45 , d_0(1) -> 5 3.44/1.45 , d_1(1) -> 1 3.44/1.45 , d_1(1) -> 4 3.44/1.45 , d_1(1) -> 5 3.44/1.45 , d_1(4) -> 1 3.44/1.45 , d_1(4) -> 4 3.44/1.45 , d_1(4) -> 5 3.44/1.45 , d_1(5) -> 1 3.44/1.45 , d_1(5) -> 4 3.44/1.45 , d_1(5) -> 5 3.44/1.45 , d_1(8) -> 1 3.44/1.45 , d_1(8) -> 4 3.44/1.45 , d_1(8) -> 5 3.44/1.45 , d_2(1) -> 4 3.44/1.45 , d_2(1) -> 5 3.44/1.45 , d_2(4) -> 4 3.44/1.45 , d_2(4) -> 5 3.44/1.45 , d_2(5) -> 1 3.44/1.45 , d_2(5) -> 4 3.44/1.45 , d_2(5) -> 5 3.44/1.45 , d_2(8) -> 4 3.44/1.45 , d_2(8) -> 5 3.44/1.45 , d_3(1) -> 5 3.44/1.45 , d_3(4) -> 5 3.44/1.45 , d_3(5) -> 5 3.44/1.45 , d_3(8) -> 1 3.44/1.45 , d_3(8) -> 4 3.44/1.45 , d_3(8) -> 5 3.44/1.45 , activate_0(1) -> 1 3.44/1.45 , activate_0(1) -> 4 3.44/1.45 , activate_0(1) -> 5 3.44/1.45 , activate_1(1) -> 4 3.44/1.45 , activate_1(1) -> 5 3.44/1.45 , activate_2(2) -> 5 3.44/1.45 , activate_2(4) -> 5 3.44/1.45 , activate_3(6) -> 8 3.44/1.45 , h_0(1) -> 1 3.44/1.45 , h_0(1) -> 4 3.44/1.45 , h_0(1) -> 5 3.44/1.45 , n__d_0(1) -> 1 3.44/1.45 , n__d_0(1) -> 4 3.44/1.45 , n__d_0(1) -> 5 3.44/1.45 , n__d_1(1) -> 1 3.44/1.45 , n__d_1(1) -> 4 3.44/1.45 , n__d_1(1) -> 5 3.44/1.45 , n__d_2(1) -> 1 3.44/1.45 , n__d_2(1) -> 4 3.44/1.45 , n__d_2(1) -> 5 3.44/1.45 , n__d_2(4) -> 1 3.44/1.45 , n__d_2(4) -> 4 3.44/1.45 , n__d_2(4) -> 5 3.44/1.45 , n__d_2(5) -> 1 3.44/1.45 , n__d_2(5) -> 4 3.44/1.45 , n__d_2(5) -> 5 3.44/1.45 , n__d_2(8) -> 1 3.44/1.45 , n__d_2(8) -> 4 3.44/1.45 , n__d_2(8) -> 5 3.44/1.45 , n__d_3(1) -> 4 3.44/1.45 , n__d_3(1) -> 5 3.44/1.45 , n__d_3(4) -> 4 3.44/1.45 , n__d_3(4) -> 5 3.44/1.45 , n__d_3(5) -> 1 3.44/1.45 , n__d_3(5) -> 4 3.44/1.45 , n__d_3(5) -> 5 3.44/1.45 , n__d_3(8) -> 4 3.44/1.45 , n__d_3(8) -> 5 3.44/1.45 , n__d_4(1) -> 5 3.44/1.45 , n__d_4(4) -> 5 3.44/1.45 , n__d_4(5) -> 5 3.44/1.45 , n__d_4(8) -> 1 3.44/1.45 , n__d_4(8) -> 4 3.44/1.45 , n__d_4(8) -> 5 } 3.44/1.45 3.44/1.45 Hurray, we answered YES(?,O(n^1)) 3.44/1.46 EOF