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

Strict Trs:
  { active(f(x)) -> f(active(x))
  , active(f(x)) -> mark(x)
  , f(mark(x)) -> mark(f(x))
  , f(ok(x)) -> ok(f(x))
  , f(found(x)) -> found(f(x))
  , top(active(c())) -> top(mark(c()))
  , top(mark(x)) -> top(check(x))
  , top(found(x)) -> top(active(x))
  , check(x) -> start(match(f(X()), x))
  , check(f(x)) -> f(check(x))
  , start(ok(x)) -> found(x)
  , match(f(x), f(y)) -> f(match(x, y))
  , match(X(), x) -> proper(x)
  , proper(f(x)) -> f(proper(x))
  , proper(c()) -> ok(c()) }
Obligation:
  innermost runtime complexity
Answer:
  YES(?,O(n^1))

The problem is match-bounded by 3. The enriched problem is
compatible with the following automaton.
{ active_0(3) -> 1
, active_0(5) -> 1
, active_0(9) -> 1
, active_0(11) -> 1
, active_0(12) -> 1
, active_1(3) -> 14
, active_1(5) -> 14
, active_1(9) -> 14
, active_1(11) -> 14
, active_1(12) -> 14
, f_0(3) -> 2
, f_0(5) -> 2
, f_0(9) -> 2
, f_0(11) -> 2
, f_0(12) -> 2
, f_1(3) -> 13
, f_1(5) -> 13
, f_1(9) -> 13
, f_1(11) -> 13
, f_1(12) -> 13
, f_1(17) -> 16
, f_2(20) -> 19
, f_3(25) -> 24
, mark_0(3) -> 3
, mark_0(5) -> 3
, mark_0(9) -> 3
, mark_0(11) -> 3
, mark_0(12) -> 3
, mark_1(13) -> 2
, mark_1(13) -> 13
, mark_1(21) -> 14
, top_0(3) -> 4
, top_0(5) -> 4
, top_0(9) -> 4
, top_0(11) -> 4
, top_0(12) -> 4
, top_1(14) -> 4
, top_2(22) -> 4
, c_0() -> 5
, c_1() -> 21
, check_0(3) -> 6
, check_0(5) -> 6
, check_0(9) -> 6
, check_0(11) -> 6
, check_0(12) -> 6
, check_1(3) -> 14
, check_1(5) -> 14
, check_1(9) -> 14
, check_1(11) -> 14
, check_1(12) -> 14
, check_2(21) -> 22
, start_0(3) -> 7
, start_0(5) -> 7
, start_0(9) -> 7
, start_0(11) -> 7
, start_0(12) -> 7
, start_1(15) -> 6
, start_2(18) -> 14
, start_3(23) -> 22
, match_0(3, 3) -> 8
, match_0(3, 5) -> 8
, match_0(3, 9) -> 8
, match_0(3, 11) -> 8
, match_0(3, 12) -> 8
, match_0(5, 3) -> 8
, match_0(5, 5) -> 8
, match_0(5, 9) -> 8
, match_0(5, 11) -> 8
, match_0(5, 12) -> 8
, match_0(9, 3) -> 8
, match_0(9, 5) -> 8
, match_0(9, 9) -> 8
, match_0(9, 11) -> 8
, match_0(9, 12) -> 8
, match_0(11, 3) -> 8
, match_0(11, 5) -> 8
, match_0(11, 9) -> 8
, match_0(11, 11) -> 8
, match_0(11, 12) -> 8
, match_0(12, 3) -> 8
, match_0(12, 5) -> 8
, match_0(12, 9) -> 8
, match_0(12, 11) -> 8
, match_0(12, 12) -> 8
, match_1(16, 3) -> 15
, match_1(16, 5) -> 15
, match_1(16, 9) -> 15
, match_1(16, 11) -> 15
, match_1(16, 12) -> 15
, match_2(19, 3) -> 18
, match_2(19, 5) -> 18
, match_2(19, 9) -> 18
, match_2(19, 11) -> 18
, match_2(19, 12) -> 18
, match_3(24, 21) -> 23
, X_0() -> 9
, X_1() -> 17
, X_2() -> 20
, X_3() -> 25
, proper_0(3) -> 10
, proper_0(5) -> 10
, proper_0(9) -> 10
, proper_0(11) -> 10
, proper_0(12) -> 10
, proper_1(3) -> 8
, proper_1(5) -> 8
, proper_1(9) -> 8
, proper_1(11) -> 8
, proper_1(12) -> 8
, ok_0(3) -> 11
, ok_0(5) -> 11
, ok_0(9) -> 11
, ok_0(11) -> 11
, ok_0(12) -> 11
, ok_1(13) -> 2
, ok_1(13) -> 13
, ok_1(21) -> 8
, ok_1(21) -> 10
, found_0(3) -> 12
, found_0(5) -> 12
, found_0(9) -> 12
, found_0(11) -> 12
, found_0(12) -> 12
, found_1(3) -> 7
, found_1(5) -> 7
, found_1(9) -> 7
, found_1(11) -> 7
, found_1(12) -> 7
, found_1(13) -> 2
, found_1(13) -> 13 }

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