*** 1 Progress [(O(1),O(n^1))]  ***
    Considered Problem:
      Strict DP Rules:
        
      Strict TRS Rules:
        active(adx(X)) -> adx(active(X))
        active(adx(cons(X,L))) -> mark(incr(cons(X,adx(L))))
        active(adx(nil())) -> mark(nil())
        active(cons(X1,X2)) -> cons(active(X1),X2)
        active(head(X)) -> head(active(X))
        active(head(cons(X,L))) -> mark(X)
        active(incr(X)) -> incr(active(X))
        active(incr(cons(X,L))) -> mark(cons(s(X),incr(L)))
        active(incr(nil())) -> mark(nil())
        active(nats()) -> mark(adx(zeros()))
        active(s(X)) -> s(active(X))
        active(tail(X)) -> tail(active(X))
        active(tail(cons(X,L))) -> mark(L)
        active(zeros()) -> mark(cons(0(),zeros()))
        adx(mark(X)) -> mark(adx(X))
        adx(ok(X)) -> ok(adx(X))
        cons(mark(X1),X2) -> mark(cons(X1,X2))
        cons(ok(X1),ok(X2)) -> ok(cons(X1,X2))
        head(mark(X)) -> mark(head(X))
        head(ok(X)) -> ok(head(X))
        incr(mark(X)) -> mark(incr(X))
        incr(ok(X)) -> ok(incr(X))
        proper(0()) -> ok(0())
        proper(adx(X)) -> adx(proper(X))
        proper(cons(X1,X2)) -> cons(proper(X1),proper(X2))
        proper(head(X)) -> head(proper(X))
        proper(incr(X)) -> incr(proper(X))
        proper(nats()) -> ok(nats())
        proper(nil()) -> ok(nil())
        proper(s(X)) -> s(proper(X))
        proper(tail(X)) -> tail(proper(X))
        proper(zeros()) -> ok(zeros())
        s(mark(X)) -> mark(s(X))
        s(ok(X)) -> ok(s(X))
        tail(mark(X)) -> mark(tail(X))
        tail(ok(X)) -> ok(tail(X))
        top(mark(X)) -> top(proper(X))
        top(ok(X)) -> top(active(X))
      Weak DP Rules:
        
      Weak TRS Rules:
        
      Signature:
        {active/1,adx/1,cons/2,head/1,incr/1,proper/1,s/1,tail/1,top/1} / {0/0,mark/1,nats/0,nil/0,ok/1,zeros/0}
      Obligation:
        Innermost
        basic terms: {active,adx,cons,head,incr,proper,s,tail,top}/{0,mark,nats,nil,ok,zeros}
    Applied Processor:
      Bounds {initialAutomaton = perSymbol, enrichment = match}
    Proof:
      The problem is match-bounded by 10.
      The enriched problem is compatible with follwoing automaton.
        0_0() -> 1
        0_1() -> 18
        0_2() -> 29
        0_3() -> 42
        0_4() -> 48
        0_5() -> 64
        0_6() -> 93
        0_7() -> 132
        0_8() -> 160
        active_0(1) -> 2
        active_0(7) -> 2
        active_0(8) -> 2
        active_0(9) -> 2
        active_0(10) -> 2
        active_0(15) -> 2
        active_1(1) -> 25
        active_1(7) -> 25
        active_1(8) -> 25
        active_1(9) -> 25
        active_1(10) -> 25
        active_1(15) -> 25
        active_2(17) -> 26
        active_2(18) -> 26
        active_3(34) -> 33
        active_4(28) -> 38
        active_4(29) -> 39
        active_4(32) -> 39
        active_4(44) -> 45
        active_5(37) -> 46
        active_5(42) -> 56
        active_5(61) -> 65
        active_5(62) -> 55
        active_5(66) -> 55
        active_6(48) -> 72
        active_6(49) -> 68
        active_6(63) -> 57
        active_6(75) -> 76
        active_6(106) -> 111
        active_6(107) -> 76
        active_7(64) -> 81
        active_7(67) -> 77
        active_7(99) -> 121
        active_7(100) -> 85
        active_7(144) -> 149
        active_7(148) -> 85
        active_8(93) -> 123
        active_8(98) -> 91
        active_8(109) -> 110
        active_8(142) -> 150
        active_8(166) -> 168
        active_8(167) -> 110
        active_9(108) -> 112
        active_9(119) -> 141
        active_9(132) -> 147
        active_9(139) -> 120
        active_9(163) -> 169
        active_10(137) -> 146
        active_10(143) -> 145
        active_10(160) -> 170
        adx_0(1) -> 3
        adx_0(7) -> 3
        adx_0(8) -> 3
        adx_0(9) -> 3
        adx_0(10) -> 3
        adx_0(15) -> 3
        adx_1(1) -> 19
        adx_1(7) -> 19
        adx_1(8) -> 19
        adx_1(9) -> 19
        adx_1(10) -> 19
        adx_1(15) -> 19
        adx_1(17) -> 16
        adx_2(28) -> 27
        adx_2(30) -> 26
        adx_3(28) -> 34
        adx_3(35) -> 33
        adx_3(37) -> 40
        adx_4(37) -> 44
        adx_4(38) -> 33
        adx_4(41) -> 43
        adx_4(52) -> 53
        adx_5(46) -> 45
        adx_5(47) -> 50
        adx_5(49) -> 61
        adx_6(49) -> 71
        adx_6(57) -> 55
        adx_6(60) -> 97
        adx_6(63) -> 66
        adx_6(68) -> 65
        adx_6(73) -> 74
        adx_7(60) -> 80
        adx_7(67) -> 75
        adx_7(77) -> 76
        adx_7(86) -> 82
        adx_7(92) -> 105
        adx_7(94) -> 90
        adx_7(121) -> 111
        adx_7(124) -> 118
        adx_8(99) -> 106
        adx_8(101) -> 96
        adx_8(133) -> 130
        adx_8(133) -> 135
        adx_8(136) -> 138
        adx_9(161) -> 158
        adx_9(162) -> 164
        cons_0(1,1) -> 4
        cons_0(1,7) -> 4
        cons_0(1,8) -> 4
        cons_0(1,9) -> 4
        cons_0(1,10) -> 4
        cons_0(1,15) -> 4
        cons_0(7,1) -> 4
        cons_0(7,7) -> 4
        cons_0(7,8) -> 4
        cons_0(7,9) -> 4
        cons_0(7,10) -> 4
        cons_0(7,15) -> 4
        cons_0(8,1) -> 4
        cons_0(8,7) -> 4
        cons_0(8,8) -> 4
        cons_0(8,9) -> 4
        cons_0(8,10) -> 4
        cons_0(8,15) -> 4
        cons_0(9,1) -> 4
        cons_0(9,7) -> 4
        cons_0(9,8) -> 4
        cons_0(9,9) -> 4
        cons_0(9,10) -> 4
        cons_0(9,15) -> 4
        cons_0(10,1) -> 4
        cons_0(10,7) -> 4
        cons_0(10,8) -> 4
        cons_0(10,9) -> 4
        cons_0(10,10) -> 4
        cons_0(10,15) -> 4
        cons_0(15,1) -> 4
        cons_0(15,7) -> 4
        cons_0(15,8) -> 4
        cons_0(15,9) -> 4
        cons_0(15,10) -> 4
        cons_0(15,15) -> 4
        cons_1(1,1) -> 20
        cons_1(1,7) -> 20
        cons_1(1,8) -> 20
        cons_1(1,9) -> 20
        cons_1(1,10) -> 20
        cons_1(1,15) -> 20
        cons_1(7,1) -> 20
        cons_1(7,7) -> 20
        cons_1(7,8) -> 20
        cons_1(7,9) -> 20
        cons_1(7,10) -> 20
        cons_1(7,15) -> 20
        cons_1(8,1) -> 20
        cons_1(8,7) -> 20
        cons_1(8,8) -> 20
        cons_1(8,9) -> 20
        cons_1(8,10) -> 20
        cons_1(8,15) -> 20
        cons_1(9,1) -> 20
        cons_1(9,7) -> 20
        cons_1(9,8) -> 20
        cons_1(9,9) -> 20
        cons_1(9,10) -> 20
        cons_1(9,15) -> 20
        cons_1(10,1) -> 20
        cons_1(10,7) -> 20
        cons_1(10,8) -> 20
        cons_1(10,9) -> 20
        cons_1(10,10) -> 20
        cons_1(10,15) -> 20
        cons_1(15,1) -> 20
        cons_1(15,7) -> 20
        cons_1(15,8) -> 20
        cons_1(15,9) -> 20
        cons_1(15,10) -> 20
        cons_1(15,15) -> 20
        cons_1(18,17) -> 16
        cons_2(29,28) -> 27
        cons_2(31,30) -> 26
        cons_3(29,28) -> 34
        cons_3(32,28) -> 34
        cons_3(36,35) -> 33
        cons_3(42,37) -> 41
        cons_4(39,28) -> 33
        cons_4(40,28) -> 43
        cons_4(42,37) -> 44
        cons_4(48,49) -> 47
        cons_4(51,52) -> 46
        cons_4(61,37) -> 62
        cons_5(48,49) -> 63
        cons_5(53,54) -> 45
        cons_5(56,37) -> 45
        cons_5(58,59) -> 57
        cons_5(64,60) -> 73
        cons_5(65,37) -> 55
        cons_5(106,49) -> 107
        cons_6(48,71) -> 70
        cons_6(64,60) -> 67
        cons_6(64,97) -> 98
        cons_6(72,49) -> 57
        cons_6(74,37) -> 69
        cons_6(87,88) -> 86
        cons_6(111,49) -> 76
        cons_6(144,60) -> 148
        cons_7(64,80) -> 79
        cons_7(81,60) -> 77
        cons_7(81,97) -> 91
        cons_7(82,83) -> 76
        cons_7(89,90) -> 84
        cons_7(93,92) -> 99
        cons_7(93,105) -> 108
        cons_7(103,104) -> 102
        cons_7(122,49) -> 78
        cons_7(149,60) -> 85
        cons_7(166,92) -> 167
        cons_8(95,96) -> 91
        cons_8(114,115) -> 113
        cons_8(116,117) -> 110
        cons_8(119,115) -> 139
        cons_8(123,92) -> 121
        cons_8(123,105) -> 112
        cons_8(125,126) -> 85
        cons_8(132,138) -> 142
        cons_8(134,135) -> 129
        cons_8(137,152) -> 151
        cons_8(151,60) -> 153
        cons_8(168,92) -> 110
        cons_9(127,128) -> 120
        cons_9(137,140) -> 143
        cons_9(141,115) -> 120
        cons_9(147,138) -> 150
        cons_9(154,155) -> 110
        cons_9(156,157) -> 154
        cons_9(169,165) -> 168
        cons_10(146,140) -> 145
        cons_10(163,165) -> 166
        head_0(1) -> 5
        head_0(7) -> 5
        head_0(8) -> 5
        head_0(9) -> 5
        head_0(10) -> 5
        head_0(15) -> 5
        head_1(1) -> 21
        head_1(7) -> 21
        head_1(8) -> 21
        head_1(9) -> 21
        head_1(10) -> 21
        head_1(15) -> 21
        incr_0(1) -> 6
        incr_0(7) -> 6
        incr_0(8) -> 6
        incr_0(9) -> 6
        incr_0(10) -> 6
        incr_0(15) -> 6
        incr_1(1) -> 22
        incr_1(7) -> 22
        incr_1(8) -> 22
        incr_1(9) -> 22
        incr_1(10) -> 22
        incr_1(15) -> 22
        incr_6(70) -> 69
        incr_7(79) -> 78
        incr_7(84) -> 76
        incr_7(97) -> 104
        incr_7(98) -> 100
        incr_7(108) -> 122
        incr_8(91) -> 85
        incr_8(105) -> 115
        incr_8(108) -> 109
        incr_8(118) -> 117
        incr_8(129) -> 125
        incr_8(138) -> 152
        incr_8(150) -> 149
        incr_9(112) -> 110
        incr_9(130) -> 128
        incr_9(138) -> 140
        incr_9(142) -> 144
        incr_9(158) -> 157
        incr_10(164) -> 165
        mark_0(1) -> 7
        mark_0(7) -> 7
        mark_0(8) -> 7
        mark_0(9) -> 7
        mark_0(10) -> 7
        mark_0(15) -> 7
        mark_1(16) -> 2
        mark_1(16) -> 25
        mark_1(19) -> 3
        mark_1(19) -> 19
        mark_1(20) -> 4
        mark_1(20) -> 20
        mark_1(21) -> 5
        mark_1(21) -> 21
        mark_1(22) -> 6
        mark_1(22) -> 22
        mark_1(23) -> 12
        mark_1(23) -> 23
        mark_1(24) -> 13
        mark_1(24) -> 24
        mark_2(27) -> 26
        mark_3(40) -> 39
        mark_3(41) -> 38
        mark_4(43) -> 33
        mark_4(47) -> 46
        mark_5(50) -> 45
        mark_5(73) -> 68
        mark_6(69) -> 55
        mark_6(74) -> 65
        mark_7(78) -> 76
        mark_7(102) -> 85
        mark_7(122) -> 111
        mark_8(113) -> 110
        mark_8(151) -> 149
        mark_8(153) -> 85
        nats_0() -> 8
        nats_1() -> 18
        nats_2() -> 32
        nil_0() -> 9
        nil_1() -> 18
        nil_2() -> 32
        ok_0(1) -> 10
        ok_0(7) -> 10
        ok_0(8) -> 10
        ok_0(9) -> 10
        ok_0(10) -> 10
        ok_0(15) -> 10
        ok_1(17) -> 11
        ok_1(17) -> 25
        ok_1(18) -> 11
        ok_1(18) -> 25
        ok_1(19) -> 3
        ok_1(19) -> 19
        ok_1(20) -> 4
        ok_1(20) -> 20
        ok_1(21) -> 5
        ok_1(21) -> 21
        ok_1(22) -> 6
        ok_1(22) -> 22
        ok_1(23) -> 12
        ok_1(23) -> 23
        ok_1(24) -> 13
        ok_1(24) -> 24
        ok_2(28) -> 30
        ok_2(29) -> 31
        ok_2(32) -> 31
        ok_3(34) -> 26
        ok_3(37) -> 35
        ok_3(37) -> 54
        ok_3(42) -> 36
        ok_4(44) -> 33
        ok_4(48) -> 51
        ok_4(49) -> 52
        ok_4(49) -> 83
        ok_4(62) -> 45
        ok_5(60) -> 59
        ok_5(60) -> 94
        ok_5(60) -> 126
        ok_5(61) -> 53
        ok_5(63) -> 46
        ok_5(64) -> 58
        ok_5(64) -> 89
        ok_5(107) -> 76
        ok_6(66) -> 45
        ok_6(67) -> 57
        ok_6(92) -> 88
        ok_6(92) -> 101
        ok_6(92) -> 124
        ok_6(92) -> 155
        ok_6(93) -> 87
        ok_6(93) -> 95
        ok_6(97) -> 90
        ok_6(98) -> 84
        ok_6(148) -> 85
        ok_7(75) -> 55
        ok_7(99) -> 86
        ok_7(100) -> 76
        ok_7(105) -> 96
        ok_7(105) -> 118
        ok_7(108) -> 91
        ok_7(119) -> 116
        ok_7(132) -> 131
        ok_7(132) -> 134
        ok_7(136) -> 133
        ok_7(167) -> 110
        ok_8(106) -> 82
        ok_8(109) -> 85
        ok_8(115) -> 117
        ok_8(137) -> 127
        ok_8(138) -> 130
        ok_8(138) -> 135
        ok_8(139) -> 110
        ok_8(142) -> 129
        ok_8(160) -> 159
        ok_8(162) -> 161
        ok_9(140) -> 128
        ok_9(143) -> 120
        ok_9(144) -> 125
        ok_9(163) -> 156
        ok_9(164) -> 158
        ok_10(165) -> 157
        ok_10(166) -> 154
        proper_0(1) -> 11
        proper_0(7) -> 11
        proper_0(8) -> 11
        proper_0(9) -> 11
        proper_0(10) -> 11
        proper_0(15) -> 11
        proper_1(1) -> 25
        proper_1(7) -> 25
        proper_1(8) -> 25
        proper_1(9) -> 25
        proper_1(10) -> 25
        proper_1(15) -> 25
        proper_2(16) -> 26
        proper_2(17) -> 30
        proper_2(18) -> 31
        proper_3(27) -> 33
        proper_3(28) -> 35
        proper_3(29) -> 36
        proper_4(37) -> 52
        proper_4(42) -> 51
        proper_4(43) -> 45
        proper_5(28) -> 54
        proper_5(40) -> 53
        proper_5(41) -> 46
        proper_5(48) -> 58
        proper_5(49) -> 59
        proper_5(50) -> 55
        proper_6(47) -> 57
        proper_6(60) -> 88
        proper_6(64) -> 87
        proper_6(69) -> 76
        proper_7(37) -> 83
        proper_7(48) -> 89
        proper_7(49) -> 94
        proper_7(60) -> 124
        proper_7(70) -> 84
        proper_7(71) -> 90
        proper_7(73) -> 86
        proper_7(74) -> 82
        proper_7(78) -> 85
        proper_8(49) -> 126
        proper_8(60) -> 101
        proper_8(64) -> 95
        proper_8(79) -> 91
        proper_8(80) -> 96
        proper_8(92) -> 133
        proper_8(93) -> 134
        proper_8(97) -> 118
        proper_8(102) -> 110
        proper_8(103) -> 116
        proper_8(104) -> 117
        proper_8(105) -> 135
        proper_8(108) -> 129
        proper_8(122) -> 125
        proper_8(153) -> 110
        proper_9(60) -> 155
        proper_9(93) -> 131
        proper_9(105) -> 130
        proper_9(113) -> 120
        proper_9(114) -> 127
        proper_9(115) -> 128
        proper_9(132) -> 159
        proper_9(136) -> 161
        proper_9(137) -> 156
        proper_9(138) -> 158
        proper_9(151) -> 154
        proper_9(152) -> 157
        s_0(1) -> 12
        s_0(7) -> 12
        s_0(8) -> 12
        s_0(9) -> 12
        s_0(10) -> 12
        s_0(15) -> 12
        s_1(1) -> 23
        s_1(7) -> 23
        s_1(8) -> 23
        s_1(9) -> 23
        s_1(10) -> 23
        s_1(15) -> 23
        s_7(64) -> 103
        s_7(93) -> 119
        s_8(93) -> 114
        s_8(95) -> 116
        s_8(123) -> 141
        s_8(132) -> 137
        s_9(131) -> 127
        s_9(147) -> 146
        s_9(159) -> 156
        s_9(160) -> 163
        s_10(170) -> 169
        tail_0(1) -> 13
        tail_0(7) -> 13
        tail_0(8) -> 13
        tail_0(9) -> 13
        tail_0(10) -> 13
        tail_0(15) -> 13
        tail_1(1) -> 24
        tail_1(7) -> 24
        tail_1(8) -> 24
        tail_1(9) -> 24
        tail_1(10) -> 24
        tail_1(15) -> 24
        top_0(1) -> 14
        top_0(7) -> 14
        top_0(8) -> 14
        top_0(9) -> 14
        top_0(10) -> 14
        top_0(15) -> 14
        top_1(25) -> 14
        top_2(26) -> 14
        top_3(33) -> 14
        top_4(45) -> 14
        top_5(55) -> 14
        top_6(76) -> 14
        top_7(85) -> 14
        top_8(110) -> 14
        top_9(120) -> 14
        top_10(145) -> 14
        zeros_0() -> 15
        zeros_1() -> 17
        zeros_2() -> 28
        zeros_3() -> 37
        zeros_4() -> 49
        zeros_5() -> 60
        zeros_6() -> 92
        zeros_7() -> 136
        zeros_8() -> 162
