WORST_CASE(?,O(n^3)) * Step 1: DependencyPairs WORST_CASE(?,O(n^3)) + Considered Problem: - Strict TRS: #abs(#0()) -> #0() #abs(#neg(@x)) -> #pos(@x) #abs(#pos(@x)) -> #pos(@x) #abs(#s(@x)) -> #pos(#s(@x)) #less(@x,@y) -> #cklt(#compare(@x,@y)) insert(@x,@l) -> insert#1(@l,@x) insert#1(::(@y,@ys),@x) -> insert#2(#less(@y,@x),@x,@y,@ys) insert#1(nil(),@x) -> ::(@x,nil()) insert#2(#false(),@x,@y,@ys) -> ::(@x,::(@y,@ys)) insert#2(#true(),@x,@y,@ys) -> ::(@y,insert(@x,@ys)) insertD(@x,@l) -> insertD#1(@l,@x) insertD#1(::(@y,@ys),@x) -> insertD#2(#less(@y,@x),@x,@y,@ys) insertD#1(nil(),@x) -> ::(@x,nil()) insertD#2(#false(),@x,@y,@ys) -> ::(@x,::(@y,@ys)) insertD#2(#true(),@x,@y,@ys) -> ::(@y,insertD(@x,@ys)) insertionsort(@l) -> insertionsort#1(@l) insertionsort#1(::(@x,@xs)) -> insert(@x,insertionsort(@xs)) insertionsort#1(nil()) -> nil() insertionsortD(@l) -> insertionsortD#1(@l) insertionsortD#1(::(@x,@xs)) -> insertD(@x,insertionsortD(@xs)) insertionsortD#1(nil()) -> nil() testInsertionsort(@x) -> insertionsort(testList(#unit())) testInsertionsortD(@x) -> insertionsortD(testList(#unit())) testList(@_) -> ::(#abs(#0()) ,::(#abs(#pos(#s(#s(#s(#s(#0())))))) ,::(#abs(#pos(#s(#s(#s(#s(#s(#0()))))))) ,::(#abs(#pos(#s(#s(#s(#s(#s(#s(#s(#s(#s(#0()))))))))))) ,::(#abs(#pos(#s(#s(#s(#s(#s(#s(#s(#0()))))))))) ,::(#abs(#pos(#s(#0()))) ,::(#abs(#pos(#s(#s(#0())))) ,::(#abs(#pos(#s(#s(#s(#s(#s(#s(#s(#s(#0())))))))))) ,::(#abs(#pos(#s(#s(#s(#s(#s(#s(#0())))))))) ,::(#abs(#pos(#s(#s(#s(#0()))))),nil())))))))))) - Weak TRS: #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) - Signature: {#abs/1,#cklt/1,#compare/2,#less/2,insert/2,insert#1/2,insert#2/4,insertD/2,insertD#1/2,insertD#2/4 ,insertionsort/1,insertionsort#1/1,insertionsortD/1,insertionsortD#1/1,testInsertionsort/1 ,testInsertionsortD/1,testList/1} / {#0/0,#EQ/0,#GT/0,#LT/0,#false/0,#neg/1,#pos/1,#s/1,#true/0,#unit/0,::/2 ,nil/0} - Obligation: innermost runtime complexity wrt. defined symbols {#abs,#cklt,#compare,#less,insert,insert#1,insert#2 ,insertD,insertD#1,insertD#2,insertionsort,insertionsort#1,insertionsortD,insertionsortD#1,testInsertionsort ,testInsertionsortD,testList} and constructors {#0,#EQ,#GT,#LT,#false,#neg,#pos,#s,#true,#unit,::,nil} + Applied Processor: DependencyPairs {dpKind_ = DT} + Details: We add the following dependency tuples: Strict DPs #abs#(#0()) -> c_1() #abs#(#neg(@x)) -> c_2() #abs#(#pos(@x)) -> c_3() #abs#(#s(@x)) -> c_4() #less#(@x,@y) -> c_5(#cklt#(#compare(@x,@y)),#compare#(@x,@y)) insert#(@x,@l) -> c_6(insert#1#(@l,@x)) insert#1#(::(@y,@ys),@x) -> c_7(insert#2#(#less(@y,@x),@x,@y,@ys),#less#(@y,@x)) insert#1#(nil(),@x) -> c_8() insert#2#(#false(),@x,@y,@ys) -> c_9() insert#2#(#true(),@x,@y,@ys) -> c_10(insert#(@x,@ys)) insertD#(@x,@l) -> c_11(insertD#1#(@l,@x)) insertD#1#(::(@y,@ys),@x) -> c_12(insertD#2#(#less(@y,@x),@x,@y,@ys),#less#(@y,@x)) insertD#1#(nil(),@x) -> c_13() insertD#2#(#false(),@x,@y,@ys) -> c_14() insertD#2#(#true(),@x,@y,@ys) -> c_15(insertD#(@x,@ys)) insertionsort#(@l) -> c_16(insertionsort#1#(@l)) insertionsort#1#(::(@x,@xs)) -> c_17(insert#(@x,insertionsort(@xs)),insertionsort#(@xs)) insertionsort#1#(nil()) -> c_18() insertionsortD#(@l) -> c_19(insertionsortD#1#(@l)) insertionsortD#1#(::(@x,@xs)) -> c_20(insertD#(@x,insertionsortD(@xs)),insertionsortD#(@xs)) insertionsortD#1#(nil()) -> c_21() testInsertionsort#(@x) -> c_22(insertionsort#(testList(#unit())),testList#(#unit())) testInsertionsortD#(@x) -> c_23(insertionsortD#(testList(#unit())),testList#(#unit())) testList#(@_) -> c_24(#abs#(#0()) ,#abs#(#pos(#s(#s(#s(#s(#0())))))) ,#abs#(#pos(#s(#s(#s(#s(#s(#0()))))))) ,#abs#(#pos(#s(#s(#s(#s(#s(#s(#s(#s(#s(#0()))))))))))) ,#abs#(#pos(#s(#s(#s(#s(#s(#s(#s(#0()))))))))) ,#abs#(#pos(#s(#0()))) ,#abs#(#pos(#s(#s(#0())))) ,#abs#(#pos(#s(#s(#s(#s(#s(#s(#s(#s(#0())))))))))) ,#abs#(#pos(#s(#s(#s(#s(#s(#s(#0())))))))) ,#abs#(#pos(#s(#s(#s(#0())))))) Weak DPs #cklt#(#EQ()) -> c_25() #cklt#(#GT()) -> c_26() #cklt#(#LT()) -> c_27() #compare#(#0(),#0()) -> c_28() #compare#(#0(),#neg(@y)) -> c_29() #compare#(#0(),#pos(@y)) -> c_30() #compare#(#0(),#s(@y)) -> c_31() #compare#(#neg(@x),#0()) -> c_32() #compare#(#neg(@x),#neg(@y)) -> c_33(#compare#(@y,@x)) #compare#(#neg(@x),#pos(@y)) -> c_34() #compare#(#pos(@x),#0()) -> c_35() #compare#(#pos(@x),#neg(@y)) -> c_36() #compare#(#pos(@x),#pos(@y)) -> c_37(#compare#(@x,@y)) #compare#(#s(@x),#0()) -> c_38() #compare#(#s(@x),#s(@y)) -> c_39(#compare#(@x,@y)) and mark the set of starting terms. * Step 2: PredecessorEstimation WORST_CASE(?,O(n^3)) + Considered Problem: - Strict DPs: #abs#(#0()) -> c_1() #abs#(#neg(@x)) -> c_2() #abs#(#pos(@x)) -> c_3() #abs#(#s(@x)) -> c_4() #less#(@x,@y) -> c_5(#cklt#(#compare(@x,@y)),#compare#(@x,@y)) insert#(@x,@l) -> c_6(insert#1#(@l,@x)) insert#1#(::(@y,@ys),@x) -> c_7(insert#2#(#less(@y,@x),@x,@y,@ys),#less#(@y,@x)) insert#1#(nil(),@x) -> c_8() insert#2#(#false(),@x,@y,@ys) -> c_9() insert#2#(#true(),@x,@y,@ys) -> c_10(insert#(@x,@ys)) insertD#(@x,@l) -> c_11(insertD#1#(@l,@x)) insertD#1#(::(@y,@ys),@x) -> c_12(insertD#2#(#less(@y,@x),@x,@y,@ys),#less#(@y,@x)) insertD#1#(nil(),@x) -> c_13() insertD#2#(#false(),@x,@y,@ys) -> c_14() insertD#2#(#true(),@x,@y,@ys) -> c_15(insertD#(@x,@ys)) insertionsort#(@l) -> c_16(insertionsort#1#(@l)) insertionsort#1#(::(@x,@xs)) -> c_17(insert#(@x,insertionsort(@xs)),insertionsort#(@xs)) insertionsort#1#(nil()) -> c_18() insertionsortD#(@l) -> c_19(insertionsortD#1#(@l)) insertionsortD#1#(::(@x,@xs)) -> c_20(insertD#(@x,insertionsortD(@xs)),insertionsortD#(@xs)) insertionsortD#1#(nil()) -> c_21() testInsertionsort#(@x) -> c_22(insertionsort#(testList(#unit())),testList#(#unit())) testInsertionsortD#(@x) -> c_23(insertionsortD#(testList(#unit())),testList#(#unit())) testList#(@_) -> c_24(#abs#(#0()) ,#abs#(#pos(#s(#s(#s(#s(#0())))))) ,#abs#(#pos(#s(#s(#s(#s(#s(#0()))))))) ,#abs#(#pos(#s(#s(#s(#s(#s(#s(#s(#s(#s(#0()))))))))))) ,#abs#(#pos(#s(#s(#s(#s(#s(#s(#s(#0()))))))))) ,#abs#(#pos(#s(#0()))) ,#abs#(#pos(#s(#s(#0())))) ,#abs#(#pos(#s(#s(#s(#s(#s(#s(#s(#s(#0())))))))))) ,#abs#(#pos(#s(#s(#s(#s(#s(#s(#0())))))))) ,#abs#(#pos(#s(#s(#s(#0())))))) - Weak DPs: #cklt#(#EQ()) -> c_25() #cklt#(#GT()) -> c_26() #cklt#(#LT()) -> c_27() #compare#(#0(),#0()) -> c_28() #compare#(#0(),#neg(@y)) -> c_29() #compare#(#0(),#pos(@y)) -> c_30() #compare#(#0(),#s(@y)) -> c_31() #compare#(#neg(@x),#0()) -> c_32() #compare#(#neg(@x),#neg(@y)) -> c_33(#compare#(@y,@x)) #compare#(#neg(@x),#pos(@y)) -> c_34() #compare#(#pos(@x),#0()) -> c_35() #compare#(#pos(@x),#neg(@y)) -> c_36() #compare#(#pos(@x),#pos(@y)) -> c_37(#compare#(@x,@y)) #compare#(#s(@x),#0()) -> c_38() #compare#(#s(@x),#s(@y)) -> c_39(#compare#(@x,@y)) - Weak TRS: #abs(#0()) -> #0() #abs(#neg(@x)) -> #pos(@x) #abs(#pos(@x)) -> #pos(@x) #abs(#s(@x)) -> #pos(#s(@x)) #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) #less(@x,@y) -> #cklt(#compare(@x,@y)) insert(@x,@l) -> insert#1(@l,@x) insert#1(::(@y,@ys),@x) -> insert#2(#less(@y,@x),@x,@y,@ys) insert#1(nil(),@x) -> ::(@x,nil()) insert#2(#false(),@x,@y,@ys) -> ::(@x,::(@y,@ys)) insert#2(#true(),@x,@y,@ys) -> ::(@y,insert(@x,@ys)) insertD(@x,@l) -> insertD#1(@l,@x) insertD#1(::(@y,@ys),@x) -> insertD#2(#less(@y,@x),@x,@y,@ys) insertD#1(nil(),@x) -> ::(@x,nil()) insertD#2(#false(),@x,@y,@ys) -> ::(@x,::(@y,@ys)) insertD#2(#true(),@x,@y,@ys) -> ::(@y,insertD(@x,@ys)) insertionsort(@l) -> insertionsort#1(@l) insertionsort#1(::(@x,@xs)) -> insert(@x,insertionsort(@xs)) insertionsort#1(nil()) -> nil() insertionsortD(@l) -> insertionsortD#1(@l) insertionsortD#1(::(@x,@xs)) -> insertD(@x,insertionsortD(@xs)) insertionsortD#1(nil()) -> nil() testInsertionsort(@x) -> insertionsort(testList(#unit())) testInsertionsortD(@x) -> insertionsortD(testList(#unit())) testList(@_) -> ::(#abs(#0()) ,::(#abs(#pos(#s(#s(#s(#s(#0())))))) ,::(#abs(#pos(#s(#s(#s(#s(#s(#0()))))))) ,::(#abs(#pos(#s(#s(#s(#s(#s(#s(#s(#s(#s(#0()))))))))))) ,::(#abs(#pos(#s(#s(#s(#s(#s(#s(#s(#0()))))))))) ,::(#abs(#pos(#s(#0()))) ,::(#abs(#pos(#s(#s(#0())))) ,::(#abs(#pos(#s(#s(#s(#s(#s(#s(#s(#s(#0())))))))))) ,::(#abs(#pos(#s(#s(#s(#s(#s(#s(#0())))))))) ,::(#abs(#pos(#s(#s(#s(#0()))))),nil())))))))))) - Signature: {#abs/1,#cklt/1,#compare/2,#less/2,insert/2,insert#1/2,insert#2/4,insertD/2,insertD#1/2,insertD#2/4 ,insertionsort/1,insertionsort#1/1,insertionsortD/1,insertionsortD#1/1,testInsertionsort/1 ,testInsertionsortD/1,testList/1,#abs#/1,#cklt#/1,#compare#/2,#less#/2,insert#/2,insert#1#/2,insert#2#/4 ,insertD#/2,insertD#1#/2,insertD#2#/4,insertionsort#/1,insertionsort#1#/1,insertionsortD#/1 ,insertionsortD#1#/1,testInsertionsort#/1,testInsertionsortD#/1,testList#/1} / {#0/0,#EQ/0,#GT/0,#LT/0 ,#false/0,#neg/1,#pos/1,#s/1,#true/0,#unit/0,::/2,nil/0,c_1/0,c_2/0,c_3/0,c_4/0,c_5/2,c_6/1,c_7/2,c_8/0 ,c_9/0,c_10/1,c_11/1,c_12/2,c_13/0,c_14/0,c_15/1,c_16/1,c_17/2,c_18/0,c_19/1,c_20/2,c_21/0,c_22/2,c_23/2 ,c_24/10,c_25/0,c_26/0,c_27/0,c_28/0,c_29/0,c_30/0,c_31/0,c_32/0,c_33/1,c_34/0,c_35/0,c_36/0,c_37/1,c_38/0 ,c_39/1} - Obligation: innermost runtime complexity wrt. defined symbols {#abs#,#cklt#,#compare#,#less#,insert#,insert#1#,insert#2# ,insertD#,insertD#1#,insertD#2#,insertionsort#,insertionsort#1#,insertionsortD#,insertionsortD#1# ,testInsertionsort#,testInsertionsortD#,testList#} and constructors {#0,#EQ,#GT,#LT,#false,#neg,#pos,#s ,#true,#unit,::,nil} + Applied Processor: PredecessorEstimation {onSelection = all simple predecessor estimation selector} + Details: We estimate the number of application of {1,2,3,4,5,8,9,13,14,18,21} by application of Pre({1,2,3,4,5,8,9,13,14,18,21}) = {6,7,11,12,16,19,24}. Here rules are labelled as follows: 1: #abs#(#0()) -> c_1() 2: #abs#(#neg(@x)) -> c_2() 3: #abs#(#pos(@x)) -> c_3() 4: #abs#(#s(@x)) -> c_4() 5: #less#(@x,@y) -> c_5(#cklt#(#compare(@x,@y)),#compare#(@x,@y)) 6: insert#(@x,@l) -> c_6(insert#1#(@l,@x)) 7: insert#1#(::(@y,@ys),@x) -> c_7(insert#2#(#less(@y,@x),@x,@y,@ys),#less#(@y,@x)) 8: insert#1#(nil(),@x) -> c_8() 9: insert#2#(#false(),@x,@y,@ys) -> c_9() 10: insert#2#(#true(),@x,@y,@ys) -> c_10(insert#(@x,@ys)) 11: insertD#(@x,@l) -> c_11(insertD#1#(@l,@x)) 12: insertD#1#(::(@y,@ys),@x) -> c_12(insertD#2#(#less(@y,@x),@x,@y,@ys),#less#(@y,@x)) 13: insertD#1#(nil(),@x) -> c_13() 14: insertD#2#(#false(),@x,@y,@ys) -> c_14() 15: insertD#2#(#true(),@x,@y,@ys) -> c_15(insertD#(@x,@ys)) 16: insertionsort#(@l) -> c_16(insertionsort#1#(@l)) 17: insertionsort#1#(::(@x,@xs)) -> c_17(insert#(@x,insertionsort(@xs)),insertionsort#(@xs)) 18: insertionsort#1#(nil()) -> c_18() 19: insertionsortD#(@l) -> c_19(insertionsortD#1#(@l)) 20: insertionsortD#1#(::(@x,@xs)) -> c_20(insertD#(@x,insertionsortD(@xs)),insertionsortD#(@xs)) 21: insertionsortD#1#(nil()) -> c_21() 22: testInsertionsort#(@x) -> c_22(insertionsort#(testList(#unit())),testList#(#unit())) 23: testInsertionsortD#(@x) -> c_23(insertionsortD#(testList(#unit())),testList#(#unit())) 24: testList#(@_) -> c_24(#abs#(#0()) ,#abs#(#pos(#s(#s(#s(#s(#0())))))) ,#abs#(#pos(#s(#s(#s(#s(#s(#0()))))))) ,#abs#(#pos(#s(#s(#s(#s(#s(#s(#s(#s(#s(#0()))))))))))) ,#abs#(#pos(#s(#s(#s(#s(#s(#s(#s(#0()))))))))) ,#abs#(#pos(#s(#0()))) ,#abs#(#pos(#s(#s(#0())))) ,#abs#(#pos(#s(#s(#s(#s(#s(#s(#s(#s(#0())))))))))) ,#abs#(#pos(#s(#s(#s(#s(#s(#s(#0())))))))) ,#abs#(#pos(#s(#s(#s(#0())))))) 25: #cklt#(#EQ()) -> c_25() 26: #cklt#(#GT()) -> c_26() 27: #cklt#(#LT()) -> c_27() 28: #compare#(#0(),#0()) -> c_28() 29: #compare#(#0(),#neg(@y)) -> c_29() 30: #compare#(#0(),#pos(@y)) -> c_30() 31: #compare#(#0(),#s(@y)) -> c_31() 32: #compare#(#neg(@x),#0()) -> c_32() 33: #compare#(#neg(@x),#neg(@y)) -> c_33(#compare#(@y,@x)) 34: #compare#(#neg(@x),#pos(@y)) -> c_34() 35: #compare#(#pos(@x),#0()) -> c_35() 36: #compare#(#pos(@x),#neg(@y)) -> c_36() 37: #compare#(#pos(@x),#pos(@y)) -> c_37(#compare#(@x,@y)) 38: #compare#(#s(@x),#0()) -> c_38() 39: #compare#(#s(@x),#s(@y)) -> c_39(#compare#(@x,@y)) * Step 3: PredecessorEstimation WORST_CASE(?,O(n^3)) + Considered Problem: - Strict DPs: insert#(@x,@l) -> c_6(insert#1#(@l,@x)) insert#1#(::(@y,@ys),@x) -> c_7(insert#2#(#less(@y,@x),@x,@y,@ys),#less#(@y,@x)) insert#2#(#true(),@x,@y,@ys) -> c_10(insert#(@x,@ys)) insertD#(@x,@l) -> c_11(insertD#1#(@l,@x)) insertD#1#(::(@y,@ys),@x) -> c_12(insertD#2#(#less(@y,@x),@x,@y,@ys),#less#(@y,@x)) insertD#2#(#true(),@x,@y,@ys) -> c_15(insertD#(@x,@ys)) insertionsort#(@l) -> c_16(insertionsort#1#(@l)) insertionsort#1#(::(@x,@xs)) -> c_17(insert#(@x,insertionsort(@xs)),insertionsort#(@xs)) insertionsortD#(@l) -> c_19(insertionsortD#1#(@l)) insertionsortD#1#(::(@x,@xs)) -> c_20(insertD#(@x,insertionsortD(@xs)),insertionsortD#(@xs)) testInsertionsort#(@x) -> c_22(insertionsort#(testList(#unit())),testList#(#unit())) testInsertionsortD#(@x) -> c_23(insertionsortD#(testList(#unit())),testList#(#unit())) testList#(@_) -> c_24(#abs#(#0()) ,#abs#(#pos(#s(#s(#s(#s(#0())))))) ,#abs#(#pos(#s(#s(#s(#s(#s(#0()))))))) ,#abs#(#pos(#s(#s(#s(#s(#s(#s(#s(#s(#s(#0()))))))))))) ,#abs#(#pos(#s(#s(#s(#s(#s(#s(#s(#0()))))))))) ,#abs#(#pos(#s(#0()))) ,#abs#(#pos(#s(#s(#0())))) ,#abs#(#pos(#s(#s(#s(#s(#s(#s(#s(#s(#0())))))))))) ,#abs#(#pos(#s(#s(#s(#s(#s(#s(#0())))))))) ,#abs#(#pos(#s(#s(#s(#0())))))) - Weak DPs: #abs#(#0()) -> c_1() #abs#(#neg(@x)) -> c_2() #abs#(#pos(@x)) -> c_3() #abs#(#s(@x)) -> c_4() #cklt#(#EQ()) -> c_25() #cklt#(#GT()) -> c_26() #cklt#(#LT()) -> c_27() #compare#(#0(),#0()) -> c_28() #compare#(#0(),#neg(@y)) -> c_29() #compare#(#0(),#pos(@y)) -> c_30() #compare#(#0(),#s(@y)) -> c_31() #compare#(#neg(@x),#0()) -> c_32() #compare#(#neg(@x),#neg(@y)) -> c_33(#compare#(@y,@x)) #compare#(#neg(@x),#pos(@y)) -> c_34() #compare#(#pos(@x),#0()) -> c_35() #compare#(#pos(@x),#neg(@y)) -> c_36() #compare#(#pos(@x),#pos(@y)) -> c_37(#compare#(@x,@y)) #compare#(#s(@x),#0()) -> c_38() #compare#(#s(@x),#s(@y)) -> c_39(#compare#(@x,@y)) #less#(@x,@y) -> c_5(#cklt#(#compare(@x,@y)),#compare#(@x,@y)) insert#1#(nil(),@x) -> c_8() insert#2#(#false(),@x,@y,@ys) -> c_9() insertD#1#(nil(),@x) -> c_13() insertD#2#(#false(),@x,@y,@ys) -> c_14() insertionsort#1#(nil()) -> c_18() insertionsortD#1#(nil()) -> c_21() - Weak TRS: #abs(#0()) -> #0() #abs(#neg(@x)) -> #pos(@x) #abs(#pos(@x)) -> #pos(@x) #abs(#s(@x)) -> #pos(#s(@x)) #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) #less(@x,@y) -> #cklt(#compare(@x,@y)) insert(@x,@l) -> insert#1(@l,@x) insert#1(::(@y,@ys),@x) -> insert#2(#less(@y,@x),@x,@y,@ys) insert#1(nil(),@x) -> ::(@x,nil()) insert#2(#false(),@x,@y,@ys) -> ::(@x,::(@y,@ys)) insert#2(#true(),@x,@y,@ys) -> ::(@y,insert(@x,@ys)) insertD(@x,@l) -> insertD#1(@l,@x) insertD#1(::(@y,@ys),@x) -> insertD#2(#less(@y,@x),@x,@y,@ys) insertD#1(nil(),@x) -> ::(@x,nil()) insertD#2(#false(),@x,@y,@ys) -> ::(@x,::(@y,@ys)) insertD#2(#true(),@x,@y,@ys) -> ::(@y,insertD(@x,@ys)) insertionsort(@l) -> insertionsort#1(@l) insertionsort#1(::(@x,@xs)) -> insert(@x,insertionsort(@xs)) insertionsort#1(nil()) -> nil() insertionsortD(@l) -> insertionsortD#1(@l) insertionsortD#1(::(@x,@xs)) -> insertD(@x,insertionsortD(@xs)) insertionsortD#1(nil()) -> nil() testInsertionsort(@x) -> insertionsort(testList(#unit())) testInsertionsortD(@x) -> insertionsortD(testList(#unit())) testList(@_) -> ::(#abs(#0()) ,::(#abs(#pos(#s(#s(#s(#s(#0())))))) ,::(#abs(#pos(#s(#s(#s(#s(#s(#0()))))))) ,::(#abs(#pos(#s(#s(#s(#s(#s(#s(#s(#s(#s(#0()))))))))))) ,::(#abs(#pos(#s(#s(#s(#s(#s(#s(#s(#0()))))))))) ,::(#abs(#pos(#s(#0()))) ,::(#abs(#pos(#s(#s(#0())))) ,::(#abs(#pos(#s(#s(#s(#s(#s(#s(#s(#s(#0())))))))))) ,::(#abs(#pos(#s(#s(#s(#s(#s(#s(#0())))))))) ,::(#abs(#pos(#s(#s(#s(#0()))))),nil())))))))))) - Signature: {#abs/1,#cklt/1,#compare/2,#less/2,insert/2,insert#1/2,insert#2/4,insertD/2,insertD#1/2,insertD#2/4 ,insertionsort/1,insertionsort#1/1,insertionsortD/1,insertionsortD#1/1,testInsertionsort/1 ,testInsertionsortD/1,testList/1,#abs#/1,#cklt#/1,#compare#/2,#less#/2,insert#/2,insert#1#/2,insert#2#/4 ,insertD#/2,insertD#1#/2,insertD#2#/4,insertionsort#/1,insertionsort#1#/1,insertionsortD#/1 ,insertionsortD#1#/1,testInsertionsort#/1,testInsertionsortD#/1,testList#/1} / {#0/0,#EQ/0,#GT/0,#LT/0 ,#false/0,#neg/1,#pos/1,#s/1,#true/0,#unit/0,::/2,nil/0,c_1/0,c_2/0,c_3/0,c_4/0,c_5/2,c_6/1,c_7/2,c_8/0 ,c_9/0,c_10/1,c_11/1,c_12/2,c_13/0,c_14/0,c_15/1,c_16/1,c_17/2,c_18/0,c_19/1,c_20/2,c_21/0,c_22/2,c_23/2 ,c_24/10,c_25/0,c_26/0,c_27/0,c_28/0,c_29/0,c_30/0,c_31/0,c_32/0,c_33/1,c_34/0,c_35/0,c_36/0,c_37/1,c_38/0 ,c_39/1} - Obligation: innermost runtime complexity wrt. defined symbols {#abs#,#cklt#,#compare#,#less#,insert#,insert#1#,insert#2# ,insertD#,insertD#1#,insertD#2#,insertionsort#,insertionsort#1#,insertionsortD#,insertionsortD#1# ,testInsertionsort#,testInsertionsortD#,testList#} and constructors {#0,#EQ,#GT,#LT,#false,#neg,#pos,#s ,#true,#unit,::,nil} + Applied Processor: PredecessorEstimation {onSelection = all simple predecessor estimation selector} + Details: We estimate the number of application of {13} by application of Pre({13}) = {11,12}. Here rules are labelled as follows: 1: insert#(@x,@l) -> c_6(insert#1#(@l,@x)) 2: insert#1#(::(@y,@ys),@x) -> c_7(insert#2#(#less(@y,@x),@x,@y,@ys),#less#(@y,@x)) 3: insert#2#(#true(),@x,@y,@ys) -> c_10(insert#(@x,@ys)) 4: insertD#(@x,@l) -> c_11(insertD#1#(@l,@x)) 5: insertD#1#(::(@y,@ys),@x) -> c_12(insertD#2#(#less(@y,@x),@x,@y,@ys),#less#(@y,@x)) 6: insertD#2#(#true(),@x,@y,@ys) -> c_15(insertD#(@x,@ys)) 7: insertionsort#(@l) -> c_16(insertionsort#1#(@l)) 8: insertionsort#1#(::(@x,@xs)) -> c_17(insert#(@x,insertionsort(@xs)),insertionsort#(@xs)) 9: insertionsortD#(@l) -> c_19(insertionsortD#1#(@l)) 10: insertionsortD#1#(::(@x,@xs)) -> c_20(insertD#(@x,insertionsortD(@xs)),insertionsortD#(@xs)) 11: testInsertionsort#(@x) -> c_22(insertionsort#(testList(#unit())),testList#(#unit())) 12: testInsertionsortD#(@x) -> c_23(insertionsortD#(testList(#unit())),testList#(#unit())) 13: testList#(@_) -> c_24(#abs#(#0()) ,#abs#(#pos(#s(#s(#s(#s(#0())))))) ,#abs#(#pos(#s(#s(#s(#s(#s(#0()))))))) ,#abs#(#pos(#s(#s(#s(#s(#s(#s(#s(#s(#s(#0()))))))))))) ,#abs#(#pos(#s(#s(#s(#s(#s(#s(#s(#0()))))))))) ,#abs#(#pos(#s(#0()))) ,#abs#(#pos(#s(#s(#0())))) ,#abs#(#pos(#s(#s(#s(#s(#s(#s(#s(#s(#0())))))))))) ,#abs#(#pos(#s(#s(#s(#s(#s(#s(#0())))))))) ,#abs#(#pos(#s(#s(#s(#0())))))) 14: #abs#(#0()) -> c_1() 15: #abs#(#neg(@x)) -> c_2() 16: #abs#(#pos(@x)) -> c_3() 17: #abs#(#s(@x)) -> c_4() 18: #cklt#(#EQ()) -> c_25() 19: #cklt#(#GT()) -> c_26() 20: #cklt#(#LT()) -> c_27() 21: #compare#(#0(),#0()) -> c_28() 22: #compare#(#0(),#neg(@y)) -> c_29() 23: #compare#(#0(),#pos(@y)) -> c_30() 24: #compare#(#0(),#s(@y)) -> c_31() 25: #compare#(#neg(@x),#0()) -> c_32() 26: #compare#(#neg(@x),#neg(@y)) -> c_33(#compare#(@y,@x)) 27: #compare#(#neg(@x),#pos(@y)) -> c_34() 28: #compare#(#pos(@x),#0()) -> c_35() 29: #compare#(#pos(@x),#neg(@y)) -> c_36() 30: #compare#(#pos(@x),#pos(@y)) -> c_37(#compare#(@x,@y)) 31: #compare#(#s(@x),#0()) -> c_38() 32: #compare#(#s(@x),#s(@y)) -> c_39(#compare#(@x,@y)) 33: #less#(@x,@y) -> c_5(#cklt#(#compare(@x,@y)),#compare#(@x,@y)) 34: insert#1#(nil(),@x) -> c_8() 35: insert#2#(#false(),@x,@y,@ys) -> c_9() 36: insertD#1#(nil(),@x) -> c_13() 37: insertD#2#(#false(),@x,@y,@ys) -> c_14() 38: insertionsort#1#(nil()) -> c_18() 39: insertionsortD#1#(nil()) -> c_21() * Step 4: RemoveWeakSuffixes WORST_CASE(?,O(n^3)) + Considered Problem: - Strict DPs: insert#(@x,@l) -> c_6(insert#1#(@l,@x)) insert#1#(::(@y,@ys),@x) -> c_7(insert#2#(#less(@y,@x),@x,@y,@ys),#less#(@y,@x)) insert#2#(#true(),@x,@y,@ys) -> c_10(insert#(@x,@ys)) insertD#(@x,@l) -> c_11(insertD#1#(@l,@x)) insertD#1#(::(@y,@ys),@x) -> c_12(insertD#2#(#less(@y,@x),@x,@y,@ys),#less#(@y,@x)) insertD#2#(#true(),@x,@y,@ys) -> c_15(insertD#(@x,@ys)) insertionsort#(@l) -> c_16(insertionsort#1#(@l)) insertionsort#1#(::(@x,@xs)) -> c_17(insert#(@x,insertionsort(@xs)),insertionsort#(@xs)) insertionsortD#(@l) -> c_19(insertionsortD#1#(@l)) insertionsortD#1#(::(@x,@xs)) -> c_20(insertD#(@x,insertionsortD(@xs)),insertionsortD#(@xs)) testInsertionsort#(@x) -> c_22(insertionsort#(testList(#unit())),testList#(#unit())) testInsertionsortD#(@x) -> c_23(insertionsortD#(testList(#unit())),testList#(#unit())) - Weak DPs: #abs#(#0()) -> c_1() #abs#(#neg(@x)) -> c_2() #abs#(#pos(@x)) -> c_3() #abs#(#s(@x)) -> c_4() #cklt#(#EQ()) -> c_25() #cklt#(#GT()) -> c_26() #cklt#(#LT()) -> c_27() #compare#(#0(),#0()) -> c_28() #compare#(#0(),#neg(@y)) -> c_29() #compare#(#0(),#pos(@y)) -> c_30() #compare#(#0(),#s(@y)) -> c_31() #compare#(#neg(@x),#0()) -> c_32() #compare#(#neg(@x),#neg(@y)) -> c_33(#compare#(@y,@x)) #compare#(#neg(@x),#pos(@y)) -> c_34() #compare#(#pos(@x),#0()) -> c_35() #compare#(#pos(@x),#neg(@y)) -> c_36() #compare#(#pos(@x),#pos(@y)) -> c_37(#compare#(@x,@y)) #compare#(#s(@x),#0()) -> c_38() #compare#(#s(@x),#s(@y)) -> c_39(#compare#(@x,@y)) #less#(@x,@y) -> c_5(#cklt#(#compare(@x,@y)),#compare#(@x,@y)) insert#1#(nil(),@x) -> c_8() insert#2#(#false(),@x,@y,@ys) -> c_9() insertD#1#(nil(),@x) -> c_13() insertD#2#(#false(),@x,@y,@ys) -> c_14() insertionsort#1#(nil()) -> c_18() insertionsortD#1#(nil()) -> c_21() testList#(@_) -> c_24(#abs#(#0()) ,#abs#(#pos(#s(#s(#s(#s(#0())))))) ,#abs#(#pos(#s(#s(#s(#s(#s(#0()))))))) ,#abs#(#pos(#s(#s(#s(#s(#s(#s(#s(#s(#s(#0()))))))))))) ,#abs#(#pos(#s(#s(#s(#s(#s(#s(#s(#0()))))))))) ,#abs#(#pos(#s(#0()))) ,#abs#(#pos(#s(#s(#0())))) ,#abs#(#pos(#s(#s(#s(#s(#s(#s(#s(#s(#0())))))))))) ,#abs#(#pos(#s(#s(#s(#s(#s(#s(#0())))))))) ,#abs#(#pos(#s(#s(#s(#0())))))) - Weak TRS: #abs(#0()) -> #0() #abs(#neg(@x)) -> #pos(@x) #abs(#pos(@x)) -> #pos(@x) #abs(#s(@x)) -> #pos(#s(@x)) #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) #less(@x,@y) -> #cklt(#compare(@x,@y)) insert(@x,@l) -> insert#1(@l,@x) insert#1(::(@y,@ys),@x) -> insert#2(#less(@y,@x),@x,@y,@ys) insert#1(nil(),@x) -> ::(@x,nil()) insert#2(#false(),@x,@y,@ys) -> ::(@x,::(@y,@ys)) insert#2(#true(),@x,@y,@ys) -> ::(@y,insert(@x,@ys)) insertD(@x,@l) -> insertD#1(@l,@x) insertD#1(::(@y,@ys),@x) -> insertD#2(#less(@y,@x),@x,@y,@ys) insertD#1(nil(),@x) -> ::(@x,nil()) insertD#2(#false(),@x,@y,@ys) -> ::(@x,::(@y,@ys)) insertD#2(#true(),@x,@y,@ys) -> ::(@y,insertD(@x,@ys)) insertionsort(@l) -> insertionsort#1(@l) insertionsort#1(::(@x,@xs)) -> insert(@x,insertionsort(@xs)) insertionsort#1(nil()) -> nil() insertionsortD(@l) -> insertionsortD#1(@l) insertionsortD#1(::(@x,@xs)) -> insertD(@x,insertionsortD(@xs)) insertionsortD#1(nil()) -> nil() testInsertionsort(@x) -> insertionsort(testList(#unit())) testInsertionsortD(@x) -> insertionsortD(testList(#unit())) testList(@_) -> ::(#abs(#0()) ,::(#abs(#pos(#s(#s(#s(#s(#0())))))) ,::(#abs(#pos(#s(#s(#s(#s(#s(#0()))))))) ,::(#abs(#pos(#s(#s(#s(#s(#s(#s(#s(#s(#s(#0()))))))))))) ,::(#abs(#pos(#s(#s(#s(#s(#s(#s(#s(#0()))))))))) ,::(#abs(#pos(#s(#0()))) ,::(#abs(#pos(#s(#s(#0())))) ,::(#abs(#pos(#s(#s(#s(#s(#s(#s(#s(#s(#0())))))))))) ,::(#abs(#pos(#s(#s(#s(#s(#s(#s(#0())))))))) ,::(#abs(#pos(#s(#s(#s(#0()))))),nil())))))))))) - Signature: {#abs/1,#cklt/1,#compare/2,#less/2,insert/2,insert#1/2,insert#2/4,insertD/2,insertD#1/2,insertD#2/4 ,insertionsort/1,insertionsort#1/1,insertionsortD/1,insertionsortD#1/1,testInsertionsort/1 ,testInsertionsortD/1,testList/1,#abs#/1,#cklt#/1,#compare#/2,#less#/2,insert#/2,insert#1#/2,insert#2#/4 ,insertD#/2,insertD#1#/2,insertD#2#/4,insertionsort#/1,insertionsort#1#/1,insertionsortD#/1 ,insertionsortD#1#/1,testInsertionsort#/1,testInsertionsortD#/1,testList#/1} / {#0/0,#EQ/0,#GT/0,#LT/0 ,#false/0,#neg/1,#pos/1,#s/1,#true/0,#unit/0,::/2,nil/0,c_1/0,c_2/0,c_3/0,c_4/0,c_5/2,c_6/1,c_7/2,c_8/0 ,c_9/0,c_10/1,c_11/1,c_12/2,c_13/0,c_14/0,c_15/1,c_16/1,c_17/2,c_18/0,c_19/1,c_20/2,c_21/0,c_22/2,c_23/2 ,c_24/10,c_25/0,c_26/0,c_27/0,c_28/0,c_29/0,c_30/0,c_31/0,c_32/0,c_33/1,c_34/0,c_35/0,c_36/0,c_37/1,c_38/0 ,c_39/1} - Obligation: innermost runtime complexity wrt. defined symbols {#abs#,#cklt#,#compare#,#less#,insert#,insert#1#,insert#2# ,insertD#,insertD#1#,insertD#2#,insertionsort#,insertionsort#1#,insertionsortD#,insertionsortD#1# ,testInsertionsort#,testInsertionsortD#,testList#} and constructors {#0,#EQ,#GT,#LT,#false,#neg,#pos,#s ,#true,#unit,::,nil} + Applied Processor: RemoveWeakSuffixes + Details: Consider the dependency graph 1:S:insert#(@x,@l) -> c_6(insert#1#(@l,@x)) -->_1 insert#1#(::(@y,@ys),@x) -> c_7(insert#2#(#less(@y,@x),@x,@y,@ys),#less#(@y,@x)):2 -->_1 insert#1#(nil(),@x) -> c_8():33 2:S:insert#1#(::(@y,@ys),@x) -> c_7(insert#2#(#less(@y,@x),@x,@y,@ys),#less#(@y,@x)) -->_2 #less#(@x,@y) -> c_5(#cklt#(#compare(@x,@y)),#compare#(@x,@y)):32 -->_1 insert#2#(#true(),@x,@y,@ys) -> c_10(insert#(@x,@ys)):3 -->_1 insert#2#(#false(),@x,@y,@ys) -> c_9():34 3:S:insert#2#(#true(),@x,@y,@ys) -> c_10(insert#(@x,@ys)) -->_1 insert#(@x,@l) -> c_6(insert#1#(@l,@x)):1 4:S:insertD#(@x,@l) -> c_11(insertD#1#(@l,@x)) -->_1 insertD#1#(::(@y,@ys),@x) -> c_12(insertD#2#(#less(@y,@x),@x,@y,@ys),#less#(@y,@x)):5 -->_1 insertD#1#(nil(),@x) -> c_13():35 5:S:insertD#1#(::(@y,@ys),@x) -> c_12(insertD#2#(#less(@y,@x),@x,@y,@ys),#less#(@y,@x)) -->_2 #less#(@x,@y) -> c_5(#cklt#(#compare(@x,@y)),#compare#(@x,@y)):32 -->_1 insertD#2#(#true(),@x,@y,@ys) -> c_15(insertD#(@x,@ys)):6 -->_1 insertD#2#(#false(),@x,@y,@ys) -> c_14():36 6:S:insertD#2#(#true(),@x,@y,@ys) -> c_15(insertD#(@x,@ys)) -->_1 insertD#(@x,@l) -> c_11(insertD#1#(@l,@x)):4 7:S:insertionsort#(@l) -> c_16(insertionsort#1#(@l)) -->_1 insertionsort#1#(::(@x,@xs)) -> c_17(insert#(@x,insertionsort(@xs)),insertionsort#(@xs)):8 -->_1 insertionsort#1#(nil()) -> c_18():37 8:S:insertionsort#1#(::(@x,@xs)) -> c_17(insert#(@x,insertionsort(@xs)),insertionsort#(@xs)) -->_2 insertionsort#(@l) -> c_16(insertionsort#1#(@l)):7 -->_1 insert#(@x,@l) -> c_6(insert#1#(@l,@x)):1 9:S:insertionsortD#(@l) -> c_19(insertionsortD#1#(@l)) -->_1 insertionsortD#1#(::(@x,@xs)) -> c_20(insertD#(@x,insertionsortD(@xs)),insertionsortD#(@xs)):10 -->_1 insertionsortD#1#(nil()) -> c_21():38 10:S:insertionsortD#1#(::(@x,@xs)) -> c_20(insertD#(@x,insertionsortD(@xs)),insertionsortD#(@xs)) -->_2 insertionsortD#(@l) -> c_19(insertionsortD#1#(@l)):9 -->_1 insertD#(@x,@l) -> c_11(insertD#1#(@l,@x)):4 11:S:testInsertionsort#(@x) -> c_22(insertionsort#(testList(#unit())),testList#(#unit())) -->_2 testList#(@_) -> c_24(#abs#(#0()) ,#abs#(#pos(#s(#s(#s(#s(#0())))))) ,#abs#(#pos(#s(#s(#s(#s(#s(#0()))))))) ,#abs#(#pos(#s(#s(#s(#s(#s(#s(#s(#s(#s(#0()))))))))))) ,#abs#(#pos(#s(#s(#s(#s(#s(#s(#s(#0()))))))))) ,#abs#(#pos(#s(#0()))) ,#abs#(#pos(#s(#s(#0())))) ,#abs#(#pos(#s(#s(#s(#s(#s(#s(#s(#s(#0())))))))))) ,#abs#(#pos(#s(#s(#s(#s(#s(#s(#0())))))))) ,#abs#(#pos(#s(#s(#s(#0())))))):39 -->_1 insertionsort#(@l) -> c_16(insertionsort#1#(@l)):7 12:S:testInsertionsortD#(@x) -> c_23(insertionsortD#(testList(#unit())),testList#(#unit())) -->_2 testList#(@_) -> c_24(#abs#(#0()) ,#abs#(#pos(#s(#s(#s(#s(#0())))))) ,#abs#(#pos(#s(#s(#s(#s(#s(#0()))))))) ,#abs#(#pos(#s(#s(#s(#s(#s(#s(#s(#s(#s(#0()))))))))))) ,#abs#(#pos(#s(#s(#s(#s(#s(#s(#s(#0()))))))))) ,#abs#(#pos(#s(#0()))) ,#abs#(#pos(#s(#s(#0())))) ,#abs#(#pos(#s(#s(#s(#s(#s(#s(#s(#s(#0())))))))))) ,#abs#(#pos(#s(#s(#s(#s(#s(#s(#0())))))))) ,#abs#(#pos(#s(#s(#s(#0())))))):39 -->_1 insertionsortD#(@l) -> c_19(insertionsortD#1#(@l)):9 13:W:#abs#(#0()) -> c_1() 14:W:#abs#(#neg(@x)) -> c_2() 15:W:#abs#(#pos(@x)) -> c_3() 16:W:#abs#(#s(@x)) -> c_4() 17:W:#cklt#(#EQ()) -> c_25() 18:W:#cklt#(#GT()) -> c_26() 19:W:#cklt#(#LT()) -> c_27() 20:W:#compare#(#0(),#0()) -> c_28() 21:W:#compare#(#0(),#neg(@y)) -> c_29() 22:W:#compare#(#0(),#pos(@y)) -> c_30() 23:W:#compare#(#0(),#s(@y)) -> c_31() 24:W:#compare#(#neg(@x),#0()) -> c_32() 25:W:#compare#(#neg(@x),#neg(@y)) -> c_33(#compare#(@y,@x)) -->_1 #compare#(#s(@x),#s(@y)) -> c_39(#compare#(@x,@y)):31 -->_1 #compare#(#pos(@x),#pos(@y)) -> c_37(#compare#(@x,@y)):29 -->_1 #compare#(#s(@x),#0()) -> c_38():30 -->_1 #compare#(#pos(@x),#neg(@y)) -> c_36():28 -->_1 #compare#(#pos(@x),#0()) -> c_35():27 -->_1 #compare#(#neg(@x),#pos(@y)) -> c_34():26 -->_1 #compare#(#neg(@x),#neg(@y)) -> c_33(#compare#(@y,@x)):25 -->_1 #compare#(#neg(@x),#0()) -> c_32():24 -->_1 #compare#(#0(),#s(@y)) -> c_31():23 -->_1 #compare#(#0(),#pos(@y)) -> c_30():22 -->_1 #compare#(#0(),#neg(@y)) -> c_29():21 -->_1 #compare#(#0(),#0()) -> c_28():20 26:W:#compare#(#neg(@x),#pos(@y)) -> c_34() 27:W:#compare#(#pos(@x),#0()) -> c_35() 28:W:#compare#(#pos(@x),#neg(@y)) -> c_36() 29:W:#compare#(#pos(@x),#pos(@y)) -> c_37(#compare#(@x,@y)) -->_1 #compare#(#s(@x),#s(@y)) -> c_39(#compare#(@x,@y)):31 -->_1 #compare#(#s(@x),#0()) -> c_38():30 -->_1 #compare#(#pos(@x),#pos(@y)) -> c_37(#compare#(@x,@y)):29 -->_1 #compare#(#pos(@x),#neg(@y)) -> c_36():28 -->_1 #compare#(#pos(@x),#0()) -> c_35():27 -->_1 #compare#(#neg(@x),#pos(@y)) -> c_34():26 -->_1 #compare#(#neg(@x),#neg(@y)) -> c_33(#compare#(@y,@x)):25 -->_1 #compare#(#neg(@x),#0()) -> c_32():24 -->_1 #compare#(#0(),#s(@y)) -> c_31():23 -->_1 #compare#(#0(),#pos(@y)) -> c_30():22 -->_1 #compare#(#0(),#neg(@y)) -> c_29():21 -->_1 #compare#(#0(),#0()) -> c_28():20 30:W:#compare#(#s(@x),#0()) -> c_38() 31:W:#compare#(#s(@x),#s(@y)) -> c_39(#compare#(@x,@y)) -->_1 #compare#(#s(@x),#s(@y)) -> c_39(#compare#(@x,@y)):31 -->_1 #compare#(#s(@x),#0()) -> c_38():30 -->_1 #compare#(#pos(@x),#pos(@y)) -> c_37(#compare#(@x,@y)):29 -->_1 #compare#(#pos(@x),#neg(@y)) -> c_36():28 -->_1 #compare#(#pos(@x),#0()) -> c_35():27 -->_1 #compare#(#neg(@x),#pos(@y)) -> c_34():26 -->_1 #compare#(#neg(@x),#neg(@y)) -> c_33(#compare#(@y,@x)):25 -->_1 #compare#(#neg(@x),#0()) -> c_32():24 -->_1 #compare#(#0(),#s(@y)) -> c_31():23 -->_1 #compare#(#0(),#pos(@y)) -> c_30():22 -->_1 #compare#(#0(),#neg(@y)) -> c_29():21 -->_1 #compare#(#0(),#0()) -> c_28():20 32:W:#less#(@x,@y) -> c_5(#cklt#(#compare(@x,@y)),#compare#(@x,@y)) -->_2 #compare#(#s(@x),#s(@y)) -> c_39(#compare#(@x,@y)):31 -->_2 #compare#(#s(@x),#0()) -> c_38():30 -->_2 #compare#(#pos(@x),#pos(@y)) -> c_37(#compare#(@x,@y)):29 -->_2 #compare#(#pos(@x),#neg(@y)) -> c_36():28 -->_2 #compare#(#pos(@x),#0()) -> c_35():27 -->_2 #compare#(#neg(@x),#pos(@y)) -> c_34():26 -->_2 #compare#(#neg(@x),#neg(@y)) -> c_33(#compare#(@y,@x)):25 -->_2 #compare#(#neg(@x),#0()) -> c_32():24 -->_2 #compare#(#0(),#s(@y)) -> c_31():23 -->_2 #compare#(#0(),#pos(@y)) -> c_30():22 -->_2 #compare#(#0(),#neg(@y)) -> c_29():21 -->_2 #compare#(#0(),#0()) -> c_28():20 -->_1 #cklt#(#LT()) -> c_27():19 -->_1 #cklt#(#GT()) -> c_26():18 -->_1 #cklt#(#EQ()) -> c_25():17 33:W:insert#1#(nil(),@x) -> c_8() 34:W:insert#2#(#false(),@x,@y,@ys) -> c_9() 35:W:insertD#1#(nil(),@x) -> c_13() 36:W:insertD#2#(#false(),@x,@y,@ys) -> c_14() 37:W:insertionsort#1#(nil()) -> c_18() 38:W:insertionsortD#1#(nil()) -> c_21() 39:W:testList#(@_) -> c_24(#abs#(#0()) ,#abs#(#pos(#s(#s(#s(#s(#0())))))) ,#abs#(#pos(#s(#s(#s(#s(#s(#0()))))))) ,#abs#(#pos(#s(#s(#s(#s(#s(#s(#s(#s(#s(#0()))))))))))) ,#abs#(#pos(#s(#s(#s(#s(#s(#s(#s(#0()))))))))) ,#abs#(#pos(#s(#0()))) ,#abs#(#pos(#s(#s(#0())))) ,#abs#(#pos(#s(#s(#s(#s(#s(#s(#s(#s(#0())))))))))) ,#abs#(#pos(#s(#s(#s(#s(#s(#s(#0())))))))) ,#abs#(#pos(#s(#s(#s(#0())))))) -->_10 #abs#(#pos(@x)) -> c_3():15 -->_9 #abs#(#pos(@x)) -> c_3():15 -->_8 #abs#(#pos(@x)) -> c_3():15 -->_7 #abs#(#pos(@x)) -> c_3():15 -->_6 #abs#(#pos(@x)) -> c_3():15 -->_5 #abs#(#pos(@x)) -> c_3():15 -->_4 #abs#(#pos(@x)) -> c_3():15 -->_3 #abs#(#pos(@x)) -> c_3():15 -->_2 #abs#(#pos(@x)) -> c_3():15 -->_1 #abs#(#0()) -> c_1():13 The following weak DPs constitute a sub-graph of the DG that is closed under successors. The DPs are removed. 16: #abs#(#s(@x)) -> c_4() 14: #abs#(#neg(@x)) -> c_2() 39: testList#(@_) -> c_24(#abs#(#0()) ,#abs#(#pos(#s(#s(#s(#s(#0())))))) ,#abs#(#pos(#s(#s(#s(#s(#s(#0()))))))) ,#abs#(#pos(#s(#s(#s(#s(#s(#s(#s(#s(#s(#0()))))))))))) ,#abs#(#pos(#s(#s(#s(#s(#s(#s(#s(#0()))))))))) ,#abs#(#pos(#s(#0()))) ,#abs#(#pos(#s(#s(#0())))) ,#abs#(#pos(#s(#s(#s(#s(#s(#s(#s(#s(#0())))))))))) ,#abs#(#pos(#s(#s(#s(#s(#s(#s(#0())))))))) ,#abs#(#pos(#s(#s(#s(#0())))))) 13: #abs#(#0()) -> c_1() 15: #abs#(#pos(@x)) -> c_3() 38: insertionsortD#1#(nil()) -> c_21() 37: insertionsort#1#(nil()) -> c_18() 35: insertD#1#(nil(),@x) -> c_13() 36: insertD#2#(#false(),@x,@y,@ys) -> c_14() 33: insert#1#(nil(),@x) -> c_8() 34: insert#2#(#false(),@x,@y,@ys) -> c_9() 32: #less#(@x,@y) -> c_5(#cklt#(#compare(@x,@y)),#compare#(@x,@y)) 17: #cklt#(#EQ()) -> c_25() 18: #cklt#(#GT()) -> c_26() 19: #cklt#(#LT()) -> c_27() 31: #compare#(#s(@x),#s(@y)) -> c_39(#compare#(@x,@y)) 29: #compare#(#pos(@x),#pos(@y)) -> c_37(#compare#(@x,@y)) 25: #compare#(#neg(@x),#neg(@y)) -> c_33(#compare#(@y,@x)) 20: #compare#(#0(),#0()) -> c_28() 21: #compare#(#0(),#neg(@y)) -> c_29() 22: #compare#(#0(),#pos(@y)) -> c_30() 23: #compare#(#0(),#s(@y)) -> c_31() 24: #compare#(#neg(@x),#0()) -> c_32() 26: #compare#(#neg(@x),#pos(@y)) -> c_34() 27: #compare#(#pos(@x),#0()) -> c_35() 28: #compare#(#pos(@x),#neg(@y)) -> c_36() 30: #compare#(#s(@x),#0()) -> c_38() * Step 5: SimplifyRHS WORST_CASE(?,O(n^3)) + Considered Problem: - Strict DPs: insert#(@x,@l) -> c_6(insert#1#(@l,@x)) insert#1#(::(@y,@ys),@x) -> c_7(insert#2#(#less(@y,@x),@x,@y,@ys),#less#(@y,@x)) insert#2#(#true(),@x,@y,@ys) -> c_10(insert#(@x,@ys)) insertD#(@x,@l) -> c_11(insertD#1#(@l,@x)) insertD#1#(::(@y,@ys),@x) -> c_12(insertD#2#(#less(@y,@x),@x,@y,@ys),#less#(@y,@x)) insertD#2#(#true(),@x,@y,@ys) -> c_15(insertD#(@x,@ys)) insertionsort#(@l) -> c_16(insertionsort#1#(@l)) insertionsort#1#(::(@x,@xs)) -> c_17(insert#(@x,insertionsort(@xs)),insertionsort#(@xs)) insertionsortD#(@l) -> c_19(insertionsortD#1#(@l)) insertionsortD#1#(::(@x,@xs)) -> c_20(insertD#(@x,insertionsortD(@xs)),insertionsortD#(@xs)) testInsertionsort#(@x) -> c_22(insertionsort#(testList(#unit())),testList#(#unit())) testInsertionsortD#(@x) -> c_23(insertionsortD#(testList(#unit())),testList#(#unit())) - Weak TRS: #abs(#0()) -> #0() #abs(#neg(@x)) -> #pos(@x) #abs(#pos(@x)) -> #pos(@x) #abs(#s(@x)) -> #pos(#s(@x)) #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) #less(@x,@y) -> #cklt(#compare(@x,@y)) insert(@x,@l) -> insert#1(@l,@x) insert#1(::(@y,@ys),@x) -> insert#2(#less(@y,@x),@x,@y,@ys) insert#1(nil(),@x) -> ::(@x,nil()) insert#2(#false(),@x,@y,@ys) -> ::(@x,::(@y,@ys)) insert#2(#true(),@x,@y,@ys) -> ::(@y,insert(@x,@ys)) insertD(@x,@l) -> insertD#1(@l,@x) insertD#1(::(@y,@ys),@x) -> insertD#2(#less(@y,@x),@x,@y,@ys) insertD#1(nil(),@x) -> ::(@x,nil()) insertD#2(#false(),@x,@y,@ys) -> ::(@x,::(@y,@ys)) insertD#2(#true(),@x,@y,@ys) -> ::(@y,insertD(@x,@ys)) insertionsort(@l) -> insertionsort#1(@l) insertionsort#1(::(@x,@xs)) -> insert(@x,insertionsort(@xs)) insertionsort#1(nil()) -> nil() insertionsortD(@l) -> insertionsortD#1(@l) insertionsortD#1(::(@x,@xs)) -> insertD(@x,insertionsortD(@xs)) insertionsortD#1(nil()) -> nil() testInsertionsort(@x) -> insertionsort(testList(#unit())) testInsertionsortD(@x) -> insertionsortD(testList(#unit())) testList(@_) -> ::(#abs(#0()) ,::(#abs(#pos(#s(#s(#s(#s(#0())))))) ,::(#abs(#pos(#s(#s(#s(#s(#s(#0()))))))) ,::(#abs(#pos(#s(#s(#s(#s(#s(#s(#s(#s(#s(#0()))))))))))) ,::(#abs(#pos(#s(#s(#s(#s(#s(#s(#s(#0()))))))))) ,::(#abs(#pos(#s(#0()))) ,::(#abs(#pos(#s(#s(#0())))) ,::(#abs(#pos(#s(#s(#s(#s(#s(#s(#s(#s(#0())))))))))) ,::(#abs(#pos(#s(#s(#s(#s(#s(#s(#0())))))))) ,::(#abs(#pos(#s(#s(#s(#0()))))),nil())))))))))) - Signature: {#abs/1,#cklt/1,#compare/2,#less/2,insert/2,insert#1/2,insert#2/4,insertD/2,insertD#1/2,insertD#2/4 ,insertionsort/1,insertionsort#1/1,insertionsortD/1,insertionsortD#1/1,testInsertionsort/1 ,testInsertionsortD/1,testList/1,#abs#/1,#cklt#/1,#compare#/2,#less#/2,insert#/2,insert#1#/2,insert#2#/4 ,insertD#/2,insertD#1#/2,insertD#2#/4,insertionsort#/1,insertionsort#1#/1,insertionsortD#/1 ,insertionsortD#1#/1,testInsertionsort#/1,testInsertionsortD#/1,testList#/1} / {#0/0,#EQ/0,#GT/0,#LT/0 ,#false/0,#neg/1,#pos/1,#s/1,#true/0,#unit/0,::/2,nil/0,c_1/0,c_2/0,c_3/0,c_4/0,c_5/2,c_6/1,c_7/2,c_8/0 ,c_9/0,c_10/1,c_11/1,c_12/2,c_13/0,c_14/0,c_15/1,c_16/1,c_17/2,c_18/0,c_19/1,c_20/2,c_21/0,c_22/2,c_23/2 ,c_24/10,c_25/0,c_26/0,c_27/0,c_28/0,c_29/0,c_30/0,c_31/0,c_32/0,c_33/1,c_34/0,c_35/0,c_36/0,c_37/1,c_38/0 ,c_39/1} - Obligation: innermost runtime complexity wrt. defined symbols {#abs#,#cklt#,#compare#,#less#,insert#,insert#1#,insert#2# ,insertD#,insertD#1#,insertD#2#,insertionsort#,insertionsort#1#,insertionsortD#,insertionsortD#1# ,testInsertionsort#,testInsertionsortD#,testList#} and constructors {#0,#EQ,#GT,#LT,#false,#neg,#pos,#s ,#true,#unit,::,nil} + Applied Processor: SimplifyRHS + Details: Consider the dependency graph 1:S:insert#(@x,@l) -> c_6(insert#1#(@l,@x)) -->_1 insert#1#(::(@y,@ys),@x) -> c_7(insert#2#(#less(@y,@x),@x,@y,@ys),#less#(@y,@x)):2 2:S:insert#1#(::(@y,@ys),@x) -> c_7(insert#2#(#less(@y,@x),@x,@y,@ys),#less#(@y,@x)) -->_1 insert#2#(#true(),@x,@y,@ys) -> c_10(insert#(@x,@ys)):3 3:S:insert#2#(#true(),@x,@y,@ys) -> c_10(insert#(@x,@ys)) -->_1 insert#(@x,@l) -> c_6(insert#1#(@l,@x)):1 4:S:insertD#(@x,@l) -> c_11(insertD#1#(@l,@x)) -->_1 insertD#1#(::(@y,@ys),@x) -> c_12(insertD#2#(#less(@y,@x),@x,@y,@ys),#less#(@y,@x)):5 5:S:insertD#1#(::(@y,@ys),@x) -> c_12(insertD#2#(#less(@y,@x),@x,@y,@ys),#less#(@y,@x)) -->_1 insertD#2#(#true(),@x,@y,@ys) -> c_15(insertD#(@x,@ys)):6 6:S:insertD#2#(#true(),@x,@y,@ys) -> c_15(insertD#(@x,@ys)) -->_1 insertD#(@x,@l) -> c_11(insertD#1#(@l,@x)):4 7:S:insertionsort#(@l) -> c_16(insertionsort#1#(@l)) -->_1 insertionsort#1#(::(@x,@xs)) -> c_17(insert#(@x,insertionsort(@xs)),insertionsort#(@xs)):8 8:S:insertionsort#1#(::(@x,@xs)) -> c_17(insert#(@x,insertionsort(@xs)),insertionsort#(@xs)) -->_2 insertionsort#(@l) -> c_16(insertionsort#1#(@l)):7 -->_1 insert#(@x,@l) -> c_6(insert#1#(@l,@x)):1 9:S:insertionsortD#(@l) -> c_19(insertionsortD#1#(@l)) -->_1 insertionsortD#1#(::(@x,@xs)) -> c_20(insertD#(@x,insertionsortD(@xs)),insertionsortD#(@xs)):10 10:S:insertionsortD#1#(::(@x,@xs)) -> c_20(insertD#(@x,insertionsortD(@xs)),insertionsortD#(@xs)) -->_2 insertionsortD#(@l) -> c_19(insertionsortD#1#(@l)):9 -->_1 insertD#(@x,@l) -> c_11(insertD#1#(@l,@x)):4 11:S:testInsertionsort#(@x) -> c_22(insertionsort#(testList(#unit())),testList#(#unit())) -->_1 insertionsort#(@l) -> c_16(insertionsort#1#(@l)):7 12:S:testInsertionsortD#(@x) -> c_23(insertionsortD#(testList(#unit())),testList#(#unit())) -->_1 insertionsortD#(@l) -> c_19(insertionsortD#1#(@l)):9 Due to missing edges in the depndency graph, the right-hand sides of following rules could be simplified: insert#1#(::(@y,@ys),@x) -> c_7(insert#2#(#less(@y,@x),@x,@y,@ys)) insertD#1#(::(@y,@ys),@x) -> c_12(insertD#2#(#less(@y,@x),@x,@y,@ys)) testInsertionsort#(@x) -> c_22(insertionsort#(testList(#unit()))) testInsertionsortD#(@x) -> c_23(insertionsortD#(testList(#unit()))) * Step 6: UsableRules WORST_CASE(?,O(n^3)) + Considered Problem: - Strict DPs: insert#(@x,@l) -> c_6(insert#1#(@l,@x)) insert#1#(::(@y,@ys),@x) -> c_7(insert#2#(#less(@y,@x),@x,@y,@ys)) insert#2#(#true(),@x,@y,@ys) -> c_10(insert#(@x,@ys)) insertD#(@x,@l) -> c_11(insertD#1#(@l,@x)) insertD#1#(::(@y,@ys),@x) -> c_12(insertD#2#(#less(@y,@x),@x,@y,@ys)) insertD#2#(#true(),@x,@y,@ys) -> c_15(insertD#(@x,@ys)) insertionsort#(@l) -> c_16(insertionsort#1#(@l)) insertionsort#1#(::(@x,@xs)) -> c_17(insert#(@x,insertionsort(@xs)),insertionsort#(@xs)) insertionsortD#(@l) -> c_19(insertionsortD#1#(@l)) insertionsortD#1#(::(@x,@xs)) -> c_20(insertD#(@x,insertionsortD(@xs)),insertionsortD#(@xs)) testInsertionsort#(@x) -> c_22(insertionsort#(testList(#unit()))) testInsertionsortD#(@x) -> c_23(insertionsortD#(testList(#unit()))) - Weak TRS: #abs(#0()) -> #0() #abs(#neg(@x)) -> #pos(@x) #abs(#pos(@x)) -> #pos(@x) #abs(#s(@x)) -> #pos(#s(@x)) #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) #less(@x,@y) -> #cklt(#compare(@x,@y)) insert(@x,@l) -> insert#1(@l,@x) insert#1(::(@y,@ys),@x) -> insert#2(#less(@y,@x),@x,@y,@ys) insert#1(nil(),@x) -> ::(@x,nil()) insert#2(#false(),@x,@y,@ys) -> ::(@x,::(@y,@ys)) insert#2(#true(),@x,@y,@ys) -> ::(@y,insert(@x,@ys)) insertD(@x,@l) -> insertD#1(@l,@x) insertD#1(::(@y,@ys),@x) -> insertD#2(#less(@y,@x),@x,@y,@ys) insertD#1(nil(),@x) -> ::(@x,nil()) insertD#2(#false(),@x,@y,@ys) -> ::(@x,::(@y,@ys)) insertD#2(#true(),@x,@y,@ys) -> ::(@y,insertD(@x,@ys)) insertionsort(@l) -> insertionsort#1(@l) insertionsort#1(::(@x,@xs)) -> insert(@x,insertionsort(@xs)) insertionsort#1(nil()) -> nil() insertionsortD(@l) -> insertionsortD#1(@l) insertionsortD#1(::(@x,@xs)) -> insertD(@x,insertionsortD(@xs)) insertionsortD#1(nil()) -> nil() testInsertionsort(@x) -> insertionsort(testList(#unit())) testInsertionsortD(@x) -> insertionsortD(testList(#unit())) testList(@_) -> ::(#abs(#0()) ,::(#abs(#pos(#s(#s(#s(#s(#0())))))) ,::(#abs(#pos(#s(#s(#s(#s(#s(#0()))))))) ,::(#abs(#pos(#s(#s(#s(#s(#s(#s(#s(#s(#s(#0()))))))))))) ,::(#abs(#pos(#s(#s(#s(#s(#s(#s(#s(#0()))))))))) ,::(#abs(#pos(#s(#0()))) ,::(#abs(#pos(#s(#s(#0())))) ,::(#abs(#pos(#s(#s(#s(#s(#s(#s(#s(#s(#0())))))))))) ,::(#abs(#pos(#s(#s(#s(#s(#s(#s(#0())))))))) ,::(#abs(#pos(#s(#s(#s(#0()))))),nil())))))))))) - Signature: {#abs/1,#cklt/1,#compare/2,#less/2,insert/2,insert#1/2,insert#2/4,insertD/2,insertD#1/2,insertD#2/4 ,insertionsort/1,insertionsort#1/1,insertionsortD/1,insertionsortD#1/1,testInsertionsort/1 ,testInsertionsortD/1,testList/1,#abs#/1,#cklt#/1,#compare#/2,#less#/2,insert#/2,insert#1#/2,insert#2#/4 ,insertD#/2,insertD#1#/2,insertD#2#/4,insertionsort#/1,insertionsort#1#/1,insertionsortD#/1 ,insertionsortD#1#/1,testInsertionsort#/1,testInsertionsortD#/1,testList#/1} / {#0/0,#EQ/0,#GT/0,#LT/0 ,#false/0,#neg/1,#pos/1,#s/1,#true/0,#unit/0,::/2,nil/0,c_1/0,c_2/0,c_3/0,c_4/0,c_5/2,c_6/1,c_7/1,c_8/0 ,c_9/0,c_10/1,c_11/1,c_12/1,c_13/0,c_14/0,c_15/1,c_16/1,c_17/2,c_18/0,c_19/1,c_20/2,c_21/0,c_22/1,c_23/1 ,c_24/10,c_25/0,c_26/0,c_27/0,c_28/0,c_29/0,c_30/0,c_31/0,c_32/0,c_33/1,c_34/0,c_35/0,c_36/0,c_37/1,c_38/0 ,c_39/1} - Obligation: innermost runtime complexity wrt. defined symbols {#abs#,#cklt#,#compare#,#less#,insert#,insert#1#,insert#2# ,insertD#,insertD#1#,insertD#2#,insertionsort#,insertionsort#1#,insertionsortD#,insertionsortD#1# ,testInsertionsort#,testInsertionsortD#,testList#} and constructors {#0,#EQ,#GT,#LT,#false,#neg,#pos,#s ,#true,#unit,::,nil} + Applied Processor: UsableRules + Details: We replace rewrite rules by usable rules: #abs(#0()) -> #0() #abs(#pos(@x)) -> #pos(@x) #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) #less(@x,@y) -> #cklt(#compare(@x,@y)) insert(@x,@l) -> insert#1(@l,@x) insert#1(::(@y,@ys),@x) -> insert#2(#less(@y,@x),@x,@y,@ys) insert#1(nil(),@x) -> ::(@x,nil()) insert#2(#false(),@x,@y,@ys) -> ::(@x,::(@y,@ys)) insert#2(#true(),@x,@y,@ys) -> ::(@y,insert(@x,@ys)) insertD(@x,@l) -> insertD#1(@l,@x) insertD#1(::(@y,@ys),@x) -> insertD#2(#less(@y,@x),@x,@y,@ys) insertD#1(nil(),@x) -> ::(@x,nil()) insertD#2(#false(),@x,@y,@ys) -> ::(@x,::(@y,@ys)) insertD#2(#true(),@x,@y,@ys) -> ::(@y,insertD(@x,@ys)) insertionsort(@l) -> insertionsort#1(@l) insertionsort#1(::(@x,@xs)) -> insert(@x,insertionsort(@xs)) insertionsort#1(nil()) -> nil() insertionsortD(@l) -> insertionsortD#1(@l) insertionsortD#1(::(@x,@xs)) -> insertD(@x,insertionsortD(@xs)) insertionsortD#1(nil()) -> nil() testList(@_) -> ::(#abs(#0()) ,::(#abs(#pos(#s(#s(#s(#s(#0())))))) ,::(#abs(#pos(#s(#s(#s(#s(#s(#0()))))))) ,::(#abs(#pos(#s(#s(#s(#s(#s(#s(#s(#s(#s(#0()))))))))))) ,::(#abs(#pos(#s(#s(#s(#s(#s(#s(#s(#0()))))))))) ,::(#abs(#pos(#s(#0()))) ,::(#abs(#pos(#s(#s(#0())))) ,::(#abs(#pos(#s(#s(#s(#s(#s(#s(#s(#s(#0())))))))))) ,::(#abs(#pos(#s(#s(#s(#s(#s(#s(#0())))))))) ,::(#abs(#pos(#s(#s(#s(#0()))))),nil())))))))))) insert#(@x,@l) -> c_6(insert#1#(@l,@x)) insert#1#(::(@y,@ys),@x) -> c_7(insert#2#(#less(@y,@x),@x,@y,@ys)) insert#2#(#true(),@x,@y,@ys) -> c_10(insert#(@x,@ys)) insertD#(@x,@l) -> c_11(insertD#1#(@l,@x)) insertD#1#(::(@y,@ys),@x) -> c_12(insertD#2#(#less(@y,@x),@x,@y,@ys)) insertD#2#(#true(),@x,@y,@ys) -> c_15(insertD#(@x,@ys)) insertionsort#(@l) -> c_16(insertionsort#1#(@l)) insertionsort#1#(::(@x,@xs)) -> c_17(insert#(@x,insertionsort(@xs)),insertionsort#(@xs)) insertionsortD#(@l) -> c_19(insertionsortD#1#(@l)) insertionsortD#1#(::(@x,@xs)) -> c_20(insertD#(@x,insertionsortD(@xs)),insertionsortD#(@xs)) testInsertionsort#(@x) -> c_22(insertionsort#(testList(#unit()))) testInsertionsortD#(@x) -> c_23(insertionsortD#(testList(#unit()))) * Step 7: DecomposeDG WORST_CASE(?,O(n^3)) + Considered Problem: - Strict DPs: insert#(@x,@l) -> c_6(insert#1#(@l,@x)) insert#1#(::(@y,@ys),@x) -> c_7(insert#2#(#less(@y,@x),@x,@y,@ys)) insert#2#(#true(),@x,@y,@ys) -> c_10(insert#(@x,@ys)) insertD#(@x,@l) -> c_11(insertD#1#(@l,@x)) insertD#1#(::(@y,@ys),@x) -> c_12(insertD#2#(#less(@y,@x),@x,@y,@ys)) insertD#2#(#true(),@x,@y,@ys) -> c_15(insertD#(@x,@ys)) insertionsort#(@l) -> c_16(insertionsort#1#(@l)) insertionsort#1#(::(@x,@xs)) -> c_17(insert#(@x,insertionsort(@xs)),insertionsort#(@xs)) insertionsortD#(@l) -> c_19(insertionsortD#1#(@l)) insertionsortD#1#(::(@x,@xs)) -> c_20(insertD#(@x,insertionsortD(@xs)),insertionsortD#(@xs)) testInsertionsort#(@x) -> c_22(insertionsort#(testList(#unit()))) testInsertionsortD#(@x) -> c_23(insertionsortD#(testList(#unit()))) - Weak TRS: #abs(#0()) -> #0() #abs(#pos(@x)) -> #pos(@x) #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) #less(@x,@y) -> #cklt(#compare(@x,@y)) insert(@x,@l) -> insert#1(@l,@x) insert#1(::(@y,@ys),@x) -> insert#2(#less(@y,@x),@x,@y,@ys) insert#1(nil(),@x) -> ::(@x,nil()) insert#2(#false(),@x,@y,@ys) -> ::(@x,::(@y,@ys)) insert#2(#true(),@x,@y,@ys) -> ::(@y,insert(@x,@ys)) insertD(@x,@l) -> insertD#1(@l,@x) insertD#1(::(@y,@ys),@x) -> insertD#2(#less(@y,@x),@x,@y,@ys) insertD#1(nil(),@x) -> ::(@x,nil()) insertD#2(#false(),@x,@y,@ys) -> ::(@x,::(@y,@ys)) insertD#2(#true(),@x,@y,@ys) -> ::(@y,insertD(@x,@ys)) insertionsort(@l) -> insertionsort#1(@l) insertionsort#1(::(@x,@xs)) -> insert(@x,insertionsort(@xs)) insertionsort#1(nil()) -> nil() insertionsortD(@l) -> insertionsortD#1(@l) insertionsortD#1(::(@x,@xs)) -> insertD(@x,insertionsortD(@xs)) insertionsortD#1(nil()) -> nil() testList(@_) -> ::(#abs(#0()) ,::(#abs(#pos(#s(#s(#s(#s(#0())))))) ,::(#abs(#pos(#s(#s(#s(#s(#s(#0()))))))) ,::(#abs(#pos(#s(#s(#s(#s(#s(#s(#s(#s(#s(#0()))))))))))) ,::(#abs(#pos(#s(#s(#s(#s(#s(#s(#s(#0()))))))))) ,::(#abs(#pos(#s(#0()))) ,::(#abs(#pos(#s(#s(#0())))) ,::(#abs(#pos(#s(#s(#s(#s(#s(#s(#s(#s(#0())))))))))) ,::(#abs(#pos(#s(#s(#s(#s(#s(#s(#0())))))))) ,::(#abs(#pos(#s(#s(#s(#0()))))),nil())))))))))) - Signature: {#abs/1,#cklt/1,#compare/2,#less/2,insert/2,insert#1/2,insert#2/4,insertD/2,insertD#1/2,insertD#2/4 ,insertionsort/1,insertionsort#1/1,insertionsortD/1,insertionsortD#1/1,testInsertionsort/1 ,testInsertionsortD/1,testList/1,#abs#/1,#cklt#/1,#compare#/2,#less#/2,insert#/2,insert#1#/2,insert#2#/4 ,insertD#/2,insertD#1#/2,insertD#2#/4,insertionsort#/1,insertionsort#1#/1,insertionsortD#/1 ,insertionsortD#1#/1,testInsertionsort#/1,testInsertionsortD#/1,testList#/1} / {#0/0,#EQ/0,#GT/0,#LT/0 ,#false/0,#neg/1,#pos/1,#s/1,#true/0,#unit/0,::/2,nil/0,c_1/0,c_2/0,c_3/0,c_4/0,c_5/2,c_6/1,c_7/1,c_8/0 ,c_9/0,c_10/1,c_11/1,c_12/1,c_13/0,c_14/0,c_15/1,c_16/1,c_17/2,c_18/0,c_19/1,c_20/2,c_21/0,c_22/1,c_23/1 ,c_24/10,c_25/0,c_26/0,c_27/0,c_28/0,c_29/0,c_30/0,c_31/0,c_32/0,c_33/1,c_34/0,c_35/0,c_36/0,c_37/1,c_38/0 ,c_39/1} - Obligation: innermost runtime complexity wrt. defined symbols {#abs#,#cklt#,#compare#,#less#,insert#,insert#1#,insert#2# ,insertD#,insertD#1#,insertD#2#,insertionsort#,insertionsort#1#,insertionsortD#,insertionsortD#1# ,testInsertionsort#,testInsertionsortD#,testList#} and constructors {#0,#EQ,#GT,#LT,#false,#neg,#pos,#s ,#true,#unit,::,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 insertionsort#(@l) -> c_16(insertionsort#1#(@l)) insertionsort#1#(::(@x,@xs)) -> c_17(insert#(@x,insertionsort(@xs)),insertionsort#(@xs)) insertionsortD#(@l) -> c_19(insertionsortD#1#(@l)) insertionsortD#1#(::(@x,@xs)) -> c_20(insertD#(@x,insertionsortD(@xs)),insertionsortD#(@xs)) testInsertionsort#(@x) -> c_22(insertionsort#(testList(#unit()))) testInsertionsortD#(@x) -> c_23(insertionsortD#(testList(#unit()))) and a lower component insert#(@x,@l) -> c_6(insert#1#(@l,@x)) insert#1#(::(@y,@ys),@x) -> c_7(insert#2#(#less(@y,@x),@x,@y,@ys)) insert#2#(#true(),@x,@y,@ys) -> c_10(insert#(@x,@ys)) insertD#(@x,@l) -> c_11(insertD#1#(@l,@x)) insertD#1#(::(@y,@ys),@x) -> c_12(insertD#2#(#less(@y,@x),@x,@y,@ys)) insertD#2#(#true(),@x,@y,@ys) -> c_15(insertD#(@x,@ys)) Further, following extension rules are added to the lower component. insertionsort#(@l) -> insertionsort#1#(@l) insertionsort#1#(::(@x,@xs)) -> insert#(@x,insertionsort(@xs)) insertionsort#1#(::(@x,@xs)) -> insertionsort#(@xs) insertionsortD#(@l) -> insertionsortD#1#(@l) insertionsortD#1#(::(@x,@xs)) -> insertD#(@x,insertionsortD(@xs)) insertionsortD#1#(::(@x,@xs)) -> insertionsortD#(@xs) testInsertionsort#(@x) -> insertionsort#(testList(#unit())) testInsertionsortD#(@x) -> insertionsortD#(testList(#unit())) ** Step 7.a:1: SimplifyRHS WORST_CASE(?,O(n^1)) + Considered Problem: - Strict DPs: insertionsort#(@l) -> c_16(insertionsort#1#(@l)) insertionsort#1#(::(@x,@xs)) -> c_17(insert#(@x,insertionsort(@xs)),insertionsort#(@xs)) insertionsortD#(@l) -> c_19(insertionsortD#1#(@l)) insertionsortD#1#(::(@x,@xs)) -> c_20(insertD#(@x,insertionsortD(@xs)),insertionsortD#(@xs)) testInsertionsort#(@x) -> c_22(insertionsort#(testList(#unit()))) testInsertionsortD#(@x) -> c_23(insertionsortD#(testList(#unit()))) - Weak TRS: #abs(#0()) -> #0() #abs(#pos(@x)) -> #pos(@x) #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) #less(@x,@y) -> #cklt(#compare(@x,@y)) insert(@x,@l) -> insert#1(@l,@x) insert#1(::(@y,@ys),@x) -> insert#2(#less(@y,@x),@x,@y,@ys) insert#1(nil(),@x) -> ::(@x,nil()) insert#2(#false(),@x,@y,@ys) -> ::(@x,::(@y,@ys)) insert#2(#true(),@x,@y,@ys) -> ::(@y,insert(@x,@ys)) insertD(@x,@l) -> insertD#1(@l,@x) insertD#1(::(@y,@ys),@x) -> insertD#2(#less(@y,@x),@x,@y,@ys) insertD#1(nil(),@x) -> ::(@x,nil()) insertD#2(#false(),@x,@y,@ys) -> ::(@x,::(@y,@ys)) insertD#2(#true(),@x,@y,@ys) -> ::(@y,insertD(@x,@ys)) insertionsort(@l) -> insertionsort#1(@l) insertionsort#1(::(@x,@xs)) -> insert(@x,insertionsort(@xs)) insertionsort#1(nil()) -> nil() insertionsortD(@l) -> insertionsortD#1(@l) insertionsortD#1(::(@x,@xs)) -> insertD(@x,insertionsortD(@xs)) insertionsortD#1(nil()) -> nil() testList(@_) -> ::(#abs(#0()) ,::(#abs(#pos(#s(#s(#s(#s(#0())))))) ,::(#abs(#pos(#s(#s(#s(#s(#s(#0()))))))) ,::(#abs(#pos(#s(#s(#s(#s(#s(#s(#s(#s(#s(#0()))))))))))) ,::(#abs(#pos(#s(#s(#s(#s(#s(#s(#s(#0()))))))))) ,::(#abs(#pos(#s(#0()))) ,::(#abs(#pos(#s(#s(#0())))) ,::(#abs(#pos(#s(#s(#s(#s(#s(#s(#s(#s(#0())))))))))) ,::(#abs(#pos(#s(#s(#s(#s(#s(#s(#0())))))))) ,::(#abs(#pos(#s(#s(#s(#0()))))),nil())))))))))) - Signature: {#abs/1,#cklt/1,#compare/2,#less/2,insert/2,insert#1/2,insert#2/4,insertD/2,insertD#1/2,insertD#2/4 ,insertionsort/1,insertionsort#1/1,insertionsortD/1,insertionsortD#1/1,testInsertionsort/1 ,testInsertionsortD/1,testList/1,#abs#/1,#cklt#/1,#compare#/2,#less#/2,insert#/2,insert#1#/2,insert#2#/4 ,insertD#/2,insertD#1#/2,insertD#2#/4,insertionsort#/1,insertionsort#1#/1,insertionsortD#/1 ,insertionsortD#1#/1,testInsertionsort#/1,testInsertionsortD#/1,testList#/1} / {#0/0,#EQ/0,#GT/0,#LT/0 ,#false/0,#neg/1,#pos/1,#s/1,#true/0,#unit/0,::/2,nil/0,c_1/0,c_2/0,c_3/0,c_4/0,c_5/2,c_6/1,c_7/1,c_8/0 ,c_9/0,c_10/1,c_11/1,c_12/1,c_13/0,c_14/0,c_15/1,c_16/1,c_17/2,c_18/0,c_19/1,c_20/2,c_21/0,c_22/1,c_23/1 ,c_24/10,c_25/0,c_26/0,c_27/0,c_28/0,c_29/0,c_30/0,c_31/0,c_32/0,c_33/1,c_34/0,c_35/0,c_36/0,c_37/1,c_38/0 ,c_39/1} - Obligation: innermost runtime complexity wrt. defined symbols {#abs#,#cklt#,#compare#,#less#,insert#,insert#1#,insert#2# ,insertD#,insertD#1#,insertD#2#,insertionsort#,insertionsort#1#,insertionsortD#,insertionsortD#1# ,testInsertionsort#,testInsertionsortD#,testList#} and constructors {#0,#EQ,#GT,#LT,#false,#neg,#pos,#s ,#true,#unit,::,nil} + Applied Processor: SimplifyRHS + Details: Consider the dependency graph 1:S:insertionsort#(@l) -> c_16(insertionsort#1#(@l)) -->_1 insertionsort#1#(::(@x,@xs)) -> c_17(insert#(@x,insertionsort(@xs)),insertionsort#(@xs)):2 2:S:insertionsort#1#(::(@x,@xs)) -> c_17(insert#(@x,insertionsort(@xs)),insertionsort#(@xs)) -->_2 insertionsort#(@l) -> c_16(insertionsort#1#(@l)):1 3:S:insertionsortD#(@l) -> c_19(insertionsortD#1#(@l)) -->_1 insertionsortD#1#(::(@x,@xs)) -> c_20(insertD#(@x,insertionsortD(@xs)),insertionsortD#(@xs)):4 4:S:insertionsortD#1#(::(@x,@xs)) -> c_20(insertD#(@x,insertionsortD(@xs)),insertionsortD#(@xs)) -->_2 insertionsortD#(@l) -> c_19(insertionsortD#1#(@l)):3 5:S:testInsertionsort#(@x) -> c_22(insertionsort#(testList(#unit()))) -->_1 insertionsort#(@l) -> c_16(insertionsort#1#(@l)):1 6:S:testInsertionsortD#(@x) -> c_23(insertionsortD#(testList(#unit()))) -->_1 insertionsortD#(@l) -> c_19(insertionsortD#1#(@l)):3 Due to missing edges in the depndency graph, the right-hand sides of following rules could be simplified: insertionsort#1#(::(@x,@xs)) -> c_17(insertionsort#(@xs)) insertionsortD#1#(::(@x,@xs)) -> c_20(insertionsortD#(@xs)) ** Step 7.a:2: UsableRules WORST_CASE(?,O(n^1)) + Considered Problem: - Strict DPs: insertionsort#(@l) -> c_16(insertionsort#1#(@l)) insertionsort#1#(::(@x,@xs)) -> c_17(insertionsort#(@xs)) insertionsortD#(@l) -> c_19(insertionsortD#1#(@l)) insertionsortD#1#(::(@x,@xs)) -> c_20(insertionsortD#(@xs)) testInsertionsort#(@x) -> c_22(insertionsort#(testList(#unit()))) testInsertionsortD#(@x) -> c_23(insertionsortD#(testList(#unit()))) - Weak TRS: #abs(#0()) -> #0() #abs(#pos(@x)) -> #pos(@x) #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) #less(@x,@y) -> #cklt(#compare(@x,@y)) insert(@x,@l) -> insert#1(@l,@x) insert#1(::(@y,@ys),@x) -> insert#2(#less(@y,@x),@x,@y,@ys) insert#1(nil(),@x) -> ::(@x,nil()) insert#2(#false(),@x,@y,@ys) -> ::(@x,::(@y,@ys)) insert#2(#true(),@x,@y,@ys) -> ::(@y,insert(@x,@ys)) insertD(@x,@l) -> insertD#1(@l,@x) insertD#1(::(@y,@ys),@x) -> insertD#2(#less(@y,@x),@x,@y,@ys) insertD#1(nil(),@x) -> ::(@x,nil()) insertD#2(#false(),@x,@y,@ys) -> ::(@x,::(@y,@ys)) insertD#2(#true(),@x,@y,@ys) -> ::(@y,insertD(@x,@ys)) insertionsort(@l) -> insertionsort#1(@l) insertionsort#1(::(@x,@xs)) -> insert(@x,insertionsort(@xs)) insertionsort#1(nil()) -> nil() insertionsortD(@l) -> insertionsortD#1(@l) insertionsortD#1(::(@x,@xs)) -> insertD(@x,insertionsortD(@xs)) insertionsortD#1(nil()) -> nil() testList(@_) -> ::(#abs(#0()) ,::(#abs(#pos(#s(#s(#s(#s(#0())))))) ,::(#abs(#pos(#s(#s(#s(#s(#s(#0()))))))) ,::(#abs(#pos(#s(#s(#s(#s(#s(#s(#s(#s(#s(#0()))))))))))) ,::(#abs(#pos(#s(#s(#s(#s(#s(#s(#s(#0()))))))))) ,::(#abs(#pos(#s(#0()))) ,::(#abs(#pos(#s(#s(#0())))) ,::(#abs(#pos(#s(#s(#s(#s(#s(#s(#s(#s(#0())))))))))) ,::(#abs(#pos(#s(#s(#s(#s(#s(#s(#0())))))))) ,::(#abs(#pos(#s(#s(#s(#0()))))),nil())))))))))) - Signature: {#abs/1,#cklt/1,#compare/2,#less/2,insert/2,insert#1/2,insert#2/4,insertD/2,insertD#1/2,insertD#2/4 ,insertionsort/1,insertionsort#1/1,insertionsortD/1,insertionsortD#1/1,testInsertionsort/1 ,testInsertionsortD/1,testList/1,#abs#/1,#cklt#/1,#compare#/2,#less#/2,insert#/2,insert#1#/2,insert#2#/4 ,insertD#/2,insertD#1#/2,insertD#2#/4,insertionsort#/1,insertionsort#1#/1,insertionsortD#/1 ,insertionsortD#1#/1,testInsertionsort#/1,testInsertionsortD#/1,testList#/1} / {#0/0,#EQ/0,#GT/0,#LT/0 ,#false/0,#neg/1,#pos/1,#s/1,#true/0,#unit/0,::/2,nil/0,c_1/0,c_2/0,c_3/0,c_4/0,c_5/2,c_6/1,c_7/1,c_8/0 ,c_9/0,c_10/1,c_11/1,c_12/1,c_13/0,c_14/0,c_15/1,c_16/1,c_17/1,c_18/0,c_19/1,c_20/1,c_21/0,c_22/1,c_23/1 ,c_24/10,c_25/0,c_26/0,c_27/0,c_28/0,c_29/0,c_30/0,c_31/0,c_32/0,c_33/1,c_34/0,c_35/0,c_36/0,c_37/1,c_38/0 ,c_39/1} - Obligation: innermost runtime complexity wrt. defined symbols {#abs#,#cklt#,#compare#,#less#,insert#,insert#1#,insert#2# ,insertD#,insertD#1#,insertD#2#,insertionsort#,insertionsort#1#,insertionsortD#,insertionsortD#1# ,testInsertionsort#,testInsertionsortD#,testList#} and constructors {#0,#EQ,#GT,#LT,#false,#neg,#pos,#s ,#true,#unit,::,nil} + Applied Processor: UsableRules + Details: We replace rewrite rules by usable rules: #abs(#0()) -> #0() #abs(#pos(@x)) -> #pos(@x) testList(@_) -> ::(#abs(#0()) ,::(#abs(#pos(#s(#s(#s(#s(#0())))))) ,::(#abs(#pos(#s(#s(#s(#s(#s(#0()))))))) ,::(#abs(#pos(#s(#s(#s(#s(#s(#s(#s(#s(#s(#0()))))))))))) ,::(#abs(#pos(#s(#s(#s(#s(#s(#s(#s(#0()))))))))) ,::(#abs(#pos(#s(#0()))) ,::(#abs(#pos(#s(#s(#0())))) ,::(#abs(#pos(#s(#s(#s(#s(#s(#s(#s(#s(#0())))))))))) ,::(#abs(#pos(#s(#s(#s(#s(#s(#s(#0())))))))) ,::(#abs(#pos(#s(#s(#s(#0()))))),nil())))))))))) insertionsort#(@l) -> c_16(insertionsort#1#(@l)) insertionsort#1#(::(@x,@xs)) -> c_17(insertionsort#(@xs)) insertionsortD#(@l) -> c_19(insertionsortD#1#(@l)) insertionsortD#1#(::(@x,@xs)) -> c_20(insertionsortD#(@xs)) testInsertionsort#(@x) -> c_22(insertionsort#(testList(#unit()))) testInsertionsortD#(@x) -> c_23(insertionsortD#(testList(#unit()))) ** Step 7.a:3: WeightGap WORST_CASE(?,O(n^1)) + Considered Problem: - Strict DPs: insertionsort#(@l) -> c_16(insertionsort#1#(@l)) insertionsort#1#(::(@x,@xs)) -> c_17(insertionsort#(@xs)) insertionsortD#(@l) -> c_19(insertionsortD#1#(@l)) insertionsortD#1#(::(@x,@xs)) -> c_20(insertionsortD#(@xs)) testInsertionsort#(@x) -> c_22(insertionsort#(testList(#unit()))) testInsertionsortD#(@x) -> c_23(insertionsortD#(testList(#unit()))) - Weak TRS: #abs(#0()) -> #0() #abs(#pos(@x)) -> #pos(@x) testList(@_) -> ::(#abs(#0()) ,::(#abs(#pos(#s(#s(#s(#s(#0())))))) ,::(#abs(#pos(#s(#s(#s(#s(#s(#0()))))))) ,::(#abs(#pos(#s(#s(#s(#s(#s(#s(#s(#s(#s(#0()))))))))))) ,::(#abs(#pos(#s(#s(#s(#s(#s(#s(#s(#0()))))))))) ,::(#abs(#pos(#s(#0()))) ,::(#abs(#pos(#s(#s(#0())))) ,::(#abs(#pos(#s(#s(#s(#s(#s(#s(#s(#s(#0())))))))))) ,::(#abs(#pos(#s(#s(#s(#s(#s(#s(#0())))))))) ,::(#abs(#pos(#s(#s(#s(#0()))))),nil())))))))))) - Signature: {#abs/1,#cklt/1,#compare/2,#less/2,insert/2,insert#1/2,insert#2/4,insertD/2,insertD#1/2,insertD#2/4 ,insertionsort/1,insertionsort#1/1,insertionsortD/1,insertionsortD#1/1,testInsertionsort/1 ,testInsertionsortD/1,testList/1,#abs#/1,#cklt#/1,#compare#/2,#less#/2,insert#/2,insert#1#/2,insert#2#/4 ,insertD#/2,insertD#1#/2,insertD#2#/4,insertionsort#/1,insertionsort#1#/1,insertionsortD#/1 ,insertionsortD#1#/1,testInsertionsort#/1,testInsertionsortD#/1,testList#/1} / {#0/0,#EQ/0,#GT/0,#LT/0 ,#false/0,#neg/1,#pos/1,#s/1,#true/0,#unit/0,::/2,nil/0,c_1/0,c_2/0,c_3/0,c_4/0,c_5/2,c_6/1,c_7/1,c_8/0 ,c_9/0,c_10/1,c_11/1,c_12/1,c_13/0,c_14/0,c_15/1,c_16/1,c_17/1,c_18/0,c_19/1,c_20/1,c_21/0,c_22/1,c_23/1 ,c_24/10,c_25/0,c_26/0,c_27/0,c_28/0,c_29/0,c_30/0,c_31/0,c_32/0,c_33/1,c_34/0,c_35/0,c_36/0,c_37/1,c_38/0 ,c_39/1} - Obligation: innermost runtime complexity wrt. defined symbols {#abs#,#cklt#,#compare#,#less#,insert#,insert#1#,insert#2# ,insertD#,insertD#1#,insertD#2#,insertionsort#,insertionsort#1#,insertionsortD#,insertionsortD#1# ,testInsertionsort#,testInsertionsortD#,testList#} and constructors {#0,#EQ,#GT,#LT,#false,#neg,#pos,#s ,#true,#unit,::,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(::) = {1,2}, uargs(insertionsort#) = {1}, uargs(insertionsortD#) = {1}, uargs(c_16) = {1}, uargs(c_17) = {1}, uargs(c_19) = {1}, uargs(c_20) = {1}, uargs(c_22) = {1}, uargs(c_23) = {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(#abs) = [0] p(#cklt) = [0] p(#compare) = [0] p(#false) = [0] p(#less) = [0] p(#neg) = [1] x1 + [0] p(#pos) = [0] p(#s) = [1] x1 + [0] p(#true) = [0] p(#unit) = [0] p(::) = [1] x1 + [1] x2 + [0] p(insert) = [0] p(insert#1) = [0] p(insert#2) = [0] p(insertD) = [0] p(insertD#1) = [0] p(insertD#2) = [0] p(insertionsort) = [0] p(insertionsort#1) = [0] p(insertionsortD) = [0] p(insertionsortD#1) = [0] p(nil) = [0] p(testInsertionsort) = [0] p(testInsertionsortD) = [0] p(testList) = [0] p(#abs#) = [0] p(#cklt#) = [0] p(#compare#) = [0] p(#less#) = [0] p(insert#) = [0] p(insert#1#) = [0] p(insert#2#) = [0] p(insertD#) = [0] p(insertD#1#) = [0] p(insertD#2#) = [0] p(insertionsort#) = [1] x1 + [0] p(insertionsort#1#) = [1] x1 + [0] p(insertionsortD#) = [1] x1 + [0] p(insertionsortD#1#) = [1] x1 + [0] p(testInsertionsort#) = [0] p(testInsertionsortD#) = [1] p(testList#) = [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) = [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) = [1] x1 + [0] p(c_17) = [1] x1 + [0] p(c_18) = [0] p(c_19) = [1] x1 + [0] p(c_20) = [1] x1 + [0] p(c_21) = [0] p(c_22) = [1] x1 + [0] p(c_23) = [1] x1 + [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] Following rules are strictly oriented: testInsertionsortD#(@x) = [1] > [0] = c_23(insertionsortD#(testList(#unit()))) Following rules are (at-least) weakly oriented: insertionsort#(@l) = [1] @l + [0] >= [1] @l + [0] = c_16(insertionsort#1#(@l)) insertionsort#1#(::(@x,@xs)) = [1] @x + [1] @xs + [0] >= [1] @xs + [0] = c_17(insertionsort#(@xs)) insertionsortD#(@l) = [1] @l + [0] >= [1] @l + [0] = c_19(insertionsortD#1#(@l)) insertionsortD#1#(::(@x,@xs)) = [1] @x + [1] @xs + [0] >= [1] @xs + [0] = c_20(insertionsortD#(@xs)) testInsertionsort#(@x) = [0] >= [0] = c_22(insertionsort#(testList(#unit()))) #abs(#0()) = [0] >= [0] = #0() #abs(#pos(@x)) = [0] >= [0] = #pos(@x) testList(@_) = [0] >= [0] = ::(#abs(#0()) ,::(#abs(#pos(#s(#s(#s(#s(#0())))))) ,::(#abs(#pos(#s(#s(#s(#s(#s(#0()))))))) ,::(#abs(#pos(#s(#s(#s(#s(#s(#s(#s(#s(#s(#0()))))))))))) ,::(#abs(#pos(#s(#s(#s(#s(#s(#s(#s(#0()))))))))) ,::(#abs(#pos(#s(#0()))) ,::(#abs(#pos(#s(#s(#0())))) ,::(#abs(#pos(#s(#s(#s(#s(#s(#s(#s(#s(#0())))))))))) ,::(#abs(#pos(#s(#s(#s(#s(#s(#s(#0())))))))),::(#abs(#pos(#s(#s(#s(#0()))))),nil())))))))))) Further, it can be verified that all rules not oriented are covered by the weightgap condition. ** Step 7.a:4: WeightGap WORST_CASE(?,O(n^1)) + Considered Problem: - Strict DPs: insertionsort#(@l) -> c_16(insertionsort#1#(@l)) insertionsort#1#(::(@x,@xs)) -> c_17(insertionsort#(@xs)) insertionsortD#(@l) -> c_19(insertionsortD#1#(@l)) insertionsortD#1#(::(@x,@xs)) -> c_20(insertionsortD#(@xs)) testInsertionsort#(@x) -> c_22(insertionsort#(testList(#unit()))) - Weak DPs: testInsertionsortD#(@x) -> c_23(insertionsortD#(testList(#unit()))) - Weak TRS: #abs(#0()) -> #0() #abs(#pos(@x)) -> #pos(@x) testList(@_) -> ::(#abs(#0()) ,::(#abs(#pos(#s(#s(#s(#s(#0())))))) ,::(#abs(#pos(#s(#s(#s(#s(#s(#0()))))))) ,::(#abs(#pos(#s(#s(#s(#s(#s(#s(#s(#s(#s(#0()))))))))))) ,::(#abs(#pos(#s(#s(#s(#s(#s(#s(#s(#0()))))))))) ,::(#abs(#pos(#s(#0()))) ,::(#abs(#pos(#s(#s(#0())))) ,::(#abs(#pos(#s(#s(#s(#s(#s(#s(#s(#s(#0())))))))))) ,::(#abs(#pos(#s(#s(#s(#s(#s(#s(#0())))))))) ,::(#abs(#pos(#s(#s(#s(#0()))))),nil())))))))))) - Signature: {#abs/1,#cklt/1,#compare/2,#less/2,insert/2,insert#1/2,insert#2/4,insertD/2,insertD#1/2,insertD#2/4 ,insertionsort/1,insertionsort#1/1,insertionsortD/1,insertionsortD#1/1,testInsertionsort/1 ,testInsertionsortD/1,testList/1,#abs#/1,#cklt#/1,#compare#/2,#less#/2,insert#/2,insert#1#/2,insert#2#/4 ,insertD#/2,insertD#1#/2,insertD#2#/4,insertionsort#/1,insertionsort#1#/1,insertionsortD#/1 ,insertionsortD#1#/1,testInsertionsort#/1,testInsertionsortD#/1,testList#/1} / {#0/0,#EQ/0,#GT/0,#LT/0 ,#false/0,#neg/1,#pos/1,#s/1,#true/0,#unit/0,::/2,nil/0,c_1/0,c_2/0,c_3/0,c_4/0,c_5/2,c_6/1,c_7/1,c_8/0 ,c_9/0,c_10/1,c_11/1,c_12/1,c_13/0,c_14/0,c_15/1,c_16/1,c_17/1,c_18/0,c_19/1,c_20/1,c_21/0,c_22/1,c_23/1 ,c_24/10,c_25/0,c_26/0,c_27/0,c_28/0,c_29/0,c_30/0,c_31/0,c_32/0,c_33/1,c_34/0,c_35/0,c_36/0,c_37/1,c_38/0 ,c_39/1} - Obligation: innermost runtime complexity wrt. defined symbols {#abs#,#cklt#,#compare#,#less#,insert#,insert#1#,insert#2# ,insertD#,insertD#1#,insertD#2#,insertionsort#,insertionsort#1#,insertionsortD#,insertionsortD#1# ,testInsertionsort#,testInsertionsortD#,testList#} and constructors {#0,#EQ,#GT,#LT,#false,#neg,#pos,#s ,#true,#unit,::,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(::) = {1,2}, uargs(insertionsort#) = {1}, uargs(insertionsortD#) = {1}, uargs(c_16) = {1}, uargs(c_17) = {1}, uargs(c_19) = {1}, uargs(c_20) = {1}, uargs(c_22) = {1}, uargs(c_23) = {1} Following symbols are considered usable: all TcT has computed the following interpretation: p(#0) = [0] p(#EQ) = [1] p(#GT) = [0] p(#LT) = [1] p(#abs) = [0] p(#cklt) = [0] p(#compare) = [0] p(#false) = [1] p(#less) = [2] x2 + [2] p(#neg) = [1] x1 + [0] p(#pos) = [0] p(#s) = [0] p(#true) = [0] p(#unit) = [0] p(::) = [1] x1 + [1] x2 + [0] p(insert) = [1] x1 + [2] x2 + [0] p(insert#1) = [2] x1 + [2] p(insert#2) = [1] x1 + [1] x2 + [1] x4 + [2] p(insertD) = [0] p(insertD#1) = [2] x1 + [1] x2 + [0] p(insertD#2) = [1] x4 + [1] p(insertionsort) = [0] p(insertionsort#1) = [1] p(insertionsortD) = [2] x1 + [2] p(insertionsortD#1) = [2] x1 + [0] p(nil) = [1] p(testInsertionsort) = [4] p(testInsertionsortD) = [1] x1 + [1] p(testList) = [2] x1 + [1] p(#abs#) = [2] x1 + [0] p(#cklt#) = [1] p(#compare#) = [2] x2 + [2] p(#less#) = [1] x1 + [2] p(insert#) = [1] x2 + [1] p(insert#1#) = [1] x2 + [0] p(insert#2#) = [1] x1 + [1] x2 + [1] x3 + [1] p(insertD#) = [2] p(insertD#1#) = [1] x2 + [4] p(insertD#2#) = [1] x3 + [1] p(insertionsort#) = [1] x1 + [2] p(insertionsort#1#) = [1] x1 + [6] p(insertionsortD#) = [1] x1 + [1] p(insertionsortD#1#) = [1] x1 + [4] p(testInsertionsort#) = [1] p(testInsertionsortD#) = [1] x1 + [7] p(testList#) = [4] x1 + [1] p(c_1) = [0] p(c_2) = [0] p(c_3) = [2] p(c_4) = [1] p(c_5) = [2] x1 + [4] p(c_6) = [1] p(c_7) = [2] x1 + [4] p(c_8) = [0] p(c_9) = [1] p(c_10) = [0] p(c_11) = [1] x1 + [1] p(c_12) = [4] x1 + [2] p(c_13) = [0] p(c_14) = [0] p(c_15) = [1] x1 + [1] p(c_16) = [1] x1 + [2] p(c_17) = [1] x1 + [0] p(c_18) = [1] p(c_19) = [1] x1 + [1] p(c_20) = [1] x1 + [0] p(c_21) = [1] p(c_22) = [1] x1 + [0] p(c_23) = [1] x1 + [4] p(c_24) = [1] x1 + [4] x2 + [1] x5 + [1] x6 + [2] x8 + [2] p(c_25) = [0] p(c_26) = [4] p(c_27) = [1] p(c_28) = [0] p(c_29) = [4] p(c_30) = [0] p(c_31) = [4] p(c_32) = [2] p(c_33) = [4] x1 + [4] p(c_34) = [0] p(c_35) = [1] p(c_36) = [1] p(c_37) = [2] x1 + [0] p(c_38) = [1] p(c_39) = [0] Following rules are strictly oriented: insertionsort#1#(::(@x,@xs)) = [1] @x + [1] @xs + [6] > [1] @xs + [2] = c_17(insertionsort#(@xs)) insertionsortD#1#(::(@x,@xs)) = [1] @x + [1] @xs + [4] > [1] @xs + [1] = c_20(insertionsortD#(@xs)) Following rules are (at-least) weakly oriented: insertionsort#(@l) = [1] @l + [2] >= [1] @l + [8] = c_16(insertionsort#1#(@l)) insertionsortD#(@l) = [1] @l + [1] >= [1] @l + [5] = c_19(insertionsortD#1#(@l)) testInsertionsort#(@x) = [1] >= [3] = c_22(insertionsort#(testList(#unit()))) testInsertionsortD#(@x) = [1] @x + [7] >= [6] = c_23(insertionsortD#(testList(#unit()))) #abs(#0()) = [0] >= [0] = #0() #abs(#pos(@x)) = [0] >= [0] = #pos(@x) testList(@_) = [2] @_ + [1] >= [1] = ::(#abs(#0()) ,::(#abs(#pos(#s(#s(#s(#s(#0())))))) ,::(#abs(#pos(#s(#s(#s(#s(#s(#0()))))))) ,::(#abs(#pos(#s(#s(#s(#s(#s(#s(#s(#s(#s(#0()))))))))))) ,::(#abs(#pos(#s(#s(#s(#s(#s(#s(#s(#0()))))))))) ,::(#abs(#pos(#s(#0()))) ,::(#abs(#pos(#s(#s(#0())))) ,::(#abs(#pos(#s(#s(#s(#s(#s(#s(#s(#s(#0())))))))))) ,::(#abs(#pos(#s(#s(#s(#s(#s(#s(#0())))))))),::(#abs(#pos(#s(#s(#s(#0()))))),nil())))))))))) Further, it can be verified that all rules not oriented are covered by the weightgap condition. ** Step 7.a:5: WeightGap WORST_CASE(?,O(n^1)) + Considered Problem: - Strict DPs: insertionsort#(@l) -> c_16(insertionsort#1#(@l)) insertionsortD#(@l) -> c_19(insertionsortD#1#(@l)) testInsertionsort#(@x) -> c_22(insertionsort#(testList(#unit()))) - Weak DPs: insertionsort#1#(::(@x,@xs)) -> c_17(insertionsort#(@xs)) insertionsortD#1#(::(@x,@xs)) -> c_20(insertionsortD#(@xs)) testInsertionsortD#(@x) -> c_23(insertionsortD#(testList(#unit()))) - Weak TRS: #abs(#0()) -> #0() #abs(#pos(@x)) -> #pos(@x) testList(@_) -> ::(#abs(#0()) ,::(#abs(#pos(#s(#s(#s(#s(#0())))))) ,::(#abs(#pos(#s(#s(#s(#s(#s(#0()))))))) ,::(#abs(#pos(#s(#s(#s(#s(#s(#s(#s(#s(#s(#0()))))))))))) ,::(#abs(#pos(#s(#s(#s(#s(#s(#s(#s(#0()))))))))) ,::(#abs(#pos(#s(#0()))) ,::(#abs(#pos(#s(#s(#0())))) ,::(#abs(#pos(#s(#s(#s(#s(#s(#s(#s(#s(#0())))))))))) ,::(#abs(#pos(#s(#s(#s(#s(#s(#s(#0())))))))) ,::(#abs(#pos(#s(#s(#s(#0()))))),nil())))))))))) - Signature: {#abs/1,#cklt/1,#compare/2,#less/2,insert/2,insert#1/2,insert#2/4,insertD/2,insertD#1/2,insertD#2/4 ,insertionsort/1,insertionsort#1/1,insertionsortD/1,insertionsortD#1/1,testInsertionsort/1 ,testInsertionsortD/1,testList/1,#abs#/1,#cklt#/1,#compare#/2,#less#/2,insert#/2,insert#1#/2,insert#2#/4 ,insertD#/2,insertD#1#/2,insertD#2#/4,insertionsort#/1,insertionsort#1#/1,insertionsortD#/1 ,insertionsortD#1#/1,testInsertionsort#/1,testInsertionsortD#/1,testList#/1} / {#0/0,#EQ/0,#GT/0,#LT/0 ,#false/0,#neg/1,#pos/1,#s/1,#true/0,#unit/0,::/2,nil/0,c_1/0,c_2/0,c_3/0,c_4/0,c_5/2,c_6/1,c_7/1,c_8/0 ,c_9/0,c_10/1,c_11/1,c_12/1,c_13/0,c_14/0,c_15/1,c_16/1,c_17/1,c_18/0,c_19/1,c_20/1,c_21/0,c_22/1,c_23/1 ,c_24/10,c_25/0,c_26/0,c_27/0,c_28/0,c_29/0,c_30/0,c_31/0,c_32/0,c_33/1,c_34/0,c_35/0,c_36/0,c_37/1,c_38/0 ,c_39/1} - Obligation: innermost runtime complexity wrt. defined symbols {#abs#,#cklt#,#compare#,#less#,insert#,insert#1#,insert#2# ,insertD#,insertD#1#,insertD#2#,insertionsort#,insertionsort#1#,insertionsortD#,insertionsortD#1# ,testInsertionsort#,testInsertionsortD#,testList#} and constructors {#0,#EQ,#GT,#LT,#false,#neg,#pos,#s ,#true,#unit,::,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(::) = {1,2}, uargs(insertionsort#) = {1}, uargs(insertionsortD#) = {1}, uargs(c_16) = {1}, uargs(c_17) = {1}, uargs(c_19) = {1}, uargs(c_20) = {1}, uargs(c_22) = {1}, uargs(c_23) = {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(#abs) = [0] p(#cklt) = [0] p(#compare) = [0] p(#false) = [0] p(#less) = [0] p(#neg) = [1] x1 + [0] p(#pos) = [0] p(#s) = [3] p(#true) = [0] p(#unit) = [0] p(::) = [1] x1 + [1] x2 + [0] p(insert) = [0] p(insert#1) = [0] p(insert#2) = [0] p(insertD) = [0] p(insertD#1) = [1] x1 + [2] p(insertD#2) = [4] x1 + [4] x2 + [2] p(insertionsort) = [1] x1 + [0] p(insertionsort#1) = [1] p(insertionsortD) = [1] p(insertionsortD#1) = [1] p(nil) = [4] p(testInsertionsort) = [1] x1 + [1] p(testInsertionsortD) = [2] x1 + [0] p(testList) = [4] x1 + [4] p(#abs#) = [1] x1 + [1] p(#cklt#) = [1] x1 + [0] p(#compare#) = [1] x1 + [0] p(#less#) = [2] x1 + [1] x2 + [0] p(insert#) = [4] x1 + [4] x2 + [0] p(insert#1#) = [0] p(insert#2#) = [2] x1 + [1] x2 + [4] p(insertD#) = [0] p(insertD#1#) = [1] x1 + [4] x2 + [0] p(insertD#2#) = [4] x2 + [2] x3 + [4] x4 + [1] p(insertionsort#) = [1] x1 + [0] p(insertionsort#1#) = [1] x1 + [4] p(insertionsortD#) = [1] x1 + [0] p(insertionsortD#1#) = [1] x1 + [2] p(testInsertionsort#) = [1] x1 + [5] p(testInsertionsortD#) = [6] p(testList#) = [1] x1 + [0] p(c_1) = [2] p(c_2) = [0] p(c_3) = [1] p(c_4) = [0] p(c_5) = [0] p(c_6) = [1] x1 + [4] p(c_7) = [1] x1 + [1] p(c_8) = [2] p(c_9) = [1] p(c_10) = [0] p(c_11) = [1] p(c_12) = [4] x1 + [1] p(c_13) = [0] p(c_14) = [0] p(c_15) = [4] x1 + [4] p(c_16) = [1] x1 + [3] p(c_17) = [1] x1 + [0] p(c_18) = [0] p(c_19) = [1] x1 + [5] p(c_20) = [1] x1 + [0] p(c_21) = [1] p(c_22) = [1] x1 + [0] p(c_23) = [1] x1 + [2] p(c_24) = [1] x1 + [2] x4 + [1] x5 + [1] x7 + [4] x8 + [1] x9 + [1] x10 + [0] p(c_25) = [1] p(c_26) = [1] p(c_27) = [0] p(c_28) = [0] p(c_29) = [1] p(c_30) = [1] p(c_31) = [0] p(c_32) = [1] p(c_33) = [1] x1 + [0] p(c_34) = [2] p(c_35) = [0] p(c_36) = [4] p(c_37) = [4] x1 + [2] p(c_38) = [0] p(c_39) = [1] Following rules are strictly oriented: testInsertionsort#(@x) = [1] @x + [5] > [4] = c_22(insertionsort#(testList(#unit()))) Following rules are (at-least) weakly oriented: insertionsort#(@l) = [1] @l + [0] >= [1] @l + [7] = c_16(insertionsort#1#(@l)) insertionsort#1#(::(@x,@xs)) = [1] @x + [1] @xs + [4] >= [1] @xs + [0] = c_17(insertionsort#(@xs)) insertionsortD#(@l) = [1] @l + [0] >= [1] @l + [7] = c_19(insertionsortD#1#(@l)) insertionsortD#1#(::(@x,@xs)) = [1] @x + [1] @xs + [2] >= [1] @xs + [0] = c_20(insertionsortD#(@xs)) testInsertionsortD#(@x) = [6] >= [6] = c_23(insertionsortD#(testList(#unit()))) #abs(#0()) = [0] >= [0] = #0() #abs(#pos(@x)) = [0] >= [0] = #pos(@x) testList(@_) = [4] @_ + [4] >= [4] = ::(#abs(#0()) ,::(#abs(#pos(#s(#s(#s(#s(#0())))))) ,::(#abs(#pos(#s(#s(#s(#s(#s(#0()))))))) ,::(#abs(#pos(#s(#s(#s(#s(#s(#s(#s(#s(#s(#0()))))))))))) ,::(#abs(#pos(#s(#s(#s(#s(#s(#s(#s(#0()))))))))) ,::(#abs(#pos(#s(#0()))) ,::(#abs(#pos(#s(#s(#0())))) ,::(#abs(#pos(#s(#s(#s(#s(#s(#s(#s(#s(#0())))))))))) ,::(#abs(#pos(#s(#s(#s(#s(#s(#s(#0())))))))),::(#abs(#pos(#s(#s(#s(#0()))))),nil())))))))))) Further, it can be verified that all rules not oriented are covered by the weightgap condition. ** Step 7.a:6: NaturalMI WORST_CASE(?,O(n^1)) + Considered Problem: - Strict DPs: insertionsort#(@l) -> c_16(insertionsort#1#(@l)) insertionsortD#(@l) -> c_19(insertionsortD#1#(@l)) - Weak DPs: insertionsort#1#(::(@x,@xs)) -> c_17(insertionsort#(@xs)) insertionsortD#1#(::(@x,@xs)) -> c_20(insertionsortD#(@xs)) testInsertionsort#(@x) -> c_22(insertionsort#(testList(#unit()))) testInsertionsortD#(@x) -> c_23(insertionsortD#(testList(#unit()))) - Weak TRS: #abs(#0()) -> #0() #abs(#pos(@x)) -> #pos(@x) testList(@_) -> ::(#abs(#0()) ,::(#abs(#pos(#s(#s(#s(#s(#0())))))) ,::(#abs(#pos(#s(#s(#s(#s(#s(#0()))))))) ,::(#abs(#pos(#s(#s(#s(#s(#s(#s(#s(#s(#s(#0()))))))))))) ,::(#abs(#pos(#s(#s(#s(#s(#s(#s(#s(#0()))))))))) ,::(#abs(#pos(#s(#0()))) ,::(#abs(#pos(#s(#s(#0())))) ,::(#abs(#pos(#s(#s(#s(#s(#s(#s(#s(#s(#0())))))))))) ,::(#abs(#pos(#s(#s(#s(#s(#s(#s(#0())))))))) ,::(#abs(#pos(#s(#s(#s(#0()))))),nil())))))))))) - Signature: {#abs/1,#cklt/1,#compare/2,#less/2,insert/2,insert#1/2,insert#2/4,insertD/2,insertD#1/2,insertD#2/4 ,insertionsort/1,insertionsort#1/1,insertionsortD/1,insertionsortD#1/1,testInsertionsort/1 ,testInsertionsortD/1,testList/1,#abs#/1,#cklt#/1,#compare#/2,#less#/2,insert#/2,insert#1#/2,insert#2#/4 ,insertD#/2,insertD#1#/2,insertD#2#/4,insertionsort#/1,insertionsort#1#/1,insertionsortD#/1 ,insertionsortD#1#/1,testInsertionsort#/1,testInsertionsortD#/1,testList#/1} / {#0/0,#EQ/0,#GT/0,#LT/0 ,#false/0,#neg/1,#pos/1,#s/1,#true/0,#unit/0,::/2,nil/0,c_1/0,c_2/0,c_3/0,c_4/0,c_5/2,c_6/1,c_7/1,c_8/0 ,c_9/0,c_10/1,c_11/1,c_12/1,c_13/0,c_14/0,c_15/1,c_16/1,c_17/1,c_18/0,c_19/1,c_20/1,c_21/0,c_22/1,c_23/1 ,c_24/10,c_25/0,c_26/0,c_27/0,c_28/0,c_29/0,c_30/0,c_31/0,c_32/0,c_33/1,c_34/0,c_35/0,c_36/0,c_37/1,c_38/0 ,c_39/1} - Obligation: innermost runtime complexity wrt. defined symbols {#abs#,#cklt#,#compare#,#less#,insert#,insert#1#,insert#2# ,insertD#,insertD#1#,insertD#2#,insertionsort#,insertionsort#1#,insertionsortD#,insertionsortD#1# ,testInsertionsort#,testInsertionsortD#,testList#} and constructors {#0,#EQ,#GT,#LT,#false,#neg,#pos,#s ,#true,#unit,::,nil} + Applied Processor: NaturalMI {miDimension = 1, miDegree = 1, miKind = Algebraic, uargs = UArgs, urules = URules, selector = Just any strict-rules} + Details: We apply a matrix interpretation of kind constructor based matrix interpretation: The following argument positions are considered usable: uargs(c_16) = {1}, uargs(c_17) = {1}, uargs(c_19) = {1}, uargs(c_20) = {1}, uargs(c_22) = {1}, uargs(c_23) = {1} Following symbols are considered usable: {testList,#abs#,#cklt#,#compare#,#less#,insert#,insert#1#,insert#2#,insertD#,insertD#1#,insertD#2# ,insertionsort#,insertionsort#1#,insertionsortD#,insertionsortD#1#,testInsertionsort#,testInsertionsortD# ,testList#} TcT has computed the following interpretation: p(#0) = [0] p(#EQ) = [1] p(#GT) = [2] p(#LT) = [2] p(#abs) = [9] x1 + [12] p(#cklt) = [2] x1 + [1] p(#compare) = [1] p(#false) = [1] p(#less) = [1] x2 + [1] p(#neg) = [1] x1 + [1] p(#pos) = [2] p(#s) = [0] p(#true) = [0] p(#unit) = [1] p(::) = [1] x2 + [1] p(insert) = [1] x1 + [4] x2 + [0] p(insert#1) = [1] x1 + [1] p(insert#2) = [2] x2 + [1] x3 + [1] x4 + [8] p(insertD) = [2] x1 + [4] p(insertD#1) = [1] p(insertD#2) = [2] x1 + [4] x3 + [1] x4 + [1] p(insertionsort) = [1] p(insertionsort#1) = [1] x1 + [2] p(insertionsortD) = [1] p(insertionsortD#1) = [1] x1 + [0] p(nil) = [1] p(testInsertionsort) = [1] x1 + [2] p(testInsertionsortD) = [8] x1 + [1] p(testList) = [1] x1 + [13] p(#abs#) = [1] x1 + [1] p(#cklt#) = [2] x1 + [0] p(#compare#) = [1] x1 + [0] p(#less#) = [2] x2 + [1] p(insert#) = [1] x2 + [1] p(insert#1#) = [1] x2 + [1] p(insert#2#) = [0] p(insertD#) = [0] p(insertD#1#) = [1] x1 + [8] x2 + [2] p(insertD#2#) = [4] x2 + [1] x3 + [1] x4 + [1] p(insertionsort#) = [1] x1 + [1] p(insertionsort#1#) = [1] x1 + [0] p(insertionsortD#) = [0] p(insertionsortD#1#) = [0] p(testInsertionsort#) = [15] p(testInsertionsortD#) = [1] x1 + [11] p(testList#) = [0] p(c_1) = [0] p(c_2) = [2] p(c_3) = [4] p(c_4) = [8] p(c_5) = [1] p(c_6) = [1] x1 + [1] p(c_7) = [1] x1 + [1] p(c_8) = [0] p(c_9) = [1] p(c_10) = [1] p(c_11) = [1] x1 + [0] p(c_12) = [1] p(c_13) = [0] p(c_14) = [1] p(c_15) = [8] p(c_16) = [1] x1 + [0] p(c_17) = [1] x1 + [0] p(c_18) = [2] p(c_19) = [8] x1 + [0] p(c_20) = [8] x1 + [0] p(c_21) = [0] p(c_22) = [1] x1 + [0] p(c_23) = [1] x1 + [11] p(c_24) = [1] x1 + [1] x2 + [2] x4 + [1] x6 + [2] x7 + [8] x8 + [4] x10 + [0] p(c_25) = [2] p(c_26) = [2] p(c_27) = [1] p(c_28) = [0] p(c_29) = [8] p(c_30) = [8] p(c_31) = [2] p(c_32) = [2] p(c_33) = [1] x1 + [0] p(c_34) = [0] p(c_35) = [0] p(c_36) = [1] p(c_37) = [1] x1 + [1] p(c_38) = [2] p(c_39) = [2] Following rules are strictly oriented: insertionsort#(@l) = [1] @l + [1] > [1] @l + [0] = c_16(insertionsort#1#(@l)) Following rules are (at-least) weakly oriented: insertionsort#1#(::(@x,@xs)) = [1] @xs + [1] >= [1] @xs + [1] = c_17(insertionsort#(@xs)) insertionsortD#(@l) = [0] >= [0] = c_19(insertionsortD#1#(@l)) insertionsortD#1#(::(@x,@xs)) = [0] >= [0] = c_20(insertionsortD#(@xs)) testInsertionsort#(@x) = [15] >= [15] = c_22(insertionsort#(testList(#unit()))) testInsertionsortD#(@x) = [1] @x + [11] >= [11] = c_23(insertionsortD#(testList(#unit()))) testList(@_) = [1] @_ + [13] >= [11] = ::(#abs(#0()) ,::(#abs(#pos(#s(#s(#s(#s(#0())))))) ,::(#abs(#pos(#s(#s(#s(#s(#s(#0()))))))) ,::(#abs(#pos(#s(#s(#s(#s(#s(#s(#s(#s(#s(#0()))))))))))) ,::(#abs(#pos(#s(#s(#s(#s(#s(#s(#s(#0()))))))))) ,::(#abs(#pos(#s(#0()))) ,::(#abs(#pos(#s(#s(#0())))) ,::(#abs(#pos(#s(#s(#s(#s(#s(#s(#s(#s(#0())))))))))) ,::(#abs(#pos(#s(#s(#s(#s(#s(#s(#0())))))))),::(#abs(#pos(#s(#s(#s(#0()))))),nil())))))))))) ** Step 7.a:7: NaturalMI WORST_CASE(?,O(n^1)) + Considered Problem: - Strict DPs: insertionsortD#(@l) -> c_19(insertionsortD#1#(@l)) - Weak DPs: insertionsort#(@l) -> c_16(insertionsort#1#(@l)) insertionsort#1#(::(@x,@xs)) -> c_17(insertionsort#(@xs)) insertionsortD#1#(::(@x,@xs)) -> c_20(insertionsortD#(@xs)) testInsertionsort#(@x) -> c_22(insertionsort#(testList(#unit()))) testInsertionsortD#(@x) -> c_23(insertionsortD#(testList(#unit()))) - Weak TRS: #abs(#0()) -> #0() #abs(#pos(@x)) -> #pos(@x) testList(@_) -> ::(#abs(#0()) ,::(#abs(#pos(#s(#s(#s(#s(#0())))))) ,::(#abs(#pos(#s(#s(#s(#s(#s(#0()))))))) ,::(#abs(#pos(#s(#s(#s(#s(#s(#s(#s(#s(#s(#0()))))))))))) ,::(#abs(#pos(#s(#s(#s(#s(#s(#s(#s(#0()))))))))) ,::(#abs(#pos(#s(#0()))) ,::(#abs(#pos(#s(#s(#0())))) ,::(#abs(#pos(#s(#s(#s(#s(#s(#s(#s(#s(#0())))))))))) ,::(#abs(#pos(#s(#s(#s(#s(#s(#s(#0())))))))) ,::(#abs(#pos(#s(#s(#s(#0()))))),nil())))))))))) - Signature: {#abs/1,#cklt/1,#compare/2,#less/2,insert/2,insert#1/2,insert#2/4,insertD/2,insertD#1/2,insertD#2/4 ,insertionsort/1,insertionsort#1/1,insertionsortD/1,insertionsortD#1/1,testInsertionsort/1 ,testInsertionsortD/1,testList/1,#abs#/1,#cklt#/1,#compare#/2,#less#/2,insert#/2,insert#1#/2,insert#2#/4 ,insertD#/2,insertD#1#/2,insertD#2#/4,insertionsort#/1,insertionsort#1#/1,insertionsortD#/1 ,insertionsortD#1#/1,testInsertionsort#/1,testInsertionsortD#/1,testList#/1} / {#0/0,#EQ/0,#GT/0,#LT/0 ,#false/0,#neg/1,#pos/1,#s/1,#true/0,#unit/0,::/2,nil/0,c_1/0,c_2/0,c_3/0,c_4/0,c_5/2,c_6/1,c_7/1,c_8/0 ,c_9/0,c_10/1,c_11/1,c_12/1,c_13/0,c_14/0,c_15/1,c_16/1,c_17/1,c_18/0,c_19/1,c_20/1,c_21/0,c_22/1,c_23/1 ,c_24/10,c_25/0,c_26/0,c_27/0,c_28/0,c_29/0,c_30/0,c_31/0,c_32/0,c_33/1,c_34/0,c_35/0,c_36/0,c_37/1,c_38/0 ,c_39/1} - Obligation: innermost runtime complexity wrt. defined symbols {#abs#,#cklt#,#compare#,#less#,insert#,insert#1#,insert#2# ,insertD#,insertD#1#,insertD#2#,insertionsort#,insertionsort#1#,insertionsortD#,insertionsortD#1# ,testInsertionsort#,testInsertionsortD#,testList#} and constructors {#0,#EQ,#GT,#LT,#false,#neg,#pos,#s ,#true,#unit,::,nil} + Applied Processor: NaturalMI {miDimension = 1, miDegree = 1, miKind = Algebraic, uargs = UArgs, urules = URules, selector = Just any strict-rules} + Details: We apply a matrix interpretation of kind constructor based matrix interpretation: The following argument positions are considered usable: uargs(c_16) = {1}, uargs(c_17) = {1}, uargs(c_19) = {1}, uargs(c_20) = {1}, uargs(c_22) = {1}, uargs(c_23) = {1} Following symbols are considered usable: {testList,#abs#,#cklt#,#compare#,#less#,insert#,insert#1#,insert#2#,insertD#,insertD#1#,insertD#2# ,insertionsort#,insertionsort#1#,insertionsortD#,insertionsortD#1#,testInsertionsort#,testInsertionsortD# ,testList#} TcT has computed the following interpretation: p(#0) = [0] p(#EQ) = [2] p(#GT) = [0] p(#LT) = [0] p(#abs) = [8] p(#cklt) = [2] p(#compare) = [1] x1 + [2] x2 + [1] p(#false) = [1] p(#less) = [1] x1 + [2] x2 + [1] p(#neg) = [1] p(#pos) = [8] p(#s) = [0] p(#true) = [1] p(#unit) = [0] p(::) = [1] x2 + [1] p(insert) = [1] x1 + [1] p(insert#1) = [1] p(insert#2) = [2] x1 + [2] p(insertD) = [1] x2 + [2] p(insertD#1) = [1] p(insertD#2) = [1] x3 + [1] p(insertionsort) = [1] x1 + [8] p(insertionsort#1) = [0] p(insertionsortD) = [4] x1 + [1] p(insertionsortD#1) = [0] p(nil) = [0] p(testInsertionsort) = [2] p(testInsertionsortD) = [0] p(testList) = [8] x1 + [11] p(#abs#) = [1] p(#cklt#) = [1] x1 + [2] p(#compare#) = [1] x1 + [1] x2 + [0] p(#less#) = [2] p(insert#) = [8] x1 + [1] p(insert#1#) = [1] p(insert#2#) = [1] x1 + [1] x3 + [2] x4 + [1] p(insertD#) = [1] x1 + [0] p(insertD#1#) = [1] p(insertD#2#) = [8] x4 + [0] p(insertionsort#) = [0] p(insertionsort#1#) = [0] p(insertionsortD#) = [1] x1 + [1] p(insertionsortD#1#) = [1] x1 + [0] p(testInsertionsort#) = [2] x1 + [10] p(testInsertionsortD#) = [13] p(testList#) = [1] x1 + [8] p(c_1) = [1] p(c_2) = [1] p(c_3) = [4] p(c_4) = [1] p(c_5) = [1] x2 + [0] p(c_6) = [1] p(c_7) = [0] p(c_8) = [1] p(c_9) = [1] p(c_10) = [1] p(c_11) = [1] x1 + [4] p(c_12) = [1] x1 + [1] p(c_13) = [2] p(c_14) = [0] p(c_15) = [1] p(c_16) = [1] x1 + [0] p(c_17) = [1] x1 + [0] p(c_18) = [1] p(c_19) = [1] x1 + [0] p(c_20) = [1] x1 + [0] p(c_21) = [0] p(c_22) = [8] x1 + [0] p(c_23) = [1] x1 + [1] p(c_24) = [2] x2 + [1] x4 + [1] x5 + [1] x8 + [2] x10 + [0] p(c_25) = [1] p(c_26) = [8] p(c_27) = [1] p(c_28) = [1] p(c_29) = [1] p(c_30) = [0] p(c_31) = [1] p(c_32) = [2] p(c_33) = [0] p(c_34) = [0] p(c_35) = [0] p(c_36) = [1] p(c_37) = [1] x1 + [1] p(c_38) = [1] p(c_39) = [2] x1 + [2] Following rules are strictly oriented: insertionsortD#(@l) = [1] @l + [1] > [1] @l + [0] = c_19(insertionsortD#1#(@l)) Following rules are (at-least) weakly oriented: insertionsort#(@l) = [0] >= [0] = c_16(insertionsort#1#(@l)) insertionsort#1#(::(@x,@xs)) = [0] >= [0] = c_17(insertionsort#(@xs)) insertionsortD#1#(::(@x,@xs)) = [1] @xs + [1] >= [1] @xs + [1] = c_20(insertionsortD#(@xs)) testInsertionsort#(@x) = [2] @x + [10] >= [0] = c_22(insertionsort#(testList(#unit()))) testInsertionsortD#(@x) = [13] >= [13] = c_23(insertionsortD#(testList(#unit()))) testList(@_) = [8] @_ + [11] >= [10] = ::(#abs(#0()) ,::(#abs(#pos(#s(#s(#s(#s(#0())))))) ,::(#abs(#pos(#s(#s(#s(#s(#s(#0()))))))) ,::(#abs(#pos(#s(#s(#s(#s(#s(#s(#s(#s(#s(#0()))))))))))) ,::(#abs(#pos(#s(#s(#s(#s(#s(#s(#s(#0()))))))))) ,::(#abs(#pos(#s(#0()))) ,::(#abs(#pos(#s(#s(#0())))) ,::(#abs(#pos(#s(#s(#s(#s(#s(#s(#s(#s(#0())))))))))) ,::(#abs(#pos(#s(#s(#s(#s(#s(#s(#0())))))))),::(#abs(#pos(#s(#s(#s(#0()))))),nil())))))))))) ** Step 7.a:8: EmptyProcessor WORST_CASE(?,O(1)) + Considered Problem: - Weak DPs: insertionsort#(@l) -> c_16(insertionsort#1#(@l)) insertionsort#1#(::(@x,@xs)) -> c_17(insertionsort#(@xs)) insertionsortD#(@l) -> c_19(insertionsortD#1#(@l)) insertionsortD#1#(::(@x,@xs)) -> c_20(insertionsortD#(@xs)) testInsertionsort#(@x) -> c_22(insertionsort#(testList(#unit()))) testInsertionsortD#(@x) -> c_23(insertionsortD#(testList(#unit()))) - Weak TRS: #abs(#0()) -> #0() #abs(#pos(@x)) -> #pos(@x) testList(@_) -> ::(#abs(#0()) ,::(#abs(#pos(#s(#s(#s(#s(#0())))))) ,::(#abs(#pos(#s(#s(#s(#s(#s(#0()))))))) ,::(#abs(#pos(#s(#s(#s(#s(#s(#s(#s(#s(#s(#0()))))))))))) ,::(#abs(#pos(#s(#s(#s(#s(#s(#s(#s(#0()))))))))) ,::(#abs(#pos(#s(#0()))) ,::(#abs(#pos(#s(#s(#0())))) ,::(#abs(#pos(#s(#s(#s(#s(#s(#s(#s(#s(#0())))))))))) ,::(#abs(#pos(#s(#s(#s(#s(#s(#s(#0())))))))) ,::(#abs(#pos(#s(#s(#s(#0()))))),nil())))))))))) - Signature: {#abs/1,#cklt/1,#compare/2,#less/2,insert/2,insert#1/2,insert#2/4,insertD/2,insertD#1/2,insertD#2/4 ,insertionsort/1,insertionsort#1/1,insertionsortD/1,insertionsortD#1/1,testInsertionsort/1 ,testInsertionsortD/1,testList/1,#abs#/1,#cklt#/1,#compare#/2,#less#/2,insert#/2,insert#1#/2,insert#2#/4 ,insertD#/2,insertD#1#/2,insertD#2#/4,insertionsort#/1,insertionsort#1#/1,insertionsortD#/1 ,insertionsortD#1#/1,testInsertionsort#/1,testInsertionsortD#/1,testList#/1} / {#0/0,#EQ/0,#GT/0,#LT/0 ,#false/0,#neg/1,#pos/1,#s/1,#true/0,#unit/0,::/2,nil/0,c_1/0,c_2/0,c_3/0,c_4/0,c_5/2,c_6/1,c_7/1,c_8/0 ,c_9/0,c_10/1,c_11/1,c_12/1,c_13/0,c_14/0,c_15/1,c_16/1,c_17/1,c_18/0,c_19/1,c_20/1,c_21/0,c_22/1,c_23/1 ,c_24/10,c_25/0,c_26/0,c_27/0,c_28/0,c_29/0,c_30/0,c_31/0,c_32/0,c_33/1,c_34/0,c_35/0,c_36/0,c_37/1,c_38/0 ,c_39/1} - Obligation: innermost runtime complexity wrt. defined symbols {#abs#,#cklt#,#compare#,#less#,insert#,insert#1#,insert#2# ,insertD#,insertD#1#,insertD#2#,insertionsort#,insertionsort#1#,insertionsortD#,insertionsortD#1# ,testInsertionsort#,testInsertionsortD#,testList#} and constructors {#0,#EQ,#GT,#LT,#false,#neg,#pos,#s ,#true,#unit,::,nil} + Applied Processor: EmptyProcessor + Details: The problem is already closed. The intended complexity is O(1). ** Step 7.b:1: WeightGap WORST_CASE(?,O(n^2)) + Considered Problem: - Strict DPs: insert#(@x,@l) -> c_6(insert#1#(@l,@x)) insert#1#(::(@y,@ys),@x) -> c_7(insert#2#(#less(@y,@x),@x,@y,@ys)) insert#2#(#true(),@x,@y,@ys) -> c_10(insert#(@x,@ys)) insertD#(@x,@l) -> c_11(insertD#1#(@l,@x)) insertD#1#(::(@y,@ys),@x) -> c_12(insertD#2#(#less(@y,@x),@x,@y,@ys)) insertD#2#(#true(),@x,@y,@ys) -> c_15(insertD#(@x,@ys)) - Weak DPs: insertionsort#(@l) -> insertionsort#1#(@l) insertionsort#1#(::(@x,@xs)) -> insert#(@x,insertionsort(@xs)) insertionsort#1#(::(@x,@xs)) -> insertionsort#(@xs) insertionsortD#(@l) -> insertionsortD#1#(@l) insertionsortD#1#(::(@x,@xs)) -> insertD#(@x,insertionsortD(@xs)) insertionsortD#1#(::(@x,@xs)) -> insertionsortD#(@xs) testInsertionsort#(@x) -> insertionsort#(testList(#unit())) testInsertionsortD#(@x) -> insertionsortD#(testList(#unit())) - Weak TRS: #abs(#0()) -> #0() #abs(#pos(@x)) -> #pos(@x) #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) #less(@x,@y) -> #cklt(#compare(@x,@y)) insert(@x,@l) -> insert#1(@l,@x) insert#1(::(@y,@ys),@x) -> insert#2(#less(@y,@x),@x,@y,@ys) insert#1(nil(),@x) -> ::(@x,nil()) insert#2(#false(),@x,@y,@ys) -> ::(@x,::(@y,@ys)) insert#2(#true(),@x,@y,@ys) -> ::(@y,insert(@x,@ys)) insertD(@x,@l) -> insertD#1(@l,@x) insertD#1(::(@y,@ys),@x) -> insertD#2(#less(@y,@x),@x,@y,@ys) insertD#1(nil(),@x) -> ::(@x,nil()) insertD#2(#false(),@x,@y,@ys) -> ::(@x,::(@y,@ys)) insertD#2(#true(),@x,@y,@ys) -> ::(@y,insertD(@x,@ys)) insertionsort(@l) -> insertionsort#1(@l) insertionsort#1(::(@x,@xs)) -> insert(@x,insertionsort(@xs)) insertionsort#1(nil()) -> nil() insertionsortD(@l) -> insertionsortD#1(@l) insertionsortD#1(::(@x,@xs)) -> insertD(@x,insertionsortD(@xs)) insertionsortD#1(nil()) -> nil() testList(@_) -> ::(#abs(#0()) ,::(#abs(#pos(#s(#s(#s(#s(#0())))))) ,::(#abs(#pos(#s(#s(#s(#s(#s(#0()))))))) ,::(#abs(#pos(#s(#s(#s(#s(#s(#s(#s(#s(#s(#0()))))))))))) ,::(#abs(#pos(#s(#s(#s(#s(#s(#s(#s(#0()))))))))) ,::(#abs(#pos(#s(#0()))) ,::(#abs(#pos(#s(#s(#0())))) ,::(#abs(#pos(#s(#s(#s(#s(#s(#s(#s(#s(#0())))))))))) ,::(#abs(#pos(#s(#s(#s(#s(#s(#s(#0())))))))) ,::(#abs(#pos(#s(#s(#s(#0()))))),nil())))))))))) - Signature: {#abs/1,#cklt/1,#compare/2,#less/2,insert/2,insert#1/2,insert#2/4,insertD/2,insertD#1/2,insertD#2/4 ,insertionsort/1,insertionsort#1/1,insertionsortD/1,insertionsortD#1/1,testInsertionsort/1 ,testInsertionsortD/1,testList/1,#abs#/1,#cklt#/1,#compare#/2,#less#/2,insert#/2,insert#1#/2,insert#2#/4 ,insertD#/2,insertD#1#/2,insertD#2#/4,insertionsort#/1,insertionsort#1#/1,insertionsortD#/1 ,insertionsortD#1#/1,testInsertionsort#/1,testInsertionsortD#/1,testList#/1} / {#0/0,#EQ/0,#GT/0,#LT/0 ,#false/0,#neg/1,#pos/1,#s/1,#true/0,#unit/0,::/2,nil/0,c_1/0,c_2/0,c_3/0,c_4/0,c_5/2,c_6/1,c_7/1,c_8/0 ,c_9/0,c_10/1,c_11/1,c_12/1,c_13/0,c_14/0,c_15/1,c_16/1,c_17/2,c_18/0,c_19/1,c_20/2,c_21/0,c_22/1,c_23/1 ,c_24/10,c_25/0,c_26/0,c_27/0,c_28/0,c_29/0,c_30/0,c_31/0,c_32/0,c_33/1,c_34/0,c_35/0,c_36/0,c_37/1,c_38/0 ,c_39/1} - Obligation: innermost runtime complexity wrt. defined symbols {#abs#,#cklt#,#compare#,#less#,insert#,insert#1#,insert#2# ,insertD#,insertD#1#,insertD#2#,insertionsort#,insertionsort#1#,insertionsortD#,insertionsortD#1# ,testInsertionsort#,testInsertionsortD#,testList#} and constructors {#0,#EQ,#GT,#LT,#false,#neg,#pos,#s ,#true,#unit,::,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(#cklt) = {1}, uargs(::) = {1,2}, uargs(insert) = {2}, uargs(insert#2) = {1}, uargs(insertD) = {2}, uargs(insertD#2) = {1}, uargs(insert#) = {2}, uargs(insert#2#) = {1}, uargs(insertD#) = {2}, uargs(insertD#2#) = {1}, uargs(insertionsort#) = {1}, uargs(insertionsortD#) = {1}, uargs(c_6) = {1}, uargs(c_7) = {1}, uargs(c_10) = {1}, uargs(c_11) = {1}, uargs(c_12) = {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(#abs) = [0] p(#cklt) = [1] x1 + [0] p(#compare) = [0] p(#false) = [0] p(#less) = [0] p(#neg) = [4] p(#pos) = [0] p(#s) = [4] p(#true) = [0] p(#unit) = [1] p(::) = [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(insertD) = [1] x1 + [1] x2 + [0] p(insertD#1) = [1] x1 + [1] x2 + [0] p(insertD#2) = [1] x1 + [1] x2 + [1] x3 + [1] x4 + [0] p(insertionsort) = [1] x1 + [0] p(insertionsort#1) = [1] x1 + [0] p(insertionsortD) = [1] x1 + [0] p(insertionsortD#1) = [1] x1 + [0] p(nil) = [0] p(testInsertionsort) = [2] x1 + [0] p(testInsertionsortD) = [0] p(testList) = [1] x1 + [0] p(#abs#) = [0] p(#cklt#) = [0] p(#compare#) = [4] x1 + [1] x2 + [0] p(#less#) = [1] x1 + [1] p(insert#) = [1] x2 + [0] p(insert#1#) = [1] x1 + [0] p(insert#2#) = [1] x1 + [1] x4 + [1] p(insertD#) = [1] x2 + [2] p(insertD#1#) = [1] x1 + [5] p(insertD#2#) = [1] x1 + [1] x3 + [1] x4 + [0] p(insertionsort#) = [1] x1 + [1] p(insertionsort#1#) = [1] x1 + [1] p(insertionsortD#) = [1] x1 + [2] p(insertionsortD#1#) = [1] x1 + [2] p(testInsertionsort#) = [2] p(testInsertionsortD#) = [1] x1 + [3] p(testList#) = [1] x1 + [1] p(c_1) = [0] p(c_2) = [0] p(c_3) = [1] p(c_4) = [1] p(c_5) = [1] x2 + [0] p(c_6) = [1] x1 + [0] p(c_7) = [1] x1 + [0] p(c_8) = [0] p(c_9) = [4] p(c_10) = [1] x1 + [1] p(c_11) = [1] x1 + [5] p(c_12) = [1] x1 + [1] p(c_13) = [1] p(c_14) = [1] p(c_15) = [1] x1 + [5] p(c_16) = [4] x1 + [0] p(c_17) = [1] x1 + [1] x2 + [4] p(c_18) = [1] p(c_19) = [0] p(c_20) = [1] x1 + [2] p(c_21) = [0] p(c_22) = [4] x1 + [1] p(c_23) = [4] x1 + [0] p(c_24) = [4] x2 + [2] x3 + [1] x4 + [1] x7 + [1] x8 + [2] p(c_25) = [1] p(c_26) = [1] p(c_27) = [1] p(c_28) = [1] p(c_29) = [2] p(c_30) = [1] p(c_31) = [0] p(c_32) = [1] p(c_33) = [4] x1 + [1] p(c_34) = [1] p(c_35) = [4] p(c_36) = [1] p(c_37) = [2] x1 + [1] p(c_38) = [0] p(c_39) = [1] x1 + [1] Following rules are strictly oriented: insertD#1#(::(@y,@ys),@x) = [1] @y + [1] @ys + [5] > [1] @y + [1] @ys + [1] = c_12(insertD#2#(#less(@y,@x),@x,@y,@ys)) Following rules are (at-least) weakly oriented: insert#(@x,@l) = [1] @l + [0] >= [1] @l + [0] = c_6(insert#1#(@l,@x)) insert#1#(::(@y,@ys),@x) = [1] @y + [1] @ys + [0] >= [1] @ys + [1] = c_7(insert#2#(#less(@y,@x),@x,@y,@ys)) insert#2#(#true(),@x,@y,@ys) = [1] @ys + [1] >= [1] @ys + [1] = c_10(insert#(@x,@ys)) insertD#(@x,@l) = [1] @l + [2] >= [1] @l + [10] = c_11(insertD#1#(@l,@x)) insertD#2#(#true(),@x,@y,@ys) = [1] @y + [1] @ys + [0] >= [1] @ys + [7] = c_15(insertD#(@x,@ys)) insertionsort#(@l) = [1] @l + [1] >= [1] @l + [1] = insertionsort#1#(@l) insertionsort#1#(::(@x,@xs)) = [1] @x + [1] @xs + [1] >= [1] @xs + [0] = insert#(@x,insertionsort(@xs)) insertionsort#1#(::(@x,@xs)) = [1] @x + [1] @xs + [1] >= [1] @xs + [1] = insertionsort#(@xs) insertionsortD#(@l) = [1] @l + [2] >= [1] @l + [2] = insertionsortD#1#(@l) insertionsortD#1#(::(@x,@xs)) = [1] @x + [1] @xs + [2] >= [1] @xs + [2] = insertD#(@x,insertionsortD(@xs)) insertionsortD#1#(::(@x,@xs)) = [1] @x + [1] @xs + [2] >= [1] @xs + [2] = insertionsortD#(@xs) testInsertionsort#(@x) = [2] >= [2] = insertionsort#(testList(#unit())) testInsertionsortD#(@x) = [1] @x + [3] >= [3] = insertionsortD#(testList(#unit())) #abs(#0()) = [0] >= [0] = #0() #abs(#pos(@x)) = [0] >= [0] = #pos(@x) #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) #less(@x,@y) = [0] >= [0] = #cklt(#compare(@x,@y)) 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 + [0] >= [1] @x + [1] @y + [1] @ys + [0] = insert#2(#less(@y,@x),@x,@y,@ys) insert#1(nil(),@x) = [1] @x + [0] >= [1] @x + [0] = ::(@x,nil()) insert#2(#false(),@x,@y,@ys) = [1] @x + [1] @y + [1] @ys + [0] >= [1] @x + [1] @y + [1] @ys + [0] = ::(@x,::(@y,@ys)) insert#2(#true(),@x,@y,@ys) = [1] @x + [1] @y + [1] @ys + [0] >= [1] @x + [1] @y + [1] @ys + [0] = ::(@y,insert(@x,@ys)) insertD(@x,@l) = [1] @l + [1] @x + [0] >= [1] @l + [1] @x + [0] = insertD#1(@l,@x) insertD#1(::(@y,@ys),@x) = [1] @x + [1] @y + [1] @ys + [0] >= [1] @x + [1] @y + [1] @ys + [0] = insertD#2(#less(@y,@x),@x,@y,@ys) insertD#1(nil(),@x) = [1] @x + [0] >= [1] @x + [0] = ::(@x,nil()) insertD#2(#false(),@x,@y,@ys) = [1] @x + [1] @y + [1] @ys + [0] >= [1] @x + [1] @y + [1] @ys + [0] = ::(@x,::(@y,@ys)) insertD#2(#true(),@x,@y,@ys) = [1] @x + [1] @y + [1] @ys + [0] >= [1] @x + [1] @y + [1] @ys + [0] = ::(@y,insertD(@x,@ys)) insertionsort(@l) = [1] @l + [0] >= [1] @l + [0] = insertionsort#1(@l) insertionsort#1(::(@x,@xs)) = [1] @x + [1] @xs + [0] >= [1] @x + [1] @xs + [0] = insert(@x,insertionsort(@xs)) insertionsort#1(nil()) = [0] >= [0] = nil() insertionsortD(@l) = [1] @l + [0] >= [1] @l + [0] = insertionsortD#1(@l) insertionsortD#1(::(@x,@xs)) = [1] @x + [1] @xs + [0] >= [1] @x + [1] @xs + [0] = insertD(@x,insertionsortD(@xs)) insertionsortD#1(nil()) = [0] >= [0] = nil() testList(@_) = [1] @_ + [0] >= [0] = ::(#abs(#0()) ,::(#abs(#pos(#s(#s(#s(#s(#0())))))) ,::(#abs(#pos(#s(#s(#s(#s(#s(#0()))))))) ,::(#abs(#pos(#s(#s(#s(#s(#s(#s(#s(#s(#s(#0()))))))))))) ,::(#abs(#pos(#s(#s(#s(#s(#s(#s(#s(#0()))))))))) ,::(#abs(#pos(#s(#0()))) ,::(#abs(#pos(#s(#s(#0())))) ,::(#abs(#pos(#s(#s(#s(#s(#s(#s(#s(#s(#0())))))))))) ,::(#abs(#pos(#s(#s(#s(#s(#s(#s(#0())))))))),::(#abs(#pos(#s(#s(#s(#0()))))),nil())))))))))) Further, it can be verified that all rules not oriented are covered by the weightgap condition. ** Step 7.b:2: WeightGap WORST_CASE(?,O(n^2)) + Considered Problem: - Strict DPs: insert#(@x,@l) -> c_6(insert#1#(@l,@x)) insert#1#(::(@y,@ys),@x) -> c_7(insert#2#(#less(@y,@x),@x,@y,@ys)) insert#2#(#true(),@x,@y,@ys) -> c_10(insert#(@x,@ys)) insertD#(@x,@l) -> c_11(insertD#1#(@l,@x)) insertD#2#(#true(),@x,@y,@ys) -> c_15(insertD#(@x,@ys)) - Weak DPs: insertD#1#(::(@y,@ys),@x) -> c_12(insertD#2#(#less(@y,@x),@x,@y,@ys)) insertionsort#(@l) -> insertionsort#1#(@l) insertionsort#1#(::(@x,@xs)) -> insert#(@x,insertionsort(@xs)) insertionsort#1#(::(@x,@xs)) -> insertionsort#(@xs) insertionsortD#(@l) -> insertionsortD#1#(@l) insertionsortD#1#(::(@x,@xs)) -> insertD#(@x,insertionsortD(@xs)) insertionsortD#1#(::(@x,@xs)) -> insertionsortD#(@xs) testInsertionsort#(@x) -> insertionsort#(testList(#unit())) testInsertionsortD#(@x) -> insertionsortD#(testList(#unit())) - Weak TRS: #abs(#0()) -> #0() #abs(#pos(@x)) -> #pos(@x) #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) #less(@x,@y) -> #cklt(#compare(@x,@y)) insert(@x,@l) -> insert#1(@l,@x) insert#1(::(@y,@ys),@x) -> insert#2(#less(@y,@x),@x,@y,@ys) insert#1(nil(),@x) -> ::(@x,nil()) insert#2(#false(),@x,@y,@ys) -> ::(@x,::(@y,@ys)) insert#2(#true(),@x,@y,@ys) -> ::(@y,insert(@x,@ys)) insertD(@x,@l) -> insertD#1(@l,@x) insertD#1(::(@y,@ys),@x) -> insertD#2(#less(@y,@x),@x,@y,@ys) insertD#1(nil(),@x) -> ::(@x,nil()) insertD#2(#false(),@x,@y,@ys) -> ::(@x,::(@y,@ys)) insertD#2(#true(),@x,@y,@ys) -> ::(@y,insertD(@x,@ys)) insertionsort(@l) -> insertionsort#1(@l) insertionsort#1(::(@x,@xs)) -> insert(@x,insertionsort(@xs)) insertionsort#1(nil()) -> nil() insertionsortD(@l) -> insertionsortD#1(@l) insertionsortD#1(::(@x,@xs)) -> insertD(@x,insertionsortD(@xs)) insertionsortD#1(nil()) -> nil() testList(@_) -> ::(#abs(#0()) ,::(#abs(#pos(#s(#s(#s(#s(#0())))))) ,::(#abs(#pos(#s(#s(#s(#s(#s(#0()))))))) ,::(#abs(#pos(#s(#s(#s(#s(#s(#s(#s(#s(#s(#0()))))))))))) ,::(#abs(#pos(#s(#s(#s(#s(#s(#s(#s(#0()))))))))) ,::(#abs(#pos(#s(#0()))) ,::(#abs(#pos(#s(#s(#0())))) ,::(#abs(#pos(#s(#s(#s(#s(#s(#s(#s(#s(#0())))))))))) ,::(#abs(#pos(#s(#s(#s(#s(#s(#s(#0())))))))) ,::(#abs(#pos(#s(#s(#s(#0()))))),nil())))))))))) - Signature: {#abs/1,#cklt/1,#compare/2,#less/2,insert/2,insert#1/2,insert#2/4,insertD/2,insertD#1/2,insertD#2/4 ,insertionsort/1,insertionsort#1/1,insertionsortD/1,insertionsortD#1/1,testInsertionsort/1 ,testInsertionsortD/1,testList/1,#abs#/1,#cklt#/1,#compare#/2,#less#/2,insert#/2,insert#1#/2,insert#2#/4 ,insertD#/2,insertD#1#/2,insertD#2#/4,insertionsort#/1,insertionsort#1#/1,insertionsortD#/1 ,insertionsortD#1#/1,testInsertionsort#/1,testInsertionsortD#/1,testList#/1} / {#0/0,#EQ/0,#GT/0,#LT/0 ,#false/0,#neg/1,#pos/1,#s/1,#true/0,#unit/0,::/2,nil/0,c_1/0,c_2/0,c_3/0,c_4/0,c_5/2,c_6/1,c_7/1,c_8/0 ,c_9/0,c_10/1,c_11/1,c_12/1,c_13/0,c_14/0,c_15/1,c_16/1,c_17/2,c_18/0,c_19/1,c_20/2,c_21/0,c_22/1,c_23/1 ,c_24/10,c_25/0,c_26/0,c_27/0,c_28/0,c_29/0,c_30/0,c_31/0,c_32/0,c_33/1,c_34/0,c_35/0,c_36/0,c_37/1,c_38/0 ,c_39/1} - Obligation: innermost runtime complexity wrt. defined symbols {#abs#,#cklt#,#compare#,#less#,insert#,insert#1#,insert#2# ,insertD#,insertD#1#,insertD#2#,insertionsort#,insertionsort#1#,insertionsortD#,insertionsortD#1# ,testInsertionsort#,testInsertionsortD#,testList#} and constructors {#0,#EQ,#GT,#LT,#false,#neg,#pos,#s ,#true,#unit,::,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(#cklt) = {1}, uargs(::) = {1,2}, uargs(insert) = {2}, uargs(insert#2) = {1}, uargs(insertD) = {2}, uargs(insertD#2) = {1}, uargs(insert#) = {2}, uargs(insert#2#) = {1}, uargs(insertD#) = {2}, uargs(insertD#2#) = {1}, uargs(insertionsort#) = {1}, uargs(insertionsortD#) = {1}, uargs(c_6) = {1}, uargs(c_7) = {1}, uargs(c_10) = {1}, uargs(c_11) = {1}, uargs(c_12) = {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(#abs) = [0] p(#cklt) = [1] x1 + [0] p(#compare) = [0] p(#false) = [0] p(#less) = [0] p(#neg) = [1] x1 + [0] p(#pos) = [0] p(#s) = [0] p(#true) = [0] p(#unit) = [0] p(::) = [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(insertD) = [1] x1 + [1] x2 + [0] p(insertD#1) = [1] x1 + [1] x2 + [0] p(insertD#2) = [1] x1 + [1] x2 + [1] x3 + [1] x4 + [0] p(insertionsort) = [1] x1 + [0] p(insertionsort#1) = [1] x1 + [0] p(insertionsortD) = [1] x1 + [0] p(insertionsortD#1) = [1] x1 + [0] p(nil) = [2] p(testInsertionsort) = [1] x1 + [1] p(testInsertionsortD) = [4] x1 + [2] p(testList) = [1] x1 + [3] p(#abs#) = [4] p(#cklt#) = [2] x1 + [1] p(#compare#) = [0] p(#less#) = [1] x1 + [1] x2 + [0] p(insert#) = [1] x2 + [0] p(insert#1#) = [1] x1 + [1] p(insert#2#) = [1] x1 + [1] x3 + [1] x4 + [6] p(insertD#) = [1] x1 + [1] x2 + [0] p(insertD#1#) = [1] x1 + [1] x2 + [4] p(insertD#2#) = [1] x1 + [1] x2 + [1] x4 + [0] p(insertionsort#) = [1] x1 + [1] p(insertionsort#1#) = [1] x1 + [1] p(insertionsortD#) = [1] x1 + [0] p(insertionsortD#1#) = [1] x1 + [0] p(testInsertionsort#) = [4] x1 + [4] p(testInsertionsortD#) = [5] p(testList#) = [1] x1 + [0] p(c_1) = [4] p(c_2) = [1] p(c_3) = [1] p(c_4) = [1] p(c_5) = [4] p(c_6) = [1] x1 + [0] p(c_7) = [1] x1 + [2] p(c_8) = [1] p(c_9) = [0] p(c_10) = [1] x1 + [1] p(c_11) = [1] x1 + [2] p(c_12) = [1] x1 + [2] p(c_13) = [1] p(c_14) = [2] p(c_15) = [1] x1 + [0] p(c_16) = [4] p(c_17) = [1] x1 + [0] p(c_18) = [2] p(c_19) = [1] x1 + [2] p(c_20) = [1] p(c_21) = [4] p(c_22) = [1] p(c_23) = [2] p(c_24) = [1] x3 + [1] x4 + [1] x7 + [4] x8 + [2] x10 + [0] p(c_25) = [0] p(c_26) = [1] p(c_27) = [0] p(c_28) = [0] p(c_29) = [0] p(c_30) = [0] p(c_31) = [2] p(c_32) = [0] p(c_33) = [1] x1 + [0] p(c_34) = [0] p(c_35) = [1] p(c_36) = [1] p(c_37) = [2] x1 + [2] p(c_38) = [1] p(c_39) = [4] x1 + [0] Following rules are strictly oriented: insert#2#(#true(),@x,@y,@ys) = [1] @y + [1] @ys + [6] > [1] @ys + [1] = c_10(insert#(@x,@ys)) Following rules are (at-least) weakly oriented: insert#(@x,@l) = [1] @l + [0] >= [1] @l + [1] = c_6(insert#1#(@l,@x)) insert#1#(::(@y,@ys),@x) = [1] @y + [1] @ys + [1] >= [1] @y + [1] @ys + [8] = c_7(insert#2#(#less(@y,@x),@x,@y,@ys)) insertD#(@x,@l) = [1] @l + [1] @x + [0] >= [1] @l + [1] @x + [6] = c_11(insertD#1#(@l,@x)) insertD#1#(::(@y,@ys),@x) = [1] @x + [1] @y + [1] @ys + [4] >= [1] @x + [1] @ys + [2] = c_12(insertD#2#(#less(@y,@x),@x,@y,@ys)) insertD#2#(#true(),@x,@y,@ys) = [1] @x + [1] @ys + [0] >= [1] @x + [1] @ys + [0] = c_15(insertD#(@x,@ys)) insertionsort#(@l) = [1] @l + [1] >= [1] @l + [1] = insertionsort#1#(@l) insertionsort#1#(::(@x,@xs)) = [1] @x + [1] @xs + [1] >= [1] @xs + [0] = insert#(@x,insertionsort(@xs)) insertionsort#1#(::(@x,@xs)) = [1] @x + [1] @xs + [1] >= [1] @xs + [1] = insertionsort#(@xs) insertionsortD#(@l) = [1] @l + [0] >= [1] @l + [0] = insertionsortD#1#(@l) insertionsortD#1#(::(@x,@xs)) = [1] @x + [1] @xs + [0] >= [1] @x + [1] @xs + [0] = insertD#(@x,insertionsortD(@xs)) insertionsortD#1#(::(@x,@xs)) = [1] @x + [1] @xs + [0] >= [1] @xs + [0] = insertionsortD#(@xs) testInsertionsort#(@x) = [4] @x + [4] >= [4] = insertionsort#(testList(#unit())) testInsertionsortD#(@x) = [5] >= [3] = insertionsortD#(testList(#unit())) #abs(#0()) = [0] >= [0] = #0() #abs(#pos(@x)) = [0] >= [0] = #pos(@x) #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) #less(@x,@y) = [0] >= [0] = #cklt(#compare(@x,@y)) 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 + [0] >= [1] @x + [1] @y + [1] @ys + [0] = insert#2(#less(@y,@x),@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 + [0] >= [1] @x + [1] @y + [1] @ys + [0] = ::(@x,::(@y,@ys)) insert#2(#true(),@x,@y,@ys) = [1] @x + [1] @y + [1] @ys + [0] >= [1] @x + [1] @y + [1] @ys + [0] = ::(@y,insert(@x,@ys)) insertD(@x,@l) = [1] @l + [1] @x + [0] >= [1] @l + [1] @x + [0] = insertD#1(@l,@x) insertD#1(::(@y,@ys),@x) = [1] @x + [1] @y + [1] @ys + [0] >= [1] @x + [1] @y + [1] @ys + [0] = insertD#2(#less(@y,@x),@x,@y,@ys) insertD#1(nil(),@x) = [1] @x + [2] >= [1] @x + [2] = ::(@x,nil()) insertD#2(#false(),@x,@y,@ys) = [1] @x + [1] @y + [1] @ys + [0] >= [1] @x + [1] @y + [1] @ys + [0] = ::(@x,::(@y,@ys)) insertD#2(#true(),@x,@y,@ys) = [1] @x + [1] @y + [1] @ys + [0] >= [1] @x + [1] @y + [1] @ys + [0] = ::(@y,insertD(@x,@ys)) insertionsort(@l) = [1] @l + [0] >= [1] @l + [0] = insertionsort#1(@l) insertionsort#1(::(@x,@xs)) = [1] @x + [1] @xs + [0] >= [1] @x + [1] @xs + [0] = insert(@x,insertionsort(@xs)) insertionsort#1(nil()) = [2] >= [2] = nil() insertionsortD(@l) = [1] @l + [0] >= [1] @l + [0] = insertionsortD#1(@l) insertionsortD#1(::(@x,@xs)) = [1] @x + [1] @xs + [0] >= [1] @x + [1] @xs + [0] = insertD(@x,insertionsortD(@xs)) insertionsortD#1(nil()) = [2] >= [2] = nil() testList(@_) = [1] @_ + [3] >= [2] = ::(#abs(#0()) ,::(#abs(#pos(#s(#s(#s(#s(#0())))))) ,::(#abs(#pos(#s(#s(#s(#s(#s(#0()))))))) ,::(#abs(#pos(#s(#s(#s(#s(#s(#s(#s(#s(#s(#0()))))))))))) ,::(#abs(#pos(#s(#s(#s(#s(#s(#s(#s(#0()))))))))) ,::(#abs(#pos(#s(#0()))) ,::(#abs(#pos(#s(#s(#0())))) ,::(#abs(#pos(#s(#s(#s(#s(#s(#s(#s(#s(#0())))))))))) ,::(#abs(#pos(#s(#s(#s(#s(#s(#s(#0())))))))),::(#abs(#pos(#s(#s(#s(#0()))))),nil())))))))))) Further, it can be verified that all rules not oriented are covered by the weightgap condition. ** Step 7.b:3: WeightGap WORST_CASE(?,O(n^2)) + Considered Problem: - Strict DPs: insert#(@x,@l) -> c_6(insert#1#(@l,@x)) insert#1#(::(@y,@ys),@x) -> c_7(insert#2#(#less(@y,@x),@x,@y,@ys)) insertD#(@x,@l) -> c_11(insertD#1#(@l,@x)) insertD#2#(#true(),@x,@y,@ys) -> c_15(insertD#(@x,@ys)) - Weak DPs: insert#2#(#true(),@x,@y,@ys) -> c_10(insert#(@x,@ys)) insertD#1#(::(@y,@ys),@x) -> c_12(insertD#2#(#less(@y,@x),@x,@y,@ys)) insertionsort#(@l) -> insertionsort#1#(@l) insertionsort#1#(::(@x,@xs)) -> insert#(@x,insertionsort(@xs)) insertionsort#1#(::(@x,@xs)) -> insertionsort#(@xs) insertionsortD#(@l) -> insertionsortD#1#(@l) insertionsortD#1#(::(@x,@xs)) -> insertD#(@x,insertionsortD(@xs)) insertionsortD#1#(::(@x,@xs)) -> insertionsortD#(@xs) testInsertionsort#(@x) -> insertionsort#(testList(#unit())) testInsertionsortD#(@x) -> insertionsortD#(testList(#unit())) - Weak TRS: #abs(#0()) -> #0() #abs(#pos(@x)) -> #pos(@x) #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) #less(@x,@y) -> #cklt(#compare(@x,@y)) insert(@x,@l) -> insert#1(@l,@x) insert#1(::(@y,@ys),@x) -> insert#2(#less(@y,@x),@x,@y,@ys) insert#1(nil(),@x) -> ::(@x,nil()) insert#2(#false(),@x,@y,@ys) -> ::(@x,::(@y,@ys)) insert#2(#true(),@x,@y,@ys) -> ::(@y,insert(@x,@ys)) insertD(@x,@l) -> insertD#1(@l,@x) insertD#1(::(@y,@ys),@x) -> insertD#2(#less(@y,@x),@x,@y,@ys) insertD#1(nil(),@x) -> ::(@x,nil()) insertD#2(#false(),@x,@y,@ys) -> ::(@x,::(@y,@ys)) insertD#2(#true(),@x,@y,@ys) -> ::(@y,insertD(@x,@ys)) insertionsort(@l) -> insertionsort#1(@l) insertionsort#1(::(@x,@xs)) -> insert(@x,insertionsort(@xs)) insertionsort#1(nil()) -> nil() insertionsortD(@l) -> insertionsortD#1(@l) insertionsortD#1(::(@x,@xs)) -> insertD(@x,insertionsortD(@xs)) insertionsortD#1(nil()) -> nil() testList(@_) -> ::(#abs(#0()) ,::(#abs(#pos(#s(#s(#s(#s(#0())))))) ,::(#abs(#pos(#s(#s(#s(#s(#s(#0()))))))) ,::(#abs(#pos(#s(#s(#s(#s(#s(#s(#s(#s(#s(#0()))))))))))) ,::(#abs(#pos(#s(#s(#s(#s(#s(#s(#s(#0()))))))))) ,::(#abs(#pos(#s(#0()))) ,::(#abs(#pos(#s(#s(#0())))) ,::(#abs(#pos(#s(#s(#s(#s(#s(#s(#s(#s(#0())))))))))) ,::(#abs(#pos(#s(#s(#s(#s(#s(#s(#0())))))))) ,::(#abs(#pos(#s(#s(#s(#0()))))),nil())))))))))) - Signature: {#abs/1,#cklt/1,#compare/2,#less/2,insert/2,insert#1/2,insert#2/4,insertD/2,insertD#1/2,insertD#2/4 ,insertionsort/1,insertionsort#1/1,insertionsortD/1,insertionsortD#1/1,testInsertionsort/1 ,testInsertionsortD/1,testList/1,#abs#/1,#cklt#/1,#compare#/2,#less#/2,insert#/2,insert#1#/2,insert#2#/4 ,insertD#/2,insertD#1#/2,insertD#2#/4,insertionsort#/1,insertionsort#1#/1,insertionsortD#/1 ,insertionsortD#1#/1,testInsertionsort#/1,testInsertionsortD#/1,testList#/1} / {#0/0,#EQ/0,#GT/0,#LT/0 ,#false/0,#neg/1,#pos/1,#s/1,#true/0,#unit/0,::/2,nil/0,c_1/0,c_2/0,c_3/0,c_4/0,c_5/2,c_6/1,c_7/1,c_8/0 ,c_9/0,c_10/1,c_11/1,c_12/1,c_13/0,c_14/0,c_15/1,c_16/1,c_17/2,c_18/0,c_19/1,c_20/2,c_21/0,c_22/1,c_23/1 ,c_24/10,c_25/0,c_26/0,c_27/0,c_28/0,c_29/0,c_30/0,c_31/0,c_32/0,c_33/1,c_34/0,c_35/0,c_36/0,c_37/1,c_38/0 ,c_39/1} - Obligation: innermost runtime complexity wrt. defined symbols {#abs#,#cklt#,#compare#,#less#,insert#,insert#1#,insert#2# ,insertD#,insertD#1#,insertD#2#,insertionsort#,insertionsort#1#,insertionsortD#,insertionsortD#1# ,testInsertionsort#,testInsertionsortD#,testList#} and constructors {#0,#EQ,#GT,#LT,#false,#neg,#pos,#s ,#true,#unit,::,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(#cklt) = {1}, uargs(::) = {1,2}, uargs(insert) = {2}, uargs(insert#2) = {1}, uargs(insertD) = {2}, uargs(insertD#2) = {1}, uargs(insert#) = {2}, uargs(insert#2#) = {1}, uargs(insertD#) = {2}, uargs(insertD#2#) = {1}, uargs(insertionsort#) = {1}, uargs(insertionsortD#) = {1}, uargs(c_6) = {1}, uargs(c_7) = {1}, uargs(c_10) = {1}, uargs(c_11) = {1}, uargs(c_12) = {1}, uargs(c_15) = {1} Following symbols are considered usable: all TcT has computed the following interpretation: p(#0) = [4] p(#EQ) = [0] p(#GT) = [0] p(#LT) = [0] p(#abs) = [1] x1 + [0] p(#cklt) = [1] x1 + [0] p(#compare) = [0] p(#false) = [0] p(#less) = [0] p(#neg) = [1] x1 + [1] p(#pos) = [0] p(#s) = [1] x1 + [1] p(#true) = [0] p(#unit) = [1] p(::) = [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(insertD) = [1] x1 + [1] x2 + [0] p(insertD#1) = [1] x1 + [1] x2 + [0] p(insertD#2) = [1] x1 + [1] x2 + [1] x3 + [1] x4 + [0] p(insertionsort) = [1] x1 + [0] p(insertionsort#1) = [1] x1 + [0] p(insertionsortD) = [1] x1 + [1] p(insertionsortD#1) = [1] x1 + [1] p(nil) = [0] p(testInsertionsort) = [4] x1 + [1] p(testInsertionsortD) = [1] x1 + [1] p(testList) = [1] x1 + [4] p(#abs#) = [1] x1 + [2] p(#cklt#) = [1] x1 + [0] p(#compare#) = [1] x1 + [0] p(#less#) = [1] x1 + [0] p(insert#) = [1] x2 + [2] p(insert#1#) = [1] x1 + [7] p(insert#2#) = [1] x1 + [1] x4 + [4] p(insertD#) = [1] x2 + [0] p(insertD#1#) = [1] x1 + [1] p(insertD#2#) = [1] x1 + [1] x3 + [1] x4 + [0] p(insertionsort#) = [1] x1 + [2] p(insertionsort#1#) = [1] x1 + [2] p(insertionsortD#) = [1] x1 + [1] p(insertionsortD#1#) = [1] x1 + [1] p(testInsertionsort#) = [7] p(testInsertionsortD#) = [6] p(testList#) = [0] p(c_1) = [1] p(c_2) = [1] p(c_3) = [1] p(c_4) = [1] p(c_5) = [1] x1 + [1] x2 + [0] p(c_6) = [1] x1 + [2] p(c_7) = [1] x1 + [2] p(c_8) = [1] p(c_9) = [0] p(c_10) = [1] x1 + [0] p(c_11) = [1] x1 + [4] p(c_12) = [1] x1 + [0] p(c_13) = [2] p(c_14) = [1] p(c_15) = [1] x1 + [0] p(c_16) = [2] x1 + [1] p(c_17) = [1] x1 + [2] x2 + [1] p(c_18) = [1] p(c_19) = [4] x1 + [1] p(c_20) = [4] x1 + [2] x2 + [4] p(c_21) = [1] p(c_22) = [4] x1 + [2] p(c_23) = [1] p(c_24) = [1] x1 + [2] x2 + [1] x4 + [1] x6 + [4] x7 + [1] x8 + [1] x9 + [2] x10 + [1] p(c_25) = [4] p(c_26) = [0] p(c_27) = [2] p(c_28) = [1] p(c_29) = [0] p(c_30) = [4] p(c_31) = [0] p(c_32) = [2] p(c_33) = [1] x1 + [2] p(c_34) = [1] p(c_35) = [0] p(c_36) = [1] p(c_37) = [4] x1 + [0] p(c_38) = [0] p(c_39) = [2] Following rules are strictly oriented: insert#1#(::(@y,@ys),@x) = [1] @y + [1] @ys + [7] > [1] @ys + [6] = c_7(insert#2#(#less(@y,@x),@x,@y,@ys)) Following rules are (at-least) weakly oriented: insert#(@x,@l) = [1] @l + [2] >= [1] @l + [9] = c_6(insert#1#(@l,@x)) insert#2#(#true(),@x,@y,@ys) = [1] @ys + [4] >= [1] @ys + [2] = c_10(insert#(@x,@ys)) insertD#(@x,@l) = [1] @l + [0] >= [1] @l + [5] = c_11(insertD#1#(@l,@x)) insertD#1#(::(@y,@ys),@x) = [1] @y + [1] @ys + [1] >= [1] @y + [1] @ys + [0] = c_12(insertD#2#(#less(@y,@x),@x,@y,@ys)) insertD#2#(#true(),@x,@y,@ys) = [1] @y + [1] @ys + [0] >= [1] @ys + [0] = c_15(insertD#(@x,@ys)) insertionsort#(@l) = [1] @l + [2] >= [1] @l + [2] = insertionsort#1#(@l) insertionsort#1#(::(@x,@xs)) = [1] @x + [1] @xs + [2] >= [1] @xs + [2] = insert#(@x,insertionsort(@xs)) insertionsort#1#(::(@x,@xs)) = [1] @x + [1] @xs + [2] >= [1] @xs + [2] = insertionsort#(@xs) insertionsortD#(@l) = [1] @l + [1] >= [1] @l + [1] = insertionsortD#1#(@l) insertionsortD#1#(::(@x,@xs)) = [1] @x + [1] @xs + [1] >= [1] @xs + [1] = insertD#(@x,insertionsortD(@xs)) insertionsortD#1#(::(@x,@xs)) = [1] @x + [1] @xs + [1] >= [1] @xs + [1] = insertionsortD#(@xs) testInsertionsort#(@x) = [7] >= [7] = insertionsort#(testList(#unit())) testInsertionsortD#(@x) = [6] >= [6] = insertionsortD#(testList(#unit())) #abs(#0()) = [4] >= [4] = #0() #abs(#pos(@x)) = [0] >= [0] = #pos(@x) #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) #less(@x,@y) = [0] >= [0] = #cklt(#compare(@x,@y)) 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 + [0] >= [1] @x + [1] @y + [1] @ys + [0] = insert#2(#less(@y,@x),@x,@y,@ys) insert#1(nil(),@x) = [1] @x + [0] >= [1] @x + [0] = ::(@x,nil()) insert#2(#false(),@x,@y,@ys) = [1] @x + [1] @y + [1] @ys + [0] >= [1] @x + [1] @y + [1] @ys + [0] = ::(@x,::(@y,@ys)) insert#2(#true(),@x,@y,@ys) = [1] @x + [1] @y + [1] @ys + [0] >= [1] @x + [1] @y + [1] @ys + [0] = ::(@y,insert(@x,@ys)) insertD(@x,@l) = [1] @l + [1] @x + [0] >= [1] @l + [1] @x + [0] = insertD#1(@l,@x) insertD#1(::(@y,@ys),@x) = [1] @x + [1] @y + [1] @ys + [0] >= [1] @x + [1] @y + [1] @ys + [0] = insertD#2(#less(@y,@x),@x,@y,@ys) insertD#1(nil(),@x) = [1] @x + [0] >= [1] @x + [0] = ::(@x,nil()) insertD#2(#false(),@x,@y,@ys) = [1] @x + [1] @y + [1] @ys + [0] >= [1] @x + [1] @y + [1] @ys + [0] = ::(@x,::(@y,@ys)) insertD#2(#true(),@x,@y,@ys) = [1] @x + [1] @y + [1] @ys + [0] >= [1] @x + [1] @y + [1] @ys + [0] = ::(@y,insertD(@x,@ys)) insertionsort(@l) = [1] @l + [0] >= [1] @l + [0] = insertionsort#1(@l) insertionsort#1(::(@x,@xs)) = [1] @x + [1] @xs + [0] >= [1] @x + [1] @xs + [0] = insert(@x,insertionsort(@xs)) insertionsort#1(nil()) = [0] >= [0] = nil() insertionsortD(@l) = [1] @l + [1] >= [1] @l + [1] = insertionsortD#1(@l) insertionsortD#1(::(@x,@xs)) = [1] @x + [1] @xs + [1] >= [1] @x + [1] @xs + [1] = insertD(@x,insertionsortD(@xs)) insertionsortD#1(nil()) = [1] >= [0] = nil() testList(@_) = [1] @_ + [4] >= [4] = ::(#abs(#0()) ,::(#abs(#pos(#s(#s(#s(#s(#0())))))) ,::(#abs(#pos(#s(#s(#s(#s(#s(#0()))))))) ,::(#abs(#pos(#s(#s(#s(#s(#s(#s(#s(#s(#s(#0()))))))))))) ,::(#abs(#pos(#s(#s(#s(#s(#s(#s(#s(#0()))))))))) ,::(#abs(#pos(#s(#0()))) ,::(#abs(#pos(#s(#s(#0())))) ,::(#abs(#pos(#s(#s(#s(#s(#s(#s(#s(#s(#0())))))))))) ,::(#abs(#pos(#s(#s(#s(#s(#s(#s(#0())))))))),::(#abs(#pos(#s(#s(#s(#0()))))),nil())))))))))) Further, it can be verified that all rules not oriented are covered by the weightgap condition. ** Step 7.b:4: WeightGap WORST_CASE(?,O(n^2)) + Considered Problem: - Strict DPs: insert#(@x,@l) -> c_6(insert#1#(@l,@x)) insertD#(@x,@l) -> c_11(insertD#1#(@l,@x)) insertD#2#(#true(),@x,@y,@ys) -> c_15(insertD#(@x,@ys)) - Weak DPs: insert#1#(::(@y,@ys),@x) -> c_7(insert#2#(#less(@y,@x),@x,@y,@ys)) insert#2#(#true(),@x,@y,@ys) -> c_10(insert#(@x,@ys)) insertD#1#(::(@y,@ys),@x) -> c_12(insertD#2#(#less(@y,@x),@x,@y,@ys)) insertionsort#(@l) -> insertionsort#1#(@l) insertionsort#1#(::(@x,@xs)) -> insert#(@x,insertionsort(@xs)) insertionsort#1#(::(@x,@xs)) -> insertionsort#(@xs) insertionsortD#(@l) -> insertionsortD#1#(@l) insertionsortD#1#(::(@x,@xs)) -> insertD#(@x,insertionsortD(@xs)) insertionsortD#1#(::(@x,@xs)) -> insertionsortD#(@xs) testInsertionsort#(@x) -> insertionsort#(testList(#unit())) testInsertionsortD#(@x) -> insertionsortD#(testList(#unit())) - Weak TRS: #abs(#0()) -> #0() #abs(#pos(@x)) -> #pos(@x) #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) #less(@x,@y) -> #cklt(#compare(@x,@y)) insert(@x,@l) -> insert#1(@l,@x) insert#1(::(@y,@ys),@x) -> insert#2(#less(@y,@x),@x,@y,@ys) insert#1(nil(),@x) -> ::(@x,nil()) insert#2(#false(),@x,@y,@ys) -> ::(@x,::(@y,@ys)) insert#2(#true(),@x,@y,@ys) -> ::(@y,insert(@x,@ys)) insertD(@x,@l) -> insertD#1(@l,@x) insertD#1(::(@y,@ys),@x) -> insertD#2(#less(@y,@x),@x,@y,@ys) insertD#1(nil(),@x) -> ::(@x,nil()) insertD#2(#false(),@x,@y,@ys) -> ::(@x,::(@y,@ys)) insertD#2(#true(),@x,@y,@ys) -> ::(@y,insertD(@x,@ys)) insertionsort(@l) -> insertionsort#1(@l) insertionsort#1(::(@x,@xs)) -> insert(@x,insertionsort(@xs)) insertionsort#1(nil()) -> nil() insertionsortD(@l) -> insertionsortD#1(@l) insertionsortD#1(::(@x,@xs)) -> insertD(@x,insertionsortD(@xs)) insertionsortD#1(nil()) -> nil() testList(@_) -> ::(#abs(#0()) ,::(#abs(#pos(#s(#s(#s(#s(#0())))))) ,::(#abs(#pos(#s(#s(#s(#s(#s(#0()))))))) ,::(#abs(#pos(#s(#s(#s(#s(#s(#s(#s(#s(#s(#0()))))))))))) ,::(#abs(#pos(#s(#s(#s(#s(#s(#s(#s(#0()))))))))) ,::(#abs(#pos(#s(#0()))) ,::(#abs(#pos(#s(#s(#0())))) ,::(#abs(#pos(#s(#s(#s(#s(#s(#s(#s(#s(#0())))))))))) ,::(#abs(#pos(#s(#s(#s(#s(#s(#s(#0())))))))) ,::(#abs(#pos(#s(#s(#s(#0()))))),nil())))))))))) - Signature: {#abs/1,#cklt/1,#compare/2,#less/2,insert/2,insert#1/2,insert#2/4,insertD/2,insertD#1/2,insertD#2/4 ,insertionsort/1,insertionsort#1/1,insertionsortD/1,insertionsortD#1/1,testInsertionsort/1 ,testInsertionsortD/1,testList/1,#abs#/1,#cklt#/1,#compare#/2,#less#/2,insert#/2,insert#1#/2,insert#2#/4 ,insertD#/2,insertD#1#/2,insertD#2#/4,insertionsort#/1,insertionsort#1#/1,insertionsortD#/1 ,insertionsortD#1#/1,testInsertionsort#/1,testInsertionsortD#/1,testList#/1} / {#0/0,#EQ/0,#GT/0,#LT/0 ,#false/0,#neg/1,#pos/1,#s/1,#true/0,#unit/0,::/2,nil/0,c_1/0,c_2/0,c_3/0,c_4/0,c_5/2,c_6/1,c_7/1,c_8/0 ,c_9/0,c_10/1,c_11/1,c_12/1,c_13/0,c_14/0,c_15/1,c_16/1,c_17/2,c_18/0,c_19/1,c_20/2,c_21/0,c_22/1,c_23/1 ,c_24/10,c_25/0,c_26/0,c_27/0,c_28/0,c_29/0,c_30/0,c_31/0,c_32/0,c_33/1,c_34/0,c_35/0,c_36/0,c_37/1,c_38/0 ,c_39/1} - Obligation: innermost runtime complexity wrt. defined symbols {#abs#,#cklt#,#compare#,#less#,insert#,insert#1#,insert#2# ,insertD#,insertD#1#,insertD#2#,insertionsort#,insertionsort#1#,insertionsortD#,insertionsortD#1# ,testInsertionsort#,testInsertionsortD#,testList#} and constructors {#0,#EQ,#GT,#LT,#false,#neg,#pos,#s ,#true,#unit,::,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(#cklt) = {1}, uargs(::) = {1,2}, uargs(insert) = {2}, uargs(insert#2) = {1}, uargs(insertD) = {2}, uargs(insertD#2) = {1}, uargs(insert#) = {2}, uargs(insert#2#) = {1}, uargs(insertD#) = {2}, uargs(insertD#2#) = {1}, uargs(insertionsort#) = {1}, uargs(insertionsortD#) = {1}, uargs(c_6) = {1}, uargs(c_7) = {1}, uargs(c_10) = {1}, uargs(c_11) = {1}, uargs(c_12) = {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(#abs) = [0] p(#cklt) = [1] x1 + [0] p(#compare) = [0] p(#false) = [0] p(#less) = [0] p(#neg) = [0] p(#pos) = [0] p(#s) = [1] x1 + [1] p(#true) = [0] p(#unit) = [1] p(::) = [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(insertD) = [1] x1 + [1] x2 + [0] p(insertD#1) = [1] x1 + [1] x2 + [0] p(insertD#2) = [1] x1 + [1] x2 + [1] x3 + [1] x4 + [0] p(insertionsort) = [1] x1 + [0] p(insertionsort#1) = [1] x1 + [0] p(insertionsortD) = [1] x1 + [0] p(insertionsortD#1) = [1] x1 + [0] p(nil) = [0] p(testInsertionsort) = [1] x1 + [1] p(testInsertionsortD) = [2] x1 + [0] p(testList) = [1] x1 + [1] p(#abs#) = [2] x1 + [2] p(#cklt#) = [1] x1 + [0] p(#compare#) = [1] x1 + [1] x2 + [0] p(#less#) = [4] x2 + [0] p(insert#) = [1] x2 + [0] p(insert#1#) = [1] x1 + [4] p(insert#2#) = [1] x1 + [1] x3 + [1] x4 + [1] p(insertD#) = [1] x2 + [0] p(insertD#1#) = [1] x1 + [3] p(insertD#2#) = [1] x1 + [1] x4 + [2] p(insertionsort#) = [1] x1 + [0] p(insertionsort#1#) = [1] x1 + [0] p(insertionsortD#) = [1] x1 + [0] p(insertionsortD#1#) = [1] x1 + [0] p(testInsertionsort#) = [1] x1 + [3] p(testInsertionsortD#) = [2] x1 + [4] p(testList#) = [0] p(c_1) = [1] p(c_2) = [0] p(c_3) = [1] p(c_4) = [1] p(c_5) = [4] x1 + [4] x2 + [0] p(c_6) = [1] x1 + [1] p(c_7) = [1] x1 + [3] p(c_8) = [0] p(c_9) = [2] p(c_10) = [1] x1 + [1] p(c_11) = [1] x1 + [4] p(c_12) = [1] x1 + [0] p(c_13) = [0] p(c_14) = [1] p(c_15) = [1] x1 + [0] p(c_16) = [0] p(c_17) = [1] x1 + [2] x2 + [0] p(c_18) = [0] p(c_19) = [4] p(c_20) = [4] x2 + [0] p(c_21) = [2] p(c_22) = [4] x1 + [0] p(c_23) = [1] x1 + [0] p(c_24) = [4] x2 + [1] x4 + [2] x5 + [1] x6 + [1] x7 + [1] x9 + [0] p(c_25) = [0] p(c_26) = [1] p(c_27) = [0] p(c_28) = [1] p(c_29) = [0] p(c_30) = [4] p(c_31) = [2] p(c_32) = [4] p(c_33) = [1] x1 + [0] p(c_34) = [0] p(c_35) = [1] p(c_36) = [1] p(c_37) = [2] p(c_38) = [0] p(c_39) = [4] x1 + [0] Following rules are strictly oriented: insertD#2#(#true(),@x,@y,@ys) = [1] @ys + [2] > [1] @ys + [0] = c_15(insertD#(@x,@ys)) Following rules are (at-least) weakly oriented: insert#(@x,@l) = [1] @l + [0] >= [1] @l + [5] = c_6(insert#1#(@l,@x)) insert#1#(::(@y,@ys),@x) = [1] @y + [1] @ys + [4] >= [1] @y + [1] @ys + [4] = c_7(insert#2#(#less(@y,@x),@x,@y,@ys)) insert#2#(#true(),@x,@y,@ys) = [1] @y + [1] @ys + [1] >= [1] @ys + [1] = c_10(insert#(@x,@ys)) insertD#(@x,@l) = [1] @l + [0] >= [1] @l + [7] = c_11(insertD#1#(@l,@x)) insertD#1#(::(@y,@ys),@x) = [1] @y + [1] @ys + [3] >= [1] @ys + [2] = c_12(insertD#2#(#less(@y,@x),@x,@y,@ys)) insertionsort#(@l) = [1] @l + [0] >= [1] @l + [0] = insertionsort#1#(@l) insertionsort#1#(::(@x,@xs)) = [1] @x + [1] @xs + [0] >= [1] @xs + [0] = insert#(@x,insertionsort(@xs)) insertionsort#1#(::(@x,@xs)) = [1] @x + [1] @xs + [0] >= [1] @xs + [0] = insertionsort#(@xs) insertionsortD#(@l) = [1] @l + [0] >= [1] @l + [0] = insertionsortD#1#(@l) insertionsortD#1#(::(@x,@xs)) = [1] @x + [1] @xs + [0] >= [1] @xs + [0] = insertD#(@x,insertionsortD(@xs)) insertionsortD#1#(::(@x,@xs)) = [1] @x + [1] @xs + [0] >= [1] @xs + [0] = insertionsortD#(@xs) testInsertionsort#(@x) = [1] @x + [3] >= [2] = insertionsort#(testList(#unit())) testInsertionsortD#(@x) = [2] @x + [4] >= [2] = insertionsortD#(testList(#unit())) #abs(#0()) = [0] >= [0] = #0() #abs(#pos(@x)) = [0] >= [0] = #pos(@x) #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) #less(@x,@y) = [0] >= [0] = #cklt(#compare(@x,@y)) 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 + [0] >= [1] @x + [1] @y + [1] @ys + [0] = insert#2(#less(@y,@x),@x,@y,@ys) insert#1(nil(),@x) = [1] @x + [0] >= [1] @x + [0] = ::(@x,nil()) insert#2(#false(),@x,@y,@ys) = [1] @x + [1] @y + [1] @ys + [0] >= [1] @x + [1] @y + [1] @ys + [0] = ::(@x,::(@y,@ys)) insert#2(#true(),@x,@y,@ys) = [1] @x + [1] @y + [1] @ys + [0] >= [1] @x + [1] @y + [1] @ys + [0] = ::(@y,insert(@x,@ys)) insertD(@x,@l) = [1] @l + [1] @x + [0] >= [1] @l + [1] @x + [0] = insertD#1(@l,@x) insertD#1(::(@y,@ys),@x) = [1] @x + [1] @y + [1] @ys + [0] >= [1] @x + [1] @y + [1] @ys + [0] = insertD#2(#less(@y,@x),@x,@y,@ys) insertD#1(nil(),@x) = [1] @x + [0] >= [1] @x + [0] = ::(@x,nil()) insertD#2(#false(),@x,@y,@ys) = [1] @x + [1] @y + [1] @ys + [0] >= [1] @x + [1] @y + [1] @ys + [0] = ::(@x,::(@y,@ys)) insertD#2(#true(),@x,@y,@ys) = [1] @x + [1] @y + [1] @ys + [0] >= [1] @x + [1] @y + [1] @ys + [0] = ::(@y,insertD(@x,@ys)) insertionsort(@l) = [1] @l + [0] >= [1] @l + [0] = insertionsort#1(@l) insertionsort#1(::(@x,@xs)) = [1] @x + [1] @xs + [0] >= [1] @x + [1] @xs + [0] = insert(@x,insertionsort(@xs)) insertionsort#1(nil()) = [0] >= [0] = nil() insertionsortD(@l) = [1] @l + [0] >= [1] @l + [0] = insertionsortD#1(@l) insertionsortD#1(::(@x,@xs)) = [1] @x + [1] @xs + [0] >= [1] @x + [1] @xs + [0] = insertD(@x,insertionsortD(@xs)) insertionsortD#1(nil()) = [0] >= [0] = nil() testList(@_) = [1] @_ + [1] >= [0] = ::(#abs(#0()) ,::(#abs(#pos(#s(#s(#s(#s(#0())))))) ,::(#abs(#pos(#s(#s(#s(#s(#s(#0()))))))) ,::(#abs(#pos(#s(#s(#s(#s(#s(#s(#s(#s(#s(#0()))))))))))) ,::(#abs(#pos(#s(#s(#s(#s(#s(#s(#s(#0()))))))))) ,::(#abs(#pos(#s(#0()))) ,::(#abs(#pos(#s(#s(#0())))) ,::(#abs(#pos(#s(#s(#s(#s(#s(#s(#s(#s(#0())))))))))) ,::(#abs(#pos(#s(#s(#s(#s(#s(#s(#0())))))))),::(#abs(#pos(#s(#s(#s(#0()))))),nil())))))))))) Further, it can be verified that all rules not oriented are covered by the weightgap condition. ** Step 7.b:5: Ara WORST_CASE(?,O(n^2)) + Considered Problem: - Strict DPs: insert#(@x,@l) -> c_6(insert#1#(@l,@x)) insertD#(@x,@l) -> c_11(insertD#1#(@l,@x)) - Weak DPs: insert#1#(::(@y,@ys),@x) -> c_7(insert#2#(#less(@y,@x),@x,@y,@ys)) insert#2#(#true(),@x,@y,@ys) -> c_10(insert#(@x,@ys)) insertD#1#(::(@y,@ys),@x) -> c_12(insertD#2#(#less(@y,@x),@x,@y,@ys)) insertD#2#(#true(),@x,@y,@ys) -> c_15(insertD#(@x,@ys)) insertionsort#(@l) -> insertionsort#1#(@l) insertionsort#1#(::(@x,@xs)) -> insert#(@x,insertionsort(@xs)) insertionsort#1#(::(@x,@xs)) -> insertionsort#(@xs) insertionsortD#(@l) -> insertionsortD#1#(@l) insertionsortD#1#(::(@x,@xs)) -> insertD#(@x,insertionsortD(@xs)) insertionsortD#1#(::(@x,@xs)) -> insertionsortD#(@xs) testInsertionsort#(@x) -> insertionsort#(testList(#unit())) testInsertionsortD#(@x) -> insertionsortD#(testList(#unit())) - Weak TRS: #abs(#0()) -> #0() #abs(#pos(@x)) -> #pos(@x) #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) #less(@x,@y) -> #cklt(#compare(@x,@y)) insert(@x,@l) -> insert#1(@l,@x) insert#1(::(@y,@ys),@x) -> insert#2(#less(@y,@x),@x,@y,@ys) insert#1(nil(),@x) -> ::(@x,nil()) insert#2(#false(),@x,@y,@ys) -> ::(@x,::(@y,@ys)) insert#2(#true(),@x,@y,@ys) -> ::(@y,insert(@x,@ys)) insertD(@x,@l) -> insertD#1(@l,@x) insertD#1(::(@y,@ys),@x) -> insertD#2(#less(@y,@x),@x,@y,@ys) insertD#1(nil(),@x) -> ::(@x,nil()) insertD#2(#false(),@x,@y,@ys) -> ::(@x,::(@y,@ys)) insertD#2(#true(),@x,@y,@ys) -> ::(@y,insertD(@x,@ys)) insertionsort(@l) -> insertionsort#1(@l) insertionsort#1(::(@x,@xs)) -> insert(@x,insertionsort(@xs)) insertionsort#1(nil()) -> nil() insertionsortD(@l) -> insertionsortD#1(@l) insertionsortD#1(::(@x,@xs)) -> insertD(@x,insertionsortD(@xs)) insertionsortD#1(nil()) -> nil() testList(@_) -> ::(#abs(#0()) ,::(#abs(#pos(#s(#s(#s(#s(#0())))))) ,::(#abs(#pos(#s(#s(#s(#s(#s(#0()))))))) ,::(#abs(#pos(#s(#s(#s(#s(#s(#s(#s(#s(#s(#0()))))))))))) ,::(#abs(#pos(#s(#s(#s(#s(#s(#s(#s(#0()))))))))) ,::(#abs(#pos(#s(#0()))) ,::(#abs(#pos(#s(#s(#0())))) ,::(#abs(#pos(#s(#s(#s(#s(#s(#s(#s(#s(#0())))))))))) ,::(#abs(#pos(#s(#s(#s(#s(#s(#s(#0())))))))) ,::(#abs(#pos(#s(#s(#s(#0()))))),nil())))))))))) - Signature: {#abs/1,#cklt/1,#compare/2,#less/2,insert/2,insert#1/2,insert#2/4,insertD/2,insertD#1/2,insertD#2/4 ,insertionsort/1,insertionsort#1/1,insertionsortD/1,insertionsortD#1/1,testInsertionsort/1 ,testInsertionsortD/1,testList/1,#abs#/1,#cklt#/1,#compare#/2,#less#/2,insert#/2,insert#1#/2,insert#2#/4 ,insertD#/2,insertD#1#/2,insertD#2#/4,insertionsort#/1,insertionsort#1#/1,insertionsortD#/1 ,insertionsortD#1#/1,testInsertionsort#/1,testInsertionsortD#/1,testList#/1} / {#0/0,#EQ/0,#GT/0,#LT/0 ,#false/0,#neg/1,#pos/1,#s/1,#true/0,#unit/0,::/2,nil/0,c_1/0,c_2/0,c_3/0,c_4/0,c_5/2,c_6/1,c_7/1,c_8/0 ,c_9/0,c_10/1,c_11/1,c_12/1,c_13/0,c_14/0,c_15/1,c_16/1,c_17/2,c_18/0,c_19/1,c_20/2,c_21/0,c_22/1,c_23/1 ,c_24/10,c_25/0,c_26/0,c_27/0,c_28/0,c_29/0,c_30/0,c_31/0,c_32/0,c_33/1,c_34/0,c_35/0,c_36/0,c_37/1,c_38/0 ,c_39/1} - Obligation: innermost runtime complexity wrt. defined symbols {#abs#,#cklt#,#compare#,#less#,insert#,insert#1#,insert#2# ,insertD#,insertD#1#,insertD#2#,insertionsort#,insertionsort#1#,insertionsortD#,insertionsortD#1# ,testInsertionsort#,testInsertionsortD#,testList#} and constructors {#0,#EQ,#GT,#LT,#false,#neg,#pos,#s ,#true,#unit,::,nil} + Applied Processor: Ara {araHeuristics = NoHeuristics, minDegree = 2, maxDegree = 2, araTimeout = 8, araRuleShifting = Just 1} + Details: Signatures used: ---------------- #0 :: [] -(0)-> "A"(1, 8) #0 :: [] -(0)-> "A"(0, 0) #0 :: [] -(0)-> "A"(13, 10) #0 :: [] -(0)-> "A"(15, 14) #0 :: [] -(0)-> "A"(15, 12) #0 :: [] -(0)-> "A"(14, 14) #0 :: [] -(0)-> "A"(14, 12) #EQ :: [] -(0)-> "A"(0, 0) #EQ :: [] -(0)-> "A"(12, 12) #GT :: [] -(0)-> "A"(0, 0) #GT :: [] -(0)-> "A"(12, 12) #LT :: [] -(0)-> "A"(0, 0) #LT :: [] -(0)-> "A"(12, 12) #abs :: ["A"(1, 8)] -(0)-> "A"(11, 4) #cklt :: ["A"(0, 0)] -(0)-> "A"(9, 9) #compare :: ["A"(0, 0) x "A"(0, 0)] -(0)-> "A"(10, 10) #false :: [] -(0)-> "A"(0, 0) #false :: [] -(0)-> "A"(15, 15) #less :: ["A"(0, 0) x "A"(0, 0)] -(0)-> "A"(0, 0) #neg :: ["A"(0, 0)] -(0)-> "A"(0, 0) #pos :: ["A"(0, 0)] -(0)-> "A"(1, 8) #pos :: ["A"(0, 0)] -(0)-> "A"(0, 0) #pos :: ["A"(0, 0)] -(0)-> "A"(11, 5) #pos :: ["A"(0, 0)] -(0)-> "A"(9, 13) #pos :: ["A"(0, 0)] -(0)-> "A"(9, 14) #pos :: ["A"(0, 0)] -(0)-> "A"(13, 14) #pos :: ["A"(0, 0)] -(0)-> "A"(5, 8) #pos :: ["A"(0, 0)] -(0)-> "A"(12, 12) #pos :: ["A"(0, 0)] -(0)-> "A"(13, 13) #pos :: ["A"(0, 0)] -(0)-> "A"(11, 13) #pos :: ["A"(0, 0)] -(0)-> "A"(11, 14) #s :: ["A"(0, 0)] -(0)-> "A"(0, 0) #s :: ["A"(12, 0)] -(0)-> "A"(12, 1) #s :: ["A"(12, 0)] -(0)-> "A"(12, 0) #s :: ["A"(12, 0)] -(0)-> "A"(12, 3) #s :: ["A"(14, 0)] -(0)-> "A"(14, 1) #s :: ["A"(8, 0)] -(0)-> "A"(8, 9) #s :: ["A"(11, 0)] -(0)-> "A"(11, 7) #s :: ["A"(11, 0)] -(0)-> "A"(11, 12) #s :: ["A"(11, 0)] -(0)-> "A"(11, 13) #s :: ["A"(13, 0)] -(0)-> "A"(13, 1) #s :: ["A"(0, 0)] -(0)-> "A"(0, 4) #s :: ["A"(2, 0)] -(0)-> "A"(2, 0) #s :: ["A"(2, 0)] -(0)-> "A"(2, 13) #s :: ["A"(15, 0)] -(0)-> "A"(15, 0) #s :: ["A"(9, 0)] -(0)-> "A"(9, 2) #s :: ["A"(9, 0)] -(0)-> "A"(9, 0) #s :: ["A"(9, 0)] -(0)-> "A"(9, 8) #s :: ["A"(9, 0)] -(0)-> "A"(9, 5) #s :: ["A"(6, 0)] -(0)-> "A"(6, 8) #s :: ["A"(8, 0)] -(0)-> "A"(8, 5) #s :: ["A"(13, 0)] -(0)-> "A"(13, 0) #s :: ["A"(1, 0)] -(0)-> "A"(1, 11) #s :: ["A"(1, 0)] -(0)-> "A"(1, 0) #s :: ["A"(4, 0)] -(0)-> "A"(4, 7) #s :: ["A"(4, 0)] -(0)-> "A"(4, 1) #s :: ["A"(4, 0)] -(0)-> "A"(4, 0) #s :: ["A"(4, 0)] -(0)-> "A"(4, 8) #s :: ["A"(5, 0)] -(0)-> "A"(5, 4) #s :: ["A"(8, 0)] -(0)-> "A"(8, 8) #s :: ["A"(9, 0)] -(0)-> "A"(9, 1) #s :: ["A"(12, 0)] -(0)-> "A"(12, 9) #true :: [] -(0)-> "A"(0, 0) #true :: [] -(0)-> "A"(15, 15) #unit :: [] -(0)-> "A"(7, 7) #unit :: [] -(0)-> "A"(15, 15) :: :: ["A"(0, 0) x "A"(7, 0)] -(0)-> "A"(7, 0) :: :: ["A"(1, 1) x "A"(10, 1)] -(1)-> "A"(10, 1) :: :: ["A"(1, 1) x "A"(1, 1)] -(1)-> "A"(1, 1) :: :: ["A"(0, 0) x "A"(6, 0)] -(0)-> "A"(6, 0) :: :: ["A"(1, 1) x "A"(8, 1)] -(1)-> "A"(8, 1) :: :: ["A"(0, 0) x "A"(10, 0)] -(0)-> "A"(10, 0) :: :: ["A"(1, 1) x "A"(13, 1)] -(1)-> "A"(13, 1) :: :: ["A"(1, 1) x "A"(2, 1)] -(1)-> "A"(2, 1) :: :: ["A"(1, 1) x "A"(4, 1)] -(1)-> "A"(4, 1) :: :: ["A"(1, 1) x "A"(9, 1)] -(1)-> "A"(9, 1) :: :: ["A"(1, 1) x "A"(14, 1)] -(1)-> "A"(14, 1) :: :: ["A"(1, 1) x "A"(15, 1)] -(1)-> "A"(15, 1) insert :: ["A"(1, 1) x "A"(7, 0)] -(0)-> "A"(7, 0) insert#1 :: ["A"(7, 0) x "A"(1, 1)] -(0)-> "A"(7, 0) insert#2 :: ["A"(0, 0) x "A"(1, 1) x "A"(0, 0) x "A"(7, 0)] -(0)-> "A"(7, 0) insertD :: ["A"(1, 1) x "A"(10, 1)] -(1)-> "A"(10, 1) insertD#1 :: ["A"(10, 1) x "A"(1, 1)] -(1)-> "A"(10, 1) insertD#2 :: ["A"(0, 0) x "A"(1, 1) x "A"(1, 1) x "A"(10, 1)] -(2)-> "A"(10, 1) insertionsort :: ["A"(1, 1)] -(1)-> "A"(7, 0) insertionsort#1 :: ["A"(1, 1)] -(1)-> "A"(7, 0) insertionsortD :: ["A"(1, 1)] -(1)-> "A"(10, 1) insertionsortD#1 :: ["A"(1, 1)] -(1)-> "A"(10, 1) nil :: [] -(0)-> "A"(7, 0) nil :: [] -(0)-> "A"(10, 1) nil :: [] -(0)-> "A"(1, 1) nil :: [] -(0)-> "A"(15, 13) nil :: [] -(0)-> "A"(15, 15) nil :: [] -(0)-> "A"(13, 7) testList :: ["A"(1, 1)] -(11)-> "A"(1, 1) insert# :: ["A"(0, 0) x "A"(6, 0)] -(0)-> "A"(1, 1) insert#1# :: ["A"(6, 0) x "A"(0, 0)] -(0)-> "A"(7, 1) insert#2# :: ["A"(0, 0) x "A"(0, 0) x "A"(0, 0) x "A"(6, 0)] -(0)-> "A"(1, 1) insertD# :: ["A"(0, 0) x "A"(8, 1)] -(1)-> "A"(5, 0) insertD#1# :: ["A"(8, 1) x "A"(0, 0)] -(0)-> "A"(5, 1) insertD#2# :: ["A"(0, 0) x "A"(0, 0) x "A"(0, 0) x "A"(8, 1)] -(1)-> "A"(12, 5) insertionsort# :: ["A"(1, 1)] -(0)-> "A"(0, 0) insertionsort#1# :: ["A"(1, 1)] -(0)-> "A"(0, 0) insertionsortD# :: ["A"(1, 1)] -(1)-> "A"(1, 0) insertionsortD#1# :: ["A"(1, 1)] -(1)-> "A"(1, 0) testInsertionsort# :: ["A"(0)] -(13)-> "A"(0, 0) testInsertionsortD# :: ["A"(0)] -(14)-> "A"(0, 0) c_6 :: ["A"(3, 0)] -(0)-> "A"(3, 3) c_7 :: ["A"(1, 1)] -(0)-> "A"(8, 1) c_10 :: ["A"(1, 1)] -(0)-> "A"(9, 1) c_11 :: ["A"(1, 0)] -(0)-> "A"(6, 1) c_12 :: ["A"(11, 1)] -(0)-> "A"(11, 1) c_15 :: ["A"(5, 0)] -(0)-> "A"(12, 5) Cost-free Signatures used: -------------------------- Base Constructor Signatures used: --------------------------------- "#0_A" :: [] -(0)-> "A"(0) "#EQ_A" :: [] -(0)-> "A"(0) "#GT_A" :: [] -(0)-> "A"(0) "#LT_A" :: [] -(0)-> "A"(0) "#false_A" :: [] -(0)-> "A"(0) "#neg_A" :: ["A"(0)] -(0)-> "A"(0) "#pos_A" :: ["A"(0)] -(0)-> "A"(0) "#s_A" :: ["A"(0)] -(0)-> "A"(0) "#true_A" :: [] -(0)-> "A"(0) "#unit_A" :: [] -(0)-> "A"(0) "::_A" :: ["A"(0) x "A"(0)] -(0)-> "A"(0) "c_10_A" :: ["A"(0)] -(0)-> "A"(1, 0) "c_10_A" :: ["A"(0)] -(0)-> "A"(0, 1) "c_11_A" :: ["A"(0)] -(0)-> "A"(1, 0) "c_11_A" :: ["A"(0)] -(0)-> "A"(0, 1) "c_12_A" :: ["A"(0)] -(0)-> "A"(1, 0) "c_12_A" :: ["A"(0)] -(0)-> "A"(0, 1) "c_15_A" :: ["A"(0)] -(0)-> "A"(1, 0) "c_15_A" :: ["A"(0)] -(0)-> "A"(0, 1) "c_6_A" :: ["A"(0)] -(0)-> "A"(1, 0) "c_6_A" :: ["A"(0)] -(0)-> "A"(0, 1) "c_7_A" :: ["A"(0)] -(0)-> "A"(1, 0) "c_7_A" :: ["A"(0)] -(0)-> "A"(0, 1) "nil_A" :: [] -(0)-> "A"(1, 0) "nil_A" :: [] -(0)-> "A"(0, 1) Following Still Strict Rules were Typed as: ------------------------------------------- 1. Strict: insertD#(@x,@l) -> c_11(insertD#1#(@l,@x)) 2. Weak: insert#(@x,@l) -> c_6(insert#1#(@l,@x)) ** Step 7.b:6: Ara WORST_CASE(?,O(n^2)) + Considered Problem: - Strict DPs: insert#(@x,@l) -> c_6(insert#1#(@l,@x)) - Weak DPs: insert#1#(::(@y,@ys),@x) -> c_7(insert#2#(#less(@y,@x),@x,@y,@ys)) insert#2#(#true(),@x,@y,@ys) -> c_10(insert#(@x,@ys)) insertD#(@x,@l) -> c_11(insertD#1#(@l,@x)) insertD#1#(::(@y,@ys),@x) -> c_12(insertD#2#(#less(@y,@x),@x,@y,@ys)) insertD#2#(#true(),@x,@y,@ys) -> c_15(insertD#(@x,@ys)) insertionsort#(@l) -> insertionsort#1#(@l) insertionsort#1#(::(@x,@xs)) -> insert#(@x,insertionsort(@xs)) insertionsort#1#(::(@x,@xs)) -> insertionsort#(@xs) insertionsortD#(@l) -> insertionsortD#1#(@l) insertionsortD#1#(::(@x,@xs)) -> insertD#(@x,insertionsortD(@xs)) insertionsortD#1#(::(@x,@xs)) -> insertionsortD#(@xs) testInsertionsort#(@x) -> insertionsort#(testList(#unit())) testInsertionsortD#(@x) -> insertionsortD#(testList(#unit())) - Weak TRS: #abs(#0()) -> #0() #abs(#pos(@x)) -> #pos(@x) #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) #less(@x,@y) -> #cklt(#compare(@x,@y)) insert(@x,@l) -> insert#1(@l,@x) insert#1(::(@y,@ys),@x) -> insert#2(#less(@y,@x),@x,@y,@ys) insert#1(nil(),@x) -> ::(@x,nil()) insert#2(#false(),@x,@y,@ys) -> ::(@x,::(@y,@ys)) insert#2(#true(),@x,@y,@ys) -> ::(@y,insert(@x,@ys)) insertD(@x,@l) -> insertD#1(@l,@x) insertD#1(::(@y,@ys),@x) -> insertD#2(#less(@y,@x),@x,@y,@ys) insertD#1(nil(),@x) -> ::(@x,nil()) insertD#2(#false(),@x,@y,@ys) -> ::(@x,::(@y,@ys)) insertD#2(#true(),@x,@y,@ys) -> ::(@y,insertD(@x,@ys)) insertionsort(@l) -> insertionsort#1(@l) insertionsort#1(::(@x,@xs)) -> insert(@x,insertionsort(@xs)) insertionsort#1(nil()) -> nil() insertionsortD(@l) -> insertionsortD#1(@l) insertionsortD#1(::(@x,@xs)) -> insertD(@x,insertionsortD(@xs)) insertionsortD#1(nil()) -> nil() testList(@_) -> ::(#abs(#0()) ,::(#abs(#pos(#s(#s(#s(#s(#0())))))) ,::(#abs(#pos(#s(#s(#s(#s(#s(#0()))))))) ,::(#abs(#pos(#s(#s(#s(#s(#s(#s(#s(#s(#s(#0()))))))))))) ,::(#abs(#pos(#s(#s(#s(#s(#s(#s(#s(#0()))))))))) ,::(#abs(#pos(#s(#0()))) ,::(#abs(#pos(#s(#s(#0())))) ,::(#abs(#pos(#s(#s(#s(#s(#s(#s(#s(#s(#0())))))))))) ,::(#abs(#pos(#s(#s(#s(#s(#s(#s(#0())))))))) ,::(#abs(#pos(#s(#s(#s(#0()))))),nil())))))))))) - Signature: {#abs/1,#cklt/1,#compare/2,#less/2,insert/2,insert#1/2,insert#2/4,insertD/2,insertD#1/2,insertD#2/4 ,insertionsort/1,insertionsort#1/1,insertionsortD/1,insertionsortD#1/1,testInsertionsort/1 ,testInsertionsortD/1,testList/1,#abs#/1,#cklt#/1,#compare#/2,#less#/2,insert#/2,insert#1#/2,insert#2#/4 ,insertD#/2,insertD#1#/2,insertD#2#/4,insertionsort#/1,insertionsort#1#/1,insertionsortD#/1 ,insertionsortD#1#/1,testInsertionsort#/1,testInsertionsortD#/1,testList#/1} / {#0/0,#EQ/0,#GT/0,#LT/0 ,#false/0,#neg/1,#pos/1,#s/1,#true/0,#unit/0,::/2,nil/0,c_1/0,c_2/0,c_3/0,c_4/0,c_5/2,c_6/1,c_7/1,c_8/0 ,c_9/0,c_10/1,c_11/1,c_12/1,c_13/0,c_14/0,c_15/1,c_16/1,c_17/2,c_18/0,c_19/1,c_20/2,c_21/0,c_22/1,c_23/1 ,c_24/10,c_25/0,c_26/0,c_27/0,c_28/0,c_29/0,c_30/0,c_31/0,c_32/0,c_33/1,c_34/0,c_35/0,c_36/0,c_37/1,c_38/0 ,c_39/1} - Obligation: innermost runtime complexity wrt. defined symbols {#abs#,#cklt#,#compare#,#less#,insert#,insert#1#,insert#2# ,insertD#,insertD#1#,insertD#2#,insertionsort#,insertionsort#1#,insertionsortD#,insertionsortD#1# ,testInsertionsort#,testInsertionsortD#,testList#} and constructors {#0,#EQ,#GT,#LT,#false,#neg,#pos,#s ,#true,#unit,::,nil} + Applied Processor: Ara {araHeuristics = NoHeuristics, minDegree = 2, maxDegree = 2, araTimeout = 8, araRuleShifting = Just 1} + Details: Signatures used: ---------------- #0 :: [] -(0)-> "A"(1, 1) #0 :: [] -(0)-> "A"(0, 0) #0 :: [] -(0)-> "A"(11, 15) #0 :: [] -(0)-> "A"(15, 14) #0 :: [] -(0)-> "A"(15, 6) #0 :: [] -(0)-> "A"(15, 12) #0 :: [] -(0)-> "A"(11, 12) #0 :: [] -(0)-> "A"(14, 12) #EQ :: [] -(0)-> "A"(0, 0) #EQ :: [] -(0)-> "A"(12, 12) #GT :: [] -(0)-> "A"(0, 0) #GT :: [] -(0)-> "A"(12, 12) #LT :: [] -(0)-> "A"(0, 0) #LT :: [] -(0)-> "A"(12, 12) #abs :: ["A"(1, 1)] -(0)-> "A"(5, 12) #cklt :: ["A"(0, 0)] -(0)-> "A"(9, 9) #compare :: ["A"(0, 0) x "A"(0, 0)] -(0)-> "A"(10, 10) #false :: [] -(0)-> "A"(0, 0) #false :: [] -(0)-> "A"(15, 15) #less :: ["A"(0, 0) x "A"(0, 0)] -(0)-> "A"(0, 0) #neg :: ["A"(0, 0)] -(0)-> "A"(0, 0) #pos :: ["A"(0, 0)] -(0)-> "A"(1, 1) #pos :: ["A"(0, 0)] -(0)-> "A"(0, 0) #pos :: ["A"(0, 0)] -(0)-> "A"(8, 14) #pos :: ["A"(0, 0)] -(0)-> "A"(5, 12) #pos :: ["A"(0, 0)] -(0)-> "A"(3, 10) #pos :: ["A"(0, 0)] -(0)-> "A"(5, 13) #pos :: ["A"(0, 0)] -(0)-> "A"(8, 8) #pos :: ["A"(0, 0)] -(0)-> "A"(1, 10) #pos :: ["A"(0, 0)] -(0)-> "A"(9, 11) #pos :: ["A"(0, 0)] -(0)-> "A"(9, 8) #pos :: ["A"(0, 0)] -(0)-> "A"(12, 8) #pos :: ["A"(0, 0)] -(0)-> "A"(13, 14) #s :: ["A"(0, 0)] -(0)-> "A"(0, 0) #s :: ["A"(14, 0)] -(0)-> "A"(10, 4) #s :: ["A"(14, 0)] -(0)-> "A"(14, 0) #s :: ["A"(15, 0)] -(0)-> "A"(14, 1) #s :: ["A"(4, 0)] -(0)-> "A"(2, 2) #s :: ["A"(5, 0)] -(0)-> "A"(4, 1) #s :: ["A"(10, 0)] -(0)-> "A"(7, 3) #s :: ["A"(12, 0)] -(0)-> "A"(11, 1) #s :: ["A"(14, 0)] -(0)-> "A"(13, 1) #s :: ["A"(2, 0)] -(0)-> "A"(2, 0) #s :: ["A"(6, 0)] -(0)-> "A"(3, 3) #s :: ["A"(8, 0)] -(0)-> "A"(8, 0) #s :: ["A"(10, 0)] -(0)-> "A"(9, 1) #s :: ["A"(10, 0)] -(0)-> "A"(10, 0) #s :: ["A"(5, 0)] -(0)-> "A"(5, 0) #s :: ["A"(7, 0)] -(0)-> "A"(7, 0) #s :: ["A"(12, 0)] -(0)-> "A"(7, 5) #s :: ["A"(14, 0)] -(0)-> "A"(12, 2) #s :: ["A"(4, 0)] -(0)-> "A"(0, 4) #s :: ["A"(8, 0)] -(0)-> "A"(4, 4) #s :: ["A"(10, 0)] -(0)-> "A"(8, 2) #s :: ["A"(11, 0)] -(0)-> "A"(11, 0) #s :: ["A"(12, 0)] -(0)-> "A"(12, 0) #s :: ["A"(13, 0)] -(0)-> "A"(12, 1) #s :: ["A"(2, 0)] -(0)-> "A"(1, 1) #s :: ["A"(11, 0)] -(0)-> "A"(2, 9) #s :: ["A"(15, 0)] -(0)-> "A"(13, 2) #s :: ["A"(15, 0)] -(0)-> "A"(15, 0) #true :: [] -(0)-> "A"(0, 0) #true :: [] -(0)-> "A"(15, 15) #unit :: [] -(0)-> "A"(7, 7) #unit :: [] -(0)-> "A"(15, 15) :: :: ["A"(0, 0) x "A"(10, 1)] -(1)-> "A"(10, 1) :: :: ["A"(0, 0) x "A"(1, 1)] -(1)-> "A"(1, 1) :: :: ["A"(0, 0) x "A"(0, 1)] -(1)-> "A"(0, 1) :: :: ["A"(0, 0) x "A"(4, 1)] -(1)-> "A"(4, 1) :: :: ["A"(0, 0) x "A"(0, 0)] -(0)-> "A"(0, 0) :: :: ["A"(0, 0) x "A"(3, 1)] -(1)-> "A"(3, 1) :: :: ["A"(0, 0) x "A"(14, 1)] -(1)-> "A"(14, 1) :: :: ["A"(0, 0) x "A"(8, 1)] -(1)-> "A"(8, 1) :: :: ["A"(0, 0) x "A"(12, 1)] -(1)-> "A"(12, 1) :: :: ["A"(0, 0) x "A"(13, 1)] -(1)-> "A"(13, 1) insert :: ["A"(0, 0) x "A"(10, 1)] -(1)-> "A"(10, 1) insert#1 :: ["A"(10, 1) x "A"(0, 0)] -(1)-> "A"(10, 1) insert#2 :: ["A"(0, 0) x "A"(0, 0) x "A"(0, 0) x "A"(10, 1)] -(2)-> "A"(10, 1) insertD :: ["A"(0, 0) x "A"(1, 1)] -(1)-> "A"(1, 1) insertD#1 :: ["A"(1, 1) x "A"(0, 0)] -(1)-> "A"(1, 1) insertD#2 :: ["A"(0, 0) x "A"(0, 0) x "A"(0, 0) x "A"(1, 1)] -(2)-> "A"(1, 1) insertionsort :: ["A"(0, 1)] -(0)-> "A"(10, 1) insertionsort#1 :: ["A"(0, 1)] -(0)-> "A"(10, 1) insertionsortD :: ["A"(1, 1)] -(0)-> "A"(1, 1) insertionsortD#1 :: ["A"(1, 1)] -(0)-> "A"(1, 1) nil :: [] -(0)-> "A"(10, 1) nil :: [] -(0)-> "A"(1, 1) nil :: [] -(0)-> "A"(0, 1) nil :: [] -(0)-> "A"(15, 15) nil :: [] -(0)-> "A"(13, 7) nil :: [] -(0)-> "A"(7, 7) nil :: [] -(0)-> "A"(14, 15) testList :: ["A"(1, 1)] -(11)-> "A"(3, 1) insert# :: ["A"(0, 0) x "A"(4, 1)] -(1)-> "A"(6, 0) insert#1# :: ["A"(4, 1) x "A"(0, 0)] -(0)-> "A"(8, 5) insert#2# :: ["A"(0, 0) x "A"(0, 0) x "A"(0, 0) x "A"(4, 1)] -(1)-> "A"(13, 4) insertD# :: ["A"(0, 0) x "A"(0, 0)] -(1)-> "A"(4, 4) insertD#1# :: ["A"(0, 0) x "A"(0, 0)] -(1)-> "A"(1, 4) insertD#2# :: ["A"(0, 0) x "A"(0, 0) x "A"(0, 0) x "A"(0, 0)] -(1)-> "A"(8, 0) insertionsort# :: ["A"(1, 1)] -(4)-> "A"(0, 0) insertionsort#1# :: ["A"(1, 1)] -(4)-> "A"(0, 0) insertionsortD# :: ["A"(3, 1)] -(1)-> "A"(2, 0) insertionsortD#1# :: ["A"(3, 1)] -(0)-> "A"(2, 0) testInsertionsort# :: ["A"(0)] -(15)-> "A"(0, 0) testInsertionsortD# :: ["A"(0)] -(15)-> "A"(0, 0) c_6 :: ["A"(0, 0)] -(0)-> "A"(9, 0) c_7 :: ["A"(8, 0)] -(0)-> "A"(8, 8) c_10 :: ["A"(6, 0)] -(0)-> "A"(13, 6) c_11 :: ["A"(0, 4)] -(0)-> "A"(12, 4) c_12 :: ["A"(0, 0)] -(0)-> "A"(1, 4) c_15 :: ["A"(0, 0)] -(0)-> "A"(8, 8) Cost-free Signatures used: -------------------------- Base Constructor Signatures used: --------------------------------- "#0_A" :: [] -(0)-> "A"(0) "#EQ_A" :: [] -(0)-> "A"(0) "#GT_A" :: [] -(0)-> "A"(0) "#LT_A" :: [] -(0)-> "A"(0) "#false_A" :: [] -(0)-> "A"(0) "#neg_A" :: ["A"(0)] -(0)-> "A"(0) "#pos_A" :: ["A"(0)] -(0)-> "A"(0) "#s_A" :: ["A"(0)] -(0)-> "A"(0) "#true_A" :: [] -(0)-> "A"(0) "#unit_A" :: [] -(0)-> "A"(0) "::_A" :: ["A"(0) x "A"(0)] -(0)-> "A"(0) "c_10_A" :: ["A"(0)] -(0)-> "A"(1, 0) "c_10_A" :: ["A"(0)] -(0)-> "A"(0, 1) "c_11_A" :: ["A"(0)] -(0)-> "A"(1, 0) "c_11_A" :: ["A"(0)] -(0)-> "A"(0, 1) "c_12_A" :: ["A"(0)] -(0)-> "A"(1, 0) "c_12_A" :: ["A"(0)] -(0)-> "A"(0, 1) "c_15_A" :: ["A"(0)] -(0)-> "A"(1, 0) "c_15_A" :: ["A"(0)] -(0)-> "A"(0, 1) "c_6_A" :: ["A"(0)] -(0)-> "A"(1, 0) "c_6_A" :: ["A"(0)] -(0)-> "A"(0, 1) "c_7_A" :: ["A"(0)] -(0)-> "A"(1, 0) "c_7_A" :: ["A"(0)] -(0)-> "A"(0, 1) "nil_A" :: [] -(0)-> "A"(1, 0) "nil_A" :: [] -(0)-> "A"(0, 1) Following Still Strict Rules were Typed as: ------------------------------------------- 1. Strict: insert#(@x,@l) -> c_6(insert#1#(@l,@x)) 2. Weak: WORST_CASE(?,O(n^3))