YES(?,O(n^1))

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

Strict Trs:
  { active(incr(X)) -> incr(active(X))
  , active(incr(nil())) -> mark(nil())
  , active(incr(cons(X, L))) -> mark(cons(s(X), incr(L)))
  , active(cons(X1, X2)) -> cons(active(X1), X2)
  , active(s(X)) -> s(active(X))
  , active(adx(X)) -> adx(active(X))
  , active(adx(nil())) -> mark(nil())
  , active(adx(cons(X, L))) -> mark(incr(cons(X, adx(L))))
  , active(nats()) -> mark(adx(zeros()))
  , active(zeros()) -> mark(cons(0(), zeros()))
  , active(head(X)) -> head(active(X))
  , active(head(cons(X, L))) -> mark(X)
  , active(tail(X)) -> tail(active(X))
  , active(tail(cons(X, L))) -> mark(L)
  , incr(mark(X)) -> mark(incr(X))
  , incr(ok(X)) -> ok(incr(X))
  , cons(mark(X1), X2) -> mark(cons(X1, X2))
  , cons(ok(X1), ok(X2)) -> ok(cons(X1, X2))
  , s(mark(X)) -> mark(s(X))
  , s(ok(X)) -> ok(s(X))
  , adx(mark(X)) -> mark(adx(X))
  , adx(ok(X)) -> ok(adx(X))
  , head(mark(X)) -> mark(head(X))
  , head(ok(X)) -> ok(head(X))
  , tail(mark(X)) -> mark(tail(X))
  , tail(ok(X)) -> ok(tail(X))
  , proper(incr(X)) -> incr(proper(X))
  , proper(nil()) -> ok(nil())
  , proper(cons(X1, X2)) -> cons(proper(X1), proper(X2))
  , proper(s(X)) -> s(proper(X))
  , proper(adx(X)) -> adx(proper(X))
  , proper(nats()) -> ok(nats())
  , proper(zeros()) -> ok(zeros())
  , proper(0()) -> ok(0())
  , proper(head(X)) -> head(proper(X))
  , proper(tail(X)) -> tail(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(3) -> 1
, active_0(4) -> 1
, active_0(8) -> 1
, active_0(9) -> 1
, active_0(10) -> 1
, active_0(14) -> 1
, active_1(3) -> 26
, active_1(4) -> 26
, active_1(8) -> 26
, active_1(9) -> 26
, active_1(10) -> 26
, active_1(14) -> 26
, active_2(17) -> 27
, active_2(18) -> 27
, active_2(25) -> 27
, active_3(34) -> 33
, active_4(29) -> 40
, active_4(30) -> 39
, active_4(42) -> 44
, active_5(37) -> 46
, active_5(38) -> 45
, active_5(56) -> 51
, active_6(48) -> 67
, active_6(55) -> 54
, active_6(65) -> 66
, active_7(60) -> 77
, active_7(64) -> 68
, active_7(87) -> 76
, active_8(84) -> 98
, active_8(85) -> 79
, active_8(92) -> 93
, active_9(88) -> 94
, active_9(102) -> 115
, active_9(108) -> 120
, active_9(113) -> 101
, active_10(109) -> 119
, active_10(117) -> 118
, incr_0(3) -> 2
, incr_0(4) -> 2
, incr_0(8) -> 2
, incr_0(9) -> 2
, incr_0(10) -> 2
, incr_0(14) -> 2
, incr_1(3) -> 19
, incr_1(4) -> 19
, incr_1(8) -> 19
, incr_1(9) -> 19
, incr_1(10) -> 19
, incr_1(14) -> 19
, incr_6(62) -> 61
, incr_7(70) -> 69
, incr_7(72) -> 66
, incr_7(78) -> 91
, incr_7(85) -> 87
, incr_8(79) -> 76
, incr_8(86) -> 97
, incr_8(88) -> 92
, incr_8(103) -> 100
, incr_9(94) -> 93
, incr_9(110) -> 105
, incr_9(114) -> 116
, nil_0() -> 3
, nil_1() -> 25
, mark_0(3) -> 4
, mark_0(4) -> 4
, mark_0(8) -> 4
, mark_0(9) -> 4
, mark_0(10) -> 4
, mark_0(14) -> 4
, mark_1(16) -> 1
, mark_1(16) -> 26
, mark_1(19) -> 2
, mark_1(19) -> 19
, mark_1(20) -> 5
, mark_1(20) -> 20
, mark_1(21) -> 6
, mark_1(21) -> 21
, mark_1(22) -> 7
, mark_1(22) -> 22
, mark_1(23) -> 11
, mark_1(23) -> 23
, mark_1(24) -> 12
, mark_1(24) -> 24
, mark_2(28) -> 27
, mark_3(41) -> 40
, mark_4(43) -> 33
, mark_4(47) -> 46
, mark_5(50) -> 44
, mark_6(61) -> 51
, mark_7(69) -> 66
, mark_7(89) -> 76
, mark_8(95) -> 93
, cons_0(3, 3) -> 5
, cons_0(3, 4) -> 5
, cons_0(3, 8) -> 5
, cons_0(3, 9) -> 5
, cons_0(3, 10) -> 5
, cons_0(3, 14) -> 5
, cons_0(4, 3) -> 5
, cons_0(4, 4) -> 5
, cons_0(4, 8) -> 5
, cons_0(4, 9) -> 5
, cons_0(4, 10) -> 5
, cons_0(4, 14) -> 5
, cons_0(8, 3) -> 5
, cons_0(8, 4) -> 5
, cons_0(8, 8) -> 5
, cons_0(8, 9) -> 5
, cons_0(8, 10) -> 5
, cons_0(8, 14) -> 5
, cons_0(9, 3) -> 5
, cons_0(9, 4) -> 5
, cons_0(9, 8) -> 5
, cons_0(9, 9) -> 5
, cons_0(9, 10) -> 5
, cons_0(9, 14) -> 5
, cons_0(10, 3) -> 5
, cons_0(10, 4) -> 5
, cons_0(10, 8) -> 5
, cons_0(10, 9) -> 5
, cons_0(10, 10) -> 5
, cons_0(10, 14) -> 5
, cons_0(14, 3) -> 5
, cons_0(14, 4) -> 5
, cons_0(14, 8) -> 5
, cons_0(14, 9) -> 5
, cons_0(14, 10) -> 5
, cons_0(14, 14) -> 5
, cons_1(3, 3) -> 20
, cons_1(3, 4) -> 20
, cons_1(3, 8) -> 20
, cons_1(3, 9) -> 20
, cons_1(3, 10) -> 20
, cons_1(3, 14) -> 20
, cons_1(4, 3) -> 20
, cons_1(4, 4) -> 20
, cons_1(4, 8) -> 20
, cons_1(4, 9) -> 20
, cons_1(4, 10) -> 20
, cons_1(4, 14) -> 20
, cons_1(8, 3) -> 20
, cons_1(8, 4) -> 20
, cons_1(8, 8) -> 20
, cons_1(8, 9) -> 20
, cons_1(8, 10) -> 20
, cons_1(8, 14) -> 20
, cons_1(9, 3) -> 20
, cons_1(9, 4) -> 20
, cons_1(9, 8) -> 20
, cons_1(9, 9) -> 20
, cons_1(9, 10) -> 20
, cons_1(9, 14) -> 20
, cons_1(10, 3) -> 20
, cons_1(10, 4) -> 20
, cons_1(10, 8) -> 20
, cons_1(10, 9) -> 20
, cons_1(10, 10) -> 20
, cons_1(10, 14) -> 20
, cons_1(14, 3) -> 20
, cons_1(14, 4) -> 20
, cons_1(14, 8) -> 20
, cons_1(14, 9) -> 20
, cons_1(14, 10) -> 20
, cons_1(14, 14) -> 20
, cons_1(18, 17) -> 16
, cons_2(30, 29) -> 28
, cons_2(31, 32) -> 27
, cons_3(30, 29) -> 34
, cons_3(35, 36) -> 33
, cons_3(38, 37) -> 41
, cons_4(38, 37) -> 42
, cons_4(39, 29) -> 33
, cons_4(48, 49) -> 47
, cons_4(52, 53) -> 46
, cons_5(45, 37) -> 44
, cons_5(48, 49) -> 55
, cons_5(57, 58) -> 54
, cons_6(48, 63) -> 62
, cons_6(60, 59) -> 64
, cons_6(60, 78) -> 85
, cons_6(67, 49) -> 54
, cons_7(60, 71) -> 70
, cons_7(73, 74) -> 72
, cons_7(77, 59) -> 68
, cons_7(77, 78) -> 79
, cons_7(84, 86) -> 88
, cons_7(90, 91) -> 89
, cons_8(80, 81) -> 79
, cons_8(96, 97) -> 95
, cons_8(98, 86) -> 94
, cons_8(99, 100) -> 93
, cons_8(102, 97) -> 113
, cons_9(104, 105) -> 101
, cons_9(109, 116) -> 117
, cons_9(115, 97) -> 101
, cons_10(119, 116) -> 118
, s_0(3) -> 6
, s_0(4) -> 6
, s_0(8) -> 6
, s_0(9) -> 6
, s_0(10) -> 6
, s_0(14) -> 6
, s_1(3) -> 21
, s_1(4) -> 21
, s_1(8) -> 21
, s_1(9) -> 21
, s_1(10) -> 21
, s_1(14) -> 21
, s_7(60) -> 90
, s_7(84) -> 102
, s_8(80) -> 99
, s_8(84) -> 96
, s_8(98) -> 115
, s_8(108) -> 109
, s_9(106) -> 104
, s_9(120) -> 119
, adx_0(3) -> 7
, adx_0(4) -> 7
, adx_0(8) -> 7
, adx_0(9) -> 7
, adx_0(10) -> 7
, adx_0(14) -> 7
, adx_1(3) -> 22
, adx_1(4) -> 22
, adx_1(8) -> 22
, adx_1(9) -> 22
, adx_1(10) -> 22
, adx_1(14) -> 22
, adx_1(17) -> 16
, adx_2(29) -> 28
, adx_2(32) -> 27
, adx_3(29) -> 34
, adx_3(36) -> 33
, adx_4(37) -> 42
, adx_4(40) -> 33
, adx_4(41) -> 43
, adx_5(46) -> 44
, adx_5(47) -> 50
, adx_6(49) -> 63
, adx_6(54) -> 51
, adx_6(55) -> 56
, adx_6(59) -> 78
, adx_7(59) -> 71
, adx_7(64) -> 65
, adx_7(68) -> 66
, adx_7(75) -> 74
, adx_7(83) -> 86
, adx_7(107) -> 103
, adx_8(82) -> 81
, adx_8(111) -> 110
, adx_8(112) -> 114
, nats_0() -> 8
, nats_1() -> 25
, zeros_0() -> 9
, zeros_1() -> 17
, zeros_2() -> 29
, zeros_3() -> 37
, zeros_4() -> 49
, zeros_5() -> 59
, zeros_6() -> 83
, zeros_7() -> 112
, 0_0() -> 10
, 0_1() -> 18
, 0_2() -> 30
, 0_3() -> 38
, 0_4() -> 48
, 0_5() -> 60
, 0_6() -> 84
, 0_7() -> 108
, head_0(3) -> 11
, head_0(4) -> 11
, head_0(8) -> 11
, head_0(9) -> 11
, head_0(10) -> 11
, head_0(14) -> 11
, head_1(3) -> 23
, head_1(4) -> 23
, head_1(8) -> 23
, head_1(9) -> 23
, head_1(10) -> 23
, head_1(14) -> 23
, tail_0(3) -> 12
, tail_0(4) -> 12
, tail_0(8) -> 12
, tail_0(9) -> 12
, tail_0(10) -> 12
, tail_0(14) -> 12
, tail_1(3) -> 24
, tail_1(4) -> 24
, tail_1(8) -> 24
, tail_1(9) -> 24
, tail_1(10) -> 24
, tail_1(14) -> 24
, proper_0(3) -> 13
, proper_0(4) -> 13
, proper_0(8) -> 13
, proper_0(9) -> 13
, proper_0(10) -> 13
, proper_0(14) -> 13
, proper_1(3) -> 26
, proper_1(4) -> 26
, proper_1(8) -> 26
, proper_1(9) -> 26
, proper_1(10) -> 26
, proper_1(14) -> 26
, proper_2(16) -> 27
, proper_2(17) -> 32
, proper_2(18) -> 31
, proper_3(28) -> 33
, proper_3(29) -> 36
, proper_3(30) -> 35
, proper_4(37) -> 53
, proper_4(38) -> 52
, proper_4(43) -> 44
, proper_5(41) -> 46
, proper_5(48) -> 57
, proper_5(49) -> 58
, proper_5(50) -> 51
, proper_6(47) -> 54
, proper_6(61) -> 66
, proper_7(48) -> 73
, proper_7(49) -> 75
, proper_7(59) -> 107
, proper_7(62) -> 72
, proper_7(63) -> 74
, proper_7(69) -> 76
, proper_8(59) -> 82
, proper_8(60) -> 80
, proper_8(70) -> 79
, proper_8(71) -> 81
, proper_8(78) -> 103
, proper_8(83) -> 111
, proper_8(89) -> 93
, proper_8(90) -> 99
, proper_8(91) -> 100
, proper_9(84) -> 106
, proper_9(86) -> 110
, proper_9(95) -> 101
, proper_9(96) -> 104
, proper_9(97) -> 105
, ok_0(3) -> 14
, ok_0(4) -> 14
, ok_0(8) -> 14
, ok_0(9) -> 14
, ok_0(10) -> 14
, ok_0(14) -> 14
, ok_1(17) -> 13
, ok_1(17) -> 26
, ok_1(18) -> 13
, ok_1(18) -> 26
, ok_1(19) -> 2
, ok_1(19) -> 19
, ok_1(20) -> 5
, ok_1(20) -> 20
, ok_1(21) -> 6
, ok_1(21) -> 21
, ok_1(22) -> 7
, ok_1(22) -> 22
, ok_1(23) -> 11
, ok_1(23) -> 23
, ok_1(24) -> 12
, ok_1(24) -> 24
, ok_1(25) -> 13
, ok_1(25) -> 26
, ok_2(29) -> 32
, ok_2(30) -> 31
, ok_3(34) -> 27
, ok_3(37) -> 36
, ok_3(38) -> 35
, ok_4(42) -> 33
, ok_4(48) -> 52
, ok_4(49) -> 53
, ok_5(55) -> 46
, ok_5(59) -> 58
, ok_5(59) -> 75
, ok_5(60) -> 57
, ok_5(60) -> 73
, ok_6(56) -> 44
, ok_6(64) -> 54
, ok_6(78) -> 74
, ok_6(83) -> 82
, ok_6(83) -> 107
, ok_6(84) -> 80
, ok_6(85) -> 72
, ok_7(65) -> 51
, ok_7(86) -> 81
, ok_7(86) -> 103
, ok_7(87) -> 66
, ok_7(88) -> 79
, ok_7(102) -> 99
, ok_7(108) -> 106
, ok_7(112) -> 111
, ok_8(92) -> 76
, ok_8(97) -> 100
, ok_8(109) -> 104
, ok_8(113) -> 93
, ok_8(114) -> 110
, ok_9(116) -> 105
, ok_9(117) -> 101
, top_0(3) -> 15
, top_0(4) -> 15
, top_0(8) -> 15
, top_0(9) -> 15
, top_0(10) -> 15
, top_0(14) -> 15
, top_1(26) -> 15
, top_2(27) -> 15
, top_3(33) -> 15
, top_4(44) -> 15
, top_5(51) -> 15
, top_6(66) -> 15
, top_7(76) -> 15
, top_8(93) -> 15
, top_9(101) -> 15
, top_10(118) -> 15 }

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