*** 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,Y))) -> mark(incr(cons(X,adx(Y))))
active(hd(X)) -> hd(active(X))
active(hd(cons(X,Y))) -> mark(X)
active(incr(X)) -> incr(active(X))
active(incr(cons(X,Y))) -> mark(cons(s(X),incr(Y)))
active(nats()) -> mark(adx(zeros()))
active(tl(X)) -> tl(active(X))
active(tl(cons(X,Y))) -> mark(Y)
active(zeros()) -> mark(cons(0(),zeros()))
adx(mark(X)) -> mark(adx(X))
adx(ok(X)) -> ok(adx(X))
cons(ok(X1),ok(X2)) -> ok(cons(X1,X2))
hd(mark(X)) -> mark(hd(X))
hd(ok(X)) -> ok(hd(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(hd(X)) -> hd(proper(X))
proper(incr(X)) -> incr(proper(X))
proper(nats()) -> ok(nats())
proper(s(X)) -> s(proper(X))
proper(tl(X)) -> tl(proper(X))
proper(zeros()) -> ok(zeros())
s(ok(X)) -> ok(s(X))
tl(mark(X)) -> mark(tl(X))
tl(ok(X)) -> ok(tl(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,hd/1,incr/1,proper/1,s/1,tl/1,top/1} / {0/0,mark/1,nats/0,ok/1,zeros/0}
Obligation:
Innermost
basic terms: {active,adx,cons,hd,incr,proper,s,tl,top}/{0,mark,nats,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() -> 17
0_2() -> 28
0_3() -> 39
0_4() -> 45
0_5() -> 56
0_6() -> 79
0_7() -> 103
active_0(1) -> 2
active_0(7) -> 2
active_0(8) -> 2
active_0(9) -> 2
active_0(14) -> 2
active_1(1) -> 24
active_1(7) -> 24
active_1(8) -> 24
active_1(9) -> 24
active_1(14) -> 24
active_2(16) -> 25
active_2(17) -> 25
active_3(33) -> 32
active_4(27) -> 37
active_4(41) -> 42
active_5(36) -> 43
active_5(57) -> 50
active_6(55) -> 51
active_6(62) -> 63
active_7(58) -> 64
active_7(78) -> 69
active_8(77) -> 72
active_8(87) -> 88
active_9(86) -> 89
active_9(108) -> 97
active_10(110) -> 111
adx_0(1) -> 3
adx_0(7) -> 3
adx_0(8) -> 3
adx_0(9) -> 3
adx_0(14) -> 3
adx_1(1) -> 18
adx_1(7) -> 18
adx_1(8) -> 18
adx_1(9) -> 18
adx_1(14) -> 18
adx_1(16) -> 15
adx_2(27) -> 26
adx_2(29) -> 25
adx_3(27) -> 33
adx_3(34) -> 32
adx_4(36) -> 41
adx_4(37) -> 32
adx_4(38) -> 40
adx_5(43) -> 42
adx_5(44) -> 47
adx_6(46) -> 61
adx_6(51) -> 50
adx_6(54) -> 76
adx_6(55) -> 57
adx_7(54) -> 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(104) -> 101
adx_8(105) -> 107
cons_0(1,1) -> 4
cons_0(1,7) -> 4
cons_0(1,8) -> 4
cons_0(1,9) -> 4
cons_0(1,14) -> 4
cons_0(7,1) -> 4
cons_0(7,7) -> 4
cons_0(7,8) -> 4
cons_0(7,9) -> 4
cons_0(7,14) -> 4
cons_0(8,1) -> 4
cons_0(8,7) -> 4
cons_0(8,8) -> 4
cons_0(8,9) -> 4
cons_0(8,14) -> 4
cons_0(9,1) -> 4
cons_0(9,7) -> 4
cons_0(9,8) -> 4
cons_0(9,9) -> 4
cons_0(9,14) -> 4
cons_0(14,1) -> 4
cons_0(14,7) -> 4
cons_0(14,8) -> 4
cons_0(14,9) -> 4
cons_0(14,14) -> 4
cons_1(1,1) -> 19
cons_1(1,7) -> 19
cons_1(1,8) -> 19
cons_1(1,9) -> 19
cons_1(1,14) -> 19
cons_1(7,1) -> 19
cons_1(7,7) -> 19
cons_1(7,8) -> 19
cons_1(7,9) -> 19
cons_1(7,14) -> 19
cons_1(8,1) -> 19
cons_1(8,7) -> 19
cons_1(8,8) -> 19
cons_1(8,9) -> 19
cons_1(8,14) -> 19
cons_1(9,1) -> 19
cons_1(9,7) -> 19
cons_1(9,8) -> 19
cons_1(9,9) -> 19
cons_1(9,14) -> 19
cons_1(14,1) -> 19
cons_1(14,7) -> 19
cons_1(14,8) -> 19
cons_1(14,9) -> 19
cons_1(14,14) -> 19
cons_1(17,16) -> 15
cons_2(28,27) -> 26
cons_2(30,29) -> 25
cons_3(28,27) -> 33
cons_3(31,27) -> 33
cons_3(35,34) -> 32
cons_3(39,36) -> 38
cons_4(39,36) -> 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(56,54) -> 58
cons_6(56,76) -> 77
cons_7(56,67) -> 66
cons_7(70,71) -> 68
cons_7(79,85) -> 86
cons_7(83,84) -> 82
cons_8(74,75) -> 72
cons_8(91,92) -> 90
cons_8(93,94) -> 88
cons_8(96,92) -> 108
cons_9(99,100) -> 97
cons_9(106,109) -> 110
hd_0(1) -> 5
hd_0(7) -> 5
hd_0(8) -> 5
hd_0(9) -> 5
hd_0(14) -> 5
hd_1(1) -> 20
hd_1(7) -> 20
hd_1(8) -> 20
hd_1(9) -> 20
hd_1(14) -> 20
incr_0(1) -> 6
incr_0(7) -> 6
incr_0(8) -> 6
incr_0(9) -> 6
incr_0(14) -> 6
incr_1(1) -> 21
incr_1(7) -> 21
incr_1(8) -> 21
incr_1(9) -> 21
incr_1(14) -> 21
incr_6(60) -> 59
incr_7(66) -> 65
incr_7(68) -> 63
incr_7(76) -> 84
incr_7(77) -> 78
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(107) -> 109
mark_0(1) -> 7
mark_0(7) -> 7
mark_0(8) -> 7
mark_0(9) -> 7
mark_0(14) -> 7
mark_1(15) -> 2
mark_1(15) -> 24
mark_1(18) -> 3
mark_1(18) -> 18
mark_1(20) -> 5
mark_1(20) -> 20
mark_1(21) -> 6
mark_1(21) -> 21
mark_1(23) -> 12
mark_1(23) -> 23
mark_2(26) -> 25
mark_3(38) -> 37
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
nats_0() -> 8
nats_1() -> 17
nats_2() -> 31
ok_0(1) -> 9
ok_0(7) -> 9
ok_0(8) -> 9
ok_0(9) -> 9
ok_0(14) -> 9
ok_1(16) -> 10
ok_1(16) -> 24
ok_1(17) -> 10
ok_1(17) -> 24
ok_1(18) -> 3
ok_1(18) -> 18
ok_1(19) -> 4
ok_1(19) -> 19
ok_1(20) -> 5
ok_1(20) -> 20
ok_1(21) -> 6
ok_1(21) -> 21
ok_1(22) -> 11
ok_1(22) -> 22
ok_1(23) -> 12
ok_1(23) -> 23
ok_2(27) -> 29
ok_2(28) -> 30
ok_2(31) -> 30
ok_3(33) -> 25
ok_3(36) -> 34
ok_3(39) -> 35
ok_4(41) -> 32
ok_4(45) -> 48
ok_4(46) -> 49
ok_5(54) -> 53
ok_5(54) -> 73
ok_5(55) -> 43
ok_5(56) -> 52
ok_5(56) -> 70
ok_6(57) -> 42
ok_6(58) -> 51
ok_6(76) -> 71
ok_6(77) -> 68
ok_6(79) -> 74
ok_6(81) -> 80
ok_6(81) -> 98
ok_7(62) -> 50
ok_7(78) -> 63
ok_7(85) -> 75
ok_7(85) -> 95
ok_7(86) -> 72
ok_7(96) -> 93
ok_7(103) -> 102
ok_7(105) -> 104
ok_8(87) -> 69
ok_8(92) -> 94
ok_8(106) -> 99
ok_8(107) -> 101
ok_8(108) -> 88
ok_9(109) -> 100
ok_9(110) -> 97
proper_0(1) -> 10
proper_0(7) -> 10
proper_0(8) -> 10
proper_0(9) -> 10
proper_0(14) -> 10
proper_1(1) -> 24
proper_1(7) -> 24
proper_1(8) -> 24
proper_1(9) -> 24
proper_1(14) -> 24
proper_2(15) -> 25
proper_2(16) -> 29
proper_2(17) -> 30
proper_3(26) -> 32
proper_3(27) -> 34
proper_3(28) -> 35
proper_4(36) -> 49
proper_4(39) -> 48
proper_4(40) -> 42
proper_5(38) -> 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(54) -> 98
proper_7(60) -> 68
proper_7(61) -> 71
proper_7(65) -> 69
proper_8(54) -> 80
proper_8(56) -> 74
proper_8(66) -> 72
proper_8(67) -> 75
proper_8(76) -> 95
proper_8(81) -> 104
proper_8(82) -> 88
proper_8(83) -> 93
proper_8(84) -> 94
proper_9(79) -> 102
proper_9(85) -> 101
proper_9(90) -> 97
proper_9(91) -> 99
proper_9(92) -> 100
s_0(1) -> 11
s_0(7) -> 11
s_0(8) -> 11
s_0(9) -> 11
s_0(14) -> 11
s_1(1) -> 22
s_1(7) -> 22
s_1(8) -> 22
s_1(9) -> 22
s_1(14) -> 22
s_7(56) -> 83
s_7(79) -> 96
s_8(74) -> 93
s_8(79) -> 91
s_8(103) -> 106
s_9(102) -> 99
tl_0(1) -> 12
tl_0(7) -> 12
tl_0(8) -> 12
tl_0(9) -> 12
tl_0(14) -> 12
tl_1(1) -> 23
tl_1(7) -> 23
tl_1(8) -> 23
tl_1(9) -> 23
tl_1(14) -> 23
top_0(1) -> 13
top_0(7) -> 13
top_0(8) -> 13
top_0(9) -> 13
top_0(14) -> 13
top_1(24) -> 13
top_2(25) -> 13
top_3(32) -> 13
top_4(42) -> 13
top_5(50) -> 13
top_6(63) -> 13
top_7(69) -> 13
top_8(88) -> 13
top_9(97) -> 13
top_10(111) -> 13
zeros_0() -> 14
zeros_1() -> 16
zeros_2() -> 27
zeros_3() -> 36
zeros_4() -> 46
zeros_5() -> 54
zeros_6() -> 81
zeros_7() -> 105
*** 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,Y))) -> mark(incr(cons(X,adx(Y))))
active(hd(X)) -> hd(active(X))
active(hd(cons(X,Y))) -> mark(X)
active(incr(X)) -> incr(active(X))
active(incr(cons(X,Y))) -> mark(cons(s(X),incr(Y)))
active(nats()) -> mark(adx(zeros()))
active(tl(X)) -> tl(active(X))
active(tl(cons(X,Y))) -> mark(Y)
active(zeros()) -> mark(cons(0(),zeros()))
adx(mark(X)) -> mark(adx(X))
adx(ok(X)) -> ok(adx(X))
cons(ok(X1),ok(X2)) -> ok(cons(X1,X2))
hd(mark(X)) -> mark(hd(X))
hd(ok(X)) -> ok(hd(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(hd(X)) -> hd(proper(X))
proper(incr(X)) -> incr(proper(X))
proper(nats()) -> ok(nats())
proper(s(X)) -> s(proper(X))
proper(tl(X)) -> tl(proper(X))
proper(zeros()) -> ok(zeros())
s(ok(X)) -> ok(s(X))
tl(mark(X)) -> mark(tl(X))
tl(ok(X)) -> ok(tl(X))
top(mark(X)) -> top(proper(X))
top(ok(X)) -> top(active(X))
Signature:
{active/1,adx/1,cons/2,hd/1,incr/1,proper/1,s/1,tl/1,top/1} / {0/0,mark/1,nats/0,ok/1,zeros/0}
Obligation:
Innermost
basic terms: {active,adx,cons,hd,incr,proper,s,tl,top}/{0,mark,nats,ok,zeros}
Applied Processor:
EmptyProcessor
Proof:
The problem is already closed. The intended complexity is O(1).