WORST_CASE(?,O(n^3)) * Step 1: DependencyPairs WORST_CASE(?,O(n^3)) + 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^3)) + 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^3)) + 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^3)) + 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: DecomposeDG WORST_CASE(?,O(n^3)) + 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: DecomposeDG {onSelection = all below first cut in WDG, onUpper = Nothing, onLower = Nothing} + Details: We decompose the input problem according to the dependency graph into the upper component isortlist#(@l) -> c_9(isortlist#1#(@l)) isortlist#1#(::(@x,@xs)) -> c_10(insert#(@x,isortlist(@xs)),isortlist#(@xs)) and a lower component 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)) Further, following extension rules are added to the lower component. isortlist#(@l) -> isortlist#1#(@l) isortlist#1#(::(@x,@xs)) -> insert#(@x,isortlist(@xs)) isortlist#1#(::(@x,@xs)) -> isortlist#(@xs) ** Step 5.a:1: 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.a:2: 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.a:3: WeightGap 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: WeightGap {wgDimension = 1, wgDegree = 1, wgKind = Algebraic, wgUArgs = UArgs, wgOn = WgOnAny} + Details: The weightgap principle applies using the following constant growth matrix-interpretation: 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: all 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) = [0] p(#equal) = [0] p(#false) = [0] p(#less) = [1] p(#neg) = [1] x1 + [0] p(#or) = [0] p(#pos) = [1] x1 + [0] p(#s) = [1] x1 + [0] p(#true) = [1] p(::) = [1] x1 + [0] p(and) = [0] p(insert) = [0] p(insert#1) = [0] p(insert#2) = [0] p(isortlist) = [0] p(isortlist#1) = [0] p(leq) = [0] p(leq#1) = [0] 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#) = [1] x1 + [1] p(#or#) = [0] p(and#) = [0] p(insert#) = [0] p(insert#1#) = [0] p(insert#2#) = [0] p(isortlist#) = [0] p(isortlist#1#) = [3] 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) = [0] p(c_4) = [0] p(c_5) = [0] p(c_6) = [0] p(c_7) = [0] p(c_8) = [0] p(c_9) = [1] x1 + [0] p(c_10) = [1] x1 + [0] p(c_11) = [0] p(c_12) = [0] p(c_13) = [0] p(c_14) = [0] p(c_15) = [0] 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) = [2] p(c_56) = [0] Following rules are strictly oriented: isortlist#1#(::(@x,@xs)) = [3] > [0] = c_10(isortlist#(@xs)) Following rules are (at-least) weakly oriented: isortlist#(@l) = [0] >= [3] = c_9(isortlist#1#(@l)) Further, it can be verified that all rules not oriented are covered by the weightgap condition. ** Step 5.a:4: WeightGap WORST_CASE(?,O(n^1)) + Considered Problem: - Strict DPs: isortlist#(@l) -> c_9(isortlist#1#(@l)) - Weak DPs: 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: WeightGap {wgDimension = 1, wgDegree = 1, wgKind = Algebraic, wgUArgs = UArgs, wgOn = WgOnAny} + Details: The weightgap principle applies using the following constant growth matrix-interpretation: 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: all 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) = [0] p(#equal) = [0] p(#false) = [0] p(#less) = [0] p(#neg) = [1] x1 + [0] p(#or) = [0] p(#pos) = [1] x1 + [0] p(#s) = [1] x1 + [0] p(#true) = [0] p(::) = [1] x1 + [1] x2 + [3] p(and) = [0] p(insert) = [0] p(insert#1) = [0] p(insert#2) = [0] p(isortlist) = [0] p(isortlist#1) = [0] p(leq) = [0] p(leq#1) = [0] 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#) = [2] x2 + [1] x3 + [1] x4 + [0] p(isortlist#) = [3] x1 + [9] p(isortlist#1#) = [3] 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) = [0] p(c_4) = [0] p(c_5) = [0] p(c_6) = [0] p(c_7) = [0] p(c_8) = [0] p(c_9) = [1] x1 + [0] p(c_10) = [1] x1 + [0] p(c_11) = [0] p(c_12) = [0] p(c_13) = [0] p(c_14) = [0] p(c_15) = [0] 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: isortlist#(@l) = [3] @l + [9] > [3] @l + [0] = c_9(isortlist#1#(@l)) Following rules are (at-least) weakly oriented: isortlist#1#(::(@x,@xs)) = [3] @x + [3] @xs + [9] >= [3] @xs + [9] = c_10(isortlist#(@xs)) Further, it can be verified that all rules not oriented are covered by the weightgap condition. ** Step 5.a:5: EmptyProcessor 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: EmptyProcessor + Details: The problem is already closed. The intended complexity is O(1). ** Step 5.b:1: DecomposeDG 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) -> isortlist#1#(@l) isortlist#1#(::(@x,@xs)) -> insert#(@x,isortlist(@xs)) isortlist#1#(::(@x,@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: DecomposeDG {onSelection = all below first cut in WDG, onUpper = Nothing, onLower = Nothing} + Details: We decompose the input problem according to the dependency graph into the upper component 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) -> isortlist#1#(@l) isortlist#1#(::(@x,@xs)) -> insert#(@x,isortlist(@xs)) isortlist#1#(::(@x,@xs)) -> isortlist#(@xs) and a lower component 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)) Further, following extension rules are added to the lower component. insert#(@x,@l) -> insert#1#(@l,@x) insert#1#(::(@y,@ys),@x) -> insert#2#(leq(@x,@y),@x,@y,@ys) insert#1#(::(@y,@ys),@x) -> leq#(@x,@y) insert#2#(#false(),@x,@y,@ys) -> insert#(@x,@ys) isortlist#(@l) -> isortlist#1#(@l) isortlist#1#(::(@x,@xs)) -> insert#(@x,isortlist(@xs)) isortlist#1#(::(@x,@xs)) -> isortlist#(@xs) *** Step 5.b:1.a:1: SimplifyRHS WORST_CASE(?,O(n^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)) - Weak DPs: isortlist#(@l) -> isortlist#1#(@l) isortlist#1#(::(@x,@xs)) -> insert#(@x,isortlist(@xs)) isortlist#1#(::(@x,@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) -> isortlist#1#(@l) -->_1 isortlist#1#(::(@x,@xs)) -> isortlist#(@xs):6 -->_1 isortlist#1#(::(@x,@xs)) -> insert#(@x,isortlist(@xs)):5 5:W:isortlist#1#(::(@x,@xs)) -> insert#(@x,isortlist(@xs)) -->_1 insert#(@x,@l) -> c_4(insert#1#(@l,@x)):1 6:W:isortlist#1#(::(@x,@xs)) -> isortlist#(@xs) -->_1 isortlist#(@l) -> isortlist#1#(@l):4 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.b:1.a:2: WeightGap WORST_CASE(?,O(n^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)) insert#2#(#false(),@x,@y,@ys) -> c_7(insert#(@x,@ys)) - Weak DPs: isortlist#(@l) -> isortlist#1#(@l) isortlist#1#(::(@x,@xs)) -> insert#(@x,isortlist(@xs)) isortlist#1#(::(@x,@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: WeightGap {wgDimension = 1, wgDegree = 1, wgKind = Algebraic, wgUArgs = UArgs, wgOn = WgOnAny} + Details: The weightgap principle applies using the following constant growth matrix-interpretation: We apply a matrix interpretation of kind constructor based matrix interpretation: The following argument positions are considered usable: uargs(#and) = {1,2}, uargs(#cklt) = {1}, uargs(::) = {2}, uargs(and) = {1,2}, uargs(insert) = {2}, uargs(insert#2) = {1}, uargs(or) = {1,2}, uargs(insert#) = {2}, uargs(insert#2#) = {1}, uargs(c_4) = {1}, uargs(c_5) = {1}, uargs(c_7) = {1} Following symbols are considered usable: all TcT has computed the following interpretation: p(#0) = [0] p(#EQ) = [0] p(#GT) = [0] p(#LT) = [0] p(#and) = [1] x1 + [1] x2 + [0] p(#cklt) = [1] x1 + [0] p(#compare) = [0] p(#eq) = [0] p(#equal) = [0] p(#false) = [0] p(#less) = [0] p(#neg) = [1] x1 + [0] p(#or) = [1] x1 + [0] p(#pos) = [0] p(#s) = [1] x1 + [0] p(#true) = [0] p(::) = [1] x2 + [0] p(and) = [1] x1 + [1] x2 + [0] p(insert) = [1] x2 + [0] p(insert#1) = [1] x1 + [0] p(insert#2) = [1] x1 + [1] x4 + [0] p(isortlist) = [0] p(isortlist#1) = [0] p(leq) = [0] p(leq#1) = [0] p(leq#2) = [0] p(nil) = [0] p(or) = [1] x1 + [1] x2 + [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#) = [1] x2 + [0] p(insert#1#) = [1] x1 + [0] p(insert#2#) = [1] x1 + [1] x4 + [1] p(isortlist#) = [2] x1 + [0] p(isortlist#1#) = [2] 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) = [1] x1 + [0] p(c_5) = [1] x1 + [2] p(c_6) = [4] p(c_7) = [1] x1 + [0] p(c_8) = [0] p(c_9) = [0] p(c_10) = [0] p(c_11) = [0] p(c_12) = [0] p(c_13) = [0] p(c_14) = [0] p(c_15) = [0] 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: insert#2#(#false(),@x,@y,@ys) = [1] @ys + [1] > [1] @ys + [0] = c_7(insert#(@x,@ys)) Following rules are (at-least) weakly oriented: insert#(@x,@l) = [1] @l + [0] >= [1] @l + [0] = c_4(insert#1#(@l,@x)) insert#1#(::(@y,@ys),@x) = [1] @ys + [0] >= [1] @ys + [3] = c_5(insert#2#(leq(@x,@y),@x,@y,@ys)) isortlist#(@l) = [2] @l + [0] >= [2] @l + [0] = isortlist#1#(@l) isortlist#1#(::(@x,@xs)) = [2] @xs + [0] >= [0] = insert#(@x,isortlist(@xs)) isortlist#1#(::(@x,@xs)) = [2] @xs + [0] >= [2] @xs + [0] = isortlist#(@xs) #and(#false(),#false()) = [0] >= [0] = #false() #and(#false(),#true()) = [0] >= [0] = #false() #and(#true(),#false()) = [0] >= [0] = #false() #and(#true(),#true()) = [0] >= [0] = #true() #cklt(#EQ()) = [0] >= [0] = #false() #cklt(#GT()) = [0] >= [0] = #false() #cklt(#LT()) = [0] >= [0] = #true() #compare(#0(),#0()) = [0] >= [0] = #EQ() #compare(#0(),#neg(@y)) = [0] >= [0] = #GT() #compare(#0(),#pos(@y)) = [0] >= [0] = #LT() #compare(#0(),#s(@y)) = [0] >= [0] = #LT() #compare(#neg(@x),#0()) = [0] >= [0] = #LT() #compare(#neg(@x),#neg(@y)) = [0] >= [0] = #compare(@y,@x) #compare(#neg(@x),#pos(@y)) = [0] >= [0] = #LT() #compare(#pos(@x),#0()) = [0] >= [0] = #GT() #compare(#pos(@x),#neg(@y)) = [0] >= [0] = #GT() #compare(#pos(@x),#pos(@y)) = [0] >= [0] = #compare(@x,@y) #compare(#s(@x),#0()) = [0] >= [0] = #GT() #compare(#s(@x),#s(@y)) = [0] >= [0] = #compare(@x,@y) #eq(#0(),#0()) = [0] >= [0] = #true() #eq(#0(),#neg(@y)) = [0] >= [0] = #false() #eq(#0(),#pos(@y)) = [0] >= [0] = #false() #eq(#0(),#s(@y)) = [0] >= [0] = #false() #eq(#neg(@x),#0()) = [0] >= [0] = #false() #eq(#neg(@x),#neg(@y)) = [0] >= [0] = #eq(@x,@y) #eq(#neg(@x),#pos(@y)) = [0] >= [0] = #false() #eq(#pos(@x),#0()) = [0] >= [0] = #false() #eq(#pos(@x),#neg(@y)) = [0] >= [0] = #false() #eq(#pos(@x),#pos(@y)) = [0] >= [0] = #eq(@x,@y) #eq(#s(@x),#0()) = [0] >= [0] = #false() #eq(#s(@x),#s(@y)) = [0] >= [0] = #eq(@x,@y) #eq(::(@x_1,@x_2),::(@y_1,@y_2)) = [0] >= [0] = #and(#eq(@x_1,@y_1),#eq(@x_2,@y_2)) #eq(::(@x_1,@x_2),nil()) = [0] >= [0] = #false() #eq(nil(),::(@y_1,@y_2)) = [0] >= [0] = #false() #eq(nil(),nil()) = [0] >= [0] = #true() #equal(@x,@y) = [0] >= [0] = #eq(@x,@y) #less(@x,@y) = [0] >= [0] = #cklt(#compare(@x,@y)) #or(#false(),#false()) = [0] >= [0] = #false() #or(#false(),#true()) = [0] >= [0] = #true() #or(#true(),#false()) = [0] >= [0] = #true() #or(#true(),#true()) = [0] >= [0] = #true() and(@x,@y) = [1] @x + [1] @y + [0] >= [1] @x + [1] @y + [0] = #and(@x,@y) insert(@x,@l) = [1] @l + [0] >= [1] @l + [0] = insert#1(@l,@x) insert#1(::(@y,@ys),@x) = [1] @ys + [0] >= [1] @ys + [0] = insert#2(leq(@x,@y),@x,@y,@ys) insert#1(nil(),@x) = [0] >= [0] = ::(@x,nil()) insert#2(#false(),@x,@y,@ys) = [1] @ys + [0] >= [1] @ys + [0] = ::(@y,insert(@x,@ys)) insert#2(#true(),@x,@y,@ys) = [1] @ys + [0] >= [1] @ys + [0] = ::(@x,::(@y,@ys)) isortlist(@l) = [0] >= [0] = isortlist#1(@l) isortlist#1(::(@x,@xs)) = [0] >= [0] = insert(@x,isortlist(@xs)) isortlist#1(nil()) = [0] >= [0] = nil() leq(@l1,@l2) = [0] >= [0] = leq#1(@l1,@l2) leq#1(::(@x,@xs),@l2) = [0] >= [0] = leq#2(@l2,@x,@xs) leq#1(nil(),@l2) = [0] >= [0] = #true() leq#2(::(@y,@ys),@x,@xs) = [0] >= [0] = or(#less(@x,@y),and(#equal(@x,@y),leq(@xs,@ys))) leq#2(nil(),@x,@xs) = [0] >= [0] = #false() or(@x,@y) = [1] @x + [1] @y + [0] >= [1] @x + [0] = #or(@x,@y) Further, it can be verified that all rules not oriented are covered by the weightgap condition. *** Step 5.b:1.a:3: WeightGap WORST_CASE(?,O(n^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)) - Weak DPs: insert#2#(#false(),@x,@y,@ys) -> c_7(insert#(@x,@ys)) isortlist#(@l) -> isortlist#1#(@l) isortlist#1#(::(@x,@xs)) -> insert#(@x,isortlist(@xs)) isortlist#1#(::(@x,@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: WeightGap {wgDimension = 1, wgDegree = 1, wgKind = Algebraic, wgUArgs = UArgs, wgOn = WgOnAny} + Details: The weightgap principle applies using the following constant growth matrix-interpretation: We apply a matrix interpretation of kind constructor based matrix interpretation: The following argument positions are considered usable: uargs(#and) = {1,2}, uargs(#cklt) = {1}, uargs(::) = {2}, uargs(and) = {1,2}, uargs(insert) = {2}, uargs(insert#2) = {1}, uargs(or) = {1,2}, uargs(insert#) = {2}, uargs(insert#2#) = {1}, uargs(c_4) = {1}, uargs(c_5) = {1}, uargs(c_7) = {1} Following symbols are considered usable: all TcT has computed the following interpretation: p(#0) = [0] p(#EQ) = [0] p(#GT) = [0] p(#LT) = [0] p(#and) = [1] x1 + [1] x2 + [0] p(#cklt) = [1] x1 + [0] p(#compare) = [0] p(#eq) = [0] p(#equal) = [0] p(#false) = [0] p(#less) = [0] p(#neg) = [0] p(#or) = [1] x2 + [0] p(#pos) = [1] x1 + [0] p(#s) = [1] x1 + [0] p(#true) = [0] p(::) = [1] x2 + [0] p(and) = [1] x1 + [1] x2 + [0] p(insert) = [1] x2 + [0] p(insert#1) = [1] x1 + [0] p(insert#2) = [1] x1 + [1] x4 + [0] p(isortlist) = [1] x1 + [0] p(isortlist#1) = [1] x1 + [0] p(leq) = [0] p(leq#1) = [0] p(leq#2) = [0] p(nil) = [2] p(or) = [1] x1 + [1] x2 + [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#) = [1] x2 + [0] p(insert#1#) = [1] x1 + [3] p(insert#2#) = [1] x1 + [1] x4 + [0] p(isortlist#) = [1] x1 + [0] p(isortlist#1#) = [1] 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) = [0] p(c_4) = [1] x1 + [0] p(c_5) = [1] x1 + [2] p(c_6) = [0] p(c_7) = [1] x1 + [0] p(c_8) = [0] p(c_9) = [0] p(c_10) = [0] p(c_11) = [0] p(c_12) = [0] p(c_13) = [0] p(c_14) = [0] p(c_15) = [0] 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: insert#1#(::(@y,@ys),@x) = [1] @ys + [3] > [1] @ys + [2] = c_5(insert#2#(leq(@x,@y),@x,@y,@ys)) Following rules are (at-least) weakly oriented: insert#(@x,@l) = [1] @l + [0] >= [1] @l + [3] = c_4(insert#1#(@l,@x)) insert#2#(#false(),@x,@y,@ys) = [1] @ys + [0] >= [1] @ys + [0] = c_7(insert#(@x,@ys)) isortlist#(@l) = [1] @l + [0] >= [1] @l + [0] = isortlist#1#(@l) isortlist#1#(::(@x,@xs)) = [1] @xs + [0] >= [1] @xs + [0] = insert#(@x,isortlist(@xs)) isortlist#1#(::(@x,@xs)) = [1] @xs + [0] >= [1] @xs + [0] = isortlist#(@xs) #and(#false(),#false()) = [0] >= [0] = #false() #and(#false(),#true()) = [0] >= [0] = #false() #and(#true(),#false()) = [0] >= [0] = #false() #and(#true(),#true()) = [0] >= [0] = #true() #cklt(#EQ()) = [0] >= [0] = #false() #cklt(#GT()) = [0] >= [0] = #false() #cklt(#LT()) = [0] >= [0] = #true() #compare(#0(),#0()) = [0] >= [0] = #EQ() #compare(#0(),#neg(@y)) = [0] >= [0] = #GT() #compare(#0(),#pos(@y)) = [0] >= [0] = #LT() #compare(#0(),#s(@y)) = [0] >= [0] = #LT() #compare(#neg(@x),#0()) = [0] >= [0] = #LT() #compare(#neg(@x),#neg(@y)) = [0] >= [0] = #compare(@y,@x) #compare(#neg(@x),#pos(@y)) = [0] >= [0] = #LT() #compare(#pos(@x),#0()) = [0] >= [0] = #GT() #compare(#pos(@x),#neg(@y)) = [0] >= [0] = #GT() #compare(#pos(@x),#pos(@y)) = [0] >= [0] = #compare(@x,@y) #compare(#s(@x),#0()) = [0] >= [0] = #GT() #compare(#s(@x),#s(@y)) = [0] >= [0] = #compare(@x,@y) #eq(#0(),#0()) = [0] >= [0] = #true() #eq(#0(),#neg(@y)) = [0] >= [0] = #false() #eq(#0(),#pos(@y)) = [0] >= [0] = #false() #eq(#0(),#s(@y)) = [0] >= [0] = #false() #eq(#neg(@x),#0()) = [0] >= [0] = #false() #eq(#neg(@x),#neg(@y)) = [0] >= [0] = #eq(@x,@y) #eq(#neg(@x),#pos(@y)) = [0] >= [0] = #false() #eq(#pos(@x),#0()) = [0] >= [0] = #false() #eq(#pos(@x),#neg(@y)) = [0] >= [0] = #false() #eq(#pos(@x),#pos(@y)) = [0] >= [0] = #eq(@x,@y) #eq(#s(@x),#0()) = [0] >= [0] = #false() #eq(#s(@x),#s(@y)) = [0] >= [0] = #eq(@x,@y) #eq(::(@x_1,@x_2),::(@y_1,@y_2)) = [0] >= [0] = #and(#eq(@x_1,@y_1),#eq(@x_2,@y_2)) #eq(::(@x_1,@x_2),nil()) = [0] >= [0] = #false() #eq(nil(),::(@y_1,@y_2)) = [0] >= [0] = #false() #eq(nil(),nil()) = [0] >= [0] = #true() #equal(@x,@y) = [0] >= [0] = #eq(@x,@y) #less(@x,@y) = [0] >= [0] = #cklt(#compare(@x,@y)) #or(#false(),#false()) = [0] >= [0] = #false() #or(#false(),#true()) = [0] >= [0] = #true() #or(#true(),#false()) = [0] >= [0] = #true() #or(#true(),#true()) = [0] >= [0] = #true() and(@x,@y) = [1] @x + [1] @y + [0] >= [1] @x + [1] @y + [0] = #and(@x,@y) insert(@x,@l) = [1] @l + [0] >= [1] @l + [0] = insert#1(@l,@x) insert#1(::(@y,@ys),@x) = [1] @ys + [0] >= [1] @ys + [0] = insert#2(leq(@x,@y),@x,@y,@ys) insert#1(nil(),@x) = [2] >= [2] = ::(@x,nil()) insert#2(#false(),@x,@y,@ys) = [1] @ys + [0] >= [1] @ys + [0] = ::(@y,insert(@x,@ys)) insert#2(#true(),@x,@y,@ys) = [1] @ys + [0] >= [1] @ys + [0] = ::(@x,::(@y,@ys)) isortlist(@l) = [1] @l + [0] >= [1] @l + [0] = isortlist#1(@l) isortlist#1(::(@x,@xs)) = [1] @xs + [0] >= [1] @xs + [0] = insert(@x,isortlist(@xs)) isortlist#1(nil()) = [2] >= [2] = nil() leq(@l1,@l2) = [0] >= [0] = leq#1(@l1,@l2) leq#1(::(@x,@xs),@l2) = [0] >= [0] = leq#2(@l2,@x,@xs) leq#1(nil(),@l2) = [0] >= [0] = #true() leq#2(::(@y,@ys),@x,@xs) = [0] >= [0] = or(#less(@x,@y),and(#equal(@x,@y),leq(@xs,@ys))) leq#2(nil(),@x,@xs) = [0] >= [0] = #false() or(@x,@y) = [1] @x + [1] @y + [0] >= [1] @y + [0] = #or(@x,@y) Further, it can be verified that all rules not oriented are covered by the weightgap condition. *** Step 5.b:1.a:4: WeightGap WORST_CASE(?,O(n^1)) + 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) -> isortlist#1#(@l) isortlist#1#(::(@x,@xs)) -> insert#(@x,isortlist(@xs)) isortlist#1#(::(@x,@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: WeightGap {wgDimension = 1, wgDegree = 1, wgKind = Algebraic, wgUArgs = UArgs, wgOn = WgOnAny} + Details: The weightgap principle applies using the following constant growth matrix-interpretation: We apply a matrix interpretation of kind constructor based matrix interpretation: The following argument positions are considered usable: uargs(#and) = {1,2}, uargs(#cklt) = {1}, uargs(::) = {2}, uargs(and) = {1,2}, uargs(insert) = {2}, uargs(insert#2) = {1}, uargs(or) = {1,2}, uargs(insert#) = {2}, uargs(insert#2#) = {1}, uargs(c_4) = {1}, uargs(c_5) = {1}, uargs(c_7) = {1} Following symbols are considered usable: all TcT has computed the following interpretation: p(#0) = [0] p(#EQ) = [0] p(#GT) = [0] p(#LT) = [0] p(#and) = [1] x1 + [1] x2 + [0] p(#cklt) = [1] x1 + [0] p(#compare) = [0] p(#eq) = [0] p(#equal) = [0] p(#false) = [0] p(#less) = [0] p(#neg) = [1] x1 + [0] p(#or) = [0] p(#pos) = [1] x1 + [0] p(#s) = [1] x1 + [0] p(#true) = [0] p(::) = [1] x2 + [1] p(and) = [1] x1 + [1] x2 + [0] p(insert) = [1] x2 + [1] p(insert#1) = [1] x1 + [1] p(insert#2) = [1] x1 + [1] x4 + [2] p(isortlist) = [2] x1 + [1] p(isortlist#1) = [2] x1 + [0] p(leq) = [0] p(leq#1) = [0] p(leq#2) = [0] p(nil) = [0] p(or) = [1] x1 + [1] x2 + [0] p(#and#) = [0] p(#cklt#) = [4] x1 + [1] p(#compare#) = [1] x1 + [0] p(#eq#) = [1] x1 + [4] x2 + [0] p(#equal#) = [1] p(#less#) = [1] x1 + [4] x2 + [0] p(#or#) = [1] x1 + [2] x2 + [0] p(and#) = [1] x1 + [1] x2 + [1] p(insert#) = [1] x2 + [3] p(insert#1#) = [1] x1 + [2] p(insert#2#) = [1] x1 + [1] x4 + [3] p(isortlist#) = [5] x1 + [3] p(isortlist#1#) = [5] x1 + [3] p(leq#) = [1] x1 + [0] p(leq#1#) = [4] x1 + [1] p(leq#2#) = [2] x1 + [1] x3 + [0] p(or#) = [1] x1 + [1] x2 + [0] p(c_1) = [1] p(c_2) = [4] p(c_3) = [1] x1 + [0] p(c_4) = [1] x1 + [0] p(c_5) = [1] x1 + [0] p(c_6) = [0] p(c_7) = [1] x1 + [0] p(c_8) = [0] p(c_9) = [1] p(c_10) = [1] x1 + [0] p(c_11) = [0] p(c_12) = [1] p(c_13) = [1] x1 + [1] p(c_14) = [0] p(c_15) = [0] p(c_16) = [1] p(c_17) = [1] x1 + [2] p(c_18) = [0] p(c_19) = [1] p(c_20) = [1] p(c_21) = [2] p(c_22) = [2] p(c_23) = [0] p(c_24) = [0] p(c_25) = [0] p(c_26) = [0] p(c_27) = [1] p(c_28) = [0] p(c_29) = [0] p(c_30) = [1] x1 + [1] p(c_31) = [1] p(c_32) = [0] p(c_33) = [0] p(c_34) = [1] p(c_35) = [0] p(c_36) = [1] x1 + [0] p(c_37) = [1] p(c_38) = [1] p(c_39) = [2] p(c_40) = [0] p(c_41) = [4] p(c_42) = [1] x1 + [1] p(c_43) = [2] p(c_44) = [1] p(c_45) = [1] p(c_46) = [4] x1 + [4] p(c_47) = [1] p(c_48) = [0] p(c_49) = [4] p(c_50) = [0] p(c_51) = [1] p(c_52) = [1] p(c_53) = [1] p(c_54) = [4] p(c_55) = [0] p(c_56) = [1] Following rules are strictly oriented: insert#(@x,@l) = [1] @l + [3] > [1] @l + [2] = c_4(insert#1#(@l,@x)) Following rules are (at-least) weakly oriented: insert#1#(::(@y,@ys),@x) = [1] @ys + [3] >= [1] @ys + [3] = c_5(insert#2#(leq(@x,@y),@x,@y,@ys)) insert#2#(#false(),@x,@y,@ys) = [1] @ys + [3] >= [1] @ys + [3] = c_7(insert#(@x,@ys)) isortlist#(@l) = [5] @l + [3] >= [5] @l + [3] = isortlist#1#(@l) isortlist#1#(::(@x,@xs)) = [5] @xs + [8] >= [2] @xs + [4] = insert#(@x,isortlist(@xs)) isortlist#1#(::(@x,@xs)) = [5] @xs + [8] >= [5] @xs + [3] = isortlist#(@xs) #and(#false(),#false()) = [0] >= [0] = #false() #and(#false(),#true()) = [0] >= [0] = #false() #and(#true(),#false()) = [0] >= [0] = #false() #and(#true(),#true()) = [0] >= [0] = #true() #cklt(#EQ()) = [0] >= [0] = #false() #cklt(#GT()) = [0] >= [0] = #false() #cklt(#LT()) = [0] >= [0] = #true() #compare(#0(),#0()) = [0] >= [0] = #EQ() #compare(#0(),#neg(@y)) = [0] >= [0] = #GT() #compare(#0(),#pos(@y)) = [0] >= [0] = #LT() #compare(#0(),#s(@y)) = [0] >= [0] = #LT() #compare(#neg(@x),#0()) = [0] >= [0] = #LT() #compare(#neg(@x),#neg(@y)) = [0] >= [0] = #compare(@y,@x) #compare(#neg(@x),#pos(@y)) = [0] >= [0] = #LT() #compare(#pos(@x),#0()) = [0] >= [0] = #GT() #compare(#pos(@x),#neg(@y)) = [0] >= [0] = #GT() #compare(#pos(@x),#pos(@y)) = [0] >= [0] = #compare(@x,@y) #compare(#s(@x),#0()) = [0] >= [0] = #GT() #compare(#s(@x),#s(@y)) = [0] >= [0] = #compare(@x,@y) #eq(#0(),#0()) = [0] >= [0] = #true() #eq(#0(),#neg(@y)) = [0] >= [0] = #false() #eq(#0(),#pos(@y)) = [0] >= [0] = #false() #eq(#0(),#s(@y)) = [0] >= [0] = #false() #eq(#neg(@x),#0()) = [0] >= [0] = #false() #eq(#neg(@x),#neg(@y)) = [0] >= [0] = #eq(@x,@y) #eq(#neg(@x),#pos(@y)) = [0] >= [0] = #false() #eq(#pos(@x),#0()) = [0] >= [0] = #false() #eq(#pos(@x),#neg(@y)) = [0] >= [0] = #false() #eq(#pos(@x),#pos(@y)) = [0] >= [0] = #eq(@x,@y) #eq(#s(@x),#0()) = [0] >= [0] = #false() #eq(#s(@x),#s(@y)) = [0] >= [0] = #eq(@x,@y) #eq(::(@x_1,@x_2),::(@y_1,@y_2)) = [0] >= [0] = #and(#eq(@x_1,@y_1),#eq(@x_2,@y_2)) #eq(::(@x_1,@x_2),nil()) = [0] >= [0] = #false() #eq(nil(),::(@y_1,@y_2)) = [0] >= [0] = #false() #eq(nil(),nil()) = [0] >= [0] = #true() #equal(@x,@y) = [0] >= [0] = #eq(@x,@y) #less(@x,@y) = [0] >= [0] = #cklt(#compare(@x,@y)) #or(#false(),#false()) = [0] >= [0] = #false() #or(#false(),#true()) = [0] >= [0] = #true() #or(#true(),#false()) = [0] >= [0] = #true() #or(#true(),#true()) = [0] >= [0] = #true() and(@x,@y) = [1] @x + [1] @y + [0] >= [1] @x + [1] @y + [0] = #and(@x,@y) insert(@x,@l) = [1] @l + [1] >= [1] @l + [1] = insert#1(@l,@x) insert#1(::(@y,@ys),@x) = [1] @ys + [2] >= [1] @ys + [2] = insert#2(leq(@x,@y),@x,@y,@ys) insert#1(nil(),@x) = [1] >= [1] = ::(@x,nil()) insert#2(#false(),@x,@y,@ys) = [1] @ys + [2] >= [1] @ys + [2] = ::(@y,insert(@x,@ys)) insert#2(#true(),@x,@y,@ys) = [1] @ys + [2] >= [1] @ys + [2] = ::(@x,::(@y,@ys)) isortlist(@l) = [2] @l + [1] >= [2] @l + [0] = isortlist#1(@l) isortlist#1(::(@x,@xs)) = [2] @xs + [2] >= [2] @xs + [2] = insert(@x,isortlist(@xs)) isortlist#1(nil()) = [0] >= [0] = nil() leq(@l1,@l2) = [0] >= [0] = leq#1(@l1,@l2) leq#1(::(@x,@xs),@l2) = [0] >= [0] = leq#2(@l2,@x,@xs) leq#1(nil(),@l2) = [0] >= [0] = #true() leq#2(::(@y,@ys),@x,@xs) = [0] >= [0] = or(#less(@x,@y),and(#equal(@x,@y),leq(@xs,@ys))) leq#2(nil(),@x,@xs) = [0] >= [0] = #false() or(@x,@y) = [1] @x + [1] @y + [0] >= [0] = #or(@x,@y) Further, it can be verified that all rules not oriented are covered by the weightgap condition. *** Step 5.b:1.a:5: EmptyProcessor 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) -> isortlist#1#(@l) isortlist#1#(::(@x,@xs)) -> insert#(@x,isortlist(@xs)) isortlist#1#(::(@x,@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: EmptyProcessor + Details: The problem is already closed. The intended complexity is O(1). *** Step 5.b:1.b:1: WeightGap WORST_CASE(?,O(n^1)) + Considered Problem: - Strict DPs: 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: insert#(@x,@l) -> insert#1#(@l,@x) insert#1#(::(@y,@ys),@x) -> insert#2#(leq(@x,@y),@x,@y,@ys) insert#1#(::(@y,@ys),@x) -> leq#(@x,@y) insert#2#(#false(),@x,@y,@ys) -> insert#(@x,@ys) isortlist#(@l) -> isortlist#1#(@l) isortlist#1#(::(@x,@xs)) -> insert#(@x,isortlist(@xs)) isortlist#1#(::(@x,@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: WeightGap {wgDimension = 1, wgDegree = 1, wgKind = Algebraic, wgUArgs = UArgs, wgOn = WgOnAny} + Details: The weightgap principle applies using the following constant growth matrix-interpretation: We apply a matrix interpretation of kind constructor based matrix interpretation: The following argument positions are considered usable: uargs(#and) = {1,2}, uargs(#cklt) = {1}, uargs(::) = {2}, uargs(and) = {1,2}, uargs(insert) = {2}, uargs(insert#2) = {1}, uargs(or) = {1,2}, uargs(insert#) = {2}, uargs(insert#2#) = {1}, uargs(c_12) = {1}, uargs(c_13) = {1}, uargs(c_15) = {1} Following symbols are considered usable: all TcT has computed the following interpretation: p(#0) = [0] p(#EQ) = [0] p(#GT) = [0] p(#LT) = [0] p(#and) = [1] x1 + [1] x2 + [0] p(#cklt) = [1] x1 + [0] p(#compare) = [0] p(#eq) = [0] p(#equal) = [0] p(#false) = [0] p(#less) = [0] p(#neg) = [1] x1 + [0] p(#or) = [0] p(#pos) = [1] x1 + [0] p(#s) = [1] x1 + [0] p(#true) = [0] p(::) = [1] x1 + [1] x2 + [1] p(and) = [1] x1 + [1] x2 + [0] p(insert) = [1] x1 + [1] x2 + [1] p(insert#1) = [1] x1 + [1] x2 + [1] p(insert#2) = [1] x1 + [1] x2 + [1] x3 + [1] x4 + [2] p(isortlist) = [2] x1 + [2] p(isortlist#1) = [2] x1 + [1] p(leq) = [0] p(leq#1) = [0] p(leq#2) = [0] p(nil) = [0] p(or) = [1] x1 + [1] x2 + [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#) = [1] x2 + [0] p(insert#1#) = [1] x1 + [0] p(insert#2#) = [1] x1 + [1] x3 + [1] x4 + [1] p(isortlist#) = [4] x1 + [0] p(isortlist#1#) = [4] x1 + [0] p(leq#) = [1] p(leq#1#) = [0] p(leq#2#) = [3] p(or#) = [0] p(c_1) = [0] p(c_2) = [0] p(c_3) = [1] x1 + [0] p(c_4) = [0] p(c_5) = [0] p(c_6) = [0] p(c_7) = [0] p(c_8) = [0] p(c_9) = [0] p(c_10) = [0] p(c_11) = [0] p(c_12) = [1] x1 + [0] p(c_13) = [1] x1 + [0] p(c_14) = [0] p(c_15) = [1] x1 + [0] 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] > [0] = c_12(leq#1#(@l1,@l2)) leq#2#(::(@y,@ys),@x,@xs) = [3] > [1] = c_15(leq#(@xs,@ys)) Following rules are (at-least) weakly oriented: insert#(@x,@l) = [1] @l + [0] >= [1] @l + [0] = insert#1#(@l,@x) insert#1#(::(@y,@ys),@x) = [1] @y + [1] @ys + [1] >= [1] @y + [1] @ys + [1] = insert#2#(leq(@x,@y),@x,@y,@ys) insert#1#(::(@y,@ys),@x) = [1] @y + [1] @ys + [1] >= [1] = leq#(@x,@y) insert#2#(#false(),@x,@y,@ys) = [1] @y + [1] @ys + [1] >= [1] @ys + [0] = insert#(@x,@ys) isortlist#(@l) = [4] @l + [0] >= [4] @l + [0] = isortlist#1#(@l) isortlist#1#(::(@x,@xs)) = [4] @x + [4] @xs + [4] >= [2] @xs + [2] = insert#(@x,isortlist(@xs)) isortlist#1#(::(@x,@xs)) = [4] @x + [4] @xs + [4] >= [4] @xs + [0] = isortlist#(@xs) leq#1#(::(@x,@xs),@l2) = [0] >= [3] = c_13(leq#2#(@l2,@x,@xs)) #and(#false(),#false()) = [0] >= [0] = #false() #and(#false(),#true()) = [0] >= [0] = #false() #and(#true(),#false()) = [0] >= [0] = #false() #and(#true(),#true()) = [0] >= [0] = #true() #cklt(#EQ()) = [0] >= [0] = #false() #cklt(#GT()) = [0] >= [0] = #false() #cklt(#LT()) = [0] >= [0] = #true() #compare(#0(),#0()) = [0] >= [0] = #EQ() #compare(#0(),#neg(@y)) = [0] >= [0] = #GT() #compare(#0(),#pos(@y)) = [0] >= [0] = #LT() #compare(#0(),#s(@y)) = [0] >= [0] = #LT() #compare(#neg(@x),#0()) = [0] >= [0] = #LT() #compare(#neg(@x),#neg(@y)) = [0] >= [0] = #compare(@y,@x) #compare(#neg(@x),#pos(@y)) = [0] >= [0] = #LT() #compare(#pos(@x),#0()) = [0] >= [0] = #GT() #compare(#pos(@x),#neg(@y)) = [0] >= [0] = #GT() #compare(#pos(@x),#pos(@y)) = [0] >= [0] = #compare(@x,@y) #compare(#s(@x),#0()) = [0] >= [0] = #GT() #compare(#s(@x),#s(@y)) = [0] >= [0] = #compare(@x,@y) #eq(#0(),#0()) = [0] >= [0] = #true() #eq(#0(),#neg(@y)) = [0] >= [0] = #false() #eq(#0(),#pos(@y)) = [0] >= [0] = #false() #eq(#0(),#s(@y)) = [0] >= [0] = #false() #eq(#neg(@x),#0()) = [0] >= [0] = #false() #eq(#neg(@x),#neg(@y)) = [0] >= [0] = #eq(@x,@y) #eq(#neg(@x),#pos(@y)) = [0] >= [0] = #false() #eq(#pos(@x),#0()) = [0] >= [0] = #false() #eq(#pos(@x),#neg(@y)) = [0] >= [0] = #false() #eq(#pos(@x),#pos(@y)) = [0] >= [0] = #eq(@x,@y) #eq(#s(@x),#0()) = [0] >= [0] = #false() #eq(#s(@x),#s(@y)) = [0] >= [0] = #eq(@x,@y) #eq(::(@x_1,@x_2),::(@y_1,@y_2)) = [0] >= [0] = #and(#eq(@x_1,@y_1),#eq(@x_2,@y_2)) #eq(::(@x_1,@x_2),nil()) = [0] >= [0] = #false() #eq(nil(),::(@y_1,@y_2)) = [0] >= [0] = #false() #eq(nil(),nil()) = [0] >= [0] = #true() #equal(@x,@y) = [0] >= [0] = #eq(@x,@y) #less(@x,@y) = [0] >= [0] = #cklt(#compare(@x,@y)) #or(#false(),#false()) = [0] >= [0] = #false() #or(#false(),#true()) = [0] >= [0] = #true() #or(#true(),#false()) = [0] >= [0] = #true() #or(#true(),#true()) = [0] >= [0] = #true() and(@x,@y) = [1] @x + [1] @y + [0] >= [1] @x + [1] @y + [0] = #and(@x,@y) insert(@x,@l) = [1] @l + [1] @x + [1] >= [1] @l + [1] @x + [1] = insert#1(@l,@x) insert#1(::(@y,@ys),@x) = [1] @x + [1] @y + [1] @ys + [2] >= [1] @x + [1] @y + [1] @ys + [2] = insert#2(leq(@x,@y),@x,@y,@ys) insert#1(nil(),@x) = [1] @x + [1] >= [1] @x + [1] = ::(@x,nil()) insert#2(#false(),@x,@y,@ys) = [1] @x + [1] @y + [1] @ys + [2] >= [1] @x + [1] @y + [1] @ys + [2] = ::(@y,insert(@x,@ys)) insert#2(#true(),@x,@y,@ys) = [1] @x + [1] @y + [1] @ys + [2] >= [1] @x + [1] @y + [1] @ys + [2] = ::(@x,::(@y,@ys)) isortlist(@l) = [2] @l + [2] >= [2] @l + [1] = isortlist#1(@l) isortlist#1(::(@x,@xs)) = [2] @x + [2] @xs + [3] >= [1] @x + [2] @xs + [3] = insert(@x,isortlist(@xs)) isortlist#1(nil()) = [1] >= [0] = nil() leq(@l1,@l2) = [0] >= [0] = leq#1(@l1,@l2) leq#1(::(@x,@xs),@l2) = [0] >= [0] = leq#2(@l2,@x,@xs) leq#1(nil(),@l2) = [0] >= [0] = #true() leq#2(::(@y,@ys),@x,@xs) = [0] >= [0] = or(#less(@x,@y),and(#equal(@x,@y),leq(@xs,@ys))) leq#2(nil(),@x,@xs) = [0] >= [0] = #false() or(@x,@y) = [1] @x + [1] @y + [0] >= [0] = #or(@x,@y) Further, it can be verified that all rules not oriented are covered by the weightgap condition. *** Step 5.b:1.b:2: WeightGap WORST_CASE(?,O(n^1)) + Considered Problem: - Strict DPs: leq#1#(::(@x,@xs),@l2) -> c_13(leq#2#(@l2,@x,@xs)) - Weak DPs: insert#(@x,@l) -> insert#1#(@l,@x) insert#1#(::(@y,@ys),@x) -> insert#2#(leq(@x,@y),@x,@y,@ys) insert#1#(::(@y,@ys),@x) -> leq#(@x,@y) insert#2#(#false(),@x,@y,@ys) -> insert#(@x,@ys) isortlist#(@l) -> isortlist#1#(@l) isortlist#1#(::(@x,@xs)) -> insert#(@x,isortlist(@xs)) isortlist#1#(::(@x,@xs)) -> isortlist#(@xs) leq#(@l1,@l2) -> c_12(leq#1#(@l1,@l2)) 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: WeightGap {wgDimension = 1, wgDegree = 1, wgKind = Algebraic, wgUArgs = UArgs, wgOn = WgOnAny} + Details: The weightgap principle applies using the following constant growth matrix-interpretation: We apply a matrix interpretation of kind constructor based matrix interpretation: The following argument positions are considered usable: uargs(#and) = {1,2}, uargs(#cklt) = {1}, uargs(::) = {2}, uargs(and) = {1,2}, uargs(insert) = {2}, uargs(insert#2) = {1}, uargs(or) = {1,2}, uargs(insert#) = {2}, uargs(insert#2#) = {1}, uargs(c_12) = {1}, uargs(c_13) = {1}, uargs(c_15) = {1} Following symbols are considered usable: all TcT has computed the following interpretation: p(#0) = [2] p(#EQ) = [0] p(#GT) = [0] p(#LT) = [0] p(#and) = [1] x1 + [1] x2 + [0] p(#cklt) = [1] x1 + [0] p(#compare) = [0] p(#eq) = [0] p(#equal) = [0] p(#false) = [0] p(#less) = [0] p(#neg) = [1] x1 + [0] p(#or) = [1] x2 + [0] p(#pos) = [1] x1 + [0] p(#s) = [4] p(#true) = [0] p(::) = [1] x1 + [1] x2 + [1] p(and) = [1] x1 + [1] x2 + [0] p(insert) = [1] x1 + [1] x2 + [1] p(insert#1) = [1] x1 + [1] x2 + [1] p(insert#2) = [1] x1 + [1] x2 + [1] x3 + [1] x4 + [2] p(isortlist) = [1] x1 + [0] p(isortlist#1) = [1] x1 + [0] p(leq) = [0] p(leq#1) = [0] p(leq#2) = [0] p(nil) = [1] p(or) = [1] x1 + [1] x2 + [0] p(#and#) = [1] x2 + [0] p(#cklt#) = [2] x1 + [1] p(#compare#) = [4] x1 + [1] x2 + [4] p(#eq#) = [2] x1 + [0] p(#equal#) = [1] x1 + [2] p(#less#) = [1] x1 + [2] x2 + [1] p(#or#) = [4] x1 + [4] p(and#) = [1] x1 + [1] x2 + [0] p(insert#) = [1] x1 + [1] x2 + [0] p(insert#1#) = [1] x1 + [1] x2 + [0] p(insert#2#) = [1] x1 + [1] x2 + [1] x3 + [1] x4 + [0] p(isortlist#) = [1] x1 + [5] p(isortlist#1#) = [1] x1 + [4] p(leq#) = [1] x1 + [0] p(leq#1#) = [1] x1 + [0] p(leq#2#) = [1] x2 + [1] x3 + [0] p(or#) = [1] x2 + [0] p(c_1) = [1] x1 + [0] p(c_2) = [4] x1 + [1] x2 + [1] p(c_3) = [0] p(c_4) = [0] p(c_5) = [2] x1 + [1] p(c_6) = [2] p(c_7) = [2] p(c_8) = [0] p(c_9) = [4] x1 + [2] p(c_10) = [1] x1 + [1] x2 + [1] p(c_11) = [1] p(c_12) = [1] x1 + [0] p(c_13) = [1] x1 + [0] p(c_14) = [1] p(c_15) = [1] x1 + [0] p(c_16) = [1] p(c_17) = [1] x1 + [0] p(c_18) = [1] p(c_19) = [4] p(c_20) = [4] p(c_21) = [0] p(c_22) = [0] p(c_23) = [0] p(c_24) = [4] p(c_25) = [0] p(c_26) = [4] p(c_27) = [1] p(c_28) = [1] p(c_29) = [4] p(c_30) = [0] p(c_31) = [0] p(c_32) = [1] p(c_33) = [1] p(c_34) = [1] x1 + [0] p(c_35) = [2] p(c_36) = [1] p(c_37) = [1] p(c_38) = [0] p(c_39) = [4] p(c_40) = [1] p(c_41) = [0] p(c_42) = [0] p(c_43) = [1] p(c_44) = [4] p(c_45) = [0] p(c_46) = [4] x1 + [0] p(c_47) = [0] p(c_48) = [1] x1 + [2] p(c_49) = [1] x1 + [1] p(c_50) = [0] p(c_51) = [1] p(c_52) = [1] p(c_53) = [1] p(c_54) = [0] p(c_55) = [1] p(c_56) = [0] Following rules are strictly oriented: leq#1#(::(@x,@xs),@l2) = [1] @x + [1] @xs + [1] > [1] @x + [1] @xs + [0] = c_13(leq#2#(@l2,@x,@xs)) Following rules are (at-least) weakly oriented: insert#(@x,@l) = [1] @l + [1] @x + [0] >= [1] @l + [1] @x + [0] = insert#1#(@l,@x) insert#1#(::(@y,@ys),@x) = [1] @x + [1] @y + [1] @ys + [1] >= [1] @x + [1] @y + [1] @ys + [0] = insert#2#(leq(@x,@y),@x,@y,@ys) insert#1#(::(@y,@ys),@x) = [1] @x + [1] @y + [1] @ys + [1] >= [1] @x + [0] = leq#(@x,@y) insert#2#(#false(),@x,@y,@ys) = [1] @x + [1] @y + [1] @ys + [0] >= [1] @x + [1] @ys + [0] = insert#(@x,@ys) isortlist#(@l) = [1] @l + [5] >= [1] @l + [4] = isortlist#1#(@l) isortlist#1#(::(@x,@xs)) = [1] @x + [1] @xs + [5] >= [1] @x + [1] @xs + [0] = insert#(@x,isortlist(@xs)) isortlist#1#(::(@x,@xs)) = [1] @x + [1] @xs + [5] >= [1] @xs + [5] = isortlist#(@xs) leq#(@l1,@l2) = [1] @l1 + [0] >= [1] @l1 + [0] = c_12(leq#1#(@l1,@l2)) leq#2#(::(@y,@ys),@x,@xs) = [1] @x + [1] @xs + [0] >= [1] @xs + [0] = c_15(leq#(@xs,@ys)) #and(#false(),#false()) = [0] >= [0] = #false() #and(#false(),#true()) = [0] >= [0] = #false() #and(#true(),#false()) = [0] >= [0] = #false() #and(#true(),#true()) = [0] >= [0] = #true() #cklt(#EQ()) = [0] >= [0] = #false() #cklt(#GT()) = [0] >= [0] = #false() #cklt(#LT()) = [0] >= [0] = #true() #compare(#0(),#0()) = [0] >= [0] = #EQ() #compare(#0(),#neg(@y)) = [0] >= [0] = #GT() #compare(#0(),#pos(@y)) = [0] >= [0] = #LT() #compare(#0(),#s(@y)) = [0] >= [0] = #LT() #compare(#neg(@x),#0()) = [0] >= [0] = #LT() #compare(#neg(@x),#neg(@y)) = [0] >= [0] = #compare(@y,@x) #compare(#neg(@x),#pos(@y)) = [0] >= [0] = #LT() #compare(#pos(@x),#0()) = [0] >= [0] = #GT() #compare(#pos(@x),#neg(@y)) = [0] >= [0] = #GT() #compare(#pos(@x),#pos(@y)) = [0] >= [0] = #compare(@x,@y) #compare(#s(@x),#0()) = [0] >= [0] = #GT() #compare(#s(@x),#s(@y)) = [0] >= [0] = #compare(@x,@y) #eq(#0(),#0()) = [0] >= [0] = #true() #eq(#0(),#neg(@y)) = [0] >= [0] = #false() #eq(#0(),#pos(@y)) = [0] >= [0] = #false() #eq(#0(),#s(@y)) = [0] >= [0] = #false() #eq(#neg(@x),#0()) = [0] >= [0] = #false() #eq(#neg(@x),#neg(@y)) = [0] >= [0] = #eq(@x,@y) #eq(#neg(@x),#pos(@y)) = [0] >= [0] = #false() #eq(#pos(@x),#0()) = [0] >= [0] = #false() #eq(#pos(@x),#neg(@y)) = [0] >= [0] = #false() #eq(#pos(@x),#pos(@y)) = [0] >= [0] = #eq(@x,@y) #eq(#s(@x),#0()) = [0] >= [0] = #false() #eq(#s(@x),#s(@y)) = [0] >= [0] = #eq(@x,@y) #eq(::(@x_1,@x_2),::(@y_1,@y_2)) = [0] >= [0] = #and(#eq(@x_1,@y_1),#eq(@x_2,@y_2)) #eq(::(@x_1,@x_2),nil()) = [0] >= [0] = #false() #eq(nil(),::(@y_1,@y_2)) = [0] >= [0] = #false() #eq(nil(),nil()) = [0] >= [0] = #true() #equal(@x,@y) = [0] >= [0] = #eq(@x,@y) #less(@x,@y) = [0] >= [0] = #cklt(#compare(@x,@y)) #or(#false(),#false()) = [0] >= [0] = #false() #or(#false(),#true()) = [0] >= [0] = #true() #or(#true(),#false()) = [0] >= [0] = #true() #or(#true(),#true()) = [0] >= [0] = #true() and(@x,@y) = [1] @x + [1] @y + [0] >= [1] @x + [1] @y + [0] = #and(@x,@y) insert(@x,@l) = [1] @l + [1] @x + [1] >= [1] @l + [1] @x + [1] = insert#1(@l,@x) insert#1(::(@y,@ys),@x) = [1] @x + [1] @y + [1] @ys + [2] >= [1] @x + [1] @y + [1] @ys + [2] = insert#2(leq(@x,@y),@x,@y,@ys) insert#1(nil(),@x) = [1] @x + [2] >= [1] @x + [2] = ::(@x,nil()) insert#2(#false(),@x,@y,@ys) = [1] @x + [1] @y + [1] @ys + [2] >= [1] @x + [1] @y + [1] @ys + [2] = ::(@y,insert(@x,@ys)) insert#2(#true(),@x,@y,@ys) = [1] @x + [1] @y + [1] @ys + [2] >= [1] @x + [1] @y + [1] @ys + [2] = ::(@x,::(@y,@ys)) isortlist(@l) = [1] @l + [0] >= [1] @l + [0] = isortlist#1(@l) isortlist#1(::(@x,@xs)) = [1] @x + [1] @xs + [1] >= [1] @x + [1] @xs + [1] = insert(@x,isortlist(@xs)) isortlist#1(nil()) = [1] >= [1] = nil() leq(@l1,@l2) = [0] >= [0] = leq#1(@l1,@l2) leq#1(::(@x,@xs),@l2) = [0] >= [0] = leq#2(@l2,@x,@xs) leq#1(nil(),@l2) = [0] >= [0] = #true() leq#2(::(@y,@ys),@x,@xs) = [0] >= [0] = or(#less(@x,@y),and(#equal(@x,@y),leq(@xs,@ys))) leq#2(nil(),@x,@xs) = [0] >= [0] = #false() or(@x,@y) = [1] @x + [1] @y + [0] >= [1] @y + [0] = #or(@x,@y) Further, it can be verified that all rules not oriented are covered by the weightgap condition. *** Step 5.b:1.b:3: EmptyProcessor WORST_CASE(?,O(1)) + Considered Problem: - Weak DPs: insert#(@x,@l) -> insert#1#(@l,@x) insert#1#(::(@y,@ys),@x) -> insert#2#(leq(@x,@y),@x,@y,@ys) insert#1#(::(@y,@ys),@x) -> leq#(@x,@y) insert#2#(#false(),@x,@y,@ys) -> insert#(@x,@ys) isortlist#(@l) -> isortlist#1#(@l) isortlist#1#(::(@x,@xs)) -> insert#(@x,isortlist(@xs)) isortlist#1#(::(@x,@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: EmptyProcessor + Details: The problem is already closed. The intended complexity is O(1). WORST_CASE(?,O(n^3))