YES(?,O(n^1))

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

Strict Trs:
  { active(nats()) -> mark(cons(0(), incr(nats())))
  , active(cons(X1, X2)) -> cons(active(X1), X2)
  , active(incr(X)) -> incr(active(X))
  , active(incr(cons(X, XS))) -> mark(cons(s(X), incr(XS)))
  , active(pairs()) -> mark(cons(0(), incr(odds())))
  , active(odds()) -> mark(incr(pairs()))
  , active(s(X)) -> s(active(X))
  , active(head(X)) -> head(active(X))
  , active(head(cons(X, XS))) -> mark(X)
  , active(tail(X)) -> tail(active(X))
  , active(tail(cons(X, XS))) -> mark(XS)
  , cons(mark(X1), X2) -> mark(cons(X1, X2))
  , cons(ok(X1), ok(X2)) -> ok(cons(X1, X2))
  , incr(mark(X)) -> mark(incr(X))
  , incr(ok(X)) -> ok(incr(X))
  , s(mark(X)) -> mark(s(X))
  , s(ok(X)) -> ok(s(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(nats()) -> ok(nats())
  , proper(cons(X1, X2)) -> cons(proper(X1), proper(X2))
  , proper(0()) -> ok(0())
  , proper(incr(X)) -> incr(proper(X))
  , proper(pairs()) -> ok(pairs())
  , proper(odds()) -> ok(odds())
  , proper(s(X)) -> s(proper(X))
  , 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 9. 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(8) -> 1
, active_0(13) -> 1
, active_1(2) -> 25
, active_1(3) -> 25
, active_1(5) -> 25
, active_1(7) -> 25
, active_1(8) -> 25
, active_1(13) -> 25
, active_2(16) -> 26
, active_2(18) -> 26
, active_2(19) -> 26
, active_3(38) -> 36
, active_4(28) -> 53
, active_4(31) -> 46
, active_4(50) -> 52
, active_5(41) -> 61
, active_5(44) -> 54
, active_5(74) -> 60
, active_6(56) -> 81
, active_6(72) -> 65
, active_6(79) -> 80
, active_7(69) -> 91
, active_7(78) -> 82
, active_7(103) -> 90
, active_8(97) -> 105
, active_8(98) -> 109
, active_8(106) -> 107
, active_9(102) -> 108
, nats_0() -> 2
, nats_1() -> 18
, nats_2() -> 30
, nats_3() -> 45
, nats_4() -> 58
, nats_5() -> 71
, nats_6() -> 100
, mark_0(2) -> 3
, mark_0(3) -> 3
, mark_0(5) -> 3
, mark_0(7) -> 3
, mark_0(8) -> 3
, mark_0(13) -> 3
, mark_1(15) -> 1
, mark_1(15) -> 25
, mark_1(20) -> 4
, mark_1(20) -> 20
, mark_1(21) -> 6
, mark_1(21) -> 21
, mark_1(22) -> 9
, mark_1(22) -> 22
, mark_1(23) -> 10
, mark_1(23) -> 23
, mark_1(24) -> 11
, mark_1(24) -> 24
, mark_2(27) -> 26
, mark_3(47) -> 46
, mark_4(49) -> 36
, mark_4(55) -> 54
, mark_5(59) -> 52
, mark_6(75) -> 60
, mark_7(83) -> 80
, cons_0(2, 2) -> 4
, cons_0(2, 3) -> 4
, cons_0(2, 5) -> 4
, cons_0(2, 7) -> 4
, cons_0(2, 8) -> 4
, cons_0(2, 13) -> 4
, cons_0(3, 2) -> 4
, cons_0(3, 3) -> 4
, cons_0(3, 5) -> 4
, cons_0(3, 7) -> 4
, cons_0(3, 8) -> 4
, cons_0(3, 13) -> 4
, cons_0(5, 2) -> 4
, cons_0(5, 3) -> 4
, cons_0(5, 5) -> 4
, cons_0(5, 7) -> 4
, cons_0(5, 8) -> 4
, cons_0(5, 13) -> 4
, cons_0(7, 2) -> 4
, cons_0(7, 3) -> 4
, cons_0(7, 5) -> 4
, cons_0(7, 7) -> 4
, cons_0(7, 8) -> 4
, cons_0(7, 13) -> 4
, cons_0(8, 2) -> 4
, cons_0(8, 3) -> 4
, cons_0(8, 5) -> 4
, cons_0(8, 7) -> 4
, cons_0(8, 8) -> 4
, cons_0(8, 13) -> 4
, cons_0(13, 2) -> 4
, cons_0(13, 3) -> 4
, cons_0(13, 5) -> 4
, cons_0(13, 7) -> 4
, cons_0(13, 8) -> 4
, cons_0(13, 13) -> 4
, cons_1(2, 2) -> 20
, cons_1(2, 3) -> 20
, cons_1(2, 5) -> 20
, cons_1(2, 7) -> 20
, cons_1(2, 8) -> 20
, cons_1(2, 13) -> 20
, cons_1(3, 2) -> 20
, cons_1(3, 3) -> 20
, cons_1(3, 5) -> 20
, cons_1(3, 7) -> 20
, cons_1(3, 8) -> 20
, cons_1(3, 13) -> 20
, cons_1(5, 2) -> 20
, cons_1(5, 3) -> 20
, cons_1(5, 5) -> 20
, cons_1(5, 7) -> 20
, cons_1(5, 8) -> 20
, cons_1(5, 13) -> 20
, cons_1(7, 2) -> 20
, cons_1(7, 3) -> 20
, cons_1(7, 5) -> 20
, cons_1(7, 7) -> 20
, cons_1(7, 8) -> 20
, cons_1(7, 13) -> 20
, cons_1(8, 2) -> 20
, cons_1(8, 3) -> 20
, cons_1(8, 5) -> 20
, cons_1(8, 7) -> 20
, cons_1(8, 8) -> 20
, cons_1(8, 13) -> 20
, cons_1(13, 2) -> 20
, cons_1(13, 3) -> 20
, cons_1(13, 5) -> 20
, cons_1(13, 7) -> 20
, cons_1(13, 8) -> 20
, cons_1(13, 13) -> 20
, cons_1(16, 17) -> 15
, cons_2(28, 29) -> 27
, cons_2(32, 33) -> 26
, cons_3(28, 37) -> 38
, cons_3(39, 40) -> 36
, cons_3(41, 48) -> 47
, cons_4(41, 51) -> 50
, cons_4(53, 37) -> 36
, cons_4(56, 57) -> 55
, cons_4(62, 63) -> 54
, cons_5(56, 66) -> 72
, cons_5(61, 51) -> 52
, cons_5(67, 68) -> 65
, cons_6(69, 73) -> 78
, cons_6(76, 77) -> 75
, cons_6(81, 66) -> 65
, cons_7(84, 85) -> 83
, cons_7(86, 87) -> 80
, cons_7(91, 73) -> 82
, cons_7(97, 85) -> 103
, cons_8(92, 93) -> 90
, cons_8(102, 104) -> 106
, cons_8(105, 85) -> 90
, cons_9(108, 104) -> 107
, 0_0() -> 5
, 0_1() -> 16
, 0_2() -> 28
, 0_3() -> 41
, 0_4() -> 56
, 0_5() -> 69
, 0_6() -> 98
, incr_0(2) -> 6
, incr_0(3) -> 6
, incr_0(5) -> 6
, incr_0(7) -> 6
, incr_0(8) -> 6
, incr_0(13) -> 6
, incr_1(2) -> 21
, incr_1(3) -> 21
, incr_1(5) -> 21
, incr_1(7) -> 21
, incr_1(8) -> 21
, incr_1(13) -> 21
, incr_1(18) -> 17
, incr_1(19) -> 15
, incr_2(30) -> 29
, incr_2(31) -> 27
, incr_2(34) -> 33
, incr_2(35) -> 26
, incr_3(30) -> 37
, incr_3(31) -> 38
, incr_3(42) -> 40
, incr_3(43) -> 36
, incr_3(45) -> 48
, incr_4(44) -> 50
, incr_4(45) -> 51
, incr_4(46) -> 36
, incr_4(47) -> 49
, incr_4(58) -> 57
, incr_4(64) -> 63
, incr_5(54) -> 52
, incr_5(55) -> 59
, incr_5(58) -> 66
, incr_5(70) -> 68
, incr_6(65) -> 60
, incr_6(66) -> 77
, incr_6(71) -> 73
, incr_6(72) -> 74
, incr_6(94) -> 88
, incr_7(73) -> 85
, incr_7(78) -> 79
, incr_7(82) -> 80
, incr_7(88) -> 87
, incr_7(99) -> 95
, incr_7(100) -> 101
, incr_8(95) -> 93
, incr_8(101) -> 104
, pairs_0() -> 7
, pairs_1() -> 19
, pairs_2() -> 31
, pairs_3() -> 44
, odds_0() -> 8
, odds_1() -> 18
, odds_2() -> 30
, odds_3() -> 45
, odds_4() -> 58
, odds_5() -> 71
, odds_6() -> 100
, s_0(2) -> 9
, s_0(3) -> 9
, s_0(5) -> 9
, s_0(7) -> 9
, s_0(8) -> 9
, s_0(13) -> 9
, s_1(2) -> 22
, s_1(3) -> 22
, s_1(5) -> 22
, s_1(7) -> 22
, s_1(8) -> 22
, s_1(13) -> 22
, s_6(56) -> 76
, s_6(69) -> 97
, s_7(69) -> 84
, s_7(89) -> 86
, s_7(91) -> 105
, s_7(98) -> 102
, s_8(96) -> 92
, s_8(109) -> 108
, head_0(2) -> 10
, head_0(3) -> 10
, head_0(5) -> 10
, head_0(7) -> 10
, head_0(8) -> 10
, head_0(13) -> 10
, head_1(2) -> 23
, head_1(3) -> 23
, head_1(5) -> 23
, head_1(7) -> 23
, head_1(8) -> 23
, head_1(13) -> 23
, tail_0(2) -> 11
, tail_0(3) -> 11
, tail_0(5) -> 11
, tail_0(7) -> 11
, tail_0(8) -> 11
, tail_0(13) -> 11
, tail_1(2) -> 24
, tail_1(3) -> 24
, tail_1(5) -> 24
, tail_1(7) -> 24
, tail_1(8) -> 24
, tail_1(13) -> 24
, proper_0(2) -> 12
, proper_0(3) -> 12
, proper_0(5) -> 12
, proper_0(7) -> 12
, proper_0(8) -> 12
, proper_0(13) -> 12
, proper_1(2) -> 25
, proper_1(3) -> 25
, proper_1(5) -> 25
, proper_1(7) -> 25
, proper_1(8) -> 25
, proper_1(13) -> 25
, proper_2(15) -> 26
, proper_2(16) -> 32
, proper_2(17) -> 33
, proper_2(18) -> 34
, proper_2(19) -> 35
, proper_3(27) -> 36
, proper_3(28) -> 39
, proper_3(29) -> 40
, proper_3(30) -> 42
, proper_3(31) -> 43
, proper_4(41) -> 62
, proper_4(45) -> 64
, proper_4(48) -> 63
, proper_4(49) -> 52
, proper_5(47) -> 54
, proper_5(56) -> 67
, proper_5(57) -> 68
, proper_5(58) -> 70
, proper_5(59) -> 60
, proper_6(55) -> 65
, proper_6(58) -> 94
, proper_6(75) -> 80
, proper_7(56) -> 89
, proper_7(66) -> 88
, proper_7(71) -> 99
, proper_7(76) -> 86
, proper_7(77) -> 87
, proper_7(83) -> 90
, proper_8(69) -> 96
, proper_8(73) -> 95
, proper_8(84) -> 92
, proper_8(85) -> 93
, ok_0(2) -> 13
, ok_0(3) -> 13
, ok_0(5) -> 13
, ok_0(7) -> 13
, ok_0(8) -> 13
, ok_0(13) -> 13
, ok_1(16) -> 12
, ok_1(16) -> 25
, ok_1(18) -> 12
, ok_1(18) -> 25
, ok_1(19) -> 12
, ok_1(19) -> 25
, ok_1(20) -> 4
, ok_1(20) -> 20
, ok_1(21) -> 6
, ok_1(21) -> 21
, ok_1(22) -> 9
, ok_1(22) -> 22
, ok_1(23) -> 10
, ok_1(23) -> 23
, ok_1(24) -> 11
, ok_1(24) -> 24
, ok_2(28) -> 32
, ok_2(30) -> 34
, ok_2(31) -> 35
, ok_3(37) -> 33
, ok_3(38) -> 26
, ok_3(41) -> 39
, ok_3(44) -> 43
, ok_3(45) -> 42
, ok_4(50) -> 36
, ok_4(51) -> 40
, ok_4(56) -> 62
, ok_4(58) -> 64
, ok_5(66) -> 63
, ok_5(69) -> 67
, ok_5(69) -> 89
, ok_5(71) -> 70
, ok_5(71) -> 94
, ok_5(72) -> 54
, ok_6(73) -> 68
, ok_6(73) -> 88
, ok_6(74) -> 52
, ok_6(78) -> 65
, ok_6(97) -> 86
, ok_6(98) -> 96
, ok_6(100) -> 99
, ok_7(79) -> 60
, ok_7(85) -> 87
, ok_7(101) -> 95
, ok_7(102) -> 92
, ok_7(103) -> 80
, ok_8(104) -> 93
, ok_8(106) -> 90
, top_0(2) -> 14
, top_0(3) -> 14
, top_0(5) -> 14
, top_0(7) -> 14
, top_0(8) -> 14
, top_0(13) -> 14
, top_1(25) -> 14
, top_2(26) -> 14
, top_3(36) -> 14
, top_4(52) -> 14
, top_5(60) -> 14
, top_6(80) -> 14
, top_7(90) -> 14
, top_8(107) -> 14 }

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