* Step 1: Sum WORST_CASE(Omega(n^1),?)
+ Considered Problem:
- Strict TRS:
active(d()) -> m(b())
active(d()) -> mark(c())
active(f(x,y,z)) -> f(x,y,active(z))
active(f(b(),c(),x)) -> mark(f(x,x,x))
f(x,y,mark(z)) -> mark(f(x,y,z))
f(ok(x),ok(y),ok(z)) -> ok(f(x,y,z))
proper(b()) -> ok(b())
proper(c()) -> ok(c())
proper(d()) -> ok(d())
proper(f(x,y,z)) -> f(proper(x),proper(y),proper(z))
top(mark(x)) -> top(proper(x))
top(ok(x)) -> top(active(x))
- Signature:
{active/1,f/3,proper/1,top/1} / {b/0,c/0,d/0,m/1,mark/1,ok/1}
- Obligation:
innermost runtime complexity wrt. defined symbols {active,f,proper,top} and constructors {b,c,d,m,mark,ok}
+ Applied Processor:
Sum {left = someStrategy, right = someStrategy}
+ Details:
()
* Step 2: DecreasingLoops WORST_CASE(Omega(n^1),?)
+ Considered Problem:
- Strict TRS:
active(d()) -> m(b())
active(d()) -> mark(c())
active(f(x,y,z)) -> f(x,y,active(z))
active(f(b(),c(),x)) -> mark(f(x,x,x))
f(x,y,mark(z)) -> mark(f(x,y,z))
f(ok(x),ok(y),ok(z)) -> ok(f(x,y,z))
proper(b()) -> ok(b())
proper(c()) -> ok(c())
proper(d()) -> ok(d())
proper(f(x,y,z)) -> f(proper(x),proper(y),proper(z))
top(mark(x)) -> top(proper(x))
top(ok(x)) -> top(active(x))
- Signature:
{active/1,f/3,proper/1,top/1} / {b/0,c/0,d/0,m/1,mark/1,ok/1}
- Obligation:
innermost runtime complexity wrt. defined symbols {active,f,proper,top} and constructors {b,c,d,m,mark,ok}
+ Applied Processor:
DecreasingLoops {bound = AnyLoop, narrow = 10}
+ Details:
The system has following decreasing Loops:
f(x,y,z){z -> mark(z)} =
f(x,y,mark(z)) ->^+ mark(f(x,y,z))
= C[f(x,y,z) = f(x,y,z){}]
WORST_CASE(Omega(n^1),?)