YES(?,O(n^1)) 0.00/0.92 YES(?,O(n^1)) 0.00/0.92 0.00/0.92 We are left with following problem, upon which TcT provides the 0.00/0.92 certificate YES(?,O(n^1)). 0.00/0.92 0.00/0.92 Strict Trs: 0.00/0.92 { second(C(x1, x2)) -> x2 0.00/0.92 , eqZList(Z(), Z()) -> True() 0.00/0.92 , eqZList(Z(), C(y1, y2)) -> False() 0.00/0.92 , eqZList(C(x1, x2), Z()) -> False() 0.00/0.92 , eqZList(C(x1, x2), C(y1, y2)) -> 0.00/0.92 and(eqZList(x1, y1), eqZList(x2, y2)) 0.00/0.92 , f(Z()) -> Z() 0.00/0.92 , f(C(x1, x2)) -> C(f(x1), f(x2)) 0.00/0.92 , first(C(x1, x2)) -> x1 0.00/0.92 , g(x) -> x } 0.00/0.92 Weak Trs: 0.00/0.92 { and(True(), True()) -> True() 0.00/0.92 , and(True(), False()) -> False() 0.00/0.92 , and(False(), True()) -> False() 0.00/0.92 , and(False(), False()) -> False() } 0.00/0.92 Obligation: 0.00/0.92 innermost runtime complexity 0.00/0.92 Answer: 0.00/0.92 YES(?,O(n^1)) 0.00/0.92 0.00/0.92 The problem is match-bounded by 1. The enriched problem is 0.00/0.92 compatible with the following automaton. 0.00/0.92 { second_0(2) -> 1 0.00/0.92 , eqZList_0(2, 2) -> 1 0.00/0.92 , eqZList_1(2, 2) -> 3 0.00/0.92 , eqZList_1(2, 2) -> 4 0.00/0.92 , Z_0() -> 1 0.00/0.92 , Z_0() -> 2 0.00/0.92 , Z_1() -> 1 0.00/0.92 , Z_1() -> 5 0.00/0.92 , Z_1() -> 6 0.00/0.92 , True_0() -> 1 0.00/0.92 , True_0() -> 2 0.00/0.92 , True_1() -> 1 0.00/0.92 , True_1() -> 3 0.00/0.92 , True_1() -> 4 0.00/0.92 , f_0(2) -> 1 0.00/0.92 , f_1(2) -> 5 0.00/0.92 , f_1(2) -> 6 0.00/0.92 , C_0(2, 2) -> 1 0.00/0.92 , C_0(2, 2) -> 2 0.00/0.92 , C_1(5, 6) -> 1 0.00/0.92 , C_1(6, 6) -> 5 0.00/0.92 , C_1(6, 6) -> 6 0.00/0.92 , and_0(2, 2) -> 1 0.00/0.92 , and_1(3, 4) -> 1 0.00/0.92 , and_1(4, 4) -> 3 0.00/0.92 , and_1(4, 4) -> 4 0.00/0.92 , first_0(2) -> 1 0.00/0.92 , False_0() -> 1 0.00/0.92 , False_0() -> 2 0.00/0.92 , False_1() -> 1 0.00/0.92 , False_1() -> 3 0.00/0.92 , False_1() -> 4 0.00/0.92 , g_0(2) -> 1 } 0.00/0.92 0.00/0.92 Hurray, we answered YES(?,O(n^1)) 0.00/0.93 EOF