*** 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:
Full
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:
Full
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).