MAYBE * Step 1: DependencyPairs MAYBE + 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: DependencyPairs {dpKind_ = DT} + Details: We add the following dependency tuples: Strict DPs cond_merge_ys_zs_2#(False(),Cons(x7,x8),Cons(x5,x6),x4,x3,x2,x1) -> c_1(merge#2#(Cons(x7,x8),x1)) cond_merge_ys_zs_2#(True(),Cons(x7,x8),Cons(x5,x6),x4,x3,x2,x1) -> c_2(merge#2#(x3,Cons(x5,x6))) const_f#2#(x3,Cons(x6,Cons(x4,x2))) -> c_3(merge#2#(x6,x4)) dc#1#(map(),divisible(),mergesort_zs_3(),divide(),const_f(),Cons(x229,Nil())) -> c_4() dc#1#(map(),divisible(),mergesort_zs_3(),divide(),const_f(),Cons(x51,Cons(x25,x33))) -> c_5(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)))))) ,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))))) ,divide_ys#1#(Cons(x51,Cons(x25,x33)),S(halve#1(length#1(x33)))) ,halve#1#(length#1(x33)) ,length#1#(x33)) dc#1#(map(),divisible(),mergesort_zs_3(),divide(),const_f(),Nil()) -> c_6() divide_ys#1#(x2,x1) -> c_7(take#2#(x1,x2),drop#2#(x1,x2)) drop#2#(0(),x2) -> c_8() drop#2#(S(x10),Cons(x56,x64)) -> c_9(drop#2#(x10,x64)) drop#2#(S(0()),Nil()) -> c_10() halve#1#(0()) -> c_11() halve#1#(S(0())) -> c_12() halve#1#(S(S(x14))) -> c_13(halve#1#(x14)) length#1#(Cons(x6,x8)) -> c_14(length#1#(x8)) length#1#(Nil()) -> c_15() leq#2#(0(),x16) -> c_16() leq#2#(S(x20),0()) -> c_17() leq#2#(S(x4),S(x2)) -> c_18(leq#2#(x4,x2)) main#(x113) -> c_19(dc#1#(map(),divisible(),mergesort_zs_3(),divide(),const_f(),x113)) map#2#(dc(x2,x4,x6,x8,x10),Nil()) -> c_20() map#2#(dc(x6,x8,x10,x12,x14),Cons(x4,x2)) -> c_21(dc#1#(x6,x8,x10,x12,x14,x4) ,map#2#(dc(x6,x8,x10,x12,x14),x2)) merge#2#(Cons(x4,x2),Nil()) -> c_22() merge#2#(Cons(x8,x6),Cons(x4,x2)) -> c_23(cond_merge_ys_zs_2#(leq#2(x8,x4) ,Cons(x8,x6) ,Cons(x4,x2) ,x8 ,x6 ,x4 ,x2) ,leq#2#(x8,x4)) merge#2#(Nil(),x2) -> c_24() take#2#(0(),x2) -> c_25() take#2#(S(x22),Cons(x56,x64)) -> c_26(take#2#(x22,x64)) take#2#(S(0()),Nil()) -> c_27() Weak DPs and mark the set of starting terms. * Step 2: UsableRules MAYBE + Considered Problem: - Strict DPs: cond_merge_ys_zs_2#(False(),Cons(x7,x8),Cons(x5,x6),x4,x3,x2,x1) -> c_1(merge#2#(Cons(x7,x8),x1)) cond_merge_ys_zs_2#(True(),Cons(x7,x8),Cons(x5,x6),x4,x3,x2,x1) -> c_2(merge#2#(x3,Cons(x5,x6))) const_f#2#(x3,Cons(x6,Cons(x4,x2))) -> c_3(merge#2#(x6,x4)) dc#1#(map(),divisible(),mergesort_zs_3(),divide(),const_f(),Cons(x229,Nil())) -> c_4() dc#1#(map(),divisible(),mergesort_zs_3(),divide(),const_f(),Cons(x51,Cons(x25,x33))) -> c_5(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)))))) ,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))))) ,divide_ys#1#(Cons(x51,Cons(x25,x33)),S(halve#1(length#1(x33)))) ,halve#1#(length#1(x33)) ,length#1#(x33)) dc#1#(map(),divisible(),mergesort_zs_3(),divide(),const_f(),Nil()) -> c_6() divide_ys#1#(x2,x1) -> c_7(take#2#(x1,x2),drop#2#(x1,x2)) drop#2#(0(),x2) -> c_8() drop#2#(S(x10),Cons(x56,x64)) -> c_9(drop#2#(x10,x64)) drop#2#(S(0()),Nil()) -> c_10() halve#1#(0()) -> c_11() halve#1#(S(0())) -> c_12() halve#1#(S(S(x14))) -> c_13(halve#1#(x14)) length#1#(Cons(x6,x8)) -> c_14(length#1#(x8)) length#1#(Nil()) -> c_15() leq#2#(0(),x16) -> c_16() leq#2#(S(x20),0()) -> c_17() leq#2#(S(x4),S(x2)) -> c_18(leq#2#(x4,x2)) main#(x113) -> c_19(dc#1#(map(),divisible(),mergesort_zs_3(),divide(),const_f(),x113)) map#2#(dc(x2,x4,x6,x8,x10),Nil()) -> c_20() map#2#(dc(x6,x8,x10,x12,x14),Cons(x4,x2)) -> c_21(dc#1#(x6,x8,x10,x12,x14,x4) ,map#2#(dc(x6,x8,x10,x12,x14),x2)) merge#2#(Cons(x4,x2),Nil()) -> c_22() merge#2#(Cons(x8,x6),Cons(x4,x2)) -> c_23(cond_merge_ys_zs_2#(leq#2(x8,x4) ,Cons(x8,x6) ,Cons(x4,x2) ,x8 ,x6 ,x4 ,x2) ,leq#2#(x8,x4)) merge#2#(Nil(),x2) -> c_24() take#2#(0(),x2) -> c_25() take#2#(S(x22),Cons(x56,x64)) -> c_26(take#2#(x22,x64)) take#2#(S(0()),Nil()) -> c_27() - Weak 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,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,c_1/1,c_2/1,c_3/1,c_4/0,c_5/5,c_6/0 ,c_7/2,c_8/0,c_9/1,c_10/0,c_11/0,c_12/0,c_13/1,c_14/1,c_15/0,c_16/0,c_17/0,c_18/1,c_19/1,c_20/0,c_21/2 ,c_22/0,c_23/2,c_24/0,c_25/0,c_26/1,c_27/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: UsableRules + Details: We replace rewrite rules by usable rules: 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) 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()) cond_merge_ys_zs_2#(False(),Cons(x7,x8),Cons(x5,x6),x4,x3,x2,x1) -> c_1(merge#2#(Cons(x7,x8),x1)) cond_merge_ys_zs_2#(True(),Cons(x7,x8),Cons(x5,x6),x4,x3,x2,x1) -> c_2(merge#2#(x3,Cons(x5,x6))) const_f#2#(x3,Cons(x6,Cons(x4,x2))) -> c_3(merge#2#(x6,x4)) dc#1#(map(),divisible(),mergesort_zs_3(),divide(),const_f(),Cons(x229,Nil())) -> c_4() dc#1#(map(),divisible(),mergesort_zs_3(),divide(),const_f(),Cons(x51,Cons(x25,x33))) -> c_5(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)))))) ,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))))) ,divide_ys#1#(Cons(x51,Cons(x25,x33)),S(halve#1(length#1(x33)))) ,halve#1#(length#1(x33)) ,length#1#(x33)) dc#1#(map(),divisible(),mergesort_zs_3(),divide(),const_f(),Nil()) -> c_6() divide_ys#1#(x2,x1) -> c_7(take#2#(x1,x2),drop#2#(x1,x2)) drop#2#(0(),x2) -> c_8() drop#2#(S(x10),Cons(x56,x64)) -> c_9(drop#2#(x10,x64)) drop#2#(S(0()),Nil()) -> c_10() halve#1#(0()) -> c_11() halve#1#(S(0())) -> c_12() halve#1#(S(S(x14))) -> c_13(halve#1#(x14)) length#1#(Cons(x6,x8)) -> c_14(length#1#(x8)) length#1#(Nil()) -> c_15() leq#2#(0(),x16) -> c_16() leq#2#(S(x20),0()) -> c_17() leq#2#(S(x4),S(x2)) -> c_18(leq#2#(x4,x2)) main#(x113) -> c_19(dc#1#(map(),divisible(),mergesort_zs_3(),divide(),const_f(),x113)) map#2#(dc(x2,x4,x6,x8,x10),Nil()) -> c_20() map#2#(dc(x6,x8,x10,x12,x14),Cons(x4,x2)) -> c_21(dc#1#(x6,x8,x10,x12,x14,x4) ,map#2#(dc(x6,x8,x10,x12,x14),x2)) merge#2#(Cons(x4,x2),Nil()) -> c_22() merge#2#(Cons(x8,x6),Cons(x4,x2)) -> c_23(cond_merge_ys_zs_2#(leq#2(x8,x4) ,Cons(x8,x6) ,Cons(x4,x2) ,x8 ,x6 ,x4 ,x2) ,leq#2#(x8,x4)) merge#2#(Nil(),x2) -> c_24() take#2#(0(),x2) -> c_25() take#2#(S(x22),Cons(x56,x64)) -> c_26(take#2#(x22,x64)) take#2#(S(0()),Nil()) -> c_27() * Step 3: PredecessorEstimation MAYBE + Considered Problem: - Strict DPs: cond_merge_ys_zs_2#(False(),Cons(x7,x8),Cons(x5,x6),x4,x3,x2,x1) -> c_1(merge#2#(Cons(x7,x8),x1)) cond_merge_ys_zs_2#(True(),Cons(x7,x8),Cons(x5,x6),x4,x3,x2,x1) -> c_2(merge#2#(x3,Cons(x5,x6))) const_f#2#(x3,Cons(x6,Cons(x4,x2))) -> c_3(merge#2#(x6,x4)) dc#1#(map(),divisible(),mergesort_zs_3(),divide(),const_f(),Cons(x229,Nil())) -> c_4() dc#1#(map(),divisible(),mergesort_zs_3(),divide(),const_f(),Cons(x51,Cons(x25,x33))) -> c_5(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)))))) ,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))))) ,divide_ys#1#(Cons(x51,Cons(x25,x33)),S(halve#1(length#1(x33)))) ,halve#1#(length#1(x33)) ,length#1#(x33)) dc#1#(map(),divisible(),mergesort_zs_3(),divide(),const_f(),Nil()) -> c_6() divide_ys#1#(x2,x1) -> c_7(take#2#(x1,x2),drop#2#(x1,x2)) drop#2#(0(),x2) -> c_8() drop#2#(S(x10),Cons(x56,x64)) -> c_9(drop#2#(x10,x64)) drop#2#(S(0()),Nil()) -> c_10() halve#1#(0()) -> c_11() halve#1#(S(0())) -> c_12() halve#1#(S(S(x14))) -> c_13(halve#1#(x14)) length#1#(Cons(x6,x8)) -> c_14(length#1#(x8)) length#1#(Nil()) -> c_15() leq#2#(0(),x16) -> c_16() leq#2#(S(x20),0()) -> c_17() leq#2#(S(x4),S(x2)) -> c_18(leq#2#(x4,x2)) main#(x113) -> c_19(dc#1#(map(),divisible(),mergesort_zs_3(),divide(),const_f(),x113)) map#2#(dc(x2,x4,x6,x8,x10),Nil()) -> c_20() map#2#(dc(x6,x8,x10,x12,x14),Cons(x4,x2)) -> c_21(dc#1#(x6,x8,x10,x12,x14,x4) ,map#2#(dc(x6,x8,x10,x12,x14),x2)) merge#2#(Cons(x4,x2),Nil()) -> c_22() merge#2#(Cons(x8,x6),Cons(x4,x2)) -> c_23(cond_merge_ys_zs_2#(leq#2(x8,x4) ,Cons(x8,x6) ,Cons(x4,x2) ,x8 ,x6 ,x4 ,x2) ,leq#2#(x8,x4)) merge#2#(Nil(),x2) -> c_24() take#2#(0(),x2) -> c_25() take#2#(S(x22),Cons(x56,x64)) -> c_26(take#2#(x22,x64)) take#2#(S(0()),Nil()) -> c_27() - Weak 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) 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,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,c_1/1,c_2/1,c_3/1,c_4/0,c_5/5,c_6/0 ,c_7/2,c_8/0,c_9/1,c_10/0,c_11/0,c_12/0,c_13/1,c_14/1,c_15/0,c_16/0,c_17/0,c_18/1,c_19/1,c_20/0,c_21/2 ,c_22/0,c_23/2,c_24/0,c_25/0,c_26/1,c_27/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: PredecessorEstimation {onSelection = all simple predecessor estimation selector} + Details: We estimate the number of application of {4,6,8,10,11,12,15,16,17,20,22,24,25,27} by application of Pre({4,6,8,10,11,12,15,16,17,20,22,24,25,27}) = {1,2,3,5,7,9,13,14,18,19,21,23,26}. Here rules are labelled as follows: 1: cond_merge_ys_zs_2#(False(),Cons(x7,x8),Cons(x5,x6),x4,x3,x2,x1) -> c_1(merge#2#(Cons(x7,x8),x1)) 2: cond_merge_ys_zs_2#(True(),Cons(x7,x8),Cons(x5,x6),x4,x3,x2,x1) -> c_2(merge#2#(x3,Cons(x5,x6))) 3: const_f#2#(x3,Cons(x6,Cons(x4,x2))) -> c_3(merge#2#(x6,x4)) 4: dc#1#(map(),divisible(),mergesort_zs_3(),divide(),const_f(),Cons(x229,Nil())) -> c_4() 5: dc#1#(map(),divisible(),mergesort_zs_3(),divide(),const_f(),Cons(x51,Cons(x25,x33))) -> c_5(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)))))) ,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))))) ,divide_ys#1#(Cons(x51,Cons(x25,x33)),S(halve#1(length#1(x33)))) ,halve#1#(length#1(x33)) ,length#1#(x33)) 6: dc#1#(map(),divisible(),mergesort_zs_3(),divide(),const_f(),Nil()) -> c_6() 7: divide_ys#1#(x2,x1) -> c_7(take#2#(x1,x2),drop#2#(x1,x2)) 8: drop#2#(0(),x2) -> c_8() 9: drop#2#(S(x10),Cons(x56,x64)) -> c_9(drop#2#(x10,x64)) 10: drop#2#(S(0()),Nil()) -> c_10() 11: halve#1#(0()) -> c_11() 12: halve#1#(S(0())) -> c_12() 13: halve#1#(S(S(x14))) -> c_13(halve#1#(x14)) 14: length#1#(Cons(x6,x8)) -> c_14(length#1#(x8)) 15: length#1#(Nil()) -> c_15() 16: leq#2#(0(),x16) -> c_16() 17: leq#2#(S(x20),0()) -> c_17() 18: leq#2#(S(x4),S(x2)) -> c_18(leq#2#(x4,x2)) 19: main#(x113) -> c_19(dc#1#(map(),divisible(),mergesort_zs_3(),divide(),const_f(),x113)) 20: map#2#(dc(x2,x4,x6,x8,x10),Nil()) -> c_20() 21: map#2#(dc(x6,x8,x10,x12,x14),Cons(x4,x2)) -> c_21(dc#1#(x6,x8,x10,x12,x14,x4) ,map#2#(dc(x6,x8,x10,x12,x14),x2)) 22: merge#2#(Cons(x4,x2),Nil()) -> c_22() 23: merge#2#(Cons(x8,x6),Cons(x4,x2)) -> c_23(cond_merge_ys_zs_2#(leq#2(x8,x4) ,Cons(x8,x6) ,Cons(x4,x2) ,x8 ,x6 ,x4 ,x2) ,leq#2#(x8,x4)) 24: merge#2#(Nil(),x2) -> c_24() 25: take#2#(0(),x2) -> c_25() 26: take#2#(S(x22),Cons(x56,x64)) -> c_26(take#2#(x22,x64)) 27: take#2#(S(0()),Nil()) -> c_27() * Step 4: RemoveWeakSuffixes MAYBE + Considered Problem: - Strict DPs: cond_merge_ys_zs_2#(False(),Cons(x7,x8),Cons(x5,x6),x4,x3,x2,x1) -> c_1(merge#2#(Cons(x7,x8),x1)) cond_merge_ys_zs_2#(True(),Cons(x7,x8),Cons(x5,x6),x4,x3,x2,x1) -> c_2(merge#2#(x3,Cons(x5,x6))) const_f#2#(x3,Cons(x6,Cons(x4,x2))) -> c_3(merge#2#(x6,x4)) dc#1#(map(),divisible(),mergesort_zs_3(),divide(),const_f(),Cons(x51,Cons(x25,x33))) -> c_5(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)))))) ,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))))) ,divide_ys#1#(Cons(x51,Cons(x25,x33)),S(halve#1(length#1(x33)))) ,halve#1#(length#1(x33)) ,length#1#(x33)) divide_ys#1#(x2,x1) -> c_7(take#2#(x1,x2),drop#2#(x1,x2)) drop#2#(S(x10),Cons(x56,x64)) -> c_9(drop#2#(x10,x64)) halve#1#(S(S(x14))) -> c_13(halve#1#(x14)) length#1#(Cons(x6,x8)) -> c_14(length#1#(x8)) leq#2#(S(x4),S(x2)) -> c_18(leq#2#(x4,x2)) main#(x113) -> c_19(dc#1#(map(),divisible(),mergesort_zs_3(),divide(),const_f(),x113)) map#2#(dc(x6,x8,x10,x12,x14),Cons(x4,x2)) -> c_21(dc#1#(x6,x8,x10,x12,x14,x4) ,map#2#(dc(x6,x8,x10,x12,x14),x2)) merge#2#(Cons(x8,x6),Cons(x4,x2)) -> c_23(cond_merge_ys_zs_2#(leq#2(x8,x4) ,Cons(x8,x6) ,Cons(x4,x2) ,x8 ,x6 ,x4 ,x2) ,leq#2#(x8,x4)) take#2#(S(x22),Cons(x56,x64)) -> c_26(take#2#(x22,x64)) - Weak DPs: dc#1#(map(),divisible(),mergesort_zs_3(),divide(),const_f(),Cons(x229,Nil())) -> c_4() dc#1#(map(),divisible(),mergesort_zs_3(),divide(),const_f(),Nil()) -> c_6() drop#2#(0(),x2) -> c_8() drop#2#(S(0()),Nil()) -> c_10() halve#1#(0()) -> c_11() halve#1#(S(0())) -> c_12() length#1#(Nil()) -> c_15() leq#2#(0(),x16) -> c_16() leq#2#(S(x20),0()) -> c_17() map#2#(dc(x2,x4,x6,x8,x10),Nil()) -> c_20() merge#2#(Cons(x4,x2),Nil()) -> c_22() merge#2#(Nil(),x2) -> c_24() take#2#(0(),x2) -> c_25() take#2#(S(0()),Nil()) -> c_27() - Weak 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) 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,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,c_1/1,c_2/1,c_3/1,c_4/0,c_5/5,c_6/0 ,c_7/2,c_8/0,c_9/1,c_10/0,c_11/0,c_12/0,c_13/1,c_14/1,c_15/0,c_16/0,c_17/0,c_18/1,c_19/1,c_20/0,c_21/2 ,c_22/0,c_23/2,c_24/0,c_25/0,c_26/1,c_27/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: RemoveWeakSuffixes + Details: Consider the dependency graph 1:S:cond_merge_ys_zs_2#(False(),Cons(x7,x8),Cons(x5,x6),x4,x3,x2,x1) -> c_1(merge#2#(Cons(x7,x8),x1)) -->_1 merge#2#(Cons(x8,x6),Cons(x4,x2)) -> c_23(cond_merge_ys_zs_2#(leq#2(x8,x4) ,Cons(x8,x6) ,Cons(x4,x2) ,x8 ,x6 ,x4 ,x2) ,leq#2#(x8,x4)):12 -->_1 merge#2#(Cons(x4,x2),Nil()) -> c_22():24 2:S:cond_merge_ys_zs_2#(True(),Cons(x7,x8),Cons(x5,x6),x4,x3,x2,x1) -> c_2(merge#2#(x3,Cons(x5,x6))) -->_1 merge#2#(Cons(x8,x6),Cons(x4,x2)) -> c_23(cond_merge_ys_zs_2#(leq#2(x8,x4) ,Cons(x8,x6) ,Cons(x4,x2) ,x8 ,x6 ,x4 ,x2) ,leq#2#(x8,x4)):12 -->_1 merge#2#(Nil(),x2) -> c_24():25 3:S:const_f#2#(x3,Cons(x6,Cons(x4,x2))) -> c_3(merge#2#(x6,x4)) -->_1 merge#2#(Cons(x8,x6),Cons(x4,x2)) -> c_23(cond_merge_ys_zs_2#(leq#2(x8,x4) ,Cons(x8,x6) ,Cons(x4,x2) ,x8 ,x6 ,x4 ,x2) ,leq#2#(x8,x4)):12 -->_1 merge#2#(Nil(),x2) -> c_24():25 -->_1 merge#2#(Cons(x4,x2),Nil()) -> c_22():24 4:S:dc#1#(map(),divisible(),mergesort_zs_3(),divide(),const_f(),Cons(x51,Cons(x25,x33))) -> c_5(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)))))) ,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))))) ,divide_ys#1#(Cons(x51,Cons(x25,x33)),S(halve#1(length#1(x33)))) ,halve#1#(length#1(x33)) ,length#1#(x33)) -->_2 map#2#(dc(x6,x8,x10,x12,x14),Cons(x4,x2)) -> c_21(dc#1#(x6,x8,x10,x12,x14,x4) ,map#2#(dc(x6,x8,x10,x12,x14),x2)):11 -->_5 length#1#(Cons(x6,x8)) -> c_14(length#1#(x8)):8 -->_4 halve#1#(S(S(x14))) -> c_13(halve#1#(x14)):7 -->_3 divide_ys#1#(x2,x1) -> c_7(take#2#(x1,x2),drop#2#(x1,x2)):5 -->_2 map#2#(dc(x2,x4,x6,x8,x10),Nil()) -> c_20():23 -->_5 length#1#(Nil()) -> c_15():20 -->_4 halve#1#(S(0())) -> c_12():19 -->_4 halve#1#(0()) -> c_11():18 -->_1 const_f#2#(x3,Cons(x6,Cons(x4,x2))) -> c_3(merge#2#(x6,x4)):3 5:S:divide_ys#1#(x2,x1) -> c_7(take#2#(x1,x2),drop#2#(x1,x2)) -->_1 take#2#(S(x22),Cons(x56,x64)) -> c_26(take#2#(x22,x64)):13 -->_2 drop#2#(S(x10),Cons(x56,x64)) -> c_9(drop#2#(x10,x64)):6 -->_1 take#2#(S(0()),Nil()) -> c_27():27 -->_1 take#2#(0(),x2) -> c_25():26 -->_2 drop#2#(S(0()),Nil()) -> c_10():17 -->_2 drop#2#(0(),x2) -> c_8():16 6:S:drop#2#(S(x10),Cons(x56,x64)) -> c_9(drop#2#(x10,x64)) -->_1 drop#2#(S(0()),Nil()) -> c_10():17 -->_1 drop#2#(0(),x2) -> c_8():16 -->_1 drop#2#(S(x10),Cons(x56,x64)) -> c_9(drop#2#(x10,x64)):6 7:S:halve#1#(S(S(x14))) -> c_13(halve#1#(x14)) -->_1 halve#1#(S(0())) -> c_12():19 -->_1 halve#1#(0()) -> c_11():18 -->_1 halve#1#(S(S(x14))) -> c_13(halve#1#(x14)):7 8:S:length#1#(Cons(x6,x8)) -> c_14(length#1#(x8)) -->_1 length#1#(Nil()) -> c_15():20 -->_1 length#1#(Cons(x6,x8)) -> c_14(length#1#(x8)):8 9:S:leq#2#(S(x4),S(x2)) -> c_18(leq#2#(x4,x2)) -->_1 leq#2#(S(x20),0()) -> c_17():22 -->_1 leq#2#(0(),x16) -> c_16():21 -->_1 leq#2#(S(x4),S(x2)) -> c_18(leq#2#(x4,x2)):9 10:S:main#(x113) -> c_19(dc#1#(map(),divisible(),mergesort_zs_3(),divide(),const_f(),x113)) -->_1 dc#1#(map(),divisible(),mergesort_zs_3(),divide(),const_f(),Nil()) -> c_6():15 -->_1 dc#1#(map(),divisible(),mergesort_zs_3(),divide(),const_f(),Cons(x229,Nil())) -> c_4():14 -->_1 dc#1#(map(),divisible(),mergesort_zs_3(),divide(),const_f(),Cons(x51,Cons(x25,x33))) -> c_5(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)))))) ,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))))) ,divide_ys#1#(Cons(x51,Cons(x25,x33)),S(halve#1(length#1(x33)))) ,halve#1#(length#1(x33)) ,length#1#(x33)):4 11:S:map#2#(dc(x6,x8,x10,x12,x14),Cons(x4,x2)) -> c_21(dc#1#(x6,x8,x10,x12,x14,x4) ,map#2#(dc(x6,x8,x10,x12,x14),x2)) -->_2 map#2#(dc(x2,x4,x6,x8,x10),Nil()) -> c_20():23 -->_1 dc#1#(map(),divisible(),mergesort_zs_3(),divide(),const_f(),Nil()) -> c_6():15 -->_1 dc#1#(map(),divisible(),mergesort_zs_3(),divide(),const_f(),Cons(x229,Nil())) -> c_4():14 -->_2 map#2#(dc(x6,x8,x10,x12,x14),Cons(x4,x2)) -> c_21(dc#1#(x6,x8,x10,x12,x14,x4) ,map#2#(dc(x6,x8,x10,x12,x14),x2)):11 -->_1 dc#1#(map(),divisible(),mergesort_zs_3(),divide(),const_f(),Cons(x51,Cons(x25,x33))) -> c_5(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)))))) ,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))))) ,divide_ys#1#(Cons(x51,Cons(x25,x33)),S(halve#1(length#1(x33)))) ,halve#1#(length#1(x33)) ,length#1#(x33)):4 12:S:merge#2#(Cons(x8,x6),Cons(x4,x2)) -> c_23(cond_merge_ys_zs_2#(leq#2(x8,x4) ,Cons(x8,x6) ,Cons(x4,x2) ,x8 ,x6 ,x4 ,x2) ,leq#2#(x8,x4)) -->_2 leq#2#(S(x20),0()) -> c_17():22 -->_2 leq#2#(0(),x16) -> c_16():21 -->_2 leq#2#(S(x4),S(x2)) -> c_18(leq#2#(x4,x2)):9 -->_1 cond_merge_ys_zs_2#(True(),Cons(x7,x8),Cons(x5,x6),x4,x3,x2,x1) -> c_2(merge#2#(x3,Cons(x5,x6))):2 -->_1 cond_merge_ys_zs_2#(False(),Cons(x7,x8),Cons(x5,x6),x4,x3,x2,x1) -> c_1(merge#2#(Cons(x7,x8),x1)):1 13:S:take#2#(S(x22),Cons(x56,x64)) -> c_26(take#2#(x22,x64)) -->_1 take#2#(S(0()),Nil()) -> c_27():27 -->_1 take#2#(0(),x2) -> c_25():26 -->_1 take#2#(S(x22),Cons(x56,x64)) -> c_26(take#2#(x22,x64)):13 14:W:dc#1#(map(),divisible(),mergesort_zs_3(),divide(),const_f(),Cons(x229,Nil())) -> c_4() 15:W:dc#1#(map(),divisible(),mergesort_zs_3(),divide(),const_f(),Nil()) -> c_6() 16:W:drop#2#(0(),x2) -> c_8() 17:W:drop#2#(S(0()),Nil()) -> c_10() 18:W:halve#1#(0()) -> c_11() 19:W:halve#1#(S(0())) -> c_12() 20:W:length#1#(Nil()) -> c_15() 21:W:leq#2#(0(),x16) -> c_16() 22:W:leq#2#(S(x20),0()) -> c_17() 23:W:map#2#(dc(x2,x4,x6,x8,x10),Nil()) -> c_20() 24:W:merge#2#(Cons(x4,x2),Nil()) -> c_22() 25:W:merge#2#(Nil(),x2) -> c_24() 26:W:take#2#(0(),x2) -> c_25() 27:W:take#2#(S(0()),Nil()) -> c_27() The following weak DPs constitute a sub-graph of the DG that is closed under successors. The DPs are removed. 16: drop#2#(0(),x2) -> c_8() 17: drop#2#(S(0()),Nil()) -> c_10() 26: take#2#(0(),x2) -> c_25() 27: take#2#(S(0()),Nil()) -> c_27() 18: halve#1#(0()) -> c_11() 19: halve#1#(S(0())) -> c_12() 20: length#1#(Nil()) -> c_15() 14: dc#1#(map(),divisible(),mergesort_zs_3(),divide(),const_f(),Cons(x229,Nil())) -> c_4() 15: dc#1#(map(),divisible(),mergesort_zs_3(),divide(),const_f(),Nil()) -> c_6() 23: map#2#(dc(x2,x4,x6,x8,x10),Nil()) -> c_20() 24: merge#2#(Cons(x4,x2),Nil()) -> c_22() 25: merge#2#(Nil(),x2) -> c_24() 21: leq#2#(0(),x16) -> c_16() 22: leq#2#(S(x20),0()) -> c_17() * Step 5: RemoveHeads MAYBE + Considered Problem: - Strict DPs: cond_merge_ys_zs_2#(False(),Cons(x7,x8),Cons(x5,x6),x4,x3,x2,x1) -> c_1(merge#2#(Cons(x7,x8),x1)) cond_merge_ys_zs_2#(True(),Cons(x7,x8),Cons(x5,x6),x4,x3,x2,x1) -> c_2(merge#2#(x3,Cons(x5,x6))) const_f#2#(x3,Cons(x6,Cons(x4,x2))) -> c_3(merge#2#(x6,x4)) dc#1#(map(),divisible(),mergesort_zs_3(),divide(),const_f(),Cons(x51,Cons(x25,x33))) -> c_5(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)))))) ,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))))) ,divide_ys#1#(Cons(x51,Cons(x25,x33)),S(halve#1(length#1(x33)))) ,halve#1#(length#1(x33)) ,length#1#(x33)) divide_ys#1#(x2,x1) -> c_7(take#2#(x1,x2),drop#2#(x1,x2)) drop#2#(S(x10),Cons(x56,x64)) -> c_9(drop#2#(x10,x64)) halve#1#(S(S(x14))) -> c_13(halve#1#(x14)) length#1#(Cons(x6,x8)) -> c_14(length#1#(x8)) leq#2#(S(x4),S(x2)) -> c_18(leq#2#(x4,x2)) main#(x113) -> c_19(dc#1#(map(),divisible(),mergesort_zs_3(),divide(),const_f(),x113)) map#2#(dc(x6,x8,x10,x12,x14),Cons(x4,x2)) -> c_21(dc#1#(x6,x8,x10,x12,x14,x4) ,map#2#(dc(x6,x8,x10,x12,x14),x2)) merge#2#(Cons(x8,x6),Cons(x4,x2)) -> c_23(cond_merge_ys_zs_2#(leq#2(x8,x4) ,Cons(x8,x6) ,Cons(x4,x2) ,x8 ,x6 ,x4 ,x2) ,leq#2#(x8,x4)) take#2#(S(x22),Cons(x56,x64)) -> c_26(take#2#(x22,x64)) - Weak 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) 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,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,c_1/1,c_2/1,c_3/1,c_4/0,c_5/5,c_6/0 ,c_7/2,c_8/0,c_9/1,c_10/0,c_11/0,c_12/0,c_13/1,c_14/1,c_15/0,c_16/0,c_17/0,c_18/1,c_19/1,c_20/0,c_21/2 ,c_22/0,c_23/2,c_24/0,c_25/0,c_26/1,c_27/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: RemoveHeads + Details: Consider the dependency graph 1:S:cond_merge_ys_zs_2#(False(),Cons(x7,x8),Cons(x5,x6),x4,x3,x2,x1) -> c_1(merge#2#(Cons(x7,x8),x1)) -->_1 merge#2#(Cons(x8,x6),Cons(x4,x2)) -> c_23(cond_merge_ys_zs_2#(leq#2(x8,x4) ,Cons(x8,x6) ,Cons(x4,x2) ,x8 ,x6 ,x4 ,x2) ,leq#2#(x8,x4)):12 2:S:cond_merge_ys_zs_2#(True(),Cons(x7,x8),Cons(x5,x6),x4,x3,x2,x1) -> c_2(merge#2#(x3,Cons(x5,x6))) -->_1 merge#2#(Cons(x8,x6),Cons(x4,x2)) -> c_23(cond_merge_ys_zs_2#(leq#2(x8,x4) ,Cons(x8,x6) ,Cons(x4,x2) ,x8 ,x6 ,x4 ,x2) ,leq#2#(x8,x4)):12 3:S:const_f#2#(x3,Cons(x6,Cons(x4,x2))) -> c_3(merge#2#(x6,x4)) -->_1 merge#2#(Cons(x8,x6),Cons(x4,x2)) -> c_23(cond_merge_ys_zs_2#(leq#2(x8,x4) ,Cons(x8,x6) ,Cons(x4,x2) ,x8 ,x6 ,x4 ,x2) ,leq#2#(x8,x4)):12 4:S:dc#1#(map(),divisible(),mergesort_zs_3(),divide(),const_f(),Cons(x51,Cons(x25,x33))) -> c_5(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)))))) ,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))))) ,divide_ys#1#(Cons(x51,Cons(x25,x33)),S(halve#1(length#1(x33)))) ,halve#1#(length#1(x33)) ,length#1#(x33)) -->_2 map#2#(dc(x6,x8,x10,x12,x14),Cons(x4,x2)) -> c_21(dc#1#(x6,x8,x10,x12,x14,x4) ,map#2#(dc(x6,x8,x10,x12,x14),x2)):11 -->_5 length#1#(Cons(x6,x8)) -> c_14(length#1#(x8)):8 -->_4 halve#1#(S(S(x14))) -> c_13(halve#1#(x14)):7 -->_3 divide_ys#1#(x2,x1) -> c_7(take#2#(x1,x2),drop#2#(x1,x2)):5 -->_1 const_f#2#(x3,Cons(x6,Cons(x4,x2))) -> c_3(merge#2#(x6,x4)):3 5:S:divide_ys#1#(x2,x1) -> c_7(take#2#(x1,x2),drop#2#(x1,x2)) -->_1 take#2#(S(x22),Cons(x56,x64)) -> c_26(take#2#(x22,x64)):13 -->_2 drop#2#(S(x10),Cons(x56,x64)) -> c_9(drop#2#(x10,x64)):6 6:S:drop#2#(S(x10),Cons(x56,x64)) -> c_9(drop#2#(x10,x64)) -->_1 drop#2#(S(x10),Cons(x56,x64)) -> c_9(drop#2#(x10,x64)):6 7:S:halve#1#(S(S(x14))) -> c_13(halve#1#(x14)) -->_1 halve#1#(S(S(x14))) -> c_13(halve#1#(x14)):7 8:S:length#1#(Cons(x6,x8)) -> c_14(length#1#(x8)) -->_1 length#1#(Cons(x6,x8)) -> c_14(length#1#(x8)):8 9:S:leq#2#(S(x4),S(x2)) -> c_18(leq#2#(x4,x2)) -->_1 leq#2#(S(x4),S(x2)) -> c_18(leq#2#(x4,x2)):9 10:S:main#(x113) -> c_19(dc#1#(map(),divisible(),mergesort_zs_3(),divide(),const_f(),x113)) -->_1 dc#1#(map(),divisible(),mergesort_zs_3(),divide(),const_f(),Cons(x51,Cons(x25,x33))) -> c_5(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)))))) ,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))))) ,divide_ys#1#(Cons(x51,Cons(x25,x33)),S(halve#1(length#1(x33)))) ,halve#1#(length#1(x33)) ,length#1#(x33)):4 11:S:map#2#(dc(x6,x8,x10,x12,x14),Cons(x4,x2)) -> c_21(dc#1#(x6,x8,x10,x12,x14,x4) ,map#2#(dc(x6,x8,x10,x12,x14),x2)) -->_2 map#2#(dc(x6,x8,x10,x12,x14),Cons(x4,x2)) -> c_21(dc#1#(x6,x8,x10,x12,x14,x4) ,map#2#(dc(x6,x8,x10,x12,x14),x2)):11 -->_1 dc#1#(map(),divisible(),mergesort_zs_3(),divide(),const_f(),Cons(x51,Cons(x25,x33))) -> c_5(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)))))) ,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))))) ,divide_ys#1#(Cons(x51,Cons(x25,x33)),S(halve#1(length#1(x33)))) ,halve#1#(length#1(x33)) ,length#1#(x33)):4 12:S:merge#2#(Cons(x8,x6),Cons(x4,x2)) -> c_23(cond_merge_ys_zs_2#(leq#2(x8,x4) ,Cons(x8,x6) ,Cons(x4,x2) ,x8 ,x6 ,x4 ,x2) ,leq#2#(x8,x4)) -->_2 leq#2#(S(x4),S(x2)) -> c_18(leq#2#(x4,x2)):9 -->_1 cond_merge_ys_zs_2#(True(),Cons(x7,x8),Cons(x5,x6),x4,x3,x2,x1) -> c_2(merge#2#(x3,Cons(x5,x6))):2 -->_1 cond_merge_ys_zs_2#(False(),Cons(x7,x8),Cons(x5,x6),x4,x3,x2,x1) -> c_1(merge#2#(Cons(x7,x8),x1)):1 13:S:take#2#(S(x22),Cons(x56,x64)) -> c_26(take#2#(x22,x64)) -->_1 take#2#(S(x22),Cons(x56,x64)) -> c_26(take#2#(x22,x64)):13 Following roots of the dependency graph are removed, as the considered set of starting terms is closed under reduction with respect to these rules (modulo compound contexts). [(10,main#(x113) -> c_19(dc#1#(map(),divisible(),mergesort_zs_3(),divide(),const_f(),x113)))] * Step 6: Failure MAYBE + Considered Problem: - Strict DPs: cond_merge_ys_zs_2#(False(),Cons(x7,x8),Cons(x5,x6),x4,x3,x2,x1) -> c_1(merge#2#(Cons(x7,x8),x1)) cond_merge_ys_zs_2#(True(),Cons(x7,x8),Cons(x5,x6),x4,x3,x2,x1) -> c_2(merge#2#(x3,Cons(x5,x6))) const_f#2#(x3,Cons(x6,Cons(x4,x2))) -> c_3(merge#2#(x6,x4)) dc#1#(map(),divisible(),mergesort_zs_3(),divide(),const_f(),Cons(x51,Cons(x25,x33))) -> c_5(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)))))) ,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))))) ,divide_ys#1#(Cons(x51,Cons(x25,x33)),S(halve#1(length#1(x33)))) ,halve#1#(length#1(x33)) ,length#1#(x33)) divide_ys#1#(x2,x1) -> c_7(take#2#(x1,x2),drop#2#(x1,x2)) drop#2#(S(x10),Cons(x56,x64)) -> c_9(drop#2#(x10,x64)) halve#1#(S(S(x14))) -> c_13(halve#1#(x14)) length#1#(Cons(x6,x8)) -> c_14(length#1#(x8)) leq#2#(S(x4),S(x2)) -> c_18(leq#2#(x4,x2)) map#2#(dc(x6,x8,x10,x12,x14),Cons(x4,x2)) -> c_21(dc#1#(x6,x8,x10,x12,x14,x4) ,map#2#(dc(x6,x8,x10,x12,x14),x2)) merge#2#(Cons(x8,x6),Cons(x4,x2)) -> c_23(cond_merge_ys_zs_2#(leq#2(x8,x4) ,Cons(x8,x6) ,Cons(x4,x2) ,x8 ,x6 ,x4 ,x2) ,leq#2#(x8,x4)) take#2#(S(x22),Cons(x56,x64)) -> c_26(take#2#(x22,x64)) - Weak 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) 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,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,c_1/1,c_2/1,c_3/1,c_4/0,c_5/5,c_6/0 ,c_7/2,c_8/0,c_9/1,c_10/0,c_11/0,c_12/0,c_13/1,c_14/1,c_15/0,c_16/0,c_17/0,c_18/1,c_19/1,c_20/0,c_21/2 ,c_22/0,c_23/2,c_24/0,c_25/0,c_26/1,c_27/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: EmptyProcessor + Details: The problem is still open. MAYBE