*** 1 Progress [(O(1),O(n^1))] ***
Considered Problem:
Strict DP Rules:
Strict TRS Rules:
active(and(X1,X2)) -> and(active(X1),X2)
active(and(tt(),X)) -> mark(X)
active(cons(X1,X2)) -> cons(active(X1),X2)
active(length(X)) -> length(active(X))
active(length(cons(N,L))) -> mark(s(length(L)))
active(length(nil())) -> mark(0())
active(s(X)) -> s(active(X))
active(zeros()) -> mark(cons(0(),zeros()))
and(mark(X1),X2) -> mark(and(X1,X2))
and(ok(X1),ok(X2)) -> ok(and(X1,X2))
cons(mark(X1),X2) -> mark(cons(X1,X2))
cons(ok(X1),ok(X2)) -> ok(cons(X1,X2))
length(mark(X)) -> mark(length(X))
length(ok(X)) -> ok(length(X))
proper(0()) -> ok(0())
proper(and(X1,X2)) -> and(proper(X1),proper(X2))
proper(cons(X1,X2)) -> cons(proper(X1),proper(X2))
proper(length(X)) -> length(proper(X))
proper(nil()) -> ok(nil())
proper(s(X)) -> s(proper(X))
proper(tt()) -> ok(tt())
proper(zeros()) -> ok(zeros())
s(mark(X)) -> mark(s(X))
s(ok(X)) -> ok(s(X))
top(mark(X)) -> top(proper(X))
top(ok(X)) -> top(active(X))
Weak DP Rules:
Weak TRS Rules:
Signature:
{active/1,and/2,cons/2,length/1,proper/1,s/1,top/1} / {0/0,mark/1,nil/0,ok/1,tt/0,zeros/0}
Obligation:
Full
basic terms: {active,and,cons,length,proper,s,top}/{0,mark,nil,ok,tt,zeros}
Applied Processor:
Bounds {initialAutomaton = perSymbol, enrichment = match}
Proof:
The problem is match-bounded by 5.
The enriched problem is compatible with follwoing automaton.
0_0() -> 1
0_1() -> 15
0_2() -> 24
0_3() -> 35
active_0(1) -> 2
active_0(6) -> 2
active_0(7) -> 2
active_0(8) -> 2
active_0(12) -> 2
active_0(13) -> 2
active_1(1) -> 21
active_1(6) -> 21
active_1(7) -> 21
active_1(8) -> 21
active_1(12) -> 21
active_1(13) -> 21
active_2(15) -> 22
active_2(16) -> 22
active_3(30) -> 29
active_4(24) -> 34
active_4(28) -> 34
active_4(36) -> 37
active_5(35) -> 38
and_0(1,1) -> 3
and_0(1,6) -> 3
and_0(1,7) -> 3
and_0(1,8) -> 3
and_0(1,12) -> 3
and_0(1,13) -> 3
and_0(6,1) -> 3
and_0(6,6) -> 3
and_0(6,7) -> 3
and_0(6,8) -> 3
and_0(6,12) -> 3
and_0(6,13) -> 3
and_0(7,1) -> 3
and_0(7,6) -> 3
and_0(7,7) -> 3
and_0(7,8) -> 3
and_0(7,12) -> 3
and_0(7,13) -> 3
and_0(8,1) -> 3
and_0(8,6) -> 3
and_0(8,7) -> 3
and_0(8,8) -> 3
and_0(8,12) -> 3
and_0(8,13) -> 3
and_0(12,1) -> 3
and_0(12,6) -> 3
and_0(12,7) -> 3
and_0(12,8) -> 3
and_0(12,12) -> 3
and_0(12,13) -> 3
and_0(13,1) -> 3
and_0(13,6) -> 3
and_0(13,7) -> 3
and_0(13,8) -> 3
and_0(13,12) -> 3
and_0(13,13) -> 3
and_1(1,1) -> 17
and_1(1,6) -> 17
and_1(1,7) -> 17
and_1(1,8) -> 17
and_1(1,12) -> 17
and_1(1,13) -> 17
and_1(6,1) -> 17
and_1(6,6) -> 17
and_1(6,7) -> 17
and_1(6,8) -> 17
and_1(6,12) -> 17
and_1(6,13) -> 17
and_1(7,1) -> 17
and_1(7,6) -> 17
and_1(7,7) -> 17
and_1(7,8) -> 17
and_1(7,12) -> 17
and_1(7,13) -> 17
and_1(8,1) -> 17
and_1(8,6) -> 17
and_1(8,7) -> 17
and_1(8,8) -> 17
and_1(8,12) -> 17
and_1(8,13) -> 17
and_1(12,1) -> 17
and_1(12,6) -> 17
and_1(12,7) -> 17
and_1(12,8) -> 17
and_1(12,12) -> 17
and_1(12,13) -> 17
and_1(13,1) -> 17
and_1(13,6) -> 17
and_1(13,7) -> 17
and_1(13,8) -> 17
and_1(13,12) -> 17
and_1(13,13) -> 17
cons_0(1,1) -> 4
cons_0(1,6) -> 4
cons_0(1,7) -> 4
cons_0(1,8) -> 4
cons_0(1,12) -> 4
cons_0(1,13) -> 4
cons_0(6,1) -> 4
cons_0(6,6) -> 4
cons_0(6,7) -> 4
cons_0(6,8) -> 4
cons_0(6,12) -> 4
cons_0(6,13) -> 4
cons_0(7,1) -> 4
cons_0(7,6) -> 4
cons_0(7,7) -> 4
cons_0(7,8) -> 4
cons_0(7,12) -> 4
cons_0(7,13) -> 4
cons_0(8,1) -> 4
cons_0(8,6) -> 4
cons_0(8,7) -> 4
cons_0(8,8) -> 4
cons_0(8,12) -> 4
cons_0(8,13) -> 4
cons_0(12,1) -> 4
cons_0(12,6) -> 4
cons_0(12,7) -> 4
cons_0(12,8) -> 4
cons_0(12,12) -> 4
cons_0(12,13) -> 4
cons_0(13,1) -> 4
cons_0(13,6) -> 4
cons_0(13,7) -> 4
cons_0(13,8) -> 4
cons_0(13,12) -> 4
cons_0(13,13) -> 4
cons_1(1,1) -> 18
cons_1(1,6) -> 18
cons_1(1,7) -> 18
cons_1(1,8) -> 18
cons_1(1,12) -> 18
cons_1(1,13) -> 18
cons_1(6,1) -> 18
cons_1(6,6) -> 18
cons_1(6,7) -> 18
cons_1(6,8) -> 18
cons_1(6,12) -> 18
cons_1(6,13) -> 18
cons_1(7,1) -> 18
cons_1(7,6) -> 18
cons_1(7,7) -> 18
cons_1(7,8) -> 18
cons_1(7,12) -> 18
cons_1(7,13) -> 18
cons_1(8,1) -> 18
cons_1(8,6) -> 18
cons_1(8,7) -> 18
cons_1(8,8) -> 18
cons_1(8,12) -> 18
cons_1(8,13) -> 18
cons_1(12,1) -> 18
cons_1(12,6) -> 18
cons_1(12,7) -> 18
cons_1(12,8) -> 18
cons_1(12,12) -> 18
cons_1(12,13) -> 18
cons_1(13,1) -> 18
cons_1(13,6) -> 18
cons_1(13,7) -> 18
cons_1(13,8) -> 18
cons_1(13,12) -> 18
cons_1(13,13) -> 18
cons_1(15,16) -> 14
cons_2(24,25) -> 23
cons_2(26,27) -> 22
cons_3(24,25) -> 30
cons_3(28,25) -> 30
cons_3(31,32) -> 29
cons_4(34,25) -> 29
cons_4(35,33) -> 36
cons_5(38,33) -> 37
length_0(1) -> 5
length_0(6) -> 5
length_0(7) -> 5
length_0(8) -> 5
length_0(12) -> 5
length_0(13) -> 5
length_1(1) -> 19
length_1(6) -> 19
length_1(7) -> 19
length_1(8) -> 19
length_1(12) -> 19
length_1(13) -> 19
mark_0(1) -> 6
mark_0(6) -> 6
mark_0(7) -> 6
mark_0(8) -> 6
mark_0(12) -> 6
mark_0(13) -> 6
mark_1(14) -> 2
mark_1(14) -> 21
mark_1(17) -> 3
mark_1(17) -> 17
mark_1(18) -> 4
mark_1(18) -> 18
mark_1(19) -> 5
mark_1(19) -> 19
mark_1(20) -> 10
mark_1(20) -> 20
mark_2(23) -> 22
nil_0() -> 7
nil_1() -> 15
nil_2() -> 28
ok_0(1) -> 8
ok_0(6) -> 8
ok_0(7) -> 8
ok_0(8) -> 8
ok_0(12) -> 8
ok_0(13) -> 8
ok_1(15) -> 9
ok_1(15) -> 21
ok_1(16) -> 9
ok_1(16) -> 21
ok_1(17) -> 3
ok_1(17) -> 17
ok_1(18) -> 4
ok_1(18) -> 18
ok_1(19) -> 5
ok_1(19) -> 19
ok_1(20) -> 10
ok_1(20) -> 20
ok_2(24) -> 26
ok_2(25) -> 27
ok_2(28) -> 26
ok_3(30) -> 22
ok_3(33) -> 32
ok_3(35) -> 31
ok_4(36) -> 29
proper_0(1) -> 9
proper_0(6) -> 9
proper_0(7) -> 9
proper_0(8) -> 9
proper_0(12) -> 9
proper_0(13) -> 9
proper_1(1) -> 21
proper_1(6) -> 21
proper_1(7) -> 21
proper_1(8) -> 21
proper_1(12) -> 21
proper_1(13) -> 21
proper_2(14) -> 22
proper_2(15) -> 26
proper_2(16) -> 27
proper_3(23) -> 29
proper_3(24) -> 31
proper_3(25) -> 32
s_0(1) -> 10
s_0(6) -> 10
s_0(7) -> 10
s_0(8) -> 10
s_0(12) -> 10
s_0(13) -> 10
s_1(1) -> 20
s_1(6) -> 20
s_1(7) -> 20
s_1(8) -> 20
s_1(12) -> 20
s_1(13) -> 20
top_0(1) -> 11
top_0(6) -> 11
top_0(7) -> 11
top_0(8) -> 11
top_0(12) -> 11
top_0(13) -> 11
top_1(21) -> 11
top_2(22) -> 11
top_3(29) -> 11
top_4(37) -> 11
tt_0() -> 12
tt_1() -> 15
tt_2() -> 28
zeros_0() -> 13
zeros_1() -> 16
zeros_2() -> 25
zeros_3() -> 33
*** 1.1 Progress [(O(1),O(1))] ***
Considered Problem:
Strict DP Rules:
Strict TRS Rules:
Weak DP Rules:
Weak TRS Rules:
active(and(X1,X2)) -> and(active(X1),X2)
active(and(tt(),X)) -> mark(X)
active(cons(X1,X2)) -> cons(active(X1),X2)
active(length(X)) -> length(active(X))
active(length(cons(N,L))) -> mark(s(length(L)))
active(length(nil())) -> mark(0())
active(s(X)) -> s(active(X))
active(zeros()) -> mark(cons(0(),zeros()))
and(mark(X1),X2) -> mark(and(X1,X2))
and(ok(X1),ok(X2)) -> ok(and(X1,X2))
cons(mark(X1),X2) -> mark(cons(X1,X2))
cons(ok(X1),ok(X2)) -> ok(cons(X1,X2))
length(mark(X)) -> mark(length(X))
length(ok(X)) -> ok(length(X))
proper(0()) -> ok(0())
proper(and(X1,X2)) -> and(proper(X1),proper(X2))
proper(cons(X1,X2)) -> cons(proper(X1),proper(X2))
proper(length(X)) -> length(proper(X))
proper(nil()) -> ok(nil())
proper(s(X)) -> s(proper(X))
proper(tt()) -> ok(tt())
proper(zeros()) -> ok(zeros())
s(mark(X)) -> mark(s(X))
s(ok(X)) -> ok(s(X))
top(mark(X)) -> top(proper(X))
top(ok(X)) -> top(active(X))
Signature:
{active/1,and/2,cons/2,length/1,proper/1,s/1,top/1} / {0/0,mark/1,nil/0,ok/1,tt/0,zeros/0}
Obligation:
Full
basic terms: {active,and,cons,length,proper,s,top}/{0,mark,nil,ok,tt,zeros}
Applied Processor:
EmptyProcessor
Proof:
The problem is already closed. The intended complexity is O(1).