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