*** 1 Progress [(O(1),O(n^1))] ***
Considered Problem:
Strict DP Rules:
Strict TRS Rules:
active(cons(X1,X2)) -> cons(active(X1),X2)
active(head(X)) -> head(active(X))
active(head(cons(X,XS))) -> mark(X)
active(incr(X)) -> incr(active(X))
active(incr(cons(X,XS))) -> mark(cons(s(X),incr(XS)))
active(nats()) -> mark(cons(0(),incr(nats())))
active(odds()) -> mark(incr(pairs()))
active(pairs()) -> mark(cons(0(),incr(odds())))
active(s(X)) -> s(active(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))
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(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(odds()) -> ok(odds())
proper(pairs()) -> ok(pairs())
proper(s(X)) -> s(proper(X))
proper(tail(X)) -> tail(proper(X))
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,cons/2,head/1,incr/1,proper/1,s/1,tail/1,top/1} / {0/0,mark/1,nats/0,odds/0,ok/1,pairs/0}
Obligation:
Full
basic terms: {active,cons,head,incr,proper,s,tail,top}/{0,mark,nats,odds,ok,pairs}
Applied Processor:
Bounds {initialAutomaton = perSymbol, enrichment = match}
Proof:
The problem is match-bounded by 9.
The enriched problem is compatible with follwoing automaton.
0_0() -> 1
0_1() -> 16
0_2() -> 28
0_3() -> 47
0_4() -> 56
0_5() -> 75
0_6() -> 100
active_0(1) -> 2
active_0(6) -> 2
active_0(7) -> 2
active_0(8) -> 2
active_0(9) -> 2
active_0(10) -> 2
active_1(1) -> 25
active_1(6) -> 25
active_1(7) -> 25
active_1(8) -> 25
active_1(9) -> 25
active_1(10) -> 25
active_2(16) -> 26
active_2(18) -> 26
active_2(19) -> 26
active_3(38) -> 36
active_4(28) -> 53
active_4(31) -> 45
active_4(51) -> 52
active_5(44) -> 54
active_5(47) -> 61
active_5(74) -> 60
active_6(56) -> 82
active_6(72) -> 65
active_6(80) -> 81
active_7(75) -> 92
active_7(79) -> 83
active_7(105) -> 91
active_8(99) -> 107
active_8(100) -> 111
active_8(108) -> 109
active_9(103) -> 110
cons_0(1,1) -> 3
cons_0(1,6) -> 3
cons_0(1,7) -> 3
cons_0(1,8) -> 3
cons_0(1,9) -> 3
cons_0(1,10) -> 3
cons_0(6,1) -> 3
cons_0(6,6) -> 3
cons_0(6,7) -> 3
cons_0(6,8) -> 3
cons_0(6,9) -> 3
cons_0(6,10) -> 3
cons_0(7,1) -> 3
cons_0(7,6) -> 3
cons_0(7,7) -> 3
cons_0(7,8) -> 3
cons_0(7,9) -> 3
cons_0(7,10) -> 3
cons_0(8,1) -> 3
cons_0(8,6) -> 3
cons_0(8,7) -> 3
cons_0(8,8) -> 3
cons_0(8,9) -> 3
cons_0(8,10) -> 3
cons_0(9,1) -> 3
cons_0(9,6) -> 3
cons_0(9,7) -> 3
cons_0(9,8) -> 3
cons_0(9,9) -> 3
cons_0(9,10) -> 3
cons_0(10,1) -> 3
cons_0(10,6) -> 3
cons_0(10,7) -> 3
cons_0(10,8) -> 3
cons_0(10,9) -> 3
cons_0(10,10) -> 3
cons_1(1,1) -> 20
cons_1(1,6) -> 20
cons_1(1,7) -> 20
cons_1(1,8) -> 20
cons_1(1,9) -> 20
cons_1(1,10) -> 20
cons_1(6,1) -> 20
cons_1(6,6) -> 20
cons_1(6,7) -> 20
cons_1(6,8) -> 20
cons_1(6,9) -> 20
cons_1(6,10) -> 20
cons_1(7,1) -> 20
cons_1(7,6) -> 20
cons_1(7,7) -> 20
cons_1(7,8) -> 20
cons_1(7,9) -> 20
cons_1(7,10) -> 20
cons_1(8,1) -> 20
cons_1(8,6) -> 20
cons_1(8,7) -> 20
cons_1(8,8) -> 20
cons_1(8,9) -> 20
cons_1(8,10) -> 20
cons_1(9,1) -> 20
cons_1(9,6) -> 20
cons_1(9,7) -> 20
cons_1(9,8) -> 20
cons_1(9,9) -> 20
cons_1(9,10) -> 20
cons_1(10,1) -> 20
cons_1(10,6) -> 20
cons_1(10,7) -> 20
cons_1(10,8) -> 20
cons_1(10,9) -> 20
cons_1(10,10) -> 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(47,48) -> 46
cons_4(47,50) -> 51
cons_4(53,37) -> 36
cons_4(56,57) -> 55
cons_4(62,63) -> 54
cons_5(56,67) -> 72
cons_5(61,50) -> 52
cons_5(68,69) -> 65
cons_6(75,73) -> 79
cons_6(77,78) -> 76
cons_6(82,67) -> 65
cons_7(85,86) -> 84
cons_7(87,88) -> 81
cons_7(92,73) -> 83
cons_7(99,86) -> 105
cons_8(93,94) -> 91
cons_8(103,106) -> 108
cons_8(107,86) -> 91
cons_9(110,106) -> 109
head_0(1) -> 4
head_0(6) -> 4
head_0(7) -> 4
head_0(8) -> 4
head_0(9) -> 4
head_0(10) -> 4
head_1(1) -> 21
head_1(6) -> 21
head_1(7) -> 21
head_1(8) -> 21
head_1(9) -> 21
head_1(10) -> 21
incr_0(1) -> 5
incr_0(6) -> 5
incr_0(7) -> 5
incr_0(8) -> 5
incr_0(9) -> 5
incr_0(10) -> 5
incr_1(1) -> 22
incr_1(6) -> 22
incr_1(7) -> 22
incr_1(8) -> 22
incr_1(9) -> 22
incr_1(10) -> 22
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(41) -> 40
incr_3(42) -> 36
incr_3(43) -> 48
incr_4(43) -> 50
incr_4(44) -> 51
incr_4(45) -> 36
incr_4(46) -> 49
incr_4(58) -> 57
incr_4(64) -> 63
incr_5(54) -> 52
incr_5(55) -> 59
incr_5(58) -> 67
incr_5(66) -> 67
incr_5(70) -> 69
incr_6(65) -> 60
incr_6(67) -> 78
incr_6(71) -> 73
incr_6(72) -> 74
incr_6(95) -> 89
incr_6(97) -> 73
incr_7(73) -> 86
incr_7(79) -> 80
incr_7(83) -> 81
incr_7(89) -> 88
incr_7(101) -> 96
incr_7(102) -> 104
incr_8(96) -> 94
incr_8(104) -> 106
mark_0(1) -> 6
mark_0(6) -> 6
mark_0(7) -> 6
mark_0(8) -> 6
mark_0(9) -> 6
mark_0(10) -> 6
mark_1(15) -> 2
mark_1(15) -> 25
mark_1(20) -> 3
mark_1(20) -> 20
mark_1(21) -> 4
mark_1(21) -> 21
mark_1(22) -> 5
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(46) -> 45
mark_4(49) -> 36
mark_4(55) -> 54
mark_5(59) -> 52
mark_6(76) -> 60
mark_7(84) -> 81
nats_0() -> 7
nats_1() -> 18
nats_2() -> 30
nats_3() -> 43
nats_4() -> 66
nats_5() -> 97
nats_6() -> 102
odds_0() -> 8
odds_1() -> 18
odds_2() -> 30
odds_3() -> 43
odds_4() -> 58
odds_5() -> 71
odds_6() -> 102
ok_0(1) -> 9
ok_0(6) -> 9
ok_0(7) -> 9
ok_0(8) -> 9
ok_0(9) -> 9
ok_0(10) -> 9
ok_1(16) -> 11
ok_1(16) -> 25
ok_1(18) -> 11
ok_1(18) -> 25
ok_1(19) -> 11
ok_1(19) -> 25
ok_1(20) -> 3
ok_1(20) -> 20
ok_1(21) -> 4
ok_1(21) -> 21
ok_1(22) -> 5
ok_1(22) -> 22
ok_1(23) -> 12
ok_1(23) -> 23
ok_1(24) -> 13
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(43) -> 41
ok_3(44) -> 42
ok_3(47) -> 39
ok_4(50) -> 40
ok_4(51) -> 36
ok_4(56) -> 62
ok_4(58) -> 64
ok_4(66) -> 64
ok_5(67) -> 63
ok_5(71) -> 70
ok_5(71) -> 95
ok_5(72) -> 54
ok_5(75) -> 68
ok_5(75) -> 90
ok_5(97) -> 95
ok_6(73) -> 69
ok_6(73) -> 89
ok_6(74) -> 52
ok_6(79) -> 65
ok_6(99) -> 87
ok_6(100) -> 98
ok_6(102) -> 101
ok_7(80) -> 60
ok_7(86) -> 88
ok_7(103) -> 93
ok_7(104) -> 96
ok_7(105) -> 81
ok_8(106) -> 94
ok_8(108) -> 91
pairs_0() -> 10
pairs_1() -> 19
pairs_2() -> 31
pairs_3() -> 44
proper_0(1) -> 11
proper_0(6) -> 11
proper_0(7) -> 11
proper_0(8) -> 11
proper_0(9) -> 11
proper_0(10) -> 11
proper_1(1) -> 25
proper_1(6) -> 25
proper_1(7) -> 25
proper_1(8) -> 25
proper_1(9) -> 25
proper_1(10) -> 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) -> 41
proper_3(31) -> 42
proper_4(43) -> 64
proper_4(47) -> 62
proper_4(48) -> 63
proper_4(49) -> 52
proper_5(46) -> 54
proper_5(56) -> 68
proper_5(57) -> 69
proper_5(58) -> 70
proper_5(59) -> 60
proper_6(55) -> 65
proper_6(58) -> 95
proper_6(66) -> 95
proper_6(76) -> 81
proper_7(56) -> 90
proper_7(67) -> 89
proper_7(71) -> 101
proper_7(77) -> 87
proper_7(78) -> 88
proper_7(84) -> 91
proper_7(97) -> 101
proper_8(73) -> 96
proper_8(75) -> 98
proper_8(85) -> 93
proper_8(86) -> 94
s_0(1) -> 12
s_0(6) -> 12
s_0(7) -> 12
s_0(8) -> 12
s_0(9) -> 12
s_0(10) -> 12
s_1(1) -> 23
s_1(6) -> 23
s_1(7) -> 23
s_1(8) -> 23
s_1(9) -> 23
s_1(10) -> 23
s_6(56) -> 77
s_6(75) -> 99
s_7(75) -> 85
s_7(90) -> 87
s_7(92) -> 107
s_7(100) -> 103
s_8(98) -> 93
s_8(111) -> 110
tail_0(1) -> 13
tail_0(6) -> 13
tail_0(7) -> 13
tail_0(8) -> 13
tail_0(9) -> 13
tail_0(10) -> 13
tail_1(1) -> 24
tail_1(6) -> 24
tail_1(7) -> 24
tail_1(8) -> 24
tail_1(9) -> 24
tail_1(10) -> 24
top_0(1) -> 14
top_0(6) -> 14
top_0(7) -> 14
top_0(8) -> 14
top_0(9) -> 14
top_0(10) -> 14
top_1(25) -> 14
top_2(26) -> 14
top_3(36) -> 14
top_4(52) -> 14
top_5(60) -> 14
top_6(81) -> 14
top_7(91) -> 14
top_8(109) -> 14
*** 1.1 Progress [(O(1),O(1))] ***
Considered Problem:
Strict DP Rules:
Strict TRS Rules:
Weak DP Rules:
Weak TRS Rules:
active(cons(X1,X2)) -> cons(active(X1),X2)
active(head(X)) -> head(active(X))
active(head(cons(X,XS))) -> mark(X)
active(incr(X)) -> incr(active(X))
active(incr(cons(X,XS))) -> mark(cons(s(X),incr(XS)))
active(nats()) -> mark(cons(0(),incr(nats())))
active(odds()) -> mark(incr(pairs()))
active(pairs()) -> mark(cons(0(),incr(odds())))
active(s(X)) -> s(active(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))
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(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(odds()) -> ok(odds())
proper(pairs()) -> ok(pairs())
proper(s(X)) -> s(proper(X))
proper(tail(X)) -> tail(proper(X))
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,cons/2,head/1,incr/1,proper/1,s/1,tail/1,top/1} / {0/0,mark/1,nats/0,odds/0,ok/1,pairs/0}
Obligation:
Full
basic terms: {active,cons,head,incr,proper,s,tail,top}/{0,mark,nats,odds,ok,pairs}
Applied Processor:
EmptyProcessor
Proof:
The problem is already closed. The intended complexity is O(1).