* Step 1: Sum WORST_CASE(Omega(n^1),?)
+ Considered Problem:
- Strict TRS:
cond_merge_ys_zs_2(False(),Cons(x7,x8),Cons(x5,x6),x4,x3,x2,x1) -> Cons(x2,merge#2(Cons(x7,x8),x1))
cond_merge_ys_zs_2(True(),Cons(x7,x8),Cons(x5,x6),x4,x3,x2,x1) -> Cons(x4,merge#2(x3,Cons(x5,x6)))
const_f#2(x3,Cons(x6,Cons(x4,x2))) -> merge#2(x6,x4)
dc#1(map(),divisible(),mergesort_zs_3(),divide(),const_f(),Cons(x229,Nil())) -> Cons(x229,Nil())
dc#1(map(),divisible(),mergesort_zs_3(),divide(),const_f(),Cons(x51,Cons(x25,x33))) -> const_f#2(Cons(x51
,Cons(x25
,x33))
,map#2(dc(map()
,divisible()
,mergesort_zs_3()
,divide()
,const_f())
,divide_ys#1(Cons(x51
,Cons(x25
,x33))
,S(halve#1(length#1(x33))))))
dc#1(map(),divisible(),mergesort_zs_3(),divide(),const_f(),Nil()) -> Nil()
divide_ys#1(x2,x1) -> Cons(take#2(x1,x2),Cons(drop#2(x1,x2),Nil()))
drop#2(0(),x2) -> x2
drop#2(S(x10),Cons(x56,x64)) -> drop#2(x10,x64)
drop#2(S(0()),Nil()) -> bot[1]()
halve#1(0()) -> 0()
halve#1(S(0())) -> S(0())
halve#1(S(S(x14))) -> S(halve#1(x14))
length#1(Cons(x6,x8)) -> S(length#1(x8))
length#1(Nil()) -> 0()
leq#2(0(),x16) -> True()
leq#2(S(x20),0()) -> False()
leq#2(S(x4),S(x2)) -> leq#2(x4,x2)
main(x113) -> dc#1(map(),divisible(),mergesort_zs_3(),divide(),const_f(),x113)
map#2(dc(x2,x4,x6,x8,x10),Nil()) -> Nil()
map#2(dc(x6,x8,x10,x12,x14),Cons(x4,x2)) -> Cons(dc#1(x6,x8,x10,x12,x14,x4),map#2(dc(x6,x8,x10,x12,x14),x2))
merge#2(Cons(x4,x2),Nil()) -> Cons(x4,x2)
merge#2(Cons(x8,x6),Cons(x4,x2)) -> cond_merge_ys_zs_2(leq#2(x8,x4),Cons(x8,x6),Cons(x4,x2),x8,x6,x4,x2)
merge#2(Nil(),x2) -> x2
take#2(0(),x2) -> Nil()
take#2(S(x22),Cons(x56,x64)) -> Cons(x56,take#2(x22,x64))
take#2(S(0()),Nil()) -> Cons(bot[0](),Nil())
- Signature:
{cond_merge_ys_zs_2/7,const_f#2/2,dc#1/6,divide_ys#1/2,drop#2/2,halve#1/1,length#1/1,leq#2/2,main/1,map#2/2
,merge#2/2,take#2/2} / {0/0,Cons/2,False/0,Nil/0,S/1,True/0,bot[0]/0,bot[1]/0,const_f/0,dc/5,divide/0
,divisible/0,map/0,mergesort_zs_3/0}
- Obligation:
innermost runtime complexity wrt. defined symbols {cond_merge_ys_zs_2,const_f#2,dc#1,divide_ys#1,drop#2
,halve#1,length#1,leq#2,main,map#2,merge#2,take#2} and constructors {0,Cons,False,Nil,S,True,bot[0],bot[1]
,const_f,dc,divide,divisible,map,mergesort_zs_3}
+ Applied Processor:
Sum {left = someStrategy, right = someStrategy}
+ Details:
()
* Step 2: DecreasingLoops WORST_CASE(Omega(n^1),?)
+ Considered Problem:
- Strict TRS:
cond_merge_ys_zs_2(False(),Cons(x7,x8),Cons(x5,x6),x4,x3,x2,x1) -> Cons(x2,merge#2(Cons(x7,x8),x1))
cond_merge_ys_zs_2(True(),Cons(x7,x8),Cons(x5,x6),x4,x3,x2,x1) -> Cons(x4,merge#2(x3,Cons(x5,x6)))
const_f#2(x3,Cons(x6,Cons(x4,x2))) -> merge#2(x6,x4)
dc#1(map(),divisible(),mergesort_zs_3(),divide(),const_f(),Cons(x229,Nil())) -> Cons(x229,Nil())
dc#1(map(),divisible(),mergesort_zs_3(),divide(),const_f(),Cons(x51,Cons(x25,x33))) -> const_f#2(Cons(x51
,Cons(x25
,x33))
,map#2(dc(map()
,divisible()
,mergesort_zs_3()
,divide()
,const_f())
,divide_ys#1(Cons(x51
,Cons(x25
,x33))
,S(halve#1(length#1(x33))))))
dc#1(map(),divisible(),mergesort_zs_3(),divide(),const_f(),Nil()) -> Nil()
divide_ys#1(x2,x1) -> Cons(take#2(x1,x2),Cons(drop#2(x1,x2),Nil()))
drop#2(0(),x2) -> x2
drop#2(S(x10),Cons(x56,x64)) -> drop#2(x10,x64)
drop#2(S(0()),Nil()) -> bot[1]()
halve#1(0()) -> 0()
halve#1(S(0())) -> S(0())
halve#1(S(S(x14))) -> S(halve#1(x14))
length#1(Cons(x6,x8)) -> S(length#1(x8))
length#1(Nil()) -> 0()
leq#2(0(),x16) -> True()
leq#2(S(x20),0()) -> False()
leq#2(S(x4),S(x2)) -> leq#2(x4,x2)
main(x113) -> dc#1(map(),divisible(),mergesort_zs_3(),divide(),const_f(),x113)
map#2(dc(x2,x4,x6,x8,x10),Nil()) -> Nil()
map#2(dc(x6,x8,x10,x12,x14),Cons(x4,x2)) -> Cons(dc#1(x6,x8,x10,x12,x14,x4),map#2(dc(x6,x8,x10,x12,x14),x2))
merge#2(Cons(x4,x2),Nil()) -> Cons(x4,x2)
merge#2(Cons(x8,x6),Cons(x4,x2)) -> cond_merge_ys_zs_2(leq#2(x8,x4),Cons(x8,x6),Cons(x4,x2),x8,x6,x4,x2)
merge#2(Nil(),x2) -> x2
take#2(0(),x2) -> Nil()
take#2(S(x22),Cons(x56,x64)) -> Cons(x56,take#2(x22,x64))
take#2(S(0()),Nil()) -> Cons(bot[0](),Nil())
- Signature:
{cond_merge_ys_zs_2/7,const_f#2/2,dc#1/6,divide_ys#1/2,drop#2/2,halve#1/1,length#1/1,leq#2/2,main/1,map#2/2
,merge#2/2,take#2/2} / {0/0,Cons/2,False/0,Nil/0,S/1,True/0,bot[0]/0,bot[1]/0,const_f/0,dc/5,divide/0
,divisible/0,map/0,mergesort_zs_3/0}
- Obligation:
innermost runtime complexity wrt. defined symbols {cond_merge_ys_zs_2,const_f#2,dc#1,divide_ys#1,drop#2
,halve#1,length#1,leq#2,main,map#2,merge#2,take#2} and constructors {0,Cons,False,Nil,S,True,bot[0],bot[1]
,const_f,dc,divide,divisible,map,mergesort_zs_3}
+ Applied Processor:
DecreasingLoops {bound = AnyLoop, narrow = 10}
+ Details:
The system has following decreasing Loops:
drop#2(x,z){x -> S(x),z -> Cons(y,z)} =
drop#2(S(x),Cons(y,z)) ->^+ drop#2(x,z)
= C[drop#2(x,z) = drop#2(x,z){}]
WORST_CASE(Omega(n^1),?)