WORST_CASE(?,O(n^2)) * Step 1: DependencyPairs WORST_CASE(?,O(n^2)) + Considered Problem: - Strict TRS: #equal(@x,@y) -> #eq(@x,@y) #less(@x,@y) -> #cklt(#compare(@x,@y)) and(@x,@y) -> #and(@x,@y) insert(@x,@l) -> insert#1(@l,@x) insert#1(::(@y,@ys),@x) -> insert#2(leq(@x,@y),@x,@y,@ys) insert#1(nil(),@x) -> ::(@x,nil()) insert#2(#false(),@x,@y,@ys) -> ::(@y,insert(@x,@ys)) insert#2(#true(),@x,@y,@ys) -> ::(@x,::(@y,@ys)) isortlist(@l) -> isortlist#1(@l) isortlist#1(::(@x,@xs)) -> insert(@x,isortlist(@xs)) isortlist#1(nil()) -> nil() leq(@l1,@l2) -> leq#1(@l1,@l2) leq#1(::(@x,@xs),@l2) -> leq#2(@l2,@x,@xs) leq#1(nil(),@l2) -> #true() leq#2(::(@y,@ys),@x,@xs) -> or(#less(@x,@y),and(#equal(@x,@y),leq(@xs,@ys))) leq#2(nil(),@x,@xs) -> #false() or(@x,@y) -> #or(@x,@y) - Weak TRS: #and(#false(),#false()) -> #false() #and(#false(),#true()) -> #false() #and(#true(),#false()) -> #false() #and(#true(),#true()) -> #true() #cklt(#EQ()) -> #false() #cklt(#GT()) -> #false() #cklt(#LT()) -> #true() #compare(#0(),#0()) -> #EQ() #compare(#0(),#neg(@y)) -> #GT() #compare(#0(),#pos(@y)) -> #LT() #compare(#0(),#s(@y)) -> #LT() #compare(#neg(@x),#0()) -> #LT() #compare(#neg(@x),#neg(@y)) -> #compare(@y,@x) #compare(#neg(@x),#pos(@y)) -> #LT() #compare(#pos(@x),#0()) -> #GT() #compare(#pos(@x),#neg(@y)) -> #GT() #compare(#pos(@x),#pos(@y)) -> #compare(@x,@y) #compare(#s(@x),#0()) -> #GT() #compare(#s(@x),#s(@y)) -> #compare(@x,@y) #eq(#0(),#0()) -> #true() #eq(#0(),#neg(@y)) -> #false() #eq(#0(),#pos(@y)) -> #false() #eq(#0(),#s(@y)) -> #false() #eq(#neg(@x),#0()) -> #false() #eq(#neg(@x),#neg(@y)) -> #eq(@x,@y) #eq(#neg(@x),#pos(@y)) -> #false() #eq(#pos(@x),#0()) -> #false() #eq(#pos(@x),#neg(@y)) -> #false() #eq(#pos(@x),#pos(@y)) -> #eq(@x,@y) #eq(#s(@x),#0()) -> #false() #eq(#s(@x),#s(@y)) -> #eq(@x,@y) #eq(::(@x_1,@x_2),::(@y_1,@y_2)) -> #and(#eq(@x_1,@y_1),#eq(@x_2,@y_2)) #eq(::(@x_1,@x_2),nil()) -> #false() #eq(nil(),::(@y_1,@y_2)) -> #false() #eq(nil(),nil()) -> #true() #or(#false(),#false()) -> #false() #or(#false(),#true()) -> #true() #or(#true(),#false()) -> #true() #or(#true(),#true()) -> #true() - Signature: {#and/2,#cklt/1,#compare/2,#eq/2,#equal/2,#less/2,#or/2,and/2,insert/2,insert#1/2,insert#2/4,isortlist/1 ,isortlist#1/1,leq/2,leq#1/2,leq#2/3,or/2} / {#0/0,#EQ/0,#GT/0,#LT/0,#false/0,#neg/1,#pos/1,#s/1,#true/0 ,::/2,nil/0} - Obligation: innermost runtime complexity wrt. defined symbols {#and,#cklt,#compare,#eq,#equal,#less,#or,and,insert ,insert#1,insert#2,isortlist,isortlist#1,leq,leq#1,leq#2,or} and constructors {#0,#EQ,#GT,#LT,#false,#neg ,#pos,#s,#true,::,nil} + Applied Processor: DependencyPairs {dpKind_ = DT} + Details: We add the following dependency tuples: Strict DPs #equal#(@x,@y) -> c_1(#eq#(@x,@y)) #less#(@x,@y) -> c_2(#cklt#(#compare(@x,@y)),#compare#(@x,@y)) and#(@x,@y) -> c_3(#and#(@x,@y)) insert#(@x,@l) -> c_4(insert#1#(@l,@x)) insert#1#(::(@y,@ys),@x) -> c_5(insert#2#(leq(@x,@y),@x,@y,@ys),leq#(@x,@y)) insert#1#(nil(),@x) -> c_6() insert#2#(#false(),@x,@y,@ys) -> c_7(insert#(@x,@ys)) insert#2#(#true(),@x,@y,@ys) -> c_8() isortlist#(@l) -> c_9(isortlist#1#(@l)) isortlist#1#(::(@x,@xs)) -> c_10(insert#(@x,isortlist(@xs)),isortlist#(@xs)) isortlist#1#(nil()) -> c_11() leq#(@l1,@l2) -> c_12(leq#1#(@l1,@l2)) leq#1#(::(@x,@xs),@l2) -> c_13(leq#2#(@l2,@x,@xs)) leq#1#(nil(),@l2) -> c_14() leq#2#(::(@y,@ys),@x,@xs) -> c_15(or#(#less(@x,@y),and(#equal(@x,@y),leq(@xs,@ys))) ,#less#(@x,@y) ,and#(#equal(@x,@y),leq(@xs,@ys)) ,#equal#(@x,@y) ,leq#(@xs,@ys)) leq#2#(nil(),@x,@xs) -> c_16() or#(@x,@y) -> c_17(#or#(@x,@y)) Weak DPs #and#(#false(),#false()) -> c_18() #and#(#false(),#true()) -> c_19() #and#(#true(),#false()) -> c_20() #and#(#true(),#true()) -> c_21() #cklt#(#EQ()) -> c_22() #cklt#(#GT()) -> c_23() #cklt#(#LT()) -> c_24() #compare#(#0(),#0()) -> c_25() #compare#(#0(),#neg(@y)) -> c_26() #compare#(#0(),#pos(@y)) -> c_27() #compare#(#0(),#s(@y)) -> c_28() #compare#(#neg(@x),#0()) -> c_29() #compare#(#neg(@x),#neg(@y)) -> c_30(#compare#(@y,@x)) #compare#(#neg(@x),#pos(@y)) -> c_31() #compare#(#pos(@x),#0()) -> c_32() #compare#(#pos(@x),#neg(@y)) -> c_33() #compare#(#pos(@x),#pos(@y)) -> c_34(#compare#(@x,@y)) #compare#(#s(@x),#0()) -> c_35() #compare#(#s(@x),#s(@y)) -> c_36(#compare#(@x,@y)) #eq#(#0(),#0()) -> c_37() #eq#(#0(),#neg(@y)) -> c_38() #eq#(#0(),#pos(@y)) -> c_39() #eq#(#0(),#s(@y)) -> c_40() #eq#(#neg(@x),#0()) -> c_41() #eq#(#neg(@x),#neg(@y)) -> c_42(#eq#(@x,@y)) #eq#(#neg(@x),#pos(@y)) -> c_43() #eq#(#pos(@x),#0()) -> c_44() #eq#(#pos(@x),#neg(@y)) -> c_45() #eq#(#pos(@x),#pos(@y)) -> c_46(#eq#(@x,@y)) #eq#(#s(@x),#0()) -> c_47() #eq#(#s(@x),#s(@y)) -> c_48(#eq#(@x,@y)) #eq#(::(@x_1,@x_2),::(@y_1,@y_2)) -> c_49(#and#(#eq(@x_1,@y_1),#eq(@x_2,@y_2)) ,#eq#(@x_1,@y_1) ,#eq#(@x_2,@y_2)) #eq#(::(@x_1,@x_2),nil()) -> c_50() #eq#(nil(),::(@y_1,@y_2)) -> c_51() #eq#(nil(),nil()) -> c_52() #or#(#false(),#false()) -> c_53() #or#(#false(),#true()) -> c_54() #or#(#true(),#false()) -> c_55() #or#(#true(),#true()) -> c_56() and mark the set of starting terms. * Step 2: PredecessorEstimation WORST_CASE(?,O(n^2)) + Considered Problem: - Strict DPs: #equal#(@x,@y) -> c_1(#eq#(@x,@y)) #less#(@x,@y) -> c_2(#cklt#(#compare(@x,@y)),#compare#(@x,@y)) and#(@x,@y) -> c_3(#and#(@x,@y)) insert#(@x,@l) -> c_4(insert#1#(@l,@x)) insert#1#(::(@y,@ys),@x) -> c_5(insert#2#(leq(@x,@y),@x,@y,@ys),leq#(@x,@y)) insert#1#(nil(),@x) -> c_6() insert#2#(#false(),@x,@y,@ys) -> c_7(insert#(@x,@ys)) insert#2#(#true(),@x,@y,@ys) -> c_8() isortlist#(@l) -> c_9(isortlist#1#(@l)) isortlist#1#(::(@x,@xs)) -> c_10(insert#(@x,isortlist(@xs)),isortlist#(@xs)) isortlist#1#(nil()) -> c_11() leq#(@l1,@l2) -> c_12(leq#1#(@l1,@l2)) leq#1#(::(@x,@xs),@l2) -> c_13(leq#2#(@l2,@x,@xs)) leq#1#(nil(),@l2) -> c_14() leq#2#(::(@y,@ys),@x,@xs) -> c_15(or#(#less(@x,@y),and(#equal(@x,@y),leq(@xs,@ys))) ,#less#(@x,@y) ,and#(#equal(@x,@y),leq(@xs,@ys)) ,#equal#(@x,@y) ,leq#(@xs,@ys)) leq#2#(nil(),@x,@xs) -> c_16() or#(@x,@y) -> c_17(#or#(@x,@y)) - Weak DPs: #and#(#false(),#false()) -> c_18() #and#(#false(),#true()) -> c_19() #and#(#true(),#false()) -> c_20() #and#(#true(),#true()) -> c_21() #cklt#(#EQ()) -> c_22() #cklt#(#GT()) -> c_23() #cklt#(#LT()) -> c_24() #compare#(#0(),#0()) -> c_25() #compare#(#0(),#neg(@y)) -> c_26() #compare#(#0(),#pos(@y)) -> c_27() #compare#(#0(),#s(@y)) -> c_28() #compare#(#neg(@x),#0()) -> c_29() #compare#(#neg(@x),#neg(@y)) -> c_30(#compare#(@y,@x)) #compare#(#neg(@x),#pos(@y)) -> c_31() #compare#(#pos(@x),#0()) -> c_32() #compare#(#pos(@x),#neg(@y)) -> c_33() #compare#(#pos(@x),#pos(@y)) -> c_34(#compare#(@x,@y)) #compare#(#s(@x),#0()) -> c_35() #compare#(#s(@x),#s(@y)) -> c_36(#compare#(@x,@y)) #eq#(#0(),#0()) -> c_37() #eq#(#0(),#neg(@y)) -> c_38() #eq#(#0(),#pos(@y)) -> c_39() #eq#(#0(),#s(@y)) -> c_40() #eq#(#neg(@x),#0()) -> c_41() #eq#(#neg(@x),#neg(@y)) -> c_42(#eq#(@x,@y)) #eq#(#neg(@x),#pos(@y)) -> c_43() #eq#(#pos(@x),#0()) -> c_44() #eq#(#pos(@x),#neg(@y)) -> c_45() #eq#(#pos(@x),#pos(@y)) -> c_46(#eq#(@x,@y)) #eq#(#s(@x),#0()) -> c_47() #eq#(#s(@x),#s(@y)) -> c_48(#eq#(@x,@y)) #eq#(::(@x_1,@x_2),::(@y_1,@y_2)) -> c_49(#and#(#eq(@x_1,@y_1),#eq(@x_2,@y_2)) ,#eq#(@x_1,@y_1) ,#eq#(@x_2,@y_2)) #eq#(::(@x_1,@x_2),nil()) -> c_50() #eq#(nil(),::(@y_1,@y_2)) -> c_51() #eq#(nil(),nil()) -> c_52() #or#(#false(),#false()) -> c_53() #or#(#false(),#true()) -> c_54() #or#(#true(),#false()) -> c_55() #or#(#true(),#true()) -> c_56() - Weak TRS: #and(#false(),#false()) -> #false() #and(#false(),#true()) -> #false() #and(#true(),#false()) -> #false() #and(#true(),#true()) -> #true() #cklt(#EQ()) -> #false() #cklt(#GT()) -> #false() #cklt(#LT()) -> #true() #compare(#0(),#0()) -> #EQ() #compare(#0(),#neg(@y)) -> #GT() #compare(#0(),#pos(@y)) -> #LT() #compare(#0(),#s(@y)) -> #LT() #compare(#neg(@x),#0()) -> #LT() #compare(#neg(@x),#neg(@y)) -> #compare(@y,@x) #compare(#neg(@x),#pos(@y)) -> #LT() #compare(#pos(@x),#0()) -> #GT() #compare(#pos(@x),#neg(@y)) -> #GT() #compare(#pos(@x),#pos(@y)) -> #compare(@x,@y) #compare(#s(@x),#0()) -> #GT() #compare(#s(@x),#s(@y)) -> #compare(@x,@y) #eq(#0(),#0()) -> #true() #eq(#0(),#neg(@y)) -> #false() #eq(#0(),#pos(@y)) -> #false() #eq(#0(),#s(@y)) -> #false() #eq(#neg(@x),#0()) -> #false() #eq(#neg(@x),#neg(@y)) -> #eq(@x,@y) #eq(#neg(@x),#pos(@y)) -> #false() #eq(#pos(@x),#0()) -> #false() #eq(#pos(@x),#neg(@y)) -> #false() #eq(#pos(@x),#pos(@y)) -> #eq(@x,@y) #eq(#s(@x),#0()) -> #false() #eq(#s(@x),#s(@y)) -> #eq(@x,@y) #eq(::(@x_1,@x_2),::(@y_1,@y_2)) -> #and(#eq(@x_1,@y_1),#eq(@x_2,@y_2)) #eq(::(@x_1,@x_2),nil()) -> #false() #eq(nil(),::(@y_1,@y_2)) -> #false() #eq(nil(),nil()) -> #true() #equal(@x,@y) -> #eq(@x,@y) #less(@x,@y) -> #cklt(#compare(@x,@y)) #or(#false(),#false()) -> #false() #or(#false(),#true()) -> #true() #or(#true(),#false()) -> #true() #or(#true(),#true()) -> #true() and(@x,@y) -> #and(@x,@y) insert(@x,@l) -> insert#1(@l,@x) insert#1(::(@y,@ys),@x) -> insert#2(leq(@x,@y),@x,@y,@ys) insert#1(nil(),@x) -> ::(@x,nil()) insert#2(#false(),@x,@y,@ys) -> ::(@y,insert(@x,@ys)) insert#2(#true(),@x,@y,@ys) -> ::(@x,::(@y,@ys)) isortlist(@l) -> isortlist#1(@l) isortlist#1(::(@x,@xs)) -> insert(@x,isortlist(@xs)) isortlist#1(nil()) -> nil() leq(@l1,@l2) -> leq#1(@l1,@l2) leq#1(::(@x,@xs),@l2) -> leq#2(@l2,@x,@xs) leq#1(nil(),@l2) -> #true() leq#2(::(@y,@ys),@x,@xs) -> or(#less(@x,@y),and(#equal(@x,@y),leq(@xs,@ys))) leq#2(nil(),@x,@xs) -> #false() or(@x,@y) -> #or(@x,@y) - Signature: {#and/2,#cklt/1,#compare/2,#eq/2,#equal/2,#less/2,#or/2,and/2,insert/2,insert#1/2,insert#2/4,isortlist/1 ,isortlist#1/1,leq/2,leq#1/2,leq#2/3,or/2,#and#/2,#cklt#/1,#compare#/2,#eq#/2,#equal#/2,#less#/2,#or#/2 ,and#/2,insert#/2,insert#1#/2,insert#2#/4,isortlist#/1,isortlist#1#/1,leq#/2,leq#1#/2,leq#2#/3 ,or#/2} / {#0/0,#EQ/0,#GT/0,#LT/0,#false/0,#neg/1,#pos/1,#s/1,#true/0,::/2,nil/0,c_1/1,c_2/2,c_3/1,c_4/1 ,c_5/2,c_6/0,c_7/1,c_8/0,c_9/1,c_10/2,c_11/0,c_12/1,c_13/1,c_14/0,c_15/5,c_16/0,c_17/1,c_18/0,c_19/0,c_20/0 ,c_21/0,c_22/0,c_23/0,c_24/0,c_25/0,c_26/0,c_27/0,c_28/0,c_29/0,c_30/1,c_31/0,c_32/0,c_33/0,c_34/1,c_35/0 ,c_36/1,c_37/0,c_38/0,c_39/0,c_40/0,c_41/0,c_42/1,c_43/0,c_44/0,c_45/0,c_46/1,c_47/0,c_48/1,c_49/3,c_50/0 ,c_51/0,c_52/0,c_53/0,c_54/0,c_55/0,c_56/0} - Obligation: innermost runtime complexity wrt. defined symbols {#and#,#cklt#,#compare#,#eq#,#equal#,#less#,#or#,and# ,insert#,insert#1#,insert#2#,isortlist#,isortlist#1#,leq#,leq#1#,leq#2#,or#} and constructors {#0,#EQ,#GT ,#LT,#false,#neg,#pos,#s,#true,::,nil} + Applied Processor: PredecessorEstimation {onSelection = all simple predecessor estimation selector} + Details: We estimate the number of application of {1,2,3,6,8,11,14,16,17} by application of Pre({1,2,3,6,8,11,14,16,17}) = {4,5,9,12,13,15}. Here rules are labelled as follows: 1: #equal#(@x,@y) -> c_1(#eq#(@x,@y)) 2: #less#(@x,@y) -> c_2(#cklt#(#compare(@x,@y)),#compare#(@x,@y)) 3: and#(@x,@y) -> c_3(#and#(@x,@y)) 4: insert#(@x,@l) -> c_4(insert#1#(@l,@x)) 5: insert#1#(::(@y,@ys),@x) -> c_5(insert#2#(leq(@x,@y),@x,@y,@ys),leq#(@x,@y)) 6: insert#1#(nil(),@x) -> c_6() 7: insert#2#(#false(),@x,@y,@ys) -> c_7(insert#(@x,@ys)) 8: insert#2#(#true(),@x,@y,@ys) -> c_8() 9: isortlist#(@l) -> c_9(isortlist#1#(@l)) 10: isortlist#1#(::(@x,@xs)) -> c_10(insert#(@x,isortlist(@xs)),isortlist#(@xs)) 11: isortlist#1#(nil()) -> c_11() 12: leq#(@l1,@l2) -> c_12(leq#1#(@l1,@l2)) 13: leq#1#(::(@x,@xs),@l2) -> c_13(leq#2#(@l2,@x,@xs)) 14: leq#1#(nil(),@l2) -> c_14() 15: leq#2#(::(@y,@ys),@x,@xs) -> c_15(or#(#less(@x,@y),and(#equal(@x,@y),leq(@xs,@ys))) ,#less#(@x,@y) ,and#(#equal(@x,@y),leq(@xs,@ys)) ,#equal#(@x,@y) ,leq#(@xs,@ys)) 16: leq#2#(nil(),@x,@xs) -> c_16() 17: or#(@x,@y) -> c_17(#or#(@x,@y)) 18: #and#(#false(),#false()) -> c_18() 19: #and#(#false(),#true()) -> c_19() 20: #and#(#true(),#false()) -> c_20() 21: #and#(#true(),#true()) -> c_21() 22: #cklt#(#EQ()) -> c_22() 23: #cklt#(#GT()) -> c_23() 24: #cklt#(#LT()) -> c_24() 25: #compare#(#0(),#0()) -> c_25() 26: #compare#(#0(),#neg(@y)) -> c_26() 27: #compare#(#0(),#pos(@y)) -> c_27() 28: #compare#(#0(),#s(@y)) -> c_28() 29: #compare#(#neg(@x),#0()) -> c_29() 30: #compare#(#neg(@x),#neg(@y)) -> c_30(#compare#(@y,@x)) 31: #compare#(#neg(@x),#pos(@y)) -> c_31() 32: #compare#(#pos(@x),#0()) -> c_32() 33: #compare#(#pos(@x),#neg(@y)) -> c_33() 34: #compare#(#pos(@x),#pos(@y)) -> c_34(#compare#(@x,@y)) 35: #compare#(#s(@x),#0()) -> c_35() 36: #compare#(#s(@x),#s(@y)) -> c_36(#compare#(@x,@y)) 37: #eq#(#0(),#0()) -> c_37() 38: #eq#(#0(),#neg(@y)) -> c_38() 39: #eq#(#0(),#pos(@y)) -> c_39() 40: #eq#(#0(),#s(@y)) -> c_40() 41: #eq#(#neg(@x),#0()) -> c_41() 42: #eq#(#neg(@x),#neg(@y)) -> c_42(#eq#(@x,@y)) 43: #eq#(#neg(@x),#pos(@y)) -> c_43() 44: #eq#(#pos(@x),#0()) -> c_44() 45: #eq#(#pos(@x),#neg(@y)) -> c_45() 46: #eq#(#pos(@x),#pos(@y)) -> c_46(#eq#(@x,@y)) 47: #eq#(#s(@x),#0()) -> c_47() 48: #eq#(#s(@x),#s(@y)) -> c_48(#eq#(@x,@y)) 49: #eq#(::(@x_1,@x_2),::(@y_1,@y_2)) -> c_49(#and#(#eq(@x_1,@y_1),#eq(@x_2,@y_2)) ,#eq#(@x_1,@y_1) ,#eq#(@x_2,@y_2)) 50: #eq#(::(@x_1,@x_2),nil()) -> c_50() 51: #eq#(nil(),::(@y_1,@y_2)) -> c_51() 52: #eq#(nil(),nil()) -> c_52() 53: #or#(#false(),#false()) -> c_53() 54: #or#(#false(),#true()) -> c_54() 55: #or#(#true(),#false()) -> c_55() 56: #or#(#true(),#true()) -> c_56() * Step 3: RemoveWeakSuffixes WORST_CASE(?,O(n^2)) + Considered Problem: - Strict DPs: insert#(@x,@l) -> c_4(insert#1#(@l,@x)) insert#1#(::(@y,@ys),@x) -> c_5(insert#2#(leq(@x,@y),@x,@y,@ys),leq#(@x,@y)) insert#2#(#false(),@x,@y,@ys) -> c_7(insert#(@x,@ys)) isortlist#(@l) -> c_9(isortlist#1#(@l)) isortlist#1#(::(@x,@xs)) -> c_10(insert#(@x,isortlist(@xs)),isortlist#(@xs)) leq#(@l1,@l2) -> c_12(leq#1#(@l1,@l2)) leq#1#(::(@x,@xs),@l2) -> c_13(leq#2#(@l2,@x,@xs)) leq#2#(::(@y,@ys),@x,@xs) -> c_15(or#(#less(@x,@y),and(#equal(@x,@y),leq(@xs,@ys))) ,#less#(@x,@y) ,and#(#equal(@x,@y),leq(@xs,@ys)) ,#equal#(@x,@y) ,leq#(@xs,@ys)) - Weak DPs: #and#(#false(),#false()) -> c_18() #and#(#false(),#true()) -> c_19() #and#(#true(),#false()) -> c_20() #and#(#true(),#true()) -> c_21() #cklt#(#EQ()) -> c_22() #cklt#(#GT()) -> c_23() #cklt#(#LT()) -> c_24() #compare#(#0(),#0()) -> c_25() #compare#(#0(),#neg(@y)) -> c_26() #compare#(#0(),#pos(@y)) -> c_27() #compare#(#0(),#s(@y)) -> c_28() #compare#(#neg(@x),#0()) -> c_29() #compare#(#neg(@x),#neg(@y)) -> c_30(#compare#(@y,@x)) #compare#(#neg(@x),#pos(@y)) -> c_31() #compare#(#pos(@x),#0()) -> c_32() #compare#(#pos(@x),#neg(@y)) -> c_33() #compare#(#pos(@x),#pos(@y)) -> c_34(#compare#(@x,@y)) #compare#(#s(@x),#0()) -> c_35() #compare#(#s(@x),#s(@y)) -> c_36(#compare#(@x,@y)) #eq#(#0(),#0()) -> c_37() #eq#(#0(),#neg(@y)) -> c_38() #eq#(#0(),#pos(@y)) -> c_39() #eq#(#0(),#s(@y)) -> c_40() #eq#(#neg(@x),#0()) -> c_41() #eq#(#neg(@x),#neg(@y)) -> c_42(#eq#(@x,@y)) #eq#(#neg(@x),#pos(@y)) -> c_43() #eq#(#pos(@x),#0()) -> c_44() #eq#(#pos(@x),#neg(@y)) -> c_45() #eq#(#pos(@x),#pos(@y)) -> c_46(#eq#(@x,@y)) #eq#(#s(@x),#0()) -> c_47() #eq#(#s(@x),#s(@y)) -> c_48(#eq#(@x,@y)) #eq#(::(@x_1,@x_2),::(@y_1,@y_2)) -> c_49(#and#(#eq(@x_1,@y_1),#eq(@x_2,@y_2)) ,#eq#(@x_1,@y_1) ,#eq#(@x_2,@y_2)) #eq#(::(@x_1,@x_2),nil()) -> c_50() #eq#(nil(),::(@y_1,@y_2)) -> c_51() #eq#(nil(),nil()) -> c_52() #equal#(@x,@y) -> c_1(#eq#(@x,@y)) #less#(@x,@y) -> c_2(#cklt#(#compare(@x,@y)),#compare#(@x,@y)) #or#(#false(),#false()) -> c_53() #or#(#false(),#true()) -> c_54() #or#(#true(),#false()) -> c_55() #or#(#true(),#true()) -> c_56() and#(@x,@y) -> c_3(#and#(@x,@y)) insert#1#(nil(),@x) -> c_6() insert#2#(#true(),@x,@y,@ys) -> c_8() isortlist#1#(nil()) -> c_11() leq#1#(nil(),@l2) -> c_14() leq#2#(nil(),@x,@xs) -> c_16() or#(@x,@y) -> c_17(#or#(@x,@y)) - Weak TRS: #and(#false(),#false()) -> #false() #and(#false(),#true()) -> #false() #and(#true(),#false()) -> #false() #and(#true(),#true()) -> #true() #cklt(#EQ()) -> #false() #cklt(#GT()) -> #false() #cklt(#LT()) -> #true() #compare(#0(),#0()) -> #EQ() #compare(#0(),#neg(@y)) -> #GT() #compare(#0(),#pos(@y)) -> #LT() #compare(#0(),#s(@y)) -> #LT() #compare(#neg(@x),#0()) -> #LT() #compare(#neg(@x),#neg(@y)) -> #compare(@y,@x) #compare(#neg(@x),#pos(@y)) -> #LT() #compare(#pos(@x),#0()) -> #GT() #compare(#pos(@x),#neg(@y)) -> #GT() #compare(#pos(@x),#pos(@y)) -> #compare(@x,@y) #compare(#s(@x),#0()) -> #GT() #compare(#s(@x),#s(@y)) -> #compare(@x,@y) #eq(#0(),#0()) -> #true() #eq(#0(),#neg(@y)) -> #false() #eq(#0(),#pos(@y)) -> #false() #eq(#0(),#s(@y)) -> #false() #eq(#neg(@x),#0()) -> #false() #eq(#neg(@x),#neg(@y)) -> #eq(@x,@y) #eq(#neg(@x),#pos(@y)) -> #false() #eq(#pos(@x),#0()) -> #false() #eq(#pos(@x),#neg(@y)) -> #false() #eq(#pos(@x),#pos(@y)) -> #eq(@x,@y) #eq(#s(@x),#0()) -> #false() #eq(#s(@x),#s(@y)) -> #eq(@x,@y) #eq(::(@x_1,@x_2),::(@y_1,@y_2)) -> #and(#eq(@x_1,@y_1),#eq(@x_2,@y_2)) #eq(::(@x_1,@x_2),nil()) -> #false() #eq(nil(),::(@y_1,@y_2)) -> #false() #eq(nil(),nil()) -> #true() #equal(@x,@y) -> #eq(@x,@y) #less(@x,@y) -> #cklt(#compare(@x,@y)) #or(#false(),#false()) -> #false() #or(#false(),#true()) -> #true() #or(#true(),#false()) -> #true() #or(#true(),#true()) -> #true() and(@x,@y) -> #and(@x,@y) insert(@x,@l) -> insert#1(@l,@x) insert#1(::(@y,@ys),@x) -> insert#2(leq(@x,@y),@x,@y,@ys) insert#1(nil(),@x) -> ::(@x,nil()) insert#2(#false(),@x,@y,@ys) -> ::(@y,insert(@x,@ys)) insert#2(#true(),@x,@y,@ys) -> ::(@x,::(@y,@ys)) isortlist(@l) -> isortlist#1(@l) isortlist#1(::(@x,@xs)) -> insert(@x,isortlist(@xs)) isortlist#1(nil()) -> nil() leq(@l1,@l2) -> leq#1(@l1,@l2) leq#1(::(@x,@xs),@l2) -> leq#2(@l2,@x,@xs) leq#1(nil(),@l2) -> #true() leq#2(::(@y,@ys),@x,@xs) -> or(#less(@x,@y),and(#equal(@x,@y),leq(@xs,@ys))) leq#2(nil(),@x,@xs) -> #false() or(@x,@y) -> #or(@x,@y) - Signature: {#and/2,#cklt/1,#compare/2,#eq/2,#equal/2,#less/2,#or/2,and/2,insert/2,insert#1/2,insert#2/4,isortlist/1 ,isortlist#1/1,leq/2,leq#1/2,leq#2/3,or/2,#and#/2,#cklt#/1,#compare#/2,#eq#/2,#equal#/2,#less#/2,#or#/2 ,and#/2,insert#/2,insert#1#/2,insert#2#/4,isortlist#/1,isortlist#1#/1,leq#/2,leq#1#/2,leq#2#/3 ,or#/2} / {#0/0,#EQ/0,#GT/0,#LT/0,#false/0,#neg/1,#pos/1,#s/1,#true/0,::/2,nil/0,c_1/1,c_2/2,c_3/1,c_4/1 ,c_5/2,c_6/0,c_7/1,c_8/0,c_9/1,c_10/2,c_11/0,c_12/1,c_13/1,c_14/0,c_15/5,c_16/0,c_17/1,c_18/0,c_19/0,c_20/0 ,c_21/0,c_22/0,c_23/0,c_24/0,c_25/0,c_26/0,c_27/0,c_28/0,c_29/0,c_30/1,c_31/0,c_32/0,c_33/0,c_34/1,c_35/0 ,c_36/1,c_37/0,c_38/0,c_39/0,c_40/0,c_41/0,c_42/1,c_43/0,c_44/0,c_45/0,c_46/1,c_47/0,c_48/1,c_49/3,c_50/0 ,c_51/0,c_52/0,c_53/0,c_54/0,c_55/0,c_56/0} - Obligation: innermost runtime complexity wrt. defined symbols {#and#,#cklt#,#compare#,#eq#,#equal#,#less#,#or#,and# ,insert#,insert#1#,insert#2#,isortlist#,isortlist#1#,leq#,leq#1#,leq#2#,or#} and constructors {#0,#EQ,#GT ,#LT,#false,#neg,#pos,#s,#true,::,nil} + Applied Processor: RemoveWeakSuffixes + Details: Consider the dependency graph 1:S:insert#(@x,@l) -> c_4(insert#1#(@l,@x)) -->_1 insert#1#(::(@y,@ys),@x) -> c_5(insert#2#(leq(@x,@y),@x,@y,@ys),leq#(@x,@y)):2 -->_1 insert#1#(nil(),@x) -> c_6():51 2:S:insert#1#(::(@y,@ys),@x) -> c_5(insert#2#(leq(@x,@y),@x,@y,@ys),leq#(@x,@y)) -->_2 leq#(@l1,@l2) -> c_12(leq#1#(@l1,@l2)):6 -->_1 insert#2#(#false(),@x,@y,@ys) -> c_7(insert#(@x,@ys)):3 -->_1 insert#2#(#true(),@x,@y,@ys) -> c_8():52 3:S:insert#2#(#false(),@x,@y,@ys) -> c_7(insert#(@x,@ys)) -->_1 insert#(@x,@l) -> c_4(insert#1#(@l,@x)):1 4:S:isortlist#(@l) -> c_9(isortlist#1#(@l)) -->_1 isortlist#1#(::(@x,@xs)) -> c_10(insert#(@x,isortlist(@xs)),isortlist#(@xs)):5 -->_1 isortlist#1#(nil()) -> c_11():53 5:S:isortlist#1#(::(@x,@xs)) -> c_10(insert#(@x,isortlist(@xs)),isortlist#(@xs)) -->_2 isortlist#(@l) -> c_9(isortlist#1#(@l)):4 -->_1 insert#(@x,@l) -> c_4(insert#1#(@l,@x)):1 6:S:leq#(@l1,@l2) -> c_12(leq#1#(@l1,@l2)) -->_1 leq#1#(::(@x,@xs),@l2) -> c_13(leq#2#(@l2,@x,@xs)):7 -->_1 leq#1#(nil(),@l2) -> c_14():54 7:S:leq#1#(::(@x,@xs),@l2) -> c_13(leq#2#(@l2,@x,@xs)) -->_1 leq#2#(::(@y,@ys),@x,@xs) -> c_15(or#(#less(@x,@y),and(#equal(@x,@y),leq(@xs,@ys))) ,#less#(@x,@y) ,and#(#equal(@x,@y),leq(@xs,@ys)) ,#equal#(@x,@y) ,leq#(@xs,@ys)):8 -->_1 leq#2#(nil(),@x,@xs) -> c_16():55 8:S:leq#2#(::(@y,@ys),@x,@xs) -> c_15(or#(#less(@x,@y),and(#equal(@x,@y),leq(@xs,@ys))) ,#less#(@x,@y) ,and#(#equal(@x,@y),leq(@xs,@ys)) ,#equal#(@x,@y) ,leq#(@xs,@ys)) -->_1 or#(@x,@y) -> c_17(#or#(@x,@y)):56 -->_3 and#(@x,@y) -> c_3(#and#(@x,@y)):50 -->_2 #less#(@x,@y) -> c_2(#cklt#(#compare(@x,@y)),#compare#(@x,@y)):45 -->_4 #equal#(@x,@y) -> c_1(#eq#(@x,@y)):44 -->_5 leq#(@l1,@l2) -> c_12(leq#1#(@l1,@l2)):6 9:W:#and#(#false(),#false()) -> c_18() 10:W:#and#(#false(),#true()) -> c_19() 11:W:#and#(#true(),#false()) -> c_20() 12:W:#and#(#true(),#true()) -> c_21() 13:W:#cklt#(#EQ()) -> c_22() 14:W:#cklt#(#GT()) -> c_23() 15:W:#cklt#(#LT()) -> c_24() 16:W:#compare#(#0(),#0()) -> c_25() 17:W:#compare#(#0(),#neg(@y)) -> c_26() 18:W:#compare#(#0(),#pos(@y)) -> c_27() 19:W:#compare#(#0(),#s(@y)) -> c_28() 20:W:#compare#(#neg(@x),#0()) -> c_29() 21:W:#compare#(#neg(@x),#neg(@y)) -> c_30(#compare#(@y,@x)) -->_1 #compare#(#s(@x),#s(@y)) -> c_36(#compare#(@x,@y)):27 -->_1 #compare#(#pos(@x),#pos(@y)) -> c_34(#compare#(@x,@y)):25 -->_1 #compare#(#s(@x),#0()) -> c_35():26 -->_1 #compare#(#pos(@x),#neg(@y)) -> c_33():24 -->_1 #compare#(#pos(@x),#0()) -> c_32():23 -->_1 #compare#(#neg(@x),#pos(@y)) -> c_31():22 -->_1 #compare#(#neg(@x),#neg(@y)) -> c_30(#compare#(@y,@x)):21 -->_1 #compare#(#neg(@x),#0()) -> c_29():20 -->_1 #compare#(#0(),#s(@y)) -> c_28():19 -->_1 #compare#(#0(),#pos(@y)) -> c_27():18 -->_1 #compare#(#0(),#neg(@y)) -> c_26():17 -->_1 #compare#(#0(),#0()) -> c_25():16 22:W:#compare#(#neg(@x),#pos(@y)) -> c_31() 23:W:#compare#(#pos(@x),#0()) -> c_32() 24:W:#compare#(#pos(@x),#neg(@y)) -> c_33() 25:W:#compare#(#pos(@x),#pos(@y)) -> c_34(#compare#(@x,@y)) -->_1 #compare#(#s(@x),#s(@y)) -> c_36(#compare#(@x,@y)):27 -->_1 #compare#(#s(@x),#0()) -> c_35():26 -->_1 #compare#(#pos(@x),#pos(@y)) -> c_34(#compare#(@x,@y)):25 -->_1 #compare#(#pos(@x),#neg(@y)) -> c_33():24 -->_1 #compare#(#pos(@x),#0()) -> c_32():23 -->_1 #compare#(#neg(@x),#pos(@y)) -> c_31():22 -->_1 #compare#(#neg(@x),#neg(@y)) -> c_30(#compare#(@y,@x)):21 -->_1 #compare#(#neg(@x),#0()) -> c_29():20 -->_1 #compare#(#0(),#s(@y)) -> c_28():19 -->_1 #compare#(#0(),#pos(@y)) -> c_27():18 -->_1 #compare#(#0(),#neg(@y)) -> c_26():17 -->_1 #compare#(#0(),#0()) -> c_25():16 26:W:#compare#(#s(@x),#0()) -> c_35() 27:W:#compare#(#s(@x),#s(@y)) -> c_36(#compare#(@x,@y)) -->_1 #compare#(#s(@x),#s(@y)) -> c_36(#compare#(@x,@y)):27 -->_1 #compare#(#s(@x),#0()) -> c_35():26 -->_1 #compare#(#pos(@x),#pos(@y)) -> c_34(#compare#(@x,@y)):25 -->_1 #compare#(#pos(@x),#neg(@y)) -> c_33():24 -->_1 #compare#(#pos(@x),#0()) -> c_32():23 -->_1 #compare#(#neg(@x),#pos(@y)) -> c_31():22 -->_1 #compare#(#neg(@x),#neg(@y)) -> c_30(#compare#(@y,@x)):21 -->_1 #compare#(#neg(@x),#0()) -> c_29():20 -->_1 #compare#(#0(),#s(@y)) -> c_28():19 -->_1 #compare#(#0(),#pos(@y)) -> c_27():18 -->_1 #compare#(#0(),#neg(@y)) -> c_26():17 -->_1 #compare#(#0(),#0()) -> c_25():16 28:W:#eq#(#0(),#0()) -> c_37() 29:W:#eq#(#0(),#neg(@y)) -> c_38() 30:W:#eq#(#0(),#pos(@y)) -> c_39() 31:W:#eq#(#0(),#s(@y)) -> c_40() 32:W:#eq#(#neg(@x),#0()) -> c_41() 33:W:#eq#(#neg(@x),#neg(@y)) -> c_42(#eq#(@x,@y)) -->_1 #eq#(::(@x_1,@x_2),::(@y_1,@y_2)) -> c_49(#and#(#eq(@x_1,@y_1),#eq(@x_2,@y_2)) ,#eq#(@x_1,@y_1) ,#eq#(@x_2,@y_2)):40 -->_1 #eq#(#s(@x),#s(@y)) -> c_48(#eq#(@x,@y)):39 -->_1 #eq#(#pos(@x),#pos(@y)) -> c_46(#eq#(@x,@y)):37 -->_1 #eq#(nil(),nil()) -> c_52():43 -->_1 #eq#(nil(),::(@y_1,@y_2)) -> c_51():42 -->_1 #eq#(::(@x_1,@x_2),nil()) -> c_50():41 -->_1 #eq#(#s(@x),#0()) -> c_47():38 -->_1 #eq#(#pos(@x),#neg(@y)) -> c_45():36 -->_1 #eq#(#pos(@x),#0()) -> c_44():35 -->_1 #eq#(#neg(@x),#pos(@y)) -> c_43():34 -->_1 #eq#(#neg(@x),#neg(@y)) -> c_42(#eq#(@x,@y)):33 -->_1 #eq#(#neg(@x),#0()) -> c_41():32 -->_1 #eq#(#0(),#s(@y)) -> c_40():31 -->_1 #eq#(#0(),#pos(@y)) -> c_39():30 -->_1 #eq#(#0(),#neg(@y)) -> c_38():29 -->_1 #eq#(#0(),#0()) -> c_37():28 34:W:#eq#(#neg(@x),#pos(@y)) -> c_43() 35:W:#eq#(#pos(@x),#0()) -> c_44() 36:W:#eq#(#pos(@x),#neg(@y)) -> c_45() 37:W:#eq#(#pos(@x),#pos(@y)) -> c_46(#eq#(@x,@y)) -->_1 #eq#(::(@x_1,@x_2),::(@y_1,@y_2)) -> c_49(#and#(#eq(@x_1,@y_1),#eq(@x_2,@y_2)) ,#eq#(@x_1,@y_1) ,#eq#(@x_2,@y_2)):40 -->_1 #eq#(#s(@x),#s(@y)) -> c_48(#eq#(@x,@y)):39 -->_1 #eq#(nil(),nil()) -> c_52():43 -->_1 #eq#(nil(),::(@y_1,@y_2)) -> c_51():42 -->_1 #eq#(::(@x_1,@x_2),nil()) -> c_50():41 -->_1 #eq#(#s(@x),#0()) -> c_47():38 -->_1 #eq#(#pos(@x),#pos(@y)) -> c_46(#eq#(@x,@y)):37 -->_1 #eq#(#pos(@x),#neg(@y)) -> c_45():36 -->_1 #eq#(#pos(@x),#0()) -> c_44():35 -->_1 #eq#(#neg(@x),#pos(@y)) -> c_43():34 -->_1 #eq#(#neg(@x),#neg(@y)) -> c_42(#eq#(@x,@y)):33 -->_1 #eq#(#neg(@x),#0()) -> c_41():32 -->_1 #eq#(#0(),#s(@y)) -> c_40():31 -->_1 #eq#(#0(),#pos(@y)) -> c_39():30 -->_1 #eq#(#0(),#neg(@y)) -> c_38():29 -->_1 #eq#(#0(),#0()) -> c_37():28 38:W:#eq#(#s(@x),#0()) -> c_47() 39:W:#eq#(#s(@x),#s(@y)) -> c_48(#eq#(@x,@y)) -->_1 #eq#(::(@x_1,@x_2),::(@y_1,@y_2)) -> c_49(#and#(#eq(@x_1,@y_1),#eq(@x_2,@y_2)) ,#eq#(@x_1,@y_1) ,#eq#(@x_2,@y_2)):40 -->_1 #eq#(nil(),nil()) -> c_52():43 -->_1 #eq#(nil(),::(@y_1,@y_2)) -> c_51():42 -->_1 #eq#(::(@x_1,@x_2),nil()) -> c_50():41 -->_1 #eq#(#s(@x),#s(@y)) -> c_48(#eq#(@x,@y)):39 -->_1 #eq#(#s(@x),#0()) -> c_47():38 -->_1 #eq#(#pos(@x),#pos(@y)) -> c_46(#eq#(@x,@y)):37 -->_1 #eq#(#pos(@x),#neg(@y)) -> c_45():36 -->_1 #eq#(#pos(@x),#0()) -> c_44():35 -->_1 #eq#(#neg(@x),#pos(@y)) -> c_43():34 -->_1 #eq#(#neg(@x),#neg(@y)) -> c_42(#eq#(@x,@y)):33 -->_1 #eq#(#neg(@x),#0()) -> c_41():32 -->_1 #eq#(#0(),#s(@y)) -> c_40():31 -->_1 #eq#(#0(),#pos(@y)) -> c_39():30 -->_1 #eq#(#0(),#neg(@y)) -> c_38():29 -->_1 #eq#(#0(),#0()) -> c_37():28 40:W:#eq#(::(@x_1,@x_2),::(@y_1,@y_2)) -> c_49(#and#(#eq(@x_1,@y_1),#eq(@x_2,@y_2)) ,#eq#(@x_1,@y_1) ,#eq#(@x_2,@y_2)) -->_3 #eq#(nil(),nil()) -> c_52():43 -->_2 #eq#(nil(),nil()) -> c_52():43 -->_3 #eq#(nil(),::(@y_1,@y_2)) -> c_51():42 -->_2 #eq#(nil(),::(@y_1,@y_2)) -> c_51():42 -->_3 #eq#(::(@x_1,@x_2),nil()) -> c_50():41 -->_2 #eq#(::(@x_1,@x_2),nil()) -> c_50():41 -->_3 #eq#(::(@x_1,@x_2),::(@y_1,@y_2)) -> c_49(#and#(#eq(@x_1,@y_1),#eq(@x_2,@y_2)) ,#eq#(@x_1,@y_1) ,#eq#(@x_2,@y_2)):40 -->_2 #eq#(::(@x_1,@x_2),::(@y_1,@y_2)) -> c_49(#and#(#eq(@x_1,@y_1),#eq(@x_2,@y_2)) ,#eq#(@x_1,@y_1) ,#eq#(@x_2,@y_2)):40 -->_3 #eq#(#s(@x),#s(@y)) -> c_48(#eq#(@x,@y)):39 -->_2 #eq#(#s(@x),#s(@y)) -> c_48(#eq#(@x,@y)):39 -->_3 #eq#(#s(@x),#0()) -> c_47():38 -->_2 #eq#(#s(@x),#0()) -> c_47():38 -->_3 #eq#(#pos(@x),#pos(@y)) -> c_46(#eq#(@x,@y)):37 -->_2 #eq#(#pos(@x),#pos(@y)) -> c_46(#eq#(@x,@y)):37 -->_3 #eq#(#pos(@x),#neg(@y)) -> c_45():36 -->_2 #eq#(#pos(@x),#neg(@y)) -> c_45():36 -->_3 #eq#(#pos(@x),#0()) -> c_44():35 -->_2 #eq#(#pos(@x),#0()) -> c_44():35 -->_3 #eq#(#neg(@x),#pos(@y)) -> c_43():34 -->_2 #eq#(#neg(@x),#pos(@y)) -> c_43():34 -->_3 #eq#(#neg(@x),#neg(@y)) -> c_42(#eq#(@x,@y)):33 -->_2 #eq#(#neg(@x),#neg(@y)) -> c_42(#eq#(@x,@y)):33 -->_3 #eq#(#neg(@x),#0()) -> c_41():32 -->_2 #eq#(#neg(@x),#0()) -> c_41():32 -->_3 #eq#(#0(),#s(@y)) -> c_40():31 -->_2 #eq#(#0(),#s(@y)) -> c_40():31 -->_3 #eq#(#0(),#pos(@y)) -> c_39():30 -->_2 #eq#(#0(),#pos(@y)) -> c_39():30 -->_3 #eq#(#0(),#neg(@y)) -> c_38():29 -->_2 #eq#(#0(),#neg(@y)) -> c_38():29 -->_3 #eq#(#0(),#0()) -> c_37():28 -->_2 #eq#(#0(),#0()) -> c_37():28 -->_1 #and#(#true(),#true()) -> c_21():12 -->_1 #and#(#true(),#false()) -> c_20():11 -->_1 #and#(#false(),#true()) -> c_19():10 -->_1 #and#(#false(),#false()) -> c_18():9 41:W:#eq#(::(@x_1,@x_2),nil()) -> c_50() 42:W:#eq#(nil(),::(@y_1,@y_2)) -> c_51() 43:W:#eq#(nil(),nil()) -> c_52() 44:W:#equal#(@x,@y) -> c_1(#eq#(@x,@y)) -->_1 #eq#(nil(),nil()) -> c_52():43 -->_1 #eq#(nil(),::(@y_1,@y_2)) -> c_51():42 -->_1 #eq#(::(@x_1,@x_2),nil()) -> c_50():41 -->_1 #eq#(::(@x_1,@x_2),::(@y_1,@y_2)) -> c_49(#and#(#eq(@x_1,@y_1),#eq(@x_2,@y_2)) ,#eq#(@x_1,@y_1) ,#eq#(@x_2,@y_2)):40 -->_1 #eq#(#s(@x),#s(@y)) -> c_48(#eq#(@x,@y)):39 -->_1 #eq#(#s(@x),#0()) -> c_47():38 -->_1 #eq#(#pos(@x),#pos(@y)) -> c_46(#eq#(@x,@y)):37 -->_1 #eq#(#pos(@x),#neg(@y)) -> c_45():36 -->_1 #eq#(#pos(@x),#0()) -> c_44():35 -->_1 #eq#(#neg(@x),#pos(@y)) -> c_43():34 -->_1 #eq#(#neg(@x),#neg(@y)) -> c_42(#eq#(@x,@y)):33 -->_1 #eq#(#neg(@x),#0()) -> c_41():32 -->_1 #eq#(#0(),#s(@y)) -> c_40():31 -->_1 #eq#(#0(),#pos(@y)) -> c_39():30 -->_1 #eq#(#0(),#neg(@y)) -> c_38():29 -->_1 #eq#(#0(),#0()) -> c_37():28 45:W:#less#(@x,@y) -> c_2(#cklt#(#compare(@x,@y)),#compare#(@x,@y)) -->_2 #compare#(#s(@x),#s(@y)) -> c_36(#compare#(@x,@y)):27 -->_2 #compare#(#s(@x),#0()) -> c_35():26 -->_2 #compare#(#pos(@x),#pos(@y)) -> c_34(#compare#(@x,@y)):25 -->_2 #compare#(#pos(@x),#neg(@y)) -> c_33():24 -->_2 #compare#(#pos(@x),#0()) -> c_32():23 -->_2 #compare#(#neg(@x),#pos(@y)) -> c_31():22 -->_2 #compare#(#neg(@x),#neg(@y)) -> c_30(#compare#(@y,@x)):21 -->_2 #compare#(#neg(@x),#0()) -> c_29():20 -->_2 #compare#(#0(),#s(@y)) -> c_28():19 -->_2 #compare#(#0(),#pos(@y)) -> c_27():18 -->_2 #compare#(#0(),#neg(@y)) -> c_26():17 -->_2 #compare#(#0(),#0()) -> c_25():16 -->_1 #cklt#(#LT()) -> c_24():15 -->_1 #cklt#(#GT()) -> c_23():14 -->_1 #cklt#(#EQ()) -> c_22():13 46:W:#or#(#false(),#false()) -> c_53() 47:W:#or#(#false(),#true()) -> c_54() 48:W:#or#(#true(),#false()) -> c_55() 49:W:#or#(#true(),#true()) -> c_56() 50:W:and#(@x,@y) -> c_3(#and#(@x,@y)) -->_1 #and#(#true(),#true()) -> c_21():12 -->_1 #and#(#true(),#false()) -> c_20():11 -->_1 #and#(#false(),#true()) -> c_19():10 -->_1 #and#(#false(),#false()) -> c_18():9 51:W:insert#1#(nil(),@x) -> c_6() 52:W:insert#2#(#true(),@x,@y,@ys) -> c_8() 53:W:isortlist#1#(nil()) -> c_11() 54:W:leq#1#(nil(),@l2) -> c_14() 55:W:leq#2#(nil(),@x,@xs) -> c_16() 56:W:or#(@x,@y) -> c_17(#or#(@x,@y)) -->_1 #or#(#true(),#true()) -> c_56():49 -->_1 #or#(#true(),#false()) -> c_55():48 -->_1 #or#(#false(),#true()) -> c_54():47 -->_1 #or#(#false(),#false()) -> c_53():46 The following weak DPs constitute a sub-graph of the DG that is closed under successors. The DPs are removed. 53: isortlist#1#(nil()) -> c_11() 51: insert#1#(nil(),@x) -> c_6() 52: insert#2#(#true(),@x,@y,@ys) -> c_8() 54: leq#1#(nil(),@l2) -> c_14() 55: leq#2#(nil(),@x,@xs) -> c_16() 44: #equal#(@x,@y) -> c_1(#eq#(@x,@y)) 40: #eq#(::(@x_1,@x_2),::(@y_1,@y_2)) -> c_49(#and#(#eq(@x_1,@y_1),#eq(@x_2,@y_2)) ,#eq#(@x_1,@y_1) ,#eq#(@x_2,@y_2)) 39: #eq#(#s(@x),#s(@y)) -> c_48(#eq#(@x,@y)) 37: #eq#(#pos(@x),#pos(@y)) -> c_46(#eq#(@x,@y)) 33: #eq#(#neg(@x),#neg(@y)) -> c_42(#eq#(@x,@y)) 28: #eq#(#0(),#0()) -> c_37() 29: #eq#(#0(),#neg(@y)) -> c_38() 30: #eq#(#0(),#pos(@y)) -> c_39() 31: #eq#(#0(),#s(@y)) -> c_40() 32: #eq#(#neg(@x),#0()) -> c_41() 34: #eq#(#neg(@x),#pos(@y)) -> c_43() 35: #eq#(#pos(@x),#0()) -> c_44() 36: #eq#(#pos(@x),#neg(@y)) -> c_45() 38: #eq#(#s(@x),#0()) -> c_47() 41: #eq#(::(@x_1,@x_2),nil()) -> c_50() 42: #eq#(nil(),::(@y_1,@y_2)) -> c_51() 43: #eq#(nil(),nil()) -> c_52() 45: #less#(@x,@y) -> c_2(#cklt#(#compare(@x,@y)),#compare#(@x,@y)) 13: #cklt#(#EQ()) -> c_22() 14: #cklt#(#GT()) -> c_23() 15: #cklt#(#LT()) -> c_24() 27: #compare#(#s(@x),#s(@y)) -> c_36(#compare#(@x,@y)) 25: #compare#(#pos(@x),#pos(@y)) -> c_34(#compare#(@x,@y)) 21: #compare#(#neg(@x),#neg(@y)) -> c_30(#compare#(@y,@x)) 16: #compare#(#0(),#0()) -> c_25() 17: #compare#(#0(),#neg(@y)) -> c_26() 18: #compare#(#0(),#pos(@y)) -> c_27() 19: #compare#(#0(),#s(@y)) -> c_28() 20: #compare#(#neg(@x),#0()) -> c_29() 22: #compare#(#neg(@x),#pos(@y)) -> c_31() 23: #compare#(#pos(@x),#0()) -> c_32() 24: #compare#(#pos(@x),#neg(@y)) -> c_33() 26: #compare#(#s(@x),#0()) -> c_35() 50: and#(@x,@y) -> c_3(#and#(@x,@y)) 9: #and#(#false(),#false()) -> c_18() 10: #and#(#false(),#true()) -> c_19() 11: #and#(#true(),#false()) -> c_20() 12: #and#(#true(),#true()) -> c_21() 56: or#(@x,@y) -> c_17(#or#(@x,@y)) 46: #or#(#false(),#false()) -> c_53() 47: #or#(#false(),#true()) -> c_54() 48: #or#(#true(),#false()) -> c_55() 49: #or#(#true(),#true()) -> c_56() * Step 4: SimplifyRHS WORST_CASE(?,O(n^2)) + Considered Problem: - Strict DPs: insert#(@x,@l) -> c_4(insert#1#(@l,@x)) insert#1#(::(@y,@ys),@x) -> c_5(insert#2#(leq(@x,@y),@x,@y,@ys),leq#(@x,@y)) insert#2#(#false(),@x,@y,@ys) -> c_7(insert#(@x,@ys)) isortlist#(@l) -> c_9(isortlist#1#(@l)) isortlist#1#(::(@x,@xs)) -> c_10(insert#(@x,isortlist(@xs)),isortlist#(@xs)) leq#(@l1,@l2) -> c_12(leq#1#(@l1,@l2)) leq#1#(::(@x,@xs),@l2) -> c_13(leq#2#(@l2,@x,@xs)) leq#2#(::(@y,@ys),@x,@xs) -> c_15(or#(#less(@x,@y),and(#equal(@x,@y),leq(@xs,@ys))) ,#less#(@x,@y) ,and#(#equal(@x,@y),leq(@xs,@ys)) ,#equal#(@x,@y) ,leq#(@xs,@ys)) - Weak TRS: #and(#false(),#false()) -> #false() #and(#false(),#true()) -> #false() #and(#true(),#false()) -> #false() #and(#true(),#true()) -> #true() #cklt(#EQ()) -> #false() #cklt(#GT()) -> #false() #cklt(#LT()) -> #true() #compare(#0(),#0()) -> #EQ() #compare(#0(),#neg(@y)) -> #GT() #compare(#0(),#pos(@y)) -> #LT() #compare(#0(),#s(@y)) -> #LT() #compare(#neg(@x),#0()) -> #LT() #compare(#neg(@x),#neg(@y)) -> #compare(@y,@x) #compare(#neg(@x),#pos(@y)) -> #LT() #compare(#pos(@x),#0()) -> #GT() #compare(#pos(@x),#neg(@y)) -> #GT() #compare(#pos(@x),#pos(@y)) -> #compare(@x,@y) #compare(#s(@x),#0()) -> #GT() #compare(#s(@x),#s(@y)) -> #compare(@x,@y) #eq(#0(),#0()) -> #true() #eq(#0(),#neg(@y)) -> #false() #eq(#0(),#pos(@y)) -> #false() #eq(#0(),#s(@y)) -> #false() #eq(#neg(@x),#0()) -> #false() #eq(#neg(@x),#neg(@y)) -> #eq(@x,@y) #eq(#neg(@x),#pos(@y)) -> #false() #eq(#pos(@x),#0()) -> #false() #eq(#pos(@x),#neg(@y)) -> #false() #eq(#pos(@x),#pos(@y)) -> #eq(@x,@y) #eq(#s(@x),#0()) -> #false() #eq(#s(@x),#s(@y)) -> #eq(@x,@y) #eq(::(@x_1,@x_2),::(@y_1,@y_2)) -> #and(#eq(@x_1,@y_1),#eq(@x_2,@y_2)) #eq(::(@x_1,@x_2),nil()) -> #false() #eq(nil(),::(@y_1,@y_2)) -> #false() #eq(nil(),nil()) -> #true() #equal(@x,@y) -> #eq(@x,@y) #less(@x,@y) -> #cklt(#compare(@x,@y)) #or(#false(),#false()) -> #false() #or(#false(),#true()) -> #true() #or(#true(),#false()) -> #true() #or(#true(),#true()) -> #true() and(@x,@y) -> #and(@x,@y) insert(@x,@l) -> insert#1(@l,@x) insert#1(::(@y,@ys),@x) -> insert#2(leq(@x,@y),@x,@y,@ys) insert#1(nil(),@x) -> ::(@x,nil()) insert#2(#false(),@x,@y,@ys) -> ::(@y,insert(@x,@ys)) insert#2(#true(),@x,@y,@ys) -> ::(@x,::(@y,@ys)) isortlist(@l) -> isortlist#1(@l) isortlist#1(::(@x,@xs)) -> insert(@x,isortlist(@xs)) isortlist#1(nil()) -> nil() leq(@l1,@l2) -> leq#1(@l1,@l2) leq#1(::(@x,@xs),@l2) -> leq#2(@l2,@x,@xs) leq#1(nil(),@l2) -> #true() leq#2(::(@y,@ys),@x,@xs) -> or(#less(@x,@y),and(#equal(@x,@y),leq(@xs,@ys))) leq#2(nil(),@x,@xs) -> #false() or(@x,@y) -> #or(@x,@y) - Signature: {#and/2,#cklt/1,#compare/2,#eq/2,#equal/2,#less/2,#or/2,and/2,insert/2,insert#1/2,insert#2/4,isortlist/1 ,isortlist#1/1,leq/2,leq#1/2,leq#2/3,or/2,#and#/2,#cklt#/1,#compare#/2,#eq#/2,#equal#/2,#less#/2,#or#/2 ,and#/2,insert#/2,insert#1#/2,insert#2#/4,isortlist#/1,isortlist#1#/1,leq#/2,leq#1#/2,leq#2#/3 ,or#/2} / {#0/0,#EQ/0,#GT/0,#LT/0,#false/0,#neg/1,#pos/1,#s/1,#true/0,::/2,nil/0,c_1/1,c_2/2,c_3/1,c_4/1 ,c_5/2,c_6/0,c_7/1,c_8/0,c_9/1,c_10/2,c_11/0,c_12/1,c_13/1,c_14/0,c_15/5,c_16/0,c_17/1,c_18/0,c_19/0,c_20/0 ,c_21/0,c_22/0,c_23/0,c_24/0,c_25/0,c_26/0,c_27/0,c_28/0,c_29/0,c_30/1,c_31/0,c_32/0,c_33/0,c_34/1,c_35/0 ,c_36/1,c_37/0,c_38/0,c_39/0,c_40/0,c_41/0,c_42/1,c_43/0,c_44/0,c_45/0,c_46/1,c_47/0,c_48/1,c_49/3,c_50/0 ,c_51/0,c_52/0,c_53/0,c_54/0,c_55/0,c_56/0} - Obligation: innermost runtime complexity wrt. defined symbols {#and#,#cklt#,#compare#,#eq#,#equal#,#less#,#or#,and# ,insert#,insert#1#,insert#2#,isortlist#,isortlist#1#,leq#,leq#1#,leq#2#,or#} and constructors {#0,#EQ,#GT ,#LT,#false,#neg,#pos,#s,#true,::,nil} + Applied Processor: SimplifyRHS + Details: Consider the dependency graph 1:S:insert#(@x,@l) -> c_4(insert#1#(@l,@x)) -->_1 insert#1#(::(@y,@ys),@x) -> c_5(insert#2#(leq(@x,@y),@x,@y,@ys),leq#(@x,@y)):2 2:S:insert#1#(::(@y,@ys),@x) -> c_5(insert#2#(leq(@x,@y),@x,@y,@ys),leq#(@x,@y)) -->_2 leq#(@l1,@l2) -> c_12(leq#1#(@l1,@l2)):6 -->_1 insert#2#(#false(),@x,@y,@ys) -> c_7(insert#(@x,@ys)):3 3:S:insert#2#(#false(),@x,@y,@ys) -> c_7(insert#(@x,@ys)) -->_1 insert#(@x,@l) -> c_4(insert#1#(@l,@x)):1 4:S:isortlist#(@l) -> c_9(isortlist#1#(@l)) -->_1 isortlist#1#(::(@x,@xs)) -> c_10(insert#(@x,isortlist(@xs)),isortlist#(@xs)):5 5:S:isortlist#1#(::(@x,@xs)) -> c_10(insert#(@x,isortlist(@xs)),isortlist#(@xs)) -->_2 isortlist#(@l) -> c_9(isortlist#1#(@l)):4 -->_1 insert#(@x,@l) -> c_4(insert#1#(@l,@x)):1 6:S:leq#(@l1,@l2) -> c_12(leq#1#(@l1,@l2)) -->_1 leq#1#(::(@x,@xs),@l2) -> c_13(leq#2#(@l2,@x,@xs)):7 7:S:leq#1#(::(@x,@xs),@l2) -> c_13(leq#2#(@l2,@x,@xs)) -->_1 leq#2#(::(@y,@ys),@x,@xs) -> c_15(or#(#less(@x,@y),and(#equal(@x,@y),leq(@xs,@ys))) ,#less#(@x,@y) ,and#(#equal(@x,@y),leq(@xs,@ys)) ,#equal#(@x,@y) ,leq#(@xs,@ys)):8 8:S:leq#2#(::(@y,@ys),@x,@xs) -> c_15(or#(#less(@x,@y),and(#equal(@x,@y),leq(@xs,@ys))) ,#less#(@x,@y) ,and#(#equal(@x,@y),leq(@xs,@ys)) ,#equal#(@x,@y) ,leq#(@xs,@ys)) -->_5 leq#(@l1,@l2) -> c_12(leq#1#(@l1,@l2)):6 Due to missing edges in the depndency graph, the right-hand sides of following rules could be simplified: leq#2#(::(@y,@ys),@x,@xs) -> c_15(leq#(@xs,@ys)) * Step 5: Decompose WORST_CASE(?,O(n^2)) + Considered Problem: - Strict DPs: insert#(@x,@l) -> c_4(insert#1#(@l,@x)) insert#1#(::(@y,@ys),@x) -> c_5(insert#2#(leq(@x,@y),@x,@y,@ys),leq#(@x,@y)) insert#2#(#false(),@x,@y,@ys) -> c_7(insert#(@x,@ys)) isortlist#(@l) -> c_9(isortlist#1#(@l)) isortlist#1#(::(@x,@xs)) -> c_10(insert#(@x,isortlist(@xs)),isortlist#(@xs)) leq#(@l1,@l2) -> c_12(leq#1#(@l1,@l2)) leq#1#(::(@x,@xs),@l2) -> c_13(leq#2#(@l2,@x,@xs)) leq#2#(::(@y,@ys),@x,@xs) -> c_15(leq#(@xs,@ys)) - Weak TRS: #and(#false(),#false()) -> #false() #and(#false(),#true()) -> #false() #and(#true(),#false()) -> #false() #and(#true(),#true()) -> #true() #cklt(#EQ()) -> #false() #cklt(#GT()) -> #false() #cklt(#LT()) -> #true() #compare(#0(),#0()) -> #EQ() #compare(#0(),#neg(@y)) -> #GT() #compare(#0(),#pos(@y)) -> #LT() #compare(#0(),#s(@y)) -> #LT() #compare(#neg(@x),#0()) -> #LT() #compare(#neg(@x),#neg(@y)) -> #compare(@y,@x) #compare(#neg(@x),#pos(@y)) -> #LT() #compare(#pos(@x),#0()) -> #GT() #compare(#pos(@x),#neg(@y)) -> #GT() #compare(#pos(@x),#pos(@y)) -> #compare(@x,@y) #compare(#s(@x),#0()) -> #GT() #compare(#s(@x),#s(@y)) -> #compare(@x,@y) #eq(#0(),#0()) -> #true() #eq(#0(),#neg(@y)) -> #false() #eq(#0(),#pos(@y)) -> #false() #eq(#0(),#s(@y)) -> #false() #eq(#neg(@x),#0()) -> #false() #eq(#neg(@x),#neg(@y)) -> #eq(@x,@y) #eq(#neg(@x),#pos(@y)) -> #false() #eq(#pos(@x),#0()) -> #false() #eq(#pos(@x),#neg(@y)) -> #false() #eq(#pos(@x),#pos(@y)) -> #eq(@x,@y) #eq(#s(@x),#0()) -> #false() #eq(#s(@x),#s(@y)) -> #eq(@x,@y) #eq(::(@x_1,@x_2),::(@y_1,@y_2)) -> #and(#eq(@x_1,@y_1),#eq(@x_2,@y_2)) #eq(::(@x_1,@x_2),nil()) -> #false() #eq(nil(),::(@y_1,@y_2)) -> #false() #eq(nil(),nil()) -> #true() #equal(@x,@y) -> #eq(@x,@y) #less(@x,@y) -> #cklt(#compare(@x,@y)) #or(#false(),#false()) -> #false() #or(#false(),#true()) -> #true() #or(#true(),#false()) -> #true() #or(#true(),#true()) -> #true() and(@x,@y) -> #and(@x,@y) insert(@x,@l) -> insert#1(@l,@x) insert#1(::(@y,@ys),@x) -> insert#2(leq(@x,@y),@x,@y,@ys) insert#1(nil(),@x) -> ::(@x,nil()) insert#2(#false(),@x,@y,@ys) -> ::(@y,insert(@x,@ys)) insert#2(#true(),@x,@y,@ys) -> ::(@x,::(@y,@ys)) isortlist(@l) -> isortlist#1(@l) isortlist#1(::(@x,@xs)) -> insert(@x,isortlist(@xs)) isortlist#1(nil()) -> nil() leq(@l1,@l2) -> leq#1(@l1,@l2) leq#1(::(@x,@xs),@l2) -> leq#2(@l2,@x,@xs) leq#1(nil(),@l2) -> #true() leq#2(::(@y,@ys),@x,@xs) -> or(#less(@x,@y),and(#equal(@x,@y),leq(@xs,@ys))) leq#2(nil(),@x,@xs) -> #false() or(@x,@y) -> #or(@x,@y) - Signature: {#and/2,#cklt/1,#compare/2,#eq/2,#equal/2,#less/2,#or/2,and/2,insert/2,insert#1/2,insert#2/4,isortlist/1 ,isortlist#1/1,leq/2,leq#1/2,leq#2/3,or/2,#and#/2,#cklt#/1,#compare#/2,#eq#/2,#equal#/2,#less#/2,#or#/2 ,and#/2,insert#/2,insert#1#/2,insert#2#/4,isortlist#/1,isortlist#1#/1,leq#/2,leq#1#/2,leq#2#/3 ,or#/2} / {#0/0,#EQ/0,#GT/0,#LT/0,#false/0,#neg/1,#pos/1,#s/1,#true/0,::/2,nil/0,c_1/1,c_2/2,c_3/1,c_4/1 ,c_5/2,c_6/0,c_7/1,c_8/0,c_9/1,c_10/2,c_11/0,c_12/1,c_13/1,c_14/0,c_15/1,c_16/0,c_17/1,c_18/0,c_19/0,c_20/0 ,c_21/0,c_22/0,c_23/0,c_24/0,c_25/0,c_26/0,c_27/0,c_28/0,c_29/0,c_30/1,c_31/0,c_32/0,c_33/0,c_34/1,c_35/0 ,c_36/1,c_37/0,c_38/0,c_39/0,c_40/0,c_41/0,c_42/1,c_43/0,c_44/0,c_45/0,c_46/1,c_47/0,c_48/1,c_49/3,c_50/0 ,c_51/0,c_52/0,c_53/0,c_54/0,c_55/0,c_56/0} - Obligation: innermost runtime complexity wrt. defined symbols {#and#,#cklt#,#compare#,#eq#,#equal#,#less#,#or#,and# ,insert#,insert#1#,insert#2#,isortlist#,isortlist#1#,leq#,leq#1#,leq#2#,or#} and constructors {#0,#EQ,#GT ,#LT,#false,#neg,#pos,#s,#true,::,nil} + Applied Processor: Decompose {onSelection = all cycle independent sub-graph, withBound = RelativeAdd} + Details: We analyse the complexity of following sub-problems (R) and (S). Problem (S) is obtained from the input problem by shifting strict rules from (R) into the weak component. Problem (R) - Strict DPs: insert#(@x,@l) -> c_4(insert#1#(@l,@x)) insert#1#(::(@y,@ys),@x) -> c_5(insert#2#(leq(@x,@y),@x,@y,@ys),leq#(@x,@y)) insert#2#(#false(),@x,@y,@ys) -> c_7(insert#(@x,@ys)) leq#(@l1,@l2) -> c_12(leq#1#(@l1,@l2)) leq#1#(::(@x,@xs),@l2) -> c_13(leq#2#(@l2,@x,@xs)) leq#2#(::(@y,@ys),@x,@xs) -> c_15(leq#(@xs,@ys)) - Weak DPs: isortlist#(@l) -> c_9(isortlist#1#(@l)) isortlist#1#(::(@x,@xs)) -> c_10(insert#(@x,isortlist(@xs)),isortlist#(@xs)) - Weak TRS: #and(#false(),#false()) -> #false() #and(#false(),#true()) -> #false() #and(#true(),#false()) -> #false() #and(#true(),#true()) -> #true() #cklt(#EQ()) -> #false() #cklt(#GT()) -> #false() #cklt(#LT()) -> #true() #compare(#0(),#0()) -> #EQ() #compare(#0(),#neg(@y)) -> #GT() #compare(#0(),#pos(@y)) -> #LT() #compare(#0(),#s(@y)) -> #LT() #compare(#neg(@x),#0()) -> #LT() #compare(#neg(@x),#neg(@y)) -> #compare(@y,@x) #compare(#neg(@x),#pos(@y)) -> #LT() #compare(#pos(@x),#0()) -> #GT() #compare(#pos(@x),#neg(@y)) -> #GT() #compare(#pos(@x),#pos(@y)) -> #compare(@x,@y) #compare(#s(@x),#0()) -> #GT() #compare(#s(@x),#s(@y)) -> #compare(@x,@y) #eq(#0(),#0()) -> #true() #eq(#0(),#neg(@y)) -> #false() #eq(#0(),#pos(@y)) -> #false() #eq(#0(),#s(@y)) -> #false() #eq(#neg(@x),#0()) -> #false() #eq(#neg(@x),#neg(@y)) -> #eq(@x,@y) #eq(#neg(@x),#pos(@y)) -> #false() #eq(#pos(@x),#0()) -> #false() #eq(#pos(@x),#neg(@y)) -> #false() #eq(#pos(@x),#pos(@y)) -> #eq(@x,@y) #eq(#s(@x),#0()) -> #false() #eq(#s(@x),#s(@y)) -> #eq(@x,@y) #eq(::(@x_1,@x_2),::(@y_1,@y_2)) -> #and(#eq(@x_1,@y_1),#eq(@x_2,@y_2)) #eq(::(@x_1,@x_2),nil()) -> #false() #eq(nil(),::(@y_1,@y_2)) -> #false() #eq(nil(),nil()) -> #true() #equal(@x,@y) -> #eq(@x,@y) #less(@x,@y) -> #cklt(#compare(@x,@y)) #or(#false(),#false()) -> #false() #or(#false(),#true()) -> #true() #or(#true(),#false()) -> #true() #or(#true(),#true()) -> #true() and(@x,@y) -> #and(@x,@y) insert(@x,@l) -> insert#1(@l,@x) insert#1(::(@y,@ys),@x) -> insert#2(leq(@x,@y),@x,@y,@ys) insert#1(nil(),@x) -> ::(@x,nil()) insert#2(#false(),@x,@y,@ys) -> ::(@y,insert(@x,@ys)) insert#2(#true(),@x,@y,@ys) -> ::(@x,::(@y,@ys)) isortlist(@l) -> isortlist#1(@l) isortlist#1(::(@x,@xs)) -> insert(@x,isortlist(@xs)) isortlist#1(nil()) -> nil() leq(@l1,@l2) -> leq#1(@l1,@l2) leq#1(::(@x,@xs),@l2) -> leq#2(@l2,@x,@xs) leq#1(nil(),@l2) -> #true() leq#2(::(@y,@ys),@x,@xs) -> or(#less(@x,@y),and(#equal(@x,@y),leq(@xs,@ys))) leq#2(nil(),@x,@xs) -> #false() or(@x,@y) -> #or(@x,@y) - Signature: {#and/2,#cklt/1,#compare/2,#eq/2,#equal/2,#less/2,#or/2,and/2,insert/2,insert#1/2,insert#2/4,isortlist/1 ,isortlist#1/1,leq/2,leq#1/2,leq#2/3,or/2,#and#/2,#cklt#/1,#compare#/2,#eq#/2,#equal#/2,#less#/2,#or#/2 ,and#/2,insert#/2,insert#1#/2,insert#2#/4,isortlist#/1,isortlist#1#/1,leq#/2,leq#1#/2,leq#2#/3 ,or#/2} / {#0/0,#EQ/0,#GT/0,#LT/0,#false/0,#neg/1,#pos/1,#s/1,#true/0,::/2,nil/0,c_1/1,c_2/2,c_3/1,c_4/1 ,c_5/2,c_6/0,c_7/1,c_8/0,c_9/1,c_10/2,c_11/0,c_12/1,c_13/1,c_14/0,c_15/1,c_16/0,c_17/1,c_18/0,c_19/0 ,c_20/0,c_21/0,c_22/0,c_23/0,c_24/0,c_25/0,c_26/0,c_27/0,c_28/0,c_29/0,c_30/1,c_31/0,c_32/0,c_33/0,c_34/1 ,c_35/0,c_36/1,c_37/0,c_38/0,c_39/0,c_40/0,c_41/0,c_42/1,c_43/0,c_44/0,c_45/0,c_46/1,c_47/0,c_48/1,c_49/3 ,c_50/0,c_51/0,c_52/0,c_53/0,c_54/0,c_55/0,c_56/0} - Obligation: innermost runtime complexity wrt. defined symbols {#and#,#cklt#,#compare#,#eq#,#equal#,#less#,#or#,and# ,insert#,insert#1#,insert#2#,isortlist#,isortlist#1#,leq#,leq#1#,leq#2#,or#} and constructors {#0,#EQ,#GT ,#LT,#false,#neg,#pos,#s,#true,::,nil} Problem (S) - Strict DPs: isortlist#(@l) -> c_9(isortlist#1#(@l)) isortlist#1#(::(@x,@xs)) -> c_10(insert#(@x,isortlist(@xs)),isortlist#(@xs)) - Weak DPs: insert#(@x,@l) -> c_4(insert#1#(@l,@x)) insert#1#(::(@y,@ys),@x) -> c_5(insert#2#(leq(@x,@y),@x,@y,@ys),leq#(@x,@y)) insert#2#(#false(),@x,@y,@ys) -> c_7(insert#(@x,@ys)) leq#(@l1,@l2) -> c_12(leq#1#(@l1,@l2)) leq#1#(::(@x,@xs),@l2) -> c_13(leq#2#(@l2,@x,@xs)) leq#2#(::(@y,@ys),@x,@xs) -> c_15(leq#(@xs,@ys)) - Weak TRS: #and(#false(),#false()) -> #false() #and(#false(),#true()) -> #false() #and(#true(),#false()) -> #false() #and(#true(),#true()) -> #true() #cklt(#EQ()) -> #false() #cklt(#GT()) -> #false() #cklt(#LT()) -> #true() #compare(#0(),#0()) -> #EQ() #compare(#0(),#neg(@y)) -> #GT() #compare(#0(),#pos(@y)) -> #LT() #compare(#0(),#s(@y)) -> #LT() #compare(#neg(@x),#0()) -> #LT() #compare(#neg(@x),#neg(@y)) -> #compare(@y,@x) #compare(#neg(@x),#pos(@y)) -> #LT() #compare(#pos(@x),#0()) -> #GT() #compare(#pos(@x),#neg(@y)) -> #GT() #compare(#pos(@x),#pos(@y)) -> #compare(@x,@y) #compare(#s(@x),#0()) -> #GT() #compare(#s(@x),#s(@y)) -> #compare(@x,@y) #eq(#0(),#0()) -> #true() #eq(#0(),#neg(@y)) -> #false() #eq(#0(),#pos(@y)) -> #false() #eq(#0(),#s(@y)) -> #false() #eq(#neg(@x),#0()) -> #false() #eq(#neg(@x),#neg(@y)) -> #eq(@x,@y) #eq(#neg(@x),#pos(@y)) -> #false() #eq(#pos(@x),#0()) -> #false() #eq(#pos(@x),#neg(@y)) -> #false() #eq(#pos(@x),#pos(@y)) -> #eq(@x,@y) #eq(#s(@x),#0()) -> #false() #eq(#s(@x),#s(@y)) -> #eq(@x,@y) #eq(::(@x_1,@x_2),::(@y_1,@y_2)) -> #and(#eq(@x_1,@y_1),#eq(@x_2,@y_2)) #eq(::(@x_1,@x_2),nil()) -> #false() #eq(nil(),::(@y_1,@y_2)) -> #false() #eq(nil(),nil()) -> #true() #equal(@x,@y) -> #eq(@x,@y) #less(@x,@y) -> #cklt(#compare(@x,@y)) #or(#false(),#false()) -> #false() #or(#false(),#true()) -> #true() #or(#true(),#false()) -> #true() #or(#true(),#true()) -> #true() and(@x,@y) -> #and(@x,@y) insert(@x,@l) -> insert#1(@l,@x) insert#1(::(@y,@ys),@x) -> insert#2(leq(@x,@y),@x,@y,@ys) insert#1(nil(),@x) -> ::(@x,nil()) insert#2(#false(),@x,@y,@ys) -> ::(@y,insert(@x,@ys)) insert#2(#true(),@x,@y,@ys) -> ::(@x,::(@y,@ys)) isortlist(@l) -> isortlist#1(@l) isortlist#1(::(@x,@xs)) -> insert(@x,isortlist(@xs)) isortlist#1(nil()) -> nil() leq(@l1,@l2) -> leq#1(@l1,@l2) leq#1(::(@x,@xs),@l2) -> leq#2(@l2,@x,@xs) leq#1(nil(),@l2) -> #true() leq#2(::(@y,@ys),@x,@xs) -> or(#less(@x,@y),and(#equal(@x,@y),leq(@xs,@ys))) leq#2(nil(),@x,@xs) -> #false() or(@x,@y) -> #or(@x,@y) - Signature: {#and/2,#cklt/1,#compare/2,#eq/2,#equal/2,#less/2,#or/2,and/2,insert/2,insert#1/2,insert#2/4,isortlist/1 ,isortlist#1/1,leq/2,leq#1/2,leq#2/3,or/2,#and#/2,#cklt#/1,#compare#/2,#eq#/2,#equal#/2,#less#/2,#or#/2 ,and#/2,insert#/2,insert#1#/2,insert#2#/4,isortlist#/1,isortlist#1#/1,leq#/2,leq#1#/2,leq#2#/3 ,or#/2} / {#0/0,#EQ/0,#GT/0,#LT/0,#false/0,#neg/1,#pos/1,#s/1,#true/0,::/2,nil/0,c_1/1,c_2/2,c_3/1,c_4/1 ,c_5/2,c_6/0,c_7/1,c_8/0,c_9/1,c_10/2,c_11/0,c_12/1,c_13/1,c_14/0,c_15/1,c_16/0,c_17/1,c_18/0,c_19/0 ,c_20/0,c_21/0,c_22/0,c_23/0,c_24/0,c_25/0,c_26/0,c_27/0,c_28/0,c_29/0,c_30/1,c_31/0,c_32/0,c_33/0,c_34/1 ,c_35/0,c_36/1,c_37/0,c_38/0,c_39/0,c_40/0,c_41/0,c_42/1,c_43/0,c_44/0,c_45/0,c_46/1,c_47/0,c_48/1,c_49/3 ,c_50/0,c_51/0,c_52/0,c_53/0,c_54/0,c_55/0,c_56/0} - Obligation: innermost runtime complexity wrt. defined symbols {#and#,#cklt#,#compare#,#eq#,#equal#,#less#,#or#,and# ,insert#,insert#1#,insert#2#,isortlist#,isortlist#1#,leq#,leq#1#,leq#2#,or#} and constructors {#0,#EQ,#GT ,#LT,#false,#neg,#pos,#s,#true,::,nil} ** Step 5.a:1: PredecessorEstimationCP WORST_CASE(?,O(n^2)) + Considered Problem: - Strict DPs: insert#(@x,@l) -> c_4(insert#1#(@l,@x)) insert#1#(::(@y,@ys),@x) -> c_5(insert#2#(leq(@x,@y),@x,@y,@ys),leq#(@x,@y)) insert#2#(#false(),@x,@y,@ys) -> c_7(insert#(@x,@ys)) leq#(@l1,@l2) -> c_12(leq#1#(@l1,@l2)) leq#1#(::(@x,@xs),@l2) -> c_13(leq#2#(@l2,@x,@xs)) leq#2#(::(@y,@ys),@x,@xs) -> c_15(leq#(@xs,@ys)) - Weak DPs: isortlist#(@l) -> c_9(isortlist#1#(@l)) isortlist#1#(::(@x,@xs)) -> c_10(insert#(@x,isortlist(@xs)),isortlist#(@xs)) - Weak TRS: #and(#false(),#false()) -> #false() #and(#false(),#true()) -> #false() #and(#true(),#false()) -> #false() #and(#true(),#true()) -> #true() #cklt(#EQ()) -> #false() #cklt(#GT()) -> #false() #cklt(#LT()) -> #true() #compare(#0(),#0()) -> #EQ() #compare(#0(),#neg(@y)) -> #GT() #compare(#0(),#pos(@y)) -> #LT() #compare(#0(),#s(@y)) -> #LT() #compare(#neg(@x),#0()) -> #LT() #compare(#neg(@x),#neg(@y)) -> #compare(@y,@x) #compare(#neg(@x),#pos(@y)) -> #LT() #compare(#pos(@x),#0()) -> #GT() #compare(#pos(@x),#neg(@y)) -> #GT() #compare(#pos(@x),#pos(@y)) -> #compare(@x,@y) #compare(#s(@x),#0()) -> #GT() #compare(#s(@x),#s(@y)) -> #compare(@x,@y) #eq(#0(),#0()) -> #true() #eq(#0(),#neg(@y)) -> #false() #eq(#0(),#pos(@y)) -> #false() #eq(#0(),#s(@y)) -> #false() #eq(#neg(@x),#0()) -> #false() #eq(#neg(@x),#neg(@y)) -> #eq(@x,@y) #eq(#neg(@x),#pos(@y)) -> #false() #eq(#pos(@x),#0()) -> #false() #eq(#pos(@x),#neg(@y)) -> #false() #eq(#pos(@x),#pos(@y)) -> #eq(@x,@y) #eq(#s(@x),#0()) -> #false() #eq(#s(@x),#s(@y)) -> #eq(@x,@y) #eq(::(@x_1,@x_2),::(@y_1,@y_2)) -> #and(#eq(@x_1,@y_1),#eq(@x_2,@y_2)) #eq(::(@x_1,@x_2),nil()) -> #false() #eq(nil(),::(@y_1,@y_2)) -> #false() #eq(nil(),nil()) -> #true() #equal(@x,@y) -> #eq(@x,@y) #less(@x,@y) -> #cklt(#compare(@x,@y)) #or(#false(),#false()) -> #false() #or(#false(),#true()) -> #true() #or(#true(),#false()) -> #true() #or(#true(),#true()) -> #true() and(@x,@y) -> #and(@x,@y) insert(@x,@l) -> insert#1(@l,@x) insert#1(::(@y,@ys),@x) -> insert#2(leq(@x,@y),@x,@y,@ys) insert#1(nil(),@x) -> ::(@x,nil()) insert#2(#false(),@x,@y,@ys) -> ::(@y,insert(@x,@ys)) insert#2(#true(),@x,@y,@ys) -> ::(@x,::(@y,@ys)) isortlist(@l) -> isortlist#1(@l) isortlist#1(::(@x,@xs)) -> insert(@x,isortlist(@xs)) isortlist#1(nil()) -> nil() leq(@l1,@l2) -> leq#1(@l1,@l2) leq#1(::(@x,@xs),@l2) -> leq#2(@l2,@x,@xs) leq#1(nil(),@l2) -> #true() leq#2(::(@y,@ys),@x,@xs) -> or(#less(@x,@y),and(#equal(@x,@y),leq(@xs,@ys))) leq#2(nil(),@x,@xs) -> #false() or(@x,@y) -> #or(@x,@y) - Signature: {#and/2,#cklt/1,#compare/2,#eq/2,#equal/2,#less/2,#or/2,and/2,insert/2,insert#1/2,insert#2/4,isortlist/1 ,isortlist#1/1,leq/2,leq#1/2,leq#2/3,or/2,#and#/2,#cklt#/1,#compare#/2,#eq#/2,#equal#/2,#less#/2,#or#/2 ,and#/2,insert#/2,insert#1#/2,insert#2#/4,isortlist#/1,isortlist#1#/1,leq#/2,leq#1#/2,leq#2#/3 ,or#/2} / {#0/0,#EQ/0,#GT/0,#LT/0,#false/0,#neg/1,#pos/1,#s/1,#true/0,::/2,nil/0,c_1/1,c_2/2,c_3/1,c_4/1 ,c_5/2,c_6/0,c_7/1,c_8/0,c_9/1,c_10/2,c_11/0,c_12/1,c_13/1,c_14/0,c_15/1,c_16/0,c_17/1,c_18/0,c_19/0,c_20/0 ,c_21/0,c_22/0,c_23/0,c_24/0,c_25/0,c_26/0,c_27/0,c_28/0,c_29/0,c_30/1,c_31/0,c_32/0,c_33/0,c_34/1,c_35/0 ,c_36/1,c_37/0,c_38/0,c_39/0,c_40/0,c_41/0,c_42/1,c_43/0,c_44/0,c_45/0,c_46/1,c_47/0,c_48/1,c_49/3,c_50/0 ,c_51/0,c_52/0,c_53/0,c_54/0,c_55/0,c_56/0} - Obligation: innermost runtime complexity wrt. defined symbols {#and#,#cklt#,#compare#,#eq#,#equal#,#less#,#or#,and# ,insert#,insert#1#,insert#2#,isortlist#,isortlist#1#,leq#,leq#1#,leq#2#,or#} and constructors {#0,#EQ,#GT ,#LT,#false,#neg,#pos,#s,#true,::,nil} + Applied Processor: PredecessorEstimationCP {onSelectionCP = any intersect of rules of CDG leaf and strict-rules, withComplexityPair = NaturalPI {shape = Mixed 2, restrict = Restrict, uargs = UArgs, urules = URules, selector = Nothing}} + Details: We first use the processor NaturalPI {shape = Mixed 2, restrict = Restrict, uargs = UArgs, urules = URules, selector = Nothing} to orient following rules strictly: 6: leq#(@l1,@l2) -> c_12(leq#1#(@l1,@l2)) Consider the set of all dependency pairs 1: insert#(@x,@l) -> c_4(insert#1#(@l,@x)) 2: insert#1#(::(@y,@ys),@x) -> c_5(insert#2#(leq(@x,@y),@x,@y,@ys),leq#(@x,@y)) 3: insert#2#(#false(),@x,@y,@ys) -> c_7(insert#(@x,@ys)) 4: isortlist#(@l) -> c_9(isortlist#1#(@l)) 5: isortlist#1#(::(@x,@xs)) -> c_10(insert#(@x,isortlist(@xs)),isortlist#(@xs)) 6: leq#(@l1,@l2) -> c_12(leq#1#(@l1,@l2)) 7: leq#1#(::(@x,@xs),@l2) -> c_13(leq#2#(@l2,@x,@xs)) 8: leq#2#(::(@y,@ys),@x,@xs) -> c_15(leq#(@xs,@ys)) Processor NaturalPI {shape = Mixed 2, restrict = Restrict, uargs = UArgs, urules = URules, selector = Nothing}induces the complexity certificateTIME (?,O(n^2)) SPACE(?,?)on application of the dependency pairs {6} These cover all (indirect) predecessors of dependency pairs {6,7,8} their number of applications is equally bounded. The dependency pairs are shifted into the weak component. *** Step 5.a:1.a:1: NaturalPI WORST_CASE(?,O(n^2)) + Considered Problem: - Strict DPs: insert#(@x,@l) -> c_4(insert#1#(@l,@x)) insert#1#(::(@y,@ys),@x) -> c_5(insert#2#(leq(@x,@y),@x,@y,@ys),leq#(@x,@y)) insert#2#(#false(),@x,@y,@ys) -> c_7(insert#(@x,@ys)) leq#(@l1,@l2) -> c_12(leq#1#(@l1,@l2)) leq#1#(::(@x,@xs),@l2) -> c_13(leq#2#(@l2,@x,@xs)) leq#2#(::(@y,@ys),@x,@xs) -> c_15(leq#(@xs,@ys)) - Weak DPs: isortlist#(@l) -> c_9(isortlist#1#(@l)) isortlist#1#(::(@x,@xs)) -> c_10(insert#(@x,isortlist(@xs)),isortlist#(@xs)) - Weak TRS: #and(#false(),#false()) -> #false() #and(#false(),#true()) -> #false() #and(#true(),#false()) -> #false() #and(#true(),#true()) -> #true() #cklt(#EQ()) -> #false() #cklt(#GT()) -> #false() #cklt(#LT()) -> #true() #compare(#0(),#0()) -> #EQ() #compare(#0(),#neg(@y)) -> #GT() #compare(#0(),#pos(@y)) -> #LT() #compare(#0(),#s(@y)) -> #LT() #compare(#neg(@x),#0()) -> #LT() #compare(#neg(@x),#neg(@y)) -> #compare(@y,@x) #compare(#neg(@x),#pos(@y)) -> #LT() #compare(#pos(@x),#0()) -> #GT() #compare(#pos(@x),#neg(@y)) -> #GT() #compare(#pos(@x),#pos(@y)) -> #compare(@x,@y) #compare(#s(@x),#0()) -> #GT() #compare(#s(@x),#s(@y)) -> #compare(@x,@y) #eq(#0(),#0()) -> #true() #eq(#0(),#neg(@y)) -> #false() #eq(#0(),#pos(@y)) -> #false() #eq(#0(),#s(@y)) -> #false() #eq(#neg(@x),#0()) -> #false() #eq(#neg(@x),#neg(@y)) -> #eq(@x,@y) #eq(#neg(@x),#pos(@y)) -> #false() #eq(#pos(@x),#0()) -> #false() #eq(#pos(@x),#neg(@y)) -> #false() #eq(#pos(@x),#pos(@y)) -> #eq(@x,@y) #eq(#s(@x),#0()) -> #false() #eq(#s(@x),#s(@y)) -> #eq(@x,@y) #eq(::(@x_1,@x_2),::(@y_1,@y_2)) -> #and(#eq(@x_1,@y_1),#eq(@x_2,@y_2)) #eq(::(@x_1,@x_2),nil()) -> #false() #eq(nil(),::(@y_1,@y_2)) -> #false() #eq(nil(),nil()) -> #true() #equal(@x,@y) -> #eq(@x,@y) #less(@x,@y) -> #cklt(#compare(@x,@y)) #or(#false(),#false()) -> #false() #or(#false(),#true()) -> #true() #or(#true(),#false()) -> #true() #or(#true(),#true()) -> #true() and(@x,@y) -> #and(@x,@y) insert(@x,@l) -> insert#1(@l,@x) insert#1(::(@y,@ys),@x) -> insert#2(leq(@x,@y),@x,@y,@ys) insert#1(nil(),@x) -> ::(@x,nil()) insert#2(#false(),@x,@y,@ys) -> ::(@y,insert(@x,@ys)) insert#2(#true(),@x,@y,@ys) -> ::(@x,::(@y,@ys)) isortlist(@l) -> isortlist#1(@l) isortlist#1(::(@x,@xs)) -> insert(@x,isortlist(@xs)) isortlist#1(nil()) -> nil() leq(@l1,@l2) -> leq#1(@l1,@l2) leq#1(::(@x,@xs),@l2) -> leq#2(@l2,@x,@xs) leq#1(nil(),@l2) -> #true() leq#2(::(@y,@ys),@x,@xs) -> or(#less(@x,@y),and(#equal(@x,@y),leq(@xs,@ys))) leq#2(nil(),@x,@xs) -> #false() or(@x,@y) -> #or(@x,@y) - Signature: {#and/2,#cklt/1,#compare/2,#eq/2,#equal/2,#less/2,#or/2,and/2,insert/2,insert#1/2,insert#2/4,isortlist/1 ,isortlist#1/1,leq/2,leq#1/2,leq#2/3,or/2,#and#/2,#cklt#/1,#compare#/2,#eq#/2,#equal#/2,#less#/2,#or#/2 ,and#/2,insert#/2,insert#1#/2,insert#2#/4,isortlist#/1,isortlist#1#/1,leq#/2,leq#1#/2,leq#2#/3 ,or#/2} / {#0/0,#EQ/0,#GT/0,#LT/0,#false/0,#neg/1,#pos/1,#s/1,#true/0,::/2,nil/0,c_1/1,c_2/2,c_3/1,c_4/1 ,c_5/2,c_6/0,c_7/1,c_8/0,c_9/1,c_10/2,c_11/0,c_12/1,c_13/1,c_14/0,c_15/1,c_16/0,c_17/1,c_18/0,c_19/0,c_20/0 ,c_21/0,c_22/0,c_23/0,c_24/0,c_25/0,c_26/0,c_27/0,c_28/0,c_29/0,c_30/1,c_31/0,c_32/0,c_33/0,c_34/1,c_35/0 ,c_36/1,c_37/0,c_38/0,c_39/0,c_40/0,c_41/0,c_42/1,c_43/0,c_44/0,c_45/0,c_46/1,c_47/0,c_48/1,c_49/3,c_50/0 ,c_51/0,c_52/0,c_53/0,c_54/0,c_55/0,c_56/0} - Obligation: innermost runtime complexity wrt. defined symbols {#and#,#cklt#,#compare#,#eq#,#equal#,#less#,#or#,and# ,insert#,insert#1#,insert#2#,isortlist#,isortlist#1#,leq#,leq#1#,leq#2#,or#} and constructors {#0,#EQ,#GT ,#LT,#false,#neg,#pos,#s,#true,::,nil} + Applied Processor: NaturalPI {shape = Mixed 2, restrict = Restrict, uargs = UArgs, urules = URules, selector = Just first alternative for predecessorEstimation on any intersect of rules of CDG leaf and strict-rules} + Details: We apply a polynomial interpretation of kind constructor-based(mixed(2)): The following argument positions are considered usable: uargs(c_4) = {1}, uargs(c_5) = {1,2}, uargs(c_7) = {1}, uargs(c_9) = {1}, uargs(c_10) = {1,2}, uargs(c_12) = {1}, uargs(c_13) = {1}, uargs(c_15) = {1} Following symbols are considered usable: {#or,insert,insert#1,insert#2,isortlist,isortlist#1,leq,leq#1,leq#2,or,#and#,#cklt#,#compare#,#eq#,#equal# ,#less#,#or#,and#,insert#,insert#1#,insert#2#,isortlist#,isortlist#1#,leq#,leq#1#,leq#2#,or#} TcT has computed the following interpretation: p(#0) = 0 p(#EQ) = 0 p(#GT) = 0 p(#LT) = 0 p(#and) = 0 p(#cklt) = x1 p(#compare) = 1 + x2^2 p(#eq) = 1 p(#equal) = 0 p(#false) = 1 p(#less) = x2 p(#neg) = 0 p(#or) = 1 p(#pos) = 1 p(#s) = 0 p(#true) = 1 p(::) = 1 + x1 + x2 p(and) = 0 p(insert) = 1 + x1 + x2 p(insert#1) = 1 + x1 + x2 p(insert#2) = 1 + x1*x2 + x1*x4 + x1^2 + x3 p(isortlist) = x1 p(isortlist#1) = x1 p(leq) = 1 p(leq#1) = 1 p(leq#2) = 1 p(nil) = 0 p(or) = 1 p(#and#) = 0 p(#cklt#) = 0 p(#compare#) = 0 p(#eq#) = 0 p(#equal#) = 0 p(#less#) = 0 p(#or#) = 0 p(and#) = 0 p(insert#) = x1*x2 + x1^2 + x2 p(insert#1#) = x1 + x1*x2 + x2^2 p(insert#2#) = x2 + x2*x4 + x2^2 + x3 + x4 p(isortlist#) = 1 + x1^2 p(isortlist#1#) = 1 + x1^2 p(leq#) = 1 + x1*x2 p(leq#1#) = x1*x2 p(leq#2#) = x1 + x1*x3 p(or#) = 0 p(c_1) = 0 p(c_2) = 0 p(c_3) = 0 p(c_4) = x1 p(c_5) = x1 + x2 p(c_6) = 0 p(c_7) = x1 p(c_8) = 0 p(c_9) = x1 p(c_10) = 1 + x1 + x2 p(c_11) = 0 p(c_12) = x1 p(c_13) = x1 p(c_14) = 0 p(c_15) = x1 p(c_16) = 0 p(c_17) = 0 p(c_18) = 0 p(c_19) = 0 p(c_20) = 0 p(c_21) = 0 p(c_22) = 0 p(c_23) = 0 p(c_24) = 0 p(c_25) = 0 p(c_26) = 0 p(c_27) = 0 p(c_28) = 0 p(c_29) = 0 p(c_30) = 0 p(c_31) = 0 p(c_32) = 0 p(c_33) = 0 p(c_34) = 0 p(c_35) = 0 p(c_36) = 0 p(c_37) = 0 p(c_38) = 0 p(c_39) = 0 p(c_40) = 0 p(c_41) = 0 p(c_42) = 0 p(c_43) = 0 p(c_44) = 0 p(c_45) = 0 p(c_46) = 0 p(c_47) = 0 p(c_48) = 0 p(c_49) = 0 p(c_50) = 0 p(c_51) = 0 p(c_52) = 0 p(c_53) = 0 p(c_54) = 0 p(c_55) = 0 p(c_56) = 0 Following rules are strictly oriented: leq#(@l1,@l2) = 1 + @l1*@l2 > @l1*@l2 = c_12(leq#1#(@l1,@l2)) Following rules are (at-least) weakly oriented: insert#(@x,@l) = @l + @l*@x + @x^2 >= @l + @l*@x + @x^2 = c_4(insert#1#(@l,@x)) insert#1#(::(@y,@ys),@x) = 1 + @x + @x*@y + @x*@ys + @x^2 + @y + @ys >= 1 + @x + @x*@y + @x*@ys + @x^2 + @y + @ys = c_5(insert#2#(leq(@x,@y),@x,@y,@ys),leq#(@x,@y)) insert#2#(#false(),@x,@y,@ys) = @x + @x*@ys + @x^2 + @y + @ys >= @x*@ys + @x^2 + @ys = c_7(insert#(@x,@ys)) isortlist#(@l) = 1 + @l^2 >= 1 + @l^2 = c_9(isortlist#1#(@l)) isortlist#1#(::(@x,@xs)) = 2 + 2*@x + 2*@x*@xs + @x^2 + 2*@xs + @xs^2 >= 2 + @x*@xs + @x^2 + @xs + @xs^2 = c_10(insert#(@x,isortlist(@xs)),isortlist#(@xs)) leq#1#(::(@x,@xs),@l2) = @l2 + @l2*@x + @l2*@xs >= @l2 + @l2*@xs = c_13(leq#2#(@l2,@x,@xs)) leq#2#(::(@y,@ys),@x,@xs) = 1 + @xs + @xs*@y + @xs*@ys + @y + @ys >= 1 + @xs*@ys = c_15(leq#(@xs,@ys)) #or(#false(),#false()) = 1 >= 1 = #false() #or(#false(),#true()) = 1 >= 1 = #true() #or(#true(),#false()) = 1 >= 1 = #true() #or(#true(),#true()) = 1 >= 1 = #true() insert(@x,@l) = 1 + @l + @x >= 1 + @l + @x = insert#1(@l,@x) insert#1(::(@y,@ys),@x) = 2 + @x + @y + @ys >= 2 + @x + @y + @ys = insert#2(leq(@x,@y),@x,@y,@ys) insert#1(nil(),@x) = 1 + @x >= 1 + @x = ::(@x,nil()) insert#2(#false(),@x,@y,@ys) = 2 + @x + @y + @ys >= 2 + @x + @y + @ys = ::(@y,insert(@x,@ys)) insert#2(#true(),@x,@y,@ys) = 2 + @x + @y + @ys >= 2 + @x + @y + @ys = ::(@x,::(@y,@ys)) isortlist(@l) = @l >= @l = isortlist#1(@l) isortlist#1(::(@x,@xs)) = 1 + @x + @xs >= 1 + @x + @xs = insert(@x,isortlist(@xs)) isortlist#1(nil()) = 0 >= 0 = nil() leq(@l1,@l2) = 1 >= 1 = leq#1(@l1,@l2) leq#1(::(@x,@xs),@l2) = 1 >= 1 = leq#2(@l2,@x,@xs) leq#1(nil(),@l2) = 1 >= 1 = #true() leq#2(::(@y,@ys),@x,@xs) = 1 >= 1 = or(#less(@x,@y),and(#equal(@x,@y),leq(@xs,@ys))) leq#2(nil(),@x,@xs) = 1 >= 1 = #false() or(@x,@y) = 1 >= 1 = #or(@x,@y) *** Step 5.a:1.a:2: Assumption WORST_CASE(?,O(1)) + Considered Problem: - Strict DPs: insert#(@x,@l) -> c_4(insert#1#(@l,@x)) insert#1#(::(@y,@ys),@x) -> c_5(insert#2#(leq(@x,@y),@x,@y,@ys),leq#(@x,@y)) insert#2#(#false(),@x,@y,@ys) -> c_7(insert#(@x,@ys)) leq#1#(::(@x,@xs),@l2) -> c_13(leq#2#(@l2,@x,@xs)) leq#2#(::(@y,@ys),@x,@xs) -> c_15(leq#(@xs,@ys)) - Weak DPs: isortlist#(@l) -> c_9(isortlist#1#(@l)) isortlist#1#(::(@x,@xs)) -> c_10(insert#(@x,isortlist(@xs)),isortlist#(@xs)) leq#(@l1,@l2) -> c_12(leq#1#(@l1,@l2)) - Weak TRS: #and(#false(),#false()) -> #false() #and(#false(),#true()) -> #false() #and(#true(),#false()) -> #false() #and(#true(),#true()) -> #true() #cklt(#EQ()) -> #false() #cklt(#GT()) -> #false() #cklt(#LT()) -> #true() #compare(#0(),#0()) -> #EQ() #compare(#0(),#neg(@y)) -> #GT() #compare(#0(),#pos(@y)) -> #LT() #compare(#0(),#s(@y)) -> #LT() #compare(#neg(@x),#0()) -> #LT() #compare(#neg(@x),#neg(@y)) -> #compare(@y,@x) #compare(#neg(@x),#pos(@y)) -> #LT() #compare(#pos(@x),#0()) -> #GT() #compare(#pos(@x),#neg(@y)) -> #GT() #compare(#pos(@x),#pos(@y)) -> #compare(@x,@y) #compare(#s(@x),#0()) -> #GT() #compare(#s(@x),#s(@y)) -> #compare(@x,@y) #eq(#0(),#0()) -> #true() #eq(#0(),#neg(@y)) -> #false() #eq(#0(),#pos(@y)) -> #false() #eq(#0(),#s(@y)) -> #false() #eq(#neg(@x),#0()) -> #false() #eq(#neg(@x),#neg(@y)) -> #eq(@x,@y) #eq(#neg(@x),#pos(@y)) -> #false() #eq(#pos(@x),#0()) -> #false() #eq(#pos(@x),#neg(@y)) -> #false() #eq(#pos(@x),#pos(@y)) -> #eq(@x,@y) #eq(#s(@x),#0()) -> #false() #eq(#s(@x),#s(@y)) -> #eq(@x,@y) #eq(::(@x_1,@x_2),::(@y_1,@y_2)) -> #and(#eq(@x_1,@y_1),#eq(@x_2,@y_2)) #eq(::(@x_1,@x_2),nil()) -> #false() #eq(nil(),::(@y_1,@y_2)) -> #false() #eq(nil(),nil()) -> #true() #equal(@x,@y) -> #eq(@x,@y) #less(@x,@y) -> #cklt(#compare(@x,@y)) #or(#false(),#false()) -> #false() #or(#false(),#true()) -> #true() #or(#true(),#false()) -> #true() #or(#true(),#true()) -> #true() and(@x,@y) -> #and(@x,@y) insert(@x,@l) -> insert#1(@l,@x) insert#1(::(@y,@ys),@x) -> insert#2(leq(@x,@y),@x,@y,@ys) insert#1(nil(),@x) -> ::(@x,nil()) insert#2(#false(),@x,@y,@ys) -> ::(@y,insert(@x,@ys)) insert#2(#true(),@x,@y,@ys) -> ::(@x,::(@y,@ys)) isortlist(@l) -> isortlist#1(@l) isortlist#1(::(@x,@xs)) -> insert(@x,isortlist(@xs)) isortlist#1(nil()) -> nil() leq(@l1,@l2) -> leq#1(@l1,@l2) leq#1(::(@x,@xs),@l2) -> leq#2(@l2,@x,@xs) leq#1(nil(),@l2) -> #true() leq#2(::(@y,@ys),@x,@xs) -> or(#less(@x,@y),and(#equal(@x,@y),leq(@xs,@ys))) leq#2(nil(),@x,@xs) -> #false() or(@x,@y) -> #or(@x,@y) - Signature: {#and/2,#cklt/1,#compare/2,#eq/2,#equal/2,#less/2,#or/2,and/2,insert/2,insert#1/2,insert#2/4,isortlist/1 ,isortlist#1/1,leq/2,leq#1/2,leq#2/3,or/2,#and#/2,#cklt#/1,#compare#/2,#eq#/2,#equal#/2,#less#/2,#or#/2 ,and#/2,insert#/2,insert#1#/2,insert#2#/4,isortlist#/1,isortlist#1#/1,leq#/2,leq#1#/2,leq#2#/3 ,or#/2} / {#0/0,#EQ/0,#GT/0,#LT/0,#false/0,#neg/1,#pos/1,#s/1,#true/0,::/2,nil/0,c_1/1,c_2/2,c_3/1,c_4/1 ,c_5/2,c_6/0,c_7/1,c_8/0,c_9/1,c_10/2,c_11/0,c_12/1,c_13/1,c_14/0,c_15/1,c_16/0,c_17/1,c_18/0,c_19/0,c_20/0 ,c_21/0,c_22/0,c_23/0,c_24/0,c_25/0,c_26/0,c_27/0,c_28/0,c_29/0,c_30/1,c_31/0,c_32/0,c_33/0,c_34/1,c_35/0 ,c_36/1,c_37/0,c_38/0,c_39/0,c_40/0,c_41/0,c_42/1,c_43/0,c_44/0,c_45/0,c_46/1,c_47/0,c_48/1,c_49/3,c_50/0 ,c_51/0,c_52/0,c_53/0,c_54/0,c_55/0,c_56/0} - Obligation: innermost runtime complexity wrt. defined symbols {#and#,#cklt#,#compare#,#eq#,#equal#,#less#,#or#,and# ,insert#,insert#1#,insert#2#,isortlist#,isortlist#1#,leq#,leq#1#,leq#2#,or#} and constructors {#0,#EQ,#GT ,#LT,#false,#neg,#pos,#s,#true,::,nil} + Applied Processor: Assumption {assumed = Certificate {spaceUB = Unknown, spaceLB = Unknown, timeUB = Poly (Just 0), timeLB = Unknown}} + Details: () *** Step 5.a:1.b:1: RemoveWeakSuffixes WORST_CASE(?,O(n^2)) + Considered Problem: - Strict DPs: insert#(@x,@l) -> c_4(insert#1#(@l,@x)) insert#1#(::(@y,@ys),@x) -> c_5(insert#2#(leq(@x,@y),@x,@y,@ys),leq#(@x,@y)) insert#2#(#false(),@x,@y,@ys) -> c_7(insert#(@x,@ys)) - Weak DPs: isortlist#(@l) -> c_9(isortlist#1#(@l)) isortlist#1#(::(@x,@xs)) -> c_10(insert#(@x,isortlist(@xs)),isortlist#(@xs)) leq#(@l1,@l2) -> c_12(leq#1#(@l1,@l2)) leq#1#(::(@x,@xs),@l2) -> c_13(leq#2#(@l2,@x,@xs)) leq#2#(::(@y,@ys),@x,@xs) -> c_15(leq#(@xs,@ys)) - Weak TRS: #and(#false(),#false()) -> #false() #and(#false(),#true()) -> #false() #and(#true(),#false()) -> #false() #and(#true(),#true()) -> #true() #cklt(#EQ()) -> #false() #cklt(#GT()) -> #false() #cklt(#LT()) -> #true() #compare(#0(),#0()) -> #EQ() #compare(#0(),#neg(@y)) -> #GT() #compare(#0(),#pos(@y)) -> #LT() #compare(#0(),#s(@y)) -> #LT() #compare(#neg(@x),#0()) -> #LT() #compare(#neg(@x),#neg(@y)) -> #compare(@y,@x) #compare(#neg(@x),#pos(@y)) -> #LT() #compare(#pos(@x),#0()) -> #GT() #compare(#pos(@x),#neg(@y)) -> #GT() #compare(#pos(@x),#pos(@y)) -> #compare(@x,@y) #compare(#s(@x),#0()) -> #GT() #compare(#s(@x),#s(@y)) -> #compare(@x,@y) #eq(#0(),#0()) -> #true() #eq(#0(),#neg(@y)) -> #false() #eq(#0(),#pos(@y)) -> #false() #eq(#0(),#s(@y)) -> #false() #eq(#neg(@x),#0()) -> #false() #eq(#neg(@x),#neg(@y)) -> #eq(@x,@y) #eq(#neg(@x),#pos(@y)) -> #false() #eq(#pos(@x),#0()) -> #false() #eq(#pos(@x),#neg(@y)) -> #false() #eq(#pos(@x),#pos(@y)) -> #eq(@x,@y) #eq(#s(@x),#0()) -> #false() #eq(#s(@x),#s(@y)) -> #eq(@x,@y) #eq(::(@x_1,@x_2),::(@y_1,@y_2)) -> #and(#eq(@x_1,@y_1),#eq(@x_2,@y_2)) #eq(::(@x_1,@x_2),nil()) -> #false() #eq(nil(),::(@y_1,@y_2)) -> #false() #eq(nil(),nil()) -> #true() #equal(@x,@y) -> #eq(@x,@y) #less(@x,@y) -> #cklt(#compare(@x,@y)) #or(#false(),#false()) -> #false() #or(#false(),#true()) -> #true() #or(#true(),#false()) -> #true() #or(#true(),#true()) -> #true() and(@x,@y) -> #and(@x,@y) insert(@x,@l) -> insert#1(@l,@x) insert#1(::(@y,@ys),@x) -> insert#2(leq(@x,@y),@x,@y,@ys) insert#1(nil(),@x) -> ::(@x,nil()) insert#2(#false(),@x,@y,@ys) -> ::(@y,insert(@x,@ys)) insert#2(#true(),@x,@y,@ys) -> ::(@x,::(@y,@ys)) isortlist(@l) -> isortlist#1(@l) isortlist#1(::(@x,@xs)) -> insert(@x,isortlist(@xs)) isortlist#1(nil()) -> nil() leq(@l1,@l2) -> leq#1(@l1,@l2) leq#1(::(@x,@xs),@l2) -> leq#2(@l2,@x,@xs) leq#1(nil(),@l2) -> #true() leq#2(::(@y,@ys),@x,@xs) -> or(#less(@x,@y),and(#equal(@x,@y),leq(@xs,@ys))) leq#2(nil(),@x,@xs) -> #false() or(@x,@y) -> #or(@x,@y) - Signature: {#and/2,#cklt/1,#compare/2,#eq/2,#equal/2,#less/2,#or/2,and/2,insert/2,insert#1/2,insert#2/4,isortlist/1 ,isortlist#1/1,leq/2,leq#1/2,leq#2/3,or/2,#and#/2,#cklt#/1,#compare#/2,#eq#/2,#equal#/2,#less#/2,#or#/2 ,and#/2,insert#/2,insert#1#/2,insert#2#/4,isortlist#/1,isortlist#1#/1,leq#/2,leq#1#/2,leq#2#/3 ,or#/2} / {#0/0,#EQ/0,#GT/0,#LT/0,#false/0,#neg/1,#pos/1,#s/1,#true/0,::/2,nil/0,c_1/1,c_2/2,c_3/1,c_4/1 ,c_5/2,c_6/0,c_7/1,c_8/0,c_9/1,c_10/2,c_11/0,c_12/1,c_13/1,c_14/0,c_15/1,c_16/0,c_17/1,c_18/0,c_19/0,c_20/0 ,c_21/0,c_22/0,c_23/0,c_24/0,c_25/0,c_26/0,c_27/0,c_28/0,c_29/0,c_30/1,c_31/0,c_32/0,c_33/0,c_34/1,c_35/0 ,c_36/1,c_37/0,c_38/0,c_39/0,c_40/0,c_41/0,c_42/1,c_43/0,c_44/0,c_45/0,c_46/1,c_47/0,c_48/1,c_49/3,c_50/0 ,c_51/0,c_52/0,c_53/0,c_54/0,c_55/0,c_56/0} - Obligation: innermost runtime complexity wrt. defined symbols {#and#,#cklt#,#compare#,#eq#,#equal#,#less#,#or#,and# ,insert#,insert#1#,insert#2#,isortlist#,isortlist#1#,leq#,leq#1#,leq#2#,or#} and constructors {#0,#EQ,#GT ,#LT,#false,#neg,#pos,#s,#true,::,nil} + Applied Processor: RemoveWeakSuffixes + Details: Consider the dependency graph 1:S:insert#(@x,@l) -> c_4(insert#1#(@l,@x)) -->_1 insert#1#(::(@y,@ys),@x) -> c_5(insert#2#(leq(@x,@y),@x,@y,@ys),leq#(@x,@y)):2 2:S:insert#1#(::(@y,@ys),@x) -> c_5(insert#2#(leq(@x,@y),@x,@y,@ys),leq#(@x,@y)) -->_2 leq#(@l1,@l2) -> c_12(leq#1#(@l1,@l2)):6 -->_1 insert#2#(#false(),@x,@y,@ys) -> c_7(insert#(@x,@ys)):3 3:S:insert#2#(#false(),@x,@y,@ys) -> c_7(insert#(@x,@ys)) -->_1 insert#(@x,@l) -> c_4(insert#1#(@l,@x)):1 4:W:isortlist#(@l) -> c_9(isortlist#1#(@l)) -->_1 isortlist#1#(::(@x,@xs)) -> c_10(insert#(@x,isortlist(@xs)),isortlist#(@xs)):5 5:W:isortlist#1#(::(@x,@xs)) -> c_10(insert#(@x,isortlist(@xs)),isortlist#(@xs)) -->_2 isortlist#(@l) -> c_9(isortlist#1#(@l)):4 -->_1 insert#(@x,@l) -> c_4(insert#1#(@l,@x)):1 6:W:leq#(@l1,@l2) -> c_12(leq#1#(@l1,@l2)) -->_1 leq#1#(::(@x,@xs),@l2) -> c_13(leq#2#(@l2,@x,@xs)):7 7:W:leq#1#(::(@x,@xs),@l2) -> c_13(leq#2#(@l2,@x,@xs)) -->_1 leq#2#(::(@y,@ys),@x,@xs) -> c_15(leq#(@xs,@ys)):8 8:W:leq#2#(::(@y,@ys),@x,@xs) -> c_15(leq#(@xs,@ys)) -->_1 leq#(@l1,@l2) -> c_12(leq#1#(@l1,@l2)):6 The following weak DPs constitute a sub-graph of the DG that is closed under successors. The DPs are removed. 6: leq#(@l1,@l2) -> c_12(leq#1#(@l1,@l2)) 8: leq#2#(::(@y,@ys),@x,@xs) -> c_15(leq#(@xs,@ys)) 7: leq#1#(::(@x,@xs),@l2) -> c_13(leq#2#(@l2,@x,@xs)) *** Step 5.a:1.b:2: SimplifyRHS WORST_CASE(?,O(n^2)) + Considered Problem: - Strict DPs: insert#(@x,@l) -> c_4(insert#1#(@l,@x)) insert#1#(::(@y,@ys),@x) -> c_5(insert#2#(leq(@x,@y),@x,@y,@ys),leq#(@x,@y)) insert#2#(#false(),@x,@y,@ys) -> c_7(insert#(@x,@ys)) - Weak DPs: isortlist#(@l) -> c_9(isortlist#1#(@l)) isortlist#1#(::(@x,@xs)) -> c_10(insert#(@x,isortlist(@xs)),isortlist#(@xs)) - Weak TRS: #and(#false(),#false()) -> #false() #and(#false(),#true()) -> #false() #and(#true(),#false()) -> #false() #and(#true(),#true()) -> #true() #cklt(#EQ()) -> #false() #cklt(#GT()) -> #false() #cklt(#LT()) -> #true() #compare(#0(),#0()) -> #EQ() #compare(#0(),#neg(@y)) -> #GT() #compare(#0(),#pos(@y)) -> #LT() #compare(#0(),#s(@y)) -> #LT() #compare(#neg(@x),#0()) -> #LT() #compare(#neg(@x),#neg(@y)) -> #compare(@y,@x) #compare(#neg(@x),#pos(@y)) -> #LT() #compare(#pos(@x),#0()) -> #GT() #compare(#pos(@x),#neg(@y)) -> #GT() #compare(#pos(@x),#pos(@y)) -> #compare(@x,@y) #compare(#s(@x),#0()) -> #GT() #compare(#s(@x),#s(@y)) -> #compare(@x,@y) #eq(#0(),#0()) -> #true() #eq(#0(),#neg(@y)) -> #false() #eq(#0(),#pos(@y)) -> #false() #eq(#0(),#s(@y)) -> #false() #eq(#neg(@x),#0()) -> #false() #eq(#neg(@x),#neg(@y)) -> #eq(@x,@y) #eq(#neg(@x),#pos(@y)) -> #false() #eq(#pos(@x),#0()) -> #false() #eq(#pos(@x),#neg(@y)) -> #false() #eq(#pos(@x),#pos(@y)) -> #eq(@x,@y) #eq(#s(@x),#0()) -> #false() #eq(#s(@x),#s(@y)) -> #eq(@x,@y) #eq(::(@x_1,@x_2),::(@y_1,@y_2)) -> #and(#eq(@x_1,@y_1),#eq(@x_2,@y_2)) #eq(::(@x_1,@x_2),nil()) -> #false() #eq(nil(),::(@y_1,@y_2)) -> #false() #eq(nil(),nil()) -> #true() #equal(@x,@y) -> #eq(@x,@y) #less(@x,@y) -> #cklt(#compare(@x,@y)) #or(#false(),#false()) -> #false() #or(#false(),#true()) -> #true() #or(#true(),#false()) -> #true() #or(#true(),#true()) -> #true() and(@x,@y) -> #and(@x,@y) insert(@x,@l) -> insert#1(@l,@x) insert#1(::(@y,@ys),@x) -> insert#2(leq(@x,@y),@x,@y,@ys) insert#1(nil(),@x) -> ::(@x,nil()) insert#2(#false(),@x,@y,@ys) -> ::(@y,insert(@x,@ys)) insert#2(#true(),@x,@y,@ys) -> ::(@x,::(@y,@ys)) isortlist(@l) -> isortlist#1(@l) isortlist#1(::(@x,@xs)) -> insert(@x,isortlist(@xs)) isortlist#1(nil()) -> nil() leq(@l1,@l2) -> leq#1(@l1,@l2) leq#1(::(@x,@xs),@l2) -> leq#2(@l2,@x,@xs) leq#1(nil(),@l2) -> #true() leq#2(::(@y,@ys),@x,@xs) -> or(#less(@x,@y),and(#equal(@x,@y),leq(@xs,@ys))) leq#2(nil(),@x,@xs) -> #false() or(@x,@y) -> #or(@x,@y) - Signature: {#and/2,#cklt/1,#compare/2,#eq/2,#equal/2,#less/2,#or/2,and/2,insert/2,insert#1/2,insert#2/4,isortlist/1 ,isortlist#1/1,leq/2,leq#1/2,leq#2/3,or/2,#and#/2,#cklt#/1,#compare#/2,#eq#/2,#equal#/2,#less#/2,#or#/2 ,and#/2,insert#/2,insert#1#/2,insert#2#/4,isortlist#/1,isortlist#1#/1,leq#/2,leq#1#/2,leq#2#/3 ,or#/2} / {#0/0,#EQ/0,#GT/0,#LT/0,#false/0,#neg/1,#pos/1,#s/1,#true/0,::/2,nil/0,c_1/1,c_2/2,c_3/1,c_4/1 ,c_5/2,c_6/0,c_7/1,c_8/0,c_9/1,c_10/2,c_11/0,c_12/1,c_13/1,c_14/0,c_15/1,c_16/0,c_17/1,c_18/0,c_19/0,c_20/0 ,c_21/0,c_22/0,c_23/0,c_24/0,c_25/0,c_26/0,c_27/0,c_28/0,c_29/0,c_30/1,c_31/0,c_32/0,c_33/0,c_34/1,c_35/0 ,c_36/1,c_37/0,c_38/0,c_39/0,c_40/0,c_41/0,c_42/1,c_43/0,c_44/0,c_45/0,c_46/1,c_47/0,c_48/1,c_49/3,c_50/0 ,c_51/0,c_52/0,c_53/0,c_54/0,c_55/0,c_56/0} - Obligation: innermost runtime complexity wrt. defined symbols {#and#,#cklt#,#compare#,#eq#,#equal#,#less#,#or#,and# ,insert#,insert#1#,insert#2#,isortlist#,isortlist#1#,leq#,leq#1#,leq#2#,or#} and constructors {#0,#EQ,#GT ,#LT,#false,#neg,#pos,#s,#true,::,nil} + Applied Processor: SimplifyRHS + Details: Consider the dependency graph 1:S:insert#(@x,@l) -> c_4(insert#1#(@l,@x)) -->_1 insert#1#(::(@y,@ys),@x) -> c_5(insert#2#(leq(@x,@y),@x,@y,@ys),leq#(@x,@y)):2 2:S:insert#1#(::(@y,@ys),@x) -> c_5(insert#2#(leq(@x,@y),@x,@y,@ys),leq#(@x,@y)) -->_1 insert#2#(#false(),@x,@y,@ys) -> c_7(insert#(@x,@ys)):3 3:S:insert#2#(#false(),@x,@y,@ys) -> c_7(insert#(@x,@ys)) -->_1 insert#(@x,@l) -> c_4(insert#1#(@l,@x)):1 4:W:isortlist#(@l) -> c_9(isortlist#1#(@l)) -->_1 isortlist#1#(::(@x,@xs)) -> c_10(insert#(@x,isortlist(@xs)),isortlist#(@xs)):5 5:W:isortlist#1#(::(@x,@xs)) -> c_10(insert#(@x,isortlist(@xs)),isortlist#(@xs)) -->_2 isortlist#(@l) -> c_9(isortlist#1#(@l)):4 -->_1 insert#(@x,@l) -> c_4(insert#1#(@l,@x)):1 Due to missing edges in the depndency graph, the right-hand sides of following rules could be simplified: insert#1#(::(@y,@ys),@x) -> c_5(insert#2#(leq(@x,@y),@x,@y,@ys)) *** Step 5.a:1.b:3: PredecessorEstimationCP WORST_CASE(?,O(n^2)) + Considered Problem: - Strict DPs: insert#(@x,@l) -> c_4(insert#1#(@l,@x)) insert#1#(::(@y,@ys),@x) -> c_5(insert#2#(leq(@x,@y),@x,@y,@ys)) insert#2#(#false(),@x,@y,@ys) -> c_7(insert#(@x,@ys)) - Weak DPs: isortlist#(@l) -> c_9(isortlist#1#(@l)) isortlist#1#(::(@x,@xs)) -> c_10(insert#(@x,isortlist(@xs)),isortlist#(@xs)) - Weak TRS: #and(#false(),#false()) -> #false() #and(#false(),#true()) -> #false() #and(#true(),#false()) -> #false() #and(#true(),#true()) -> #true() #cklt(#EQ()) -> #false() #cklt(#GT()) -> #false() #cklt(#LT()) -> #true() #compare(#0(),#0()) -> #EQ() #compare(#0(),#neg(@y)) -> #GT() #compare(#0(),#pos(@y)) -> #LT() #compare(#0(),#s(@y)) -> #LT() #compare(#neg(@x),#0()) -> #LT() #compare(#neg(@x),#neg(@y)) -> #compare(@y,@x) #compare(#neg(@x),#pos(@y)) -> #LT() #compare(#pos(@x),#0()) -> #GT() #compare(#pos(@x),#neg(@y)) -> #GT() #compare(#pos(@x),#pos(@y)) -> #compare(@x,@y) #compare(#s(@x),#0()) -> #GT() #compare(#s(@x),#s(@y)) -> #compare(@x,@y) #eq(#0(),#0()) -> #true() #eq(#0(),#neg(@y)) -> #false() #eq(#0(),#pos(@y)) -> #false() #eq(#0(),#s(@y)) -> #false() #eq(#neg(@x),#0()) -> #false() #eq(#neg(@x),#neg(@y)) -> #eq(@x,@y) #eq(#neg(@x),#pos(@y)) -> #false() #eq(#pos(@x),#0()) -> #false() #eq(#pos(@x),#neg(@y)) -> #false() #eq(#pos(@x),#pos(@y)) -> #eq(@x,@y) #eq(#s(@x),#0()) -> #false() #eq(#s(@x),#s(@y)) -> #eq(@x,@y) #eq(::(@x_1,@x_2),::(@y_1,@y_2)) -> #and(#eq(@x_1,@y_1),#eq(@x_2,@y_2)) #eq(::(@x_1,@x_2),nil()) -> #false() #eq(nil(),::(@y_1,@y_2)) -> #false() #eq(nil(),nil()) -> #true() #equal(@x,@y) -> #eq(@x,@y) #less(@x,@y) -> #cklt(#compare(@x,@y)) #or(#false(),#false()) -> #false() #or(#false(),#true()) -> #true() #or(#true(),#false()) -> #true() #or(#true(),#true()) -> #true() and(@x,@y) -> #and(@x,@y) insert(@x,@l) -> insert#1(@l,@x) insert#1(::(@y,@ys),@x) -> insert#2(leq(@x,@y),@x,@y,@ys) insert#1(nil(),@x) -> ::(@x,nil()) insert#2(#false(),@x,@y,@ys) -> ::(@y,insert(@x,@ys)) insert#2(#true(),@x,@y,@ys) -> ::(@x,::(@y,@ys)) isortlist(@l) -> isortlist#1(@l) isortlist#1(::(@x,@xs)) -> insert(@x,isortlist(@xs)) isortlist#1(nil()) -> nil() leq(@l1,@l2) -> leq#1(@l1,@l2) leq#1(::(@x,@xs),@l2) -> leq#2(@l2,@x,@xs) leq#1(nil(),@l2) -> #true() leq#2(::(@y,@ys),@x,@xs) -> or(#less(@x,@y),and(#equal(@x,@y),leq(@xs,@ys))) leq#2(nil(),@x,@xs) -> #false() or(@x,@y) -> #or(@x,@y) - Signature: {#and/2,#cklt/1,#compare/2,#eq/2,#equal/2,#less/2,#or/2,and/2,insert/2,insert#1/2,insert#2/4,isortlist/1 ,isortlist#1/1,leq/2,leq#1/2,leq#2/3,or/2,#and#/2,#cklt#/1,#compare#/2,#eq#/2,#equal#/2,#less#/2,#or#/2 ,and#/2,insert#/2,insert#1#/2,insert#2#/4,isortlist#/1,isortlist#1#/1,leq#/2,leq#1#/2,leq#2#/3 ,or#/2} / {#0/0,#EQ/0,#GT/0,#LT/0,#false/0,#neg/1,#pos/1,#s/1,#true/0,::/2,nil/0,c_1/1,c_2/2,c_3/1,c_4/1 ,c_5/1,c_6/0,c_7/1,c_8/0,c_9/1,c_10/2,c_11/0,c_12/1,c_13/1,c_14/0,c_15/1,c_16/0,c_17/1,c_18/0,c_19/0,c_20/0 ,c_21/0,c_22/0,c_23/0,c_24/0,c_25/0,c_26/0,c_27/0,c_28/0,c_29/0,c_30/1,c_31/0,c_32/0,c_33/0,c_34/1,c_35/0 ,c_36/1,c_37/0,c_38/0,c_39/0,c_40/0,c_41/0,c_42/1,c_43/0,c_44/0,c_45/0,c_46/1,c_47/0,c_48/1,c_49/3,c_50/0 ,c_51/0,c_52/0,c_53/0,c_54/0,c_55/0,c_56/0} - Obligation: innermost runtime complexity wrt. defined symbols {#and#,#cklt#,#compare#,#eq#,#equal#,#less#,#or#,and# ,insert#,insert#1#,insert#2#,isortlist#,isortlist#1#,leq#,leq#1#,leq#2#,or#} and constructors {#0,#EQ,#GT ,#LT,#false,#neg,#pos,#s,#true,::,nil} + Applied Processor: PredecessorEstimationCP {onSelectionCP = any intersect of rules of CDG leaf and strict-rules, withComplexityPair = NaturalMI {miDimension = 3, miDegree = 2, miKind = Algebraic, uargs = UArgs, urules = URules, selector = Nothing}} + Details: We first use the processor NaturalMI {miDimension = 3, miDegree = 2, miKind = Algebraic, uargs = UArgs, urules = URules, selector = Nothing} to orient following rules strictly: 2: insert#1#(::(@y,@ys),@x) -> c_5(insert#2#(leq(@x,@y),@x,@y,@ys)) Consider the set of all dependency pairs 1: insert#(@x,@l) -> c_4(insert#1#(@l,@x)) 2: insert#1#(::(@y,@ys),@x) -> c_5(insert#2#(leq(@x,@y),@x,@y,@ys)) 3: insert#2#(#false(),@x,@y,@ys) -> c_7(insert#(@x,@ys)) 4: isortlist#(@l) -> c_9(isortlist#1#(@l)) 5: isortlist#1#(::(@x,@xs)) -> c_10(insert#(@x,isortlist(@xs)),isortlist#(@xs)) Processor NaturalMI {miDimension = 3, miDegree = 2, miKind = Algebraic, uargs = UArgs, urules = URules, selector = Nothing}induces the complexity certificateTIME (?,O(n^2)) SPACE(?,?)on application of the dependency pairs {2} These cover all (indirect) predecessors of dependency pairs {2,3} their number of applications is equally bounded. The dependency pairs are shifted into the weak component. **** Step 5.a:1.b:3.a:1: NaturalMI WORST_CASE(?,O(n^2)) + Considered Problem: - Strict DPs: insert#(@x,@l) -> c_4(insert#1#(@l,@x)) insert#1#(::(@y,@ys),@x) -> c_5(insert#2#(leq(@x,@y),@x,@y,@ys)) insert#2#(#false(),@x,@y,@ys) -> c_7(insert#(@x,@ys)) - Weak DPs: isortlist#(@l) -> c_9(isortlist#1#(@l)) isortlist#1#(::(@x,@xs)) -> c_10(insert#(@x,isortlist(@xs)),isortlist#(@xs)) - Weak TRS: #and(#false(),#false()) -> #false() #and(#false(),#true()) -> #false() #and(#true(),#false()) -> #false() #and(#true(),#true()) -> #true() #cklt(#EQ()) -> #false() #cklt(#GT()) -> #false() #cklt(#LT()) -> #true() #compare(#0(),#0()) -> #EQ() #compare(#0(),#neg(@y)) -> #GT() #compare(#0(),#pos(@y)) -> #LT() #compare(#0(),#s(@y)) -> #LT() #compare(#neg(@x),#0()) -> #LT() #compare(#neg(@x),#neg(@y)) -> #compare(@y,@x) #compare(#neg(@x),#pos(@y)) -> #LT() #compare(#pos(@x),#0()) -> #GT() #compare(#pos(@x),#neg(@y)) -> #GT() #compare(#pos(@x),#pos(@y)) -> #compare(@x,@y) #compare(#s(@x),#0()) -> #GT() #compare(#s(@x),#s(@y)) -> #compare(@x,@y) #eq(#0(),#0()) -> #true() #eq(#0(),#neg(@y)) -> #false() #eq(#0(),#pos(@y)) -> #false() #eq(#0(),#s(@y)) -> #false() #eq(#neg(@x),#0()) -> #false() #eq(#neg(@x),#neg(@y)) -> #eq(@x,@y) #eq(#neg(@x),#pos(@y)) -> #false() #eq(#pos(@x),#0()) -> #false() #eq(#pos(@x),#neg(@y)) -> #false() #eq(#pos(@x),#pos(@y)) -> #eq(@x,@y) #eq(#s(@x),#0()) -> #false() #eq(#s(@x),#s(@y)) -> #eq(@x,@y) #eq(::(@x_1,@x_2),::(@y_1,@y_2)) -> #and(#eq(@x_1,@y_1),#eq(@x_2,@y_2)) #eq(::(@x_1,@x_2),nil()) -> #false() #eq(nil(),::(@y_1,@y_2)) -> #false() #eq(nil(),nil()) -> #true() #equal(@x,@y) -> #eq(@x,@y) #less(@x,@y) -> #cklt(#compare(@x,@y)) #or(#false(),#false()) -> #false() #or(#false(),#true()) -> #true() #or(#true(),#false()) -> #true() #or(#true(),#true()) -> #true() and(@x,@y) -> #and(@x,@y) insert(@x,@l) -> insert#1(@l,@x) insert#1(::(@y,@ys),@x) -> insert#2(leq(@x,@y),@x,@y,@ys) insert#1(nil(),@x) -> ::(@x,nil()) insert#2(#false(),@x,@y,@ys) -> ::(@y,insert(@x,@ys)) insert#2(#true(),@x,@y,@ys) -> ::(@x,::(@y,@ys)) isortlist(@l) -> isortlist#1(@l) isortlist#1(::(@x,@xs)) -> insert(@x,isortlist(@xs)) isortlist#1(nil()) -> nil() leq(@l1,@l2) -> leq#1(@l1,@l2) leq#1(::(@x,@xs),@l2) -> leq#2(@l2,@x,@xs) leq#1(nil(),@l2) -> #true() leq#2(::(@y,@ys),@x,@xs) -> or(#less(@x,@y),and(#equal(@x,@y),leq(@xs,@ys))) leq#2(nil(),@x,@xs) -> #false() or(@x,@y) -> #or(@x,@y) - Signature: {#and/2,#cklt/1,#compare/2,#eq/2,#equal/2,#less/2,#or/2,and/2,insert/2,insert#1/2,insert#2/4,isortlist/1 ,isortlist#1/1,leq/2,leq#1/2,leq#2/3,or/2,#and#/2,#cklt#/1,#compare#/2,#eq#/2,#equal#/2,#less#/2,#or#/2 ,and#/2,insert#/2,insert#1#/2,insert#2#/4,isortlist#/1,isortlist#1#/1,leq#/2,leq#1#/2,leq#2#/3 ,or#/2} / {#0/0,#EQ/0,#GT/0,#LT/0,#false/0,#neg/1,#pos/1,#s/1,#true/0,::/2,nil/0,c_1/1,c_2/2,c_3/1,c_4/1 ,c_5/1,c_6/0,c_7/1,c_8/0,c_9/1,c_10/2,c_11/0,c_12/1,c_13/1,c_14/0,c_15/1,c_16/0,c_17/1,c_18/0,c_19/0,c_20/0 ,c_21/0,c_22/0,c_23/0,c_24/0,c_25/0,c_26/0,c_27/0,c_28/0,c_29/0,c_30/1,c_31/0,c_32/0,c_33/0,c_34/1,c_35/0 ,c_36/1,c_37/0,c_38/0,c_39/0,c_40/0,c_41/0,c_42/1,c_43/0,c_44/0,c_45/0,c_46/1,c_47/0,c_48/1,c_49/3,c_50/0 ,c_51/0,c_52/0,c_53/0,c_54/0,c_55/0,c_56/0} - Obligation: innermost runtime complexity wrt. defined symbols {#and#,#cklt#,#compare#,#eq#,#equal#,#less#,#or#,and# ,insert#,insert#1#,insert#2#,isortlist#,isortlist#1#,leq#,leq#1#,leq#2#,or#} and constructors {#0,#EQ,#GT ,#LT,#false,#neg,#pos,#s,#true,::,nil} + Applied Processor: NaturalMI {miDimension = 3, miDegree = 2, miKind = Algebraic, uargs = UArgs, urules = URules, selector = Just first alternative for predecessorEstimation on any intersect of rules of CDG leaf and strict-rules} + Details: We apply a matrix interpretation of kind constructor based matrix interpretation (containing no more than 2 non-zero interpretation-entries in the diagonal of the component-wise maxima): The following argument positions are considered usable: uargs(c_4) = {1}, uargs(c_5) = {1}, uargs(c_7) = {1}, uargs(c_9) = {1}, uargs(c_10) = {1,2} Following symbols are considered usable: {#or,insert,insert#1,insert#2,isortlist,isortlist#1,leq,leq#1,leq#2,or,#and#,#cklt#,#compare#,#eq#,#equal# ,#less#,#or#,and#,insert#,insert#1#,insert#2#,isortlist#,isortlist#1#,leq#,leq#1#,leq#2#,or#} TcT has computed the following interpretation: p(#0) = [1] [0] [0] p(#EQ) = [0] [0] [0] p(#GT) = [0] [0] [0] p(#LT) = [0] [0] [0] p(#and) = [1 1 1] [0 0 0] [0] [1 0 0] x1 + [0 1 0] x2 + [0] [0 0 0] [0 0 0] [0] p(#cklt) = [0] [0] [1] p(#compare) = [0 0 0] [1 0 1] [0] [0 1 0] x1 + [1 0 0] x2 + [1] [1 1 0] [0 0 0] [0] p(#eq) = [0 0 1] [0 0 1] [0] [1 1 0] x1 + [0 0 0] x2 + [0] [1 0 0] [0 0 1] [0] p(#equal) = [0 0 0] [0 0 0] [1] [0 1 1] x1 + [1 0 0] x2 + [0] [0 1 1] [0 1 0] [1] p(#false) = [0] [1] [0] p(#less) = [0] [0] [0] p(#neg) = [0] [1] [1] p(#or) = [0] [1] [0] p(#pos) = [0 0 0] [0] [0 0 1] x1 + [1] [0 0 0] [0] p(#s) = [0] [1] [1] p(#true) = [0] [1] [0] p(::) = [1 0 1] [1 1 0] [0] [0 0 0] x1 + [0 0 1] x2 + [0] [0 0 0] [0 0 1] [1] p(and) = [0 1 1] [0 0 0] [0] [1 0 0] x1 + [1 0 0] x2 + [1] [0 0 0] [0 0 0] [0] p(insert) = [1 0 1] [1 1 0] [0] [0 0 0] x1 + [0 0 1] x2 + [0] [0 0 0] [0 0 1] [1] p(insert#1) = [1 1 0] [1 0 1] [0] [0 0 1] x1 + [0 0 0] x2 + [0] [0 0 1] [0 0 0] [1] p(insert#2) = [0 0 0] [1 0 1] [1 0 1] [1 1 1] [0] [0 0 0] x1 + [0 0 0] x2 + [0 0 0] x3 + [0 0 1] x4 + [1] [0 1 0] [0 0 0] [0 0 0] [0 0 1] [1] p(isortlist) = [1 1 0] [0] [0 0 1] x1 + [0] [0 0 1] [0] p(isortlist#1) = [1 1 0] [0] [0 0 1] x1 + [0] [0 0 1] [0] p(leq) = [1 0 1] [1 0 0] [0] [0 0 0] x1 + [0 0 0] x2 + [1] [0 1 0] [0 0 0] [0] p(leq#1) = [0 0 1] [1 0 0] [0] [0 0 0] x1 + [0 0 0] x2 + [1] [0 0 0] [0 0 0] [0] p(leq#2) = [0 0 1] [0] [0 0 0] x3 + [1] [0 0 0] [0] p(nil) = [0] [0] [0] p(or) = [0] [1] [0] p(#and#) = [0] [0] [0] p(#cklt#) = [0] [0] [0] p(#compare#) = [0] [0] [0] p(#eq#) = [0] [0] [0] p(#equal#) = [0] [0] [0] p(#less#) = [0] [0] [0] p(#or#) = [0] [0] [0] p(and#) = [0] [0] [0] p(insert#) = [0 0 0] [0 0 1] [0] [0 0 0] x1 + [0 0 0] x2 + [1] [1 0 1] [0 0 0] [0] p(insert#1#) = [0 0 1] [0 0 0] [0] [0 0 1] x1 + [1 0 1] x2 + [0] [1 1 0] [1 0 1] [1] p(insert#2#) = [0 0 0] [0 0 1] [0] [1 0 1] x2 + [0 0 0] x4 + [0] [0 0 0] [1 0 0] [1] p(isortlist#) = [1 1 0] [0] [0 1 1] x1 + [0] [0 0 1] [0] p(isortlist#1#) = [1 1 0] [0] [1 0 0] x1 + [1] [1 1 1] [1] p(leq#) = [0] [0] [0] p(leq#1#) = [0] [0] [0] p(leq#2#) = [0] [0] [0] p(or#) = [0] [0] [0] p(c_1) = [0] [0] [0] p(c_2) = [0] [0] [0] p(c_3) = [0] [0] [0] p(c_4) = [1 0 0] [0] [0 0 0] x1 + [0] [0 0 0] [0] p(c_5) = [1 0 0] [0] [0 1 0] x1 + [0] [0 0 0] [1] p(c_6) = [0] [0] [0] p(c_7) = [1 0 0] [0] [0 0 1] x1 + [0] [0 0 0] [0] p(c_8) = [0] [0] [0] p(c_9) = [1 0 0] [0] [0 0 0] x1 + [0] [0 0 0] [0] p(c_10) = [1 0 1] [1 0 0] [0] [0 0 1] x1 + [1 0 0] x2 + [1] [0 1 1] [0 1 1] [1] p(c_11) = [0] [0] [0] p(c_12) = [0] [0] [0] p(c_13) = [0] [0] [0] p(c_14) = [0] [0] [0] p(c_15) = [0] [0] [0] p(c_16) = [0] [0] [0] p(c_17) = [0] [0] [0] p(c_18) = [0] [0] [0] p(c_19) = [0] [0] [0] p(c_20) = [0] [0] [0] p(c_21) = [0] [0] [0] p(c_22) = [0] [0] [0] p(c_23) = [0] [0] [0] p(c_24) = [0] [0] [0] p(c_25) = [0] [0] [0] p(c_26) = [0] [0] [0] p(c_27) = [0] [0] [0] p(c_28) = [0] [0] [0] p(c_29) = [0] [0] [0] p(c_30) = [0] [0] [0] p(c_31) = [0] [0] [0] p(c_32) = [0] [0] [0] p(c_33) = [0] [0] [0] p(c_34) = [0] [0] [0] p(c_35) = [0] [0] [0] p(c_36) = [0] [0] [0] p(c_37) = [0] [0] [0] p(c_38) = [0] [0] [0] p(c_39) = [0] [0] [0] p(c_40) = [0] [0] [0] p(c_41) = [0] [0] [0] p(c_42) = [0] [0] [0] p(c_43) = [0] [0] [0] p(c_44) = [0] [0] [0] p(c_45) = [0] [0] [0] p(c_46) = [0] [0] [0] p(c_47) = [0] [0] [0] p(c_48) = [0] [0] [0] p(c_49) = [0] [0] [0] p(c_50) = [0] [0] [0] p(c_51) = [0] [0] [0] p(c_52) = [0] [0] [0] p(c_53) = [0] [0] [0] p(c_54) = [0] [0] [0] p(c_55) = [0] [0] [0] p(c_56) = [0] [0] [0] Following rules are strictly oriented: insert#1#(::(@y,@ys),@x) = [0 0 0] [0 0 0] [0 0 1] [1] [1 0 1] @x + [0 0 0] @y + [0 0 1] @ys + [1] [1 0 1] [1 0 1] [1 1 1] [1] > [0 0 0] [0 0 1] [0] [1 0 1] @x + [0 0 0] @ys + [0] [0 0 0] [0 0 0] [1] = c_5(insert#2#(leq(@x,@y),@x,@y,@ys)) Following rules are (at-least) weakly oriented: insert#(@x,@l) = [0 0 1] [0 0 0] [0] [0 0 0] @l + [0 0 0] @x + [1] [0 0 0] [1 0 1] [0] >= [0 0 1] [0] [0 0 0] @l + [0] [0 0 0] [0] = c_4(insert#1#(@l,@x)) insert#2#(#false(),@x,@y,@ys) = [0 0 0] [0 0 1] [0] [1 0 1] @x + [0 0 0] @ys + [0] [0 0 0] [1 0 0] [1] >= [0 0 0] [0 0 1] [0] [1 0 1] @x + [0 0 0] @ys + [0] [0 0 0] [0 0 0] [0] = c_7(insert#(@x,@ys)) isortlist#(@l) = [1 1 0] [0] [0 1 1] @l + [0] [0 0 1] [0] >= [1 1 0] [0] [0 0 0] @l + [0] [0 0 0] [0] = c_9(isortlist#1#(@l)) isortlist#1#(::(@x,@xs)) = [1 0 1] [1 1 1] [0] [1 0 1] @x + [1 1 0] @xs + [1] [1 0 1] [1 1 2] [2] >= [1 0 1] [1 1 1] [0] [1 0 1] @x + [1 1 0] @xs + [1] [1 0 1] [0 1 2] [2] = c_10(insert#(@x,isortlist(@xs)),isortlist#(@xs)) #or(#false(),#false()) = [0] [1] [0] >= [0] [1] [0] = #false() #or(#false(),#true()) = [0] [1] [0] >= [0] [1] [0] = #true() #or(#true(),#false()) = [0] [1] [0] >= [0] [1] [0] = #true() #or(#true(),#true()) = [0] [1] [0] >= [0] [1] [0] = #true() insert(@x,@l) = [1 1 0] [1 0 1] [0] [0 0 1] @l + [0 0 0] @x + [0] [0 0 1] [0 0 0] [1] >= [1 1 0] [1 0 1] [0] [0 0 1] @l + [0 0 0] @x + [0] [0 0 1] [0 0 0] [1] = insert#1(@l,@x) insert#1(::(@y,@ys),@x) = [1 0 1] [1 0 1] [1 1 1] [0] [0 0 0] @x + [0 0 0] @y + [0 0 1] @ys + [1] [0 0 0] [0 0 0] [0 0 1] [2] >= [1 0 1] [1 0 1] [1 1 1] [0] [0 0 0] @x + [0 0 0] @y + [0 0 1] @ys + [1] [0 0 0] [0 0 0] [0 0 1] [2] = insert#2(leq(@x,@y),@x,@y,@ys) insert#1(nil(),@x) = [1 0 1] [0] [0 0 0] @x + [0] [0 0 0] [1] >= [1 0 1] [0] [0 0 0] @x + [0] [0 0 0] [1] = ::(@x,nil()) insert#2(#false(),@x,@y,@ys) = [1 0 1] [1 0 1] [1 1 1] [0] [0 0 0] @x + [0 0 0] @y + [0 0 1] @ys + [1] [0 0 0] [0 0 0] [0 0 1] [2] >= [1 0 1] [1 0 1] [1 1 1] [0] [0 0 0] @x + [0 0 0] @y + [0 0 1] @ys + [1] [0 0 0] [0 0 0] [0 0 1] [2] = ::(@y,insert(@x,@ys)) insert#2(#true(),@x,@y,@ys) = [1 0 1] [1 0 1] [1 1 1] [0] [0 0 0] @x + [0 0 0] @y + [0 0 1] @ys + [1] [0 0 0] [0 0 0] [0 0 1] [2] >= [1 0 1] [1 0 1] [1 1 1] [0] [0 0 0] @x + [0 0 0] @y + [0 0 1] @ys + [1] [0 0 0] [0 0 0] [0 0 1] [2] = ::(@x,::(@y,@ys)) isortlist(@l) = [1 1 0] [0] [0 0 1] @l + [0] [0 0 1] [0] >= [1 1 0] [0] [0 0 1] @l + [0] [0 0 1] [0] = isortlist#1(@l) isortlist#1(::(@x,@xs)) = [1 0 1] [1 1 1] [0] [0 0 0] @x + [0 0 1] @xs + [1] [0 0 0] [0 0 1] [1] >= [1 0 1] [1 1 1] [0] [0 0 0] @x + [0 0 1] @xs + [0] [0 0 0] [0 0 1] [1] = insert(@x,isortlist(@xs)) isortlist#1(nil()) = [0] [0] [0] >= [0] [0] [0] = nil() leq(@l1,@l2) = [1 0 1] [1 0 0] [0] [0 0 0] @l1 + [0 0 0] @l2 + [1] [0 1 0] [0 0 0] [0] >= [0 0 1] [1 0 0] [0] [0 0 0] @l1 + [0 0 0] @l2 + [1] [0 0 0] [0 0 0] [0] = leq#1(@l1,@l2) leq#1(::(@x,@xs),@l2) = [1 0 0] [0 0 1] [1] [0 0 0] @l2 + [0 0 0] @xs + [1] [0 0 0] [0 0 0] [0] >= [0 0 1] [0] [0 0 0] @xs + [1] [0 0 0] [0] = leq#2(@l2,@x,@xs) leq#1(nil(),@l2) = [1 0 0] [0] [0 0 0] @l2 + [1] [0 0 0] [0] >= [0] [1] [0] = #true() leq#2(::(@y,@ys),@x,@xs) = [0 0 1] [0] [0 0 0] @xs + [1] [0 0 0] [0] >= [0] [1] [0] = or(#less(@x,@y),and(#equal(@x,@y),leq(@xs,@ys))) leq#2(nil(),@x,@xs) = [0 0 1] [0] [0 0 0] @xs + [1] [0 0 0] [0] >= [0] [1] [0] = #false() or(@x,@y) = [0] [1] [0] >= [0] [1] [0] = #or(@x,@y) **** Step 5.a:1.b:3.a:2: Assumption WORST_CASE(?,O(1)) + Considered Problem: - Strict DPs: insert#(@x,@l) -> c_4(insert#1#(@l,@x)) insert#2#(#false(),@x,@y,@ys) -> c_7(insert#(@x,@ys)) - Weak DPs: insert#1#(::(@y,@ys),@x) -> c_5(insert#2#(leq(@x,@y),@x,@y,@ys)) isortlist#(@l) -> c_9(isortlist#1#(@l)) isortlist#1#(::(@x,@xs)) -> c_10(insert#(@x,isortlist(@xs)),isortlist#(@xs)) - Weak TRS: #and(#false(),#false()) -> #false() #and(#false(),#true()) -> #false() #and(#true(),#false()) -> #false() #and(#true(),#true()) -> #true() #cklt(#EQ()) -> #false() #cklt(#GT()) -> #false() #cklt(#LT()) -> #true() #compare(#0(),#0()) -> #EQ() #compare(#0(),#neg(@y)) -> #GT() #compare(#0(),#pos(@y)) -> #LT() #compare(#0(),#s(@y)) -> #LT() #compare(#neg(@x),#0()) -> #LT() #compare(#neg(@x),#neg(@y)) -> #compare(@y,@x) #compare(#neg(@x),#pos(@y)) -> #LT() #compare(#pos(@x),#0()) -> #GT() #compare(#pos(@x),#neg(@y)) -> #GT() #compare(#pos(@x),#pos(@y)) -> #compare(@x,@y) #compare(#s(@x),#0()) -> #GT() #compare(#s(@x),#s(@y)) -> #compare(@x,@y) #eq(#0(),#0()) -> #true() #eq(#0(),#neg(@y)) -> #false() #eq(#0(),#pos(@y)) -> #false() #eq(#0(),#s(@y)) -> #false() #eq(#neg(@x),#0()) -> #false() #eq(#neg(@x),#neg(@y)) -> #eq(@x,@y) #eq(#neg(@x),#pos(@y)) -> #false() #eq(#pos(@x),#0()) -> #false() #eq(#pos(@x),#neg(@y)) -> #false() #eq(#pos(@x),#pos(@y)) -> #eq(@x,@y) #eq(#s(@x),#0()) -> #false() #eq(#s(@x),#s(@y)) -> #eq(@x,@y) #eq(::(@x_1,@x_2),::(@y_1,@y_2)) -> #and(#eq(@x_1,@y_1),#eq(@x_2,@y_2)) #eq(::(@x_1,@x_2),nil()) -> #false() #eq(nil(),::(@y_1,@y_2)) -> #false() #eq(nil(),nil()) -> #true() #equal(@x,@y) -> #eq(@x,@y) #less(@x,@y) -> #cklt(#compare(@x,@y)) #or(#false(),#false()) -> #false() #or(#false(),#true()) -> #true() #or(#true(),#false()) -> #true() #or(#true(),#true()) -> #true() and(@x,@y) -> #and(@x,@y) insert(@x,@l) -> insert#1(@l,@x) insert#1(::(@y,@ys),@x) -> insert#2(leq(@x,@y),@x,@y,@ys) insert#1(nil(),@x) -> ::(@x,nil()) insert#2(#false(),@x,@y,@ys) -> ::(@y,insert(@x,@ys)) insert#2(#true(),@x,@y,@ys) -> ::(@x,::(@y,@ys)) isortlist(@l) -> isortlist#1(@l) isortlist#1(::(@x,@xs)) -> insert(@x,isortlist(@xs)) isortlist#1(nil()) -> nil() leq(@l1,@l2) -> leq#1(@l1,@l2) leq#1(::(@x,@xs),@l2) -> leq#2(@l2,@x,@xs) leq#1(nil(),@l2) -> #true() leq#2(::(@y,@ys),@x,@xs) -> or(#less(@x,@y),and(#equal(@x,@y),leq(@xs,@ys))) leq#2(nil(),@x,@xs) -> #false() or(@x,@y) -> #or(@x,@y) - Signature: {#and/2,#cklt/1,#compare/2,#eq/2,#equal/2,#less/2,#or/2,and/2,insert/2,insert#1/2,insert#2/4,isortlist/1 ,isortlist#1/1,leq/2,leq#1/2,leq#2/3,or/2,#and#/2,#cklt#/1,#compare#/2,#eq#/2,#equal#/2,#less#/2,#or#/2 ,and#/2,insert#/2,insert#1#/2,insert#2#/4,isortlist#/1,isortlist#1#/1,leq#/2,leq#1#/2,leq#2#/3 ,or#/2} / {#0/0,#EQ/0,#GT/0,#LT/0,#false/0,#neg/1,#pos/1,#s/1,#true/0,::/2,nil/0,c_1/1,c_2/2,c_3/1,c_4/1 ,c_5/1,c_6/0,c_7/1,c_8/0,c_9/1,c_10/2,c_11/0,c_12/1,c_13/1,c_14/0,c_15/1,c_16/0,c_17/1,c_18/0,c_19/0,c_20/0 ,c_21/0,c_22/0,c_23/0,c_24/0,c_25/0,c_26/0,c_27/0,c_28/0,c_29/0,c_30/1,c_31/0,c_32/0,c_33/0,c_34/1,c_35/0 ,c_36/1,c_37/0,c_38/0,c_39/0,c_40/0,c_41/0,c_42/1,c_43/0,c_44/0,c_45/0,c_46/1,c_47/0,c_48/1,c_49/3,c_50/0 ,c_51/0,c_52/0,c_53/0,c_54/0,c_55/0,c_56/0} - Obligation: innermost runtime complexity wrt. defined symbols {#and#,#cklt#,#compare#,#eq#,#equal#,#less#,#or#,and# ,insert#,insert#1#,insert#2#,isortlist#,isortlist#1#,leq#,leq#1#,leq#2#,or#} and constructors {#0,#EQ,#GT ,#LT,#false,#neg,#pos,#s,#true,::,nil} + Applied Processor: Assumption {assumed = Certificate {spaceUB = Unknown, spaceLB = Unknown, timeUB = Poly (Just 0), timeLB = Unknown}} + Details: () **** Step 5.a:1.b:3.b:1: PredecessorEstimationCP WORST_CASE(?,O(n^2)) + Considered Problem: - Strict DPs: insert#(@x,@l) -> c_4(insert#1#(@l,@x)) - Weak DPs: insert#1#(::(@y,@ys),@x) -> c_5(insert#2#(leq(@x,@y),@x,@y,@ys)) insert#2#(#false(),@x,@y,@ys) -> c_7(insert#(@x,@ys)) isortlist#(@l) -> c_9(isortlist#1#(@l)) isortlist#1#(::(@x,@xs)) -> c_10(insert#(@x,isortlist(@xs)),isortlist#(@xs)) - Weak TRS: #and(#false(),#false()) -> #false() #and(#false(),#true()) -> #false() #and(#true(),#false()) -> #false() #and(#true(),#true()) -> #true() #cklt(#EQ()) -> #false() #cklt(#GT()) -> #false() #cklt(#LT()) -> #true() #compare(#0(),#0()) -> #EQ() #compare(#0(),#neg(@y)) -> #GT() #compare(#0(),#pos(@y)) -> #LT() #compare(#0(),#s(@y)) -> #LT() #compare(#neg(@x),#0()) -> #LT() #compare(#neg(@x),#neg(@y)) -> #compare(@y,@x) #compare(#neg(@x),#pos(@y)) -> #LT() #compare(#pos(@x),#0()) -> #GT() #compare(#pos(@x),#neg(@y)) -> #GT() #compare(#pos(@x),#pos(@y)) -> #compare(@x,@y) #compare(#s(@x),#0()) -> #GT() #compare(#s(@x),#s(@y)) -> #compare(@x,@y) #eq(#0(),#0()) -> #true() #eq(#0(),#neg(@y)) -> #false() #eq(#0(),#pos(@y)) -> #false() #eq(#0(),#s(@y)) -> #false() #eq(#neg(@x),#0()) -> #false() #eq(#neg(@x),#neg(@y)) -> #eq(@x,@y) #eq(#neg(@x),#pos(@y)) -> #false() #eq(#pos(@x),#0()) -> #false() #eq(#pos(@x),#neg(@y)) -> #false() #eq(#pos(@x),#pos(@y)) -> #eq(@x,@y) #eq(#s(@x),#0()) -> #false() #eq(#s(@x),#s(@y)) -> #eq(@x,@y) #eq(::(@x_1,@x_2),::(@y_1,@y_2)) -> #and(#eq(@x_1,@y_1),#eq(@x_2,@y_2)) #eq(::(@x_1,@x_2),nil()) -> #false() #eq(nil(),::(@y_1,@y_2)) -> #false() #eq(nil(),nil()) -> #true() #equal(@x,@y) -> #eq(@x,@y) #less(@x,@y) -> #cklt(#compare(@x,@y)) #or(#false(),#false()) -> #false() #or(#false(),#true()) -> #true() #or(#true(),#false()) -> #true() #or(#true(),#true()) -> #true() and(@x,@y) -> #and(@x,@y) insert(@x,@l) -> insert#1(@l,@x) insert#1(::(@y,@ys),@x) -> insert#2(leq(@x,@y),@x,@y,@ys) insert#1(nil(),@x) -> ::(@x,nil()) insert#2(#false(),@x,@y,@ys) -> ::(@y,insert(@x,@ys)) insert#2(#true(),@x,@y,@ys) -> ::(@x,::(@y,@ys)) isortlist(@l) -> isortlist#1(@l) isortlist#1(::(@x,@xs)) -> insert(@x,isortlist(@xs)) isortlist#1(nil()) -> nil() leq(@l1,@l2) -> leq#1(@l1,@l2) leq#1(::(@x,@xs),@l2) -> leq#2(@l2,@x,@xs) leq#1(nil(),@l2) -> #true() leq#2(::(@y,@ys),@x,@xs) -> or(#less(@x,@y),and(#equal(@x,@y),leq(@xs,@ys))) leq#2(nil(),@x,@xs) -> #false() or(@x,@y) -> #or(@x,@y) - Signature: {#and/2,#cklt/1,#compare/2,#eq/2,#equal/2,#less/2,#or/2,and/2,insert/2,insert#1/2,insert#2/4,isortlist/1 ,isortlist#1/1,leq/2,leq#1/2,leq#2/3,or/2,#and#/2,#cklt#/1,#compare#/2,#eq#/2,#equal#/2,#less#/2,#or#/2 ,and#/2,insert#/2,insert#1#/2,insert#2#/4,isortlist#/1,isortlist#1#/1,leq#/2,leq#1#/2,leq#2#/3 ,or#/2} / {#0/0,#EQ/0,#GT/0,#LT/0,#false/0,#neg/1,#pos/1,#s/1,#true/0,::/2,nil/0,c_1/1,c_2/2,c_3/1,c_4/1 ,c_5/1,c_6/0,c_7/1,c_8/0,c_9/1,c_10/2,c_11/0,c_12/1,c_13/1,c_14/0,c_15/1,c_16/0,c_17/1,c_18/0,c_19/0,c_20/0 ,c_21/0,c_22/0,c_23/0,c_24/0,c_25/0,c_26/0,c_27/0,c_28/0,c_29/0,c_30/1,c_31/0,c_32/0,c_33/0,c_34/1,c_35/0 ,c_36/1,c_37/0,c_38/0,c_39/0,c_40/0,c_41/0,c_42/1,c_43/0,c_44/0,c_45/0,c_46/1,c_47/0,c_48/1,c_49/3,c_50/0 ,c_51/0,c_52/0,c_53/0,c_54/0,c_55/0,c_56/0} - Obligation: innermost runtime complexity wrt. defined symbols {#and#,#cklt#,#compare#,#eq#,#equal#,#less#,#or#,and# ,insert#,insert#1#,insert#2#,isortlist#,isortlist#1#,leq#,leq#1#,leq#2#,or#} and constructors {#0,#EQ,#GT ,#LT,#false,#neg,#pos,#s,#true,::,nil} + Applied Processor: PredecessorEstimationCP {onSelectionCP = any intersect of rules of CDG leaf and strict-rules, withComplexityPair = NaturalMI {miDimension = 3, miDegree = 2, miKind = Algebraic, uargs = UArgs, urules = URules, selector = Nothing}} + Details: We first use the processor NaturalMI {miDimension = 3, miDegree = 2, miKind = Algebraic, uargs = UArgs, urules = URules, selector = Nothing} to orient following rules strictly: 1: insert#(@x,@l) -> c_4(insert#1#(@l,@x)) Consider the set of all dependency pairs 1: insert#(@x,@l) -> c_4(insert#1#(@l,@x)) 2: insert#1#(::(@y,@ys),@x) -> c_5(insert#2#(leq(@x,@y),@x,@y,@ys)) 3: insert#2#(#false(),@x,@y,@ys) -> c_7(insert#(@x,@ys)) 4: isortlist#(@l) -> c_9(isortlist#1#(@l)) 5: isortlist#1#(::(@x,@xs)) -> c_10(insert#(@x,isortlist(@xs)),isortlist#(@xs)) Processor NaturalMI {miDimension = 3, miDegree = 2, miKind = Algebraic, uargs = UArgs, urules = URules, selector = Nothing}induces the complexity certificateTIME (?,O(n^2)) SPACE(?,?)on application of the dependency pairs {1} These cover all (indirect) predecessors of dependency pairs {1,2,3} their number of applications is equally bounded. The dependency pairs are shifted into the weak component. ***** Step 5.a:1.b:3.b:1.a:1: NaturalMI WORST_CASE(?,O(n^2)) + Considered Problem: - Strict DPs: insert#(@x,@l) -> c_4(insert#1#(@l,@x)) - Weak DPs: insert#1#(::(@y,@ys),@x) -> c_5(insert#2#(leq(@x,@y),@x,@y,@ys)) insert#2#(#false(),@x,@y,@ys) -> c_7(insert#(@x,@ys)) isortlist#(@l) -> c_9(isortlist#1#(@l)) isortlist#1#(::(@x,@xs)) -> c_10(insert#(@x,isortlist(@xs)),isortlist#(@xs)) - Weak TRS: #and(#false(),#false()) -> #false() #and(#false(),#true()) -> #false() #and(#true(),#false()) -> #false() #and(#true(),#true()) -> #true() #cklt(#EQ()) -> #false() #cklt(#GT()) -> #false() #cklt(#LT()) -> #true() #compare(#0(),#0()) -> #EQ() #compare(#0(),#neg(@y)) -> #GT() #compare(#0(),#pos(@y)) -> #LT() #compare(#0(),#s(@y)) -> #LT() #compare(#neg(@x),#0()) -> #LT() #compare(#neg(@x),#neg(@y)) -> #compare(@y,@x) #compare(#neg(@x),#pos(@y)) -> #LT() #compare(#pos(@x),#0()) -> #GT() #compare(#pos(@x),#neg(@y)) -> #GT() #compare(#pos(@x),#pos(@y)) -> #compare(@x,@y) #compare(#s(@x),#0()) -> #GT() #compare(#s(@x),#s(@y)) -> #compare(@x,@y) #eq(#0(),#0()) -> #true() #eq(#0(),#neg(@y)) -> #false() #eq(#0(),#pos(@y)) -> #false() #eq(#0(),#s(@y)) -> #false() #eq(#neg(@x),#0()) -> #false() #eq(#neg(@x),#neg(@y)) -> #eq(@x,@y) #eq(#neg(@x),#pos(@y)) -> #false() #eq(#pos(@x),#0()) -> #false() #eq(#pos(@x),#neg(@y)) -> #false() #eq(#pos(@x),#pos(@y)) -> #eq(@x,@y) #eq(#s(@x),#0()) -> #false() #eq(#s(@x),#s(@y)) -> #eq(@x,@y) #eq(::(@x_1,@x_2),::(@y_1,@y_2)) -> #and(#eq(@x_1,@y_1),#eq(@x_2,@y_2)) #eq(::(@x_1,@x_2),nil()) -> #false() #eq(nil(),::(@y_1,@y_2)) -> #false() #eq(nil(),nil()) -> #true() #equal(@x,@y) -> #eq(@x,@y) #less(@x,@y) -> #cklt(#compare(@x,@y)) #or(#false(),#false()) -> #false() #or(#false(),#true()) -> #true() #or(#true(),#false()) -> #true() #or(#true(),#true()) -> #true() and(@x,@y) -> #and(@x,@y) insert(@x,@l) -> insert#1(@l,@x) insert#1(::(@y,@ys),@x) -> insert#2(leq(@x,@y),@x,@y,@ys) insert#1(nil(),@x) -> ::(@x,nil()) insert#2(#false(),@x,@y,@ys) -> ::(@y,insert(@x,@ys)) insert#2(#true(),@x,@y,@ys) -> ::(@x,::(@y,@ys)) isortlist(@l) -> isortlist#1(@l) isortlist#1(::(@x,@xs)) -> insert(@x,isortlist(@xs)) isortlist#1(nil()) -> nil() leq(@l1,@l2) -> leq#1(@l1,@l2) leq#1(::(@x,@xs),@l2) -> leq#2(@l2,@x,@xs) leq#1(nil(),@l2) -> #true() leq#2(::(@y,@ys),@x,@xs) -> or(#less(@x,@y),and(#equal(@x,@y),leq(@xs,@ys))) leq#2(nil(),@x,@xs) -> #false() or(@x,@y) -> #or(@x,@y) - Signature: {#and/2,#cklt/1,#compare/2,#eq/2,#equal/2,#less/2,#or/2,and/2,insert/2,insert#1/2,insert#2/4,isortlist/1 ,isortlist#1/1,leq/2,leq#1/2,leq#2/3,or/2,#and#/2,#cklt#/1,#compare#/2,#eq#/2,#equal#/2,#less#/2,#or#/2 ,and#/2,insert#/2,insert#1#/2,insert#2#/4,isortlist#/1,isortlist#1#/1,leq#/2,leq#1#/2,leq#2#/3 ,or#/2} / {#0/0,#EQ/0,#GT/0,#LT/0,#false/0,#neg/1,#pos/1,#s/1,#true/0,::/2,nil/0,c_1/1,c_2/2,c_3/1,c_4/1 ,c_5/1,c_6/0,c_7/1,c_8/0,c_9/1,c_10/2,c_11/0,c_12/1,c_13/1,c_14/0,c_15/1,c_16/0,c_17/1,c_18/0,c_19/0,c_20/0 ,c_21/0,c_22/0,c_23/0,c_24/0,c_25/0,c_26/0,c_27/0,c_28/0,c_29/0,c_30/1,c_31/0,c_32/0,c_33/0,c_34/1,c_35/0 ,c_36/1,c_37/0,c_38/0,c_39/0,c_40/0,c_41/0,c_42/1,c_43/0,c_44/0,c_45/0,c_46/1,c_47/0,c_48/1,c_49/3,c_50/0 ,c_51/0,c_52/0,c_53/0,c_54/0,c_55/0,c_56/0} - Obligation: innermost runtime complexity wrt. defined symbols {#and#,#cklt#,#compare#,#eq#,#equal#,#less#,#or#,and# ,insert#,insert#1#,insert#2#,isortlist#,isortlist#1#,leq#,leq#1#,leq#2#,or#} and constructors {#0,#EQ,#GT ,#LT,#false,#neg,#pos,#s,#true,::,nil} + Applied Processor: NaturalMI {miDimension = 3, miDegree = 2, miKind = Algebraic, uargs = UArgs, urules = URules, selector = Just first alternative for predecessorEstimation on any intersect of rules of CDG leaf and strict-rules} + Details: We apply a matrix interpretation of kind constructor based matrix interpretation (containing no more than 2 non-zero interpretation-entries in the diagonal of the component-wise maxima): The following argument positions are considered usable: uargs(c_4) = {1}, uargs(c_5) = {1}, uargs(c_7) = {1}, uargs(c_9) = {1}, uargs(c_10) = {1,2} Following symbols are considered usable: {#or,insert,insert#1,insert#2,isortlist,isortlist#1,leq,leq#1,leq#2,or,#and#,#cklt#,#compare#,#eq#,#equal# ,#less#,#or#,and#,insert#,insert#1#,insert#2#,isortlist#,isortlist#1#,leq#,leq#1#,leq#2#,or#} TcT has computed the following interpretation: p(#0) = [0] [0] [1] p(#EQ) = [1] [0] [0] p(#GT) = [0] [0] [0] p(#LT) = [1] [0] [0] p(#and) = [0 0 0] [0] [0 0 0] x2 + [0] [0 1 0] [1] p(#cklt) = [0 0 0] [0] [0 0 0] x1 + [1] [1 0 0] [1] p(#compare) = [1 0 0] [0 0 1] [0] [0 0 1] x1 + [0 0 1] x2 + [0] [0 0 0] [0 0 1] [1] p(#eq) = [0 0 0] [0 0 0] [0] [1 1 1] x1 + [0 0 0] x2 + [1] [0 0 0] [0 1 0] [0] p(#equal) = [0] [0] [0] p(#false) = [1] [1] [1] p(#less) = [0] [0] [0] p(#neg) = [0 1 0] [0] [0 0 1] x1 + [1] [0 0 0] [0] p(#or) = [1] [1] [1] p(#pos) = [0 0 0] [1] [0 0 1] x1 + [1] [0 0 0] [0] p(#s) = [0 0 0] [1] [0 0 1] x1 + [1] [0 0 0] [0] p(#true) = [1] [0] [1] p(::) = [1 0 1] [1 1 0] [0] [0 0 0] x1 + [0 0 1] x2 + [1] [0 0 0] [0 0 1] [1] p(and) = [1 1 0] [0] [0 1 0] x2 + [0] [0 0 0] [0] p(insert) = [1 0 1] [1 1 0] [1] [0 0 0] x1 + [0 0 1] x2 + [1] [0 0 0] [0 0 1] [1] p(insert#1) = [1 1 0] [1 0 1] [1] [0 0 1] x1 + [0 0 0] x2 + [1] [0 0 1] [0 0 0] [1] p(insert#2) = [1 0 1] [1 0 1] [1 0 1] [1 1 1] [0] [1 0 0] x1 + [0 0 0] x2 + [0 0 0] x3 + [0 0 1] x4 + [1] [0 0 1] [0 0 0] [0 0 0] [0 0 1] [1] p(isortlist) = [1 0 1] [0] [0 1 0] x1 + [0] [0 0 1] [0] p(isortlist#1) = [1 0 1] [0] [0 1 0] x1 + [0] [0 0 1] [0] p(leq) = [0 0 0] [0 0 0] [1] [1 1 0] x1 + [1 0 0] x2 + [0] [0 0 0] [0 0 0] [1] p(leq#1) = [0 0 0] [0 0 0] [1] [0 1 0] x1 + [1 0 0] x2 + [0] [0 0 0] [0 0 0] [1] p(leq#2) = [1] [1] [1] p(nil) = [0] [0] [0] p(or) = [1] [1] [1] p(#and#) = [0] [0] [0] p(#cklt#) = [0] [0] [0] p(#compare#) = [0] [0] [0] p(#eq#) = [0] [0] [0] p(#equal#) = [0] [0] [0] p(#less#) = [0] [0] [0] p(#or#) = [0] [0] [0] p(and#) = [0] [0] [0] p(insert#) = [1 0 0] [0 0 1] [1] [0 0 0] x1 + [0 1 0] x2 + [0] [0 0 1] [0 0 0] [0] p(insert#1#) = [0 0 1] [1 0 0] [0] [0 1 0] x1 + [1 0 0] x2 + [1] [0 0 0] [1 0 0] [0] p(insert#2#) = [0 0 0] [1 0 0] [0 0 0] [0 0 1] [1] [0 1 0] x1 + [1 0 0] x2 + [1 0 1] x3 + [0 0 1] x4 + [1] [0 0 0] [0 0 0] [0 0 0] [0 0 0] [1] p(isortlist#) = [1 1 0] [0] [1 0 0] x1 + [1] [1 0 0] [1] p(isortlist#1#) = [1 1 0] [0] [1 0 0] x1 + [1] [1 1 1] [0] p(leq#) = [0] [0] [0] p(leq#1#) = [0] [0] [0] p(leq#2#) = [0] [0] [0] p(or#) = [0] [0] [0] p(c_1) = [0] [0] [0] p(c_2) = [0] [0] [0] p(c_3) = [0] [0] [0] p(c_4) = [1 0 0] [0] [0 0 0] x1 + [0] [0 0 0] [0] p(c_5) = [1 0 0] [0] [1 0 1] x1 + [0] [0 0 0] [0] p(c_6) = [0] [0] [0] p(c_7) = [1 0 0] [0] [1 0 0] x1 + [0] [0 0 0] [0] p(c_8) = [0] [0] [0] p(c_9) = [1 0 0] [0] [0 0 0] x1 + [1] [0 0 0] [1] p(c_10) = [1 0 1] [1 0 0] [0] [0 1 0] x1 + [0 1 0] x2 + [0] [0 1 1] [0 0 0] [0] p(c_11) = [0] [0] [0] p(c_12) = [0] [0] [0] p(c_13) = [0] [0] [0] p(c_14) = [0] [0] [0] p(c_15) = [0] [0] [0] p(c_16) = [0] [0] [0] p(c_17) = [0] [0] [0] p(c_18) = [0] [0] [0] p(c_19) = [0] [0] [0] p(c_20) = [0] [0] [0] p(c_21) = [0] [0] [0] p(c_22) = [0] [0] [0] p(c_23) = [0] [0] [0] p(c_24) = [0] [0] [0] p(c_25) = [0] [0] [0] p(c_26) = [0] [0] [0] p(c_27) = [0] [0] [0] p(c_28) = [0] [0] [0] p(c_29) = [0] [0] [0] p(c_30) = [0] [0] [0] p(c_31) = [0] [0] [0] p(c_32) = [0] [0] [0] p(c_33) = [0] [0] [0] p(c_34) = [0] [0] [0] p(c_35) = [0] [0] [0] p(c_36) = [0] [0] [0] p(c_37) = [0] [0] [0] p(c_38) = [0] [0] [0] p(c_39) = [0] [0] [0] p(c_40) = [0] [0] [0] p(c_41) = [0] [0] [0] p(c_42) = [0] [0] [0] p(c_43) = [0] [0] [0] p(c_44) = [0] [0] [0] p(c_45) = [0] [0] [0] p(c_46) = [0] [0] [0] p(c_47) = [0] [0] [0] p(c_48) = [0] [0] [0] p(c_49) = [0] [0] [0] p(c_50) = [0] [0] [0] p(c_51) = [0] [0] [0] p(c_52) = [0] [0] [0] p(c_53) = [0] [0] [0] p(c_54) = [0] [0] [0] p(c_55) = [0] [0] [0] p(c_56) = [0] [0] [0] Following rules are strictly oriented: insert#(@x,@l) = [0 0 1] [1 0 0] [1] [0 1 0] @l + [0 0 0] @x + [0] [0 0 0] [0 0 1] [0] > [0 0 1] [1 0 0] [0] [0 0 0] @l + [0 0 0] @x + [0] [0 0 0] [0 0 0] [0] = c_4(insert#1#(@l,@x)) Following rules are (at-least) weakly oriented: insert#1#(::(@y,@ys),@x) = [1 0 0] [0 0 1] [1] [1 0 0] @x + [0 0 1] @ys + [2] [1 0 0] [0 0 0] [0] >= [1 0 0] [0 0 1] [1] [1 0 0] @x + [0 0 1] @ys + [2] [0 0 0] [0 0 0] [0] = c_5(insert#2#(leq(@x,@y),@x,@y,@ys)) insert#2#(#false(),@x,@y,@ys) = [1 0 0] [0 0 0] [0 0 1] [1] [1 0 0] @x + [1 0 1] @y + [0 0 1] @ys + [2] [0 0 0] [0 0 0] [0 0 0] [1] >= [1 0 0] [0 0 1] [1] [1 0 0] @x + [0 0 1] @ys + [1] [0 0 0] [0 0 0] [0] = c_7(insert#(@x,@ys)) isortlist#(@l) = [1 1 0] [0] [1 0 0] @l + [1] [1 0 0] [1] >= [1 1 0] [0] [0 0 0] @l + [1] [0 0 0] [1] = c_9(isortlist#1#(@l)) isortlist#1#(::(@x,@xs)) = [1 0 1] [1 1 1] [1] [1 0 1] @x + [1 1 0] @xs + [1] [1 0 1] [1 1 2] [2] >= [1 0 1] [1 1 1] [1] [0 0 0] @x + [1 1 0] @xs + [1] [0 0 1] [0 1 0] [0] = c_10(insert#(@x,isortlist(@xs)),isortlist#(@xs)) #or(#false(),#false()) = [1] [1] [1] >= [1] [1] [1] = #false() #or(#false(),#true()) = [1] [1] [1] >= [1] [0] [1] = #true() #or(#true(),#false()) = [1] [1] [1] >= [1] [0] [1] = #true() #or(#true(),#true()) = [1] [1] [1] >= [1] [0] [1] = #true() insert(@x,@l) = [1 1 0] [1 0 1] [1] [0 0 1] @l + [0 0 0] @x + [1] [0 0 1] [0 0 0] [1] >= [1 1 0] [1 0 1] [1] [0 0 1] @l + [0 0 0] @x + [1] [0 0 1] [0 0 0] [1] = insert#1(@l,@x) insert#1(::(@y,@ys),@x) = [1 0 1] [1 0 1] [1 1 1] [2] [0 0 0] @x + [0 0 0] @y + [0 0 1] @ys + [2] [0 0 0] [0 0 0] [0 0 1] [2] >= [1 0 1] [1 0 1] [1 1 1] [2] [0 0 0] @x + [0 0 0] @y + [0 0 1] @ys + [2] [0 0 0] [0 0 0] [0 0 1] [2] = insert#2(leq(@x,@y),@x,@y,@ys) insert#1(nil(),@x) = [1 0 1] [1] [0 0 0] @x + [1] [0 0 0] [1] >= [1 0 1] [0] [0 0 0] @x + [1] [0 0 0] [1] = ::(@x,nil()) insert#2(#false(),@x,@y,@ys) = [1 0 1] [1 0 1] [1 1 1] [2] [0 0 0] @x + [0 0 0] @y + [0 0 1] @ys + [2] [0 0 0] [0 0 0] [0 0 1] [2] >= [1 0 1] [1 0 1] [1 1 1] [2] [0 0 0] @x + [0 0 0] @y + [0 0 1] @ys + [2] [0 0 0] [0 0 0] [0 0 1] [2] = ::(@y,insert(@x,@ys)) insert#2(#true(),@x,@y,@ys) = [1 0 1] [1 0 1] [1 1 1] [2] [0 0 0] @x + [0 0 0] @y + [0 0 1] @ys + [2] [0 0 0] [0 0 0] [0 0 1] [2] >= [1 0 1] [1 0 1] [1 1 1] [1] [0 0 0] @x + [0 0 0] @y + [0 0 1] @ys + [2] [0 0 0] [0 0 0] [0 0 1] [2] = ::(@x,::(@y,@ys)) isortlist(@l) = [1 0 1] [0] [0 1 0] @l + [0] [0 0 1] [0] >= [1 0 1] [0] [0 1 0] @l + [0] [0 0 1] [0] = isortlist#1(@l) isortlist#1(::(@x,@xs)) = [1 0 1] [1 1 1] [1] [0 0 0] @x + [0 0 1] @xs + [1] [0 0 0] [0 0 1] [1] >= [1 0 1] [1 1 1] [1] [0 0 0] @x + [0 0 1] @xs + [1] [0 0 0] [0 0 1] [1] = insert(@x,isortlist(@xs)) isortlist#1(nil()) = [0] [0] [0] >= [0] [0] [0] = nil() leq(@l1,@l2) = [0 0 0] [0 0 0] [1] [1 1 0] @l1 + [1 0 0] @l2 + [0] [0 0 0] [0 0 0] [1] >= [0 0 0] [0 0 0] [1] [0 1 0] @l1 + [1 0 0] @l2 + [0] [0 0 0] [0 0 0] [1] = leq#1(@l1,@l2) leq#1(::(@x,@xs),@l2) = [0 0 0] [0 0 0] [1] [1 0 0] @l2 + [0 0 1] @xs + [1] [0 0 0] [0 0 0] [1] >= [1] [1] [1] = leq#2(@l2,@x,@xs) leq#1(nil(),@l2) = [0 0 0] [1] [1 0 0] @l2 + [0] [0 0 0] [1] >= [1] [0] [1] = #true() leq#2(::(@y,@ys),@x,@xs) = [1] [1] [1] >= [1] [1] [1] = or(#less(@x,@y),and(#equal(@x,@y),leq(@xs,@ys))) leq#2(nil(),@x,@xs) = [1] [1] [1] >= [1] [1] [1] = #false() or(@x,@y) = [1] [1] [1] >= [1] [1] [1] = #or(@x,@y) ***** Step 5.a:1.b:3.b:1.a:2: Assumption WORST_CASE(?,O(1)) + Considered Problem: - Weak DPs: insert#(@x,@l) -> c_4(insert#1#(@l,@x)) insert#1#(::(@y,@ys),@x) -> c_5(insert#2#(leq(@x,@y),@x,@y,@ys)) insert#2#(#false(),@x,@y,@ys) -> c_7(insert#(@x,@ys)) isortlist#(@l) -> c_9(isortlist#1#(@l)) isortlist#1#(::(@x,@xs)) -> c_10(insert#(@x,isortlist(@xs)),isortlist#(@xs)) - Weak TRS: #and(#false(),#false()) -> #false() #and(#false(),#true()) -> #false() #and(#true(),#false()) -> #false() #and(#true(),#true()) -> #true() #cklt(#EQ()) -> #false() #cklt(#GT()) -> #false() #cklt(#LT()) -> #true() #compare(#0(),#0()) -> #EQ() #compare(#0(),#neg(@y)) -> #GT() #compare(#0(),#pos(@y)) -> #LT() #compare(#0(),#s(@y)) -> #LT() #compare(#neg(@x),#0()) -> #LT() #compare(#neg(@x),#neg(@y)) -> #compare(@y,@x) #compare(#neg(@x),#pos(@y)) -> #LT() #compare(#pos(@x),#0()) -> #GT() #compare(#pos(@x),#neg(@y)) -> #GT() #compare(#pos(@x),#pos(@y)) -> #compare(@x,@y) #compare(#s(@x),#0()) -> #GT() #compare(#s(@x),#s(@y)) -> #compare(@x,@y) #eq(#0(),#0()) -> #true() #eq(#0(),#neg(@y)) -> #false() #eq(#0(),#pos(@y)) -> #false() #eq(#0(),#s(@y)) -> #false() #eq(#neg(@x),#0()) -> #false() #eq(#neg(@x),#neg(@y)) -> #eq(@x,@y) #eq(#neg(@x),#pos(@y)) -> #false() #eq(#pos(@x),#0()) -> #false() #eq(#pos(@x),#neg(@y)) -> #false() #eq(#pos(@x),#pos(@y)) -> #eq(@x,@y) #eq(#s(@x),#0()) -> #false() #eq(#s(@x),#s(@y)) -> #eq(@x,@y) #eq(::(@x_1,@x_2),::(@y_1,@y_2)) -> #and(#eq(@x_1,@y_1),#eq(@x_2,@y_2)) #eq(::(@x_1,@x_2),nil()) -> #false() #eq(nil(),::(@y_1,@y_2)) -> #false() #eq(nil(),nil()) -> #true() #equal(@x,@y) -> #eq(@x,@y) #less(@x,@y) -> #cklt(#compare(@x,@y)) #or(#false(),#false()) -> #false() #or(#false(),#true()) -> #true() #or(#true(),#false()) -> #true() #or(#true(),#true()) -> #true() and(@x,@y) -> #and(@x,@y) insert(@x,@l) -> insert#1(@l,@x) insert#1(::(@y,@ys),@x) -> insert#2(leq(@x,@y),@x,@y,@ys) insert#1(nil(),@x) -> ::(@x,nil()) insert#2(#false(),@x,@y,@ys) -> ::(@y,insert(@x,@ys)) insert#2(#true(),@x,@y,@ys) -> ::(@x,::(@y,@ys)) isortlist(@l) -> isortlist#1(@l) isortlist#1(::(@x,@xs)) -> insert(@x,isortlist(@xs)) isortlist#1(nil()) -> nil() leq(@l1,@l2) -> leq#1(@l1,@l2) leq#1(::(@x,@xs),@l2) -> leq#2(@l2,@x,@xs) leq#1(nil(),@l2) -> #true() leq#2(::(@y,@ys),@x,@xs) -> or(#less(@x,@y),and(#equal(@x,@y),leq(@xs,@ys))) leq#2(nil(),@x,@xs) -> #false() or(@x,@y) -> #or(@x,@y) - Signature: {#and/2,#cklt/1,#compare/2,#eq/2,#equal/2,#less/2,#or/2,and/2,insert/2,insert#1/2,insert#2/4,isortlist/1 ,isortlist#1/1,leq/2,leq#1/2,leq#2/3,or/2,#and#/2,#cklt#/1,#compare#/2,#eq#/2,#equal#/2,#less#/2,#or#/2 ,and#/2,insert#/2,insert#1#/2,insert#2#/4,isortlist#/1,isortlist#1#/1,leq#/2,leq#1#/2,leq#2#/3 ,or#/2} / {#0/0,#EQ/0,#GT/0,#LT/0,#false/0,#neg/1,#pos/1,#s/1,#true/0,::/2,nil/0,c_1/1,c_2/2,c_3/1,c_4/1 ,c_5/1,c_6/0,c_7/1,c_8/0,c_9/1,c_10/2,c_11/0,c_12/1,c_13/1,c_14/0,c_15/1,c_16/0,c_17/1,c_18/0,c_19/0,c_20/0 ,c_21/0,c_22/0,c_23/0,c_24/0,c_25/0,c_26/0,c_27/0,c_28/0,c_29/0,c_30/1,c_31/0,c_32/0,c_33/0,c_34/1,c_35/0 ,c_36/1,c_37/0,c_38/0,c_39/0,c_40/0,c_41/0,c_42/1,c_43/0,c_44/0,c_45/0,c_46/1,c_47/0,c_48/1,c_49/3,c_50/0 ,c_51/0,c_52/0,c_53/0,c_54/0,c_55/0,c_56/0} - Obligation: innermost runtime complexity wrt. defined symbols {#and#,#cklt#,#compare#,#eq#,#equal#,#less#,#or#,and# ,insert#,insert#1#,insert#2#,isortlist#,isortlist#1#,leq#,leq#1#,leq#2#,or#} and constructors {#0,#EQ,#GT ,#LT,#false,#neg,#pos,#s,#true,::,nil} + Applied Processor: Assumption {assumed = Certificate {spaceUB = Unknown, spaceLB = Unknown, timeUB = Poly (Just 0), timeLB = Unknown}} + Details: () ***** Step 5.a:1.b:3.b:1.b:1: RemoveWeakSuffixes WORST_CASE(?,O(1)) + Considered Problem: - Weak DPs: insert#(@x,@l) -> c_4(insert#1#(@l,@x)) insert#1#(::(@y,@ys),@x) -> c_5(insert#2#(leq(@x,@y),@x,@y,@ys)) insert#2#(#false(),@x,@y,@ys) -> c_7(insert#(@x,@ys)) isortlist#(@l) -> c_9(isortlist#1#(@l)) isortlist#1#(::(@x,@xs)) -> c_10(insert#(@x,isortlist(@xs)),isortlist#(@xs)) - Weak TRS: #and(#false(),#false()) -> #false() #and(#false(),#true()) -> #false() #and(#true(),#false()) -> #false() #and(#true(),#true()) -> #true() #cklt(#EQ()) -> #false() #cklt(#GT()) -> #false() #cklt(#LT()) -> #true() #compare(#0(),#0()) -> #EQ() #compare(#0(),#neg(@y)) -> #GT() #compare(#0(),#pos(@y)) -> #LT() #compare(#0(),#s(@y)) -> #LT() #compare(#neg(@x),#0()) -> #LT() #compare(#neg(@x),#neg(@y)) -> #compare(@y,@x) #compare(#neg(@x),#pos(@y)) -> #LT() #compare(#pos(@x),#0()) -> #GT() #compare(#pos(@x),#neg(@y)) -> #GT() #compare(#pos(@x),#pos(@y)) -> #compare(@x,@y) #compare(#s(@x),#0()) -> #GT() #compare(#s(@x),#s(@y)) -> #compare(@x,@y) #eq(#0(),#0()) -> #true() #eq(#0(),#neg(@y)) -> #false() #eq(#0(),#pos(@y)) -> #false() #eq(#0(),#s(@y)) -> #false() #eq(#neg(@x),#0()) -> #false() #eq(#neg(@x),#neg(@y)) -> #eq(@x,@y) #eq(#neg(@x),#pos(@y)) -> #false() #eq(#pos(@x),#0()) -> #false() #eq(#pos(@x),#neg(@y)) -> #false() #eq(#pos(@x),#pos(@y)) -> #eq(@x,@y) #eq(#s(@x),#0()) -> #false() #eq(#s(@x),#s(@y)) -> #eq(@x,@y) #eq(::(@x_1,@x_2),::(@y_1,@y_2)) -> #and(#eq(@x_1,@y_1),#eq(@x_2,@y_2)) #eq(::(@x_1,@x_2),nil()) -> #false() #eq(nil(),::(@y_1,@y_2)) -> #false() #eq(nil(),nil()) -> #true() #equal(@x,@y) -> #eq(@x,@y) #less(@x,@y) -> #cklt(#compare(@x,@y)) #or(#false(),#false()) -> #false() #or(#false(),#true()) -> #true() #or(#true(),#false()) -> #true() #or(#true(),#true()) -> #true() and(@x,@y) -> #and(@x,@y) insert(@x,@l) -> insert#1(@l,@x) insert#1(::(@y,@ys),@x) -> insert#2(leq(@x,@y),@x,@y,@ys) insert#1(nil(),@x) -> ::(@x,nil()) insert#2(#false(),@x,@y,@ys) -> ::(@y,insert(@x,@ys)) insert#2(#true(),@x,@y,@ys) -> ::(@x,::(@y,@ys)) isortlist(@l) -> isortlist#1(@l) isortlist#1(::(@x,@xs)) -> insert(@x,isortlist(@xs)) isortlist#1(nil()) -> nil() leq(@l1,@l2) -> leq#1(@l1,@l2) leq#1(::(@x,@xs),@l2) -> leq#2(@l2,@x,@xs) leq#1(nil(),@l2) -> #true() leq#2(::(@y,@ys),@x,@xs) -> or(#less(@x,@y),and(#equal(@x,@y),leq(@xs,@ys))) leq#2(nil(),@x,@xs) -> #false() or(@x,@y) -> #or(@x,@y) - Signature: {#and/2,#cklt/1,#compare/2,#eq/2,#equal/2,#less/2,#or/2,and/2,insert/2,insert#1/2,insert#2/4,isortlist/1 ,isortlist#1/1,leq/2,leq#1/2,leq#2/3,or/2,#and#/2,#cklt#/1,#compare#/2,#eq#/2,#equal#/2,#less#/2,#or#/2 ,and#/2,insert#/2,insert#1#/2,insert#2#/4,isortlist#/1,isortlist#1#/1,leq#/2,leq#1#/2,leq#2#/3 ,or#/2} / {#0/0,#EQ/0,#GT/0,#LT/0,#false/0,#neg/1,#pos/1,#s/1,#true/0,::/2,nil/0,c_1/1,c_2/2,c_3/1,c_4/1 ,c_5/1,c_6/0,c_7/1,c_8/0,c_9/1,c_10/2,c_11/0,c_12/1,c_13/1,c_14/0,c_15/1,c_16/0,c_17/1,c_18/0,c_19/0,c_20/0 ,c_21/0,c_22/0,c_23/0,c_24/0,c_25/0,c_26/0,c_27/0,c_28/0,c_29/0,c_30/1,c_31/0,c_32/0,c_33/0,c_34/1,c_35/0 ,c_36/1,c_37/0,c_38/0,c_39/0,c_40/0,c_41/0,c_42/1,c_43/0,c_44/0,c_45/0,c_46/1,c_47/0,c_48/1,c_49/3,c_50/0 ,c_51/0,c_52/0,c_53/0,c_54/0,c_55/0,c_56/0} - Obligation: innermost runtime complexity wrt. defined symbols {#and#,#cklt#,#compare#,#eq#,#equal#,#less#,#or#,and# ,insert#,insert#1#,insert#2#,isortlist#,isortlist#1#,leq#,leq#1#,leq#2#,or#} and constructors {#0,#EQ,#GT ,#LT,#false,#neg,#pos,#s,#true,::,nil} + Applied Processor: RemoveWeakSuffixes + Details: Consider the dependency graph 1:W:insert#(@x,@l) -> c_4(insert#1#(@l,@x)) -->_1 insert#1#(::(@y,@ys),@x) -> c_5(insert#2#(leq(@x,@y),@x,@y,@ys)):2 2:W:insert#1#(::(@y,@ys),@x) -> c_5(insert#2#(leq(@x,@y),@x,@y,@ys)) -->_1 insert#2#(#false(),@x,@y,@ys) -> c_7(insert#(@x,@ys)):3 3:W:insert#2#(#false(),@x,@y,@ys) -> c_7(insert#(@x,@ys)) -->_1 insert#(@x,@l) -> c_4(insert#1#(@l,@x)):1 4:W:isortlist#(@l) -> c_9(isortlist#1#(@l)) -->_1 isortlist#1#(::(@x,@xs)) -> c_10(insert#(@x,isortlist(@xs)),isortlist#(@xs)):5 5:W:isortlist#1#(::(@x,@xs)) -> c_10(insert#(@x,isortlist(@xs)),isortlist#(@xs)) -->_2 isortlist#(@l) -> c_9(isortlist#1#(@l)):4 -->_1 insert#(@x,@l) -> c_4(insert#1#(@l,@x)):1 The following weak DPs constitute a sub-graph of the DG that is closed under successors. The DPs are removed. 4: isortlist#(@l) -> c_9(isortlist#1#(@l)) 5: isortlist#1#(::(@x,@xs)) -> c_10(insert#(@x,isortlist(@xs)),isortlist#(@xs)) 1: insert#(@x,@l) -> c_4(insert#1#(@l,@x)) 3: insert#2#(#false(),@x,@y,@ys) -> c_7(insert#(@x,@ys)) 2: insert#1#(::(@y,@ys),@x) -> c_5(insert#2#(leq(@x,@y),@x,@y,@ys)) ***** Step 5.a:1.b:3.b:1.b:2: EmptyProcessor WORST_CASE(?,O(1)) + Considered Problem: - Weak TRS: #and(#false(),#false()) -> #false() #and(#false(),#true()) -> #false() #and(#true(),#false()) -> #false() #and(#true(),#true()) -> #true() #cklt(#EQ()) -> #false() #cklt(#GT()) -> #false() #cklt(#LT()) -> #true() #compare(#0(),#0()) -> #EQ() #compare(#0(),#neg(@y)) -> #GT() #compare(#0(),#pos(@y)) -> #LT() #compare(#0(),#s(@y)) -> #LT() #compare(#neg(@x),#0()) -> #LT() #compare(#neg(@x),#neg(@y)) -> #compare(@y,@x) #compare(#neg(@x),#pos(@y)) -> #LT() #compare(#pos(@x),#0()) -> #GT() #compare(#pos(@x),#neg(@y)) -> #GT() #compare(#pos(@x),#pos(@y)) -> #compare(@x,@y) #compare(#s(@x),#0()) -> #GT() #compare(#s(@x),#s(@y)) -> #compare(@x,@y) #eq(#0(),#0()) -> #true() #eq(#0(),#neg(@y)) -> #false() #eq(#0(),#pos(@y)) -> #false() #eq(#0(),#s(@y)) -> #false() #eq(#neg(@x),#0()) -> #false() #eq(#neg(@x),#neg(@y)) -> #eq(@x,@y) #eq(#neg(@x),#pos(@y)) -> #false() #eq(#pos(@x),#0()) -> #false() #eq(#pos(@x),#neg(@y)) -> #false() #eq(#pos(@x),#pos(@y)) -> #eq(@x,@y) #eq(#s(@x),#0()) -> #false() #eq(#s(@x),#s(@y)) -> #eq(@x,@y) #eq(::(@x_1,@x_2),::(@y_1,@y_2)) -> #and(#eq(@x_1,@y_1),#eq(@x_2,@y_2)) #eq(::(@x_1,@x_2),nil()) -> #false() #eq(nil(),::(@y_1,@y_2)) -> #false() #eq(nil(),nil()) -> #true() #equal(@x,@y) -> #eq(@x,@y) #less(@x,@y) -> #cklt(#compare(@x,@y)) #or(#false(),#false()) -> #false() #or(#false(),#true()) -> #true() #or(#true(),#false()) -> #true() #or(#true(),#true()) -> #true() and(@x,@y) -> #and(@x,@y) insert(@x,@l) -> insert#1(@l,@x) insert#1(::(@y,@ys),@x) -> insert#2(leq(@x,@y),@x,@y,@ys) insert#1(nil(),@x) -> ::(@x,nil()) insert#2(#false(),@x,@y,@ys) -> ::(@y,insert(@x,@ys)) insert#2(#true(),@x,@y,@ys) -> ::(@x,::(@y,@ys)) isortlist(@l) -> isortlist#1(@l) isortlist#1(::(@x,@xs)) -> insert(@x,isortlist(@xs)) isortlist#1(nil()) -> nil() leq(@l1,@l2) -> leq#1(@l1,@l2) leq#1(::(@x,@xs),@l2) -> leq#2(@l2,@x,@xs) leq#1(nil(),@l2) -> #true() leq#2(::(@y,@ys),@x,@xs) -> or(#less(@x,@y),and(#equal(@x,@y),leq(@xs,@ys))) leq#2(nil(),@x,@xs) -> #false() or(@x,@y) -> #or(@x,@y) - Signature: {#and/2,#cklt/1,#compare/2,#eq/2,#equal/2,#less/2,#or/2,and/2,insert/2,insert#1/2,insert#2/4,isortlist/1 ,isortlist#1/1,leq/2,leq#1/2,leq#2/3,or/2,#and#/2,#cklt#/1,#compare#/2,#eq#/2,#equal#/2,#less#/2,#or#/2 ,and#/2,insert#/2,insert#1#/2,insert#2#/4,isortlist#/1,isortlist#1#/1,leq#/2,leq#1#/2,leq#2#/3 ,or#/2} / {#0/0,#EQ/0,#GT/0,#LT/0,#false/0,#neg/1,#pos/1,#s/1,#true/0,::/2,nil/0,c_1/1,c_2/2,c_3/1,c_4/1 ,c_5/1,c_6/0,c_7/1,c_8/0,c_9/1,c_10/2,c_11/0,c_12/1,c_13/1,c_14/0,c_15/1,c_16/0,c_17/1,c_18/0,c_19/0,c_20/0 ,c_21/0,c_22/0,c_23/0,c_24/0,c_25/0,c_26/0,c_27/0,c_28/0,c_29/0,c_30/1,c_31/0,c_32/0,c_33/0,c_34/1,c_35/0 ,c_36/1,c_37/0,c_38/0,c_39/0,c_40/0,c_41/0,c_42/1,c_43/0,c_44/0,c_45/0,c_46/1,c_47/0,c_48/1,c_49/3,c_50/0 ,c_51/0,c_52/0,c_53/0,c_54/0,c_55/0,c_56/0} - Obligation: innermost runtime complexity wrt. defined symbols {#and#,#cklt#,#compare#,#eq#,#equal#,#less#,#or#,and# ,insert#,insert#1#,insert#2#,isortlist#,isortlist#1#,leq#,leq#1#,leq#2#,or#} and constructors {#0,#EQ,#GT ,#LT,#false,#neg,#pos,#s,#true,::,nil} + Applied Processor: EmptyProcessor + Details: The problem is already closed. The intended complexity is O(1). ** Step 5.b:1: RemoveWeakSuffixes WORST_CASE(?,O(n^1)) + Considered Problem: - Strict DPs: isortlist#(@l) -> c_9(isortlist#1#(@l)) isortlist#1#(::(@x,@xs)) -> c_10(insert#(@x,isortlist(@xs)),isortlist#(@xs)) - Weak DPs: insert#(@x,@l) -> c_4(insert#1#(@l,@x)) insert#1#(::(@y,@ys),@x) -> c_5(insert#2#(leq(@x,@y),@x,@y,@ys),leq#(@x,@y)) insert#2#(#false(),@x,@y,@ys) -> c_7(insert#(@x,@ys)) leq#(@l1,@l2) -> c_12(leq#1#(@l1,@l2)) leq#1#(::(@x,@xs),@l2) -> c_13(leq#2#(@l2,@x,@xs)) leq#2#(::(@y,@ys),@x,@xs) -> c_15(leq#(@xs,@ys)) - Weak TRS: #and(#false(),#false()) -> #false() #and(#false(),#true()) -> #false() #and(#true(),#false()) -> #false() #and(#true(),#true()) -> #true() #cklt(#EQ()) -> #false() #cklt(#GT()) -> #false() #cklt(#LT()) -> #true() #compare(#0(),#0()) -> #EQ() #compare(#0(),#neg(@y)) -> #GT() #compare(#0(),#pos(@y)) -> #LT() #compare(#0(),#s(@y)) -> #LT() #compare(#neg(@x),#0()) -> #LT() #compare(#neg(@x),#neg(@y)) -> #compare(@y,@x) #compare(#neg(@x),#pos(@y)) -> #LT() #compare(#pos(@x),#0()) -> #GT() #compare(#pos(@x),#neg(@y)) -> #GT() #compare(#pos(@x),#pos(@y)) -> #compare(@x,@y) #compare(#s(@x),#0()) -> #GT() #compare(#s(@x),#s(@y)) -> #compare(@x,@y) #eq(#0(),#0()) -> #true() #eq(#0(),#neg(@y)) -> #false() #eq(#0(),#pos(@y)) -> #false() #eq(#0(),#s(@y)) -> #false() #eq(#neg(@x),#0()) -> #false() #eq(#neg(@x),#neg(@y)) -> #eq(@x,@y) #eq(#neg(@x),#pos(@y)) -> #false() #eq(#pos(@x),#0()) -> #false() #eq(#pos(@x),#neg(@y)) -> #false() #eq(#pos(@x),#pos(@y)) -> #eq(@x,@y) #eq(#s(@x),#0()) -> #false() #eq(#s(@x),#s(@y)) -> #eq(@x,@y) #eq(::(@x_1,@x_2),::(@y_1,@y_2)) -> #and(#eq(@x_1,@y_1),#eq(@x_2,@y_2)) #eq(::(@x_1,@x_2),nil()) -> #false() #eq(nil(),::(@y_1,@y_2)) -> #false() #eq(nil(),nil()) -> #true() #equal(@x,@y) -> #eq(@x,@y) #less(@x,@y) -> #cklt(#compare(@x,@y)) #or(#false(),#false()) -> #false() #or(#false(),#true()) -> #true() #or(#true(),#false()) -> #true() #or(#true(),#true()) -> #true() and(@x,@y) -> #and(@x,@y) insert(@x,@l) -> insert#1(@l,@x) insert#1(::(@y,@ys),@x) -> insert#2(leq(@x,@y),@x,@y,@ys) insert#1(nil(),@x) -> ::(@x,nil()) insert#2(#false(),@x,@y,@ys) -> ::(@y,insert(@x,@ys)) insert#2(#true(),@x,@y,@ys) -> ::(@x,::(@y,@ys)) isortlist(@l) -> isortlist#1(@l) isortlist#1(::(@x,@xs)) -> insert(@x,isortlist(@xs)) isortlist#1(nil()) -> nil() leq(@l1,@l2) -> leq#1(@l1,@l2) leq#1(::(@x,@xs),@l2) -> leq#2(@l2,@x,@xs) leq#1(nil(),@l2) -> #true() leq#2(::(@y,@ys),@x,@xs) -> or(#less(@x,@y),and(#equal(@x,@y),leq(@xs,@ys))) leq#2(nil(),@x,@xs) -> #false() or(@x,@y) -> #or(@x,@y) - Signature: {#and/2,#cklt/1,#compare/2,#eq/2,#equal/2,#less/2,#or/2,and/2,insert/2,insert#1/2,insert#2/4,isortlist/1 ,isortlist#1/1,leq/2,leq#1/2,leq#2/3,or/2,#and#/2,#cklt#/1,#compare#/2,#eq#/2,#equal#/2,#less#/2,#or#/2 ,and#/2,insert#/2,insert#1#/2,insert#2#/4,isortlist#/1,isortlist#1#/1,leq#/2,leq#1#/2,leq#2#/3 ,or#/2} / {#0/0,#EQ/0,#GT/0,#LT/0,#false/0,#neg/1,#pos/1,#s/1,#true/0,::/2,nil/0,c_1/1,c_2/2,c_3/1,c_4/1 ,c_5/2,c_6/0,c_7/1,c_8/0,c_9/1,c_10/2,c_11/0,c_12/1,c_13/1,c_14/0,c_15/1,c_16/0,c_17/1,c_18/0,c_19/0,c_20/0 ,c_21/0,c_22/0,c_23/0,c_24/0,c_25/0,c_26/0,c_27/0,c_28/0,c_29/0,c_30/1,c_31/0,c_32/0,c_33/0,c_34/1,c_35/0 ,c_36/1,c_37/0,c_38/0,c_39/0,c_40/0,c_41/0,c_42/1,c_43/0,c_44/0,c_45/0,c_46/1,c_47/0,c_48/1,c_49/3,c_50/0 ,c_51/0,c_52/0,c_53/0,c_54/0,c_55/0,c_56/0} - Obligation: innermost runtime complexity wrt. defined symbols {#and#,#cklt#,#compare#,#eq#,#equal#,#less#,#or#,and# ,insert#,insert#1#,insert#2#,isortlist#,isortlist#1#,leq#,leq#1#,leq#2#,or#} and constructors {#0,#EQ,#GT ,#LT,#false,#neg,#pos,#s,#true,::,nil} + Applied Processor: RemoveWeakSuffixes + Details: Consider the dependency graph 1:S:isortlist#(@l) -> c_9(isortlist#1#(@l)) -->_1 isortlist#1#(::(@x,@xs)) -> c_10(insert#(@x,isortlist(@xs)),isortlist#(@xs)):2 2:S:isortlist#1#(::(@x,@xs)) -> c_10(insert#(@x,isortlist(@xs)),isortlist#(@xs)) -->_1 insert#(@x,@l) -> c_4(insert#1#(@l,@x)):3 -->_2 isortlist#(@l) -> c_9(isortlist#1#(@l)):1 3:W:insert#(@x,@l) -> c_4(insert#1#(@l,@x)) -->_1 insert#1#(::(@y,@ys),@x) -> c_5(insert#2#(leq(@x,@y),@x,@y,@ys),leq#(@x,@y)):4 4:W:insert#1#(::(@y,@ys),@x) -> c_5(insert#2#(leq(@x,@y),@x,@y,@ys),leq#(@x,@y)) -->_2 leq#(@l1,@l2) -> c_12(leq#1#(@l1,@l2)):6 -->_1 insert#2#(#false(),@x,@y,@ys) -> c_7(insert#(@x,@ys)):5 5:W:insert#2#(#false(),@x,@y,@ys) -> c_7(insert#(@x,@ys)) -->_1 insert#(@x,@l) -> c_4(insert#1#(@l,@x)):3 6:W:leq#(@l1,@l2) -> c_12(leq#1#(@l1,@l2)) -->_1 leq#1#(::(@x,@xs),@l2) -> c_13(leq#2#(@l2,@x,@xs)):7 7:W:leq#1#(::(@x,@xs),@l2) -> c_13(leq#2#(@l2,@x,@xs)) -->_1 leq#2#(::(@y,@ys),@x,@xs) -> c_15(leq#(@xs,@ys)):8 8:W:leq#2#(::(@y,@ys),@x,@xs) -> c_15(leq#(@xs,@ys)) -->_1 leq#(@l1,@l2) -> c_12(leq#1#(@l1,@l2)):6 The following weak DPs constitute a sub-graph of the DG that is closed under successors. The DPs are removed. 3: insert#(@x,@l) -> c_4(insert#1#(@l,@x)) 5: insert#2#(#false(),@x,@y,@ys) -> c_7(insert#(@x,@ys)) 4: insert#1#(::(@y,@ys),@x) -> c_5(insert#2#(leq(@x,@y),@x,@y,@ys),leq#(@x,@y)) 6: leq#(@l1,@l2) -> c_12(leq#1#(@l1,@l2)) 8: leq#2#(::(@y,@ys),@x,@xs) -> c_15(leq#(@xs,@ys)) 7: leq#1#(::(@x,@xs),@l2) -> c_13(leq#2#(@l2,@x,@xs)) ** Step 5.b:2: SimplifyRHS WORST_CASE(?,O(n^1)) + Considered Problem: - Strict DPs: isortlist#(@l) -> c_9(isortlist#1#(@l)) isortlist#1#(::(@x,@xs)) -> c_10(insert#(@x,isortlist(@xs)),isortlist#(@xs)) - Weak TRS: #and(#false(),#false()) -> #false() #and(#false(),#true()) -> #false() #and(#true(),#false()) -> #false() #and(#true(),#true()) -> #true() #cklt(#EQ()) -> #false() #cklt(#GT()) -> #false() #cklt(#LT()) -> #true() #compare(#0(),#0()) -> #EQ() #compare(#0(),#neg(@y)) -> #GT() #compare(#0(),#pos(@y)) -> #LT() #compare(#0(),#s(@y)) -> #LT() #compare(#neg(@x),#0()) -> #LT() #compare(#neg(@x),#neg(@y)) -> #compare(@y,@x) #compare(#neg(@x),#pos(@y)) -> #LT() #compare(#pos(@x),#0()) -> #GT() #compare(#pos(@x),#neg(@y)) -> #GT() #compare(#pos(@x),#pos(@y)) -> #compare(@x,@y) #compare(#s(@x),#0()) -> #GT() #compare(#s(@x),#s(@y)) -> #compare(@x,@y) #eq(#0(),#0()) -> #true() #eq(#0(),#neg(@y)) -> #false() #eq(#0(),#pos(@y)) -> #false() #eq(#0(),#s(@y)) -> #false() #eq(#neg(@x),#0()) -> #false() #eq(#neg(@x),#neg(@y)) -> #eq(@x,@y) #eq(#neg(@x),#pos(@y)) -> #false() #eq(#pos(@x),#0()) -> #false() #eq(#pos(@x),#neg(@y)) -> #false() #eq(#pos(@x),#pos(@y)) -> #eq(@x,@y) #eq(#s(@x),#0()) -> #false() #eq(#s(@x),#s(@y)) -> #eq(@x,@y) #eq(::(@x_1,@x_2),::(@y_1,@y_2)) -> #and(#eq(@x_1,@y_1),#eq(@x_2,@y_2)) #eq(::(@x_1,@x_2),nil()) -> #false() #eq(nil(),::(@y_1,@y_2)) -> #false() #eq(nil(),nil()) -> #true() #equal(@x,@y) -> #eq(@x,@y) #less(@x,@y) -> #cklt(#compare(@x,@y)) #or(#false(),#false()) -> #false() #or(#false(),#true()) -> #true() #or(#true(),#false()) -> #true() #or(#true(),#true()) -> #true() and(@x,@y) -> #and(@x,@y) insert(@x,@l) -> insert#1(@l,@x) insert#1(::(@y,@ys),@x) -> insert#2(leq(@x,@y),@x,@y,@ys) insert#1(nil(),@x) -> ::(@x,nil()) insert#2(#false(),@x,@y,@ys) -> ::(@y,insert(@x,@ys)) insert#2(#true(),@x,@y,@ys) -> ::(@x,::(@y,@ys)) isortlist(@l) -> isortlist#1(@l) isortlist#1(::(@x,@xs)) -> insert(@x,isortlist(@xs)) isortlist#1(nil()) -> nil() leq(@l1,@l2) -> leq#1(@l1,@l2) leq#1(::(@x,@xs),@l2) -> leq#2(@l2,@x,@xs) leq#1(nil(),@l2) -> #true() leq#2(::(@y,@ys),@x,@xs) -> or(#less(@x,@y),and(#equal(@x,@y),leq(@xs,@ys))) leq#2(nil(),@x,@xs) -> #false() or(@x,@y) -> #or(@x,@y) - Signature: {#and/2,#cklt/1,#compare/2,#eq/2,#equal/2,#less/2,#or/2,and/2,insert/2,insert#1/2,insert#2/4,isortlist/1 ,isortlist#1/1,leq/2,leq#1/2,leq#2/3,or/2,#and#/2,#cklt#/1,#compare#/2,#eq#/2,#equal#/2,#less#/2,#or#/2 ,and#/2,insert#/2,insert#1#/2,insert#2#/4,isortlist#/1,isortlist#1#/1,leq#/2,leq#1#/2,leq#2#/3 ,or#/2} / {#0/0,#EQ/0,#GT/0,#LT/0,#false/0,#neg/1,#pos/1,#s/1,#true/0,::/2,nil/0,c_1/1,c_2/2,c_3/1,c_4/1 ,c_5/2,c_6/0,c_7/1,c_8/0,c_9/1,c_10/2,c_11/0,c_12/1,c_13/1,c_14/0,c_15/1,c_16/0,c_17/1,c_18/0,c_19/0,c_20/0 ,c_21/0,c_22/0,c_23/0,c_24/0,c_25/0,c_26/0,c_27/0,c_28/0,c_29/0,c_30/1,c_31/0,c_32/0,c_33/0,c_34/1,c_35/0 ,c_36/1,c_37/0,c_38/0,c_39/0,c_40/0,c_41/0,c_42/1,c_43/0,c_44/0,c_45/0,c_46/1,c_47/0,c_48/1,c_49/3,c_50/0 ,c_51/0,c_52/0,c_53/0,c_54/0,c_55/0,c_56/0} - Obligation: innermost runtime complexity wrt. defined symbols {#and#,#cklt#,#compare#,#eq#,#equal#,#less#,#or#,and# ,insert#,insert#1#,insert#2#,isortlist#,isortlist#1#,leq#,leq#1#,leq#2#,or#} and constructors {#0,#EQ,#GT ,#LT,#false,#neg,#pos,#s,#true,::,nil} + Applied Processor: SimplifyRHS + Details: Consider the dependency graph 1:S:isortlist#(@l) -> c_9(isortlist#1#(@l)) -->_1 isortlist#1#(::(@x,@xs)) -> c_10(insert#(@x,isortlist(@xs)),isortlist#(@xs)):2 2:S:isortlist#1#(::(@x,@xs)) -> c_10(insert#(@x,isortlist(@xs)),isortlist#(@xs)) -->_2 isortlist#(@l) -> c_9(isortlist#1#(@l)):1 Due to missing edges in the depndency graph, the right-hand sides of following rules could be simplified: isortlist#1#(::(@x,@xs)) -> c_10(isortlist#(@xs)) ** Step 5.b:3: UsableRules WORST_CASE(?,O(n^1)) + Considered Problem: - Strict DPs: isortlist#(@l) -> c_9(isortlist#1#(@l)) isortlist#1#(::(@x,@xs)) -> c_10(isortlist#(@xs)) - Weak TRS: #and(#false(),#false()) -> #false() #and(#false(),#true()) -> #false() #and(#true(),#false()) -> #false() #and(#true(),#true()) -> #true() #cklt(#EQ()) -> #false() #cklt(#GT()) -> #false() #cklt(#LT()) -> #true() #compare(#0(),#0()) -> #EQ() #compare(#0(),#neg(@y)) -> #GT() #compare(#0(),#pos(@y)) -> #LT() #compare(#0(),#s(@y)) -> #LT() #compare(#neg(@x),#0()) -> #LT() #compare(#neg(@x),#neg(@y)) -> #compare(@y,@x) #compare(#neg(@x),#pos(@y)) -> #LT() #compare(#pos(@x),#0()) -> #GT() #compare(#pos(@x),#neg(@y)) -> #GT() #compare(#pos(@x),#pos(@y)) -> #compare(@x,@y) #compare(#s(@x),#0()) -> #GT() #compare(#s(@x),#s(@y)) -> #compare(@x,@y) #eq(#0(),#0()) -> #true() #eq(#0(),#neg(@y)) -> #false() #eq(#0(),#pos(@y)) -> #false() #eq(#0(),#s(@y)) -> #false() #eq(#neg(@x),#0()) -> #false() #eq(#neg(@x),#neg(@y)) -> #eq(@x,@y) #eq(#neg(@x),#pos(@y)) -> #false() #eq(#pos(@x),#0()) -> #false() #eq(#pos(@x),#neg(@y)) -> #false() #eq(#pos(@x),#pos(@y)) -> #eq(@x,@y) #eq(#s(@x),#0()) -> #false() #eq(#s(@x),#s(@y)) -> #eq(@x,@y) #eq(::(@x_1,@x_2),::(@y_1,@y_2)) -> #and(#eq(@x_1,@y_1),#eq(@x_2,@y_2)) #eq(::(@x_1,@x_2),nil()) -> #false() #eq(nil(),::(@y_1,@y_2)) -> #false() #eq(nil(),nil()) -> #true() #equal(@x,@y) -> #eq(@x,@y) #less(@x,@y) -> #cklt(#compare(@x,@y)) #or(#false(),#false()) -> #false() #or(#false(),#true()) -> #true() #or(#true(),#false()) -> #true() #or(#true(),#true()) -> #true() and(@x,@y) -> #and(@x,@y) insert(@x,@l) -> insert#1(@l,@x) insert#1(::(@y,@ys),@x) -> insert#2(leq(@x,@y),@x,@y,@ys) insert#1(nil(),@x) -> ::(@x,nil()) insert#2(#false(),@x,@y,@ys) -> ::(@y,insert(@x,@ys)) insert#2(#true(),@x,@y,@ys) -> ::(@x,::(@y,@ys)) isortlist(@l) -> isortlist#1(@l) isortlist#1(::(@x,@xs)) -> insert(@x,isortlist(@xs)) isortlist#1(nil()) -> nil() leq(@l1,@l2) -> leq#1(@l1,@l2) leq#1(::(@x,@xs),@l2) -> leq#2(@l2,@x,@xs) leq#1(nil(),@l2) -> #true() leq#2(::(@y,@ys),@x,@xs) -> or(#less(@x,@y),and(#equal(@x,@y),leq(@xs,@ys))) leq#2(nil(),@x,@xs) -> #false() or(@x,@y) -> #or(@x,@y) - Signature: {#and/2,#cklt/1,#compare/2,#eq/2,#equal/2,#less/2,#or/2,and/2,insert/2,insert#1/2,insert#2/4,isortlist/1 ,isortlist#1/1,leq/2,leq#1/2,leq#2/3,or/2,#and#/2,#cklt#/1,#compare#/2,#eq#/2,#equal#/2,#less#/2,#or#/2 ,and#/2,insert#/2,insert#1#/2,insert#2#/4,isortlist#/1,isortlist#1#/1,leq#/2,leq#1#/2,leq#2#/3 ,or#/2} / {#0/0,#EQ/0,#GT/0,#LT/0,#false/0,#neg/1,#pos/1,#s/1,#true/0,::/2,nil/0,c_1/1,c_2/2,c_3/1,c_4/1 ,c_5/2,c_6/0,c_7/1,c_8/0,c_9/1,c_10/1,c_11/0,c_12/1,c_13/1,c_14/0,c_15/1,c_16/0,c_17/1,c_18/0,c_19/0,c_20/0 ,c_21/0,c_22/0,c_23/0,c_24/0,c_25/0,c_26/0,c_27/0,c_28/0,c_29/0,c_30/1,c_31/0,c_32/0,c_33/0,c_34/1,c_35/0 ,c_36/1,c_37/0,c_38/0,c_39/0,c_40/0,c_41/0,c_42/1,c_43/0,c_44/0,c_45/0,c_46/1,c_47/0,c_48/1,c_49/3,c_50/0 ,c_51/0,c_52/0,c_53/0,c_54/0,c_55/0,c_56/0} - Obligation: innermost runtime complexity wrt. defined symbols {#and#,#cklt#,#compare#,#eq#,#equal#,#less#,#or#,and# ,insert#,insert#1#,insert#2#,isortlist#,isortlist#1#,leq#,leq#1#,leq#2#,or#} and constructors {#0,#EQ,#GT ,#LT,#false,#neg,#pos,#s,#true,::,nil} + Applied Processor: UsableRules + Details: We replace rewrite rules by usable rules: isortlist#(@l) -> c_9(isortlist#1#(@l)) isortlist#1#(::(@x,@xs)) -> c_10(isortlist#(@xs)) ** Step 5.b:4: PredecessorEstimationCP WORST_CASE(?,O(n^1)) + Considered Problem: - Strict DPs: isortlist#(@l) -> c_9(isortlist#1#(@l)) isortlist#1#(::(@x,@xs)) -> c_10(isortlist#(@xs)) - Signature: {#and/2,#cklt/1,#compare/2,#eq/2,#equal/2,#less/2,#or/2,and/2,insert/2,insert#1/2,insert#2/4,isortlist/1 ,isortlist#1/1,leq/2,leq#1/2,leq#2/3,or/2,#and#/2,#cklt#/1,#compare#/2,#eq#/2,#equal#/2,#less#/2,#or#/2 ,and#/2,insert#/2,insert#1#/2,insert#2#/4,isortlist#/1,isortlist#1#/1,leq#/2,leq#1#/2,leq#2#/3 ,or#/2} / {#0/0,#EQ/0,#GT/0,#LT/0,#false/0,#neg/1,#pos/1,#s/1,#true/0,::/2,nil/0,c_1/1,c_2/2,c_3/1,c_4/1 ,c_5/2,c_6/0,c_7/1,c_8/0,c_9/1,c_10/1,c_11/0,c_12/1,c_13/1,c_14/0,c_15/1,c_16/0,c_17/1,c_18/0,c_19/0,c_20/0 ,c_21/0,c_22/0,c_23/0,c_24/0,c_25/0,c_26/0,c_27/0,c_28/0,c_29/0,c_30/1,c_31/0,c_32/0,c_33/0,c_34/1,c_35/0 ,c_36/1,c_37/0,c_38/0,c_39/0,c_40/0,c_41/0,c_42/1,c_43/0,c_44/0,c_45/0,c_46/1,c_47/0,c_48/1,c_49/3,c_50/0 ,c_51/0,c_52/0,c_53/0,c_54/0,c_55/0,c_56/0} - Obligation: innermost runtime complexity wrt. defined symbols {#and#,#cklt#,#compare#,#eq#,#equal#,#less#,#or#,and# ,insert#,insert#1#,insert#2#,isortlist#,isortlist#1#,leq#,leq#1#,leq#2#,or#} and constructors {#0,#EQ,#GT ,#LT,#false,#neg,#pos,#s,#true,::,nil} + Applied Processor: PredecessorEstimationCP {onSelectionCP = any intersect of rules of CDG leaf and strict-rules, withComplexityPair = NaturalMI {miDimension = 1, miDegree = 1, miKind = Algebraic, uargs = UArgs, urules = URules, selector = Nothing}} + Details: We first use the processor NaturalMI {miDimension = 1, miDegree = 1, miKind = Algebraic, uargs = UArgs, urules = URules, selector = Nothing} to orient following rules strictly: 1: isortlist#(@l) -> c_9(isortlist#1#(@l)) 2: isortlist#1#(::(@x,@xs)) -> c_10(isortlist#(@xs)) The strictly oriented rules are moved into the weak component. *** Step 5.b:4.a:1: NaturalMI WORST_CASE(?,O(n^1)) + Considered Problem: - Strict DPs: isortlist#(@l) -> c_9(isortlist#1#(@l)) isortlist#1#(::(@x,@xs)) -> c_10(isortlist#(@xs)) - Signature: {#and/2,#cklt/1,#compare/2,#eq/2,#equal/2,#less/2,#or/2,and/2,insert/2,insert#1/2,insert#2/4,isortlist/1 ,isortlist#1/1,leq/2,leq#1/2,leq#2/3,or/2,#and#/2,#cklt#/1,#compare#/2,#eq#/2,#equal#/2,#less#/2,#or#/2 ,and#/2,insert#/2,insert#1#/2,insert#2#/4,isortlist#/1,isortlist#1#/1,leq#/2,leq#1#/2,leq#2#/3 ,or#/2} / {#0/0,#EQ/0,#GT/0,#LT/0,#false/0,#neg/1,#pos/1,#s/1,#true/0,::/2,nil/0,c_1/1,c_2/2,c_3/1,c_4/1 ,c_5/2,c_6/0,c_7/1,c_8/0,c_9/1,c_10/1,c_11/0,c_12/1,c_13/1,c_14/0,c_15/1,c_16/0,c_17/1,c_18/0,c_19/0,c_20/0 ,c_21/0,c_22/0,c_23/0,c_24/0,c_25/0,c_26/0,c_27/0,c_28/0,c_29/0,c_30/1,c_31/0,c_32/0,c_33/0,c_34/1,c_35/0 ,c_36/1,c_37/0,c_38/0,c_39/0,c_40/0,c_41/0,c_42/1,c_43/0,c_44/0,c_45/0,c_46/1,c_47/0,c_48/1,c_49/3,c_50/0 ,c_51/0,c_52/0,c_53/0,c_54/0,c_55/0,c_56/0} - Obligation: innermost runtime complexity wrt. defined symbols {#and#,#cklt#,#compare#,#eq#,#equal#,#less#,#or#,and# ,insert#,insert#1#,insert#2#,isortlist#,isortlist#1#,leq#,leq#1#,leq#2#,or#} and constructors {#0,#EQ,#GT ,#LT,#false,#neg,#pos,#s,#true,::,nil} + Applied Processor: NaturalMI {miDimension = 1, miDegree = 1, miKind = Algebraic, uargs = UArgs, urules = URules, selector = Just first alternative for predecessorEstimation on any intersect of rules of CDG leaf and strict-rules} + Details: We apply a matrix interpretation of kind constructor based matrix interpretation: The following argument positions are considered usable: uargs(c_9) = {1}, uargs(c_10) = {1} Following symbols are considered usable: {#and#,#cklt#,#compare#,#eq#,#equal#,#less#,#or#,and#,insert#,insert#1#,insert#2#,isortlist#,isortlist#1# ,leq#,leq#1#,leq#2#,or#} TcT has computed the following interpretation: p(#0) = [0] p(#EQ) = [0] p(#GT) = [0] p(#LT) = [0] p(#and) = [0] p(#cklt) = [0] p(#compare) = [0] p(#eq) = [1] x1 + [1] x2 + [0] p(#equal) = [2] p(#false) = [0] p(#less) = [0] p(#neg) = [0] p(#or) = [0] p(#pos) = [1] p(#s) = [4] p(#true) = [2] p(::) = [1] x2 + [2] p(and) = [1] x1 + [8] x2 + [4] p(insert) = [8] x1 + [1] p(insert#1) = [8] x1 + [0] p(insert#2) = [2] x4 + [1] p(isortlist) = [8] x1 + [1] p(isortlist#1) = [2] x1 + [2] p(leq) = [1] x1 + [2] x2 + [1] p(leq#1) = [1] p(leq#2) = [0] p(nil) = [0] p(or) = [0] p(#and#) = [0] p(#cklt#) = [0] p(#compare#) = [0] p(#eq#) = [0] p(#equal#) = [0] p(#less#) = [0] p(#or#) = [0] p(and#) = [0] p(insert#) = [0] p(insert#1#) = [0] p(insert#2#) = [0] p(isortlist#) = [4] x1 + [3] p(isortlist#1#) = [4] x1 + [0] p(leq#) = [0] p(leq#1#) = [0] p(leq#2#) = [0] p(or#) = [0] p(c_1) = [0] p(c_2) = [0] p(c_3) = [1] x1 + [4] p(c_4) = [2] x1 + [0] p(c_5) = [8] x1 + [1] x2 + [1] p(c_6) = [1] p(c_7) = [2] p(c_8) = [4] p(c_9) = [1] x1 + [2] p(c_10) = [1] x1 + [0] p(c_11) = [4] p(c_12) = [1] x1 + [0] p(c_13) = [0] p(c_14) = [0] p(c_15) = [2] x1 + [0] p(c_16) = [1] p(c_17) = [1] p(c_18) = [2] p(c_19) = [1] p(c_20) = [1] p(c_21) = [8] p(c_22) = [2] p(c_23) = [0] p(c_24) = [0] p(c_25) = [2] p(c_26) = [0] p(c_27) = [1] p(c_28) = [1] p(c_29) = [1] p(c_30) = [2] p(c_31) = [1] p(c_32) = [1] p(c_33) = [1] p(c_34) = [2] p(c_35) = [0] p(c_36) = [1] x1 + [0] p(c_37) = [1] p(c_38) = [4] p(c_39) = [2] p(c_40) = [1] p(c_41) = [0] p(c_42) = [0] p(c_43) = [1] p(c_44) = [4] p(c_45) = [1] p(c_46) = [1] p(c_47) = [2] p(c_48) = [2] x1 + [1] p(c_49) = [1] x2 + [1] x3 + [1] p(c_50) = [1] p(c_51) = [1] p(c_52) = [0] p(c_53) = [0] p(c_54) = [0] p(c_55) = [0] p(c_56) = [0] Following rules are strictly oriented: isortlist#(@l) = [4] @l + [3] > [4] @l + [2] = c_9(isortlist#1#(@l)) isortlist#1#(::(@x,@xs)) = [4] @xs + [8] > [4] @xs + [3] = c_10(isortlist#(@xs)) Following rules are (at-least) weakly oriented: *** Step 5.b:4.a:2: Assumption WORST_CASE(?,O(1)) + Considered Problem: - Weak DPs: isortlist#(@l) -> c_9(isortlist#1#(@l)) isortlist#1#(::(@x,@xs)) -> c_10(isortlist#(@xs)) - Signature: {#and/2,#cklt/1,#compare/2,#eq/2,#equal/2,#less/2,#or/2,and/2,insert/2,insert#1/2,insert#2/4,isortlist/1 ,isortlist#1/1,leq/2,leq#1/2,leq#2/3,or/2,#and#/2,#cklt#/1,#compare#/2,#eq#/2,#equal#/2,#less#/2,#or#/2 ,and#/2,insert#/2,insert#1#/2,insert#2#/4,isortlist#/1,isortlist#1#/1,leq#/2,leq#1#/2,leq#2#/3 ,or#/2} / {#0/0,#EQ/0,#GT/0,#LT/0,#false/0,#neg/1,#pos/1,#s/1,#true/0,::/2,nil/0,c_1/1,c_2/2,c_3/1,c_4/1 ,c_5/2,c_6/0,c_7/1,c_8/0,c_9/1,c_10/1,c_11/0,c_12/1,c_13/1,c_14/0,c_15/1,c_16/0,c_17/1,c_18/0,c_19/0,c_20/0 ,c_21/0,c_22/0,c_23/0,c_24/0,c_25/0,c_26/0,c_27/0,c_28/0,c_29/0,c_30/1,c_31/0,c_32/0,c_33/0,c_34/1,c_35/0 ,c_36/1,c_37/0,c_38/0,c_39/0,c_40/0,c_41/0,c_42/1,c_43/0,c_44/0,c_45/0,c_46/1,c_47/0,c_48/1,c_49/3,c_50/0 ,c_51/0,c_52/0,c_53/0,c_54/0,c_55/0,c_56/0} - Obligation: innermost runtime complexity wrt. defined symbols {#and#,#cklt#,#compare#,#eq#,#equal#,#less#,#or#,and# ,insert#,insert#1#,insert#2#,isortlist#,isortlist#1#,leq#,leq#1#,leq#2#,or#} and constructors {#0,#EQ,#GT ,#LT,#false,#neg,#pos,#s,#true,::,nil} + Applied Processor: Assumption {assumed = Certificate {spaceUB = Unknown, spaceLB = Unknown, timeUB = Poly (Just 0), timeLB = Unknown}} + Details: () *** Step 5.b:4.b:1: RemoveWeakSuffixes WORST_CASE(?,O(1)) + Considered Problem: - Weak DPs: isortlist#(@l) -> c_9(isortlist#1#(@l)) isortlist#1#(::(@x,@xs)) -> c_10(isortlist#(@xs)) - Signature: {#and/2,#cklt/1,#compare/2,#eq/2,#equal/2,#less/2,#or/2,and/2,insert/2,insert#1/2,insert#2/4,isortlist/1 ,isortlist#1/1,leq/2,leq#1/2,leq#2/3,or/2,#and#/2,#cklt#/1,#compare#/2,#eq#/2,#equal#/2,#less#/2,#or#/2 ,and#/2,insert#/2,insert#1#/2,insert#2#/4,isortlist#/1,isortlist#1#/1,leq#/2,leq#1#/2,leq#2#/3 ,or#/2} / {#0/0,#EQ/0,#GT/0,#LT/0,#false/0,#neg/1,#pos/1,#s/1,#true/0,::/2,nil/0,c_1/1,c_2/2,c_3/1,c_4/1 ,c_5/2,c_6/0,c_7/1,c_8/0,c_9/1,c_10/1,c_11/0,c_12/1,c_13/1,c_14/0,c_15/1,c_16/0,c_17/1,c_18/0,c_19/0,c_20/0 ,c_21/0,c_22/0,c_23/0,c_24/0,c_25/0,c_26/0,c_27/0,c_28/0,c_29/0,c_30/1,c_31/0,c_32/0,c_33/0,c_34/1,c_35/0 ,c_36/1,c_37/0,c_38/0,c_39/0,c_40/0,c_41/0,c_42/1,c_43/0,c_44/0,c_45/0,c_46/1,c_47/0,c_48/1,c_49/3,c_50/0 ,c_51/0,c_52/0,c_53/0,c_54/0,c_55/0,c_56/0} - Obligation: innermost runtime complexity wrt. defined symbols {#and#,#cklt#,#compare#,#eq#,#equal#,#less#,#or#,and# ,insert#,insert#1#,insert#2#,isortlist#,isortlist#1#,leq#,leq#1#,leq#2#,or#} and constructors {#0,#EQ,#GT ,#LT,#false,#neg,#pos,#s,#true,::,nil} + Applied Processor: RemoveWeakSuffixes + Details: Consider the dependency graph 1:W:isortlist#(@l) -> c_9(isortlist#1#(@l)) -->_1 isortlist#1#(::(@x,@xs)) -> c_10(isortlist#(@xs)):2 2:W:isortlist#1#(::(@x,@xs)) -> c_10(isortlist#(@xs)) -->_1 isortlist#(@l) -> c_9(isortlist#1#(@l)):1 The following weak DPs constitute a sub-graph of the DG that is closed under successors. The DPs are removed. 1: isortlist#(@l) -> c_9(isortlist#1#(@l)) 2: isortlist#1#(::(@x,@xs)) -> c_10(isortlist#(@xs)) *** Step 5.b:4.b:2: EmptyProcessor WORST_CASE(?,O(1)) + Considered Problem: - Signature: {#and/2,#cklt/1,#compare/2,#eq/2,#equal/2,#less/2,#or/2,and/2,insert/2,insert#1/2,insert#2/4,isortlist/1 ,isortlist#1/1,leq/2,leq#1/2,leq#2/3,or/2,#and#/2,#cklt#/1,#compare#/2,#eq#/2,#equal#/2,#less#/2,#or#/2 ,and#/2,insert#/2,insert#1#/2,insert#2#/4,isortlist#/1,isortlist#1#/1,leq#/2,leq#1#/2,leq#2#/3 ,or#/2} / {#0/0,#EQ/0,#GT/0,#LT/0,#false/0,#neg/1,#pos/1,#s/1,#true/0,::/2,nil/0,c_1/1,c_2/2,c_3/1,c_4/1 ,c_5/2,c_6/0,c_7/1,c_8/0,c_9/1,c_10/1,c_11/0,c_12/1,c_13/1,c_14/0,c_15/1,c_16/0,c_17/1,c_18/0,c_19/0,c_20/0 ,c_21/0,c_22/0,c_23/0,c_24/0,c_25/0,c_26/0,c_27/0,c_28/0,c_29/0,c_30/1,c_31/0,c_32/0,c_33/0,c_34/1,c_35/0 ,c_36/1,c_37/0,c_38/0,c_39/0,c_40/0,c_41/0,c_42/1,c_43/0,c_44/0,c_45/0,c_46/1,c_47/0,c_48/1,c_49/3,c_50/0 ,c_51/0,c_52/0,c_53/0,c_54/0,c_55/0,c_56/0} - Obligation: innermost runtime complexity wrt. defined symbols {#and#,#cklt#,#compare#,#eq#,#equal#,#less#,#or#,and# ,insert#,insert#1#,insert#2#,isortlist#,isortlist#1#,leq#,leq#1#,leq#2#,or#} and constructors {#0,#EQ,#GT ,#LT,#false,#neg,#pos,#s,#true,::,nil} + Applied Processor: EmptyProcessor + Details: The problem is already closed. The intended complexity is O(1). WORST_CASE(?,O(n^2))