* Step 1: Sum WORST_CASE(Omega(n^1),O(n^1))
+ Considered Problem:
- Strict TRS:
active(f(x)) -> f(active(x))
active(f(x)) -> mark(x)
check(x) -> start(match(f(X()),x))
check(f(x)) -> f(check(x))
f(found(x)) -> found(f(x))
f(mark(x)) -> mark(f(x))
f(ok(x)) -> ok(f(x))
match(X(),x) -> proper(x)
match(f(x),f(y)) -> f(match(x,y))
proper(c()) -> ok(c())
proper(f(x)) -> f(proper(x))
start(ok(x)) -> found(x)
top(active(c())) -> top(mark(c()))
top(found(x)) -> top(active(x))
top(mark(x)) -> top(check(x))
- Signature:
{active/1,check/1,f/1,match/2,proper/1,start/1,top/1} / {X/0,c/0,found/1,mark/1,ok/1}
- Obligation:
innermost runtime complexity wrt. defined symbols {active,check,f,match,proper,start
,top} and constructors {X,c,found,mark,ok}
+ Applied Processor:
Sum {left = someStrategy, right = someStrategy}
+ Details:
()
** Step 1.a:1: DecreasingLoops WORST_CASE(Omega(n^1),?)
+ Considered Problem:
- Strict TRS:
active(f(x)) -> f(active(x))
active(f(x)) -> mark(x)
check(x) -> start(match(f(X()),x))
check(f(x)) -> f(check(x))
f(found(x)) -> found(f(x))
f(mark(x)) -> mark(f(x))
f(ok(x)) -> ok(f(x))
match(X(),x) -> proper(x)
match(f(x),f(y)) -> f(match(x,y))
proper(c()) -> ok(c())
proper(f(x)) -> f(proper(x))
start(ok(x)) -> found(x)
top(active(c())) -> top(mark(c()))
top(found(x)) -> top(active(x))
top(mark(x)) -> top(check(x))
- Signature:
{active/1,check/1,f/1,match/2,proper/1,start/1,top/1} / {X/0,c/0,found/1,mark/1,ok/1}
- Obligation:
innermost runtime complexity wrt. defined symbols {active,check,f,match,proper,start
,top} and constructors {X,c,found,mark,ok}
+ Applied Processor:
DecreasingLoops {bound = AnyLoop, narrow = 10}
+ Details:
The system has following decreasing Loops:
f(x){x -> found(x)} =
f(found(x)) ->^+ found(f(x))
= C[f(x) = f(x){}]
** Step 1.b:1: Bounds WORST_CASE(?,O(n^1))
+ Considered Problem:
- Strict TRS:
active(f(x)) -> f(active(x))
active(f(x)) -> mark(x)
check(x) -> start(match(f(X()),x))
check(f(x)) -> f(check(x))
f(found(x)) -> found(f(x))
f(mark(x)) -> mark(f(x))
f(ok(x)) -> ok(f(x))
match(X(),x) -> proper(x)
match(f(x),f(y)) -> f(match(x,y))
proper(c()) -> ok(c())
proper(f(x)) -> f(proper(x))
start(ok(x)) -> found(x)
top(active(c())) -> top(mark(c()))
top(found(x)) -> top(active(x))
top(mark(x)) -> top(check(x))
- Signature:
{active/1,check/1,f/1,match/2,proper/1,start/1,top/1} / {X/0,c/0,found/1,mark/1,ok/1}
- Obligation:
innermost runtime complexity wrt. defined symbols {active,check,f,match,proper,start
,top} and constructors {X,c,found,mark,ok}
+ Applied Processor:
Bounds {initialAutomaton = perSymbol, enrichment = match}
+ Details:
The problem is match-bounded by 3.
The enriched problem is compatible with follwoing automaton.
X_0() -> 1
X_1() -> 15
X_2() -> 21
X_3() -> 25
active_0(1) -> 2
active_0(3) -> 2
active_0(6) -> 2
active_0(7) -> 2
active_0(9) -> 2
active_1(1) -> 18
active_1(3) -> 18
active_1(6) -> 18
active_1(7) -> 18
active_1(9) -> 18
c_0() -> 3
c_1() -> 17
check_0(1) -> 4
check_0(3) -> 4
check_0(6) -> 4
check_0(7) -> 4
check_0(9) -> 4
check_1(1) -> 18
check_1(3) -> 18
check_1(6) -> 18
check_1(7) -> 18
check_1(9) -> 18
check_2(17) -> 22
f_0(1) -> 5
f_0(3) -> 5
f_0(6) -> 5
f_0(7) -> 5
f_0(9) -> 5
f_1(1) -> 16
f_1(3) -> 16
f_1(6) -> 16
f_1(7) -> 16
f_1(9) -> 16
f_1(15) -> 14
f_2(21) -> 20
f_3(25) -> 24
found_0(1) -> 6
found_0(3) -> 6
found_0(6) -> 6
found_0(7) -> 6
found_0(9) -> 6
found_1(1) -> 11
found_1(3) -> 11
found_1(6) -> 11
found_1(7) -> 11
found_1(9) -> 11
found_1(16) -> 5
found_1(16) -> 16
mark_0(1) -> 7
mark_0(3) -> 7
mark_0(6) -> 7
mark_0(7) -> 7
mark_0(9) -> 7
mark_1(16) -> 5
mark_1(16) -> 16
mark_1(17) -> 18
match_0(1,1) -> 8
match_0(1,3) -> 8
match_0(1,6) -> 8
match_0(1,7) -> 8
match_0(1,9) -> 8
match_0(3,1) -> 8
match_0(3,3) -> 8
match_0(3,6) -> 8
match_0(3,7) -> 8
match_0(3,9) -> 8
match_0(6,1) -> 8
match_0(6,3) -> 8
match_0(6,6) -> 8
match_0(6,7) -> 8
match_0(6,9) -> 8
match_0(7,1) -> 8
match_0(7,3) -> 8
match_0(7,6) -> 8
match_0(7,7) -> 8
match_0(7,9) -> 8
match_0(9,1) -> 8
match_0(9,3) -> 8
match_0(9,6) -> 8
match_0(9,7) -> 8
match_0(9,9) -> 8
match_1(14,1) -> 13
match_1(14,3) -> 13
match_1(14,6) -> 13
match_1(14,7) -> 13
match_1(14,9) -> 13
match_2(20,1) -> 19
match_2(20,3) -> 19
match_2(20,6) -> 19
match_2(20,7) -> 19
match_2(20,9) -> 19
match_3(24,17) -> 23
ok_0(1) -> 9
ok_0(3) -> 9
ok_0(6) -> 9
ok_0(7) -> 9
ok_0(9) -> 9
ok_1(16) -> 5
ok_1(16) -> 16
ok_1(17) -> 8
ok_1(17) -> 10
proper_0(1) -> 10
proper_0(3) -> 10
proper_0(6) -> 10
proper_0(7) -> 10
proper_0(9) -> 10
proper_1(1) -> 8
proper_1(3) -> 8
proper_1(6) -> 8
proper_1(7) -> 8
proper_1(9) -> 8
start_0(1) -> 11
start_0(3) -> 11
start_0(6) -> 11
start_0(7) -> 11
start_0(9) -> 11
start_1(13) -> 4
start_2(19) -> 18
start_3(23) -> 22
top_0(1) -> 12
top_0(3) -> 12
top_0(6) -> 12
top_0(7) -> 12
top_0(9) -> 12
top_1(18) -> 12
top_2(22) -> 12
** Step 1.b:2: EmptyProcessor WORST_CASE(?,O(1))
+ Considered Problem:
- Weak TRS:
active(f(x)) -> f(active(x))
active(f(x)) -> mark(x)
check(x) -> start(match(f(X()),x))
check(f(x)) -> f(check(x))
f(found(x)) -> found(f(x))
f(mark(x)) -> mark(f(x))
f(ok(x)) -> ok(f(x))
match(X(),x) -> proper(x)
match(f(x),f(y)) -> f(match(x,y))
proper(c()) -> ok(c())
proper(f(x)) -> f(proper(x))
start(ok(x)) -> found(x)
top(active(c())) -> top(mark(c()))
top(found(x)) -> top(active(x))
top(mark(x)) -> top(check(x))
- Signature:
{active/1,check/1,f/1,match/2,proper/1,start/1,top/1} / {X/0,c/0,found/1,mark/1,ok/1}
- Obligation:
innermost runtime complexity wrt. defined symbols {active,check,f,match,proper,start
,top} and constructors {X,c,found,mark,ok}
+ Applied Processor:
EmptyProcessor
+ Details:
The problem is already closed. The intended complexity is O(1).
WORST_CASE(Omega(n^1),O(n^1))