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

Strict Trs:
  { active(nats()) -> mark(adx(zeros()))
  , active(adx(X)) -> adx(active(X))
  , active(adx(cons(X, Y))) -> mark(incr(cons(X, adx(Y))))
  , active(zeros()) -> mark(cons(0(), zeros()))
  , active(incr(X)) -> incr(active(X))
  , active(incr(cons(X, Y))) -> mark(cons(s(X), incr(Y)))
  , active(hd(X)) -> hd(active(X))
  , active(hd(cons(X, Y))) -> mark(X)
  , active(tl(X)) -> tl(active(X))
  , active(tl(cons(X, Y))) -> mark(Y)
  , adx(mark(X)) -> mark(adx(X))
  , adx(ok(X)) -> ok(adx(X))
  , cons(ok(X1), ok(X2)) -> ok(cons(X1, X2))
  , incr(mark(X)) -> mark(incr(X))
  , incr(ok(X)) -> ok(incr(X))
  , s(ok(X)) -> ok(s(X))
  , hd(mark(X)) -> mark(hd(X))
  , hd(ok(X)) -> ok(hd(X))
  , tl(mark(X)) -> mark(tl(X))
  , tl(ok(X)) -> ok(tl(X))
  , proper(nats()) -> ok(nats())
  , proper(adx(X)) -> adx(proper(X))
  , proper(zeros()) -> ok(zeros())
  , proper(cons(X1, X2)) -> cons(proper(X1), proper(X2))
  , proper(0()) -> ok(0())
  , proper(incr(X)) -> incr(proper(X))
  , proper(s(X)) -> s(proper(X))
  , proper(hd(X)) -> hd(proper(X))
  , proper(tl(X)) -> tl(proper(X))
  , top(mark(X)) -> top(proper(X))
  , top(ok(X)) -> top(active(X)) }
Obligation:
  innermost runtime complexity
Answer:
  YES(?,O(n^1))

