* Step 1: Sum WORST_CASE(Omega(n^1),?)
+ Considered Problem:
- Strict TRS:
del(x,.(y,z)) -> if(=(x,y),z,.(y,del(x,z)))
del(x,nil()) -> nil()
min(x,.(y,z)) -> if(<=(x,y),min(x,z),min(y,z))
min(x,nil()) -> x
msort(.(x,y)) -> .(min(x,y),msort(del(min(x,y),.(x,y))))
msort(nil()) -> nil()
- Signature:
{del/2,min/2,msort/1} / {./2,<=/2,=/2,if/3,nil/0}
- Obligation:
innermost runtime complexity wrt. defined symbols {del,min,msort} and constructors {.,<=,=,if,nil}
+ Applied Processor:
Sum {left = someStrategy, right = someStrategy}
+ Details:
()
* Step 2: DecreasingLoops WORST_CASE(Omega(n^1),?)
+ Considered Problem:
- Strict TRS:
del(x,.(y,z)) -> if(=(x,y),z,.(y,del(x,z)))
del(x,nil()) -> nil()
min(x,.(y,z)) -> if(<=(x,y),min(x,z),min(y,z))
min(x,nil()) -> x
msort(.(x,y)) -> .(min(x,y),msort(del(min(x,y),.(x,y))))
msort(nil()) -> nil()
- Signature:
{del/2,min/2,msort/1} / {./2,<=/2,=/2,if/3,nil/0}
- Obligation:
innermost runtime complexity wrt. defined symbols {del,min,msort} and constructors {.,<=,=,if,nil}
+ Applied Processor:
DecreasingLoops {bound = AnyLoop, narrow = 10}
+ Details:
The system has following decreasing Loops:
del(x,z){z -> .(y,z)} =
del(x,.(y,z)) ->^+ if(=(x,y),z,.(y,del(x,z)))
= C[del(x,z) = del(x,z){}]
WORST_CASE(Omega(n^1),?)