YES(?,O(n^1))

We are left with following problem, upon which TcT provides the
certificate YES(?,O(n^1)).

Strict Trs:
  { second(C(x1, x2)) -> x2
  , eqZList(Z(), Z()) -> True()
  , eqZList(Z(), C(y1, y2)) -> False()
  , eqZList(C(x1, x2), Z()) -> False()
  , eqZList(C(x1, x2), C(y1, y2)) ->
    and(eqZList(x1, y1), eqZList(x2, y2))
  , f(Z()) -> Z()
  , f(C(x1, x2)) -> C(f(x1), f(x2))
  , first(C(x1, x2)) -> x1
  , g(x) -> x }
Weak Trs:
  { and(True(), True()) -> True()
  , and(True(), False()) -> False()
  , and(False(), True()) -> False()
  , and(False(), False()) -> False() }
Obligation:
  innermost runtime complexity
Answer:
  YES(?,O(n^1))

The problem is match-bounded by 1. The enriched problem is
compatible with the following automaton.
{ second_0(2) -> 1
, eqZList_0(2, 2) -> 1
, eqZList_1(2, 2) -> 3
, eqZList_1(2, 2) -> 4
, Z_0() -> 1
, Z_0() -> 2
, Z_1() -> 1
, Z_1() -> 5
, Z_1() -> 6
, True_0() -> 1
, True_0() -> 2
, True_1() -> 1
, True_1() -> 3
, True_1() -> 4
, f_0(2) -> 1
, f_1(2) -> 5
, f_1(2) -> 6
, C_0(2, 2) -> 1
, C_0(2, 2) -> 2
, C_1(5, 6) -> 1
, C_1(6, 6) -> 5
, C_1(6, 6) -> 6
, and_0(2, 2) -> 1
, and_1(3, 4) -> 1
, and_1(4, 4) -> 3
, and_1(4, 4) -> 4
, first_0(2) -> 1
, False_0() -> 1
, False_0() -> 2
, False_1() -> 1
, False_1() -> 3
, False_1() -> 4
, g_0(2) -> 1
, 2 -> 1 }

Hurray, we answered YES(?,O(n^1))