YES(?,O(n^1)) 0.00/0.61 YES(?,O(n^1)) 0.00/0.61 0.00/0.61 We are left with following problem, upon which TcT provides the 0.00/0.61 certificate YES(?,O(n^1)). 0.00/0.61 0.00/0.61 Strict Trs: 0.00/0.61 { f(a, empty()) -> g(a, empty()) 0.00/0.61 , f(a, cons(x, k)) -> f(cons(x, a), k) 0.00/0.61 , g(empty(), d) -> d 0.00/0.61 , g(cons(x, k), d) -> g(k, cons(x, d)) } 0.00/0.61 Obligation: 0.00/0.61 innermost runtime complexity 0.00/0.61 Answer: 0.00/0.61 YES(?,O(n^1)) 0.00/0.61 0.00/0.61 The problem is match-bounded by 2. The enriched problem is 0.00/0.61 compatible with the following automaton. 0.00/0.61 { f_0(2, 2) -> 1 0.00/0.61 , f_0(2, 4) -> 1 0.00/0.61 , f_0(4, 2) -> 1 0.00/0.61 , f_0(4, 4) -> 1 0.00/0.61 , f_1(6, 2) -> 1 0.00/0.61 , f_1(6, 4) -> 1 0.00/0.61 , empty_0() -> 2 0.00/0.61 , empty_0() -> 3 0.00/0.61 , empty_1() -> 1 0.00/0.61 , empty_1() -> 5 0.00/0.61 , g_0(2, 2) -> 3 0.00/0.61 , g_0(2, 4) -> 3 0.00/0.61 , g_0(4, 2) -> 3 0.00/0.61 , g_0(4, 4) -> 3 0.00/0.61 , g_1(2, 5) -> 1 0.00/0.61 , g_1(2, 6) -> 3 0.00/0.61 , g_1(4, 5) -> 1 0.00/0.61 , g_1(4, 6) -> 3 0.00/0.61 , g_1(6, 5) -> 1 0.00/0.61 , g_2(2, 7) -> 1 0.00/0.61 , g_2(4, 7) -> 1 0.00/0.61 , g_2(6, 7) -> 1 0.00/0.61 , cons_0(2, 2) -> 3 0.00/0.61 , cons_0(2, 2) -> 4 0.00/0.61 , cons_0(2, 4) -> 3 0.00/0.61 , cons_0(2, 4) -> 4 0.00/0.61 , cons_0(4, 2) -> 3 0.00/0.61 , cons_0(4, 2) -> 4 0.00/0.61 , cons_0(4, 4) -> 3 0.00/0.61 , cons_0(4, 4) -> 4 0.00/0.61 , cons_1(2, 2) -> 3 0.00/0.61 , cons_1(2, 2) -> 6 0.00/0.61 , cons_1(2, 4) -> 3 0.00/0.61 , cons_1(2, 4) -> 6 0.00/0.61 , cons_1(2, 5) -> 1 0.00/0.61 , cons_1(2, 5) -> 5 0.00/0.61 , cons_1(2, 6) -> 3 0.00/0.61 , cons_1(2, 6) -> 6 0.00/0.61 , cons_1(2, 7) -> 1 0.00/0.61 , cons_1(2, 7) -> 5 0.00/0.61 , cons_1(4, 2) -> 3 0.00/0.61 , cons_1(4, 2) -> 6 0.00/0.61 , cons_1(4, 4) -> 3 0.00/0.61 , cons_1(4, 4) -> 6 0.00/0.61 , cons_1(4, 5) -> 1 0.00/0.61 , cons_1(4, 5) -> 5 0.00/0.61 , cons_1(4, 6) -> 3 0.00/0.61 , cons_1(4, 6) -> 6 0.00/0.61 , cons_1(4, 7) -> 1 0.00/0.61 , cons_1(4, 7) -> 5 0.00/0.61 , cons_2(2, 5) -> 1 0.00/0.61 , cons_2(2, 5) -> 7 0.00/0.61 , cons_2(2, 7) -> 1 0.00/0.61 , cons_2(2, 7) -> 7 0.00/0.61 , cons_2(4, 5) -> 1 0.00/0.61 , cons_2(4, 5) -> 7 0.00/0.61 , cons_2(4, 7) -> 1 0.00/0.61 , cons_2(4, 7) -> 7 } 0.00/0.61 0.00/0.61 Hurray, we answered YES(?,O(n^1)) 0.00/0.61 EOF