The problem is match-bounded by 10. The enriched problem is
compatible with the following automaton.
{ active_0(2) -> 1
, active_0(3) -> 1
, active_0(5) -> 1
, active_0(7) -> 1
, active_0(13) -> 1
, active_1(2) -> 25
, active_1(3) -> 25
, active_1(5) -> 25
, active_1(7) -> 25
, active_1(13) -> 25
, active_2(16) -> 26
, active_2(17) -> 26
, active_2(24) -> 26
, active_3(33) -> 32
, active_4(28) -> 38
, active_4(41) -> 42
, active_5(35) -> 43
, active_5(57) -> 50
, active_6(55) -> 51
, active_6(62) -> 63
, active_7(58) -> 64
, active_7(79) -> 69
, active_8(78) -> 72
, active_8(87) -> 88
, active_9(86) -> 89
, active_9(107) -> 96
, active_10(110) -> 111
, nats_0() -> 2
, nats_1() -> 24
, mark_0(2) -> 3
, mark_0(3) -> 3
, mark_0(5) -> 3
, mark_0(7) -> 3
, mark_0(13) -> 3
, mark_1(15) -> 1
, mark_1(15) -> 25
, mark_1(18) -> 4
, mark_1(18) -> 18
, mark_1(20) -> 8
, mark_1(20) -> 20
, mark_1(22) -> 10
, mark_1(22) -> 22
, mark_1(23) -> 11
, mark_1(23) -> 23
, mark_2(27) -> 26
, mark_3(39) -> 38
, mark_4(40) -> 32
, mark_4(44) -> 43
, mark_5(47) -> 42
, mark_6(59) -> 50
, mark_7(65) -> 63
, mark_7(82) -> 69
, mark_8(90) -> 88
, adx_0(2) -> 4
, adx_0(3) -> 4
, adx_0(5) -> 4
, adx_0(7) -> 4
, adx_0(13) -> 4
, adx_1(2) -> 18
, adx_1(3) -> 18
, adx_1(5) -> 18
, adx_1(7) -> 18
, adx_1(13) -> 18
, adx_1(16) -> 15
, adx_2(28) -> 27
, adx_2(30) -> 26
, adx_3(28) -> 33
, adx_3(34) -> 32
, adx_4(35) -> 41
, adx_4(38) -> 32
, adx_4(39) -> 40
, adx_5(43) -> 42
, adx_5(44) -> 47
, adx_6(46) -> 61
, adx_6(51) -> 50
, adx_6(55) -> 57
, adx_6(56) -> 77
, adx_7(56) -> 67
, adx_7(58) -> 62
, adx_7(64) -> 63
, adx_7(73) -> 71
, adx_7(81) -> 85
, adx_7(98) -> 95
, adx_8(80) -> 75
, adx_8(103) -> 101
, adx_8(104) -> 106
, zeros_0() -> 5
, zeros_1() -> 16
, zeros_2() -> 28
, zeros_3() -> 35
, zeros_4() -> 46
, zeros_5() -> 56
, zeros_6() -> 81
, zeros_7() -> 104
, cons_0(2, 2) -> 6
, cons_0(2, 3) -> 6
, cons_0(2, 5) -> 6
, cons_0(2, 7) -> 6
, cons_0(2, 13) -> 6
, cons_0(3, 2) -> 6
, cons_0(3, 3) -> 6
, cons_0(3, 5) -> 6
, cons_0(3, 7) -> 6
, cons_0(3, 13) -> 6
, cons_0(5, 2) -> 6
, cons_0(5, 3) -> 6
, cons_0(5, 5) -> 6
, cons_0(5, 7) -> 6
, cons_0(5, 13) -> 6
, cons_0(7, 2) -> 6
, cons_0(7, 3) -> 6
, cons_0(7, 5) -> 6
, cons_0(7, 7) -> 6
, cons_0(7, 13) -> 6
, cons_0(13, 2) -> 6
, cons_0(13, 3) -> 6
, cons_0(13, 5) -> 6
, cons_0(13, 7) -> 6
, cons_0(13, 13) -> 6
, cons_1(2, 2) -> 19
, cons_1(2, 3) -> 19
, cons_1(2, 5) -> 19
, cons_1(2, 7) -> 19
, cons_1(2, 13) -> 19
, cons_1(3, 2) -> 19
, cons_1(3, 3) -> 19
, cons_1(3, 5) -> 19
, cons_1(3, 7) -> 19
, cons_1(3, 13) -> 19
, cons_1(5, 2) -> 19
, cons_1(5, 3) -> 19
, cons_1(5, 5) -> 19
, cons_1(5, 7) -> 19
, cons_1(5, 13) -> 19
, cons_1(7, 2) -> 19
, cons_1(7, 3) -> 19
, cons_1(7, 5) -> 19
, cons_1(7, 7) -> 19
, cons_1(7, 13) -> 19
, cons_1(13, 2) -> 19
, cons_1(13, 3) -> 19
, cons_1(13, 5) -> 19
, cons_1(13, 7) -> 19
, cons_1(13, 13) -> 19
, cons_1(17, 16) -> 15
, cons_2(29, 28) -> 27
, cons_2(31, 30) -> 26
, cons_3(29, 28) -> 33
, cons_3(36, 34) -> 32
, cons_3(37, 35) -> 39
, cons_4(37, 35) -> 41
, cons_4(45, 46) -> 44
, cons_4(48, 49) -> 43
, cons_5(45, 46) -> 55
, cons_5(52, 53) -> 51
, cons_6(45, 61) -> 60
, cons_6(54, 56) -> 58
, cons_6(54, 77) -> 78
, cons_7(54, 67) -> 66
, cons_7(70, 71) -> 68
, cons_7(76, 85) -> 86
, cons_7(83, 84) -> 82
, cons_8(74, 75) -> 72
, cons_8(91, 92) -> 90
, cons_8(93, 94) -> 88
, cons_8(97, 92) -> 107
, cons_9(99, 100) -> 96
, cons_9(109, 108) -> 110
, 0_0() -> 7
, 0_1() -> 17
, 0_2() -> 29
, 0_3() -> 37
, 0_4() -> 45
, 0_5() -> 54
, 0_6() -> 76
, 0_7() -> 105
, incr_0(2) -> 8
, incr_0(3) -> 8
, incr_0(5) -> 8
, incr_0(7) -> 8
, incr_0(13) -> 8
, incr_1(2) -> 20
, incr_1(3) -> 20
, incr_1(5) -> 20
, incr_1(7) -> 20
, incr_1(13) -> 20
, incr_6(60) -> 59
, incr_7(66) -> 65
, incr_7(68) -> 63
, incr_7(77) -> 84
, incr_7(78) -> 79
, incr_8(72) -> 69
, incr_8(85) -> 92
, incr_8(86) -> 87
, incr_8(95) -> 94
, incr_9(89) -> 88
, incr_9(101) -> 100
, incr_9(106) -> 108
, s_0(2) -> 9
, s_0(3) -> 9
, s_0(5) -> 9
, s_0(7) -> 9
, s_0(13) -> 9
, s_1(2) -> 21
, s_1(3) -> 21
, s_1(5) -> 21
, s_1(7) -> 21
, s_1(13) -> 21
, s_7(54) -> 83
, s_7(76) -> 97
, s_8(74) -> 93
, s_8(76) -> 91
, s_8(105) -> 109
, s_9(102) -> 99
, hd_0(2) -> 10
, hd_0(3) -> 10
, hd_0(5) -> 10
, hd_0(7) -> 10
, hd_0(13) -> 10
, hd_1(2) -> 22
, hd_1(3) -> 22
, hd_1(5) -> 22
, hd_1(7) -> 22
, hd_1(13) -> 22
, tl_0(2) -> 11
, tl_0(3) -> 11
, tl_0(5) -> 11
, tl_0(7) -> 11
, tl_0(13) -> 11
, tl_1(2) -> 23
, tl_1(3) -> 23
, tl_1(5) -> 23
, tl_1(7) -> 23
, tl_1(13) -> 23
, proper_0(2) -> 12
, proper_0(3) -> 12
, proper_0(5) -> 12
, proper_0(7) -> 12
, proper_0(13) -> 12
, proper_1(2) -> 25
, proper_1(3) -> 25
, proper_1(5) -> 25
, proper_1(7) -> 25
, proper_1(13) -> 25
, proper_2(15) -> 26
, proper_2(16) -> 30
, proper_2(17) -> 31
, proper_3(27) -> 32
, proper_3(28) -> 34
, proper_3(29) -> 36
, proper_4(35) -> 49
, proper_4(37) -> 48
, proper_4(40) -> 42
, proper_5(39) -> 43
, proper_5(45) -> 52
, proper_5(46) -> 53
, proper_5(47) -> 50
, proper_6(44) -> 51
, proper_6(59) -> 63
, proper_7(45) -> 70
, proper_7(46) -> 73
, proper_7(56) -> 98
, proper_7(60) -> 68
, proper_7(61) -> 71
, proper_7(65) -> 69
, proper_8(54) -> 74
, proper_8(56) -> 80
, proper_8(66) -> 72
, proper_8(67) -> 75
, proper_8(77) -> 95
, proper_8(81) -> 103
, proper_8(82) -> 88
, proper_8(83) -> 93
, proper_8(84) -> 94
, proper_9(76) -> 102
, proper_9(85) -> 101
, proper_9(90) -> 96
, proper_9(91) -> 99
, proper_9(92) -> 100
, ok_0(2) -> 13
, ok_0(3) -> 13
, ok_0(5) -> 13
, ok_0(7) -> 13
, ok_0(13) -> 13
, ok_1(16) -> 12
, ok_1(16) -> 25
, ok_1(17) -> 12
, ok_1(17) -> 25
, ok_1(18) -> 4
, ok_1(18) -> 18
, ok_1(19) -> 6
, ok_1(19) -> 19
, ok_1(20) -> 8
, ok_1(20) -> 20
, ok_1(21) -> 9
, ok_1(21) -> 21
, ok_1(22) -> 10
, ok_1(22) -> 22
, ok_1(23) -> 11
, ok_1(23) -> 23
, ok_1(24) -> 12
, ok_1(24) -> 25
, ok_2(28) -> 30
, ok_2(29) -> 31
, ok_3(33) -> 26
, ok_3(35) -> 34
, ok_3(37) -> 36
, ok_4(41) -> 32
, ok_4(45) -> 48
, ok_4(46) -> 49
, ok_5(54) -> 52
, ok_5(54) -> 70
, ok_5(55) -> 43
, ok_5(56) -> 53
, ok_5(56) -> 73
, ok_6(57) -> 42
, ok_6(58) -> 51
, ok_6(76) -> 74
, ok_6(77) -> 71
, ok_6(78) -> 68
, ok_6(81) -> 80
, ok_6(81) -> 98
, ok_7(62) -> 50
, ok_7(79) -> 63
, ok_7(85) -> 75
, ok_7(85) -> 95
, ok_7(86) -> 72
, ok_7(97) -> 93
, ok_7(104) -> 103
, ok_7(105) -> 102
, ok_8(87) -> 69
, ok_8(92) -> 94
, ok_8(106) -> 101
, ok_8(107) -> 88
, ok_8(109) -> 99
, ok_9(108) -> 100
, ok_9(110) -> 96
, top_0(2) -> 14
, top_0(3) -> 14
, top_0(5) -> 14
, top_0(7) -> 14
, top_0(13) -> 14
, top_1(25) -> 14
, top_2(26) -> 14
, top_3(32) -> 14
, top_4(42) -> 14
, top_5(50) -> 14
, top_6(63) -> 14
, top_7(69) -> 14
, top_8(88) -> 14
, top_9(96) -> 14
, top_10(111) -> 14 }

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