YES(?,O(n^1)) 0.00/0.83 YES(?,O(n^1)) 0.00/0.83 0.00/0.83 We are left with following problem, upon which TcT provides the 0.00/0.83 certificate YES(?,O(n^1)). 0.00/0.83 0.00/0.83 Strict Trs: 0.00/0.83 { f(X) -> n__f(X) 0.00/0.83 , f(n__f(n__a())) -> f(n__g(n__f(n__a()))) 0.00/0.83 , a() -> n__a() 0.00/0.83 , g(X) -> n__g(X) 0.00/0.83 , activate(X) -> X 0.00/0.83 , activate(n__f(X)) -> f(X) 0.00/0.83 , activate(n__a()) -> a() 0.00/0.83 , activate(n__g(X)) -> g(activate(X)) } 0.00/0.83 Obligation: 0.00/0.83 innermost runtime complexity 0.00/0.83 Answer: 0.00/0.83 YES(?,O(n^1)) 0.00/0.83 0.00/0.83 The problem is match-bounded by 2. The enriched problem is 0.00/0.83 compatible with the following automaton. 0.00/0.83 { f_0(2) -> 1 0.00/0.83 , f_1(2) -> 1 0.00/0.83 , f_1(2) -> 6 0.00/0.83 , f_1(3) -> 1 0.00/0.83 , f_1(3) -> 6 0.00/0.83 , n__f_0(2) -> 1 0.00/0.83 , n__f_0(2) -> 2 0.00/0.83 , n__f_0(2) -> 6 0.00/0.83 , n__f_1(2) -> 1 0.00/0.83 , n__f_1(5) -> 4 0.00/0.83 , n__f_2(2) -> 1 0.00/0.83 , n__f_2(2) -> 6 0.00/0.83 , n__f_2(3) -> 1 0.00/0.83 , n__f_2(3) -> 6 0.00/0.83 , n__a_0() -> 1 0.00/0.83 , n__a_0() -> 2 0.00/0.83 , n__a_0() -> 6 0.00/0.83 , n__a_1() -> 1 0.00/0.83 , n__a_1() -> 5 0.00/0.83 , n__a_2() -> 1 0.00/0.83 , n__a_2() -> 6 0.00/0.83 , n__g_0(2) -> 1 0.00/0.83 , n__g_0(2) -> 2 0.00/0.83 , n__g_0(2) -> 6 0.00/0.83 , n__g_1(2) -> 1 0.00/0.83 , n__g_1(4) -> 3 0.00/0.83 , n__g_2(6) -> 1 0.00/0.83 , n__g_2(6) -> 6 0.00/0.83 , a_0() -> 1 0.00/0.83 , a_1() -> 1 0.00/0.83 , a_1() -> 6 0.00/0.83 , g_0(2) -> 1 0.00/0.83 , g_1(6) -> 1 0.00/0.83 , g_1(6) -> 6 0.00/0.83 , activate_0(2) -> 1 0.00/0.83 , activate_1(2) -> 6 } 0.00/0.83 0.00/0.83 Hurray, we answered YES(?,O(n^1)) 0.00/0.84 EOF