YES(?,O(n^1)) 633.11/166.90 YES(?,O(n^1)) 633.11/166.90 633.11/166.90 We are left with following problem, upon which TcT provides the 633.11/166.90 certificate YES(?,O(n^1)). 633.11/166.90 633.11/166.90 Strict Trs: 633.11/166.90 { active(f(X)) -> f(active(X)) 633.11/166.90 , active(f(f(a()))) -> mark(f(g(f(a())))) 633.11/166.90 , f(mark(X)) -> mark(f(X)) 633.11/166.90 , f(ok(X)) -> ok(f(X)) 633.11/166.90 , g(ok(X)) -> ok(g(X)) 633.11/166.90 , proper(f(X)) -> f(proper(X)) 633.11/166.90 , proper(a()) -> ok(a()) 633.11/166.90 , proper(g(X)) -> g(proper(X)) 633.11/166.90 , top(mark(X)) -> top(proper(X)) 633.11/166.90 , top(ok(X)) -> top(active(X)) } 633.11/166.90 Obligation: 633.11/166.90 runtime complexity 633.11/166.90 Answer: 633.11/166.90 YES(?,O(n^1)) 633.11/166.90 633.11/166.90 The problem is match-bounded by 2. The enriched problem is 633.11/166.90 compatible with the following automaton. 633.11/166.90 { active_0(3) -> 1 633.11/166.90 , active_0(4) -> 1 633.11/166.90 , active_0(7) -> 1 633.11/166.90 , active_1(3) -> 12 633.11/166.90 , active_1(4) -> 12 633.11/166.90 , active_1(7) -> 12 633.11/166.90 , active_2(11) -> 13 633.11/166.90 , f_0(3) -> 2 633.11/166.90 , f_0(4) -> 2 633.11/166.90 , f_0(7) -> 2 633.11/166.90 , f_1(3) -> 9 633.11/166.90 , f_1(4) -> 9 633.11/166.90 , f_1(7) -> 9 633.11/166.90 , a_0() -> 3 633.11/166.90 , a_1() -> 11 633.11/166.90 , mark_0(3) -> 4 633.11/166.90 , mark_0(4) -> 4 633.11/166.90 , mark_0(7) -> 4 633.11/166.90 , mark_1(9) -> 2 633.11/166.90 , mark_1(9) -> 9 633.11/166.90 , g_0(3) -> 5 633.11/166.90 , g_0(4) -> 5 633.11/166.90 , g_0(7) -> 5 633.11/166.90 , g_1(3) -> 10 633.11/166.90 , g_1(4) -> 10 633.11/166.90 , g_1(7) -> 10 633.11/166.90 , proper_0(3) -> 6 633.11/166.90 , proper_0(4) -> 6 633.11/166.90 , proper_0(7) -> 6 633.11/166.90 , proper_1(3) -> 12 633.11/166.90 , proper_1(4) -> 12 633.11/166.90 , proper_1(7) -> 12 633.11/166.90 , ok_0(3) -> 7 633.11/166.90 , ok_0(4) -> 7 633.11/166.90 , ok_0(7) -> 7 633.11/166.90 , ok_1(9) -> 2 633.11/166.90 , ok_1(9) -> 9 633.11/166.90 , ok_1(10) -> 5 633.11/166.90 , ok_1(10) -> 10 633.11/166.90 , ok_1(11) -> 6 633.11/166.90 , ok_1(11) -> 12 633.11/166.90 , top_0(3) -> 8 633.11/166.90 , top_0(4) -> 8 633.11/166.90 , top_0(7) -> 8 633.11/166.90 , top_1(12) -> 8 633.11/166.90 , top_2(13) -> 8 } 633.11/166.90 633.11/166.90 Hurray, we answered YES(?,O(n^1)) 633.11/166.95 EOF