WORST_CASE(?,O(n^3)) * Step 1: DependencyPairs WORST_CASE(?,O(n^3)) + Considered Problem: - Strict 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) 'less(x,y) -> 'cklt('compare(x,y)) append(l1,l2) -> append'1(l1,l2) append'1(dd(x,xs),l2) -> dd(x,append(xs,l2)) append'1(nil(),l2) -> l2 flatten(t) -> flatten'1(t) flatten'1(leaf()) -> nil() flatten'1(node(l,t1,t2)) -> append(l,append(flatten(t1),flatten(t2))) flattensort(t) -> insertionsort(flatten(t)) insert(x,l) -> insert'1(l,x) insert'1(dd(y,ys),x) -> insert'2('less(y,x),x,y,ys) insert'1(nil(),x) -> dd(x,nil()) insert'2('false(),x,y,ys) -> dd(x,dd(y,ys)) insert'2('true(),x,y,ys) -> dd(y,insert(x,ys)) insertionsort(l) -> insertionsort'1(l) insertionsort'1(dd(x,xs)) -> insert(x,insertionsort(xs)) insertionsort'1(nil()) -> nil() - Signature: {'cklt/1,'compare/2,'less/2,append/2,append'1/2,flatten/1,flatten'1/1,flattensort/1,insert/2,insert'1/2 ,insert'2/4,insertionsort/1,insertionsort'1/1} / {'0/0,'EQ/0,'GT/0,'LT/0,'false/0,'neg/1,'pos/1,'s/1,'true/0 ,dd/2,leaf/0,nil/0,node/3} - Obligation: innermost runtime complexity wrt. defined symbols {'cklt,'compare,'less,append,append'1,flatten,flatten'1 ,flattensort,insert,insert'1,insert'2,insertionsort,insertionsort'1} and constructors {'0,'EQ,'GT,'LT,'false ,'neg,'pos,'s,'true,dd,leaf,nil,node} + Applied Processor: DependencyPairs {dpKind_ = DT} + Details: We add the following dependency tuples: Strict DPs 'cklt#('EQ()) -> c_1() 'cklt#('GT()) -> c_2() 'cklt#('LT()) -> c_3() 'compare#('0(),'0()) -> c_4() 'compare#('0(),'neg(y)) -> c_5() 'compare#('0(),'pos(y)) -> c_6() 'compare#('0(),'s(y)) -> c_7() 'compare#('neg(x),'0()) -> c_8() 'compare#('neg(x),'neg(y)) -> c_9('compare#(y,x)) 'compare#('neg(x),'pos(y)) -> c_10() 'compare#('pos(x),'0()) -> c_11() 'compare#('pos(x),'neg(y)) -> c_12() 'compare#('pos(x),'pos(y)) -> c_13('compare#(x,y)) 'compare#('s(x),'0()) -> c_14() 'compare#('s(x),'s(y)) -> c_15('compare#(x,y)) 'less#(x,y) -> c_16('cklt#('compare(x,y)),'compare#(x,y)) append#(l1,l2) -> c_17(append'1#(l1,l2)) append'1#(dd(x,xs),l2) -> c_18(append#(xs,l2)) append'1#(nil(),l2) -> c_19() flatten#(t) -> c_20(flatten'1#(t)) flatten'1#(leaf()) -> c_21() flatten'1#(node(l,t1,t2)) -> c_22(append#(l,append(flatten(t1),flatten(t2))) ,append#(flatten(t1),flatten(t2)) ,flatten#(t1) ,flatten#(t2)) flattensort#(t) -> c_23(insertionsort#(flatten(t)),flatten#(t)) insert#(x,l) -> c_24(insert'1#(l,x)) insert'1#(dd(y,ys),x) -> c_25(insert'2#('less(y,x),x,y,ys),'less#(y,x)) insert'1#(nil(),x) -> c_26() insert'2#('false(),x,y,ys) -> c_27() insert'2#('true(),x,y,ys) -> c_28(insert#(x,ys)) insertionsort#(l) -> c_29(insertionsort'1#(l)) insertionsort'1#(dd(x,xs)) -> c_30(insert#(x,insertionsort(xs)),insertionsort#(xs)) insertionsort'1#(nil()) -> c_31() Weak DPs and mark the set of starting terms. * Step 2: PredecessorEstimation WORST_CASE(?,O(n^3)) + Considered Problem: - Strict DPs: 'cklt#('EQ()) -> c_1() 'cklt#('GT()) -> c_2() 'cklt#('LT()) -> c_3() 'compare#('0(),'0()) -> c_4() 'compare#('0(),'neg(y)) -> c_5() 'compare#('0(),'pos(y)) -> c_6() 'compare#('0(),'s(y)) -> c_7() 'compare#('neg(x),'0()) -> c_8() 'compare#('neg(x),'neg(y)) -> c_9('compare#(y,x)) 'compare#('neg(x),'pos(y)) -> c_10() 'compare#('pos(x),'0()) -> c_11() 'compare#('pos(x),'neg(y)) -> c_12() 'compare#('pos(x),'pos(y)) -> c_13('compare#(x,y)) 'compare#('s(x),'0()) -> c_14() 'compare#('s(x),'s(y)) -> c_15('compare#(x,y)) 'less#(x,y) -> c_16('cklt#('compare(x,y)),'compare#(x,y)) append#(l1,l2) -> c_17(append'1#(l1,l2)) append'1#(dd(x,xs),l2) -> c_18(append#(xs,l2)) append'1#(nil(),l2) -> c_19() flatten#(t) -> c_20(flatten'1#(t)) flatten'1#(leaf()) -> c_21() flatten'1#(node(l,t1,t2)) -> c_22(append#(l,append(flatten(t1),flatten(t2))) ,append#(flatten(t1),flatten(t2)) ,flatten#(t1) ,flatten#(t2)) flattensort#(t) -> c_23(insertionsort#(flatten(t)),flatten#(t)) insert#(x,l) -> c_24(insert'1#(l,x)) insert'1#(dd(y,ys),x) -> c_25(insert'2#('less(y,x),x,y,ys),'less#(y,x)) insert'1#(nil(),x) -> c_26() insert'2#('false(),x,y,ys) -> c_27() insert'2#('true(),x,y,ys) -> c_28(insert#(x,ys)) insertionsort#(l) -> c_29(insertionsort'1#(l)) insertionsort'1#(dd(x,xs)) -> c_30(insert#(x,insertionsort(xs)),insertionsort#(xs)) insertionsort'1#(nil()) -> c_31() - 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) 'less(x,y) -> 'cklt('compare(x,y)) append(l1,l2) -> append'1(l1,l2) append'1(dd(x,xs),l2) -> dd(x,append(xs,l2)) append'1(nil(),l2) -> l2 flatten(t) -> flatten'1(t) flatten'1(leaf()) -> nil() flatten'1(node(l,t1,t2)) -> append(l,append(flatten(t1),flatten(t2))) flattensort(t) -> insertionsort(flatten(t)) insert(x,l) -> insert'1(l,x) insert'1(dd(y,ys),x) -> insert'2('less(y,x),x,y,ys) insert'1(nil(),x) -> dd(x,nil()) insert'2('false(),x,y,ys) -> dd(x,dd(y,ys)) insert'2('true(),x,y,ys) -> dd(y,insert(x,ys)) insertionsort(l) -> insertionsort'1(l) insertionsort'1(dd(x,xs)) -> insert(x,insertionsort(xs)) insertionsort'1(nil()) -> nil() - Signature: {'cklt/1,'compare/2,'less/2,append/2,append'1/2,flatten/1,flatten'1/1,flattensort/1,insert/2,insert'1/2 ,insert'2/4,insertionsort/1,insertionsort'1/1,'cklt#/1,'compare#/2,'less#/2,append#/2,append'1#/2,flatten#/1 ,flatten'1#/1,flattensort#/1,insert#/2,insert'1#/2,insert'2#/4,insertionsort#/1,insertionsort'1#/1} / {'0/0 ,'EQ/0,'GT/0,'LT/0,'false/0,'neg/1,'pos/1,'s/1,'true/0,dd/2,leaf/0,nil/0,node/3,c_1/0,c_2/0,c_3/0,c_4/0 ,c_5/0,c_6/0,c_7/0,c_8/0,c_9/1,c_10/0,c_11/0,c_12/0,c_13/1,c_14/0,c_15/1,c_16/2,c_17/1,c_18/1,c_19/0,c_20/1 ,c_21/0,c_22/4,c_23/2,c_24/1,c_25/2,c_26/0,c_27/0,c_28/1,c_29/1,c_30/2,c_31/0} - Obligation: innermost runtime complexity wrt. defined symbols {'cklt#,'compare#,'less#,append#,append'1#,flatten# ,flatten'1#,flattensort#,insert#,insert'1#,insert'2#,insertionsort#,insertionsort'1#} and constructors {'0 ,'EQ,'GT,'LT,'false,'neg,'pos,'s,'true,dd,leaf,nil,node} + Applied Processor: PredecessorEstimation {onSelection = all simple predecessor estimation selector} + Details: We estimate the number of application of {1,2,3,4,5,6,7,8,10,11,12,14,19,21,26,27,31} by application of Pre({1,2,3,4,5,6,7,8,10,11,12,14,19,21,26,27,31}) = {9,13,15,16,17,20,24,25,29}. Here rules are labelled as follows: 1: 'cklt#('EQ()) -> c_1() 2: 'cklt#('GT()) -> c_2() 3: 'cklt#('LT()) -> c_3() 4: 'compare#('0(),'0()) -> c_4() 5: 'compare#('0(),'neg(y)) -> c_5() 6: 'compare#('0(),'pos(y)) -> c_6() 7: 'compare#('0(),'s(y)) -> c_7() 8: 'compare#('neg(x),'0()) -> c_8() 9: 'compare#('neg(x),'neg(y)) -> c_9('compare#(y,x)) 10: 'compare#('neg(x),'pos(y)) -> c_10() 11: 'compare#('pos(x),'0()) -> c_11() 12: 'compare#('pos(x),'neg(y)) -> c_12() 13: 'compare#('pos(x),'pos(y)) -> c_13('compare#(x,y)) 14: 'compare#('s(x),'0()) -> c_14() 15: 'compare#('s(x),'s(y)) -> c_15('compare#(x,y)) 16: 'less#(x,y) -> c_16('cklt#('compare(x,y)),'compare#(x,y)) 17: append#(l1,l2) -> c_17(append'1#(l1,l2)) 18: append'1#(dd(x,xs),l2) -> c_18(append#(xs,l2)) 19: append'1#(nil(),l2) -> c_19() 20: flatten#(t) -> c_20(flatten'1#(t)) 21: flatten'1#(leaf()) -> c_21() 22: flatten'1#(node(l,t1,t2)) -> c_22(append#(l,append(flatten(t1),flatten(t2))) ,append#(flatten(t1),flatten(t2)) ,flatten#(t1) ,flatten#(t2)) 23: flattensort#(t) -> c_23(insertionsort#(flatten(t)),flatten#(t)) 24: insert#(x,l) -> c_24(insert'1#(l,x)) 25: insert'1#(dd(y,ys),x) -> c_25(insert'2#('less(y,x),x,y,ys),'less#(y,x)) 26: insert'1#(nil(),x) -> c_26() 27: insert'2#('false(),x,y,ys) -> c_27() 28: insert'2#('true(),x,y,ys) -> c_28(insert#(x,ys)) 29: insertionsort#(l) -> c_29(insertionsort'1#(l)) 30: insertionsort'1#(dd(x,xs)) -> c_30(insert#(x,insertionsort(xs)),insertionsort#(xs)) 31: insertionsort'1#(nil()) -> c_31() * Step 3: RemoveWeakSuffixes WORST_CASE(?,O(n^3)) + Considered Problem: - Strict DPs: 'compare#('neg(x),'neg(y)) -> c_9('compare#(y,x)) 'compare#('pos(x),'pos(y)) -> c_13('compare#(x,y)) 'compare#('s(x),'s(y)) -> c_15('compare#(x,y)) 'less#(x,y) -> c_16('cklt#('compare(x,y)),'compare#(x,y)) append#(l1,l2) -> c_17(append'1#(l1,l2)) append'1#(dd(x,xs),l2) -> c_18(append#(xs,l2)) flatten#(t) -> c_20(flatten'1#(t)) flatten'1#(node(l,t1,t2)) -> c_22(append#(l,append(flatten(t1),flatten(t2))) ,append#(flatten(t1),flatten(t2)) ,flatten#(t1) ,flatten#(t2)) flattensort#(t) -> c_23(insertionsort#(flatten(t)),flatten#(t)) insert#(x,l) -> c_24(insert'1#(l,x)) insert'1#(dd(y,ys),x) -> c_25(insert'2#('less(y,x),x,y,ys),'less#(y,x)) insert'2#('true(),x,y,ys) -> c_28(insert#(x,ys)) insertionsort#(l) -> c_29(insertionsort'1#(l)) insertionsort'1#(dd(x,xs)) -> c_30(insert#(x,insertionsort(xs)),insertionsort#(xs)) - Weak DPs: 'cklt#('EQ()) -> c_1() 'cklt#('GT()) -> c_2() 'cklt#('LT()) -> c_3() 'compare#('0(),'0()) -> c_4() 'compare#('0(),'neg(y)) -> c_5() 'compare#('0(),'pos(y)) -> c_6() 'compare#('0(),'s(y)) -> c_7() 'compare#('neg(x),'0()) -> c_8() 'compare#('neg(x),'pos(y)) -> c_10() 'compare#('pos(x),'0()) -> c_11() 'compare#('pos(x),'neg(y)) -> c_12() 'compare#('s(x),'0()) -> c_14() append'1#(nil(),l2) -> c_19() flatten'1#(leaf()) -> c_21() insert'1#(nil(),x) -> c_26() insert'2#('false(),x,y,ys) -> c_27() insertionsort'1#(nil()) -> c_31() - 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) 'less(x,y) -> 'cklt('compare(x,y)) append(l1,l2) -> append'1(l1,l2) append'1(dd(x,xs),l2) -> dd(x,append(xs,l2)) append'1(nil(),l2) -> l2 flatten(t) -> flatten'1(t) flatten'1(leaf()) -> nil() flatten'1(node(l,t1,t2)) -> append(l,append(flatten(t1),flatten(t2))) flattensort(t) -> insertionsort(flatten(t)) insert(x,l) -> insert'1(l,x) insert'1(dd(y,ys),x) -> insert'2('less(y,x),x,y,ys) insert'1(nil(),x) -> dd(x,nil()) insert'2('false(),x,y,ys) -> dd(x,dd(y,ys)) insert'2('true(),x,y,ys) -> dd(y,insert(x,ys)) insertionsort(l) -> insertionsort'1(l) insertionsort'1(dd(x,xs)) -> insert(x,insertionsort(xs)) insertionsort'1(nil()) -> nil() - Signature: {'cklt/1,'compare/2,'less/2,append/2,append'1/2,flatten/1,flatten'1/1,flattensort/1,insert/2,insert'1/2 ,insert'2/4,insertionsort/1,insertionsort'1/1,'cklt#/1,'compare#/2,'less#/2,append#/2,append'1#/2,flatten#/1 ,flatten'1#/1,flattensort#/1,insert#/2,insert'1#/2,insert'2#/4,insertionsort#/1,insertionsort'1#/1} / {'0/0 ,'EQ/0,'GT/0,'LT/0,'false/0,'neg/1,'pos/1,'s/1,'true/0,dd/2,leaf/0,nil/0,node/3,c_1/0,c_2/0,c_3/0,c_4/0 ,c_5/0,c_6/0,c_7/0,c_8/0,c_9/1,c_10/0,c_11/0,c_12/0,c_13/1,c_14/0,c_15/1,c_16/2,c_17/1,c_18/1,c_19/0,c_20/1 ,c_21/0,c_22/4,c_23/2,c_24/1,c_25/2,c_26/0,c_27/0,c_28/1,c_29/1,c_30/2,c_31/0} - Obligation: innermost runtime complexity wrt. defined symbols {'cklt#,'compare#,'less#,append#,append'1#,flatten# ,flatten'1#,flattensort#,insert#,insert'1#,insert'2#,insertionsort#,insertionsort'1#} and constructors {'0 ,'EQ,'GT,'LT,'false,'neg,'pos,'s,'true,dd,leaf,nil,node} + Applied Processor: RemoveWeakSuffixes + Details: Consider the dependency graph 1:S:'compare#('neg(x),'neg(y)) -> c_9('compare#(y,x)) -->_1 'compare#('s(x),'s(y)) -> c_15('compare#(x,y)):3 -->_1 'compare#('pos(x),'pos(y)) -> c_13('compare#(x,y)):2 -->_1 'compare#('s(x),'0()) -> c_14():26 -->_1 'compare#('pos(x),'neg(y)) -> c_12():25 -->_1 'compare#('pos(x),'0()) -> c_11():24 -->_1 'compare#('neg(x),'pos(y)) -> c_10():23 -->_1 'compare#('neg(x),'0()) -> c_8():22 -->_1 'compare#('0(),'s(y)) -> c_7():21 -->_1 'compare#('0(),'pos(y)) -> c_6():20 -->_1 'compare#('0(),'neg(y)) -> c_5():19 -->_1 'compare#('0(),'0()) -> c_4():18 -->_1 'compare#('neg(x),'neg(y)) -> c_9('compare#(y,x)):1 2:S:'compare#('pos(x),'pos(y)) -> c_13('compare#(x,y)) -->_1 'compare#('s(x),'s(y)) -> c_15('compare#(x,y)):3 -->_1 'compare#('s(x),'0()) -> c_14():26 -->_1 'compare#('pos(x),'neg(y)) -> c_12():25 -->_1 'compare#('pos(x),'0()) -> c_11():24 -->_1 'compare#('neg(x),'pos(y)) -> c_10():23 -->_1 'compare#('neg(x),'0()) -> c_8():22 -->_1 'compare#('0(),'s(y)) -> c_7():21 -->_1 'compare#('0(),'pos(y)) -> c_6():20 -->_1 'compare#('0(),'neg(y)) -> c_5():19 -->_1 'compare#('0(),'0()) -> c_4():18 -->_1 'compare#('pos(x),'pos(y)) -> c_13('compare#(x,y)):2 -->_1 'compare#('neg(x),'neg(y)) -> c_9('compare#(y,x)):1 3:S:'compare#('s(x),'s(y)) -> c_15('compare#(x,y)) -->_1 'compare#('s(x),'0()) -> c_14():26 -->_1 'compare#('pos(x),'neg(y)) -> c_12():25 -->_1 'compare#('pos(x),'0()) -> c_11():24 -->_1 'compare#('neg(x),'pos(y)) -> c_10():23 -->_1 'compare#('neg(x),'0()) -> c_8():22 -->_1 'compare#('0(),'s(y)) -> c_7():21 -->_1 'compare#('0(),'pos(y)) -> c_6():20 -->_1 'compare#('0(),'neg(y)) -> c_5():19 -->_1 'compare#('0(),'0()) -> c_4():18 -->_1 'compare#('s(x),'s(y)) -> c_15('compare#(x,y)):3 -->_1 'compare#('pos(x),'pos(y)) -> c_13('compare#(x,y)):2 -->_1 'compare#('neg(x),'neg(y)) -> c_9('compare#(y,x)):1 4:S:'less#(x,y) -> c_16('cklt#('compare(x,y)),'compare#(x,y)) -->_2 'compare#('s(x),'0()) -> c_14():26 -->_2 'compare#('pos(x),'neg(y)) -> c_12():25 -->_2 'compare#('pos(x),'0()) -> c_11():24 -->_2 'compare#('neg(x),'pos(y)) -> c_10():23 -->_2 'compare#('neg(x),'0()) -> c_8():22 -->_2 'compare#('0(),'s(y)) -> c_7():21 -->_2 'compare#('0(),'pos(y)) -> c_6():20 -->_2 'compare#('0(),'neg(y)) -> c_5():19 -->_2 'compare#('0(),'0()) -> c_4():18 -->_1 'cklt#('LT()) -> c_3():17 -->_1 'cklt#('GT()) -> c_2():16 -->_1 'cklt#('EQ()) -> c_1():15 -->_2 'compare#('s(x),'s(y)) -> c_15('compare#(x,y)):3 -->_2 'compare#('pos(x),'pos(y)) -> c_13('compare#(x,y)):2 -->_2 'compare#('neg(x),'neg(y)) -> c_9('compare#(y,x)):1 5:S:append#(l1,l2) -> c_17(append'1#(l1,l2)) -->_1 append'1#(dd(x,xs),l2) -> c_18(append#(xs,l2)):6 -->_1 append'1#(nil(),l2) -> c_19():27 6:S:append'1#(dd(x,xs),l2) -> c_18(append#(xs,l2)) -->_1 append#(l1,l2) -> c_17(append'1#(l1,l2)):5 7:S:flatten#(t) -> c_20(flatten'1#(t)) -->_1 flatten'1#(node(l,t1,t2)) -> c_22(append#(l,append(flatten(t1),flatten(t2))) ,append#(flatten(t1),flatten(t2)) ,flatten#(t1) ,flatten#(t2)):8 -->_1 flatten'1#(leaf()) -> c_21():28 8:S:flatten'1#(node(l,t1,t2)) -> c_22(append#(l,append(flatten(t1),flatten(t2))) ,append#(flatten(t1),flatten(t2)) ,flatten#(t1) ,flatten#(t2)) -->_4 flatten#(t) -> c_20(flatten'1#(t)):7 -->_3 flatten#(t) -> c_20(flatten'1#(t)):7 -->_2 append#(l1,l2) -> c_17(append'1#(l1,l2)):5 -->_1 append#(l1,l2) -> c_17(append'1#(l1,l2)):5 9:S:flattensort#(t) -> c_23(insertionsort#(flatten(t)),flatten#(t)) -->_1 insertionsort#(l) -> c_29(insertionsort'1#(l)):13 -->_2 flatten#(t) -> c_20(flatten'1#(t)):7 10:S:insert#(x,l) -> c_24(insert'1#(l,x)) -->_1 insert'1#(dd(y,ys),x) -> c_25(insert'2#('less(y,x),x,y,ys),'less#(y,x)):11 -->_1 insert'1#(nil(),x) -> c_26():29 11:S:insert'1#(dd(y,ys),x) -> c_25(insert'2#('less(y,x),x,y,ys),'less#(y,x)) -->_1 insert'2#('true(),x,y,ys) -> c_28(insert#(x,ys)):12 -->_1 insert'2#('false(),x,y,ys) -> c_27():30 -->_2 'less#(x,y) -> c_16('cklt#('compare(x,y)),'compare#(x,y)):4 12:S:insert'2#('true(),x,y,ys) -> c_28(insert#(x,ys)) -->_1 insert#(x,l) -> c_24(insert'1#(l,x)):10 13:S:insertionsort#(l) -> c_29(insertionsort'1#(l)) -->_1 insertionsort'1#(dd(x,xs)) -> c_30(insert#(x,insertionsort(xs)),insertionsort#(xs)):14 -->_1 insertionsort'1#(nil()) -> c_31():31 14:S:insertionsort'1#(dd(x,xs)) -> c_30(insert#(x,insertionsort(xs)),insertionsort#(xs)) -->_2 insertionsort#(l) -> c_29(insertionsort'1#(l)):13 -->_1 insert#(x,l) -> c_24(insert'1#(l,x)):10 15:W:'cklt#('EQ()) -> c_1() 16:W:'cklt#('GT()) -> c_2() 17:W:'cklt#('LT()) -> c_3() 18:W:'compare#('0(),'0()) -> c_4() 19:W:'compare#('0(),'neg(y)) -> c_5() 20:W:'compare#('0(),'pos(y)) -> c_6() 21:W:'compare#('0(),'s(y)) -> c_7() 22:W:'compare#('neg(x),'0()) -> c_8() 23:W:'compare#('neg(x),'pos(y)) -> c_10() 24:W:'compare#('pos(x),'0()) -> c_11() 25:W:'compare#('pos(x),'neg(y)) -> c_12() 26:W:'compare#('s(x),'0()) -> c_14() 27:W:append'1#(nil(),l2) -> c_19() 28:W:flatten'1#(leaf()) -> c_21() 29:W:insert'1#(nil(),x) -> c_26() 30:W:insert'2#('false(),x,y,ys) -> c_27() 31:W:insertionsort'1#(nil()) -> c_31() The following weak DPs constitute a sub-graph of the DG that is closed under successors. The DPs are removed. 31: insertionsort'1#(nil()) -> c_31() 29: insert'1#(nil(),x) -> c_26() 30: insert'2#('false(),x,y,ys) -> c_27() 28: flatten'1#(leaf()) -> c_21() 27: append'1#(nil(),l2) -> c_19() 15: 'cklt#('EQ()) -> c_1() 16: 'cklt#('GT()) -> c_2() 17: 'cklt#('LT()) -> c_3() 18: 'compare#('0(),'0()) -> c_4() 19: 'compare#('0(),'neg(y)) -> c_5() 20: 'compare#('0(),'pos(y)) -> c_6() 21: 'compare#('0(),'s(y)) -> c_7() 22: 'compare#('neg(x),'0()) -> c_8() 23: 'compare#('neg(x),'pos(y)) -> c_10() 24: 'compare#('pos(x),'0()) -> c_11() 25: 'compare#('pos(x),'neg(y)) -> c_12() 26: 'compare#('s(x),'0()) -> c_14() * Step 4: SimplifyRHS WORST_CASE(?,O(n^3)) + Considered Problem: - Strict DPs: 'compare#('neg(x),'neg(y)) -> c_9('compare#(y,x)) 'compare#('pos(x),'pos(y)) -> c_13('compare#(x,y)) 'compare#('s(x),'s(y)) -> c_15('compare#(x,y)) 'less#(x,y) -> c_16('cklt#('compare(x,y)),'compare#(x,y)) append#(l1,l2) -> c_17(append'1#(l1,l2)) append'1#(dd(x,xs),l2) -> c_18(append#(xs,l2)) flatten#(t) -> c_20(flatten'1#(t)) flatten'1#(node(l,t1,t2)) -> c_22(append#(l,append(flatten(t1),flatten(t2))) ,append#(flatten(t1),flatten(t2)) ,flatten#(t1) ,flatten#(t2)) flattensort#(t) -> c_23(insertionsort#(flatten(t)),flatten#(t)) insert#(x,l) -> c_24(insert'1#(l,x)) insert'1#(dd(y,ys),x) -> c_25(insert'2#('less(y,x),x,y,ys),'less#(y,x)) insert'2#('true(),x,y,ys) -> c_28(insert#(x,ys)) insertionsort#(l) -> c_29(insertionsort'1#(l)) insertionsort'1#(dd(x,xs)) -> c_30(insert#(x,insertionsort(xs)),insertionsort#(xs)) - 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) 'less(x,y) -> 'cklt('compare(x,y)) append(l1,l2) -> append'1(l1,l2) append'1(dd(x,xs),l2) -> dd(x,append(xs,l2)) append'1(nil(),l2) -> l2 flatten(t) -> flatten'1(t) flatten'1(leaf()) -> nil() flatten'1(node(l,t1,t2)) -> append(l,append(flatten(t1),flatten(t2))) flattensort(t) -> insertionsort(flatten(t)) insert(x,l) -> insert'1(l,x) insert'1(dd(y,ys),x) -> insert'2('less(y,x),x,y,ys) insert'1(nil(),x) -> dd(x,nil()) insert'2('false(),x,y,ys) -> dd(x,dd(y,ys)) insert'2('true(),x,y,ys) -> dd(y,insert(x,ys)) insertionsort(l) -> insertionsort'1(l) insertionsort'1(dd(x,xs)) -> insert(x,insertionsort(xs)) insertionsort'1(nil()) -> nil() - Signature: {'cklt/1,'compare/2,'less/2,append/2,append'1/2,flatten/1,flatten'1/1,flattensort/1,insert/2,insert'1/2 ,insert'2/4,insertionsort/1,insertionsort'1/1,'cklt#/1,'compare#/2,'less#/2,append#/2,append'1#/2,flatten#/1 ,flatten'1#/1,flattensort#/1,insert#/2,insert'1#/2,insert'2#/4,insertionsort#/1,insertionsort'1#/1} / {'0/0 ,'EQ/0,'GT/0,'LT/0,'false/0,'neg/1,'pos/1,'s/1,'true/0,dd/2,leaf/0,nil/0,node/3,c_1/0,c_2/0,c_3/0,c_4/0 ,c_5/0,c_6/0,c_7/0,c_8/0,c_9/1,c_10/0,c_11/0,c_12/0,c_13/1,c_14/0,c_15/1,c_16/2,c_17/1,c_18/1,c_19/0,c_20/1 ,c_21/0,c_22/4,c_23/2,c_24/1,c_25/2,c_26/0,c_27/0,c_28/1,c_29/1,c_30/2,c_31/0} - Obligation: innermost runtime complexity wrt. defined symbols {'cklt#,'compare#,'less#,append#,append'1#,flatten# ,flatten'1#,flattensort#,insert#,insert'1#,insert'2#,insertionsort#,insertionsort'1#} and constructors {'0 ,'EQ,'GT,'LT,'false,'neg,'pos,'s,'true,dd,leaf,nil,node} + Applied Processor: SimplifyRHS + Details: Consider the dependency graph 1:S:'compare#('neg(x),'neg(y)) -> c_9('compare#(y,x)) -->_1 'compare#('s(x),'s(y)) -> c_15('compare#(x,y)):3 -->_1 'compare#('pos(x),'pos(y)) -> c_13('compare#(x,y)):2 -->_1 'compare#('neg(x),'neg(y)) -> c_9('compare#(y,x)):1 2:S:'compare#('pos(x),'pos(y)) -> c_13('compare#(x,y)) -->_1 'compare#('s(x),'s(y)) -> c_15('compare#(x,y)):3 -->_1 'compare#('pos(x),'pos(y)) -> c_13('compare#(x,y)):2 -->_1 'compare#('neg(x),'neg(y)) -> c_9('compare#(y,x)):1 3:S:'compare#('s(x),'s(y)) -> c_15('compare#(x,y)) -->_1 'compare#('s(x),'s(y)) -> c_15('compare#(x,y)):3 -->_1 'compare#('pos(x),'pos(y)) -> c_13('compare#(x,y)):2 -->_1 'compare#('neg(x),'neg(y)) -> c_9('compare#(y,x)):1 4:S:'less#(x,y) -> c_16('cklt#('compare(x,y)),'compare#(x,y)) -->_2 'compare#('s(x),'s(y)) -> c_15('compare#(x,y)):3 -->_2 'compare#('pos(x),'pos(y)) -> c_13('compare#(x,y)):2 -->_2 'compare#('neg(x),'neg(y)) -> c_9('compare#(y,x)):1 5:S:append#(l1,l2) -> c_17(append'1#(l1,l2)) -->_1 append'1#(dd(x,xs),l2) -> c_18(append#(xs,l2)):6 6:S:append'1#(dd(x,xs),l2) -> c_18(append#(xs,l2)) -->_1 append#(l1,l2) -> c_17(append'1#(l1,l2)):5 7:S:flatten#(t) -> c_20(flatten'1#(t)) -->_1 flatten'1#(node(l,t1,t2)) -> c_22(append#(l,append(flatten(t1),flatten(t2))) ,append#(flatten(t1),flatten(t2)) ,flatten#(t1) ,flatten#(t2)):8 8:S:flatten'1#(node(l,t1,t2)) -> c_22(append#(l,append(flatten(t1),flatten(t2))) ,append#(flatten(t1),flatten(t2)) ,flatten#(t1) ,flatten#(t2)) -->_4 flatten#(t) -> c_20(flatten'1#(t)):7 -->_3 flatten#(t) -> c_20(flatten'1#(t)):7 -->_2 append#(l1,l2) -> c_17(append'1#(l1,l2)):5 -->_1 append#(l1,l2) -> c_17(append'1#(l1,l2)):5 9:S:flattensort#(t) -> c_23(insertionsort#(flatten(t)),flatten#(t)) -->_1 insertionsort#(l) -> c_29(insertionsort'1#(l)):13 -->_2 flatten#(t) -> c_20(flatten'1#(t)):7 10:S:insert#(x,l) -> c_24(insert'1#(l,x)) -->_1 insert'1#(dd(y,ys),x) -> c_25(insert'2#('less(y,x),x,y,ys),'less#(y,x)):11 11:S:insert'1#(dd(y,ys),x) -> c_25(insert'2#('less(y,x),x,y,ys),'less#(y,x)) -->_1 insert'2#('true(),x,y,ys) -> c_28(insert#(x,ys)):12 -->_2 'less#(x,y) -> c_16('cklt#('compare(x,y)),'compare#(x,y)):4 12:S:insert'2#('true(),x,y,ys) -> c_28(insert#(x,ys)) -->_1 insert#(x,l) -> c_24(insert'1#(l,x)):10 13:S:insertionsort#(l) -> c_29(insertionsort'1#(l)) -->_1 insertionsort'1#(dd(x,xs)) -> c_30(insert#(x,insertionsort(xs)),insertionsort#(xs)):14 14:S:insertionsort'1#(dd(x,xs)) -> c_30(insert#(x,insertionsort(xs)),insertionsort#(xs)) -->_2 insertionsort#(l) -> c_29(insertionsort'1#(l)):13 -->_1 insert#(x,l) -> c_24(insert'1#(l,x)):10 Due to missing edges in the depndency graph, the right-hand sides of following rules could be simplified: 'less#(x,y) -> c_16('compare#(x,y)) * Step 5: UsableRules WORST_CASE(?,O(n^3)) + Considered Problem: - Strict DPs: 'compare#('neg(x),'neg(y)) -> c_9('compare#(y,x)) 'compare#('pos(x),'pos(y)) -> c_13('compare#(x,y)) 'compare#('s(x),'s(y)) -> c_15('compare#(x,y)) 'less#(x,y) -> c_16('compare#(x,y)) append#(l1,l2) -> c_17(append'1#(l1,l2)) append'1#(dd(x,xs),l2) -> c_18(append#(xs,l2)) flatten#(t) -> c_20(flatten'1#(t)) flatten'1#(node(l,t1,t2)) -> c_22(append#(l,append(flatten(t1),flatten(t2))) ,append#(flatten(t1),flatten(t2)) ,flatten#(t1) ,flatten#(t2)) flattensort#(t) -> c_23(insertionsort#(flatten(t)),flatten#(t)) insert#(x,l) -> c_24(insert'1#(l,x)) insert'1#(dd(y,ys),x) -> c_25(insert'2#('less(y,x),x,y,ys),'less#(y,x)) insert'2#('true(),x,y,ys) -> c_28(insert#(x,ys)) insertionsort#(l) -> c_29(insertionsort'1#(l)) insertionsort'1#(dd(x,xs)) -> c_30(insert#(x,insertionsort(xs)),insertionsort#(xs)) - 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) 'less(x,y) -> 'cklt('compare(x,y)) append(l1,l2) -> append'1(l1,l2) append'1(dd(x,xs),l2) -> dd(x,append(xs,l2)) append'1(nil(),l2) -> l2 flatten(t) -> flatten'1(t) flatten'1(leaf()) -> nil() flatten'1(node(l,t1,t2)) -> append(l,append(flatten(t1),flatten(t2))) flattensort(t) -> insertionsort(flatten(t)) insert(x,l) -> insert'1(l,x) insert'1(dd(y,ys),x) -> insert'2('less(y,x),x,y,ys) insert'1(nil(),x) -> dd(x,nil()) insert'2('false(),x,y,ys) -> dd(x,dd(y,ys)) insert'2('true(),x,y,ys) -> dd(y,insert(x,ys)) insertionsort(l) -> insertionsort'1(l) insertionsort'1(dd(x,xs)) -> insert(x,insertionsort(xs)) insertionsort'1(nil()) -> nil() - Signature: {'cklt/1,'compare/2,'less/2,append/2,append'1/2,flatten/1,flatten'1/1,flattensort/1,insert/2,insert'1/2 ,insert'2/4,insertionsort/1,insertionsort'1/1,'cklt#/1,'compare#/2,'less#/2,append#/2,append'1#/2,flatten#/1 ,flatten'1#/1,flattensort#/1,insert#/2,insert'1#/2,insert'2#/4,insertionsort#/1,insertionsort'1#/1} / {'0/0 ,'EQ/0,'GT/0,'LT/0,'false/0,'neg/1,'pos/1,'s/1,'true/0,dd/2,leaf/0,nil/0,node/3,c_1/0,c_2/0,c_3/0,c_4/0 ,c_5/0,c_6/0,c_7/0,c_8/0,c_9/1,c_10/0,c_11/0,c_12/0,c_13/1,c_14/0,c_15/1,c_16/1,c_17/1,c_18/1,c_19/0,c_20/1 ,c_21/0,c_22/4,c_23/2,c_24/1,c_25/2,c_26/0,c_27/0,c_28/1,c_29/1,c_30/2,c_31/0} - Obligation: innermost runtime complexity wrt. defined symbols {'cklt#,'compare#,'less#,append#,append'1#,flatten# ,flatten'1#,flattensort#,insert#,insert'1#,insert'2#,insertionsort#,insertionsort'1#} and constructors {'0 ,'EQ,'GT,'LT,'false,'neg,'pos,'s,'true,dd,leaf,nil,node} + Applied Processor: UsableRules + Details: We replace rewrite rules by usable rules: '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)) append(l1,l2) -> append'1(l1,l2) append'1(dd(x,xs),l2) -> dd(x,append(xs,l2)) append'1(nil(),l2) -> l2 flatten(t) -> flatten'1(t) flatten'1(leaf()) -> nil() flatten'1(node(l,t1,t2)) -> append(l,append(flatten(t1),flatten(t2))) insert(x,l) -> insert'1(l,x) insert'1(dd(y,ys),x) -> insert'2('less(y,x),x,y,ys) insert'1(nil(),x) -> dd(x,nil()) insert'2('false(),x,y,ys) -> dd(x,dd(y,ys)) insert'2('true(),x,y,ys) -> dd(y,insert(x,ys)) insertionsort(l) -> insertionsort'1(l) insertionsort'1(dd(x,xs)) -> insert(x,insertionsort(xs)) insertionsort'1(nil()) -> nil() 'compare#('neg(x),'neg(y)) -> c_9('compare#(y,x)) 'compare#('pos(x),'pos(y)) -> c_13('compare#(x,y)) 'compare#('s(x),'s(y)) -> c_15('compare#(x,y)) 'less#(x,y) -> c_16('compare#(x,y)) append#(l1,l2) -> c_17(append'1#(l1,l2)) append'1#(dd(x,xs),l2) -> c_18(append#(xs,l2)) flatten#(t) -> c_20(flatten'1#(t)) flatten'1#(node(l,t1,t2)) -> c_22(append#(l,append(flatten(t1),flatten(t2))) ,append#(flatten(t1),flatten(t2)) ,flatten#(t1) ,flatten#(t2)) flattensort#(t) -> c_23(insertionsort#(flatten(t)),flatten#(t)) insert#(x,l) -> c_24(insert'1#(l,x)) insert'1#(dd(y,ys),x) -> c_25(insert'2#('less(y,x),x,y,ys),'less#(y,x)) insert'2#('true(),x,y,ys) -> c_28(insert#(x,ys)) insertionsort#(l) -> c_29(insertionsort'1#(l)) insertionsort'1#(dd(x,xs)) -> c_30(insert#(x,insertionsort(xs)),insertionsort#(xs)) * Step 6: DecomposeDG WORST_CASE(?,O(n^3)) + Considered Problem: - Strict DPs: 'compare#('neg(x),'neg(y)) -> c_9('compare#(y,x)) 'compare#('pos(x),'pos(y)) -> c_13('compare#(x,y)) 'compare#('s(x),'s(y)) -> c_15('compare#(x,y)) 'less#(x,y) -> c_16('compare#(x,y)) append#(l1,l2) -> c_17(append'1#(l1,l2)) append'1#(dd(x,xs),l2) -> c_18(append#(xs,l2)) flatten#(t) -> c_20(flatten'1#(t)) flatten'1#(node(l,t1,t2)) -> c_22(append#(l,append(flatten(t1),flatten(t2))) ,append#(flatten(t1),flatten(t2)) ,flatten#(t1) ,flatten#(t2)) flattensort#(t) -> c_23(insertionsort#(flatten(t)),flatten#(t)) insert#(x,l) -> c_24(insert'1#(l,x)) insert'1#(dd(y,ys),x) -> c_25(insert'2#('less(y,x),x,y,ys),'less#(y,x)) insert'2#('true(),x,y,ys) -> c_28(insert#(x,ys)) insertionsort#(l) -> c_29(insertionsort'1#(l)) insertionsort'1#(dd(x,xs)) -> c_30(insert#(x,insertionsort(xs)),insertionsort#(xs)) - 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) 'less(x,y) -> 'cklt('compare(x,y)) append(l1,l2) -> append'1(l1,l2) append'1(dd(x,xs),l2) -> dd(x,append(xs,l2)) append'1(nil(),l2) -> l2 flatten(t) -> flatten'1(t) flatten'1(leaf()) -> nil() flatten'1(node(l,t1,t2)) -> append(l,append(flatten(t1),flatten(t2))) insert(x,l) -> insert'1(l,x) insert'1(dd(y,ys),x) -> insert'2('less(y,x),x,y,ys) insert'1(nil(),x) -> dd(x,nil()) insert'2('false(),x,y,ys) -> dd(x,dd(y,ys)) insert'2('true(),x,y,ys) -> dd(y,insert(x,ys)) insertionsort(l) -> insertionsort'1(l) insertionsort'1(dd(x,xs)) -> insert(x,insertionsort(xs)) insertionsort'1(nil()) -> nil() - Signature: {'cklt/1,'compare/2,'less/2,append/2,append'1/2,flatten/1,flatten'1/1,flattensort/1,insert/2,insert'1/2 ,insert'2/4,insertionsort/1,insertionsort'1/1,'cklt#/1,'compare#/2,'less#/2,append#/2,append'1#/2,flatten#/1 ,flatten'1#/1,flattensort#/1,insert#/2,insert'1#/2,insert'2#/4,insertionsort#/1,insertionsort'1#/1} / {'0/0 ,'EQ/0,'GT/0,'LT/0,'false/0,'neg/1,'pos/1,'s/1,'true/0,dd/2,leaf/0,nil/0,node/3,c_1/0,c_2/0,c_3/0,c_4/0 ,c_5/0,c_6/0,c_7/0,c_8/0,c_9/1,c_10/0,c_11/0,c_12/0,c_13/1,c_14/0,c_15/1,c_16/1,c_17/1,c_18/1,c_19/0,c_20/1 ,c_21/0,c_22/4,c_23/2,c_24/1,c_25/2,c_26/0,c_27/0,c_28/1,c_29/1,c_30/2,c_31/0} - Obligation: innermost runtime complexity wrt. defined symbols {'cklt#,'compare#,'less#,append#,append'1#,flatten# ,flatten'1#,flattensort#,insert#,insert'1#,insert'2#,insertionsort#,insertionsort'1#} and constructors {'0 ,'EQ,'GT,'LT,'false,'neg,'pos,'s,'true,dd,leaf,nil,node} + 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 flatten#(t) -> c_20(flatten'1#(t)) flatten'1#(node(l,t1,t2)) -> c_22(append#(l,append(flatten(t1),flatten(t2))) ,append#(flatten(t1),flatten(t2)) ,flatten#(t1) ,flatten#(t2)) flattensort#(t) -> c_23(insertionsort#(flatten(t)),flatten#(t)) insertionsort#(l) -> c_29(insertionsort'1#(l)) insertionsort'1#(dd(x,xs)) -> c_30(insert#(x,insertionsort(xs)),insertionsort#(xs)) and a lower component 'compare#('neg(x),'neg(y)) -> c_9('compare#(y,x)) 'compare#('pos(x),'pos(y)) -> c_13('compare#(x,y)) 'compare#('s(x),'s(y)) -> c_15('compare#(x,y)) 'less#(x,y) -> c_16('compare#(x,y)) append#(l1,l2) -> c_17(append'1#(l1,l2)) append'1#(dd(x,xs),l2) -> c_18(append#(xs,l2)) insert#(x,l) -> c_24(insert'1#(l,x)) insert'1#(dd(y,ys),x) -> c_25(insert'2#('less(y,x),x,y,ys),'less#(y,x)) insert'2#('true(),x,y,ys) -> c_28(insert#(x,ys)) Further, following extension rules are added to the lower component. flatten#(t) -> flatten'1#(t) flatten'1#(node(l,t1,t2)) -> append#(l,append(flatten(t1),flatten(t2))) flatten'1#(node(l,t1,t2)) -> append#(flatten(t1),flatten(t2)) flatten'1#(node(l,t1,t2)) -> flatten#(t1) flatten'1#(node(l,t1,t2)) -> flatten#(t2) flattensort#(t) -> flatten#(t) flattensort#(t) -> insertionsort#(flatten(t)) insertionsort#(l) -> insertionsort'1#(l) insertionsort'1#(dd(x,xs)) -> insert#(x,insertionsort(xs)) insertionsort'1#(dd(x,xs)) -> insertionsort#(xs) ** Step 6.a:1: SimplifyRHS WORST_CASE(?,O(n^1)) + Considered Problem: - Strict DPs: flatten#(t) -> c_20(flatten'1#(t)) flatten'1#(node(l,t1,t2)) -> c_22(append#(l,append(flatten(t1),flatten(t2))) ,append#(flatten(t1),flatten(t2)) ,flatten#(t1) ,flatten#(t2)) flattensort#(t) -> c_23(insertionsort#(flatten(t)),flatten#(t)) insertionsort#(l) -> c_29(insertionsort'1#(l)) insertionsort'1#(dd(x,xs)) -> c_30(insert#(x,insertionsort(xs)),insertionsort#(xs)) - 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) 'less(x,y) -> 'cklt('compare(x,y)) append(l1,l2) -> append'1(l1,l2) append'1(dd(x,xs),l2) -> dd(x,append(xs,l2)) append'1(nil(),l2) -> l2 flatten(t) -> flatten'1(t) flatten'1(leaf()) -> nil() flatten'1(node(l,t1,t2)) -> append(l,append(flatten(t1),flatten(t2))) insert(x,l) -> insert'1(l,x) insert'1(dd(y,ys),x) -> insert'2('less(y,x),x,y,ys) insert'1(nil(),x) -> dd(x,nil()) insert'2('false(),x,y,ys) -> dd(x,dd(y,ys)) insert'2('true(),x,y,ys) -> dd(y,insert(x,ys)) insertionsort(l) -> insertionsort'1(l) insertionsort'1(dd(x,xs)) -> insert(x,insertionsort(xs)) insertionsort'1(nil()) -> nil() - Signature: {'cklt/1,'compare/2,'less/2,append/2,append'1/2,flatten/1,flatten'1/1,flattensort/1,insert/2,insert'1/2 ,insert'2/4,insertionsort/1,insertionsort'1/1,'cklt#/1,'compare#/2,'less#/2,append#/2,append'1#/2,flatten#/1 ,flatten'1#/1,flattensort#/1,insert#/2,insert'1#/2,insert'2#/4,insertionsort#/1,insertionsort'1#/1} / {'0/0 ,'EQ/0,'GT/0,'LT/0,'false/0,'neg/1,'pos/1,'s/1,'true/0,dd/2,leaf/0,nil/0,node/3,c_1/0,c_2/0,c_3/0,c_4/0 ,c_5/0,c_6/0,c_7/0,c_8/0,c_9/1,c_10/0,c_11/0,c_12/0,c_13/1,c_14/0,c_15/1,c_16/1,c_17/1,c_18/1,c_19/0,c_20/1 ,c_21/0,c_22/4,c_23/2,c_24/1,c_25/2,c_26/0,c_27/0,c_28/1,c_29/1,c_30/2,c_31/0} - Obligation: innermost runtime complexity wrt. defined symbols {'cklt#,'compare#,'less#,append#,append'1#,flatten# ,flatten'1#,flattensort#,insert#,insert'1#,insert'2#,insertionsort#,insertionsort'1#} and constructors {'0 ,'EQ,'GT,'LT,'false,'neg,'pos,'s,'true,dd,leaf,nil,node} + Applied Processor: SimplifyRHS + Details: Consider the dependency graph 1:S:flatten#(t) -> c_20(flatten'1#(t)) -->_1 flatten'1#(node(l,t1,t2)) -> c_22(append#(l,append(flatten(t1),flatten(t2))) ,append#(flatten(t1),flatten(t2)) ,flatten#(t1) ,flatten#(t2)):2 2:S:flatten'1#(node(l,t1,t2)) -> c_22(append#(l,append(flatten(t1),flatten(t2))) ,append#(flatten(t1),flatten(t2)) ,flatten#(t1) ,flatten#(t2)) -->_4 flatten#(t) -> c_20(flatten'1#(t)):1 -->_3 flatten#(t) -> c_20(flatten'1#(t)):1 3:S:flattensort#(t) -> c_23(insertionsort#(flatten(t)),flatten#(t)) -->_1 insertionsort#(l) -> c_29(insertionsort'1#(l)):4 -->_2 flatten#(t) -> c_20(flatten'1#(t)):1 4:S:insertionsort#(l) -> c_29(insertionsort'1#(l)) -->_1 insertionsort'1#(dd(x,xs)) -> c_30(insert#(x,insertionsort(xs)),insertionsort#(xs)):5 5:S:insertionsort'1#(dd(x,xs)) -> c_30(insert#(x,insertionsort(xs)),insertionsort#(xs)) -->_2 insertionsort#(l) -> c_29(insertionsort'1#(l)):4 Due to missing edges in the depndency graph, the right-hand sides of following rules could be simplified: flatten'1#(node(l,t1,t2)) -> c_22(flatten#(t1),flatten#(t2)) insertionsort'1#(dd(x,xs)) -> c_30(insertionsort#(xs)) ** Step 6.a:2: UsableRules WORST_CASE(?,O(n^1)) + Considered Problem: - Strict DPs: flatten#(t) -> c_20(flatten'1#(t)) flatten'1#(node(l,t1,t2)) -> c_22(flatten#(t1),flatten#(t2)) flattensort#(t) -> c_23(insertionsort#(flatten(t)),flatten#(t)) insertionsort#(l) -> c_29(insertionsort'1#(l)) insertionsort'1#(dd(x,xs)) -> c_30(insertionsort#(xs)) - 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) 'less(x,y) -> 'cklt('compare(x,y)) append(l1,l2) -> append'1(l1,l2) append'1(dd(x,xs),l2) -> dd(x,append(xs,l2)) append'1(nil(),l2) -> l2 flatten(t) -> flatten'1(t) flatten'1(leaf()) -> nil() flatten'1(node(l,t1,t2)) -> append(l,append(flatten(t1),flatten(t2))) insert(x,l) -> insert'1(l,x) insert'1(dd(y,ys),x) -> insert'2('less(y,x),x,y,ys) insert'1(nil(),x) -> dd(x,nil()) insert'2('false(),x,y,ys) -> dd(x,dd(y,ys)) insert'2('true(),x,y,ys) -> dd(y,insert(x,ys)) insertionsort(l) -> insertionsort'1(l) insertionsort'1(dd(x,xs)) -> insert(x,insertionsort(xs)) insertionsort'1(nil()) -> nil() - Signature: {'cklt/1,'compare/2,'less/2,append/2,append'1/2,flatten/1,flatten'1/1,flattensort/1,insert/2,insert'1/2 ,insert'2/4,insertionsort/1,insertionsort'1/1,'cklt#/1,'compare#/2,'less#/2,append#/2,append'1#/2,flatten#/1 ,flatten'1#/1,flattensort#/1,insert#/2,insert'1#/2,insert'2#/4,insertionsort#/1,insertionsort'1#/1} / {'0/0 ,'EQ/0,'GT/0,'LT/0,'false/0,'neg/1,'pos/1,'s/1,'true/0,dd/2,leaf/0,nil/0,node/3,c_1/0,c_2/0,c_3/0,c_4/0 ,c_5/0,c_6/0,c_7/0,c_8/0,c_9/1,c_10/0,c_11/0,c_12/0,c_13/1,c_14/0,c_15/1,c_16/1,c_17/1,c_18/1,c_19/0,c_20/1 ,c_21/0,c_22/2,c_23/2,c_24/1,c_25/2,c_26/0,c_27/0,c_28/1,c_29/1,c_30/1,c_31/0} - Obligation: innermost runtime complexity wrt. defined symbols {'cklt#,'compare#,'less#,append#,append'1#,flatten# ,flatten'1#,flattensort#,insert#,insert'1#,insert'2#,insertionsort#,insertionsort'1#} and constructors {'0 ,'EQ,'GT,'LT,'false,'neg,'pos,'s,'true,dd,leaf,nil,node} + Applied Processor: UsableRules + Details: We replace rewrite rules by usable rules: append(l1,l2) -> append'1(l1,l2) append'1(dd(x,xs),l2) -> dd(x,append(xs,l2)) append'1(nil(),l2) -> l2 flatten(t) -> flatten'1(t) flatten'1(leaf()) -> nil() flatten'1(node(l,t1,t2)) -> append(l,append(flatten(t1),flatten(t2))) flatten#(t) -> c_20(flatten'1#(t)) flatten'1#(node(l,t1,t2)) -> c_22(flatten#(t1),flatten#(t2)) flattensort#(t) -> c_23(insertionsort#(flatten(t)),flatten#(t)) insertionsort#(l) -> c_29(insertionsort'1#(l)) insertionsort'1#(dd(x,xs)) -> c_30(insertionsort#(xs)) ** Step 6.a:3: WeightGap WORST_CASE(?,O(n^1)) + Considered Problem: - Strict DPs: flatten#(t) -> c_20(flatten'1#(t)) flatten'1#(node(l,t1,t2)) -> c_22(flatten#(t1),flatten#(t2)) flattensort#(t) -> c_23(insertionsort#(flatten(t)),flatten#(t)) insertionsort#(l) -> c_29(insertionsort'1#(l)) insertionsort'1#(dd(x,xs)) -> c_30(insertionsort#(xs)) - Weak TRS: append(l1,l2) -> append'1(l1,l2) append'1(dd(x,xs),l2) -> dd(x,append(xs,l2)) append'1(nil(),l2) -> l2 flatten(t) -> flatten'1(t) flatten'1(leaf()) -> nil() flatten'1(node(l,t1,t2)) -> append(l,append(flatten(t1),flatten(t2))) - Signature: {'cklt/1,'compare/2,'less/2,append/2,append'1/2,flatten/1,flatten'1/1,flattensort/1,insert/2,insert'1/2 ,insert'2/4,insertionsort/1,insertionsort'1/1,'cklt#/1,'compare#/2,'less#/2,append#/2,append'1#/2,flatten#/1 ,flatten'1#/1,flattensort#/1,insert#/2,insert'1#/2,insert'2#/4,insertionsort#/1,insertionsort'1#/1} / {'0/0 ,'EQ/0,'GT/0,'LT/0,'false/0,'neg/1,'pos/1,'s/1,'true/0,dd/2,leaf/0,nil/0,node/3,c_1/0,c_2/0,c_3/0,c_4/0 ,c_5/0,c_6/0,c_7/0,c_8/0,c_9/1,c_10/0,c_11/0,c_12/0,c_13/1,c_14/0,c_15/1,c_16/1,c_17/1,c_18/1,c_19/0,c_20/1 ,c_21/0,c_22/2,c_23/2,c_24/1,c_25/2,c_26/0,c_27/0,c_28/1,c_29/1,c_30/1,c_31/0} - Obligation: innermost runtime complexity wrt. defined symbols {'cklt#,'compare#,'less#,append#,append'1#,flatten# ,flatten'1#,flattensort#,insert#,insert'1#,insert'2#,insertionsort#,insertionsort'1#} and constructors {'0 ,'EQ,'GT,'LT,'false,'neg,'pos,'s,'true,dd,leaf,nil,node} + 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(append) = {1,2}, uargs(dd) = {2}, uargs(insertionsort#) = {1}, uargs(c_20) = {1}, uargs(c_22) = {1,2}, uargs(c_23) = {1,2}, uargs(c_29) = {1}, uargs(c_30) = {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('cklt) = [0] p('compare) = [0] p('false) = [0] p('less) = [0] p('neg) = [1] x1 + [0] p('pos) = [1] x1 + [0] p('s) = [1] x1 + [0] p('true) = [0] p(append) = [1] x1 + [1] x2 + [0] p(append'1) = [1] x1 + [1] x2 + [0] p(dd) = [1] x1 + [1] x2 + [1] p(flatten) = [1] x1 + [0] p(flatten'1) = [1] x1 + [0] p(flattensort) = [0] p(insert) = [0] p(insert'1) = [0] p(insert'2) = [0] p(insertionsort) = [0] p(insertionsort'1) = [0] p(leaf) = [0] p(nil) = [0] p(node) = [1] x1 + [1] x2 + [1] x3 + [0] p('cklt#) = [1] p('compare#) = [0] p('less#) = [0] p(append#) = [0] p(append'1#) = [0] p(flatten#) = [0] p(flatten'1#) = [0] p(flattensort#) = [1] x1 + [0] p(insert#) = [0] p(insert'1#) = [0] p(insert'2#) = [0] p(insertionsort#) = [1] x1 + [0] p(insertionsort'1#) = [1] x1 + [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) = [0] p(c_17) = [0] p(c_18) = [0] p(c_19) = [0] p(c_20) = [1] x1 + [0] p(c_21) = [0] p(c_22) = [1] x1 + [1] x2 + [0] p(c_23) = [1] x1 + [1] x2 + [0] p(c_24) = [0] p(c_25) = [0] p(c_26) = [0] p(c_27) = [0] p(c_28) = [0] p(c_29) = [1] x1 + [0] p(c_30) = [1] x1 + [0] p(c_31) = [0] Following rules are strictly oriented: insertionsort'1#(dd(x,xs)) = [1] x + [1] xs + [1] > [1] xs + [0] = c_30(insertionsort#(xs)) Following rules are (at-least) weakly oriented: flatten#(t) = [0] >= [0] = c_20(flatten'1#(t)) flatten'1#(node(l,t1,t2)) = [0] >= [0] = c_22(flatten#(t1),flatten#(t2)) flattensort#(t) = [1] t + [0] >= [1] t + [0] = c_23(insertionsort#(flatten(t)),flatten#(t)) insertionsort#(l) = [1] l + [0] >= [1] l + [0] = c_29(insertionsort'1#(l)) append(l1,l2) = [1] l1 + [1] l2 + [0] >= [1] l1 + [1] l2 + [0] = append'1(l1,l2) append'1(dd(x,xs),l2) = [1] l2 + [1] x + [1] xs + [1] >= [1] l2 + [1] x + [1] xs + [1] = dd(x,append(xs,l2)) append'1(nil(),l2) = [1] l2 + [0] >= [1] l2 + [0] = l2 flatten(t) = [1] t + [0] >= [1] t + [0] = flatten'1(t) flatten'1(leaf()) = [0] >= [0] = nil() flatten'1(node(l,t1,t2)) = [1] l + [1] t1 + [1] t2 + [0] >= [1] l + [1] t1 + [1] t2 + [0] = append(l,append(flatten(t1),flatten(t2))) Further, it can be verified that all rules not oriented are covered by the weightgap condition. ** Step 6.a:4: WeightGap WORST_CASE(?,O(n^1)) + Considered Problem: - Strict DPs: flatten#(t) -> c_20(flatten'1#(t)) flatten'1#(node(l,t1,t2)) -> c_22(flatten#(t1),flatten#(t2)) flattensort#(t) -> c_23(insertionsort#(flatten(t)),flatten#(t)) insertionsort#(l) -> c_29(insertionsort'1#(l)) - Weak DPs: insertionsort'1#(dd(x,xs)) -> c_30(insertionsort#(xs)) - Weak TRS: append(l1,l2) -> append'1(l1,l2) append'1(dd(x,xs),l2) -> dd(x,append(xs,l2)) append'1(nil(),l2) -> l2 flatten(t) -> flatten'1(t) flatten'1(leaf()) -> nil() flatten'1(node(l,t1,t2)) -> append(l,append(flatten(t1),flatten(t2))) - Signature: {'cklt/1,'compare/2,'less/2,append/2,append'1/2,flatten/1,flatten'1/1,flattensort/1,insert/2,insert'1/2 ,insert'2/4,insertionsort/1,insertionsort'1/1,'cklt#/1,'compare#/2,'less#/2,append#/2,append'1#/2,flatten#/1 ,flatten'1#/1,flattensort#/1,insert#/2,insert'1#/2,insert'2#/4,insertionsort#/1,insertionsort'1#/1} / {'0/0 ,'EQ/0,'GT/0,'LT/0,'false/0,'neg/1,'pos/1,'s/1,'true/0,dd/2,leaf/0,nil/0,node/3,c_1/0,c_2/0,c_3/0,c_4/0 ,c_5/0,c_6/0,c_7/0,c_8/0,c_9/1,c_10/0,c_11/0,c_12/0,c_13/1,c_14/0,c_15/1,c_16/1,c_17/1,c_18/1,c_19/0,c_20/1 ,c_21/0,c_22/2,c_23/2,c_24/1,c_25/2,c_26/0,c_27/0,c_28/1,c_29/1,c_30/1,c_31/0} - Obligation: innermost runtime complexity wrt. defined symbols {'cklt#,'compare#,'less#,append#,append'1#,flatten# ,flatten'1#,flattensort#,insert#,insert'1#,insert'2#,insertionsort#,insertionsort'1#} and constructors {'0 ,'EQ,'GT,'LT,'false,'neg,'pos,'s,'true,dd,leaf,nil,node} + 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(append) = {1,2}, uargs(dd) = {2}, uargs(insertionsort#) = {1}, uargs(c_20) = {1}, uargs(c_22) = {1,2}, uargs(c_23) = {1,2}, uargs(c_29) = {1}, uargs(c_30) = {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('cklt) = [0] p('compare) = [0] p('false) = [0] p('less) = [0] p('neg) = [1] x1 + [0] p('pos) = [1] x1 + [0] p('s) = [1] x1 + [0] p('true) = [0] p(append) = [1] x1 + [1] x2 + [3] p(append'1) = [1] x1 + [1] x2 + [3] p(dd) = [1] x2 + [2] p(flatten) = [2] x1 + [0] p(flatten'1) = [2] x1 + [0] p(flattensort) = [0] p(insert) = [0] p(insert'1) = [0] p(insert'2) = [0] p(insertionsort) = [0] p(insertionsort'1) = [0] p(leaf) = [6] p(nil) = [0] p(node) = [1] x1 + [1] x2 + [1] x3 + [5] p('cklt#) = [0] p('compare#) = [0] p('less#) = [0] p(append#) = [0] p(append'1#) = [2] x2 + [0] p(flatten#) = [2] x1 + [0] p(flatten'1#) = [2] x1 + [0] p(flattensort#) = [6] x1 + [1] p(insert#) = [0] p(insert'1#) = [0] p(insert'2#) = [2] x2 + [2] x3 + [0] p(insertionsort#) = [1] x1 + [2] p(insertionsort'1#) = [1] x1 + [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) = [0] p(c_17) = [0] p(c_18) = [0] p(c_19) = [0] p(c_20) = [1] x1 + [0] p(c_21) = [0] p(c_22) = [1] x1 + [1] x2 + [0] p(c_23) = [1] x1 + [1] x2 + [3] p(c_24) = [0] p(c_25) = [0] p(c_26) = [0] p(c_27) = [0] p(c_28) = [0] p(c_29) = [1] x1 + [0] p(c_30) = [1] x1 + [0] p(c_31) = [0] Following rules are strictly oriented: flatten'1#(node(l,t1,t2)) = [2] l + [2] t1 + [2] t2 + [10] > [2] t1 + [2] t2 + [0] = c_22(flatten#(t1),flatten#(t2)) insertionsort#(l) = [1] l + [2] > [1] l + [0] = c_29(insertionsort'1#(l)) Following rules are (at-least) weakly oriented: flatten#(t) = [2] t + [0] >= [2] t + [0] = c_20(flatten'1#(t)) flattensort#(t) = [6] t + [1] >= [4] t + [5] = c_23(insertionsort#(flatten(t)),flatten#(t)) insertionsort'1#(dd(x,xs)) = [1] xs + [2] >= [1] xs + [2] = c_30(insertionsort#(xs)) append(l1,l2) = [1] l1 + [1] l2 + [3] >= [1] l1 + [1] l2 + [3] = append'1(l1,l2) append'1(dd(x,xs),l2) = [1] l2 + [1] xs + [5] >= [1] l2 + [1] xs + [5] = dd(x,append(xs,l2)) append'1(nil(),l2) = [1] l2 + [3] >= [1] l2 + [0] = l2 flatten(t) = [2] t + [0] >= [2] t + [0] = flatten'1(t) flatten'1(leaf()) = [12] >= [0] = nil() flatten'1(node(l,t1,t2)) = [2] l + [2] t1 + [2] t2 + [10] >= [1] l + [2] t1 + [2] t2 + [6] = append(l,append(flatten(t1),flatten(t2))) Further, it can be verified that all rules not oriented are covered by the weightgap condition. ** Step 6.a:5: WeightGap WORST_CASE(?,O(n^1)) + Considered Problem: - Strict DPs: flatten#(t) -> c_20(flatten'1#(t)) flattensort#(t) -> c_23(insertionsort#(flatten(t)),flatten#(t)) - Weak DPs: flatten'1#(node(l,t1,t2)) -> c_22(flatten#(t1),flatten#(t2)) insertionsort#(l) -> c_29(insertionsort'1#(l)) insertionsort'1#(dd(x,xs)) -> c_30(insertionsort#(xs)) - Weak TRS: append(l1,l2) -> append'1(l1,l2) append'1(dd(x,xs),l2) -> dd(x,append(xs,l2)) append'1(nil(),l2) -> l2 flatten(t) -> flatten'1(t) flatten'1(leaf()) -> nil() flatten'1(node(l,t1,t2)) -> append(l,append(flatten(t1),flatten(t2))) - Signature: {'cklt/1,'compare/2,'less/2,append/2,append'1/2,flatten/1,flatten'1/1,flattensort/1,insert/2,insert'1/2 ,insert'2/4,insertionsort/1,insertionsort'1/1,'cklt#/1,'compare#/2,'less#/2,append#/2,append'1#/2,flatten#/1 ,flatten'1#/1,flattensort#/1,insert#/2,insert'1#/2,insert'2#/4,insertionsort#/1,insertionsort'1#/1} / {'0/0 ,'EQ/0,'GT/0,'LT/0,'false/0,'neg/1,'pos/1,'s/1,'true/0,dd/2,leaf/0,nil/0,node/3,c_1/0,c_2/0,c_3/0,c_4/0 ,c_5/0,c_6/0,c_7/0,c_8/0,c_9/1,c_10/0,c_11/0,c_12/0,c_13/1,c_14/0,c_15/1,c_16/1,c_17/1,c_18/1,c_19/0,c_20/1 ,c_21/0,c_22/2,c_23/2,c_24/1,c_25/2,c_26/0,c_27/0,c_28/1,c_29/1,c_30/1,c_31/0} - Obligation: innermost runtime complexity wrt. defined symbols {'cklt#,'compare#,'less#,append#,append'1#,flatten# ,flatten'1#,flattensort#,insert#,insert'1#,insert'2#,insertionsort#,insertionsort'1#} and constructors {'0 ,'EQ,'GT,'LT,'false,'neg,'pos,'s,'true,dd,leaf,nil,node} + 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(append) = {1,2}, uargs(dd) = {2}, uargs(insertionsort#) = {1}, uargs(c_20) = {1}, uargs(c_22) = {1,2}, uargs(c_23) = {1,2}, uargs(c_29) = {1}, uargs(c_30) = {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('cklt) = [0] p('compare) = [0] p('false) = [0] p('less) = [0] p('neg) = [1] x1 + [0] p('pos) = [1] x1 + [0] p('s) = [1] x1 + [0] p('true) = [0] p(append) = [1] x1 + [1] x2 + [0] p(append'1) = [1] x1 + [1] x2 + [0] p(dd) = [1] x1 + [1] x2 + [0] p(flatten) = [1] x1 + [0] p(flatten'1) = [1] x1 + [0] p(flattensort) = [0] p(insert) = [0] p(insert'1) = [0] p(insert'2) = [0] p(insertionsort) = [0] p(insertionsort'1) = [0] p(leaf) = [0] p(nil) = [0] p(node) = [1] x1 + [1] x2 + [1] x3 + [0] p('cklt#) = [0] p('compare#) = [0] p('less#) = [0] p(append#) = [0] p(append'1#) = [0] p(flatten#) = [0] p(flatten'1#) = [0] p(flattensort#) = [1] x1 + [5] p(insert#) = [0] p(insert'1#) = [0] p(insert'2#) = [0] p(insertionsort#) = [1] x1 + [0] p(insertionsort'1#) = [1] x1 + [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) = [0] p(c_17) = [0] p(c_18) = [0] p(c_19) = [0] p(c_20) = [1] x1 + [0] p(c_21) = [0] p(c_22) = [1] x1 + [1] x2 + [0] p(c_23) = [1] x1 + [1] x2 + [0] p(c_24) = [0] p(c_25) = [0] p(c_26) = [0] p(c_27) = [0] p(c_28) = [0] p(c_29) = [1] x1 + [0] p(c_30) = [1] x1 + [0] p(c_31) = [0] Following rules are strictly oriented: flattensort#(t) = [1] t + [5] > [1] t + [0] = c_23(insertionsort#(flatten(t)),flatten#(t)) Following rules are (at-least) weakly oriented: flatten#(t) = [0] >= [0] = c_20(flatten'1#(t)) flatten'1#(node(l,t1,t2)) = [0] >= [0] = c_22(flatten#(t1),flatten#(t2)) insertionsort#(l) = [1] l + [0] >= [1] l + [0] = c_29(insertionsort'1#(l)) insertionsort'1#(dd(x,xs)) = [1] x + [1] xs + [0] >= [1] xs + [0] = c_30(insertionsort#(xs)) append(l1,l2) = [1] l1 + [1] l2 + [0] >= [1] l1 + [1] l2 + [0] = append'1(l1,l2) append'1(dd(x,xs),l2) = [1] l2 + [1] x + [1] xs + [0] >= [1] l2 + [1] x + [1] xs + [0] = dd(x,append(xs,l2)) append'1(nil(),l2) = [1] l2 + [0] >= [1] l2 + [0] = l2 flatten(t) = [1] t + [0] >= [1] t + [0] = flatten'1(t) flatten'1(leaf()) = [0] >= [0] = nil() flatten'1(node(l,t1,t2)) = [1] l + [1] t1 + [1] t2 + [0] >= [1] l + [1] t1 + [1] t2 + [0] = append(l,append(flatten(t1),flatten(t2))) Further, it can be verified that all rules not oriented are covered by the weightgap condition. ** Step 6.a:6: NaturalMI WORST_CASE(?,O(n^1)) + Considered Problem: - Strict DPs: flatten#(t) -> c_20(flatten'1#(t)) - Weak DPs: flatten'1#(node(l,t1,t2)) -> c_22(flatten#(t1),flatten#(t2)) flattensort#(t) -> c_23(insertionsort#(flatten(t)),flatten#(t)) insertionsort#(l) -> c_29(insertionsort'1#(l)) insertionsort'1#(dd(x,xs)) -> c_30(insertionsort#(xs)) - Weak TRS: append(l1,l2) -> append'1(l1,l2) append'1(dd(x,xs),l2) -> dd(x,append(xs,l2)) append'1(nil(),l2) -> l2 flatten(t) -> flatten'1(t) flatten'1(leaf()) -> nil() flatten'1(node(l,t1,t2)) -> append(l,append(flatten(t1),flatten(t2))) - Signature: {'cklt/1,'compare/2,'less/2,append/2,append'1/2,flatten/1,flatten'1/1,flattensort/1,insert/2,insert'1/2 ,insert'2/4,insertionsort/1,insertionsort'1/1,'cklt#/1,'compare#/2,'less#/2,append#/2,append'1#/2,flatten#/1 ,flatten'1#/1,flattensort#/1,insert#/2,insert'1#/2,insert'2#/4,insertionsort#/1,insertionsort'1#/1} / {'0/0 ,'EQ/0,'GT/0,'LT/0,'false/0,'neg/1,'pos/1,'s/1,'true/0,dd/2,leaf/0,nil/0,node/3,c_1/0,c_2/0,c_3/0,c_4/0 ,c_5/0,c_6/0,c_7/0,c_8/0,c_9/1,c_10/0,c_11/0,c_12/0,c_13/1,c_14/0,c_15/1,c_16/1,c_17/1,c_18/1,c_19/0,c_20/1 ,c_21/0,c_22/2,c_23/2,c_24/1,c_25/2,c_26/0,c_27/0,c_28/1,c_29/1,c_30/1,c_31/0} - Obligation: innermost runtime complexity wrt. defined symbols {'cklt#,'compare#,'less#,append#,append'1#,flatten# ,flatten'1#,flattensort#,insert#,insert'1#,insert'2#,insertionsort#,insertionsort'1#} and constructors {'0 ,'EQ,'GT,'LT,'false,'neg,'pos,'s,'true,dd,leaf,nil,node} + 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_20) = {1}, uargs(c_22) = {1,2}, uargs(c_23) = {1,2}, uargs(c_29) = {1}, uargs(c_30) = {1} Following symbols are considered usable: {'cklt#,'compare#,'less#,append#,append'1#,flatten#,flatten'1#,flattensort#,insert#,insert'1#,insert'2# ,insertionsort#,insertionsort'1#} TcT has computed the following interpretation: p('0) = [0] p('EQ) = [0] p('GT) = [0] p('LT) = [0] p('cklt) = [0] p('compare) = [0] p('false) = [0] p('less) = [0] p('neg) = [1] x1 + [0] p('pos) = [1] x1 + [0] p('s) = [1] x1 + [0] p('true) = [0] p(append) = [0] p(append'1) = [3] x1 + [0] p(dd) = [1] x1 + [1] p(flatten) = [0] p(flatten'1) = [0] p(flattensort) = [0] p(insert) = [1] x2 + [0] p(insert'1) = [1] p(insert'2) = [1] x1 + [1] x3 + [1] p(insertionsort) = [0] p(insertionsort'1) = [4] x1 + [0] p(leaf) = [0] p(nil) = [0] p(node) = [1] x2 + [1] x3 + [2] p('cklt#) = [1] x1 + [1] p('compare#) = [1] x1 + [1] x2 + [0] p('less#) = [2] x1 + [1] x2 + [1] p(append#) = [1] x1 + [2] x2 + [4] p(append'1#) = [1] x1 + [1] x2 + [1] p(flatten#) = [8] x1 + [1] p(flatten'1#) = [8] x1 + [0] p(flattensort#) = [8] x1 + [3] p(insert#) = [1] x1 + [2] x2 + [1] p(insert'1#) = [2] x1 + [0] p(insert'2#) = [2] x1 + [2] x2 + [4] x4 + [0] p(insertionsort#) = [0] p(insertionsort'1#) = [0] p(c_1) = [1] p(c_2) = [2] p(c_3) = [1] p(c_4) = [0] p(c_5) = [0] p(c_6) = [0] p(c_7) = [2] p(c_8) = [4] p(c_9) = [2] p(c_10) = [1] p(c_11) = [1] p(c_12) = [0] p(c_13) = [1] x1 + [1] p(c_14) = [8] p(c_15) = [1] x1 + [0] p(c_16) = [4] p(c_17) = [1] p(c_18) = [1] p(c_19) = [1] p(c_20) = [1] x1 + [0] p(c_21) = [0] p(c_22) = [1] x1 + [1] x2 + [7] p(c_23) = [4] x1 + [1] x2 + [1] p(c_24) = [8] p(c_25) = [8] x2 + [1] p(c_26) = [1] p(c_27) = [0] p(c_28) = [1] p(c_29) = [8] x1 + [0] p(c_30) = [2] x1 + [0] p(c_31) = [0] Following rules are strictly oriented: flatten#(t) = [8] t + [1] > [8] t + [0] = c_20(flatten'1#(t)) Following rules are (at-least) weakly oriented: flatten'1#(node(l,t1,t2)) = [8] t1 + [8] t2 + [16] >= [8] t1 + [8] t2 + [9] = c_22(flatten#(t1),flatten#(t2)) flattensort#(t) = [8] t + [3] >= [8] t + [2] = c_23(insertionsort#(flatten(t)),flatten#(t)) insertionsort#(l) = [0] >= [0] = c_29(insertionsort'1#(l)) insertionsort'1#(dd(x,xs)) = [0] >= [0] = c_30(insertionsort#(xs)) ** Step 6.a:7: EmptyProcessor WORST_CASE(?,O(1)) + Considered Problem: - Weak DPs: flatten#(t) -> c_20(flatten'1#(t)) flatten'1#(node(l,t1,t2)) -> c_22(flatten#(t1),flatten#(t2)) flattensort#(t) -> c_23(insertionsort#(flatten(t)),flatten#(t)) insertionsort#(l) -> c_29(insertionsort'1#(l)) insertionsort'1#(dd(x,xs)) -> c_30(insertionsort#(xs)) - Weak TRS: append(l1,l2) -> append'1(l1,l2) append'1(dd(x,xs),l2) -> dd(x,append(xs,l2)) append'1(nil(),l2) -> l2 flatten(t) -> flatten'1(t) flatten'1(leaf()) -> nil() flatten'1(node(l,t1,t2)) -> append(l,append(flatten(t1),flatten(t2))) - Signature: {'cklt/1,'compare/2,'less/2,append/2,append'1/2,flatten/1,flatten'1/1,flattensort/1,insert/2,insert'1/2 ,insert'2/4,insertionsort/1,insertionsort'1/1,'cklt#/1,'compare#/2,'less#/2,append#/2,append'1#/2,flatten#/1 ,flatten'1#/1,flattensort#/1,insert#/2,insert'1#/2,insert'2#/4,insertionsort#/1,insertionsort'1#/1} / {'0/0 ,'EQ/0,'GT/0,'LT/0,'false/0,'neg/1,'pos/1,'s/1,'true/0,dd/2,leaf/0,nil/0,node/3,c_1/0,c_2/0,c_3/0,c_4/0 ,c_5/0,c_6/0,c_7/0,c_8/0,c_9/1,c_10/0,c_11/0,c_12/0,c_13/1,c_14/0,c_15/1,c_16/1,c_17/1,c_18/1,c_19/0,c_20/1 ,c_21/0,c_22/2,c_23/2,c_24/1,c_25/2,c_26/0,c_27/0,c_28/1,c_29/1,c_30/1,c_31/0} - Obligation: innermost runtime complexity wrt. defined symbols {'cklt#,'compare#,'less#,append#,append'1#,flatten# ,flatten'1#,flattensort#,insert#,insert'1#,insert'2#,insertionsort#,insertionsort'1#} and constructors {'0 ,'EQ,'GT,'LT,'false,'neg,'pos,'s,'true,dd,leaf,nil,node} + Applied Processor: EmptyProcessor + Details: The problem is already closed. The intended complexity is O(1). ** Step 6.b:1: DecomposeDG WORST_CASE(?,O(n^2)) + Considered Problem: - Strict DPs: 'compare#('neg(x),'neg(y)) -> c_9('compare#(y,x)) 'compare#('pos(x),'pos(y)) -> c_13('compare#(x,y)) 'compare#('s(x),'s(y)) -> c_15('compare#(x,y)) 'less#(x,y) -> c_16('compare#(x,y)) append#(l1,l2) -> c_17(append'1#(l1,l2)) append'1#(dd(x,xs),l2) -> c_18(append#(xs,l2)) insert#(x,l) -> c_24(insert'1#(l,x)) insert'1#(dd(y,ys),x) -> c_25(insert'2#('less(y,x),x,y,ys),'less#(y,x)) insert'2#('true(),x,y,ys) -> c_28(insert#(x,ys)) - Weak DPs: flatten#(t) -> flatten'1#(t) flatten'1#(node(l,t1,t2)) -> append#(l,append(flatten(t1),flatten(t2))) flatten'1#(node(l,t1,t2)) -> append#(flatten(t1),flatten(t2)) flatten'1#(node(l,t1,t2)) -> flatten#(t1) flatten'1#(node(l,t1,t2)) -> flatten#(t2) flattensort#(t) -> flatten#(t) flattensort#(t) -> insertionsort#(flatten(t)) insertionsort#(l) -> insertionsort'1#(l) insertionsort'1#(dd(x,xs)) -> insert#(x,insertionsort(xs)) insertionsort'1#(dd(x,xs)) -> insertionsort#(xs) - 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) 'less(x,y) -> 'cklt('compare(x,y)) append(l1,l2) -> append'1(l1,l2) append'1(dd(x,xs),l2) -> dd(x,append(xs,l2)) append'1(nil(),l2) -> l2 flatten(t) -> flatten'1(t) flatten'1(leaf()) -> nil() flatten'1(node(l,t1,t2)) -> append(l,append(flatten(t1),flatten(t2))) insert(x,l) -> insert'1(l,x) insert'1(dd(y,ys),x) -> insert'2('less(y,x),x,y,ys) insert'1(nil(),x) -> dd(x,nil()) insert'2('false(),x,y,ys) -> dd(x,dd(y,ys)) insert'2('true(),x,y,ys) -> dd(y,insert(x,ys)) insertionsort(l) -> insertionsort'1(l) insertionsort'1(dd(x,xs)) -> insert(x,insertionsort(xs)) insertionsort'1(nil()) -> nil() - Signature: {'cklt/1,'compare/2,'less/2,append/2,append'1/2,flatten/1,flatten'1/1,flattensort/1,insert/2,insert'1/2 ,insert'2/4,insertionsort/1,insertionsort'1/1,'cklt#/1,'compare#/2,'less#/2,append#/2,append'1#/2,flatten#/1 ,flatten'1#/1,flattensort#/1,insert#/2,insert'1#/2,insert'2#/4,insertionsort#/1,insertionsort'1#/1} / {'0/0 ,'EQ/0,'GT/0,'LT/0,'false/0,'neg/1,'pos/1,'s/1,'true/0,dd/2,leaf/0,nil/0,node/3,c_1/0,c_2/0,c_3/0,c_4/0 ,c_5/0,c_6/0,c_7/0,c_8/0,c_9/1,c_10/0,c_11/0,c_12/0,c_13/1,c_14/0,c_15/1,c_16/1,c_17/1,c_18/1,c_19/0,c_20/1 ,c_21/0,c_22/4,c_23/2,c_24/1,c_25/2,c_26/0,c_27/0,c_28/1,c_29/1,c_30/2,c_31/0} - Obligation: innermost runtime complexity wrt. defined symbols {'cklt#,'compare#,'less#,append#,append'1#,flatten# ,flatten'1#,flattensort#,insert#,insert'1#,insert'2#,insertionsort#,insertionsort'1#} and constructors {'0 ,'EQ,'GT,'LT,'false,'neg,'pos,'s,'true,dd,leaf,nil,node} + 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 append#(l1,l2) -> c_17(append'1#(l1,l2)) append'1#(dd(x,xs),l2) -> c_18(append#(xs,l2)) flatten#(t) -> flatten'1#(t) flatten'1#(node(l,t1,t2)) -> append#(l,append(flatten(t1),flatten(t2))) flatten'1#(node(l,t1,t2)) -> append#(flatten(t1),flatten(t2)) flatten'1#(node(l,t1,t2)) -> flatten#(t1) flatten'1#(node(l,t1,t2)) -> flatten#(t2) flattensort#(t) -> flatten#(t) flattensort#(t) -> insertionsort#(flatten(t)) insert#(x,l) -> c_24(insert'1#(l,x)) insert'1#(dd(y,ys),x) -> c_25(insert'2#('less(y,x),x,y,ys),'less#(y,x)) insert'2#('true(),x,y,ys) -> c_28(insert#(x,ys)) insertionsort#(l) -> insertionsort'1#(l) insertionsort'1#(dd(x,xs)) -> insert#(x,insertionsort(xs)) insertionsort'1#(dd(x,xs)) -> insertionsort#(xs) and a lower component 'compare#('neg(x),'neg(y)) -> c_9('compare#(y,x)) 'compare#('pos(x),'pos(y)) -> c_13('compare#(x,y)) 'compare#('s(x),'s(y)) -> c_15('compare#(x,y)) 'less#(x,y) -> c_16('compare#(x,y)) Further, following extension rules are added to the lower component. append#(l1,l2) -> append'1#(l1,l2) append'1#(dd(x,xs),l2) -> append#(xs,l2) flatten#(t) -> flatten'1#(t) flatten'1#(node(l,t1,t2)) -> append#(l,append(flatten(t1),flatten(t2))) flatten'1#(node(l,t1,t2)) -> append#(flatten(t1),flatten(t2)) flatten'1#(node(l,t1,t2)) -> flatten#(t1) flatten'1#(node(l,t1,t2)) -> flatten#(t2) flattensort#(t) -> flatten#(t) flattensort#(t) -> insertionsort#(flatten(t)) insert#(x,l) -> insert'1#(l,x) insert'1#(dd(y,ys),x) -> 'less#(y,x) insert'1#(dd(y,ys),x) -> insert'2#('less(y,x),x,y,ys) insert'2#('true(),x,y,ys) -> insert#(x,ys) insertionsort#(l) -> insertionsort'1#(l) insertionsort'1#(dd(x,xs)) -> insert#(x,insertionsort(xs)) insertionsort'1#(dd(x,xs)) -> insertionsort#(xs) *** Step 6.b:1.a:1: RemoveHeads WORST_CASE(?,O(n^1)) + Considered Problem: - Strict DPs: append#(l1,l2) -> c_17(append'1#(l1,l2)) append'1#(dd(x,xs),l2) -> c_18(append#(xs,l2)) insert#(x,l) -> c_24(insert'1#(l,x)) insert'1#(dd(y,ys),x) -> c_25(insert'2#('less(y,x),x,y,ys),'less#(y,x)) insert'2#('true(),x,y,ys) -> c_28(insert#(x,ys)) - Weak DPs: flatten#(t) -> flatten'1#(t) flatten'1#(node(l,t1,t2)) -> append#(l,append(flatten(t1),flatten(t2))) flatten'1#(node(l,t1,t2)) -> append#(flatten(t1),flatten(t2)) flatten'1#(node(l,t1,t2)) -> flatten#(t1) flatten'1#(node(l,t1,t2)) -> flatten#(t2) flattensort#(t) -> flatten#(t) flattensort#(t) -> insertionsort#(flatten(t)) insertionsort#(l) -> insertionsort'1#(l) insertionsort'1#(dd(x,xs)) -> insert#(x,insertionsort(xs)) insertionsort'1#(dd(x,xs)) -> insertionsort#(xs) - 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) 'less(x,y) -> 'cklt('compare(x,y)) append(l1,l2) -> append'1(l1,l2) append'1(dd(x,xs),l2) -> dd(x,append(xs,l2)) append'1(nil(),l2) -> l2 flatten(t) -> flatten'1(t) flatten'1(leaf()) -> nil() flatten'1(node(l,t1,t2)) -> append(l,append(flatten(t1),flatten(t2))) insert(x,l) -> insert'1(l,x) insert'1(dd(y,ys),x) -> insert'2('less(y,x),x,y,ys) insert'1(nil(),x) -> dd(x,nil()) insert'2('false(),x,y,ys) -> dd(x,dd(y,ys)) insert'2('true(),x,y,ys) -> dd(y,insert(x,ys)) insertionsort(l) -> insertionsort'1(l) insertionsort'1(dd(x,xs)) -> insert(x,insertionsort(xs)) insertionsort'1(nil()) -> nil() - Signature: {'cklt/1,'compare/2,'less/2,append/2,append'1/2,flatten/1,flatten'1/1,flattensort/1,insert/2,insert'1/2 ,insert'2/4,insertionsort/1,insertionsort'1/1,'cklt#/1,'compare#/2,'less#/2,append#/2,append'1#/2,flatten#/1 ,flatten'1#/1,flattensort#/1,insert#/2,insert'1#/2,insert'2#/4,insertionsort#/1,insertionsort'1#/1} / {'0/0 ,'EQ/0,'GT/0,'LT/0,'false/0,'neg/1,'pos/1,'s/1,'true/0,dd/2,leaf/0,nil/0,node/3,c_1/0,c_2/0,c_3/0,c_4/0 ,c_5/0,c_6/0,c_7/0,c_8/0,c_9/1,c_10/0,c_11/0,c_12/0,c_13/1,c_14/0,c_15/1,c_16/1,c_17/1,c_18/1,c_19/0,c_20/1 ,c_21/0,c_22/4,c_23/2,c_24/1,c_25/2,c_26/0,c_27/0,c_28/1,c_29/1,c_30/2,c_31/0} - Obligation: innermost runtime complexity wrt. defined symbols {'cklt#,'compare#,'less#,append#,append'1#,flatten# ,flatten'1#,flattensort#,insert#,insert'1#,insert'2#,insertionsort#,insertionsort'1#} and constructors {'0 ,'EQ,'GT,'LT,'false,'neg,'pos,'s,'true,dd,leaf,nil,node} + Applied Processor: RemoveHeads + Details: Consider the dependency graph 1:S:append#(l1,l2) -> c_17(append'1#(l1,l2)) -->_1 append'1#(dd(x,xs),l2) -> c_18(append#(xs,l2)):2 2:S:append'1#(dd(x,xs),l2) -> c_18(append#(xs,l2)) -->_1 append#(l1,l2) -> c_17(append'1#(l1,l2)):1 3:S:insert#(x,l) -> c_24(insert'1#(l,x)) -->_1 insert'1#(dd(y,ys),x) -> c_25(insert'2#('less(y,x),x,y,ys),'less#(y,x)):4 4:S:insert'1#(dd(y,ys),x) -> c_25(insert'2#('less(y,x),x,y,ys),'less#(y,x)) -->_1 insert'2#('true(),x,y,ys) -> c_28(insert#(x,ys)):5 5:S:insert'2#('true(),x,y,ys) -> c_28(insert#(x,ys)) -->_1 insert#(x,l) -> c_24(insert'1#(l,x)):3 6:W:flatten#(t) -> flatten'1#(t) -->_1 flatten'1#(node(l,t1,t2)) -> flatten#(t2):10 -->_1 flatten'1#(node(l,t1,t2)) -> flatten#(t1):9 -->_1 flatten'1#(node(l,t1,t2)) -> append#(flatten(t1),flatten(t2)):8 -->_1 flatten'1#(node(l,t1,t2)) -> append#(l,append(flatten(t1),flatten(t2))):7 7:W:flatten'1#(node(l,t1,t2)) -> append#(l,append(flatten(t1),flatten(t2))) -->_1 append#(l1,l2) -> c_17(append'1#(l1,l2)):1 8:W:flatten'1#(node(l,t1,t2)) -> append#(flatten(t1),flatten(t2)) -->_1 append#(l1,l2) -> c_17(append'1#(l1,l2)):1 9:W:flatten'1#(node(l,t1,t2)) -> flatten#(t1) -->_1 flatten#(t) -> flatten'1#(t):6 10:W:flatten'1#(node(l,t1,t2)) -> flatten#(t2) -->_1 flatten#(t) -> flatten'1#(t):6 11:W:flattensort#(t) -> flatten#(t) -->_1 flatten#(t) -> flatten'1#(t):6 12:W:flattensort#(t) -> insertionsort#(flatten(t)) -->_1 insertionsort#(l) -> insertionsort'1#(l):13 13:W:insertionsort#(l) -> insertionsort'1#(l) -->_1 insertionsort'1#(dd(x,xs)) -> insertionsort#(xs):15 -->_1 insertionsort'1#(dd(x,xs)) -> insert#(x,insertionsort(xs)):14 14:W:insertionsort'1#(dd(x,xs)) -> insert#(x,insertionsort(xs)) -->_1 insert#(x,l) -> c_24(insert'1#(l,x)):3 15:W:insertionsort'1#(dd(x,xs)) -> insertionsort#(xs) -->_1 insertionsort#(l) -> insertionsort'1#(l):13 Following roots of the dependency graph are removed, as the considered set of starting terms is closed under reduction with respect to these rules (modulo compound contexts). [(11,flattensort#(t) -> flatten#(t))] *** Step 6.b:1.a:2: SimplifyRHS WORST_CASE(?,O(n^1)) + Considered Problem: - Strict DPs: append#(l1,l2) -> c_17(append'1#(l1,l2)) append'1#(dd(x,xs),l2) -> c_18(append#(xs,l2)) insert#(x,l) -> c_24(insert'1#(l,x)) insert'1#(dd(y,ys),x) -> c_25(insert'2#('less(y,x),x,y,ys),'less#(y,x)) insert'2#('true(),x,y,ys) -> c_28(insert#(x,ys)) - Weak DPs: flatten#(t) -> flatten'1#(t) flatten'1#(node(l,t1,t2)) -> append#(l,append(flatten(t1),flatten(t2))) flatten'1#(node(l,t1,t2)) -> append#(flatten(t1),flatten(t2)) flatten'1#(node(l,t1,t2)) -> flatten#(t1) flatten'1#(node(l,t1,t2)) -> flatten#(t2) flattensort#(t) -> insertionsort#(flatten(t)) insertionsort#(l) -> insertionsort'1#(l) insertionsort'1#(dd(x,xs)) -> insert#(x,insertionsort(xs)) insertionsort'1#(dd(x,xs)) -> insertionsort#(xs) - 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) 'less(x,y) -> 'cklt('compare(x,y)) append(l1,l2) -> append'1(l1,l2) append'1(dd(x,xs),l2) -> dd(x,append(xs,l2)) append'1(nil(),l2) -> l2 flatten(t) -> flatten'1(t) flatten'1(leaf()) -> nil() flatten'1(node(l,t1,t2)) -> append(l,append(flatten(t1),flatten(t2))) insert(x,l) -> insert'1(l,x) insert'1(dd(y,ys),x) -> insert'2('less(y,x),x,y,ys) insert'1(nil(),x) -> dd(x,nil()) insert'2('false(),x,y,ys) -> dd(x,dd(y,ys)) insert'2('true(),x,y,ys) -> dd(y,insert(x,ys)) insertionsort(l) -> insertionsort'1(l) insertionsort'1(dd(x,xs)) -> insert(x,insertionsort(xs)) insertionsort'1(nil()) -> nil() - Signature: {'cklt/1,'compare/2,'less/2,append/2,append'1/2,flatten/1,flatten'1/1,flattensort/1,insert/2,insert'1/2 ,insert'2/4,insertionsort/1,insertionsort'1/1,'cklt#/1,'compare#/2,'less#/2,append#/2,append'1#/2,flatten#/1 ,flatten'1#/1,flattensort#/1,insert#/2,insert'1#/2,insert'2#/4,insertionsort#/1,insertionsort'1#/1} / {'0/0 ,'EQ/0,'GT/0,'LT/0,'false/0,'neg/1,'pos/1,'s/1,'true/0,dd/2,leaf/0,nil/0,node/3,c_1/0,c_2/0,c_3/0,c_4/0 ,c_5/0,c_6/0,c_7/0,c_8/0,c_9/1,c_10/0,c_11/0,c_12/0,c_13/1,c_14/0,c_15/1,c_16/1,c_17/1,c_18/1,c_19/0,c_20/1 ,c_21/0,c_22/4,c_23/2,c_24/1,c_25/2,c_26/0,c_27/0,c_28/1,c_29/1,c_30/2,c_31/0} - Obligation: innermost runtime complexity wrt. defined symbols {'cklt#,'compare#,'less#,append#,append'1#,flatten# ,flatten'1#,flattensort#,insert#,insert'1#,insert'2#,insertionsort#,insertionsort'1#} and constructors {'0 ,'EQ,'GT,'LT,'false,'neg,'pos,'s,'true,dd,leaf,nil,node} + Applied Processor: SimplifyRHS + Details: Consider the dependency graph 1:S:append#(l1,l2) -> c_17(append'1#(l1,l2)) -->_1 append'1#(dd(x,xs),l2) -> c_18(append#(xs,l2)):2 2:S:append'1#(dd(x,xs),l2) -> c_18(append#(xs,l2)) -->_1 append#(l1,l2) -> c_17(append'1#(l1,l2)):1 3:S:insert#(x,l) -> c_24(insert'1#(l,x)) -->_1 insert'1#(dd(y,ys),x) -> c_25(insert'2#('less(y,x),x,y,ys),'less#(y,x)):4 4:S:insert'1#(dd(y,ys),x) -> c_25(insert'2#('less(y,x),x,y,ys),'less#(y,x)) -->_1 insert'2#('true(),x,y,ys) -> c_28(insert#(x,ys)):5 5:S:insert'2#('true(),x,y,ys) -> c_28(insert#(x,ys)) -->_1 insert#(x,l) -> c_24(insert'1#(l,x)):3 6:W:flatten#(t) -> flatten'1#(t) -->_1 flatten'1#(node(l,t1,t2)) -> flatten#(t2):10 -->_1 flatten'1#(node(l,t1,t2)) -> flatten#(t1):9 -->_1 flatten'1#(node(l,t1,t2)) -> append#(flatten(t1),flatten(t2)):8 -->_1 flatten'1#(node(l,t1,t2)) -> append#(l,append(flatten(t1),flatten(t2))):7 7:W:flatten'1#(node(l,t1,t2)) -> append#(l,append(flatten(t1),flatten(t2))) -->_1 append#(l1,l2) -> c_17(append'1#(l1,l2)):1 8:W:flatten'1#(node(l,t1,t2)) -> append#(flatten(t1),flatten(t2)) -->_1 append#(l1,l2) -> c_17(append'1#(l1,l2)):1 9:W:flatten'1#(node(l,t1,t2)) -> flatten#(t1) -->_1 flatten#(t) -> flatten'1#(t):6 10:W:flatten'1#(node(l,t1,t2)) -> flatten#(t2) -->_1 flatten#(t) -> flatten'1#(t):6 12:W:flattensort#(t) -> insertionsort#(flatten(t)) -->_1 insertionsort#(l) -> insertionsort'1#(l):13 13:W:insertionsort#(l) -> insertionsort'1#(l) -->_1 insertionsort'1#(dd(x,xs)) -> insertionsort#(xs):15 -->_1 insertionsort'1#(dd(x,xs)) -> insert#(x,insertionsort(xs)):14 14:W:insertionsort'1#(dd(x,xs)) -> insert#(x,insertionsort(xs)) -->_1 insert#(x,l) -> c_24(insert'1#(l,x)):3 15:W:insertionsort'1#(dd(x,xs)) -> insertionsort#(xs) -->_1 insertionsort#(l) -> insertionsort'1#(l):13 Due to missing edges in the depndency graph, the right-hand sides of following rules could be simplified: insert'1#(dd(y,ys),x) -> c_25(insert'2#('less(y,x),x,y,ys)) *** Step 6.b:1.a:3: WeightGap WORST_CASE(?,O(n^1)) + Considered Problem: - Strict DPs: append#(l1,l2) -> c_17(append'1#(l1,l2)) append'1#(dd(x,xs),l2) -> c_18(append#(xs,l2)) insert#(x,l) -> c_24(insert'1#(l,x)) insert'1#(dd(y,ys),x) -> c_25(insert'2#('less(y,x),x,y,ys)) insert'2#('true(),x,y,ys) -> c_28(insert#(x,ys)) - Weak DPs: flatten#(t) -> flatten'1#(t) flatten'1#(node(l,t1,t2)) -> append#(l,append(flatten(t1),flatten(t2))) flatten'1#(node(l,t1,t2)) -> append#(flatten(t1),flatten(t2)) flatten'1#(node(l,t1,t2)) -> flatten#(t1) flatten'1#(node(l,t1,t2)) -> flatten#(t2) flattensort#(t) -> insertionsort#(flatten(t)) insertionsort#(l) -> insertionsort'1#(l) insertionsort'1#(dd(x,xs)) -> insert#(x,insertionsort(xs)) insertionsort'1#(dd(x,xs)) -> insertionsort#(xs) - 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) 'less(x,y) -> 'cklt('compare(x,y)) append(l1,l2) -> append'1(l1,l2) append'1(dd(x,xs),l2) -> dd(x,append(xs,l2)) append'1(nil(),l2) -> l2 flatten(t) -> flatten'1(t) flatten'1(leaf()) -> nil() flatten'1(node(l,t1,t2)) -> append(l,append(flatten(t1),flatten(t2))) insert(x,l) -> insert'1(l,x) insert'1(dd(y,ys),x) -> insert'2('less(y,x),x,y,ys) insert'1(nil(),x) -> dd(x,nil()) insert'2('false(),x,y,ys) -> dd(x,dd(y,ys)) insert'2('true(),x,y,ys) -> dd(y,insert(x,ys)) insertionsort(l) -> insertionsort'1(l) insertionsort'1(dd(x,xs)) -> insert(x,insertionsort(xs)) insertionsort'1(nil()) -> nil() - Signature: {'cklt/1,'compare/2,'less/2,append/2,append'1/2,flatten/1,flatten'1/1,flattensort/1,insert/2,insert'1/2 ,insert'2/4,insertionsort/1,insertionsort'1/1,'cklt#/1,'compare#/2,'less#/2,append#/2,append'1#/2,flatten#/1 ,flatten'1#/1,flattensort#/1,insert#/2,insert'1#/2,insert'2#/4,insertionsort#/1,insertionsort'1#/1} / {'0/0 ,'EQ/0,'GT/0,'LT/0,'false/0,'neg/1,'pos/1,'s/1,'true/0,dd/2,leaf/0,nil/0,node/3,c_1/0,c_2/0,c_3/0,c_4/0 ,c_5/0,c_6/0,c_7/0,c_8/0,c_9/1,c_10/0,c_11/0,c_12/0,c_13/1,c_14/0,c_15/1,c_16/1,c_17/1,c_18/1,c_19/0,c_20/1 ,c_21/0,c_22/4,c_23/2,c_24/1,c_25/1,c_26/0,c_27/0,c_28/1,c_29/1,c_30/2,c_31/0} - Obligation: innermost runtime complexity wrt. defined symbols {'cklt#,'compare#,'less#,append#,append'1#,flatten# ,flatten'1#,flattensort#,insert#,insert'1#,insert'2#,insertionsort#,insertionsort'1#} and constructors {'0 ,'EQ,'GT,'LT,'false,'neg,'pos,'s,'true,dd,leaf,nil,node} + 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(append) = {1,2}, uargs(dd) = {2}, uargs(insert) = {2}, uargs(insert'2) = {1}, uargs(append#) = {1,2}, uargs(insert#) = {2}, uargs(insert'2#) = {1}, uargs(insertionsort#) = {1}, uargs(c_17) = {1}, uargs(c_18) = {1}, uargs(c_24) = {1}, uargs(c_25) = {1}, uargs(c_28) = {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('cklt) = [1] x1 + [0] p('compare) = [0] p('false) = [0] p('less) = [0] p('neg) = [0] p('pos) = [1] x1 + [0] p('s) = [1] x1 + [0] p('true) = [0] p(append) = [1] x1 + [1] x2 + [0] p(append'1) = [1] x1 + [1] x2 + [0] p(dd) = [1] x2 + [0] p(flatten) = [1] x1 + [2] p(flatten'1) = [1] x1 + [0] p(flattensort) = [0] p(insert) = [1] x2 + [0] p(insert'1) = [1] x1 + [0] p(insert'2) = [1] x1 + [1] x4 + [0] p(insertionsort) = [0] p(insertionsort'1) = [0] p(leaf) = [1] p(nil) = [0] p(node) = [1] x1 + [1] x2 + [1] x3 + [4] p('cklt#) = [0] p('compare#) = [1] x2 + [0] p('less#) = [1] x1 + [2] x2 + [0] p(append#) = [1] x1 + [1] x2 + [0] p(append'1#) = [1] x1 + [1] x2 + [1] p(flatten#) = [2] x1 + [5] p(flatten'1#) = [2] x1 + [4] p(flattensort#) = [4] x1 + [6] p(insert#) = [1] x2 + [3] p(insert'1#) = [1] x1 + [0] p(insert'2#) = [1] x1 + [1] x4 + [2] p(insertionsort#) = [1] x1 + [4] p(insertionsort'1#) = [1] x1 + [4] p(c_1) = [0] p(c_2) = [1] p(c_3) = [0] p(c_4) = [1] p(c_5) = [0] p(c_6) = [0] p(c_7) = [0] p(c_8) = [1] p(c_9) = [1] x1 + [0] p(c_10) = [4] p(c_11) = [1] p(c_12) = [0] p(c_13) = [1] p(c_14) = [1] p(c_15) = [0] p(c_16) = [0] p(c_17) = [1] x1 + [3] p(c_18) = [1] x1 + [0] p(c_19) = [0] p(c_20) = [2] x1 + [1] p(c_21) = [1] p(c_22) = [2] x1 + [1] x2 + [1] x3 + [4] p(c_23) = [1] x1 + [0] p(c_24) = [1] x1 + [1] p(c_25) = [1] x1 + [2] p(c_26) = [1] p(c_27) = [1] p(c_28) = [1] x1 + [2] p(c_29) = [2] p(c_30) = [1] x1 + [1] x2 + [2] p(c_31) = [1] Following rules are strictly oriented: append'1#(dd(x,xs),l2) = [1] l2 + [1] xs + [1] > [1] l2 + [1] xs + [0] = c_18(append#(xs,l2)) insert#(x,l) = [1] l + [3] > [1] l + [1] = c_24(insert'1#(l,x)) Following rules are (at-least) weakly oriented: append#(l1,l2) = [1] l1 + [1] l2 + [0] >= [1] l1 + [1] l2 + [4] = c_17(append'1#(l1,l2)) flatten#(t) = [2] t + [5] >= [2] t + [4] = flatten'1#(t) flatten'1#(node(l,t1,t2)) = [2] l + [2] t1 + [2] t2 + [12] >= [1] l + [1] t1 + [1] t2 + [4] = append#(l,append(flatten(t1),flatten(t2))) flatten'1#(node(l,t1,t2)) = [2] l + [2] t1 + [2] t2 + [12] >= [1] t1 + [1] t2 + [4] = append#(flatten(t1),flatten(t2)) flatten'1#(node(l,t1,t2)) = [2] l + [2] t1 + [2] t2 + [12] >= [2] t1 + [5] = flatten#(t1) flatten'1#(node(l,t1,t2)) = [2] l + [2] t1 + [2] t2 + [12] >= [2] t2 + [5] = flatten#(t2) flattensort#(t) = [4] t + [6] >= [1] t + [6] = insertionsort#(flatten(t)) insert'1#(dd(y,ys),x) = [1] ys + [0] >= [1] ys + [4] = c_25(insert'2#('less(y,x),x,y,ys)) insert'2#('true(),x,y,ys) = [1] ys + [2] >= [1] ys + [5] = c_28(insert#(x,ys)) insertionsort#(l) = [1] l + [4] >= [1] l + [4] = insertionsort'1#(l) insertionsort'1#(dd(x,xs)) = [1] xs + [4] >= [3] = insert#(x,insertionsort(xs)) insertionsort'1#(dd(x,xs)) = [1] xs + [4] >= [1] xs + [4] = insertionsort#(xs) '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)) append(l1,l2) = [1] l1 + [1] l2 + [0] >= [1] l1 + [1] l2 + [0] = append'1(l1,l2) append'1(dd(x,xs),l2) = [1] l2 + [1] xs + [0] >= [1] l2 + [1] xs + [0] = dd(x,append(xs,l2)) append'1(nil(),l2) = [1] l2 + [0] >= [1] l2 + [0] = l2 flatten(t) = [1] t + [2] >= [1] t + [0] = flatten'1(t) flatten'1(leaf()) = [1] >= [0] = nil() flatten'1(node(l,t1,t2)) = [1] l + [1] t1 + [1] t2 + [4] >= [1] l + [1] t1 + [1] t2 + [4] = append(l,append(flatten(t1),flatten(t2))) insert(x,l) = [1] l + [0] >= [1] l + [0] = insert'1(l,x) insert'1(dd(y,ys),x) = [1] ys + [0] >= [1] ys + [0] = insert'2('less(y,x),x,y,ys) insert'1(nil(),x) = [0] >= [0] = dd(x,nil()) insert'2('false(),x,y,ys) = [1] ys + [0] >= [1] ys + [0] = dd(x,dd(y,ys)) insert'2('true(),x,y,ys) = [1] ys + [0] >= [1] ys + [0] = dd(y,insert(x,ys)) insertionsort(l) = [0] >= [0] = insertionsort'1(l) insertionsort'1(dd(x,xs)) = [0] >= [0] = insert(x,insertionsort(xs)) insertionsort'1(nil()) = [0] >= [0] = nil() Further, it can be verified that all rules not oriented are covered by the weightgap condition. *** Step 6.b:1.a:4: WeightGap WORST_CASE(?,O(n^1)) + Considered Problem: - Strict DPs: append#(l1,l2) -> c_17(append'1#(l1,l2)) insert'1#(dd(y,ys),x) -> c_25(insert'2#('less(y,x),x,y,ys)) insert'2#('true(),x,y,ys) -> c_28(insert#(x,ys)) - Weak DPs: append'1#(dd(x,xs),l2) -> c_18(append#(xs,l2)) flatten#(t) -> flatten'1#(t) flatten'1#(node(l,t1,t2)) -> append#(l,append(flatten(t1),flatten(t2))) flatten'1#(node(l,t1,t2)) -> append#(flatten(t1),flatten(t2)) flatten'1#(node(l,t1,t2)) -> flatten#(t1) flatten'1#(node(l,t1,t2)) -> flatten#(t2) flattensort#(t) -> insertionsort#(flatten(t)) insert#(x,l) -> c_24(insert'1#(l,x)) insertionsort#(l) -> insertionsort'1#(l) insertionsort'1#(dd(x,xs)) -> insert#(x,insertionsort(xs)) insertionsort'1#(dd(x,xs)) -> insertionsort#(xs) - 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) 'less(x,y) -> 'cklt('compare(x,y)) append(l1,l2) -> append'1(l1,l2) append'1(dd(x,xs),l2) -> dd(x,append(xs,l2)) append'1(nil(),l2) -> l2 flatten(t) -> flatten'1(t) flatten'1(leaf()) -> nil() flatten'1(node(l,t1,t2)) -> append(l,append(flatten(t1),flatten(t2))) insert(x,l) -> insert'1(l,x) insert'1(dd(y,ys),x) -> insert'2('less(y,x),x,y,ys) insert'1(nil(),x) -> dd(x,nil()) insert'2('false(),x,y,ys) -> dd(x,dd(y,ys)) insert'2('true(),x,y,ys) -> dd(y,insert(x,ys)) insertionsort(l) -> insertionsort'1(l) insertionsort'1(dd(x,xs)) -> insert(x,insertionsort(xs)) insertionsort'1(nil()) -> nil() - Signature: {'cklt/1,'compare/2,'less/2,append/2,append'1/2,flatten/1,flatten'1/1,flattensort/1,insert/2,insert'1/2 ,insert'2/4,insertionsort/1,insertionsort'1/1,'cklt#/1,'compare#/2,'less#/2,append#/2,append'1#/2,flatten#/1 ,flatten'1#/1,flattensort#/1,insert#/2,insert'1#/2,insert'2#/4,insertionsort#/1,insertionsort'1#/1} / {'0/0 ,'EQ/0,'GT/0,'LT/0,'false/0,'neg/1,'pos/1,'s/1,'true/0,dd/2,leaf/0,nil/0,node/3,c_1/0,c_2/0,c_3/0,c_4/0 ,c_5/0,c_6/0,c_7/0,c_8/0,c_9/1,c_10/0,c_11/0,c_12/0,c_13/1,c_14/0,c_15/1,c_16/1,c_17/1,c_18/1,c_19/0,c_20/1 ,c_21/0,c_22/4,c_23/2,c_24/1,c_25/1,c_26/0,c_27/0,c_28/1,c_29/1,c_30/2,c_31/0} - Obligation: innermost runtime complexity wrt. defined symbols {'cklt#,'compare#,'less#,append#,append'1#,flatten# ,flatten'1#,flattensort#,insert#,insert'1#,insert'2#,insertionsort#,insertionsort'1#} and constructors {'0 ,'EQ,'GT,'LT,'false,'neg,'pos,'s,'true,dd,leaf,nil,node} + 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(append) = {1,2}, uargs(dd) = {2}, uargs(insert) = {2}, uargs(insert'2) = {1}, uargs(append#) = {1,2}, uargs(insert#) = {2}, uargs(insert'2#) = {1}, uargs(insertionsort#) = {1}, uargs(c_17) = {1}, uargs(c_18) = {1}, uargs(c_24) = {1}, uargs(c_25) = {1}, uargs(c_28) = {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('cklt) = [1] x1 + [0] p('compare) = [0] p('false) = [0] p('less) = [0] p('neg) = [1] x1 + [0] p('pos) = [1] x1 + [0] p('s) = [1] x1 + [0] p('true) = [0] p(append) = [1] x1 + [1] x2 + [4] p(append'1) = [1] x1 + [1] x2 + [4] p(dd) = [1] x2 + [0] p(flatten) = [2] x1 + [0] p(flatten'1) = [2] x1 + [0] p(flattensort) = [1] x1 + [2] p(insert) = [1] x2 + [0] p(insert'1) = [1] x1 + [0] p(insert'2) = [1] x1 + [1] x4 + [0] p(insertionsort) = [0] p(insertionsort'1) = [0] p(leaf) = [4] p(nil) = [0] p(node) = [1] x1 + [1] x2 + [1] x3 + [4] p('cklt#) = [1] x1 + [0] p('compare#) = [1] p('less#) = [1] x2 + [2] p(append#) = [1] x1 + [1] x2 + [0] p(append'1#) = [1] x1 + [1] x2 + [6] p(flatten#) = [2] x1 + [0] p(flatten'1#) = [2] x1 + [0] p(flattensort#) = [4] x1 + [4] p(insert#) = [1] x2 + [1] p(insert'1#) = [1] x1 + [0] p(insert'2#) = [1] x1 + [1] x4 + [3] p(insertionsort#) = [1] x1 + [1] p(insertionsort'1#) = [1] x1 + [1] p(c_1) = [1] p(c_2) = [0] p(c_3) = [0] p(c_4) = [0] p(c_5) = [1] p(c_6) = [1] p(c_7) = [1] p(c_8) = [2] p(c_9) = [2] p(c_10) = [4] p(c_11) = [0] p(c_12) = [2] p(c_13) = [2] x1 + [0] p(c_14) = [1] p(c_15) = [2] x1 + [1] p(c_16) = [4] x1 + [1] p(c_17) = [1] x1 + [1] p(c_18) = [1] x1 + [5] p(c_19) = [2] p(c_20) = [2] x1 + [0] p(c_21) = [1] p(c_22) = [4] x1 + [1] x3 + [1] x4 + [1] p(c_23) = [4] x1 + [0] p(c_24) = [1] x1 + [0] p(c_25) = [1] x1 + [0] p(c_26) = [1] p(c_27) = [4] p(c_28) = [1] x1 + [1] p(c_29) = [1] p(c_30) = [2] x2 + [0] p(c_31) = [0] Following rules are strictly oriented: insert'2#('true(),x,y,ys) = [1] ys + [3] > [1] ys + [2] = c_28(insert#(x,ys)) Following rules are (at-least) weakly oriented: append#(l1,l2) = [1] l1 + [1] l2 + [0] >= [1] l1 + [1] l2 + [7] = c_17(append'1#(l1,l2)) append'1#(dd(x,xs),l2) = [1] l2 + [1] xs + [6] >= [1] l2 + [1] xs + [5] = c_18(append#(xs,l2)) flatten#(t) = [2] t + [0] >= [2] t + [0] = flatten'1#(t) flatten'1#(node(l,t1,t2)) = [2] l + [2] t1 + [2] t2 + [8] >= [1] l + [2] t1 + [2] t2 + [4] = append#(l,append(flatten(t1),flatten(t2))) flatten'1#(node(l,t1,t2)) = [2] l + [2] t1 + [2] t2 + [8] >= [2] t1 + [2] t2 + [0] = append#(flatten(t1),flatten(t2)) flatten'1#(node(l,t1,t2)) = [2] l + [2] t1 + [2] t2 + [8] >= [2] t1 + [0] = flatten#(t1) flatten'1#(node(l,t1,t2)) = [2] l + [2] t1 + [2] t2 + [8] >= [2] t2 + [0] = flatten#(t2) flattensort#(t) = [4] t + [4] >= [2] t + [1] = insertionsort#(flatten(t)) insert#(x,l) = [1] l + [1] >= [1] l + [0] = c_24(insert'1#(l,x)) insert'1#(dd(y,ys),x) = [1] ys + [0] >= [1] ys + [3] = c_25(insert'2#('less(y,x),x,y,ys)) insertionsort#(l) = [1] l + [1] >= [1] l + [1] = insertionsort'1#(l) insertionsort'1#(dd(x,xs)) = [1] xs + [1] >= [1] = insert#(x,insertionsort(xs)) insertionsort'1#(dd(x,xs)) = [1] xs + [1] >= [1] xs + [1] = insertionsort#(xs) '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)) append(l1,l2) = [1] l1 + [1] l2 + [4] >= [1] l1 + [1] l2 + [4] = append'1(l1,l2) append'1(dd(x,xs),l2) = [1] l2 + [1] xs + [4] >= [1] l2 + [1] xs + [4] = dd(x,append(xs,l2)) append'1(nil(),l2) = [1] l2 + [4] >= [1] l2 + [0] = l2 flatten(t) = [2] t + [0] >= [2] t + [0] = flatten'1(t) flatten'1(leaf()) = [8] >= [0] = nil() flatten'1(node(l,t1,t2)) = [2] l + [2] t1 + [2] t2 + [8] >= [1] l + [2] t1 + [2] t2 + [8] = append(l,append(flatten(t1),flatten(t2))) insert(x,l) = [1] l + [0] >= [1] l + [0] = insert'1(l,x) insert'1(dd(y,ys),x) = [1] ys + [0] >= [1] ys + [0] = insert'2('less(y,x),x,y,ys) insert'1(nil(),x) = [0] >= [0] = dd(x,nil()) insert'2('false(),x,y,ys) = [1] ys + [0] >= [1] ys + [0] = dd(x,dd(y,ys)) insert'2('true(),x,y,ys) = [1] ys + [0] >= [1] ys + [0] = dd(y,insert(x,ys)) insertionsort(l) = [0] >= [0] = insertionsort'1(l) insertionsort'1(dd(x,xs)) = [0] >= [0] = insert(x,insertionsort(xs)) insertionsort'1(nil()) = [0] >= [0] = nil() Further, it can be verified that all rules not oriented are covered by the weightgap condition. *** Step 6.b:1.a:5: WeightGap WORST_CASE(?,O(n^1)) + Considered Problem: - Strict DPs: append#(l1,l2) -> c_17(append'1#(l1,l2)) insert'1#(dd(y,ys),x) -> c_25(insert'2#('less(y,x),x,y,ys)) - Weak DPs: append'1#(dd(x,xs),l2) -> c_18(append#(xs,l2)) flatten#(t) -> flatten'1#(t) flatten'1#(node(l,t1,t2)) -> append#(l,append(flatten(t1),flatten(t2))) flatten'1#(node(l,t1,t2)) -> append#(flatten(t1),flatten(t2)) flatten'1#(node(l,t1,t2)) -> flatten#(t1) flatten'1#(node(l,t1,t2)) -> flatten#(t2) flattensort#(t) -> insertionsort#(flatten(t)) insert#(x,l) -> c_24(insert'1#(l,x)) insert'2#('true(),x,y,ys) -> c_28(insert#(x,ys)) insertionsort#(l) -> insertionsort'1#(l) insertionsort'1#(dd(x,xs)) -> insert#(x,insertionsort(xs)) insertionsort'1#(dd(x,xs)) -> insertionsort#(xs) - 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) 'less(x,y) -> 'cklt('compare(x,y)) append(l1,l2) -> append'1(l1,l2) append'1(dd(x,xs),l2) -> dd(x,append(xs,l2)) append'1(nil(),l2) -> l2 flatten(t) -> flatten'1(t) flatten'1(leaf()) -> nil() flatten'1(node(l,t1,t2)) -> append(l,append(flatten(t1),flatten(t2))) insert(x,l) -> insert'1(l,x) insert'1(dd(y,ys),x) -> insert'2('less(y,x),x,y,ys) insert'1(nil(),x) -> dd(x,nil()) insert'2('false(),x,y,ys) -> dd(x,dd(y,ys)) insert'2('true(),x,y,ys) -> dd(y,insert(x,ys)) insertionsort(l) -> insertionsort'1(l) insertionsort'1(dd(x,xs)) -> insert(x,insertionsort(xs)) insertionsort'1(nil()) -> nil() - Signature: {'cklt/1,'compare/2,'less/2,append/2,append'1/2,flatten/1,flatten'1/1,flattensort/1,insert/2,insert'1/2 ,insert'2/4,insertionsort/1,insertionsort'1/1,'cklt#/1,'compare#/2,'less#/2,append#/2,append'1#/2,flatten#/1 ,flatten'1#/1,flattensort#/1,insert#/2,insert'1#/2,insert'2#/4,insertionsort#/1,insertionsort'1#/1} / {'0/0 ,'EQ/0,'GT/0,'LT/0,'false/0,'neg/1,'pos/1,'s/1,'true/0,dd/2,leaf/0,nil/0,node/3,c_1/0,c_2/0,c_3/0,c_4/0 ,c_5/0,c_6/0,c_7/0,c_8/0,c_9/1,c_10/0,c_11/0,c_12/0,c_13/1,c_14/0,c_15/1,c_16/1,c_17/1,c_18/1,c_19/0,c_20/1 ,c_21/0,c_22/4,c_23/2,c_24/1,c_25/1,c_26/0,c_27/0,c_28/1,c_29/1,c_30/2,c_31/0} - Obligation: innermost runtime complexity wrt. defined symbols {'cklt#,'compare#,'less#,append#,append'1#,flatten# ,flatten'1#,flattensort#,insert#,insert'1#,insert'2#,insertionsort#,insertionsort'1#} and constructors {'0 ,'EQ,'GT,'LT,'false,'neg,'pos,'s,'true,dd,leaf,nil,node} + 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(append) = {1,2}, uargs(dd) = {2}, uargs(insert) = {2}, uargs(insert'2) = {1}, uargs(append#) = {1,2}, uargs(insert#) = {2}, uargs(insert'2#) = {1}, uargs(insertionsort#) = {1}, uargs(c_17) = {1}, uargs(c_18) = {1}, uargs(c_24) = {1}, uargs(c_25) = {1}, uargs(c_28) = {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('cklt) = [1] x1 + [2] p('compare) = [0] p('false) = [2] p('less) = [2] p('neg) = [1] x1 + [2] p('pos) = [0] p('s) = [1] x1 + [4] p('true) = [2] p(append) = [1] x1 + [1] x2 + [0] p(append'1) = [1] x1 + [1] x2 + [0] p(dd) = [1] x2 + [4] p(flatten) = [2] x1 + [2] p(flatten'1) = [2] x1 + [0] p(flattensort) = [1] p(insert) = [1] x2 + [4] p(insert'1) = [1] x1 + [4] p(insert'2) = [1] x1 + [1] x4 + [6] p(insertionsort) = [1] x1 + [1] p(insertionsort'1) = [1] x1 + [1] p(leaf) = [4] p(nil) = [4] p(node) = [1] x1 + [1] x2 + [1] x3 + [6] p('cklt#) = [4] p('compare#) = [1] x1 + [4] p('less#) = [4] x2 + [4] p(append#) = [1] x1 + [1] x2 + [4] p(append'1#) = [1] x1 + [1] x2 + [0] p(flatten#) = [2] x1 + [2] p(flatten'1#) = [2] x1 + [2] p(flattensort#) = [2] x1 + [7] p(insert#) = [1] x2 + [0] p(insert'1#) = [1] x1 + [0] p(insert'2#) = [1] x1 + [1] x4 + [1] p(insertionsort#) = [1] x1 + [4] p(insertionsort'1#) = [1] x1 + [1] p(c_1) = [0] p(c_2) = [1] p(c_3) = [1] p(c_4) = [2] p(c_5) = [0] p(c_6) = [1] p(c_7) = [4] p(c_8) = [1] p(c_9) = [2] p(c_10) = [1] p(c_11) = [1] p(c_12) = [0] p(c_13) = [0] p(c_14) = [0] p(c_15) = [2] p(c_16) = [0] p(c_17) = [1] x1 + [3] p(c_18) = [1] x1 + [0] p(c_19) = [2] p(c_20) = [4] p(c_21) = [0] p(c_22) = [1] x1 + [1] x4 + [1] p(c_23) = [1] x1 + [2] p(c_24) = [1] x1 + [0] p(c_25) = [1] x1 + [3] p(c_26) = [0] p(c_27) = [0] p(c_28) = [1] x1 + [3] p(c_29) = [1] x1 + [4] p(c_30) = [0] p(c_31) = [0] Following rules are strictly oriented: append#(l1,l2) = [1] l1 + [1] l2 + [4] > [1] l1 + [1] l2 + [3] = c_17(append'1#(l1,l2)) Following rules are (at-least) weakly oriented: append'1#(dd(x,xs),l2) = [1] l2 + [1] xs + [4] >= [1] l2 + [1] xs + [4] = c_18(append#(xs,l2)) flatten#(t) = [2] t + [2] >= [2] t + [2] = flatten'1#(t) flatten'1#(node(l,t1,t2)) = [2] l + [2] t1 + [2] t2 + [14] >= [1] l + [2] t1 + [2] t2 + [8] = append#(l,append(flatten(t1),flatten(t2))) flatten'1#(node(l,t1,t2)) = [2] l + [2] t1 + [2] t2 + [14] >= [2] t1 + [2] t2 + [8] = append#(flatten(t1),flatten(t2)) flatten'1#(node(l,t1,t2)) = [2] l + [2] t1 + [2] t2 + [14] >= [2] t1 + [2] = flatten#(t1) flatten'1#(node(l,t1,t2)) = [2] l + [2] t1 + [2] t2 + [14] >= [2] t2 + [2] = flatten#(t2) flattensort#(t) = [2] t + [7] >= [2] t + [6] = insertionsort#(flatten(t)) insert#(x,l) = [1] l + [0] >= [1] l + [0] = c_24(insert'1#(l,x)) insert'1#(dd(y,ys),x) = [1] ys + [4] >= [1] ys + [6] = c_25(insert'2#('less(y,x),x,y,ys)) insert'2#('true(),x,y,ys) = [1] ys + [3] >= [1] ys + [3] = c_28(insert#(x,ys)) insertionsort#(l) = [1] l + [4] >= [1] l + [1] = insertionsort'1#(l) insertionsort'1#(dd(x,xs)) = [1] xs + [5] >= [1] xs + [1] = insert#(x,insertionsort(xs)) insertionsort'1#(dd(x,xs)) = [1] xs + [5] >= [1] xs + [4] = insertionsort#(xs) 'cklt('EQ()) = [2] >= [2] = 'false() 'cklt('GT()) = [2] >= [2] = 'false() 'cklt('LT()) = [2] >= [2] = '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) = [2] >= [2] = 'cklt('compare(x,y)) append(l1,l2) = [1] l1 + [1] l2 + [0] >= [1] l1 + [1] l2 + [0] = append'1(l1,l2) append'1(dd(x,xs),l2) = [1] l2 + [1] xs + [4] >= [1] l2 + [1] xs + [4] = dd(x,append(xs,l2)) append'1(nil(),l2) = [1] l2 + [4] >= [1] l2 + [0] = l2 flatten(t) = [2] t + [2] >= [2] t + [0] = flatten'1(t) flatten'1(leaf()) = [8] >= [4] = nil() flatten'1(node(l,t1,t2)) = [2] l + [2] t1 + [2] t2 + [12] >= [1] l + [2] t1 + [2] t2 + [4] = append(l,append(flatten(t1),flatten(t2))) insert(x,l) = [1] l + [4] >= [1] l + [4] = insert'1(l,x) insert'1(dd(y,ys),x) = [1] ys + [8] >= [1] ys + [8] = insert'2('less(y,x),x,y,ys) insert'1(nil(),x) = [8] >= [8] = dd(x,nil()) insert'2('false(),x,y,ys) = [1] ys + [8] >= [1] ys + [8] = dd(x,dd(y,ys)) insert'2('true(),x,y,ys) = [1] ys + [8] >= [1] ys + [8] = dd(y,insert(x,ys)) insertionsort(l) = [1] l + [1] >= [1] l + [1] = insertionsort'1(l) insertionsort'1(dd(x,xs)) = [1] xs + [5] >= [1] xs + [5] = insert(x,insertionsort(xs)) insertionsort'1(nil()) = [5] >= [4] = nil() Further, it can be verified that all rules not oriented are covered by the weightgap condition. *** Step 6.b:1.a:6: WeightGap WORST_CASE(?,O(n^1)) + Considered Problem: - Strict DPs: insert'1#(dd(y,ys),x) -> c_25(insert'2#('less(y,x),x,y,ys)) - Weak DPs: append#(l1,l2) -> c_17(append'1#(l1,l2)) append'1#(dd(x,xs),l2) -> c_18(append#(xs,l2)) flatten#(t) -> flatten'1#(t) flatten'1#(node(l,t1,t2)) -> append#(l,append(flatten(t1),flatten(t2))) flatten'1#(node(l,t1,t2)) -> append#(flatten(t1),flatten(t2)) flatten'1#(node(l,t1,t2)) -> flatten#(t1) flatten'1#(node(l,t1,t2)) -> flatten#(t2) flattensort#(t) -> insertionsort#(flatten(t)) insert#(x,l) -> c_24(insert'1#(l,x)) insert'2#('true(),x,y,ys) -> c_28(insert#(x,ys)) insertionsort#(l) -> insertionsort'1#(l) insertionsort'1#(dd(x,xs)) -> insert#(x,insertionsort(xs)) insertionsort'1#(dd(x,xs)) -> insertionsort#(xs) - 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) 'less(x,y) -> 'cklt('compare(x,y)) append(l1,l2) -> append'1(l1,l2) append'1(dd(x,xs),l2) -> dd(x,append(xs,l2)) append'1(nil(),l2) -> l2 flatten(t) -> flatten'1(t) flatten'1(leaf()) -> nil() flatten'1(node(l,t1,t2)) -> append(l,append(flatten(t1),flatten(t2))) insert(x,l) -> insert'1(l,x) insert'1(dd(y,ys),x) -> insert'2('less(y,x),x,y,ys) insert'1(nil(),x) -> dd(x,nil()) insert'2('false(),x,y,ys) -> dd(x,dd(y,ys)) insert'2('true(),x,y,ys) -> dd(y,insert(x,ys)) insertionsort(l) -> insertionsort'1(l) insertionsort'1(dd(x,xs)) -> insert(x,insertionsort(xs)) insertionsort'1(nil()) -> nil() - Signature: {'cklt/1,'compare/2,'less/2,append/2,append'1/2,flatten/1,flatten'1/1,flattensort/1,insert/2,insert'1/2 ,insert'2/4,insertionsort/1,insertionsort'1/1,'cklt#/1,'compare#/2,'less#/2,append#/2,append'1#/2,flatten#/1 ,flatten'1#/1,flattensort#/1,insert#/2,insert'1#/2,insert'2#/4,insertionsort#/1,insertionsort'1#/1} / {'0/0 ,'EQ/0,'GT/0,'LT/0,'false/0,'neg/1,'pos/1,'s/1,'true/0,dd/2,leaf/0,nil/0,node/3,c_1/0,c_2/0,c_3/0,c_4/0 ,c_5/0,c_6/0,c_7/0,c_8/0,c_9/1,c_10/0,c_11/0,c_12/0,c_13/1,c_14/0,c_15/1,c_16/1,c_17/1,c_18/1,c_19/0,c_20/1 ,c_21/0,c_22/4,c_23/2,c_24/1,c_25/1,c_26/0,c_27/0,c_28/1,c_29/1,c_30/2,c_31/0} - Obligation: innermost runtime complexity wrt. defined symbols {'cklt#,'compare#,'less#,append#,append'1#,flatten# ,flatten'1#,flattensort#,insert#,insert'1#,insert'2#,insertionsort#,insertionsort'1#} and constructors {'0 ,'EQ,'GT,'LT,'false,'neg,'pos,'s,'true,dd,leaf,nil,node} + 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(append) = {1,2}, uargs(dd) = {2}, uargs(insert) = {2}, uargs(insert'2) = {1}, uargs(append#) = {1,2}, uargs(insert#) = {2}, uargs(insert'2#) = {1}, uargs(insertionsort#) = {1}, uargs(c_17) = {1}, uargs(c_18) = {1}, uargs(c_24) = {1}, uargs(c_25) = {1}, uargs(c_28) = {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('cklt) = [1] x1 + [0] p('compare) = [0] p('false) = [0] p('less) = [0] p('neg) = [1] x1 + [1] p('pos) = [1] x1 + [0] p('s) = [1] p('true) = [0] p(append) = [1] x1 + [1] x2 + [0] p(append'1) = [1] x1 + [1] x2 + [0] p(dd) = [1] x2 + [2] p(flatten) = [4] x1 + [0] p(flatten'1) = [4] x1 + [0] p(flattensort) = [4] x1 + [1] p(insert) = [1] x2 + [2] p(insert'1) = [1] x1 + [2] p(insert'2) = [1] x1 + [1] x4 + [4] p(insertionsort) = [1] x1 + [0] p(insertionsort'1) = [1] x1 + [0] p(leaf) = [2] p(nil) = [2] p(node) = [1] x1 + [1] x2 + [1] x3 + [2] p('cklt#) = [1] p('compare#) = [1] p('less#) = [2] x1 + [1] x2 + [0] p(append#) = [1] x1 + [1] x2 + [0] p(append'1#) = [1] x1 + [1] x2 + [0] p(flatten#) = [4] x1 + [0] p(flatten'1#) = [4] x1 + [0] p(flattensort#) = [5] x1 + [5] p(insert#) = [1] x2 + [2] p(insert'1#) = [1] x1 + [1] p(insert'2#) = [1] x1 + [1] x4 + [2] p(insertionsort#) = [1] x1 + [5] p(insertionsort'1#) = [1] x1 + [5] p(c_1) = [4] p(c_2) = [1] p(c_3) = [1] p(c_4) = [0] p(c_5) = [0] p(c_6) = [0] p(c_7) = [2] p(c_8) = [0] p(c_9) = [1] x1 + [4] p(c_10) = [0] p(c_11) = [1] p(c_12) = [1] p(c_13) = [0] p(c_14) = [1] p(c_15) = [2] x1 + [4] p(c_16) = [1] x1 + [1] p(c_17) = [1] x1 + [0] p(c_18) = [1] x1 + [2] p(c_19) = [0] p(c_20) = [4] x1 + [1] p(c_21) = [1] p(c_22) = [1] x1 + [1] x2 + [4] x3 + [4] p(c_23) = [1] x1 + [1] p(c_24) = [1] x1 + [1] p(c_25) = [1] x1 + [0] p(c_26) = [0] p(c_27) = [0] p(c_28) = [1] x1 + [0] p(c_29) = [1] x1 + [1] p(c_30) = [1] x1 + [2] x2 + [0] p(c_31) = [1] Following rules are strictly oriented: insert'1#(dd(y,ys),x) = [1] ys + [3] > [1] ys + [2] = c_25(insert'2#('less(y,x),x,y,ys)) Following rules are (at-least) weakly oriented: append#(l1,l2) = [1] l1 + [1] l2 + [0] >= [1] l1 + [1] l2 + [0] = c_17(append'1#(l1,l2)) append'1#(dd(x,xs),l2) = [1] l2 + [1] xs + [2] >= [1] l2 + [1] xs + [2] = c_18(append#(xs,l2)) flatten#(t) = [4] t + [0] >= [4] t + [0] = flatten'1#(t) flatten'1#(node(l,t1,t2)) = [4] l + [4] t1 + [4] t2 + [8] >= [1] l + [4] t1 + [4] t2 + [0] = append#(l,append(flatten(t1),flatten(t2))) flatten'1#(node(l,t1,t2)) = [4] l + [4] t1 + [4] t2 + [8] >= [4] t1 + [4] t2 + [0] = append#(flatten(t1),flatten(t2)) flatten'1#(node(l,t1,t2)) = [4] l + [4] t1 + [4] t2 + [8] >= [4] t1 + [0] = flatten#(t1) flatten'1#(node(l,t1,t2)) = [4] l + [4] t1 + [4] t2 + [8] >= [4] t2 + [0] = flatten#(t2) flattensort#(t) = [5] t + [5] >= [4] t + [5] = insertionsort#(flatten(t)) insert#(x,l) = [1] l + [2] >= [1] l + [2] = c_24(insert'1#(l,x)) insert'2#('true(),x,y,ys) = [1] ys + [2] >= [1] ys + [2] = c_28(insert#(x,ys)) insertionsort#(l) = [1] l + [5] >= [1] l + [5] = insertionsort'1#(l) insertionsort'1#(dd(x,xs)) = [1] xs + [7] >= [1] xs + [2] = insert#(x,insertionsort(xs)) insertionsort'1#(dd(x,xs)) = [1] xs + [7] >= [1] xs + [5] = insertionsort#(xs) '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)) append(l1,l2) = [1] l1 + [1] l2 + [0] >= [1] l1 + [1] l2 + [0] = append'1(l1,l2) append'1(dd(x,xs),l2) = [1] l2 + [1] xs + [2] >= [1] l2 + [1] xs + [2] = dd(x,append(xs,l2)) append'1(nil(),l2) = [1] l2 + [2] >= [1] l2 + [0] = l2 flatten(t) = [4] t + [0] >= [4] t + [0] = flatten'1(t) flatten'1(leaf()) = [8] >= [2] = nil() flatten'1(node(l,t1,t2)) = [4] l + [4] t1 + [4] t2 + [8] >= [1] l + [4] t1 + [4] t2 + [0] = append(l,append(flatten(t1),flatten(t2))) insert(x,l) = [1] l + [2] >= [1] l + [2] = insert'1(l,x) insert'1(dd(y,ys),x) = [1] ys + [4] >= [1] ys + [4] = insert'2('less(y,x),x,y,ys) insert'1(nil(),x) = [4] >= [4] = dd(x,nil()) insert'2('false(),x,y,ys) = [1] ys + [4] >= [1] ys + [4] = dd(x,dd(y,ys)) insert'2('true(),x,y,ys) = [1] ys + [4] >= [1] ys + [4] = dd(y,insert(x,ys)) insertionsort(l) = [1] l + [0] >= [1] l + [0] = insertionsort'1(l) insertionsort'1(dd(x,xs)) = [1] xs + [2] >= [1] xs + [2] = insert(x,insertionsort(xs)) insertionsort'1(nil()) = [2] >= [2] = nil() Further, it can be verified that all rules not oriented are covered by the weightgap condition. *** Step 6.b:1.a:7: EmptyProcessor WORST_CASE(?,O(1)) + Considered Problem: - Weak DPs: append#(l1,l2) -> c_17(append'1#(l1,l2)) append'1#(dd(x,xs),l2) -> c_18(append#(xs,l2)) flatten#(t) -> flatten'1#(t) flatten'1#(node(l,t1,t2)) -> append#(l,append(flatten(t1),flatten(t2))) flatten'1#(node(l,t1,t2)) -> append#(flatten(t1),flatten(t2)) flatten'1#(node(l,t1,t2)) -> flatten#(t1) flatten'1#(node(l,t1,t2)) -> flatten#(t2) flattensort#(t) -> insertionsort#(flatten(t)) insert#(x,l) -> c_24(insert'1#(l,x)) insert'1#(dd(y,ys),x) -> c_25(insert'2#('less(y,x),x,y,ys)) insert'2#('true(),x,y,ys) -> c_28(insert#(x,ys)) insertionsort#(l) -> insertionsort'1#(l) insertionsort'1#(dd(x,xs)) -> insert#(x,insertionsort(xs)) insertionsort'1#(dd(x,xs)) -> insertionsort#(xs) - 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) 'less(x,y) -> 'cklt('compare(x,y)) append(l1,l2) -> append'1(l1,l2) append'1(dd(x,xs),l2) -> dd(x,append(xs,l2)) append'1(nil(),l2) -> l2 flatten(t) -> flatten'1(t) flatten'1(leaf()) -> nil() flatten'1(node(l,t1,t2)) -> append(l,append(flatten(t1),flatten(t2))) insert(x,l) -> insert'1(l,x) insert'1(dd(y,ys),x) -> insert'2('less(y,x),x,y,ys) insert'1(nil(),x) -> dd(x,nil()) insert'2('false(),x,y,ys) -> dd(x,dd(y,ys)) insert'2('true(),x,y,ys) -> dd(y,insert(x,ys)) insertionsort(l) -> insertionsort'1(l) insertionsort'1(dd(x,xs)) -> insert(x,insertionsort(xs)) insertionsort'1(nil()) -> nil() - Signature: {'cklt/1,'compare/2,'less/2,append/2,append'1/2,flatten/1,flatten'1/1,flattensort/1,insert/2,insert'1/2 ,insert'2/4,insertionsort/1,insertionsort'1/1,'cklt#/1,'compare#/2,'less#/2,append#/2,append'1#/2,flatten#/1 ,flatten'1#/1,flattensort#/1,insert#/2,insert'1#/2,insert'2#/4,insertionsort#/1,insertionsort'1#/1} / {'0/0 ,'EQ/0,'GT/0,'LT/0,'false/0,'neg/1,'pos/1,'s/1,'true/0,dd/2,leaf/0,nil/0,node/3,c_1/0,c_2/0,c_3/0,c_4/0 ,c_5/0,c_6/0,c_7/0,c_8/0,c_9/1,c_10/0,c_11/0,c_12/0,c_13/1,c_14/0,c_15/1,c_16/1,c_17/1,c_18/1,c_19/0,c_20/1 ,c_21/0,c_22/4,c_23/2,c_24/1,c_25/1,c_26/0,c_27/0,c_28/1,c_29/1,c_30/2,c_31/0} - Obligation: innermost runtime complexity wrt. defined symbols {'cklt#,'compare#,'less#,append#,append'1#,flatten# ,flatten'1#,flattensort#,insert#,insert'1#,insert'2#,insertionsort#,insertionsort'1#} and constructors {'0 ,'EQ,'GT,'LT,'false,'neg,'pos,'s,'true,dd,leaf,nil,node} + Applied Processor: EmptyProcessor + Details: The problem is already closed. The intended complexity is O(1). *** Step 6.b:1.b:1: RemoveWeakSuffixes WORST_CASE(?,O(n^1)) + Considered Problem: - Strict DPs: 'compare#('neg(x),'neg(y)) -> c_9('compare#(y,x)) 'compare#('pos(x),'pos(y)) -> c_13('compare#(x,y)) 'compare#('s(x),'s(y)) -> c_15('compare#(x,y)) 'less#(x,y) -> c_16('compare#(x,y)) - Weak DPs: append#(l1,l2) -> append'1#(l1,l2) append'1#(dd(x,xs),l2) -> append#(xs,l2) flatten#(t) -> flatten'1#(t) flatten'1#(node(l,t1,t2)) -> append#(l,append(flatten(t1),flatten(t2))) flatten'1#(node(l,t1,t2)) -> append#(flatten(t1),flatten(t2)) flatten'1#(node(l,t1,t2)) -> flatten#(t1) flatten'1#(node(l,t1,t2)) -> flatten#(t2) flattensort#(t) -> flatten#(t) flattensort#(t) -> insertionsort#(flatten(t)) insert#(x,l) -> insert'1#(l,x) insert'1#(dd(y,ys),x) -> 'less#(y,x) insert'1#(dd(y,ys),x) -> insert'2#('less(y,x),x,y,ys) insert'2#('true(),x,y,ys) -> insert#(x,ys) insertionsort#(l) -> insertionsort'1#(l) insertionsort'1#(dd(x,xs)) -> insert#(x,insertionsort(xs)) insertionsort'1#(dd(x,xs)) -> insertionsort#(xs) - 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) 'less(x,y) -> 'cklt('compare(x,y)) append(l1,l2) -> append'1(l1,l2) append'1(dd(x,xs),l2) -> dd(x,append(xs,l2)) append'1(nil(),l2) -> l2 flatten(t) -> flatten'1(t) flatten'1(leaf()) -> nil() flatten'1(node(l,t1,t2)) -> append(l,append(flatten(t1),flatten(t2))) insert(x,l) -> insert'1(l,x) insert'1(dd(y,ys),x) -> insert'2('less(y,x),x,y,ys) insert'1(nil(),x) -> dd(x,nil()) insert'2('false(),x,y,ys) -> dd(x,dd(y,ys)) insert'2('true(),x,y,ys) -> dd(y,insert(x,ys)) insertionsort(l) -> insertionsort'1(l) insertionsort'1(dd(x,xs)) -> insert(x,insertionsort(xs)) insertionsort'1(nil()) -> nil() - Signature: {'cklt/1,'compare/2,'less/2,append/2,append'1/2,flatten/1,flatten'1/1,flattensort/1,insert/2,insert'1/2 ,insert'2/4,insertionsort/1,insertionsort'1/1,'cklt#/1,'compare#/2,'less#/2,append#/2,append'1#/2,flatten#/1 ,flatten'1#/1,flattensort#/1,insert#/2,insert'1#/2,insert'2#/4,insertionsort#/1,insertionsort'1#/1} / {'0/0 ,'EQ/0,'GT/0,'LT/0,'false/0,'neg/1,'pos/1,'s/1,'true/0,dd/2,leaf/0,nil/0,node/3,c_1/0,c_2/0,c_3/0,c_4/0 ,c_5/0,c_6/0,c_7/0,c_8/0,c_9/1,c_10/0,c_11/0,c_12/0,c_13/1,c_14/0,c_15/1,c_16/1,c_17/1,c_18/1,c_19/0,c_20/1 ,c_21/0,c_22/4,c_23/2,c_24/1,c_25/2,c_26/0,c_27/0,c_28/1,c_29/1,c_30/2,c_31/0} - Obligation: innermost runtime complexity wrt. defined symbols {'cklt#,'compare#,'less#,append#,append'1#,flatten# ,flatten'1#,flattensort#,insert#,insert'1#,insert'2#,insertionsort#,insertionsort'1#} and constructors {'0 ,'EQ,'GT,'LT,'false,'neg,'pos,'s,'true,dd,leaf,nil,node} + Applied Processor: RemoveWeakSuffixes + Details: Consider the dependency graph 1:S:'compare#('neg(x),'neg(y)) -> c_9('compare#(y,x)) -->_1 'compare#('s(x),'s(y)) -> c_15('compare#(x,y)):3 -->_1 'compare#('pos(x),'pos(y)) -> c_13('compare#(x,y)):2 -->_1 'compare#('neg(x),'neg(y)) -> c_9('compare#(y,x)):1 2:S:'compare#('pos(x),'pos(y)) -> c_13('compare#(x,y)) -->_1 'compare#('s(x),'s(y)) -> c_15('compare#(x,y)):3 -->_1 'compare#('pos(x),'pos(y)) -> c_13('compare#(x,y)):2 -->_1 'compare#('neg(x),'neg(y)) -> c_9('compare#(y,x)):1 3:S:'compare#('s(x),'s(y)) -> c_15('compare#(x,y)) -->_1 'compare#('s(x),'s(y)) -> c_15('compare#(x,y)):3 -->_1 'compare#('pos(x),'pos(y)) -> c_13('compare#(x,y)):2 -->_1 'compare#('neg(x),'neg(y)) -> c_9('compare#(y,x)):1 4:S:'less#(x,y) -> c_16('compare#(x,y)) -->_1 'compare#('s(x),'s(y)) -> c_15('compare#(x,y)):3 -->_1 'compare#('pos(x),'pos(y)) -> c_13('compare#(x,y)):2 -->_1 'compare#('neg(x),'neg(y)) -> c_9('compare#(y,x)):1 5:W:append#(l1,l2) -> append'1#(l1,l2) -->_1 append'1#(dd(x,xs),l2) -> append#(xs,l2):6 6:W:append'1#(dd(x,xs),l2) -> append#(xs,l2) -->_1 append#(l1,l2) -> append'1#(l1,l2):5 7:W:flatten#(t) -> flatten'1#(t) -->_1 flatten'1#(node(l,t1,t2)) -> flatten#(t2):11 -->_1 flatten'1#(node(l,t1,t2)) -> flatten#(t1):10 -->_1 flatten'1#(node(l,t1,t2)) -> append#(flatten(t1),flatten(t2)):9 -->_1 flatten'1#(node(l,t1,t2)) -> append#(l,append(flatten(t1),flatten(t2))):8 8:W:flatten'1#(node(l,t1,t2)) -> append#(l,append(flatten(t1),flatten(t2))) -->_1 append#(l1,l2) -> append'1#(l1,l2):5 9:W:flatten'1#(node(l,t1,t2)) -> append#(flatten(t1),flatten(t2)) -->_1 append#(l1,l2) -> append'1#(l1,l2):5 10:W:flatten'1#(node(l,t1,t2)) -> flatten#(t1) -->_1 flatten#(t) -> flatten'1#(t):7 11:W:flatten'1#(node(l,t1,t2)) -> flatten#(t2) -->_1 flatten#(t) -> flatten'1#(t):7 12:W:flattensort#(t) -> flatten#(t) -->_1 flatten#(t) -> flatten'1#(t):7 13:W:flattensort#(t) -> insertionsort#(flatten(t)) -->_1 insertionsort#(l) -> insertionsort'1#(l):18 14:W:insert#(x,l) -> insert'1#(l,x) -->_1 insert'1#(dd(y,ys),x) -> insert'2#('less(y,x),x,y,ys):16 -->_1 insert'1#(dd(y,ys),x) -> 'less#(y,x):15 15:W:insert'1#(dd(y,ys),x) -> 'less#(y,x) -->_1 'less#(x,y) -> c_16('compare#(x,y)):4 16:W:insert'1#(dd(y,ys),x) -> insert'2#('less(y,x),x,y,ys) -->_1 insert'2#('true(),x,y,ys) -> insert#(x,ys):17 17:W:insert'2#('true(),x,y,ys) -> insert#(x,ys) -->_1 insert#(x,l) -> insert'1#(l,x):14 18:W:insertionsort#(l) -> insertionsort'1#(l) -->_1 insertionsort'1#(dd(x,xs)) -> insertionsort#(xs):20 -->_1 insertionsort'1#(dd(x,xs)) -> insert#(x,insertionsort(xs)):19 19:W:insertionsort'1#(dd(x,xs)) -> insert#(x,insertionsort(xs)) -->_1 insert#(x,l) -> insert'1#(l,x):14 20:W:insertionsort'1#(dd(x,xs)) -> insertionsort#(xs) -->_1 insertionsort#(l) -> insertionsort'1#(l):18 The following weak DPs constitute a sub-graph of the DG that is closed under successors. The DPs are removed. 12: flattensort#(t) -> flatten#(t) 7: flatten#(t) -> flatten'1#(t) 11: flatten'1#(node(l,t1,t2)) -> flatten#(t2) 10: flatten'1#(node(l,t1,t2)) -> flatten#(t1) 8: flatten'1#(node(l,t1,t2)) -> append#(l,append(flatten(t1),flatten(t2))) 9: flatten'1#(node(l,t1,t2)) -> append#(flatten(t1),flatten(t2)) 5: append#(l1,l2) -> append'1#(l1,l2) 6: append'1#(dd(x,xs),l2) -> append#(xs,l2) *** Step 6.b:1.b:2: WeightGap WORST_CASE(?,O(n^1)) + Considered Problem: - Strict DPs: 'compare#('neg(x),'neg(y)) -> c_9('compare#(y,x)) 'compare#('pos(x),'pos(y)) -> c_13('compare#(x,y)) 'compare#('s(x),'s(y)) -> c_15('compare#(x,y)) 'less#(x,y) -> c_16('compare#(x,y)) - Weak DPs: flattensort#(t) -> insertionsort#(flatten(t)) insert#(x,l) -> insert'1#(l,x) insert'1#(dd(y,ys),x) -> 'less#(y,x) insert'1#(dd(y,ys),x) -> insert'2#('less(y,x),x,y,ys) insert'2#('true(),x,y,ys) -> insert#(x,ys) insertionsort#(l) -> insertionsort'1#(l) insertionsort'1#(dd(x,xs)) -> insert#(x,insertionsort(xs)) insertionsort'1#(dd(x,xs)) -> insertionsort#(xs) - 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) 'less(x,y) -> 'cklt('compare(x,y)) append(l1,l2) -> append'1(l1,l2) append'1(dd(x,xs),l2) -> dd(x,append(xs,l2)) append'1(nil(),l2) -> l2 flatten(t) -> flatten'1(t) flatten'1(leaf()) -> nil() flatten'1(node(l,t1,t2)) -> append(l,append(flatten(t1),flatten(t2))) insert(x,l) -> insert'1(l,x) insert'1(dd(y,ys),x) -> insert'2('less(y,x),x,y,ys) insert'1(nil(),x) -> dd(x,nil()) insert'2('false(),x,y,ys) -> dd(x,dd(y,ys)) insert'2('true(),x,y,ys) -> dd(y,insert(x,ys)) insertionsort(l) -> insertionsort'1(l) insertionsort'1(dd(x,xs)) -> insert(x,insertionsort(xs)) insertionsort'1(nil()) -> nil() - Signature: {'cklt/1,'compare/2,'less/2,append/2,append'1/2,flatten/1,flatten'1/1,flattensort/1,insert/2,insert'1/2 ,insert'2/4,insertionsort/1,insertionsort'1/1,'cklt#/1,'compare#/2,'less#/2,append#/2,append'1#/2,flatten#/1 ,flatten'1#/1,flattensort#/1,insert#/2,insert'1#/2,insert'2#/4,insertionsort#/1,insertionsort'1#/1} / {'0/0 ,'EQ/0,'GT/0,'LT/0,'false/0,'neg/1,'pos/1,'s/1,'true/0,dd/2,leaf/0,nil/0,node/3,c_1/0,c_2/0,c_3/0,c_4/0 ,c_5/0,c_6/0,c_7/0,c_8/0,c_9/1,c_10/0,c_11/0,c_12/0,c_13/1,c_14/0,c_15/1,c_16/1,c_17/1,c_18/1,c_19/0,c_20/1 ,c_21/0,c_22/4,c_23/2,c_24/1,c_25/2,c_26/0,c_27/0,c_28/1,c_29/1,c_30/2,c_31/0} - Obligation: innermost runtime complexity wrt. defined symbols {'cklt#,'compare#,'less#,append#,append'1#,flatten# ,flatten'1#,flattensort#,insert#,insert'1#,insert'2#,insertionsort#,insertionsort'1#} and constructors {'0 ,'EQ,'GT,'LT,'false,'neg,'pos,'s,'true,dd,leaf,nil,node} + 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(append) = {1,2}, uargs(dd) = {2}, uargs(insert) = {2}, uargs(insert'2) = {1}, uargs(insert#) = {2}, uargs(insert'2#) = {1}, uargs(insertionsort#) = {1}, uargs(c_9) = {1}, uargs(c_13) = {1}, uargs(c_15) = {1}, uargs(c_16) = {1} Following symbols are considered usable: all TcT has computed the following interpretation: p('0) = [1] p('EQ) = [0] p('GT) = [0] p('LT) = [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(append) = [1] x1 + [1] x2 + [0] p(append'1) = [1] x1 + [1] x2 + [0] p(dd) = [1] x2 + [0] p(flatten) = [1] x1 + [0] p(flatten'1) = [1] x1 + [0] p(flattensort) = [4] x1 + [1] p(insert) = [1] x2 + [0] p(insert'1) = [1] x1 + [0] p(insert'2) = [1] x1 + [1] x4 + [0] p(insertionsort) = [0] p(insertionsort'1) = [0] p(leaf) = [5] p(nil) = [0] p(node) = [1] x1 + [1] x2 + [1] x3 + [0] p('cklt#) = [1] p('compare#) = [0] p('less#) = [4] p(append#) = [4] x1 + [1] p(append'1#) = [2] x2 + [1] p(flatten#) = [1] p(flatten'1#) = [4] x1 + [1] p(flattensort#) = [1] x1 + [4] p(insert#) = [1] x2 + [4] p(insert'1#) = [1] x1 + [4] p(insert'2#) = [1] x1 + [1] x4 + [4] p(insertionsort#) = [1] x1 + [4] p(insertionsort'1#) = [1] x1 + [4] p(c_1) = [1] p(c_2) = [0] p(c_3) = [1] p(c_4) = [0] p(c_5) = [4] p(c_6) = [0] p(c_7) = [0] p(c_8) = [0] p(c_9) = [1] x1 + [0] p(c_10) = [1] p(c_11) = [4] p(c_12) = [1] p(c_13) = [1] x1 + [3] p(c_14) = [4] p(c_15) = [1] x1 + [0] p(c_16) = [1] x1 + [2] p(c_17) = [0] p(c_18) = [1] p(c_19) = [0] p(c_20) = [4] x1 + [0] p(c_21) = [0] p(c_22) = [4] x1 + [1] x2 + [4] x3 + [1] x4 + [4] p(c_23) = [1] x1 + [2] x2 + [0] p(c_24) = [2] x1 + [2] p(c_25) = [4] x2 + [4] p(c_26) = [4] p(c_27) = [0] p(c_28) = [4] x1 + [0] p(c_29) = [1] p(c_30) = [4] x2 + [1] p(c_31) = [2] Following rules are strictly oriented: 'less#(x,y) = [4] > [2] = c_16('compare#(x,y)) Following rules are (at-least) weakly oriented: 'compare#('neg(x),'neg(y)) = [0] >= [0] = c_9('compare#(y,x)) 'compare#('pos(x),'pos(y)) = [0] >= [3] = c_13('compare#(x,y)) 'compare#('s(x),'s(y)) = [0] >= [0] = c_15('compare#(x,y)) flattensort#(t) = [1] t + [4] >= [1] t + [4] = insertionsort#(flatten(t)) insert#(x,l) = [1] l + [4] >= [1] l + [4] = insert'1#(l,x) insert'1#(dd(y,ys),x) = [1] ys + [4] >= [4] = 'less#(y,x) insert'1#(dd(y,ys),x) = [1] ys + [4] >= [1] ys + [4] = insert'2#('less(y,x),x,y,ys) insert'2#('true(),x,y,ys) = [1] ys + [4] >= [1] ys + [4] = insert#(x,ys) insertionsort#(l) = [1] l + [4] >= [1] l + [4] = insertionsort'1#(l) insertionsort'1#(dd(x,xs)) = [1] xs + [4] >= [4] = insert#(x,insertionsort(xs)) insertionsort'1#(dd(x,xs)) = [1] xs + [4] >= [1] xs + [4] = insertionsort#(xs) '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)) append(l1,l2) = [1] l1 + [1] l2 + [0] >= [1] l1 + [1] l2 + [0] = append'1(l1,l2) append'1(dd(x,xs),l2) = [1] l2 + [1] xs + [0] >= [1] l2 + [1] xs + [0] = dd(x,append(xs,l2)) append'1(nil(),l2) = [1] l2 + [0] >= [1] l2 + [0] = l2 flatten(t) = [1] t + [0] >= [1] t + [0] = flatten'1(t) flatten'1(leaf()) = [5] >= [0] = nil() flatten'1(node(l,t1,t2)) = [1] l + [1] t1 + [1] t2 + [0] >= [1] l + [1] t1 + [1] t2 + [0] = append(l,append(flatten(t1),flatten(t2))) insert(x,l) = [1] l + [0] >= [1] l + [0] = insert'1(l,x) insert'1(dd(y,ys),x) = [1] ys + [0] >= [1] ys + [0] = insert'2('less(y,x),x,y,ys) insert'1(nil(),x) = [0] >= [0] = dd(x,nil()) insert'2('false(),x,y,ys) = [1] ys + [0] >= [1] ys + [0] = dd(x,dd(y,ys)) insert'2('true(),x,y,ys) = [1] ys + [0] >= [1] ys + [0] = dd(y,insert(x,ys)) insertionsort(l) = [0] >= [0] = insertionsort'1(l) insertionsort'1(dd(x,xs)) = [0] >= [0] = insert(x,insertionsort(xs)) insertionsort'1(nil()) = [0] >= [0] = nil() Further, it can be verified that all rules not oriented are covered by the weightgap condition. *** Step 6.b:1.b:3: WeightGap WORST_CASE(?,O(n^1)) + Considered Problem: - Strict DPs: 'compare#('neg(x),'neg(y)) -> c_9('compare#(y,x)) 'compare#('pos(x),'pos(y)) -> c_13('compare#(x,y)) 'compare#('s(x),'s(y)) -> c_15('compare#(x,y)) - Weak DPs: 'less#(x,y) -> c_16('compare#(x,y)) flattensort#(t) -> insertionsort#(flatten(t)) insert#(x,l) -> insert'1#(l,x) insert'1#(dd(y,ys),x) -> 'less#(y,x) insert'1#(dd(y,ys),x) -> insert'2#('less(y,x),x,y,ys) insert'2#('true(),x,y,ys) -> insert#(x,ys) insertionsort#(l) -> insertionsort'1#(l) insertionsort'1#(dd(x,xs)) -> insert#(x,insertionsort(xs)) insertionsort'1#(dd(x,xs)) -> insertionsort#(xs) - 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) 'less(x,y) -> 'cklt('compare(x,y)) append(l1,l2) -> append'1(l1,l2) append'1(dd(x,xs),l2) -> dd(x,append(xs,l2)) append'1(nil(),l2) -> l2 flatten(t) -> flatten'1(t) flatten'1(leaf()) -> nil() flatten'1(node(l,t1,t2)) -> append(l,append(flatten(t1),flatten(t2))) insert(x,l) -> insert'1(l,x) insert'1(dd(y,ys),x) -> insert'2('less(y,x),x,y,ys) insert'1(nil(),x) -> dd(x,nil()) insert'2('false(),x,y,ys) -> dd(x,dd(y,ys)) insert'2('true(),x,y,ys) -> dd(y,insert(x,ys)) insertionsort(l) -> insertionsort'1(l) insertionsort'1(dd(x,xs)) -> insert(x,insertionsort(xs)) insertionsort'1(nil()) -> nil() - Signature: {'cklt/1,'compare/2,'less/2,append/2,append'1/2,flatten/1,flatten'1/1,flattensort/1,insert/2,insert'1/2 ,insert'2/4,insertionsort/1,insertionsort'1/1,'cklt#/1,'compare#/2,'less#/2,append#/2,append'1#/2,flatten#/1 ,flatten'1#/1,flattensort#/1,insert#/2,insert'1#/2,insert'2#/4,insertionsort#/1,insertionsort'1#/1} / {'0/0 ,'EQ/0,'GT/0,'LT/0,'false/0,'neg/1,'pos/1,'s/1,'true/0,dd/2,leaf/0,nil/0,node/3,c_1/0,c_2/0,c_3/0,c_4/0 ,c_5/0,c_6/0,c_7/0,c_8/0,c_9/1,c_10/0,c_11/0,c_12/0,c_13/1,c_14/0,c_15/1,c_16/1,c_17/1,c_18/1,c_19/0,c_20/1 ,c_21/0,c_22/4,c_23/2,c_24/1,c_25/2,c_26/0,c_27/0,c_28/1,c_29/1,c_30/2,c_31/0} - Obligation: innermost runtime complexity wrt. defined symbols {'cklt#,'compare#,'less#,append#,append'1#,flatten# ,flatten'1#,flattensort#,insert#,insert'1#,insert'2#,insertionsort#,insertionsort'1#} and constructors {'0 ,'EQ,'GT,'LT,'false,'neg,'pos,'s,'true,dd,leaf,nil,node} + 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(append) = {1,2}, uargs(dd) = {2}, uargs(insert) = {2}, uargs(insert'2) = {1}, uargs(insert#) = {2}, uargs(insert'2#) = {1}, uargs(insertionsort#) = {1}, uargs(c_9) = {1}, uargs(c_13) = {1}, uargs(c_15) = {1}, uargs(c_16) = {1} Following symbols are considered usable: all TcT has computed the following interpretation: p('0) = [1] p('EQ) = [0] p('GT) = [0] p('LT) = [0] p('cklt) = [1] x1 + [0] p('compare) = [0] p('false) = [0] p('less) = [0] p('neg) = [1] x1 + [0] p('pos) = [1] x1 + [0] p('s) = [1] x1 + [2] p('true) = [0] p(append) = [1] x1 + [1] x2 + [2] p(append'1) = [1] x1 + [1] x2 + [2] p(dd) = [1] x1 + [1] x2 + [0] p(flatten) = [1] x1 + [0] p(flatten'1) = [1] x1 + [0] p(flattensort) = [1] x1 + [2] 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(insertionsort) = [1] x1 + [0] p(insertionsort'1) = [1] x1 + [0] p(leaf) = [2] p(nil) = [0] p(node) = [1] x1 + [1] x2 + [1] x3 + [4] p('cklt#) = [0] p('compare#) = [1] x1 + [1] x2 + [0] p('less#) = [1] x1 + [1] x2 + [0] p(append#) = [2] x1 + [1] p(append'1#) = [1] x2 + [1] p(flatten#) = [1] x1 + [0] p(flatten'1#) = [0] p(flattensort#) = [2] x1 + [5] 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(insertionsort#) = [1] x1 + [0] p(insertionsort'1#) = [1] x1 + [0] p(c_1) = [1] p(c_2) = [1] p(c_3) = [4] p(c_4) = [0] p(c_5) = [2] p(c_6) = [2] p(c_7) = [0] p(c_8) = [1] p(c_9) = [1] x1 + [0] p(c_10) = [2] p(c_11) = [1] p(c_12) = [4] p(c_13) = [1] x1 + [0] p(c_14) = [1] p(c_15) = [1] x1 + [2] p(c_16) = [1] x1 + [0] p(c_17) = [4] x1 + [0] p(c_18) = [0] p(c_19) = [0] p(c_20) = [0] p(c_21) = [4] p(c_22) = [4] x2 + [4] x3 + [0] p(c_23) = [1] x1 + [4] p(c_24) = [4] p(c_25) = [1] p(c_26) = [0] p(c_27) = [2] p(c_28) = [1] x1 + [0] p(c_29) = [0] p(c_30) = [1] x2 + [1] p(c_31) = [1] Following rules are strictly oriented: 'compare#('s(x),'s(y)) = [1] x + [1] y + [4] > [1] x + [1] y + [2] = c_15('compare#(x,y)) Following rules are (at-least) weakly oriented: 'compare#('neg(x),'neg(y)) = [1] x + [1] y + [0] >= [1] x + [1] y + [0] = c_9('compare#(y,x)) 'compare#('pos(x),'pos(y)) = [1] x + [1] y + [0] >= [1] x + [1] y + [0] = c_13('compare#(x,y)) 'less#(x,y) = [1] x + [1] y + [0] >= [1] x + [1] y + [0] = c_16('compare#(x,y)) flattensort#(t) = [2] t + [5] >= [1] t + [0] = insertionsort#(flatten(t)) insert#(x,l) = [1] l + [1] x + [0] >= [1] l + [1] x + [0] = insert'1#(l,x) insert'1#(dd(y,ys),x) = [1] x + [1] y + [1] ys + [0] >= [1] x + [1] y + [0] = 'less#(y,x) insert'1#(dd(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'2#('true(),x,y,ys) = [1] x + [1] y + [1] ys + [0] >= [1] x + [1] ys + [0] = insert#(x,ys) insertionsort#(l) = [1] l + [0] >= [1] l + [0] = insertionsort'1#(l) insertionsort'1#(dd(x,xs)) = [1] x + [1] xs + [0] >= [1] x + [1] xs + [0] = insert#(x,insertionsort(xs)) insertionsort'1#(dd(x,xs)) = [1] x + [1] xs + [0] >= [1] xs + [0] = insertionsort#(xs) '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)) append(l1,l2) = [1] l1 + [1] l2 + [2] >= [1] l1 + [1] l2 + [2] = append'1(l1,l2) append'1(dd(x,xs),l2) = [1] l2 + [1] x + [1] xs + [2] >= [1] l2 + [1] x + [1] xs + [2] = dd(x,append(xs,l2)) append'1(nil(),l2) = [1] l2 + [2] >= [1] l2 + [0] = l2 flatten(t) = [1] t + [0] >= [1] t + [0] = flatten'1(t) flatten'1(leaf()) = [2] >= [0] = nil() flatten'1(node(l,t1,t2)) = [1] l + [1] t1 + [1] t2 + [4] >= [1] l + [1] t1 + [1] t2 + [4] = append(l,append(flatten(t1),flatten(t2))) insert(x,l) = [1] l + [1] x + [0] >= [1] l + [1] x + [0] = insert'1(l,x) insert'1(dd(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] = dd(x,nil()) insert'2('false(),x,y,ys) = [1] x + [1] y + [1] ys + [0] >= [1] x + [1] y + [1] ys + [0] = dd(x,dd(y,ys)) insert'2('true(),x,y,ys) = [1] x + [1] y + [1] ys + [0] >= [1] x + [1] y + [1] ys + [0] = dd(y,insert(x,ys)) insertionsort(l) = [1] l + [0] >= [1] l + [0] = insertionsort'1(l) insertionsort'1(dd(x,xs)) = [1] x + [1] xs + [0] >= [1] x + [1] xs + [0] = insert(x,insertionsort(xs)) insertionsort'1(nil()) = [0] >= [0] = nil() Further, it can be verified that all rules not oriented are covered by the weightgap condition. *** Step 6.b:1.b:4: WeightGap WORST_CASE(?,O(n^1)) + Considered Problem: - Strict DPs: 'compare#('neg(x),'neg(y)) -> c_9('compare#(y,x)) 'compare#('pos(x),'pos(y)) -> c_13('compare#(x,y)) - Weak DPs: 'compare#('s(x),'s(y)) -> c_15('compare#(x,y)) 'less#(x,y) -> c_16('compare#(x,y)) flattensort#(t) -> insertionsort#(flatten(t)) insert#(x,l) -> insert'1#(l,x) insert'1#(dd(y,ys),x) -> 'less#(y,x) insert'1#(dd(y,ys),x) -> insert'2#('less(y,x),x,y,ys) insert'2#('true(),x,y,ys) -> insert#(x,ys) insertionsort#(l) -> insertionsort'1#(l) insertionsort'1#(dd(x,xs)) -> insert#(x,insertionsort(xs)) insertionsort'1#(dd(x,xs)) -> insertionsort#(xs) - 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) 'less(x,y) -> 'cklt('compare(x,y)) append(l1,l2) -> append'1(l1,l2) append'1(dd(x,xs),l2) -> dd(x,append(xs,l2)) append'1(nil(),l2) -> l2 flatten(t) -> flatten'1(t) flatten'1(leaf()) -> nil() flatten'1(node(l,t1,t2)) -> append(l,append(flatten(t1),flatten(t2))) insert(x,l) -> insert'1(l,x) insert'1(dd(y,ys),x) -> insert'2('less(y,x),x,y,ys) insert'1(nil(),x) -> dd(x,nil()) insert'2('false(),x,y,ys) -> dd(x,dd(y,ys)) insert'2('true(),x,y,ys) -> dd(y,insert(x,ys)) insertionsort(l) -> insertionsort'1(l) insertionsort'1(dd(x,xs)) -> insert(x,insertionsort(xs)) insertionsort'1(nil()) -> nil() - Signature: {'cklt/1,'compare/2,'less/2,append/2,append'1/2,flatten/1,flatten'1/1,flattensort/1,insert/2,insert'1/2 ,insert'2/4,insertionsort/1,insertionsort'1/1,'cklt#/1,'compare#/2,'less#/2,append#/2,append'1#/2,flatten#/1 ,flatten'1#/1,flattensort#/1,insert#/2,insert'1#/2,insert'2#/4,insertionsort#/1,insertionsort'1#/1} / {'0/0 ,'EQ/0,'GT/0,'LT/0,'false/0,'neg/1,'pos/1,'s/1,'true/0,dd/2,leaf/0,nil/0,node/3,c_1/0,c_2/0,c_3/0,c_4/0 ,c_5/0,c_6/0,c_7/0,c_8/0,c_9/1,c_10/0,c_11/0,c_12/0,c_13/1,c_14/0,c_15/1,c_16/1,c_17/1,c_18/1,c_19/0,c_20/1 ,c_21/0,c_22/4,c_23/2,c_24/1,c_25/2,c_26/0,c_27/0,c_28/1,c_29/1,c_30/2,c_31/0} - Obligation: innermost runtime complexity wrt. defined symbols {'cklt#,'compare#,'less#,append#,append'1#,flatten# ,flatten'1#,flattensort#,insert#,insert'1#,insert'2#,insertionsort#,insertionsort'1#} and constructors {'0 ,'EQ,'GT,'LT,'false,'neg,'pos,'s,'true,dd,leaf,nil,node} + 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(append) = {1,2}, uargs(dd) = {2}, uargs(insert) = {2}, uargs(insert'2) = {1}, uargs(insert#) = {2}, uargs(insert'2#) = {1}, uargs(insertionsort#) = {1}, uargs(c_9) = {1}, uargs(c_13) = {1}, uargs(c_15) = {1}, uargs(c_16) = {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('cklt) = [1] x1 + [0] p('compare) = [0] p('false) = [0] p('less) = [0] p('neg) = [1] x1 + [0] p('pos) = [1] x1 + [4] p('s) = [1] x1 + [4] p('true) = [0] p(append) = [1] x1 + [1] x2 + [3] p(append'1) = [1] x1 + [1] x2 + [3] p(dd) = [1] x1 + [1] x2 + [0] p(flatten) = [4] x1 + [2] p(flatten'1) = [4] x1 + [0] p(flattensort) = [4] x1 + [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(insertionsort) = [1] x1 + [0] p(insertionsort'1) = [1] x1 + [0] p(leaf) = [0] p(nil) = [0] p(node) = [1] x1 + [1] x2 + [1] x3 + [3] p('cklt#) = [2] p('compare#) = [1] x1 + [1] x2 + [0] p('less#) = [1] x1 + [1] x2 + [0] p(append#) = [1] x1 + [1] p(append'1#) = [1] x2 + [2] p(flatten#) = [1] x1 + [4] p(flatten'1#) = [0] p(flattensort#) = [4] x1 + [3] p(insert#) = [1] x1 + [1] x2 + [0] p(insert'1#) = [1] x1 + [1] x2 + [0] p(insert'2#) = [1] x1 + [1] x2 + [1] x4 + [0] p(insertionsort#) = [1] x1 + [0] p(insertionsort'1#) = [1] x1 + [0] p(c_1) = [0] p(c_2) = [0] p(c_3) = [0] p(c_4) = [0] p(c_5) = [0] p(c_6) = [1] p(c_7) = [1] p(c_8) = [1] p(c_9) = [1] x1 + [1] p(c_10) = [4] p(c_11) = [1] p(c_12) = [2] p(c_13) = [1] x1 + [1] p(c_14) = [4] p(c_15) = [1] x1 + [1] p(c_16) = [1] x1 + [0] p(c_17) = [4] x1 + [0] p(c_18) = [1] x1 + [0] p(c_19) = [0] p(c_20) = [0] p(c_21) = [1] p(c_22) = [1] x1 + [1] x2 + [1] x3 + [2] x4 + [0] p(c_23) = [1] x2 + [2] p(c_24) = [0] p(c_25) = [1] x2 + [1] p(c_26) = [1] p(c_27) = [0] p(c_28) = [1] x1 + [0] p(c_29) = [2] x1 + [1] p(c_30) = [1] x1 + [0] p(c_31) = [2] Following rules are strictly oriented: 'compare#('pos(x),'pos(y)) = [1] x + [1] y + [8] > [1] x + [1] y + [1] = c_13('compare#(x,y)) Following rules are (at-least) weakly oriented: 'compare#('neg(x),'neg(y)) = [1] x + [1] y + [0] >= [1] x + [1] y + [1] = c_9('compare#(y,x)) 'compare#('s(x),'s(y)) = [1] x + [1] y + [8] >= [1] x + [1] y + [1] = c_15('compare#(x,y)) 'less#(x,y) = [1] x + [1] y + [0] >= [1] x + [1] y + [0] = c_16('compare#(x,y)) flattensort#(t) = [4] t + [3] >= [4] t + [2] = insertionsort#(flatten(t)) insert#(x,l) = [1] l + [1] x + [0] >= [1] l + [1] x + [0] = insert'1#(l,x) insert'1#(dd(y,ys),x) = [1] x + [1] y + [1] ys + [0] >= [1] x + [1] y + [0] = 'less#(y,x) insert'1#(dd(y,ys),x) = [1] x + [1] y + [1] ys + [0] >= [1] x + [1] ys + [0] = insert'2#('less(y,x),x,y,ys) insert'2#('true(),x,y,ys) = [1] x + [1] ys + [0] >= [1] x + [1] ys + [0] = insert#(x,ys) insertionsort#(l) = [1] l + [0] >= [1] l + [0] = insertionsort'1#(l) insertionsort'1#(dd(x,xs)) = [1] x + [1] xs + [0] >= [1] x + [1] xs + [0] = insert#(x,insertionsort(xs)) insertionsort'1#(dd(x,xs)) = [1] x + [1] xs + [0] >= [1] xs + [0] = insertionsort#(xs) '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)) append(l1,l2) = [1] l1 + [1] l2 + [3] >= [1] l1 + [1] l2 + [3] = append'1(l1,l2) append'1(dd(x,xs),l2) = [1] l2 + [1] x + [1] xs + [3] >= [1] l2 + [1] x + [1] xs + [3] = dd(x,append(xs,l2)) append'1(nil(),l2) = [1] l2 + [3] >= [1] l2 + [0] = l2 flatten(t) = [4] t + [2] >= [4] t + [0] = flatten'1(t) flatten'1(leaf()) = [0] >= [0] = nil() flatten'1(node(l,t1,t2)) = [4] l + [4] t1 + [4] t2 + [12] >= [1] l + [4] t1 + [4] t2 + [10] = append(l,append(flatten(t1),flatten(t2))) insert(x,l) = [1] l + [1] x + [0] >= [1] l + [1] x + [0] = insert'1(l,x) insert'1(dd(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] = dd(x,nil()) insert'2('false(),x,y,ys) = [1] x + [1] y + [1] ys + [0] >= [1] x + [1] y + [1] ys + [0] = dd(x,dd(y,ys)) insert'2('true(),x,y,ys) = [1] x + [1] y + [1] ys + [0] >= [1] x + [1] y + [1] ys + [0] = dd(y,insert(x,ys)) insertionsort(l) = [1] l + [0] >= [1] l + [0] = insertionsort'1(l) insertionsort'1(dd(x,xs)) = [1] x + [1] xs + [0] >= [1] x + [1] xs + [0] = insert(x,insertionsort(xs)) insertionsort'1(nil()) = [0] >= [0] = nil() Further, it can be verified that all rules not oriented are covered by the weightgap condition. *** Step 6.b:1.b:5: WeightGap WORST_CASE(?,O(n^1)) + Considered Problem: - Strict DPs: 'compare#('neg(x),'neg(y)) -> c_9('compare#(y,x)) - Weak DPs: 'compare#('pos(x),'pos(y)) -> c_13('compare#(x,y)) 'compare#('s(x),'s(y)) -> c_15('compare#(x,y)) 'less#(x,y) -> c_16('compare#(x,y)) flattensort#(t) -> insertionsort#(flatten(t)) insert#(x,l) -> insert'1#(l,x) insert'1#(dd(y,ys),x) -> 'less#(y,x) insert'1#(dd(y,ys),x) -> insert'2#('less(y,x),x,y,ys) insert'2#('true(),x,y,ys) -> insert#(x,ys) insertionsort#(l) -> insertionsort'1#(l) insertionsort'1#(dd(x,xs)) -> insert#(x,insertionsort(xs)) insertionsort'1#(dd(x,xs)) -> insertionsort#(xs) - 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) 'less(x,y) -> 'cklt('compare(x,y)) append(l1,l2) -> append'1(l1,l2) append'1(dd(x,xs),l2) -> dd(x,append(xs,l2)) append'1(nil(),l2) -> l2 flatten(t) -> flatten'1(t) flatten'1(leaf()) -> nil() flatten'1(node(l,t1,t2)) -> append(l,append(flatten(t1),flatten(t2))) insert(x,l) -> insert'1(l,x) insert'1(dd(y,ys),x) -> insert'2('less(y,x),x,y,ys) insert'1(nil(),x) -> dd(x,nil()) insert'2('false(),x,y,ys) -> dd(x,dd(y,ys)) insert'2('true(),x,y,ys) -> dd(y,insert(x,ys)) insertionsort(l) -> insertionsort'1(l) insertionsort'1(dd(x,xs)) -> insert(x,insertionsort(xs)) insertionsort'1(nil()) -> nil() - Signature: {'cklt/1,'compare/2,'less/2,append/2,append'1/2,flatten/1,flatten'1/1,flattensort/1,insert/2,insert'1/2 ,insert'2/4,insertionsort/1,insertionsort'1/1,'cklt#/1,'compare#/2,'less#/2,append#/2,append'1#/2,flatten#/1 ,flatten'1#/1,flattensort#/1,insert#/2,insert'1#/2,insert'2#/4,insertionsort#/1,insertionsort'1#/1} / {'0/0 ,'EQ/0,'GT/0,'LT/0,'false/0,'neg/1,'pos/1,'s/1,'true/0,dd/2,leaf/0,nil/0,node/3,c_1/0,c_2/0,c_3/0,c_4/0 ,c_5/0,c_6/0,c_7/0,c_8/0,c_9/1,c_10/0,c_11/0,c_12/0,c_13/1,c_14/0,c_15/1,c_16/1,c_17/1,c_18/1,c_19/0,c_20/1 ,c_21/0,c_22/4,c_23/2,c_24/1,c_25/2,c_26/0,c_27/0,c_28/1,c_29/1,c_30/2,c_31/0} - Obligation: innermost runtime complexity wrt. defined symbols {'cklt#,'compare#,'less#,append#,append'1#,flatten# ,flatten'1#,flattensort#,insert#,insert'1#,insert'2#,insertionsort#,insertionsort'1#} and constructors {'0 ,'EQ,'GT,'LT,'false,'neg,'pos,'s,'true,dd,leaf,nil,node} + 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(append) = {1,2}, uargs(dd) = {2}, uargs(insert) = {2}, uargs(insert'2) = {1}, uargs(insert#) = {2}, uargs(insert'2#) = {1}, uargs(insertionsort#) = {1}, uargs(c_9) = {1}, uargs(c_13) = {1}, uargs(c_15) = {1}, uargs(c_16) = {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('cklt) = [1] x1 + [0] p('compare) = [0] p('false) = [0] p('less) = [0] p('neg) = [1] x1 + [4] p('pos) = [1] x1 + [1] p('s) = [1] x1 + [1] p('true) = [0] p(append) = [1] x1 + [1] x2 + [1] p(append'1) = [1] x1 + [1] x2 + [1] p(dd) = [1] x1 + [1] x2 + [0] p(flatten) = [1] x1 + [2] p(flatten'1) = [1] x1 + [2] p(flattensort) = [4] 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(insertionsort) = [1] x1 + [0] p(insertionsort'1) = [1] x1 + [0] p(leaf) = [0] p(nil) = [1] p(node) = [1] x1 + [1] x2 + [1] x3 + [5] p('cklt#) = [1] p('compare#) = [1] x1 + [1] x2 + [0] p('less#) = [1] x1 + [1] x2 + [1] p(append#) = [2] x1 + [4] p(append'1#) = [2] x1 + [4] x2 + [2] p(flatten#) = [1] x1 + [1] p(flatten'1#) = [1] x1 + [2] p(flattensort#) = [2] x1 + [5] p(insert#) = [1] x1 + [1] x2 + [2] p(insert'1#) = [1] x1 + [1] x2 + [2] p(insert'2#) = [1] x1 + [1] x2 + [1] x3 + [1] x4 + [2] p(insertionsort#) = [1] x1 + [2] p(insertionsort'1#) = [1] x1 + [2] p(c_1) = [0] p(c_2) = [1] p(c_3) = [1] p(c_4) = [0] p(c_5) = [2] p(c_6) = [0] p(c_7) = [4] p(c_8) = [2] p(c_9) = [1] x1 + [4] p(c_10) = [1] p(c_11) = [2] p(c_12) = [4] p(c_13) = [1] x1 + [0] p(c_14) = [0] p(c_15) = [1] x1 + [1] p(c_16) = [1] x1 + [1] p(c_17) = [4] p(c_18) = [4] x1 + [4] p(c_19) = [0] p(c_20) = [2] x1 + [1] p(c_21) = [1] p(c_22) = [4] x1 + [4] x2 + [4] p(c_23) = [2] x2 + [1] p(c_24) = [1] p(c_25) = [1] p(c_26) = [0] p(c_27) = [1] p(c_28) = [0] p(c_29) = [4] x1 + [4] p(c_30) = [1] x1 + [1] x2 + [1] p(c_31) = [1] Following rules are strictly oriented: 'compare#('neg(x),'neg(y)) = [1] x + [1] y + [8] > [1] x + [1] y + [4] = c_9('compare#(y,x)) Following rules are (at-least) weakly oriented: 'compare#('pos(x),'pos(y)) = [1] x + [1] y + [2] >= [1] x + [1] y + [0] = c_13('compare#(x,y)) 'compare#('s(x),'s(y)) = [1] x + [1] y + [2] >= [1] x + [1] y + [1] = c_15('compare#(x,y)) 'less#(x,y) = [1] x + [1] y + [1] >= [1] x + [1] y + [1] = c_16('compare#(x,y)) flattensort#(t) = [2] t + [5] >= [1] t + [4] = insertionsort#(flatten(t)) insert#(x,l) = [1] l + [1] x + [2] >= [1] l + [1] x + [2] = insert'1#(l,x) insert'1#(dd(y,ys),x) = [1] x + [1] y + [1] ys + [2] >= [1] x + [1] y + [1] = 'less#(y,x) insert'1#(dd(y,ys),x) = [1] x + [1] y + [1] ys + [2] >= [1] x + [1] y + [1] ys + [2] = insert'2#('less(y,x),x,y,ys) insert'2#('true(),x,y,ys) = [1] x + [1] y + [1] ys + [2] >= [1] x + [1] ys + [2] = insert#(x,ys) insertionsort#(l) = [1] l + [2] >= [1] l + [2] = insertionsort'1#(l) insertionsort'1#(dd(x,xs)) = [1] x + [1] xs + [2] >= [1] x + [1] xs + [2] = insert#(x,insertionsort(xs)) insertionsort'1#(dd(x,xs)) = [1] x + [1] xs + [2] >= [1] xs + [2] = insertionsort#(xs) '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)) append(l1,l2) = [1] l1 + [1] l2 + [1] >= [1] l1 + [1] l2 + [1] = append'1(l1,l2) append'1(dd(x,xs),l2) = [1] l2 + [1] x + [1] xs + [1] >= [1] l2 + [1] x + [1] xs + [1] = dd(x,append(xs,l2)) append'1(nil(),l2) = [1] l2 + [2] >= [1] l2 + [0] = l2 flatten(t) = [1] t + [2] >= [1] t + [2] = flatten'1(t) flatten'1(leaf()) = [2] >= [1] = nil() flatten'1(node(l,t1,t2)) = [1] l + [1] t1 + [1] t2 + [7] >= [1] l + [1] t1 + [1] t2 + [6] = append(l,append(flatten(t1),flatten(t2))) insert(x,l) = [1] l + [1] x + [0] >= [1] l + [1] x + [0] = insert'1(l,x) insert'1(dd(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 + [1] >= [1] x + [1] = dd(x,nil()) insert'2('false(),x,y,ys) = [1] x + [1] y + [1] ys + [0] >= [1] x + [1] y + [1] ys + [0] = dd(x,dd(y,ys)) insert'2('true(),x,y,ys) = [1] x + [1] y + [1] ys + [0] >= [1] x + [1] y + [1] ys + [0] = dd(y,insert(x,ys)) insertionsort(l) = [1] l + [0] >= [1] l + [0] = insertionsort'1(l) insertionsort'1(dd(x,xs)) = [1] x + [1] xs + [0] >= [1] x + [1] xs + [0] = insert(x,insertionsort(xs)) insertionsort'1(nil()) = [1] >= [1] = nil() Further, it can be verified that all rules not oriented are covered by the weightgap condition. *** Step 6.b:1.b:6: EmptyProcessor WORST_CASE(?,O(1)) + Considered Problem: - Weak DPs: 'compare#('neg(x),'neg(y)) -> c_9('compare#(y,x)) 'compare#('pos(x),'pos(y)) -> c_13('compare#(x,y)) 'compare#('s(x),'s(y)) -> c_15('compare#(x,y)) 'less#(x,y) -> c_16('compare#(x,y)) flattensort#(t) -> insertionsort#(flatten(t)) insert#(x,l) -> insert'1#(l,x) insert'1#(dd(y,ys),x) -> 'less#(y,x) insert'1#(dd(y,ys),x) -> insert'2#('less(y,x),x,y,ys) insert'2#('true(),x,y,ys) -> insert#(x,ys) insertionsort#(l) -> insertionsort'1#(l) insertionsort'1#(dd(x,xs)) -> insert#(x,insertionsort(xs)) insertionsort'1#(dd(x,xs)) -> insertionsort#(xs) - 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) 'less(x,y) -> 'cklt('compare(x,y)) append(l1,l2) -> append'1(l1,l2) append'1(dd(x,xs),l2) -> dd(x,append(xs,l2)) append'1(nil(),l2) -> l2 flatten(t) -> flatten'1(t) flatten'1(leaf()) -> nil() flatten'1(node(l,t1,t2)) -> append(l,append(flatten(t1),flatten(t2))) insert(x,l) -> insert'1(l,x) insert'1(dd(y,ys),x) -> insert'2('less(y,x),x,y,ys) insert'1(nil(),x) -> dd(x,nil()) insert'2('false(),x,y,ys) -> dd(x,dd(y,ys)) insert'2('true(),x,y,ys) -> dd(y,insert(x,ys)) insertionsort(l) -> insertionsort'1(l) insertionsort'1(dd(x,xs)) -> insert(x,insertionsort(xs)) insertionsort'1(nil()) -> nil() - Signature: {'cklt/1,'compare/2,'less/2,append/2,append'1/2,flatten/1,flatten'1/1,flattensort/1,insert/2,insert'1/2 ,insert'2/4,insertionsort/1,insertionsort'1/1,'cklt#/1,'compare#/2,'less#/2,append#/2,append'1#/2,flatten#/1 ,flatten'1#/1,flattensort#/1,insert#/2,insert'1#/2,insert'2#/4,insertionsort#/1,insertionsort'1#/1} / {'0/0 ,'EQ/0,'GT/0,'LT/0,'false/0,'neg/1,'pos/1,'s/1,'true/0,dd/2,leaf/0,nil/0,node/3,c_1/0,c_2/0,c_3/0,c_4/0 ,c_5/0,c_6/0,c_7/0,c_8/0,c_9/1,c_10/0,c_11/0,c_12/0,c_13/1,c_14/0,c_15/1,c_16/1,c_17/1,c_18/1,c_19/0,c_20/1 ,c_21/0,c_22/4,c_23/2,c_24/1,c_25/2,c_26/0,c_27/0,c_28/1,c_29/1,c_30/2,c_31/0} - Obligation: innermost runtime complexity wrt. defined symbols {'cklt#,'compare#,'less#,append#,append'1#,flatten# ,flatten'1#,flattensort#,insert#,insert'1#,insert'2#,insertionsort#,insertionsort'1#} and constructors {'0 ,'EQ,'GT,'LT,'false,'neg,'pos,'s,'true,dd,leaf,nil,node} + Applied Processor: EmptyProcessor + Details: The problem is already closed. The intended complexity is O(1). WORST_CASE(?,O(n^3))