YES(?,O(n^1)) 230.83/62.78 YES(?,O(n^1)) 230.83/62.78 230.83/62.78 We are left with following problem, upon which TcT provides the 230.83/62.78 certificate YES(?,O(n^1)). 230.83/62.78 230.83/62.78 Strict Trs: 230.83/62.78 { active(f(X)) -> f(active(X)) 230.83/62.78 , active(f(X)) -> mark(g(h(f(X)))) 230.83/62.78 , active(h(X)) -> h(active(X)) 230.83/62.78 , f(mark(X)) -> mark(f(X)) 230.83/62.78 , f(ok(X)) -> ok(f(X)) 230.83/62.78 , g(ok(X)) -> ok(g(X)) 230.83/62.78 , h(mark(X)) -> mark(h(X)) 230.83/62.78 , h(ok(X)) -> ok(h(X)) 230.83/62.78 , proper(f(X)) -> f(proper(X)) 230.83/62.78 , proper(g(X)) -> g(proper(X)) 230.83/62.78 , proper(h(X)) -> h(proper(X)) 230.83/62.78 , top(mark(X)) -> top(proper(X)) 230.83/62.78 , top(ok(X)) -> top(active(X)) } 230.83/62.78 Obligation: 230.83/62.78 innermost runtime complexity 230.83/62.78 Answer: 230.83/62.78 YES(?,O(n^1)) 230.83/62.78 230.83/62.78 The problem is match-bounded by 1. The enriched problem is 230.83/62.78 compatible with the following automaton. 230.83/62.78 { active_0(2) -> 1 230.83/62.78 , active_1(2) -> 4 230.83/62.78 , f_0(2) -> 1 230.83/62.78 , f_1(2) -> 3 230.83/62.78 , mark_0(2) -> 2 230.83/62.78 , mark_1(3) -> 1 230.83/62.78 , mark_1(3) -> 3 230.83/62.78 , g_0(2) -> 1 230.83/62.78 , g_1(2) -> 3 230.83/62.78 , h_0(2) -> 1 230.83/62.78 , h_1(2) -> 3 230.83/62.78 , proper_0(2) -> 1 230.83/62.78 , proper_1(2) -> 4 230.83/62.78 , ok_0(2) -> 2 230.83/62.78 , ok_1(3) -> 1 230.83/62.78 , ok_1(3) -> 3 230.83/62.78 , top_0(2) -> 1 230.83/62.78 , top_1(4) -> 1 } 230.83/62.78 230.83/62.78 Hurray, we answered YES(?,O(n^1)) 230.83/62.80 EOF