*** 1.1 Progress [(O(1),O(1))]  ***
    Considered Problem:
      Strict DP Rules:
        
      Strict TRS Rules:
        
      Weak DP Rules:
        
      Weak TRS Rules:
        active(adx(X)) -> adx(active(X))
        active(adx(cons(X,L))) -> mark(incr(cons(X,adx(L))))
        active(adx(nil())) -> mark(nil())
        active(cons(X1,X2)) -> cons(active(X1),X2)
        active(head(X)) -> head(active(X))
        active(head(cons(X,L))) -> mark(X)
        active(incr(X)) -> incr(active(X))
        active(incr(cons(X,L))) -> mark(cons(s(X),incr(L)))
        active(incr(nil())) -> mark(nil())
        active(nats()) -> mark(adx(zeros()))
        active(s(X)) -> s(active(X))
        active(tail(X)) -> tail(active(X))
        active(tail(cons(X,L))) -> mark(L)
        active(zeros()) -> mark(cons(0(),zeros()))
        adx(mark(X)) -> mark(adx(X))
        adx(ok(X)) -> ok(adx(X))
        cons(mark(X1),X2) -> mark(cons(X1,X2))
        cons(ok(X1),ok(X2)) -> ok(cons(X1,X2))
        head(mark(X)) -> mark(head(X))
        head(ok(X)) -> ok(head(X))
        incr(mark(X)) -> mark(incr(X))
        incr(ok(X)) -> ok(incr(X))
        proper(0()) -> ok(0())
        proper(adx(X)) -> adx(proper(X))
        proper(cons(X1,X2)) -> cons(proper(X1),proper(X2))
        proper(head(X)) -> head(proper(X))
        proper(incr(X)) -> incr(proper(X))
        proper(nats()) -> ok(nats())
        proper(nil()) -> ok(nil())
        proper(s(X)) -> s(proper(X))
        proper(tail(X)) -> tail(proper(X))
        proper(zeros()) -> ok(zeros())
        s(mark(X)) -> mark(s(X))
        s(ok(X)) -> ok(s(X))
        tail(mark(X)) -> mark(tail(X))
        tail(ok(X)) -> ok(tail(X))
        top(mark(X)) -> top(proper(X))
        top(ok(X)) -> top(active(X))
      Signature:
        {active/1,adx/1,cons/2,head/1,incr/1,proper/1,s/1,tail/1,top/1} / {0/0,mark/1,nats/0,nil/0,ok/1,zeros/0}
      Obligation:
        Innermost
        basic terms: {active,adx,cons,head,incr,proper,s,tail,top}/{0,mark,nats,nil,ok,zeros}
    Applied Processor:
      EmptyProcessor
    Proof:
      The problem is already closed. The intended complexity is O(1).