WORST_CASE(?,O(n^2)) * Step 1: Sum. WORST_CASE(?,O(n^2)) + Considered Problem: - Strict TRS: #LESS(z0,z1) -> c15(#CKLT(#compare(z0,z1)),#COMPARE(z0,z1)) APPEND(z0,z1) -> c16(APPEND#1(z0,z1)) APPEND#1(::(z0,z1),z2) -> c17(APPEND(z1,z2)) APPEND#1(nil(),z0) -> c18() FLATTEN(z0) -> c19(FLATTEN#1(z0)) FLATTEN#1(leaf()) -> c20() FLATTEN#1(node(z0,z1,z2)) -> c21(APPEND(z0,append(flatten(z1),flatten(z2))) ,APPEND(flatten(z1),flatten(z2)) ,FLATTEN(z1)) FLATTEN#1(node(z0,z1,z2)) -> c22(APPEND(z0,append(flatten(z1),flatten(z2))) ,APPEND(flatten(z1),flatten(z2)) ,FLATTEN(z2)) FLATTENSORT(z0) -> c23(INSERTIONSORT(flatten(z0)),FLATTEN(z0)) INSERT(z0,z1) -> c24(INSERT#1(z1,z0)) INSERT#1(::(z0,z1),z2) -> c25(INSERT#2(#less(z0,z2),z2,z0,z1),#LESS(z0,z2)) INSERT#1(nil(),z0) -> c26() INSERT#2(#false(),z0,z1,z2) -> c27() INSERT#2(#true(),z0,z1,z2) -> c28(INSERT(z0,z2)) INSERTIONSORT(z0) -> c29(INSERTIONSORT#1(z0)) INSERTIONSORT#1(::(z0,z1)) -> c30(INSERT(z0,insertionsort(z1)),INSERTIONSORT(z1)) INSERTIONSORT#1(nil()) -> c31() - Weak TRS: #CKLT(#EQ()) -> c() #CKLT(#GT()) -> c1() #CKLT(#LT()) -> c2() #COMPARE(#0(),#0()) -> c3() #COMPARE(#0(),#neg(z0)) -> c4() #COMPARE(#0(),#pos(z0)) -> c5() #COMPARE(#0(),#s(z0)) -> c6() #COMPARE(#neg(z0),#0()) -> c7() #COMPARE(#neg(z0),#neg(z1)) -> c8(#COMPARE(z1,z0)) #COMPARE(#neg(z0),#pos(z1)) -> c9() #COMPARE(#pos(z0),#0()) -> c10() #COMPARE(#pos(z0),#neg(z1)) -> c11() #COMPARE(#pos(z0),#pos(z1)) -> c12(#COMPARE(z0,z1)) #COMPARE(#s(z0),#0()) -> c13() #COMPARE(#s(z0),#s(z1)) -> c14(#COMPARE(z0,z1)) #cklt(#EQ()) -> #false() #cklt(#GT()) -> #false() #cklt(#LT()) -> #true() #compare(#0(),#0()) -> #EQ() #compare(#0(),#neg(z0)) -> #GT() #compare(#0(),#pos(z0)) -> #LT() #compare(#0(),#s(z0)) -> #LT() #compare(#neg(z0),#0()) -> #LT() #compare(#neg(z0),#neg(z1)) -> #compare(z1,z0) #compare(#neg(z0),#pos(z1)) -> #LT() #compare(#pos(z0),#0()) -> #GT() #compare(#pos(z0),#neg(z1)) -> #GT() #compare(#pos(z0),#pos(z1)) -> #compare(z0,z1) #compare(#s(z0),#0()) -> #GT() #compare(#s(z0),#s(z1)) -> #compare(z0,z1) #less(z0,z1) -> #cklt(#compare(z0,z1)) append(z0,z1) -> append#1(z0,z1) append#1(::(z0,z1),z2) -> ::(z0,append(z1,z2)) append#1(nil(),z0) -> z0 flatten(z0) -> flatten#1(z0) flatten#1(leaf()) -> nil() flatten#1(node(z0,z1,z2)) -> append(z0,append(flatten(z1),flatten(z2))) flattensort(z0) -> insertionsort(flatten(z0)) insert(z0,z1) -> insert#1(z1,z0) insert#1(::(z0,z1),z2) -> insert#2(#less(z0,z2),z2,z0,z1) insert#1(nil(),z0) -> ::(z0,nil()) insert#2(#false(),z0,z1,z2) -> ::(z0,::(z1,z2)) insert#2(#true(),z0,z1,z2) -> ::(z1,insert(z0,z2)) insertionsort(z0) -> insertionsort#1(z0) insertionsort#1(::(z0,z1)) -> insert(z0,insertionsort(z1)) insertionsort#1(nil()) -> nil() - Signature: {#CKLT/1,#COMPARE/2,#LESS/2,#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,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,::/2,c/0,c1/0,c10/0,c11/0 ,c12/1,c13/0,c14/1,c15/2,c16/1,c17/1,c18/0,c19/1,c2/0,c20/0,c21/3,c22/3,c23/2,c24/1,c25/2,c26/0,c27/0,c28/1 ,c29/1,c3/0,c30/2,c31/0,c4/0,c5/0,c6/0,c7/0,c8/1,c9/0,leaf/0,nil/0,node/3} - Obligation: innermost runtime complexity wrt. defined symbols {#CKLT,#COMPARE,#LESS,#cklt,#compare,#less,APPEND,APPEND#1 ,FLATTEN,FLATTEN#1,FLATTENSORT,INSERT,INSERT#1,INSERT#2,INSERTIONSORT,INSERTIONSORT#1,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,::,c,c1,c10,c11,c12,c13,c14,c15,c16,c17,c18,c19,c2,c20,c21,c22,c23 ,c24,c25,c26,c27,c28,c29,c3,c30,c31,c4,c5,c6,c7,c8,c9,leaf,nil,node} + Applied Processor: Sum {left = someStrategy, right = someStrategy} + Details: () * Step 2: DependencyPairs. WORST_CASE(?,O(n^2)) + Considered Problem: - Strict TRS: #LESS(z0,z1) -> c15(#CKLT(#compare(z0,z1)),#COMPARE(z0,z1)) APPEND(z0,z1) -> c16(APPEND#1(z0,z1)) APPEND#1(::(z0,z1),z2) -> c17(APPEND(z1,z2)) APPEND#1(nil(),z0) -> c18() FLATTEN(z0) -> c19(FLATTEN#1(z0)) FLATTEN#1(leaf()) -> c20() FLATTEN#1(node(z0,z1,z2)) -> c21(APPEND(z0,append(flatten(z1),flatten(z2))) ,APPEND(flatten(z1),flatten(z2)) ,FLATTEN(z1)) FLATTEN#1(node(z0,z1,z2)) -> c22(APPEND(z0,append(flatten(z1),flatten(z2))) ,APPEND(flatten(z1),flatten(z2)) ,FLATTEN(z2)) FLATTENSORT(z0) -> c23(INSERTIONSORT(flatten(z0)),FLATTEN(z0)) INSERT(z0,z1) -> c24(INSERT#1(z1,z0)) INSERT#1(::(z0,z1),z2) -> c25(INSERT#2(#less(z0,z2),z2,z0,z1),#LESS(z0,z2)) INSERT#1(nil(),z0) -> c26() INSERT#2(#false(),z0,z1,z2) -> c27() INSERT#2(#true(),z0,z1,z2) -> c28(INSERT(z0,z2)) INSERTIONSORT(z0) -> c29(INSERTIONSORT#1(z0)) INSERTIONSORT#1(::(z0,z1)) -> c30(INSERT(z0,insertionsort(z1)),INSERTIONSORT(z1)) INSERTIONSORT#1(nil()) -> c31() - Weak TRS: #CKLT(#EQ()) -> c() #CKLT(#GT()) -> c1() #CKLT(#LT()) -> c2() #COMPARE(#0(),#0()) -> c3() #COMPARE(#0(),#neg(z0)) -> c4() #COMPARE(#0(),#pos(z0)) -> c5() #COMPARE(#0(),#s(z0)) -> c6() #COMPARE(#neg(z0),#0()) -> c7() #COMPARE(#neg(z0),#neg(z1)) -> c8(#COMPARE(z1,z0)) #COMPARE(#neg(z0),#pos(z1)) -> c9() #COMPARE(#pos(z0),#0()) -> c10() #COMPARE(#pos(z0),#neg(z1)) -> c11() #COMPARE(#pos(z0),#pos(z1)) -> c12(#COMPARE(z0,z1)) #COMPARE(#s(z0),#0()) -> c13() #COMPARE(#s(z0),#s(z1)) -> c14(#COMPARE(z0,z1)) #cklt(#EQ()) -> #false() #cklt(#GT()) -> #false() #cklt(#LT()) -> #true() #compare(#0(),#0()) -> #EQ() #compare(#0(),#neg(z0)) -> #GT() #compare(#0(),#pos(z0)) -> #LT() #compare(#0(),#s(z0)) -> #LT() #compare(#neg(z0),#0()) -> #LT() #compare(#neg(z0),#neg(z1)) -> #compare(z1,z0) #compare(#neg(z0),#pos(z1)) -> #LT() #compare(#pos(z0),#0()) -> #GT() #compare(#pos(z0),#neg(z1)) -> #GT() #compare(#pos(z0),#pos(z1)) -> #compare(z0,z1) #compare(#s(z0),#0()) -> #GT() #compare(#s(z0),#s(z1)) -> #compare(z0,z1) #less(z0,z1) -> #cklt(#compare(z0,z1)) append(z0,z1) -> append#1(z0,z1) append#1(::(z0,z1),z2) -> ::(z0,append(z1,z2)) append#1(nil(),z0) -> z0 flatten(z0) -> flatten#1(z0) flatten#1(leaf()) -> nil() flatten#1(node(z0,z1,z2)) -> append(z0,append(flatten(z1),flatten(z2))) flattensort(z0) -> insertionsort(flatten(z0)) insert(z0,z1) -> insert#1(z1,z0) insert#1(::(z0,z1),z2) -> insert#2(#less(z0,z2),z2,z0,z1) insert#1(nil(),z0) -> ::(z0,nil()) insert#2(#false(),z0,z1,z2) -> ::(z0,::(z1,z2)) insert#2(#true(),z0,z1,z2) -> ::(z1,insert(z0,z2)) insertionsort(z0) -> insertionsort#1(z0) insertionsort#1(::(z0,z1)) -> insert(z0,insertionsort(z1)) insertionsort#1(nil()) -> nil() - Signature: {#CKLT/1,#COMPARE/2,#LESS/2,#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,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,::/2,c/0,c1/0,c10/0,c11/0 ,c12/1,c13/0,c14/1,c15/2,c16/1,c17/1,c18/0,c19/1,c2/0,c20/0,c21/3,c22/3,c23/2,c24/1,c25/2,c26/0,c27/0,c28/1 ,c29/1,c3/0,c30/2,c31/0,c4/0,c5/0,c6/0,c7/0,c8/1,c9/0,leaf/0,nil/0,node/3} - Obligation: innermost runtime complexity wrt. defined symbols {#CKLT,#COMPARE,#LESS,#cklt,#compare,#less,APPEND,APPEND#1 ,FLATTEN,FLATTEN#1,FLATTENSORT,INSERT,INSERT#1,INSERT#2,INSERTIONSORT,INSERTIONSORT#1,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,::,c,c1,c10,c11,c12,c13,c14,c15,c16,c17,c18,c19,c2,c20,c21,c22,c23 ,c24,c25,c26,c27,c28,c29,c3,c30,c31,c4,c5,c6,c7,c8,c9,leaf,nil,node} + Applied Processor: DependencyPairs {dpKind_ = DT} + Details: We add the following dependency tuples: Strict DPs #LESS#(z0,z1) -> c_1(#CKLT#(#compare(z0,z1)),#compare#(z0,z1),#COMPARE#(z0,z1)) APPEND#(z0,z1) -> c_2(APPEND#1#(z0,z1)) APPEND#1#(::(z0,z1),z2) -> c_3(APPEND#(z1,z2)) APPEND#1#(nil(),z0) -> c_4() FLATTEN#(z0) -> c_5(FLATTEN#1#(z0)) FLATTEN#1#(leaf()) -> c_6() FLATTEN#1#(node(z0,z1,z2)) -> c_7(APPEND#(z0,append(flatten(z1),flatten(z2))) ,append#(flatten(z1),flatten(z2)) ,flatten#(z1) ,flatten#(z2) ,APPEND#(flatten(z1),flatten(z2)) ,flatten#(z1) ,flatten#(z2) ,FLATTEN#(z1)) FLATTEN#1#(node(z0,z1,z2)) -> c_8(APPEND#(z0,append(flatten(z1),flatten(z2))) ,append#(flatten(z1),flatten(z2)) ,flatten#(z1) ,flatten#(z2) ,APPEND#(flatten(z1),flatten(z2)) ,flatten#(z1) ,flatten#(z2) ,FLATTEN#(z2)) FLATTENSORT#(z0) -> c_9(INSERTIONSORT#(flatten(z0)),flatten#(z0),FLATTEN#(z0)) INSERT#(z0,z1) -> c_10(INSERT#1#(z1,z0)) INSERT#1#(::(z0,z1),z2) -> c_11(INSERT#2#(#less(z0,z2),z2,z0,z1),#less#(z0,z2),#LESS#(z0,z2)) INSERT#1#(nil(),z0) -> c_12() INSERT#2#(#false(),z0,z1,z2) -> c_13() INSERT#2#(#true(),z0,z1,z2) -> c_14(INSERT#(z0,z2)) INSERTIONSORT#(z0) -> c_15(INSERTIONSORT#1#(z0)) INSERTIONSORT#1#(::(z0,z1)) -> c_16(INSERT#(z0,insertionsort(z1)),insertionsort#(z1),INSERTIONSORT#(z1)) INSERTIONSORT#1#(nil()) -> c_17() Weak DPs #CKLT#(#EQ()) -> c_18() #CKLT#(#GT()) -> c_19() #CKLT#(#LT()) -> c_20() #COMPARE#(#0(),#0()) -> c_21() #COMPARE#(#0(),#neg(z0)) -> c_22() #COMPARE#(#0(),#pos(z0)) -> c_23() #COMPARE#(#0(),#s(z0)) -> c_24() #COMPARE#(#neg(z0),#0()) -> c_25() #COMPARE#(#neg(z0),#neg(z1)) -> c_26(#COMPARE#(z1,z0)) #COMPARE#(#neg(z0),#pos(z1)) -> c_27() #COMPARE#(#pos(z0),#0()) -> c_28() #COMPARE#(#pos(z0),#neg(z1)) -> c_29() #COMPARE#(#pos(z0),#pos(z1)) -> c_30(#COMPARE#(z0,z1)) #COMPARE#(#s(z0),#0()) -> c_31() #COMPARE#(#s(z0),#s(z1)) -> c_32(#COMPARE#(z0,z1)) #cklt#(#EQ()) -> c_33() #cklt#(#GT()) -> c_34() #cklt#(#LT()) -> c_35() #compare#(#0(),#0()) -> c_36() #compare#(#0(),#neg(z0)) -> c_37() #compare#(#0(),#pos(z0)) -> c_38() #compare#(#0(),#s(z0)) -> c_39() #compare#(#neg(z0),#0()) -> c_40() #compare#(#neg(z0),#neg(z1)) -> c_41(#compare#(z1,z0)) #compare#(#neg(z0),#pos(z1)) -> c_42() #compare#(#pos(z0),#0()) -> c_43() #compare#(#pos(z0),#neg(z1)) -> c_44() #compare#(#pos(z0),#pos(z1)) -> c_45(#compare#(z0,z1)) #compare#(#s(z0),#0()) -> c_46() #compare#(#s(z0),#s(z1)) -> c_47(#compare#(z0,z1)) #less#(z0,z1) -> c_48(#cklt#(#compare(z0,z1)),#compare#(z0,z1)) append#(z0,z1) -> c_49(append#1#(z0,z1)) append#1#(::(z0,z1),z2) -> c_50(append#(z1,z2)) append#1#(nil(),z0) -> c_51() flatten#(z0) -> c_52(flatten#1#(z0)) flatten#1#(leaf()) -> c_53() flatten#1#(node(z0,z1,z2)) -> c_54(append#(z0,append(flatten(z1),flatten(z2))) ,append#(flatten(z1),flatten(z2)) ,flatten#(z1) ,flatten#(z2)) flattensort#(z0) -> c_55(insertionsort#(flatten(z0)),flatten#(z0)) insert#(z0,z1) -> c_56(insert#1#(z1,z0)) insert#1#(::(z0,z1),z2) -> c_57(insert#2#(#less(z0,z2),z2,z0,z1),#less#(z0,z2)) insert#1#(nil(),z0) -> c_58() insert#2#(#false(),z0,z1,z2) -> c_59() insert#2#(#true(),z0,z1,z2) -> c_60(insert#(z0,z2)) insertionsort#(z0) -> c_61(insertionsort#1#(z0)) insertionsort#1#(::(z0,z1)) -> c_62(insert#(z0,insertionsort(z1)),insertionsort#(z1)) insertionsort#1#(nil()) -> c_63() and mark the set of starting terms. * Step 3: PredecessorEstimation. WORST_CASE(?,O(n^2)) + Considered Problem: - Strict DPs: #LESS#(z0,z1) -> c_1(#CKLT#(#compare(z0,z1)),#compare#(z0,z1),#COMPARE#(z0,z1)) APPEND#(z0,z1) -> c_2(APPEND#1#(z0,z1)) APPEND#1#(::(z0,z1),z2) -> c_3(APPEND#(z1,z2)) APPEND#1#(nil(),z0) -> c_4() FLATTEN#(z0) -> c_5(FLATTEN#1#(z0)) FLATTEN#1#(leaf()) -> c_6() FLATTEN#1#(node(z0,z1,z2)) -> c_7(APPEND#(z0,append(flatten(z1),flatten(z2))) ,append#(flatten(z1),flatten(z2)) ,flatten#(z1) ,flatten#(z2) ,APPEND#(flatten(z1),flatten(z2)) ,flatten#(z1) ,flatten#(z2) ,FLATTEN#(z1)) FLATTEN#1#(node(z0,z1,z2)) -> c_8(APPEND#(z0,append(flatten(z1),flatten(z2))) ,append#(flatten(z1),flatten(z2)) ,flatten#(z1) ,flatten#(z2) ,APPEND#(flatten(z1),flatten(z2)) ,flatten#(z1) ,flatten#(z2) ,FLATTEN#(z2)) FLATTENSORT#(z0) -> c_9(INSERTIONSORT#(flatten(z0)),flatten#(z0),FLATTEN#(z0)) INSERT#(z0,z1) -> c_10(INSERT#1#(z1,z0)) INSERT#1#(::(z0,z1),z2) -> c_11(INSERT#2#(#less(z0,z2),z2,z0,z1),#less#(z0,z2),#LESS#(z0,z2)) INSERT#1#(nil(),z0) -> c_12() INSERT#2#(#false(),z0,z1,z2) -> c_13() INSERT#2#(#true(),z0,z1,z2) -> c_14(INSERT#(z0,z2)) INSERTIONSORT#(z0) -> c_15(INSERTIONSORT#1#(z0)) INSERTIONSORT#1#(::(z0,z1)) -> c_16(INSERT#(z0,insertionsort(z1)),insertionsort#(z1),INSERTIONSORT#(z1)) INSERTIONSORT#1#(nil()) -> c_17() - Weak DPs: #CKLT#(#EQ()) -> c_18() #CKLT#(#GT()) -> c_19() #CKLT#(#LT()) -> c_20() #COMPARE#(#0(),#0()) -> c_21() #COMPARE#(#0(),#neg(z0)) -> c_22() #COMPARE#(#0(),#pos(z0)) -> c_23() #COMPARE#(#0(),#s(z0)) -> c_24() #COMPARE#(#neg(z0),#0()) -> c_25() #COMPARE#(#neg(z0),#neg(z1)) -> c_26(#COMPARE#(z1,z0)) #COMPARE#(#neg(z0),#pos(z1)) -> c_27() #COMPARE#(#pos(z0),#0()) -> c_28() #COMPARE#(#pos(z0),#neg(z1)) -> c_29() #COMPARE#(#pos(z0),#pos(z1)) -> c_30(#COMPARE#(z0,z1)) #COMPARE#(#s(z0),#0()) -> c_31() #COMPARE#(#s(z0),#s(z1)) -> c_32(#COMPARE#(z0,z1)) #cklt#(#EQ()) -> c_33() #cklt#(#GT()) -> c_34() #cklt#(#LT()) -> c_35() #compare#(#0(),#0()) -> c_36() #compare#(#0(),#neg(z0)) -> c_37() #compare#(#0(),#pos(z0)) -> c_38() #compare#(#0(),#s(z0)) -> c_39() #compare#(#neg(z0),#0()) -> c_40() #compare#(#neg(z0),#neg(z1)) -> c_41(#compare#(z1,z0)) #compare#(#neg(z0),#pos(z1)) -> c_42() #compare#(#pos(z0),#0()) -> c_43() #compare#(#pos(z0),#neg(z1)) -> c_44() #compare#(#pos(z0),#pos(z1)) -> c_45(#compare#(z0,z1)) #compare#(#s(z0),#0()) -> c_46() #compare#(#s(z0),#s(z1)) -> c_47(#compare#(z0,z1)) #less#(z0,z1) -> c_48(#cklt#(#compare(z0,z1)),#compare#(z0,z1)) append#(z0,z1) -> c_49(append#1#(z0,z1)) append#1#(::(z0,z1),z2) -> c_50(append#(z1,z2)) append#1#(nil(),z0) -> c_51() flatten#(z0) -> c_52(flatten#1#(z0)) flatten#1#(leaf()) -> c_53() flatten#1#(node(z0,z1,z2)) -> c_54(append#(z0,append(flatten(z1),flatten(z2))) ,append#(flatten(z1),flatten(z2)) ,flatten#(z1) ,flatten#(z2)) flattensort#(z0) -> c_55(insertionsort#(flatten(z0)),flatten#(z0)) insert#(z0,z1) -> c_56(insert#1#(z1,z0)) insert#1#(::(z0,z1),z2) -> c_57(insert#2#(#less(z0,z2),z2,z0,z1),#less#(z0,z2)) insert#1#(nil(),z0) -> c_58() insert#2#(#false(),z0,z1,z2) -> c_59() insert#2#(#true(),z0,z1,z2) -> c_60(insert#(z0,z2)) insertionsort#(z0) -> c_61(insertionsort#1#(z0)) insertionsort#1#(::(z0,z1)) -> c_62(insert#(z0,insertionsort(z1)),insertionsort#(z1)) insertionsort#1#(nil()) -> c_63() - Weak TRS: #CKLT(#EQ()) -> c() #CKLT(#GT()) -> c1() #CKLT(#LT()) -> c2() #COMPARE(#0(),#0()) -> c3() #COMPARE(#0(),#neg(z0)) -> c4() #COMPARE(#0(),#pos(z0)) -> c5() #COMPARE(#0(),#s(z0)) -> c6() #COMPARE(#neg(z0),#0()) -> c7() #COMPARE(#neg(z0),#neg(z1)) -> c8(#COMPARE(z1,z0)) #COMPARE(#neg(z0),#pos(z1)) -> c9() #COMPARE(#pos(z0),#0()) -> c10() #COMPARE(#pos(z0),#neg(z1)) -> c11() #COMPARE(#pos(z0),#pos(z1)) -> c12(#COMPARE(z0,z1)) #COMPARE(#s(z0),#0()) -> c13() #COMPARE(#s(z0),#s(z1)) -> c14(#COMPARE(z0,z1)) #LESS(z0,z1) -> c15(#CKLT(#compare(z0,z1)),#COMPARE(z0,z1)) #cklt(#EQ()) -> #false() #cklt(#GT()) -> #false() #cklt(#LT()) -> #true() #compare(#0(),#0()) -> #EQ() #compare(#0(),#neg(z0)) -> #GT() #compare(#0(),#pos(z0)) -> #LT() #compare(#0(),#s(z0)) -> #LT() #compare(#neg(z0),#0()) -> #LT() #compare(#neg(z0),#neg(z1)) -> #compare(z1,z0) #compare(#neg(z0),#pos(z1)) -> #LT() #compare(#pos(z0),#0()) -> #GT() #compare(#pos(z0),#neg(z1)) -> #GT() #compare(#pos(z0),#pos(z1)) -> #compare(z0,z1) #compare(#s(z0),#0()) -> #GT() #compare(#s(z0),#s(z1)) -> #compare(z0,z1) #less(z0,z1) -> #cklt(#compare(z0,z1)) APPEND(z0,z1) -> c16(APPEND#1(z0,z1)) APPEND#1(::(z0,z1),z2) -> c17(APPEND(z1,z2)) APPEND#1(nil(),z0) -> c18() FLATTEN(z0) -> c19(FLATTEN#1(z0)) FLATTEN#1(leaf()) -> c20() FLATTEN#1(node(z0,z1,z2)) -> c21(APPEND(z0,append(flatten(z1),flatten(z2))) ,APPEND(flatten(z1),flatten(z2)) ,FLATTEN(z1)) FLATTEN#1(node(z0,z1,z2)) -> c22(APPEND(z0,append(flatten(z1),flatten(z2))) ,APPEND(flatten(z1),flatten(z2)) ,FLATTEN(z2)) FLATTENSORT(z0) -> c23(INSERTIONSORT(flatten(z0)),FLATTEN(z0)) INSERT(z0,z1) -> c24(INSERT#1(z1,z0)) INSERT#1(::(z0,z1),z2) -> c25(INSERT#2(#less(z0,z2),z2,z0,z1),#LESS(z0,z2)) INSERT#1(nil(),z0) -> c26() INSERT#2(#false(),z0,z1,z2) -> c27() INSERT#2(#true(),z0,z1,z2) -> c28(INSERT(z0,z2)) INSERTIONSORT(z0) -> c29(INSERTIONSORT#1(z0)) INSERTIONSORT#1(::(z0,z1)) -> c30(INSERT(z0,insertionsort(z1)),INSERTIONSORT(z1)) INSERTIONSORT#1(nil()) -> c31() append(z0,z1) -> append#1(z0,z1) append#1(::(z0,z1),z2) -> ::(z0,append(z1,z2)) append#1(nil(),z0) -> z0 flatten(z0) -> flatten#1(z0) flatten#1(leaf()) -> nil() flatten#1(node(z0,z1,z2)) -> append(z0,append(flatten(z1),flatten(z2))) flattensort(z0) -> insertionsort(flatten(z0)) insert(z0,z1) -> insert#1(z1,z0) insert#1(::(z0,z1),z2) -> insert#2(#less(z0,z2),z2,z0,z1) insert#1(nil(),z0) -> ::(z0,nil()) insert#2(#false(),z0,z1,z2) -> ::(z0,::(z1,z2)) insert#2(#true(),z0,z1,z2) -> ::(z1,insert(z0,z2)) insertionsort(z0) -> insertionsort#1(z0) insertionsort#1(::(z0,z1)) -> insert(z0,insertionsort(z1)) insertionsort#1(nil()) -> nil() - Signature: {#CKLT/1,#COMPARE/2,#LESS/2,#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,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,#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,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,::/2,c/0,c1/0,c10/0,c11/0 ,c12/1,c13/0,c14/1,c15/2,c16/1,c17/1,c18/0,c19/1,c2/0,c20/0,c21/3,c22/3,c23/2,c24/1,c25/2,c26/0,c27/0,c28/1 ,c29/1,c3/0,c30/2,c31/0,c4/0,c5/0,c6/0,c7/0,c8/1,c9/0,leaf/0,nil/0,node/3,c_1/3,c_2/1,c_3/1,c_4/0,c_5/1 ,c_6/0,c_7/8,c_8/8,c_9/3,c_10/1,c_11/3,c_12/0,c_13/0,c_14/1,c_15/1,c_16/3,c_17/0,c_18/0,c_19/0,c_20/0,c_21/0 ,c_22/0,c_23/0,c_24/0,c_25/0,c_26/1,c_27/0,c_28/0,c_29/0,c_30/1,c_31/0,c_32/1,c_33/0,c_34/0,c_35/0,c_36/0 ,c_37/0,c_38/0,c_39/0,c_40/0,c_41/1,c_42/0,c_43/0,c_44/0,c_45/1,c_46/0,c_47/1,c_48/2,c_49/1,c_50/1,c_51/0 ,c_52/1,c_53/0,c_54/4,c_55/2,c_56/1,c_57/2,c_58/0,c_59/0,c_60/1,c_61/1,c_62/2,c_63/0} - Obligation: innermost runtime complexity wrt. defined symbols {#CKLT#,#COMPARE#,#LESS#,#cklt#,#compare#,#less#,APPEND# ,APPEND#1#,FLATTEN#,FLATTEN#1#,FLATTENSORT#,INSERT#,INSERT#1#,INSERT#2#,INSERTIONSORT#,INSERTIONSORT#1# ,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,::,c,c1,c10,c11,c12,c13,c14 ,c15,c16,c17,c18,c19,c2,c20,c21,c22,c23,c24,c25,c26,c27,c28,c29,c3,c30,c31,c4,c5,c6,c7,c8,c9,leaf,nil,node} + Applied Processor: PredecessorEstimation {onSelection = all simple predecessor estimation selector} + Details: We estimate the number of application of {1,4,6,12,13,17} by application of Pre({1,4,6,12,13,17}) = {2,5,10,11,15}. Here rules are labelled as follows: 1: #LESS#(z0,z1) -> c_1(#CKLT#(#compare(z0,z1)),#compare#(z0,z1),#COMPARE#(z0,z1)) 2: APPEND#(z0,z1) -> c_2(APPEND#1#(z0,z1)) 3: APPEND#1#(::(z0,z1),z2) -> c_3(APPEND#(z1,z2)) 4: APPEND#1#(nil(),z0) -> c_4() 5: FLATTEN#(z0) -> c_5(FLATTEN#1#(z0)) 6: FLATTEN#1#(leaf()) -> c_6() 7: FLATTEN#1#(node(z0,z1,z2)) -> c_7(APPEND#(z0,append(flatten(z1),flatten(z2))) ,append#(flatten(z1),flatten(z2)) ,flatten#(z1) ,flatten#(z2) ,APPEND#(flatten(z1),flatten(z2)) ,flatten#(z1) ,flatten#(z2) ,FLATTEN#(z1)) 8: FLATTEN#1#(node(z0,z1,z2)) -> c_8(APPEND#(z0,append(flatten(z1),flatten(z2))) ,append#(flatten(z1),flatten(z2)) ,flatten#(z1) ,flatten#(z2) ,APPEND#(flatten(z1),flatten(z2)) ,flatten#(z1) ,flatten#(z2) ,FLATTEN#(z2)) 9: FLATTENSORT#(z0) -> c_9(INSERTIONSORT#(flatten(z0)),flatten#(z0),FLATTEN#(z0)) 10: INSERT#(z0,z1) -> c_10(INSERT#1#(z1,z0)) 11: INSERT#1#(::(z0,z1),z2) -> c_11(INSERT#2#(#less(z0,z2),z2,z0,z1),#less#(z0,z2),#LESS#(z0,z2)) 12: INSERT#1#(nil(),z0) -> c_12() 13: INSERT#2#(#false(),z0,z1,z2) -> c_13() 14: INSERT#2#(#true(),z0,z1,z2) -> c_14(INSERT#(z0,z2)) 15: INSERTIONSORT#(z0) -> c_15(INSERTIONSORT#1#(z0)) 16: INSERTIONSORT#1#(::(z0,z1)) -> c_16(INSERT#(z0,insertionsort(z1)),insertionsort#(z1),INSERTIONSORT#(z1)) 17: INSERTIONSORT#1#(nil()) -> c_17() 18: #CKLT#(#EQ()) -> c_18() 19: #CKLT#(#GT()) -> c_19() 20: #CKLT#(#LT()) -> c_20() 21: #COMPARE#(#0(),#0()) -> c_21() 22: #COMPARE#(#0(),#neg(z0)) -> c_22() 23: #COMPARE#(#0(),#pos(z0)) -> c_23() 24: #COMPARE#(#0(),#s(z0)) -> c_24() 25: #COMPARE#(#neg(z0),#0()) -> c_25() 26: #COMPARE#(#neg(z0),#neg(z1)) -> c_26(#COMPARE#(z1,z0)) 27: #COMPARE#(#neg(z0),#pos(z1)) -> c_27() 28: #COMPARE#(#pos(z0),#0()) -> c_28() 29: #COMPARE#(#pos(z0),#neg(z1)) -> c_29() 30: #COMPARE#(#pos(z0),#pos(z1)) -> c_30(#COMPARE#(z0,z1)) 31: #COMPARE#(#s(z0),#0()) -> c_31() 32: #COMPARE#(#s(z0),#s(z1)) -> c_32(#COMPARE#(z0,z1)) 33: #cklt#(#EQ()) -> c_33() 34: #cklt#(#GT()) -> c_34() 35: #cklt#(#LT()) -> c_35() 36: #compare#(#0(),#0()) -> c_36() 37: #compare#(#0(),#neg(z0)) -> c_37() 38: #compare#(#0(),#pos(z0)) -> c_38() 39: #compare#(#0(),#s(z0)) -> c_39() 40: #compare#(#neg(z0),#0()) -> c_40() 41: #compare#(#neg(z0),#neg(z1)) -> c_41(#compare#(z1,z0)) 42: #compare#(#neg(z0),#pos(z1)) -> c_42() 43: #compare#(#pos(z0),#0()) -> c_43() 44: #compare#(#pos(z0),#neg(z1)) -> c_44() 45: #compare#(#pos(z0),#pos(z1)) -> c_45(#compare#(z0,z1)) 46: #compare#(#s(z0),#0()) -> c_46() 47: #compare#(#s(z0),#s(z1)) -> c_47(#compare#(z0,z1)) 48: #less#(z0,z1) -> c_48(#cklt#(#compare(z0,z1)),#compare#(z0,z1)) 49: append#(z0,z1) -> c_49(append#1#(z0,z1)) 50: append#1#(::(z0,z1),z2) -> c_50(append#(z1,z2)) 51: append#1#(nil(),z0) -> c_51() 52: flatten#(z0) -> c_52(flatten#1#(z0)) 53: flatten#1#(leaf()) -> c_53() 54: flatten#1#(node(z0,z1,z2)) -> c_54(append#(z0,append(flatten(z1),flatten(z2))) ,append#(flatten(z1),flatten(z2)) ,flatten#(z1) ,flatten#(z2)) 55: flattensort#(z0) -> c_55(insertionsort#(flatten(z0)),flatten#(z0)) 56: insert#(z0,z1) -> c_56(insert#1#(z1,z0)) 57: insert#1#(::(z0,z1),z2) -> c_57(insert#2#(#less(z0,z2),z2,z0,z1),#less#(z0,z2)) 58: insert#1#(nil(),z0) -> c_58() 59: insert#2#(#false(),z0,z1,z2) -> c_59() 60: insert#2#(#true(),z0,z1,z2) -> c_60(insert#(z0,z2)) 61: insertionsort#(z0) -> c_61(insertionsort#1#(z0)) 62: insertionsort#1#(::(z0,z1)) -> c_62(insert#(z0,insertionsort(z1)),insertionsort#(z1)) 63: insertionsort#1#(nil()) -> c_63() * Step 4: RemoveWeakSuffixes. WORST_CASE(?,O(n^2)) + Considered Problem: - Strict DPs: APPEND#(z0,z1) -> c_2(APPEND#1#(z0,z1)) APPEND#1#(::(z0,z1),z2) -> c_3(APPEND#(z1,z2)) FLATTEN#(z0) -> c_5(FLATTEN#1#(z0)) FLATTEN#1#(node(z0,z1,z2)) -> c_7(APPEND#(z0,append(flatten(z1),flatten(z2))) ,append#(flatten(z1),flatten(z2)) ,flatten#(z1) ,flatten#(z2) ,APPEND#(flatten(z1),flatten(z2)) ,flatten#(z1) ,flatten#(z2) ,FLATTEN#(z1)) FLATTEN#1#(node(z0,z1,z2)) -> c_8(APPEND#(z0,append(flatten(z1),flatten(z2))) ,append#(flatten(z1),flatten(z2)) ,flatten#(z1) ,flatten#(z2) ,APPEND#(flatten(z1),flatten(z2)) ,flatten#(z1) ,flatten#(z2) ,FLATTEN#(z2)) FLATTENSORT#(z0) -> c_9(INSERTIONSORT#(flatten(z0)),flatten#(z0),FLATTEN#(z0)) INSERT#(z0,z1) -> c_10(INSERT#1#(z1,z0)) INSERT#1#(::(z0,z1),z2) -> c_11(INSERT#2#(#less(z0,z2),z2,z0,z1),#less#(z0,z2),#LESS#(z0,z2)) INSERT#2#(#true(),z0,z1,z2) -> c_14(INSERT#(z0,z2)) INSERTIONSORT#(z0) -> c_15(INSERTIONSORT#1#(z0)) INSERTIONSORT#1#(::(z0,z1)) -> c_16(INSERT#(z0,insertionsort(z1)),insertionsort#(z1),INSERTIONSORT#(z1)) - Weak DPs: #CKLT#(#EQ()) -> c_18() #CKLT#(#GT()) -> c_19() #CKLT#(#LT()) -> c_20() #COMPARE#(#0(),#0()) -> c_21() #COMPARE#(#0(),#neg(z0)) -> c_22() #COMPARE#(#0(),#pos(z0)) -> c_23() #COMPARE#(#0(),#s(z0)) -> c_24() #COMPARE#(#neg(z0),#0()) -> c_25() #COMPARE#(#neg(z0),#neg(z1)) -> c_26(#COMPARE#(z1,z0)) #COMPARE#(#neg(z0),#pos(z1)) -> c_27() #COMPARE#(#pos(z0),#0()) -> c_28() #COMPARE#(#pos(z0),#neg(z1)) -> c_29() #COMPARE#(#pos(z0),#pos(z1)) -> c_30(#COMPARE#(z0,z1)) #COMPARE#(#s(z0),#0()) -> c_31() #COMPARE#(#s(z0),#s(z1)) -> c_32(#COMPARE#(z0,z1)) #LESS#(z0,z1) -> c_1(#CKLT#(#compare(z0,z1)),#compare#(z0,z1),#COMPARE#(z0,z1)) #cklt#(#EQ()) -> c_33() #cklt#(#GT()) -> c_34() #cklt#(#LT()) -> c_35() #compare#(#0(),#0()) -> c_36() #compare#(#0(),#neg(z0)) -> c_37() #compare#(#0(),#pos(z0)) -> c_38() #compare#(#0(),#s(z0)) -> c_39() #compare#(#neg(z0),#0()) -> c_40() #compare#(#neg(z0),#neg(z1)) -> c_41(#compare#(z1,z0)) #compare#(#neg(z0),#pos(z1)) -> c_42() #compare#(#pos(z0),#0()) -> c_43() #compare#(#pos(z0),#neg(z1)) -> c_44() #compare#(#pos(z0),#pos(z1)) -> c_45(#compare#(z0,z1)) #compare#(#s(z0),#0()) -> c_46() #compare#(#s(z0),#s(z1)) -> c_47(#compare#(z0,z1)) #less#(z0,z1) -> c_48(#cklt#(#compare(z0,z1)),#compare#(z0,z1)) APPEND#1#(nil(),z0) -> c_4() FLATTEN#1#(leaf()) -> c_6() INSERT#1#(nil(),z0) -> c_12() INSERT#2#(#false(),z0,z1,z2) -> c_13() INSERTIONSORT#1#(nil()) -> c_17() append#(z0,z1) -> c_49(append#1#(z0,z1)) append#1#(::(z0,z1),z2) -> c_50(append#(z1,z2)) append#1#(nil(),z0) -> c_51() flatten#(z0) -> c_52(flatten#1#(z0)) flatten#1#(leaf()) -> c_53() flatten#1#(node(z0,z1,z2)) -> c_54(append#(z0,append(flatten(z1),flatten(z2))) ,append#(flatten(z1),flatten(z2)) ,flatten#(z1) ,flatten#(z2)) flattensort#(z0) -> c_55(insertionsort#(flatten(z0)),flatten#(z0)) insert#(z0,z1) -> c_56(insert#1#(z1,z0)) insert#1#(::(z0,z1),z2) -> c_57(insert#2#(#less(z0,z2),z2,z0,z1),#less#(z0,z2)) insert#1#(nil(),z0) -> c_58() insert#2#(#false(),z0,z1,z2) -> c_59() insert#2#(#true(),z0,z1,z2) -> c_60(insert#(z0,z2)) insertionsort#(z0) -> c_61(insertionsort#1#(z0)) insertionsort#1#(::(z0,z1)) -> c_62(insert#(z0,insertionsort(z1)),insertionsort#(z1)) insertionsort#1#(nil()) -> c_63() - Weak TRS: #CKLT(#EQ()) -> c() #CKLT(#GT()) -> c1() #CKLT(#LT()) -> c2() #COMPARE(#0(),#0()) -> c3() #COMPARE(#0(),#neg(z0)) -> c4() #COMPARE(#0(),#pos(z0)) -> c5() #COMPARE(#0(),#s(z0)) -> c6() #COMPARE(#neg(z0),#0()) -> c7() #COMPARE(#neg(z0),#neg(z1)) -> c8(#COMPARE(z1,z0)) #COMPARE(#neg(z0),#pos(z1)) -> c9() #COMPARE(#pos(z0),#0()) -> c10() #COMPARE(#pos(z0),#neg(z1)) -> c11() #COMPARE(#pos(z0),#pos(z1)) -> c12(#COMPARE(z0,z1)) #COMPARE(#s(z0),#0()) -> c13() #COMPARE(#s(z0),#s(z1)) -> c14(#COMPARE(z0,z1)) #LESS(z0,z1) -> c15(#CKLT(#compare(z0,z1)),#COMPARE(z0,z1)) #cklt(#EQ()) -> #false() #cklt(#GT()) -> #false() #cklt(#LT()) -> #true() #compare(#0(),#0()) -> #EQ() #compare(#0(),#neg(z0)) -> #GT() #compare(#0(),#pos(z0)) -> #LT() #compare(#0(),#s(z0)) -> #LT() #compare(#neg(z0),#0()) -> #LT() #compare(#neg(z0),#neg(z1)) -> #compare(z1,z0) #compare(#neg(z0),#pos(z1)) -> #LT() #compare(#pos(z0),#0()) -> #GT() #compare(#pos(z0),#neg(z1)) -> #GT() #compare(#pos(z0),#pos(z1)) -> #compare(z0,z1) #compare(#s(z0),#0()) -> #GT() #compare(#s(z0),#s(z1)) -> #compare(z0,z1) #less(z0,z1) -> #cklt(#compare(z0,z1)) APPEND(z0,z1) -> c16(APPEND#1(z0,z1)) APPEND#1(::(z0,z1),z2) -> c17(APPEND(z1,z2)) APPEND#1(nil(),z0) -> c18() FLATTEN(z0) -> c19(FLATTEN#1(z0)) FLATTEN#1(leaf()) -> c20() FLATTEN#1(node(z0,z1,z2)) -> c21(APPEND(z0,append(flatten(z1),flatten(z2))) ,APPEND(flatten(z1),flatten(z2)) ,FLATTEN(z1)) FLATTEN#1(node(z0,z1,z2)) -> c22(APPEND(z0,append(flatten(z1),flatten(z2))) ,APPEND(flatten(z1),flatten(z2)) ,FLATTEN(z2)) FLATTENSORT(z0) -> c23(INSERTIONSORT(flatten(z0)),FLATTEN(z0)) INSERT(z0,z1) -> c24(INSERT#1(z1,z0)) INSERT#1(::(z0,z1),z2) -> c25(INSERT#2(#less(z0,z2),z2,z0,z1),#LESS(z0,z2)) INSERT#1(nil(),z0) -> c26() INSERT#2(#false(),z0,z1,z2) -> c27() INSERT#2(#true(),z0,z1,z2) -> c28(INSERT(z0,z2)) INSERTIONSORT(z0) -> c29(INSERTIONSORT#1(z0)) INSERTIONSORT#1(::(z0,z1)) -> c30(INSERT(z0,insertionsort(z1)),INSERTIONSORT(z1)) INSERTIONSORT#1(nil()) -> c31() append(z0,z1) -> append#1(z0,z1) append#1(::(z0,z1),z2) -> ::(z0,append(z1,z2)) append#1(nil(),z0) -> z0 flatten(z0) -> flatten#1(z0) flatten#1(leaf()) -> nil() flatten#1(node(z0,z1,z2)) -> append(z0,append(flatten(z1),flatten(z2))) flattensort(z0) -> insertionsort(flatten(z0)) insert(z0,z1) -> insert#1(z1,z0) insert#1(::(z0,z1),z2) -> insert#2(#less(z0,z2),z2,z0,z1) insert#1(nil(),z0) -> ::(z0,nil()) insert#2(#false(),z0,z1,z2) -> ::(z0,::(z1,z2)) insert#2(#true(),z0,z1,z2) -> ::(z1,insert(z0,z2)) insertionsort(z0) -> insertionsort#1(z0) insertionsort#1(::(z0,z1)) -> insert(z0,insertionsort(z1)) insertionsort#1(nil()) -> nil() - Signature: {#CKLT/1,#COMPARE/2,#LESS/2,#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,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,#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,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,::/2,c/0,c1/0,c10/0,c11/0 ,c12/1,c13/0,c14/1,c15/2,c16/1,c17/1,c18/0,c19/1,c2/0,c20/0,c21/3,c22/3,c23/2,c24/1,c25/2,c26/0,c27/0,c28/1 ,c29/1,c3/0,c30/2,c31/0,c4/0,c5/0,c6/0,c7/0,c8/1,c9/0,leaf/0,nil/0,node/3,c_1/3,c_2/1,c_3/1,c_4/0,c_5/1 ,c_6/0,c_7/8,c_8/8,c_9/3,c_10/1,c_11/3,c_12/0,c_13/0,c_14/1,c_15/1,c_16/3,c_17/0,c_18/0,c_19/0,c_20/0,c_21/0 ,c_22/0,c_23/0,c_24/0,c_25/0,c_26/1,c_27/0,c_28/0,c_29/0,c_30/1,c_31/0,c_32/1,c_33/0,c_34/0,c_35/0,c_36/0 ,c_37/0,c_38/0,c_39/0,c_40/0,c_41/1,c_42/0,c_43/0,c_44/0,c_45/1,c_46/0,c_47/1,c_48/2,c_49/1,c_50/1,c_51/0 ,c_52/1,c_53/0,c_54/4,c_55/2,c_56/1,c_57/2,c_58/0,c_59/0,c_60/1,c_61/1,c_62/2,c_63/0} - Obligation: innermost runtime complexity wrt. defined symbols {#CKLT#,#COMPARE#,#LESS#,#cklt#,#compare#,#less#,APPEND# ,APPEND#1#,FLATTEN#,FLATTEN#1#,FLATTENSORT#,INSERT#,INSERT#1#,INSERT#2#,INSERTIONSORT#,INSERTIONSORT#1# ,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,::,c,c1,c10,c11,c12,c13,c14 ,c15,c16,c17,c18,c19,c2,c20,c21,c22,c23,c24,c25,c26,c27,c28,c29,c3,c30,c31,c4,c5,c6,c7,c8,c9,leaf,nil,node} + Applied Processor: RemoveWeakSuffixes + Details: Consider the dependency graph 1:S:APPEND#(z0,z1) -> c_2(APPEND#1#(z0,z1)) -->_1 APPEND#1#(::(z0,z1),z2) -> c_3(APPEND#(z1,z2)):2 -->_1 APPEND#1#(nil(),z0) -> c_4():44 2:S:APPEND#1#(::(z0,z1),z2) -> c_3(APPEND#(z1,z2)) -->_1 APPEND#(z0,z1) -> c_2(APPEND#1#(z0,z1)):1 3:S:FLATTEN#(z0) -> c_5(FLATTEN#1#(z0)) -->_1 FLATTEN#1#(node(z0,z1,z2)) -> c_8(APPEND#(z0,append(flatten(z1),flatten(z2))) ,append#(flatten(z1),flatten(z2)) ,flatten#(z1) ,flatten#(z2) ,APPEND#(flatten(z1),flatten(z2)) ,flatten#(z1) ,flatten#(z2) ,FLATTEN#(z2)):5 -->_1 FLATTEN#1#(node(z0,z1,z2)) -> c_7(APPEND#(z0,append(flatten(z1),flatten(z2))) ,append#(flatten(z1),flatten(z2)) ,flatten#(z1) ,flatten#(z2) ,APPEND#(flatten(z1),flatten(z2)) ,flatten#(z1) ,flatten#(z2) ,FLATTEN#(z1)):4 -->_1 FLATTEN#1#(leaf()) -> c_6():45 4:S:FLATTEN#1#(node(z0,z1,z2)) -> c_7(APPEND#(z0,append(flatten(z1),flatten(z2))) ,append#(flatten(z1),flatten(z2)) ,flatten#(z1) ,flatten#(z2) ,APPEND#(flatten(z1),flatten(z2)) ,flatten#(z1) ,flatten#(z2) ,FLATTEN#(z1)) -->_7 flatten#(z0) -> c_52(flatten#1#(z0)):52 -->_6 flatten#(z0) -> c_52(flatten#1#(z0)):52 -->_4 flatten#(z0) -> c_52(flatten#1#(z0)):52 -->_3 flatten#(z0) -> c_52(flatten#1#(z0)):52 -->_2 append#(z0,z1) -> c_49(append#1#(z0,z1)):49 -->_8 FLATTEN#(z0) -> c_5(FLATTEN#1#(z0)):3 -->_5 APPEND#(z0,z1) -> c_2(APPEND#1#(z0,z1)):1 -->_1 APPEND#(z0,z1) -> c_2(APPEND#1#(z0,z1)):1 5:S:FLATTEN#1#(node(z0,z1,z2)) -> c_8(APPEND#(z0,append(flatten(z1),flatten(z2))) ,append#(flatten(z1),flatten(z2)) ,flatten#(z1) ,flatten#(z2) ,APPEND#(flatten(z1),flatten(z2)) ,flatten#(z1) ,flatten#(z2) ,FLATTEN#(z2)) -->_7 flatten#(z0) -> c_52(flatten#1#(z0)):52 -->_6 flatten#(z0) -> c_52(flatten#1#(z0)):52 -->_4 flatten#(z0) -> c_52(flatten#1#(z0)):52 -->_3 flatten#(z0) -> c_52(flatten#1#(z0)):52 -->_2 append#(z0,z1) -> c_49(append#1#(z0,z1)):49 -->_8 FLATTEN#(z0) -> c_5(FLATTEN#1#(z0)):3 -->_5 APPEND#(z0,z1) -> c_2(APPEND#1#(z0,z1)):1 -->_1 APPEND#(z0,z1) -> c_2(APPEND#1#(z0,z1)):1 6:S:FLATTENSORT#(z0) -> c_9(INSERTIONSORT#(flatten(z0)),flatten#(z0),FLATTEN#(z0)) -->_2 flatten#(z0) -> c_52(flatten#1#(z0)):52 -->_1 INSERTIONSORT#(z0) -> c_15(INSERTIONSORT#1#(z0)):10 -->_3 FLATTEN#(z0) -> c_5(FLATTEN#1#(z0)):3 7:S:INSERT#(z0,z1) -> c_10(INSERT#1#(z1,z0)) -->_1 INSERT#1#(::(z0,z1),z2) -> c_11(INSERT#2#(#less(z0,z2),z2,z0,z1),#less#(z0,z2),#LESS#(z0,z2)):8 -->_1 INSERT#1#(nil(),z0) -> c_12():46 8:S:INSERT#1#(::(z0,z1),z2) -> c_11(INSERT#2#(#less(z0,z2),z2,z0,z1),#less#(z0,z2),#LESS#(z0,z2)) -->_2 #less#(z0,z1) -> c_48(#cklt#(#compare(z0,z1)),#compare#(z0,z1)):43 -->_3 #LESS#(z0,z1) -> c_1(#CKLT#(#compare(z0,z1)),#compare#(z0,z1),#COMPARE#(z0,z1)):27 -->_1 INSERT#2#(#true(),z0,z1,z2) -> c_14(INSERT#(z0,z2)):9 -->_1 INSERT#2#(#false(),z0,z1,z2) -> c_13():47 9:S:INSERT#2#(#true(),z0,z1,z2) -> c_14(INSERT#(z0,z2)) -->_1 INSERT#(z0,z1) -> c_10(INSERT#1#(z1,z0)):7 10:S:INSERTIONSORT#(z0) -> c_15(INSERTIONSORT#1#(z0)) -->_1 INSERTIONSORT#1#(::(z0,z1)) -> c_16(INSERT#(z0,insertionsort(z1)) ,insertionsort#(z1) ,INSERTIONSORT#(z1)):11 -->_1 INSERTIONSORT#1#(nil()) -> c_17():48 11:S:INSERTIONSORT#1#(::(z0,z1)) -> c_16(INSERT#(z0,insertionsort(z1)) ,insertionsort#(z1) ,INSERTIONSORT#(z1)) -->_2 insertionsort#(z0) -> c_61(insertionsort#1#(z0)):61 -->_3 INSERTIONSORT#(z0) -> c_15(INSERTIONSORT#1#(z0)):10 -->_1 INSERT#(z0,z1) -> c_10(INSERT#1#(z1,z0)):7 12:W:#CKLT#(#EQ()) -> c_18() 13:W:#CKLT#(#GT()) -> c_19() 14:W:#CKLT#(#LT()) -> c_20() 15:W:#COMPARE#(#0(),#0()) -> c_21() 16:W:#COMPARE#(#0(),#neg(z0)) -> c_22() 17:W:#COMPARE#(#0(),#pos(z0)) -> c_23() 18:W:#COMPARE#(#0(),#s(z0)) -> c_24() 19:W:#COMPARE#(#neg(z0),#0()) -> c_25() 20:W:#COMPARE#(#neg(z0),#neg(z1)) -> c_26(#COMPARE#(z1,z0)) -->_1 #COMPARE#(#s(z0),#s(z1)) -> c_32(#COMPARE#(z0,z1)):26 -->_1 #COMPARE#(#pos(z0),#pos(z1)) -> c_30(#COMPARE#(z0,z1)):24 -->_1 #COMPARE#(#s(z0),#0()) -> c_31():25 -->_1 #COMPARE#(#pos(z0),#neg(z1)) -> c_29():23 -->_1 #COMPARE#(#pos(z0),#0()) -> c_28():22 -->_1 #COMPARE#(#neg(z0),#pos(z1)) -> c_27():21 -->_1 #COMPARE#(#neg(z0),#neg(z1)) -> c_26(#COMPARE#(z1,z0)):20 -->_1 #COMPARE#(#neg(z0),#0()) -> c_25():19 -->_1 #COMPARE#(#0(),#s(z0)) -> c_24():18 -->_1 #COMPARE#(#0(),#pos(z0)) -> c_23():17 -->_1 #COMPARE#(#0(),#neg(z0)) -> c_22():16 -->_1 #COMPARE#(#0(),#0()) -> c_21():15 21:W:#COMPARE#(#neg(z0),#pos(z1)) -> c_27() 22:W:#COMPARE#(#pos(z0),#0()) -> c_28() 23:W:#COMPARE#(#pos(z0),#neg(z1)) -> c_29() 24:W:#COMPARE#(#pos(z0),#pos(z1)) -> c_30(#COMPARE#(z0,z1)) -->_1 #COMPARE#(#s(z0),#s(z1)) -> c_32(#COMPARE#(z0,z1)):26 -->_1 #COMPARE#(#s(z0),#0()) -> c_31():25 -->_1 #COMPARE#(#pos(z0),#pos(z1)) -> c_30(#COMPARE#(z0,z1)):24 -->_1 #COMPARE#(#pos(z0),#neg(z1)) -> c_29():23 -->_1 #COMPARE#(#pos(z0),#0()) -> c_28():22 -->_1 #COMPARE#(#neg(z0),#pos(z1)) -> c_27():21 -->_1 #COMPARE#(#neg(z0),#neg(z1)) -> c_26(#COMPARE#(z1,z0)):20 -->_1 #COMPARE#(#neg(z0),#0()) -> c_25():19 -->_1 #COMPARE#(#0(),#s(z0)) -> c_24():18 -->_1 #COMPARE#(#0(),#pos(z0)) -> c_23():17 -->_1 #COMPARE#(#0(),#neg(z0)) -> c_22():16 -->_1 #COMPARE#(#0(),#0()) -> c_21():15 25:W:#COMPARE#(#s(z0),#0()) -> c_31() 26:W:#COMPARE#(#s(z0),#s(z1)) -> c_32(#COMPARE#(z0,z1)) -->_1 #COMPARE#(#s(z0),#s(z1)) -> c_32(#COMPARE#(z0,z1)):26 -->_1 #COMPARE#(#s(z0),#0()) -> c_31():25 -->_1 #COMPARE#(#pos(z0),#pos(z1)) -> c_30(#COMPARE#(z0,z1)):24 -->_1 #COMPARE#(#pos(z0),#neg(z1)) -> c_29():23 -->_1 #COMPARE#(#pos(z0),#0()) -> c_28():22 -->_1 #COMPARE#(#neg(z0),#pos(z1)) -> c_27():21 -->_1 #COMPARE#(#neg(z0),#neg(z1)) -> c_26(#COMPARE#(z1,z0)):20 -->_1 #COMPARE#(#neg(z0),#0()) -> c_25():19 -->_1 #COMPARE#(#0(),#s(z0)) -> c_24():18 -->_1 #COMPARE#(#0(),#pos(z0)) -> c_23():17 -->_1 #COMPARE#(#0(),#neg(z0)) -> c_22():16 -->_1 #COMPARE#(#0(),#0()) -> c_21():15 27:W:#LESS#(z0,z1) -> c_1(#CKLT#(#compare(z0,z1)),#compare#(z0,z1),#COMPARE#(z0,z1)) -->_2 #compare#(#s(z0),#s(z1)) -> c_47(#compare#(z0,z1)):42 -->_2 #compare#(#pos(z0),#pos(z1)) -> c_45(#compare#(z0,z1)):40 -->_2 #compare#(#neg(z0),#neg(z1)) -> c_41(#compare#(z1,z0)):36 -->_2 #compare#(#s(z0),#0()) -> c_46():41 -->_2 #compare#(#pos(z0),#neg(z1)) -> c_44():39 -->_2 #compare#(#pos(z0),#0()) -> c_43():38 -->_2 #compare#(#neg(z0),#pos(z1)) -> c_42():37 -->_2 #compare#(#neg(z0),#0()) -> c_40():35 -->_2 #compare#(#0(),#s(z0)) -> c_39():34 -->_2 #compare#(#0(),#pos(z0)) -> c_38():33 -->_2 #compare#(#0(),#neg(z0)) -> c_37():32 -->_2 #compare#(#0(),#0()) -> c_36():31 -->_3 #COMPARE#(#s(z0),#s(z1)) -> c_32(#COMPARE#(z0,z1)):26 -->_3 #COMPARE#(#s(z0),#0()) -> c_31():25 -->_3 #COMPARE#(#pos(z0),#pos(z1)) -> c_30(#COMPARE#(z0,z1)):24 -->_3 #COMPARE#(#pos(z0),#neg(z1)) -> c_29():23 -->_3 #COMPARE#(#pos(z0),#0()) -> c_28():22 -->_3 #COMPARE#(#neg(z0),#pos(z1)) -> c_27():21 -->_3 #COMPARE#(#neg(z0),#neg(z1)) -> c_26(#COMPARE#(z1,z0)):20 -->_3 #COMPARE#(#neg(z0),#0()) -> c_25():19 -->_3 #COMPARE#(#0(),#s(z0)) -> c_24():18 -->_3 #COMPARE#(#0(),#pos(z0)) -> c_23():17 -->_3 #COMPARE#(#0(),#neg(z0)) -> c_22():16 -->_3 #COMPARE#(#0(),#0()) -> c_21():15 -->_1 #CKLT#(#LT()) -> c_20():14 -->_1 #CKLT#(#GT()) -> c_19():13 -->_1 #CKLT#(#EQ()) -> c_18():12 28:W:#cklt#(#EQ()) -> c_33() 29:W:#cklt#(#GT()) -> c_34() 30:W:#cklt#(#LT()) -> c_35() 31:W:#compare#(#0(),#0()) -> c_36() 32:W:#compare#(#0(),#neg(z0)) -> c_37() 33:W:#compare#(#0(),#pos(z0)) -> c_38() 34:W:#compare#(#0(),#s(z0)) -> c_39() 35:W:#compare#(#neg(z0),#0()) -> c_40() 36:W:#compare#(#neg(z0),#neg(z1)) -> c_41(#compare#(z1,z0)) -->_1 #compare#(#s(z0),#s(z1)) -> c_47(#compare#(z0,z1)):42 -->_1 #compare#(#pos(z0),#pos(z1)) -> c_45(#compare#(z0,z1)):40 -->_1 #compare#(#s(z0),#0()) -> c_46():41 -->_1 #compare#(#pos(z0),#neg(z1)) -> c_44():39 -->_1 #compare#(#pos(z0),#0()) -> c_43():38 -->_1 #compare#(#neg(z0),#pos(z1)) -> c_42():37 -->_1 #compare#(#neg(z0),#neg(z1)) -> c_41(#compare#(z1,z0)):36 -->_1 #compare#(#neg(z0),#0()) -> c_40():35 -->_1 #compare#(#0(),#s(z0)) -> c_39():34 -->_1 #compare#(#0(),#pos(z0)) -> c_38():33 -->_1 #compare#(#0(),#neg(z0)) -> c_37():32 -->_1 #compare#(#0(),#0()) -> c_36():31 37:W:#compare#(#neg(z0),#pos(z1)) -> c_42() 38:W:#compare#(#pos(z0),#0()) -> c_43() 39:W:#compare#(#pos(z0),#neg(z1)) -> c_44() 40:W:#compare#(#pos(z0),#pos(z1)) -> c_45(#compare#(z0,z1)) -->_1 #compare#(#s(z0),#s(z1)) -> c_47(#compare#(z0,z1)):42 -->_1 #compare#(#s(z0),#0()) -> c_46():41 -->_1 #compare#(#pos(z0),#pos(z1)) -> c_45(#compare#(z0,z1)):40 -->_1 #compare#(#pos(z0),#neg(z1)) -> c_44():39 -->_1 #compare#(#pos(z0),#0()) -> c_43():38 -->_1 #compare#(#neg(z0),#pos(z1)) -> c_42():37 -->_1 #compare#(#neg(z0),#neg(z1)) -> c_41(#compare#(z1,z0)):36 -->_1 #compare#(#neg(z0),#0()) -> c_40():35 -->_1 #compare#(#0(),#s(z0)) -> c_39():34 -->_1 #compare#(#0(),#pos(z0)) -> c_38():33 -->_1 #compare#(#0(),#neg(z0)) -> c_37():32 -->_1 #compare#(#0(),#0()) -> c_36():31 41:W:#compare#(#s(z0),#0()) -> c_46() 42:W:#compare#(#s(z0),#s(z1)) -> c_47(#compare#(z0,z1)) -->_1 #compare#(#s(z0),#s(z1)) -> c_47(#compare#(z0,z1)):42 -->_1 #compare#(#s(z0),#0()) -> c_46():41 -->_1 #compare#(#pos(z0),#pos(z1)) -> c_45(#compare#(z0,z1)):40 -->_1 #compare#(#pos(z0),#neg(z1)) -> c_44():39 -->_1 #compare#(#pos(z0),#0()) -> c_43():38 -->_1 #compare#(#neg(z0),#pos(z1)) -> c_42():37 -->_1 #compare#(#neg(z0),#neg(z1)) -> c_41(#compare#(z1,z0)):36 -->_1 #compare#(#neg(z0),#0()) -> c_40():35 -->_1 #compare#(#0(),#s(z0)) -> c_39():34 -->_1 #compare#(#0(),#pos(z0)) -> c_38():33 -->_1 #compare#(#0(),#neg(z0)) -> c_37():32 -->_1 #compare#(#0(),#0()) -> c_36():31 43:W:#less#(z0,z1) -> c_48(#cklt#(#compare(z0,z1)),#compare#(z0,z1)) -->_2 #compare#(#s(z0),#s(z1)) -> c_47(#compare#(z0,z1)):42 -->_2 #compare#(#s(z0),#0()) -> c_46():41 -->_2 #compare#(#pos(z0),#pos(z1)) -> c_45(#compare#(z0,z1)):40 -->_2 #compare#(#pos(z0),#neg(z1)) -> c_44():39 -->_2 #compare#(#pos(z0),#0()) -> c_43():38 -->_2 #compare#(#neg(z0),#pos(z1)) -> c_42():37 -->_2 #compare#(#neg(z0),#neg(z1)) -> c_41(#compare#(z1,z0)):36 -->_2 #compare#(#neg(z0),#0()) -> c_40():35 -->_2 #compare#(#0(),#s(z0)) -> c_39():34 -->_2 #compare#(#0(),#pos(z0)) -> c_38():33 -->_2 #compare#(#0(),#neg(z0)) -> c_37():32 -->_2 #compare#(#0(),#0()) -> c_36():31 -->_1 #cklt#(#LT()) -> c_35():30 -->_1 #cklt#(#GT()) -> c_34():29 -->_1 #cklt#(#EQ()) -> c_33():28 44:W:APPEND#1#(nil(),z0) -> c_4() 45:W:FLATTEN#1#(leaf()) -> c_6() 46:W:INSERT#1#(nil(),z0) -> c_12() 47:W:INSERT#2#(#false(),z0,z1,z2) -> c_13() 48:W:INSERTIONSORT#1#(nil()) -> c_17() 49:W:append#(z0,z1) -> c_49(append#1#(z0,z1)) -->_1 append#1#(::(z0,z1),z2) -> c_50(append#(z1,z2)):50 -->_1 append#1#(nil(),z0) -> c_51():51 50:W:append#1#(::(z0,z1),z2) -> c_50(append#(z1,z2)) -->_1 append#(z0,z1) -> c_49(append#1#(z0,z1)):49 51:W:append#1#(nil(),z0) -> c_51() 52:W:flatten#(z0) -> c_52(flatten#1#(z0)) -->_1 flatten#1#(node(z0,z1,z2)) -> c_54(append#(z0,append(flatten(z1),flatten(z2))) ,append#(flatten(z1),flatten(z2)) ,flatten#(z1) ,flatten#(z2)):54 -->_1 flatten#1#(leaf()) -> c_53():53 53:W:flatten#1#(leaf()) -> c_53() 54:W:flatten#1#(node(z0,z1,z2)) -> c_54(append#(z0,append(flatten(z1),flatten(z2))) ,append#(flatten(z1),flatten(z2)) ,flatten#(z1) ,flatten#(z2)) -->_4 flatten#(z0) -> c_52(flatten#1#(z0)):52 -->_3 flatten#(z0) -> c_52(flatten#1#(z0)):52 -->_2 append#(z0,z1) -> c_49(append#1#(z0,z1)):49 -->_1 append#(z0,z1) -> c_49(append#1#(z0,z1)):49 55:W:flattensort#(z0) -> c_55(insertionsort#(flatten(z0)),flatten#(z0)) -->_1 insertionsort#(z0) -> c_61(insertionsort#1#(z0)):61 -->_2 flatten#(z0) -> c_52(flatten#1#(z0)):52 56:W:insert#(z0,z1) -> c_56(insert#1#(z1,z0)) -->_1 insert#1#(::(z0,z1),z2) -> c_57(insert#2#(#less(z0,z2),z2,z0,z1),#less#(z0,z2)):57 -->_1 insert#1#(nil(),z0) -> c_58():58 57:W:insert#1#(::(z0,z1),z2) -> c_57(insert#2#(#less(z0,z2),z2,z0,z1),#less#(z0,z2)) -->_1 insert#2#(#true(),z0,z1,z2) -> c_60(insert#(z0,z2)):60 -->_1 insert#2#(#false(),z0,z1,z2) -> c_59():59 -->_2 #less#(z0,z1) -> c_48(#cklt#(#compare(z0,z1)),#compare#(z0,z1)):43 58:W:insert#1#(nil(),z0) -> c_58() 59:W:insert#2#(#false(),z0,z1,z2) -> c_59() 60:W:insert#2#(#true(),z0,z1,z2) -> c_60(insert#(z0,z2)) -->_1 insert#(z0,z1) -> c_56(insert#1#(z1,z0)):56 61:W:insertionsort#(z0) -> c_61(insertionsort#1#(z0)) -->_1 insertionsort#1#(::(z0,z1)) -> c_62(insert#(z0,insertionsort(z1)),insertionsort#(z1)):62 -->_1 insertionsort#1#(nil()) -> c_63():63 62:W:insertionsort#1#(::(z0,z1)) -> c_62(insert#(z0,insertionsort(z1)),insertionsort#(z1)) -->_2 insertionsort#(z0) -> c_61(insertionsort#1#(z0)):61 -->_1 insert#(z0,z1) -> c_56(insert#1#(z1,z0)):56 63:W:insertionsort#1#(nil()) -> c_63() The following weak DPs constitute a sub-graph of the DG that is closed under successors. The DPs are removed. 55: flattensort#(z0) -> c_55(insertionsort#(flatten(z0)),flatten#(z0)) 48: INSERTIONSORT#1#(nil()) -> c_17() 46: INSERT#1#(nil(),z0) -> c_12() 47: INSERT#2#(#false(),z0,z1,z2) -> c_13() 27: #LESS#(z0,z1) -> c_1(#CKLT#(#compare(z0,z1)),#compare#(z0,z1),#COMPARE#(z0,z1)) 12: #CKLT#(#EQ()) -> c_18() 13: #CKLT#(#GT()) -> c_19() 14: #CKLT#(#LT()) -> c_20() 26: #COMPARE#(#s(z0),#s(z1)) -> c_32(#COMPARE#(z0,z1)) 24: #COMPARE#(#pos(z0),#pos(z1)) -> c_30(#COMPARE#(z0,z1)) 20: #COMPARE#(#neg(z0),#neg(z1)) -> c_26(#COMPARE#(z1,z0)) 15: #COMPARE#(#0(),#0()) -> c_21() 16: #COMPARE#(#0(),#neg(z0)) -> c_22() 17: #COMPARE#(#0(),#pos(z0)) -> c_23() 18: #COMPARE#(#0(),#s(z0)) -> c_24() 19: #COMPARE#(#neg(z0),#0()) -> c_25() 21: #COMPARE#(#neg(z0),#pos(z1)) -> c_27() 22: #COMPARE#(#pos(z0),#0()) -> c_28() 23: #COMPARE#(#pos(z0),#neg(z1)) -> c_29() 25: #COMPARE#(#s(z0),#0()) -> c_31() 61: insertionsort#(z0) -> c_61(insertionsort#1#(z0)) 62: insertionsort#1#(::(z0,z1)) -> c_62(insert#(z0,insertionsort(z1)),insertionsort#(z1)) 63: insertionsort#1#(nil()) -> c_63() 56: insert#(z0,z1) -> c_56(insert#1#(z1,z0)) 60: insert#2#(#true(),z0,z1,z2) -> c_60(insert#(z0,z2)) 57: insert#1#(::(z0,z1),z2) -> c_57(insert#2#(#less(z0,z2),z2,z0,z1),#less#(z0,z2)) 58: insert#1#(nil(),z0) -> c_58() 43: #less#(z0,z1) -> c_48(#cklt#(#compare(z0,z1)),#compare#(z0,z1)) 28: #cklt#(#EQ()) -> c_33() 29: #cklt#(#GT()) -> c_34() 30: #cklt#(#LT()) -> c_35() 42: #compare#(#s(z0),#s(z1)) -> c_47(#compare#(z0,z1)) 40: #compare#(#pos(z0),#pos(z1)) -> c_45(#compare#(z0,z1)) 36: #compare#(#neg(z0),#neg(z1)) -> c_41(#compare#(z1,z0)) 31: #compare#(#0(),#0()) -> c_36() 32: #compare#(#0(),#neg(z0)) -> c_37() 33: #compare#(#0(),#pos(z0)) -> c_38() 34: #compare#(#0(),#s(z0)) -> c_39() 35: #compare#(#neg(z0),#0()) -> c_40() 37: #compare#(#neg(z0),#pos(z1)) -> c_42() 38: #compare#(#pos(z0),#0()) -> c_43() 39: #compare#(#pos(z0),#neg(z1)) -> c_44() 41: #compare#(#s(z0),#0()) -> c_46() 59: insert#2#(#false(),z0,z1,z2) -> c_59() 45: FLATTEN#1#(leaf()) -> c_6() 52: flatten#(z0) -> c_52(flatten#1#(z0)) 54: flatten#1#(node(z0,z1,z2)) -> c_54(append#(z0,append(flatten(z1),flatten(z2))) ,append#(flatten(z1),flatten(z2)) ,flatten#(z1) ,flatten#(z2)) 53: flatten#1#(leaf()) -> c_53() 49: append#(z0,z1) -> c_49(append#1#(z0,z1)) 50: append#1#(::(z0,z1),z2) -> c_50(append#(z1,z2)) 51: append#1#(nil(),z0) -> c_51() 44: APPEND#1#(nil(),z0) -> c_4() * Step 5: SimplifyRHS. WORST_CASE(?,O(n^2)) + Considered Problem: - Strict DPs: APPEND#(z0,z1) -> c_2(APPEND#1#(z0,z1)) APPEND#1#(::(z0,z1),z2) -> c_3(APPEND#(z1,z2)) FLATTEN#(z0) -> c_5(FLATTEN#1#(z0)) FLATTEN#1#(node(z0,z1,z2)) -> c_7(APPEND#(z0,append(flatten(z1),flatten(z2))) ,append#(flatten(z1),flatten(z2)) ,flatten#(z1) ,flatten#(z2) ,APPEND#(flatten(z1),flatten(z2)) ,flatten#(z1) ,flatten#(z2) ,FLATTEN#(z1)) FLATTEN#1#(node(z0,z1,z2)) -> c_8(APPEND#(z0,append(flatten(z1),flatten(z2))) ,append#(flatten(z1),flatten(z2)) ,flatten#(z1) ,flatten#(z2) ,APPEND#(flatten(z1),flatten(z2)) ,flatten#(z1) ,flatten#(z2) ,FLATTEN#(z2)) FLATTENSORT#(z0) -> c_9(INSERTIONSORT#(flatten(z0)),flatten#(z0),FLATTEN#(z0)) INSERT#(z0,z1) -> c_10(INSERT#1#(z1,z0)) INSERT#1#(::(z0,z1),z2) -> c_11(INSERT#2#(#less(z0,z2),z2,z0,z1),#less#(z0,z2),#LESS#(z0,z2)) INSERT#2#(#true(),z0,z1,z2) -> c_14(INSERT#(z0,z2)) INSERTIONSORT#(z0) -> c_15(INSERTIONSORT#1#(z0)) INSERTIONSORT#1#(::(z0,z1)) -> c_16(INSERT#(z0,insertionsort(z1)),insertionsort#(z1),INSERTIONSORT#(z1)) - Weak TRS: #CKLT(#EQ()) -> c() #CKLT(#GT()) -> c1() #CKLT(#LT()) -> c2() #COMPARE(#0(),#0()) -> c3() #COMPARE(#0(),#neg(z0)) -> c4() #COMPARE(#0(),#pos(z0)) -> c5() #COMPARE(#0(),#s(z0)) -> c6() #COMPARE(#neg(z0),#0()) -> c7() #COMPARE(#neg(z0),#neg(z1)) -> c8(#COMPARE(z1,z0)) #COMPARE(#neg(z0),#pos(z1)) -> c9() #COMPARE(#pos(z0),#0()) -> c10() #COMPARE(#pos(z0),#neg(z1)) -> c11() #COMPARE(#pos(z0),#pos(z1)) -> c12(#COMPARE(z0,z1)) #COMPARE(#s(z0),#0()) -> c13() #COMPARE(#s(z0),#s(z1)) -> c14(#COMPARE(z0,z1)) #LESS(z0,z1) -> c15(#CKLT(#compare(z0,z1)),#COMPARE(z0,z1)) #cklt(#EQ()) -> #false() #cklt(#GT()) -> #false() #cklt(#LT()) -> #true() #compare(#0(),#0()) -> #EQ() #compare(#0(),#neg(z0)) -> #GT() #compare(#0(),#pos(z0)) -> #LT() #compare(#0(),#s(z0)) -> #LT() #compare(#neg(z0),#0()) -> #LT() #compare(#neg(z0),#neg(z1)) -> #compare(z1,z0) #compare(#neg(z0),#pos(z1)) -> #LT() #compare(#pos(z0),#0()) -> #GT() #compare(#pos(z0),#neg(z1)) -> #GT() #compare(#pos(z0),#pos(z1)) -> #compare(z0,z1) #compare(#s(z0),#0()) -> #GT() #compare(#s(z0),#s(z1)) -> #compare(z0,z1) #less(z0,z1) -> #cklt(#compare(z0,z1)) APPEND(z0,z1) -> c16(APPEND#1(z0,z1)) APPEND#1(::(z0,z1),z2) -> c17(APPEND(z1,z2)) APPEND#1(nil(),z0) -> c18() FLATTEN(z0) -> c19(FLATTEN#1(z0)) FLATTEN#1(leaf()) -> c20() FLATTEN#1(node(z0,z1,z2)) -> c21(APPEND(z0,append(flatten(z1),flatten(z2))) ,APPEND(flatten(z1),flatten(z2)) ,FLATTEN(z1)) FLATTEN#1(node(z0,z1,z2)) -> c22(APPEND(z0,append(flatten(z1),flatten(z2))) ,APPEND(flatten(z1),flatten(z2)) ,FLATTEN(z2)) FLATTENSORT(z0) -> c23(INSERTIONSORT(flatten(z0)),FLATTEN(z0)) INSERT(z0,z1) -> c24(INSERT#1(z1,z0)) INSERT#1(::(z0,z1),z2) -> c25(INSERT#2(#less(z0,z2),z2,z0,z1),#LESS(z0,z2)) INSERT#1(nil(),z0) -> c26() INSERT#2(#false(),z0,z1,z2) -> c27() INSERT#2(#true(),z0,z1,z2) -> c28(INSERT(z0,z2)) INSERTIONSORT(z0) -> c29(INSERTIONSORT#1(z0)) INSERTIONSORT#1(::(z0,z1)) -> c30(INSERT(z0,insertionsort(z1)),INSERTIONSORT(z1)) INSERTIONSORT#1(nil()) -> c31() append(z0,z1) -> append#1(z0,z1) append#1(::(z0,z1),z2) -> ::(z0,append(z1,z2)) append#1(nil(),z0) -> z0 flatten(z0) -> flatten#1(z0) flatten#1(leaf()) -> nil() flatten#1(node(z0,z1,z2)) -> append(z0,append(flatten(z1),flatten(z2))) flattensort(z0) -> insertionsort(flatten(z0)) insert(z0,z1) -> insert#1(z1,z0) insert#1(::(z0,z1),z2) -> insert#2(#less(z0,z2),z2,z0,z1) insert#1(nil(),z0) -> ::(z0,nil()) insert#2(#false(),z0,z1,z2) -> ::(z0,::(z1,z2)) insert#2(#true(),z0,z1,z2) -> ::(z1,insert(z0,z2)) insertionsort(z0) -> insertionsort#1(z0) insertionsort#1(::(z0,z1)) -> insert(z0,insertionsort(z1)) insertionsort#1(nil()) -> nil() - Signature: {#CKLT/1,#COMPARE/2,#LESS/2,#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,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,#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,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,::/2,c/0,c1/0,c10/0,c11/0 ,c12/1,c13/0,c14/1,c15/2,c16/1,c17/1,c18/0,c19/1,c2/0,c20/0,c21/3,c22/3,c23/2,c24/1,c25/2,c26/0,c27/0,c28/1 ,c29/1,c3/0,c30/2,c31/0,c4/0,c5/0,c6/0,c7/0,c8/1,c9/0,leaf/0,nil/0,node/3,c_1/3,c_2/1,c_3/1,c_4/0,c_5/1 ,c_6/0,c_7/8,c_8/8,c_9/3,c_10/1,c_11/3,c_12/0,c_13/0,c_14/1,c_15/1,c_16/3,c_17/0,c_18/0,c_19/0,c_20/0,c_21/0 ,c_22/0,c_23/0,c_24/0,c_25/0,c_26/1,c_27/0,c_28/0,c_29/0,c_30/1,c_31/0,c_32/1,c_33/0,c_34/0,c_35/0,c_36/0 ,c_37/0,c_38/0,c_39/0,c_40/0,c_41/1,c_42/0,c_43/0,c_44/0,c_45/1,c_46/0,c_47/1,c_48/2,c_49/1,c_50/1,c_51/0 ,c_52/1,c_53/0,c_54/4,c_55/2,c_56/1,c_57/2,c_58/0,c_59/0,c_60/1,c_61/1,c_62/2,c_63/0} - Obligation: innermost runtime complexity wrt. defined symbols {#CKLT#,#COMPARE#,#LESS#,#cklt#,#compare#,#less#,APPEND# ,APPEND#1#,FLATTEN#,FLATTEN#1#,FLATTENSORT#,INSERT#,INSERT#1#,INSERT#2#,INSERTIONSORT#,INSERTIONSORT#1# ,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,::,c,c1,c10,c11,c12,c13,c14 ,c15,c16,c17,c18,c19,c2,c20,c21,c22,c23,c24,c25,c26,c27,c28,c29,c3,c30,c31,c4,c5,c6,c7,c8,c9,leaf,nil,node} + Applied Processor: SimplifyRHS + Details: Consider the dependency graph 1:S:APPEND#(z0,z1) -> c_2(APPEND#1#(z0,z1)) -->_1 APPEND#1#(::(z0,z1),z2) -> c_3(APPEND#(z1,z2)):2 2:S:APPEND#1#(::(z0,z1),z2) -> c_3(APPEND#(z1,z2)) -->_1 APPEND#(z0,z1) -> c_2(APPEND#1#(z0,z1)):1 3:S:FLATTEN#(z0) -> c_5(FLATTEN#1#(z0)) -->_1 FLATTEN#1#(node(z0,z1,z2)) -> c_8(APPEND#(z0,append(flatten(z1),flatten(z2))) ,append#(flatten(z1),flatten(z2)) ,flatten#(z1) ,flatten#(z2) ,APPEND#(flatten(z1),flatten(z2)) ,flatten#(z1) ,flatten#(z2) ,FLATTEN#(z2)):5 -->_1 FLATTEN#1#(node(z0,z1,z2)) -> c_7(APPEND#(z0,append(flatten(z1),flatten(z2))) ,append#(flatten(z1),flatten(z2)) ,flatten#(z1) ,flatten#(z2) ,APPEND#(flatten(z1),flatten(z2)) ,flatten#(z1) ,flatten#(z2) ,FLATTEN#(z1)):4 4:S:FLATTEN#1#(node(z0,z1,z2)) -> c_7(APPEND#(z0,append(flatten(z1),flatten(z2))) ,append#(flatten(z1),flatten(z2)) ,flatten#(z1) ,flatten#(z2) ,APPEND#(flatten(z1),flatten(z2)) ,flatten#(z1) ,flatten#(z2) ,FLATTEN#(z1)) -->_8 FLATTEN#(z0) -> c_5(FLATTEN#1#(z0)):3 -->_5 APPEND#(z0,z1) -> c_2(APPEND#1#(z0,z1)):1 -->_1 APPEND#(z0,z1) -> c_2(APPEND#1#(z0,z1)):1 5:S:FLATTEN#1#(node(z0,z1,z2)) -> c_8(APPEND#(z0,append(flatten(z1),flatten(z2))) ,append#(flatten(z1),flatten(z2)) ,flatten#(z1) ,flatten#(z2) ,APPEND#(flatten(z1),flatten(z2)) ,flatten#(z1) ,flatten#(z2) ,FLATTEN#(z2)) -->_8 FLATTEN#(z0) -> c_5(FLATTEN#1#(z0)):3 -->_5 APPEND#(z0,z1) -> c_2(APPEND#1#(z0,z1)):1 -->_1 APPEND#(z0,z1) -> c_2(APPEND#1#(z0,z1)):1 6:S:FLATTENSORT#(z0) -> c_9(INSERTIONSORT#(flatten(z0)),flatten#(z0),FLATTEN#(z0)) -->_1 INSERTIONSORT#(z0) -> c_15(INSERTIONSORT#1#(z0)):10 -->_3 FLATTEN#(z0) -> c_5(FLATTEN#1#(z0)):3 7:S:INSERT#(z0,z1) -> c_10(INSERT#1#(z1,z0)) -->_1 INSERT#1#(::(z0,z1),z2) -> c_11(INSERT#2#(#less(z0,z2),z2,z0,z1),#less#(z0,z2),#LESS#(z0,z2)):8 8:S:INSERT#1#(::(z0,z1),z2) -> c_11(INSERT#2#(#less(z0,z2),z2,z0,z1),#less#(z0,z2),#LESS#(z0,z2)) -->_1 INSERT#2#(#true(),z0,z1,z2) -> c_14(INSERT#(z0,z2)):9 9:S:INSERT#2#(#true(),z0,z1,z2) -> c_14(INSERT#(z0,z2)) -->_1 INSERT#(z0,z1) -> c_10(INSERT#1#(z1,z0)):7 10:S:INSERTIONSORT#(z0) -> c_15(INSERTIONSORT#1#(z0)) -->_1 INSERTIONSORT#1#(::(z0,z1)) -> c_16(INSERT#(z0,insertionsort(z1)) ,insertionsort#(z1) ,INSERTIONSORT#(z1)):11 11:S:INSERTIONSORT#1#(::(z0,z1)) -> c_16(INSERT#(z0,insertionsort(z1)) ,insertionsort#(z1) ,INSERTIONSORT#(z1)) -->_3 INSERTIONSORT#(z0) -> c_15(INSERTIONSORT#1#(z0)):10 -->_1 INSERT#(z0,z1) -> c_10(INSERT#1#(z1,z0)):7 Due to missing edges in the depndency graph, the right-hand sides of following rules could be simplified: FLATTEN#1#(node(z0,z1,z2)) -> c_7(APPEND#(z0,append(flatten(z1),flatten(z2))) ,APPEND#(flatten(z1),flatten(z2)) ,FLATTEN#(z1)) FLATTEN#1#(node(z0,z1,z2)) -> c_8(APPEND#(z0,append(flatten(z1),flatten(z2))) ,APPEND#(flatten(z1),flatten(z2)) ,FLATTEN#(z2)) FLATTENSORT#(z0) -> c_9(INSERTIONSORT#(flatten(z0)),FLATTEN#(z0)) INSERT#1#(::(z0,z1),z2) -> c_11(INSERT#2#(#less(z0,z2),z2,z0,z1)) INSERTIONSORT#1#(::(z0,z1)) -> c_16(INSERT#(z0,insertionsort(z1)),INSERTIONSORT#(z1)) * Step 6: UsableRules. WORST_CASE(?,O(n^2)) + Considered Problem: - Strict DPs: APPEND#(z0,z1) -> c_2(APPEND#1#(z0,z1)) APPEND#1#(::(z0,z1),z2) -> c_3(APPEND#(z1,z2)) FLATTEN#(z0) -> c_5(FLATTEN#1#(z0)) FLATTEN#1#(node(z0,z1,z2)) -> c_7(APPEND#(z0,append(flatten(z1),flatten(z2))) ,APPEND#(flatten(z1),flatten(z2)) ,FLATTEN#(z1)) FLATTEN#1#(node(z0,z1,z2)) -> c_8(APPEND#(z0,append(flatten(z1),flatten(z2))) ,APPEND#(flatten(z1),flatten(z2)) ,FLATTEN#(z2)) FLATTENSORT#(z0) -> c_9(INSERTIONSORT#(flatten(z0)),FLATTEN#(z0)) INSERT#(z0,z1) -> c_10(INSERT#1#(z1,z0)) INSERT#1#(::(z0,z1),z2) -> c_11(INSERT#2#(#less(z0,z2),z2,z0,z1)) INSERT#2#(#true(),z0,z1,z2) -> c_14(INSERT#(z0,z2)) INSERTIONSORT#(z0) -> c_15(INSERTIONSORT#1#(z0)) INSERTIONSORT#1#(::(z0,z1)) -> c_16(INSERT#(z0,insertionsort(z1)),INSERTIONSORT#(z1)) - Weak TRS: #CKLT(#EQ()) -> c() #CKLT(#GT()) -> c1() #CKLT(#LT()) -> c2() #COMPARE(#0(),#0()) -> c3() #COMPARE(#0(),#neg(z0)) -> c4() #COMPARE(#0(),#pos(z0)) -> c5() #COMPARE(#0(),#s(z0)) -> c6() #COMPARE(#neg(z0),#0()) -> c7() #COMPARE(#neg(z0),#neg(z1)) -> c8(#COMPARE(z1,z0)) #COMPARE(#neg(z0),#pos(z1)) -> c9() #COMPARE(#pos(z0),#0()) -> c10() #COMPARE(#pos(z0),#neg(z1)) -> c11() #COMPARE(#pos(z0),#pos(z1)) -> c12(#COMPARE(z0,z1)) #COMPARE(#s(z0),#0()) -> c13() #COMPARE(#s(z0),#s(z1)) -> c14(#COMPARE(z0,z1)) #LESS(z0,z1) -> c15(#CKLT(#compare(z0,z1)),#COMPARE(z0,z1)) #cklt(#EQ()) -> #false() #cklt(#GT()) -> #false() #cklt(#LT()) -> #true() #compare(#0(),#0()) -> #EQ() #compare(#0(),#neg(z0)) -> #GT() #compare(#0(),#pos(z0)) -> #LT() #compare(#0(),#s(z0)) -> #LT() #compare(#neg(z0),#0()) -> #LT() #compare(#neg(z0),#neg(z1)) -> #compare(z1,z0) #compare(#neg(z0),#pos(z1)) -> #LT() #compare(#pos(z0),#0()) -> #GT() #compare(#pos(z0),#neg(z1)) -> #GT() #compare(#pos(z0),#pos(z1)) -> #compare(z0,z1) #compare(#s(z0),#0()) -> #GT() #compare(#s(z0),#s(z1)) -> #compare(z0,z1) #less(z0,z1) -> #cklt(#compare(z0,z1)) APPEND(z0,z1) -> c16(APPEND#1(z0,z1)) APPEND#1(::(z0,z1),z2) -> c17(APPEND(z1,z2)) APPEND#1(nil(),z0) -> c18() FLATTEN(z0) -> c19(FLATTEN#1(z0)) FLATTEN#1(leaf()) -> c20() FLATTEN#1(node(z0,z1,z2)) -> c21(APPEND(z0,append(flatten(z1),flatten(z2))) ,APPEND(flatten(z1),flatten(z2)) ,FLATTEN(z1)) FLATTEN#1(node(z0,z1,z2)) -> c22(APPEND(z0,append(flatten(z1),flatten(z2))) ,APPEND(flatten(z1),flatten(z2)) ,FLATTEN(z2)) FLATTENSORT(z0) -> c23(INSERTIONSORT(flatten(z0)),FLATTEN(z0)) INSERT(z0,z1) -> c24(INSERT#1(z1,z0)) INSERT#1(::(z0,z1),z2) -> c25(INSERT#2(#less(z0,z2),z2,z0,z1),#LESS(z0,z2)) INSERT#1(nil(),z0) -> c26() INSERT#2(#false(),z0,z1,z2) -> c27() INSERT#2(#true(),z0,z1,z2) -> c28(INSERT(z0,z2)) INSERTIONSORT(z0) -> c29(INSERTIONSORT#1(z0)) INSERTIONSORT#1(::(z0,z1)) -> c30(INSERT(z0,insertionsort(z1)),INSERTIONSORT(z1)) INSERTIONSORT#1(nil()) -> c31() append(z0,z1) -> append#1(z0,z1) append#1(::(z0,z1),z2) -> ::(z0,append(z1,z2)) append#1(nil(),z0) -> z0 flatten(z0) -> flatten#1(z0) flatten#1(leaf()) -> nil() flatten#1(node(z0,z1,z2)) -> append(z0,append(flatten(z1),flatten(z2))) flattensort(z0) -> insertionsort(flatten(z0)) insert(z0,z1) -> insert#1(z1,z0) insert#1(::(z0,z1),z2) -> insert#2(#less(z0,z2),z2,z0,z1) insert#1(nil(),z0) -> ::(z0,nil()) insert#2(#false(),z0,z1,z2) -> ::(z0,::(z1,z2)) insert#2(#true(),z0,z1,z2) -> ::(z1,insert(z0,z2)) insertionsort(z0) -> insertionsort#1(z0) insertionsort#1(::(z0,z1)) -> insert(z0,insertionsort(z1)) insertionsort#1(nil()) -> nil() - Signature: {#CKLT/1,#COMPARE/2,#LESS/2,#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,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,#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,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,::/2,c/0,c1/0,c10/0,c11/0 ,c12/1,c13/0,c14/1,c15/2,c16/1,c17/1,c18/0,c19/1,c2/0,c20/0,c21/3,c22/3,c23/2,c24/1,c25/2,c26/0,c27/0,c28/1 ,c29/1,c3/0,c30/2,c31/0,c4/0,c5/0,c6/0,c7/0,c8/1,c9/0,leaf/0,nil/0,node/3,c_1/3,c_2/1,c_3/1,c_4/0,c_5/1 ,c_6/0,c_7/3,c_8/3,c_9/2,c_10/1,c_11/1,c_12/0,c_13/0,c_14/1,c_15/1,c_16/2,c_17/0,c_18/0,c_19/0,c_20/0,c_21/0 ,c_22/0,c_23/0,c_24/0,c_25/0,c_26/1,c_27/0,c_28/0,c_29/0,c_30/1,c_31/0,c_32/1,c_33/0,c_34/0,c_35/0,c_36/0 ,c_37/0,c_38/0,c_39/0,c_40/0,c_41/1,c_42/0,c_43/0,c_44/0,c_45/1,c_46/0,c_47/1,c_48/2,c_49/1,c_50/1,c_51/0 ,c_52/1,c_53/0,c_54/4,c_55/2,c_56/1,c_57/2,c_58/0,c_59/0,c_60/1,c_61/1,c_62/2,c_63/0} - Obligation: innermost runtime complexity wrt. defined symbols {#CKLT#,#COMPARE#,#LESS#,#cklt#,#compare#,#less#,APPEND# ,APPEND#1#,FLATTEN#,FLATTEN#1#,FLATTENSORT#,INSERT#,INSERT#1#,INSERT#2#,INSERTIONSORT#,INSERTIONSORT#1# ,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,::,c,c1,c10,c11,c12,c13,c14 ,c15,c16,c17,c18,c19,c2,c20,c21,c22,c23,c24,c25,c26,c27,c28,c29,c3,c30,c31,c4,c5,c6,c7,c8,c9,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(z0)) -> #GT() #compare(#0(),#pos(z0)) -> #LT() #compare(#0(),#s(z0)) -> #LT() #compare(#neg(z0),#0()) -> #LT() #compare(#neg(z0),#neg(z1)) -> #compare(z1,z0) #compare(#neg(z0),#pos(z1)) -> #LT() #compare(#pos(z0),#0()) -> #GT() #compare(#pos(z0),#neg(z1)) -> #GT() #compare(#pos(z0),#pos(z1)) -> #compare(z0,z1) #compare(#s(z0),#0()) -> #GT() #compare(#s(z0),#s(z1)) -> #compare(z0,z1) #less(z0,z1) -> #cklt(#compare(z0,z1)) append(z0,z1) -> append#1(z0,z1) append#1(::(z0,z1),z2) -> ::(z0,append(z1,z2)) append#1(nil(),z0) -> z0 flatten(z0) -> flatten#1(z0) flatten#1(leaf()) -> nil() flatten#1(node(z0,z1,z2)) -> append(z0,append(flatten(z1),flatten(z2))) insert(z0,z1) -> insert#1(z1,z0) insert#1(::(z0,z1),z2) -> insert#2(#less(z0,z2),z2,z0,z1) insert#1(nil(),z0) -> ::(z0,nil()) insert#2(#false(),z0,z1,z2) -> ::(z0,::(z1,z2)) insert#2(#true(),z0,z1,z2) -> ::(z1,insert(z0,z2)) insertionsort(z0) -> insertionsort#1(z0) insertionsort#1(::(z0,z1)) -> insert(z0,insertionsort(z1)) insertionsort#1(nil()) -> nil() APPEND#(z0,z1) -> c_2(APPEND#1#(z0,z1)) APPEND#1#(::(z0,z1),z2) -> c_3(APPEND#(z1,z2)) FLATTEN#(z0) -> c_5(FLATTEN#1#(z0)) FLATTEN#1#(node(z0,z1,z2)) -> c_7(APPEND#(z0,append(flatten(z1),flatten(z2))) ,APPEND#(flatten(z1),flatten(z2)) ,FLATTEN#(z1)) FLATTEN#1#(node(z0,z1,z2)) -> c_8(APPEND#(z0,append(flatten(z1),flatten(z2))) ,APPEND#(flatten(z1),flatten(z2)) ,FLATTEN#(z2)) FLATTENSORT#(z0) -> c_9(INSERTIONSORT#(flatten(z0)),FLATTEN#(z0)) INSERT#(z0,z1) -> c_10(INSERT#1#(z1,z0)) INSERT#1#(::(z0,z1),z2) -> c_11(INSERT#2#(#less(z0,z2),z2,z0,z1)) INSERT#2#(#true(),z0,z1,z2) -> c_14(INSERT#(z0,z2)) INSERTIONSORT#(z0) -> c_15(INSERTIONSORT#1#(z0)) INSERTIONSORT#1#(::(z0,z1)) -> c_16(INSERT#(z0,insertionsort(z1)),INSERTIONSORT#(z1)) * Step 7: DecomposeDG. WORST_CASE(?,O(n^2)) + Considered Problem: - Strict DPs: APPEND#(z0,z1) -> c_2(APPEND#1#(z0,z1)) APPEND#1#(::(z0,z1),z2) -> c_3(APPEND#(z1,z2)) FLATTEN#(z0) -> c_5(FLATTEN#1#(z0)) FLATTEN#1#(node(z0,z1,z2)) -> c_7(APPEND#(z0,append(flatten(z1),flatten(z2))) ,APPEND#(flatten(z1),flatten(z2)) ,FLATTEN#(z1)) FLATTEN#1#(node(z0,z1,z2)) -> c_8(APPEND#(z0,append(flatten(z1),flatten(z2))) ,APPEND#(flatten(z1),flatten(z2)) ,FLATTEN#(z2)) FLATTENSORT#(z0) -> c_9(INSERTIONSORT#(flatten(z0)),FLATTEN#(z0)) INSERT#(z0,z1) -> c_10(INSERT#1#(z1,z0)) INSERT#1#(::(z0,z1),z2) -> c_11(INSERT#2#(#less(z0,z2),z2,z0,z1)) INSERT#2#(#true(),z0,z1,z2) -> c_14(INSERT#(z0,z2)) INSERTIONSORT#(z0) -> c_15(INSERTIONSORT#1#(z0)) INSERTIONSORT#1#(::(z0,z1)) -> c_16(INSERT#(z0,insertionsort(z1)),INSERTIONSORT#(z1)) - Weak TRS: #cklt(#EQ()) -> #false() #cklt(#GT()) -> #false() #cklt(#LT()) -> #true() #compare(#0(),#0()) -> #EQ() #compare(#0(),#neg(z0)) -> #GT() #compare(#0(),#pos(z0)) -> #LT() #compare(#0(),#s(z0)) -> #LT() #compare(#neg(z0),#0()) -> #LT() #compare(#neg(z0),#neg(z1)) -> #compare(z1,z0) #compare(#neg(z0),#pos(z1)) -> #LT() #compare(#pos(z0),#0()) -> #GT() #compare(#pos(z0),#neg(z1)) -> #GT() #compare(#pos(z0),#pos(z1)) -> #compare(z0,z1) #compare(#s(z0),#0()) -> #GT() #compare(#s(z0),#s(z1)) -> #compare(z0,z1) #less(z0,z1) -> #cklt(#compare(z0,z1)) append(z0,z1) -> append#1(z0,z1) append#1(::(z0,z1),z2) -> ::(z0,append(z1,z2)) append#1(nil(),z0) -> z0 flatten(z0) -> flatten#1(z0) flatten#1(leaf()) -> nil() flatten#1(node(z0,z1,z2)) -> append(z0,append(flatten(z1),flatten(z2))) insert(z0,z1) -> insert#1(z1,z0) insert#1(::(z0,z1),z2) -> insert#2(#less(z0,z2),z2,z0,z1) insert#1(nil(),z0) -> ::(z0,nil()) insert#2(#false(),z0,z1,z2) -> ::(z0,::(z1,z2)) insert#2(#true(),z0,z1,z2) -> ::(z1,insert(z0,z2)) insertionsort(z0) -> insertionsort#1(z0) insertionsort#1(::(z0,z1)) -> insert(z0,insertionsort(z1)) insertionsort#1(nil()) -> nil() - Signature: {#CKLT/1,#COMPARE/2,#LESS/2,#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,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,#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,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,::/2,c/0,c1/0,c10/0,c11/0 ,c12/1,c13/0,c14/1,c15/2,c16/1,c17/1,c18/0,c19/1,c2/0,c20/0,c21/3,c22/3,c23/2,c24/1,c25/2,c26/0,c27/0,c28/1 ,c29/1,c3/0,c30/2,c31/0,c4/0,c5/0,c6/0,c7/0,c8/1,c9/0,leaf/0,nil/0,node/3,c_1/3,c_2/1,c_3/1,c_4/0,c_5/1 ,c_6/0,c_7/3,c_8/3,c_9/2,c_10/1,c_11/1,c_12/0,c_13/0,c_14/1,c_15/1,c_16/2,c_17/0,c_18/0,c_19/0,c_20/0,c_21/0 ,c_22/0,c_23/0,c_24/0,c_25/0,c_26/1,c_27/0,c_28/0,c_29/0,c_30/1,c_31/0,c_32/1,c_33/0,c_34/0,c_35/0,c_36/0 ,c_37/0,c_38/0,c_39/0,c_40/0,c_41/1,c_42/0,c_43/0,c_44/0,c_45/1,c_46/0,c_47/1,c_48/2,c_49/1,c_50/1,c_51/0 ,c_52/1,c_53/0,c_54/4,c_55/2,c_56/1,c_57/2,c_58/0,c_59/0,c_60/1,c_61/1,c_62/2,c_63/0} - Obligation: innermost runtime complexity wrt. defined symbols {#CKLT#,#COMPARE#,#LESS#,#cklt#,#compare#,#less#,APPEND# ,APPEND#1#,FLATTEN#,FLATTEN#1#,FLATTENSORT#,INSERT#,INSERT#1#,INSERT#2#,INSERTIONSORT#,INSERTIONSORT#1# ,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,::,c,c1,c10,c11,c12,c13,c14 ,c15,c16,c17,c18,c19,c2,c20,c21,c22,c23,c24,c25,c26,c27,c28,c29,c3,c30,c31,c4,c5,c6,c7,c8,c9,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#(z0) -> c_5(FLATTEN#1#(z0)) FLATTEN#1#(node(z0,z1,z2)) -> c_7(APPEND#(z0,append(flatten(z1),flatten(z2))) ,APPEND#(flatten(z1),flatten(z2)) ,FLATTEN#(z1)) FLATTEN#1#(node(z0,z1,z2)) -> c_8(APPEND#(z0,append(flatten(z1),flatten(z2))) ,APPEND#(flatten(z1),flatten(z2)) ,FLATTEN#(z2)) FLATTENSORT#(z0) -> c_9(INSERTIONSORT#(flatten(z0)),FLATTEN#(z0)) INSERTIONSORT#(z0) -> c_15(INSERTIONSORT#1#(z0)) INSERTIONSORT#1#(::(z0,z1)) -> c_16(INSERT#(z0,insertionsort(z1)),INSERTIONSORT#(z1)) and a lower component APPEND#(z0,z1) -> c_2(APPEND#1#(z0,z1)) APPEND#1#(::(z0,z1),z2) -> c_3(APPEND#(z1,z2)) INSERT#(z0,z1) -> c_10(INSERT#1#(z1,z0)) INSERT#1#(::(z0,z1),z2) -> c_11(INSERT#2#(#less(z0,z2),z2,z0,z1)) INSERT#2#(#true(),z0,z1,z2) -> c_14(INSERT#(z0,z2)) Further, following extension rules are added to the lower component. FLATTEN#(z0) -> FLATTEN#1#(z0) FLATTEN#1#(node(z0,z1,z2)) -> APPEND#(z0,append(flatten(z1),flatten(z2))) FLATTEN#1#(node(z0,z1,z2)) -> APPEND#(flatten(z1),flatten(z2)) FLATTEN#1#(node(z0,z1,z2)) -> FLATTEN#(z1) FLATTEN#1#(node(z0,z1,z2)) -> FLATTEN#(z2) FLATTENSORT#(z0) -> FLATTEN#(z0) FLATTENSORT#(z0) -> INSERTIONSORT#(flatten(z0)) INSERTIONSORT#(z0) -> INSERTIONSORT#1#(z0) INSERTIONSORT#1#(::(z0,z1)) -> INSERT#(z0,insertionsort(z1)) INSERTIONSORT#1#(::(z0,z1)) -> INSERTIONSORT#(z1) ** Step 7.a:1: SimplifyRHS. WORST_CASE(?,O(n^1)) + Considered Problem: - Strict DPs: FLATTEN#(z0) -> c_5(FLATTEN#1#(z0)) FLATTEN#1#(node(z0,z1,z2)) -> c_7(APPEND#(z0,append(flatten(z1),flatten(z2))) ,APPEND#(flatten(z1),flatten(z2)) ,FLATTEN#(z1)) FLATTEN#1#(node(z0,z1,z2)) -> c_8(APPEND#(z0,append(flatten(z1),flatten(z2))) ,APPEND#(flatten(z1),flatten(z2)) ,FLATTEN#(z2)) FLATTENSORT#(z0) -> c_9(INSERTIONSORT#(flatten(z0)),FLATTEN#(z0)) INSERTIONSORT#(z0) -> c_15(INSERTIONSORT#1#(z0)) INSERTIONSORT#1#(::(z0,z1)) -> c_16(INSERT#(z0,insertionsort(z1)),INSERTIONSORT#(z1)) - Weak TRS: #cklt(#EQ()) -> #false() #cklt(#GT()) -> #false() #cklt(#LT()) -> #true() #compare(#0(),#0()) -> #EQ() #compare(#0(),#neg(z0)) -> #GT() #compare(#0(),#pos(z0)) -> #LT() #compare(#0(),#s(z0)) -> #LT() #compare(#neg(z0),#0()) -> #LT() #compare(#neg(z0),#neg(z1)) -> #compare(z1,z0) #compare(#neg(z0),#pos(z1)) -> #LT() #compare(#pos(z0),#0()) -> #GT() #compare(#pos(z0),#neg(z1)) -> #GT() #compare(#pos(z0),#pos(z1)) -> #compare(z0,z1) #compare(#s(z0),#0()) -> #GT() #compare(#s(z0),#s(z1)) -> #compare(z0,z1) #less(z0,z1) -> #cklt(#compare(z0,z1)) append(z0,z1) -> append#1(z0,z1) append#1(::(z0,z1),z2) -> ::(z0,append(z1,z2)) append#1(nil(),z0) -> z0 flatten(z0) -> flatten#1(z0) flatten#1(leaf()) -> nil() flatten#1(node(z0,z1,z2)) -> append(z0,append(flatten(z1),flatten(z2))) insert(z0,z1) -> insert#1(z1,z0) insert#1(::(z0,z1),z2) -> insert#2(#less(z0,z2),z2,z0,z1) insert#1(nil(),z0) -> ::(z0,nil()) insert#2(#false(),z0,z1,z2) -> ::(z0,::(z1,z2)) insert#2(#true(),z0,z1,z2) -> ::(z1,insert(z0,z2)) insertionsort(z0) -> insertionsort#1(z0) insertionsort#1(::(z0,z1)) -> insert(z0,insertionsort(z1)) insertionsort#1(nil()) -> nil() - Signature: {#CKLT/1,#COMPARE/2,#LESS/2,#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,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,#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,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,::/2,c/0,c1/0,c10/0,c11/0 ,c12/1,c13/0,c14/1,c15/2,c16/1,c17/1,c18/0,c19/1,c2/0,c20/0,c21/3,c22/3,c23/2,c24/1,c25/2,c26/0,c27/0,c28/1 ,c29/1,c3/0,c30/2,c31/0,c4/0,c5/0,c6/0,c7/0,c8/1,c9/0,leaf/0,nil/0,node/3,c_1/3,c_2/1,c_3/1,c_4/0,c_5/1 ,c_6/0,c_7/3,c_8/3,c_9/2,c_10/1,c_11/1,c_12/0,c_13/0,c_14/1,c_15/1,c_16/2,c_17/0,c_18/0,c_19/0,c_20/0,c_21/0 ,c_22/0,c_23/0,c_24/0,c_25/0,c_26/1,c_27/0,c_28/0,c_29/0,c_30/1,c_31/0,c_32/1,c_33/0,c_34/0,c_35/0,c_36/0 ,c_37/0,c_38/0,c_39/0,c_40/0,c_41/1,c_42/0,c_43/0,c_44/0,c_45/1,c_46/0,c_47/1,c_48/2,c_49/1,c_50/1,c_51/0 ,c_52/1,c_53/0,c_54/4,c_55/2,c_56/1,c_57/2,c_58/0,c_59/0,c_60/1,c_61/1,c_62/2,c_63/0} - Obligation: innermost runtime complexity wrt. defined symbols {#CKLT#,#COMPARE#,#LESS#,#cklt#,#compare#,#less#,APPEND# ,APPEND#1#,FLATTEN#,FLATTEN#1#,FLATTENSORT#,INSERT#,INSERT#1#,INSERT#2#,INSERTIONSORT#,INSERTIONSORT#1# ,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,::,c,c1,c10,c11,c12,c13,c14 ,c15,c16,c17,c18,c19,c2,c20,c21,c22,c23,c24,c25,c26,c27,c28,c29,c3,c30,c31,c4,c5,c6,c7,c8,c9,leaf,nil,node} + Applied Processor: SimplifyRHS + Details: Consider the dependency graph 1:S:FLATTEN#(z0) -> c_5(FLATTEN#1#(z0)) -->_1 FLATTEN#1#(node(z0,z1,z2)) -> c_8(APPEND#(z0,append(flatten(z1),flatten(z2))) ,APPEND#(flatten(z1),flatten(z2)) ,FLATTEN#(z2)):3 -->_1 FLATTEN#1#(node(z0,z1,z2)) -> c_7(APPEND#(z0,append(flatten(z1),flatten(z2))) ,APPEND#(flatten(z1),flatten(z2)) ,FLATTEN#(z1)):2 2:S:FLATTEN#1#(node(z0,z1,z2)) -> c_7(APPEND#(z0,append(flatten(z1),flatten(z2))) ,APPEND#(flatten(z1),flatten(z2)) ,FLATTEN#(z1)) -->_3 FLATTEN#(z0) -> c_5(FLATTEN#1#(z0)):1 3:S:FLATTEN#1#(node(z0,z1,z2)) -> c_8(APPEND#(z0,append(flatten(z1),flatten(z2))) ,APPEND#(flatten(z1),flatten(z2)) ,FLATTEN#(z2)) -->_3 FLATTEN#(z0) -> c_5(FLATTEN#1#(z0)):1 4:S:FLATTENSORT#(z0) -> c_9(INSERTIONSORT#(flatten(z0)),FLATTEN#(z0)) -->_1 INSERTIONSORT#(z0) -> c_15(INSERTIONSORT#1#(z0)):5 -->_2 FLATTEN#(z0) -> c_5(FLATTEN#1#(z0)):1 5:S:INSERTIONSORT#(z0) -> c_15(INSERTIONSORT#1#(z0)) -->_1 INSERTIONSORT#1#(::(z0,z1)) -> c_16(INSERT#(z0,insertionsort(z1)),INSERTIONSORT#(z1)):6 6:S:INSERTIONSORT#1#(::(z0,z1)) -> c_16(INSERT#(z0,insertionsort(z1)),INSERTIONSORT#(z1)) -->_2 INSERTIONSORT#(z0) -> c_15(INSERTIONSORT#1#(z0)):5 Due to missing edges in the depndency graph, the right-hand sides of following rules could be simplified: FLATTEN#1#(node(z0,z1,z2)) -> c_7(FLATTEN#(z1)) FLATTEN#1#(node(z0,z1,z2)) -> c_8(FLATTEN#(z2)) INSERTIONSORT#1#(::(z0,z1)) -> c_16(INSERTIONSORT#(z1)) ** Step 7.a:2: UsableRules. WORST_CASE(?,O(n^1)) + Considered Problem: - Strict DPs: FLATTEN#(z0) -> c_5(FLATTEN#1#(z0)) FLATTEN#1#(node(z0,z1,z2)) -> c_7(FLATTEN#(z1)) FLATTEN#1#(node(z0,z1,z2)) -> c_8(FLATTEN#(z2)) FLATTENSORT#(z0) -> c_9(INSERTIONSORT#(flatten(z0)),FLATTEN#(z0)) INSERTIONSORT#(z0) -> c_15(INSERTIONSORT#1#(z0)) INSERTIONSORT#1#(::(z0,z1)) -> c_16(INSERTIONSORT#(z1)) - Weak TRS: #cklt(#EQ()) -> #false() #cklt(#GT()) -> #false() #cklt(#LT()) -> #true() #compare(#0(),#0()) -> #EQ() #compare(#0(),#neg(z0)) -> #GT() #compare(#0(),#pos(z0)) -> #LT() #compare(#0(),#s(z0)) -> #LT() #compare(#neg(z0),#0()) -> #LT() #compare(#neg(z0),#neg(z1)) -> #compare(z1,z0) #compare(#neg(z0),#pos(z1)) -> #LT() #compare(#pos(z0),#0()) -> #GT() #compare(#pos(z0),#neg(z1)) -> #GT() #compare(#pos(z0),#pos(z1)) -> #compare(z0,z1) #compare(#s(z0),#0()) -> #GT() #compare(#s(z0),#s(z1)) -> #compare(z0,z1) #less(z0,z1) -> #cklt(#compare(z0,z1)) append(z0,z1) -> append#1(z0,z1) append#1(::(z0,z1),z2) -> ::(z0,append(z1,z2)) append#1(nil(),z0) -> z0 flatten(z0) -> flatten#1(z0) flatten#1(leaf()) -> nil() flatten#1(node(z0,z1,z2)) -> append(z0,append(flatten(z1),flatten(z2))) insert(z0,z1) -> insert#1(z1,z0) insert#1(::(z0,z1),z2) -> insert#2(#less(z0,z2),z2,z0,z1) insert#1(nil(),z0) -> ::(z0,nil()) insert#2(#false(),z0,z1,z2) -> ::(z0,::(z1,z2)) insert#2(#true(),z0,z1,z2) -> ::(z1,insert(z0,z2)) insertionsort(z0) -> insertionsort#1(z0) insertionsort#1(::(z0,z1)) -> insert(z0,insertionsort(z1)) insertionsort#1(nil()) -> nil() - Signature: {#CKLT/1,#COMPARE/2,#LESS/2,#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,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,#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,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,::/2,c/0,c1/0,c10/0,c11/0 ,c12/1,c13/0,c14/1,c15/2,c16/1,c17/1,c18/0,c19/1,c2/0,c20/0,c21/3,c22/3,c23/2,c24/1,c25/2,c26/0,c27/0,c28/1 ,c29/1,c3/0,c30/2,c31/0,c4/0,c5/0,c6/0,c7/0,c8/1,c9/0,leaf/0,nil/0,node/3,c_1/3,c_2/1,c_3/1,c_4/0,c_5/1 ,c_6/0,c_7/1,c_8/1,c_9/2,c_10/1,c_11/1,c_12/0,c_13/0,c_14/1,c_15/1,c_16/1,c_17/0,c_18/0,c_19/0,c_20/0,c_21/0 ,c_22/0,c_23/0,c_24/0,c_25/0,c_26/1,c_27/0,c_28/0,c_29/0,c_30/1,c_31/0,c_32/1,c_33/0,c_34/0,c_35/0,c_36/0 ,c_37/0,c_38/0,c_39/0,c_40/0,c_41/1,c_42/0,c_43/0,c_44/0,c_45/1,c_46/0,c_47/1,c_48/2,c_49/1,c_50/1,c_51/0 ,c_52/1,c_53/0,c_54/4,c_55/2,c_56/1,c_57/2,c_58/0,c_59/0,c_60/1,c_61/1,c_62/2,c_63/0} - Obligation: innermost runtime complexity wrt. defined symbols {#CKLT#,#COMPARE#,#LESS#,#cklt#,#compare#,#less#,APPEND# ,APPEND#1#,FLATTEN#,FLATTEN#1#,FLATTENSORT#,INSERT#,INSERT#1#,INSERT#2#,INSERTIONSORT#,INSERTIONSORT#1# ,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,::,c,c1,c10,c11,c12,c13,c14 ,c15,c16,c17,c18,c19,c2,c20,c21,c22,c23,c24,c25,c26,c27,c28,c29,c3,c30,c31,c4,c5,c6,c7,c8,c9,leaf,nil,node} + Applied Processor: UsableRules + Details: We replace rewrite rules by usable rules: append(z0,z1) -> append#1(z0,z1) append#1(::(z0,z1),z2) -> ::(z0,append(z1,z2)) append#1(nil(),z0) -> z0 flatten(z0) -> flatten#1(z0) flatten#1(leaf()) -> nil() flatten#1(node(z0,z1,z2)) -> append(z0,append(flatten(z1),flatten(z2))) FLATTEN#(z0) -> c_5(FLATTEN#1#(z0)) FLATTEN#1#(node(z0,z1,z2)) -> c_7(FLATTEN#(z1)) FLATTEN#1#(node(z0,z1,z2)) -> c_8(FLATTEN#(z2)) FLATTENSORT#(z0) -> c_9(INSERTIONSORT#(flatten(z0)),FLATTEN#(z0)) INSERTIONSORT#(z0) -> c_15(INSERTIONSORT#1#(z0)) INSERTIONSORT#1#(::(z0,z1)) -> c_16(INSERTIONSORT#(z1)) ** Step 7.a:3: WeightGap. WORST_CASE(?,O(n^1)) + Considered Problem: - Strict DPs: FLATTEN#(z0) -> c_5(FLATTEN#1#(z0)) FLATTEN#1#(node(z0,z1,z2)) -> c_7(FLATTEN#(z1)) FLATTEN#1#(node(z0,z1,z2)) -> c_8(FLATTEN#(z2)) FLATTENSORT#(z0) -> c_9(INSERTIONSORT#(flatten(z0)),FLATTEN#(z0)) INSERTIONSORT#(z0) -> c_15(INSERTIONSORT#1#(z0)) INSERTIONSORT#1#(::(z0,z1)) -> c_16(INSERTIONSORT#(z1)) - Weak TRS: append(z0,z1) -> append#1(z0,z1) append#1(::(z0,z1),z2) -> ::(z0,append(z1,z2)) append#1(nil(),z0) -> z0 flatten(z0) -> flatten#1(z0) flatten#1(leaf()) -> nil() flatten#1(node(z0,z1,z2)) -> append(z0,append(flatten(z1),flatten(z2))) - Signature: {#CKLT/1,#COMPARE/2,#LESS/2,#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,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,#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,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,::/2,c/0,c1/0,c10/0,c11/0 ,c12/1,c13/0,c14/1,c15/2,c16/1,c17/1,c18/0,c19/1,c2/0,c20/0,c21/3,c22/3,c23/2,c24/1,c25/2,c26/0,c27/0,c28/1 ,c29/1,c3/0,c30/2,c31/0,c4/0,c5/0,c6/0,c7/0,c8/1,c9/0,leaf/0,nil/0,node/3,c_1/3,c_2/1,c_3/1,c_4/0,c_5/1 ,c_6/0,c_7/1,c_8/1,c_9/2,c_10/1,c_11/1,c_12/0,c_13/0,c_14/1,c_15/1,c_16/1,c_17/0,c_18/0,c_19/0,c_20/0,c_21/0 ,c_22/0,c_23/0,c_24/0,c_25/0,c_26/1,c_27/0,c_28/0,c_29/0,c_30/1,c_31/0,c_32/1,c_33/0,c_34/0,c_35/0,c_36/0 ,c_37/0,c_38/0,c_39/0,c_40/0,c_41/1,c_42/0,c_43/0,c_44/0,c_45/1,c_46/0,c_47/1,c_48/2,c_49/1,c_50/1,c_51/0 ,c_52/1,c_53/0,c_54/4,c_55/2,c_56/1,c_57/2,c_58/0,c_59/0,c_60/1,c_61/1,c_62/2,c_63/0} - Obligation: innermost runtime complexity wrt. defined symbols {#CKLT#,#COMPARE#,#LESS#,#cklt#,#compare#,#less#,APPEND# ,APPEND#1#,FLATTEN#,FLATTEN#1#,FLATTENSORT#,INSERT#,INSERT#1#,INSERT#2#,INSERTIONSORT#,INSERTIONSORT#1# ,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,::,c,c1,c10,c11,c12,c13,c14 ,c15,c16,c17,c18,c19,c2,c20,c21,c22,c23,c24,c25,c26,c27,c28,c29,c3,c30,c31,c4,c5,c6,c7,c8,c9,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(::) = {2}, uargs(append) = {1,2}, uargs(INSERTIONSORT#) = {1}, uargs(c_5) = {1}, uargs(c_7) = {1}, uargs(c_8) = {1}, uargs(c_9) = {1,2}, uargs(c_15) = {1}, uargs(c_16) = {1} Following symbols are considered usable: all TcT has computed the following interpretation: p(#0) = [0] p(#CKLT) = [0] p(#COMPARE) = [0] p(#EQ) = [0] p(#GT) = [0] p(#LESS) = [0] p(#LT) = [0] p(#cklt) = [0] p(#compare) = [1] 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(::) = [1] x2 + [2] p(APPEND) = [0] p(APPEND#1) = [0] p(FLATTEN) = [2] p(FLATTEN#1) = [0] p(FLATTENSORT) = [0] p(INSERT) = [0] p(INSERT#1) = [0] p(INSERT#2) = [0] p(INSERTIONSORT) = [0] p(INSERTIONSORT#1) = [0] p(append) = [1] x1 + [1] x2 + [2] p(append#1) = [1] x1 + [1] x2 + [2] p(c) = [0] p(c1) = [0] p(c10) = [0] p(c11) = [0] p(c12) = [4] p(c13) = [1] p(c14) = [2] p(c15) = [0] p(c16) = [1] x1 + [4] p(c17) = [1] x1 + [4] p(c18) = [0] p(c19) = [1] x1 + [0] p(c2) = [0] p(c20) = [0] p(c21) = [1] x2 + [1] x3 + [0] p(c22) = [1] x2 + [1] p(c23) = [1] p(c24) = [1] x1 + [0] p(c25) = [1] x1 + [1] p(c26) = [1] p(c27) = [0] p(c28) = [0] p(c29) = [0] p(c3) = [1] p(c30) = [1] x2 + [0] p(c31) = [1] p(c4) = [0] p(c5) = [0] p(c6) = [0] p(c7) = [1] p(c8) = [1] p(c9) = [4] p(flatten) = [2] x1 + [1] p(flatten#1) = [2] x1 + [1] p(flattensort) = [1] x1 + [1] p(insert) = [4] x1 + [2] x2 + [0] p(insert#1) = [0] p(insert#2) = [2] x1 + [4] x3 + [1] x4 + [0] p(insertionsort) = [0] p(insertionsort#1) = [0] p(leaf) = [0] p(nil) = [0] p(node) = [1] x1 + [1] x2 + [1] x3 + [5] p(#CKLT#) = [0] p(#COMPARE#) = [2] p(#LESS#) = [0] p(#cklt#) = [0] p(#compare#) = [0] p(#less#) = [0] p(APPEND#) = [0] p(APPEND#1#) = [0] p(FLATTEN#) = [7] p(FLATTEN#1#) = [7] p(FLATTENSORT#) = [2] x1 + [1] p(INSERT#) = [0] p(INSERT#1#) = [0] p(INSERT#2#) = [0] p(INSERTIONSORT#) = [1] x1 + [0] p(INSERTIONSORT#1#) = [1] x1 + [4] p(append#) = [0] p(append#1#) = [0] p(flatten#) = [0] p(flatten#1#) = [0] p(flattensort#) = [0] p(insert#) = [0] p(insert#1#) = [0] p(insert#2#) = [0] p(insertionsort#) = [0] p(insertionsort#1#) = [0] p(c_1) = [0] p(c_2) = [0] p(c_3) = [0] p(c_4) = [0] p(c_5) = [1] x1 + [0] p(c_6) = [0] p(c_7) = [1] x1 + [4] p(c_8) = [1] x1 + [0] p(c_9) = [1] x1 + [1] x2 + [4] p(c_10) = [0] p(c_11) = [0] p(c_12) = [2] p(c_13) = [0] p(c_14) = [1] x1 + [0] p(c_15) = [1] x1 + [1] p(c_16) = [1] x1 + [0] p(c_17) = [0] p(c_18) = [0] p(c_19) = [0] p(c_20) = [0] p(c_21) = [0] p(c_22) = [0] p(c_23) = [0] p(c_24) = [0] p(c_25) = [0] p(c_26) = [0] p(c_27) = [0] p(c_28) = [0] p(c_29) = [0] p(c_30) = [0] p(c_31) = [0] p(c_32) = [0] p(c_33) = [0] p(c_34) = [0] p(c_35) = [0] p(c_36) = [0] p(c_37) = [0] p(c_38) = [0] p(c_39) = [0] p(c_40) = [0] p(c_41) = [0] p(c_42) = [0] p(c_43) = [0] p(c_44) = [0] p(c_45) = [0] p(c_46) = [0] p(c_47) = [0] p(c_48) = [0] p(c_49) = [0] p(c_50) = [0] p(c_51) = [0] p(c_52) = [0] p(c_53) = [0] p(c_54) = [0] p(c_55) = [0] p(c_56) = [0] p(c_57) = [0] p(c_58) = [0] p(c_59) = [0] p(c_60) = [0] p(c_61) = [0] p(c_62) = [0] p(c_63) = [0] Following rules are strictly oriented: INSERTIONSORT#1#(::(z0,z1)) = [1] z1 + [6] > [1] z1 + [0] = c_16(INSERTIONSORT#(z1)) Following rules are (at-least) weakly oriented: FLATTEN#(z0) = [7] >= [7] = c_5(FLATTEN#1#(z0)) FLATTEN#1#(node(z0,z1,z2)) = [7] >= [11] = c_7(FLATTEN#(z1)) FLATTEN#1#(node(z0,z1,z2)) = [7] >= [7] = c_8(FLATTEN#(z2)) FLATTENSORT#(z0) = [2] z0 + [1] >= [2] z0 + [12] = c_9(INSERTIONSORT#(flatten(z0)),FLATTEN#(z0)) INSERTIONSORT#(z0) = [1] z0 + [0] >= [1] z0 + [5] = c_15(INSERTIONSORT#1#(z0)) append(z0,z1) = [1] z0 + [1] z1 + [2] >= [1] z0 + [1] z1 + [2] = append#1(z0,z1) append#1(::(z0,z1),z2) = [1] z1 + [1] z2 + [4] >= [1] z1 + [1] z2 + [4] = ::(z0,append(z1,z2)) append#1(nil(),z0) = [1] z0 + [2] >= [1] z0 + [0] = z0 flatten(z0) = [2] z0 + [1] >= [2] z0 + [1] = flatten#1(z0) flatten#1(leaf()) = [1] >= [0] = nil() flatten#1(node(z0,z1,z2)) = [2] z0 + [2] z1 + [2] z2 + [11] >= [1] z0 + [2] z1 + [2] z2 + [6] = append(z0,append(flatten(z1),flatten(z2))) Further, it can be verified that all rules not oriented are covered by the weightgap condition. ** Step 7.a:4: NaturalMI. WORST_CASE(?,O(n^1)) + Considered Problem: - Strict DPs: FLATTEN#(z0) -> c_5(FLATTEN#1#(z0)) FLATTEN#1#(node(z0,z1,z2)) -> c_7(FLATTEN#(z1)) FLATTEN#1#(node(z0,z1,z2)) -> c_8(FLATTEN#(z2)) FLATTENSORT#(z0) -> c_9(INSERTIONSORT#(flatten(z0)),FLATTEN#(z0)) INSERTIONSORT#(z0) -> c_15(INSERTIONSORT#1#(z0)) - Weak DPs: INSERTIONSORT#1#(::(z0,z1)) -> c_16(INSERTIONSORT#(z1)) - Weak TRS: append(z0,z1) -> append#1(z0,z1) append#1(::(z0,z1),z2) -> ::(z0,append(z1,z2)) append#1(nil(),z0) -> z0 flatten(z0) -> flatten#1(z0) flatten#1(leaf()) -> nil() flatten#1(node(z0,z1,z2)) -> append(z0,append(flatten(z1),flatten(z2))) - Signature: {#CKLT/1,#COMPARE/2,#LESS/2,#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,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,#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,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,::/2,c/0,c1/0,c10/0,c11/0 ,c12/1,c13/0,c14/1,c15/2,c16/1,c17/1,c18/0,c19/1,c2/0,c20/0,c21/3,c22/3,c23/2,c24/1,c25/2,c26/0,c27/0,c28/1 ,c29/1,c3/0,c30/2,c31/0,c4/0,c5/0,c6/0,c7/0,c8/1,c9/0,leaf/0,nil/0,node/3,c_1/3,c_2/1,c_3/1,c_4/0,c_5/1 ,c_6/0,c_7/1,c_8/1,c_9/2,c_10/1,c_11/1,c_12/0,c_13/0,c_14/1,c_15/1,c_16/1,c_17/0,c_18/0,c_19/0,c_20/0,c_21/0 ,c_22/0,c_23/0,c_24/0,c_25/0,c_26/1,c_27/0,c_28/0,c_29/0,c_30/1,c_31/0,c_32/1,c_33/0,c_34/0,c_35/0,c_36/0 ,c_37/0,c_38/0,c_39/0,c_40/0,c_41/1,c_42/0,c_43/0,c_44/0,c_45/1,c_46/0,c_47/1,c_48/2,c_49/1,c_50/1,c_51/0 ,c_52/1,c_53/0,c_54/4,c_55/2,c_56/1,c_57/2,c_58/0,c_59/0,c_60/1,c_61/1,c_62/2,c_63/0} - Obligation: innermost runtime complexity wrt. defined symbols {#CKLT#,#COMPARE#,#LESS#,#cklt#,#compare#,#less#,APPEND# ,APPEND#1#,FLATTEN#,FLATTEN#1#,FLATTENSORT#,INSERT#,INSERT#1#,INSERT#2#,INSERTIONSORT#,INSERTIONSORT#1# ,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,::,c,c1,c10,c11,c12,c13,c14 ,c15,c16,c17,c18,c19,c2,c20,c21,c22,c23,c24,c25,c26,c27,c28,c29,c3,c30,c31,c4,c5,c6,c7,c8,c9,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_5) = {1}, uargs(c_7) = {1}, uargs(c_8) = {1}, uargs(c_9) = {1,2}, uargs(c_15) = {1}, uargs(c_16) = {1} Following symbols are considered usable: {#CKLT#,#COMPARE#,#LESS#,#cklt#,#compare#,#less#,APPEND#,APPEND#1#,FLATTEN#,FLATTEN#1#,FLATTENSORT# ,INSERT#,INSERT#1#,INSERT#2#,INSERTIONSORT#,INSERTIONSORT#1#,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(#CKLT) = [0] p(#COMPARE) = [0] p(#EQ) = [0] p(#GT) = [0] p(#LESS) = [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(::) = [1] x1 + [3] p(APPEND) = [0] p(APPEND#1) = [0] p(FLATTEN) = [0] p(FLATTEN#1) = [0] p(FLATTENSORT) = [0] p(INSERT) = [0] p(INSERT#1) = [0] p(INSERT#2) = [0] p(INSERTIONSORT) = [0] p(INSERTIONSORT#1) = [0] p(append) = [0] p(append#1) = [6] x1 + [0] p(c) = [0] p(c1) = [0] p(c10) = [0] p(c11) = [0] p(c12) = [1] x1 + [0] p(c13) = [0] p(c14) = [1] x1 + [0] p(c15) = [1] x1 + [1] x2 + [0] p(c16) = [1] x1 + [0] p(c17) = [1] x1 + [0] p(c18) = [0] p(c19) = [1] x1 + [0] p(c2) = [0] p(c20) = [0] p(c21) = [1] x1 + [1] x2 + [1] x3 + [0] p(c22) = [1] x1 + [1] x2 + [1] x3 + [0] p(c23) = [1] x1 + [1] x2 + [0] p(c24) = [1] x1 + [0] p(c25) = [1] x1 + [1] x2 + [0] p(c26) = [0] p(c27) = [0] p(c28) = [1] x1 + [0] p(c29) = [1] x1 + [0] p(c3) = [0] p(c30) = [1] x1 + [1] x2 + [0] p(c31) = [0] p(c4) = [0] p(c5) = [0] p(c6) = [0] p(c7) = [0] p(c8) = [1] x1 + [0] p(c9) = [0] p(flatten) = [0] p(flatten#1) = [4] x1 + [6] 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 + [5] p(#CKLT#) = [0] p(#COMPARE#) = [0] p(#LESS#) = [0] p(#cklt#) = [0] p(#compare#) = [0] p(#less#) = [0] p(APPEND#) = [0] p(APPEND#1#) = [1] x2 + [0] p(FLATTEN#) = [4] x1 + [0] p(FLATTEN#1#) = [4] x1 + [0] p(FLATTENSORT#) = [8] x1 + [4] p(INSERT#) = [0] p(INSERT#1#) = [0] p(INSERT#2#) = [0] p(INSERTIONSORT#) = [0] p(INSERTIONSORT#1#) = [0] p(append#) = [0] p(append#1#) = [0] p(flatten#) = [0] p(flatten#1#) = [0] p(flattensort#) = [0] p(insert#) = [1] x1 + [0] p(insert#1#) = [4] x1 + [1] x2 + [8] p(insert#2#) = [1] x1 + [1] x2 + [1] x4 + [1] p(insertionsort#) = [2] x1 + [1] p(insertionsort#1#) = [1] x1 + [0] p(c_1) = [2] x2 + [1] x3 + [0] p(c_2) = [0] p(c_3) = [2] p(c_4) = [1] p(c_5) = [1] x1 + [0] p(c_6) = [2] p(c_7) = [1] x1 + [12] p(c_8) = [1] x1 + [8] p(c_9) = [4] x1 + [1] x2 + [4] p(c_10) = [1] p(c_11) = [0] p(c_12) = [1] p(c_13) = [1] p(c_14) = [1] x1 + [1] p(c_15) = [8] x1 + [0] p(c_16) = [4] x1 + [0] p(c_17) = [0] p(c_18) = [1] p(c_19) = [1] p(c_20) = [1] p(c_21) = [1] p(c_22) = [1] p(c_23) = [8] p(c_24) = [0] p(c_25) = [0] p(c_26) = [2] x1 + [1] p(c_27) = [1] p(c_28) = [2] p(c_29) = [4] p(c_30) = [1] x1 + [0] p(c_31) = [1] p(c_32) = [1] x1 + [2] p(c_33) = [1] p(c_34) = [1] p(c_35) = [1] p(c_36) = [0] p(c_37) = [0] p(c_38) = [0] p(c_39) = [1] p(c_40) = [2] p(c_41) = [1] x1 + [1] p(c_42) = [0] p(c_43) = [0] p(c_44) = [1] p(c_45) = [1] p(c_46) = [1] p(c_47) = [1] p(c_48) = [1] x1 + [1] x2 + [0] p(c_49) = [1] p(c_50) = [0] p(c_51) = [1] p(c_52) = [8] x1 + [1] p(c_53) = [1] p(c_54) = [2] x2 + [1] x3 + [2] x4 + [1] p(c_55) = [1] x1 + [0] p(c_56) = [1] p(c_57) = [1] x1 + [4] x2 + [1] p(c_58) = [8] p(c_59) = [1] p(c_60) = [4] x1 + [1] p(c_61) = [1] x1 + [0] p(c_62) = [1] x1 + [2] x2 + [0] p(c_63) = [0] Following rules are strictly oriented: FLATTEN#1#(node(z0,z1,z2)) = [4] z0 + [4] z1 + [4] z2 + [20] > [4] z1 + [12] = c_7(FLATTEN#(z1)) FLATTEN#1#(node(z0,z1,z2)) = [4] z0 + [4] z1 + [4] z2 + [20] > [4] z2 + [8] = c_8(FLATTEN#(z2)) Following rules are (at-least) weakly oriented: FLATTEN#(z0) = [4] z0 + [0] >= [4] z0 + [0] = c_5(FLATTEN#1#(z0)) FLATTENSORT#(z0) = [8] z0 + [4] >= [4] z0 + [4] = c_9(INSERTIONSORT#(flatten(z0)),FLATTEN#(z0)) INSERTIONSORT#(z0) = [0] >= [0] = c_15(INSERTIONSORT#1#(z0)) INSERTIONSORT#1#(::(z0,z1)) = [0] >= [0] = c_16(INSERTIONSORT#(z1)) ** Step 7.a:5: NaturalMI. WORST_CASE(?,O(n^1)) + Considered Problem: - Strict DPs: FLATTEN#(z0) -> c_5(FLATTEN#1#(z0)) FLATTENSORT#(z0) -> c_9(INSERTIONSORT#(flatten(z0)),FLATTEN#(z0)) INSERTIONSORT#(z0) -> c_15(INSERTIONSORT#1#(z0)) - Weak DPs: FLATTEN#1#(node(z0,z1,z2)) -> c_7(FLATTEN#(z1)) FLATTEN#1#(node(z0,z1,z2)) -> c_8(FLATTEN#(z2)) INSERTIONSORT#1#(::(z0,z1)) -> c_16(INSERTIONSORT#(z1)) - Weak TRS: append(z0,z1) -> append#1(z0,z1) append#1(::(z0,z1),z2) -> ::(z0,append(z1,z2)) append#1(nil(),z0) -> z0 flatten(z0) -> flatten#1(z0) flatten#1(leaf()) -> nil() flatten#1(node(z0,z1,z2)) -> append(z0,append(flatten(z1),flatten(z2))) - Signature: {#CKLT/1,#COMPARE/2,#LESS/2,#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,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,#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,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,::/2,c/0,c1/0,c10/0,c11/0 ,c12/1,c13/0,c14/1,c15/2,c16/1,c17/1,c18/0,c19/1,c2/0,c20/0,c21/3,c22/3,c23/2,c24/1,c25/2,c26/0,c27/0,c28/1 ,c29/1,c3/0,c30/2,c31/0,c4/0,c5/0,c6/0,c7/0,c8/1,c9/0,leaf/0,nil/0,node/3,c_1/3,c_2/1,c_3/1,c_4/0,c_5/1 ,c_6/0,c_7/1,c_8/1,c_9/2,c_10/1,c_11/1,c_12/0,c_13/0,c_14/1,c_15/1,c_16/1,c_17/0,c_18/0,c_19/0,c_20/0,c_21/0 ,c_22/0,c_23/0,c_24/0,c_25/0,c_26/1,c_27/0,c_28/0,c_29/0,c_30/1,c_31/0,c_32/1,c_33/0,c_34/0,c_35/0,c_36/0 ,c_37/0,c_38/0,c_39/0,c_40/0,c_41/1,c_42/0,c_43/0,c_44/0,c_45/1,c_46/0,c_47/1,c_48/2,c_49/1,c_50/1,c_51/0 ,c_52/1,c_53/0,c_54/4,c_55/2,c_56/1,c_57/2,c_58/0,c_59/0,c_60/1,c_61/1,c_62/2,c_63/0} - Obligation: innermost runtime complexity wrt. defined symbols {#CKLT#,#COMPARE#,#LESS#,#cklt#,#compare#,#less#,APPEND# ,APPEND#1#,FLATTEN#,FLATTEN#1#,FLATTENSORT#,INSERT#,INSERT#1#,INSERT#2#,INSERTIONSORT#,INSERTIONSORT#1# ,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,::,c,c1,c10,c11,c12,c13,c14 ,c15,c16,c17,c18,c19,c2,c20,c21,c22,c23,c24,c25,c26,c27,c28,c29,c3,c30,c31,c4,c5,c6,c7,c8,c9,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_5) = {1}, uargs(c_7) = {1}, uargs(c_8) = {1}, uargs(c_9) = {1,2}, uargs(c_15) = {1}, uargs(c_16) = {1} Following symbols are considered usable: {#CKLT#,#COMPARE#,#LESS#,#cklt#,#compare#,#less#,APPEND#,APPEND#1#,FLATTEN#,FLATTEN#1#,FLATTENSORT# ,INSERT#,INSERT#1#,INSERT#2#,INSERTIONSORT#,INSERTIONSORT#1#,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(#CKLT) = [0] p(#COMPARE) = [0] p(#EQ) = [0] p(#GT) = [0] p(#LESS) = [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(::) = [1] x1 + [0] p(APPEND) = [0] p(APPEND#1) = [0] p(FLATTEN) = [0] p(FLATTEN#1) = [0] p(FLATTENSORT) = [0] p(INSERT) = [0] p(INSERT#1) = [0] p(INSERT#2) = [0] p(INSERTIONSORT) = [0] p(INSERTIONSORT#1) = [0] p(append) = [2] x1 + [0] p(append#1) = [0] p(c) = [0] p(c1) = [0] p(c10) = [0] p(c11) = [0] p(c12) = [0] p(c13) = [0] p(c14) = [0] p(c15) = [0] p(c16) = [0] p(c17) = [0] p(c18) = [0] p(c19) = [0] p(c2) = [0] p(c20) = [0] p(c21) = [0] p(c22) = [0] p(c23) = [0] p(c24) = [0] p(c25) = [0] p(c26) = [0] p(c27) = [0] p(c28) = [0] p(c29) = [0] p(c3) = [0] p(c30) = [0] p(c31) = [0] p(c4) = [0] p(c5) = [0] p(c6) = [0] p(c7) = [0] p(c8) = [0] p(c9) = [0] p(flatten) = [14] p(flatten#1) = [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) = [0] p(#CKLT#) = [0] p(#COMPARE#) = [0] p(#LESS#) = [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#) = [4] p(INSERT#) = [0] p(INSERT#1#) = [0] p(INSERT#2#) = [0] p(INSERTIONSORT#) = [0] p(INSERTIONSORT#1#) = [0] p(append#) = [0] p(append#1#) = [0] p(flatten#) = [0] p(flatten#1#) = [0] p(flattensort#) = [0] p(insert#) = [0] p(insert#1#) = [0] p(insert#2#) = [0] p(insertionsort#) = [0] p(insertionsort#1#) = [0] p(c_1) = [0] p(c_2) = [0] p(c_3) = [0] p(c_4) = [2] p(c_5) = [1] x1 + [0] p(c_6) = [1] p(c_7) = [8] x1 + [0] p(c_8) = [1] x1 + [0] p(c_9) = [1] x1 + [1] x2 + [2] p(c_10) = [0] p(c_11) = [0] p(c_12) = [0] p(c_13) = [0] p(c_14) = [0] p(c_15) = [1] x1 + [0] p(c_16) = [1] x1 + [0] p(c_17) = [0] p(c_18) = [0] p(c_19) = [0] p(c_20) = [0] p(c_21) = [0] p(c_22) = [0] p(c_23) = [0] p(c_24) = [0] p(c_25) = [0] p(c_26) = [0] p(c_27) = [0] p(c_28) = [0] p(c_29) = [0] p(c_30) = [0] p(c_31) = [0] p(c_32) = [0] p(c_33) = [0] p(c_34) = [0] p(c_35) = [0] p(c_36) = [0] p(c_37) = [0] p(c_38) = [0] p(c_39) = [0] p(c_40) = [0] p(c_41) = [0] p(c_42) = [0] p(c_43) = [0] p(c_44) = [0] p(c_45) = [0] p(c_46) = [0] p(c_47) = [0] p(c_48) = [0] p(c_49) = [0] p(c_50) = [0] p(c_51) = [0] p(c_52) = [0] p(c_53) = [2] p(c_54) = [1] p(c_55) = [0] p(c_56) = [0] p(c_57) = [1] p(c_58) = [1] p(c_59) = [8] p(c_60) = [0] p(c_61) = [1] p(c_62) = [0] p(c_63) = [0] Following rules are strictly oriented: FLATTENSORT#(z0) = [4] > [2] = c_9(INSERTIONSORT#(flatten(z0)),FLATTEN#(z0)) Following rules are (at-least) weakly oriented: FLATTEN#(z0) = [0] >= [0] = c_5(FLATTEN#1#(z0)) FLATTEN#1#(node(z0,z1,z2)) = [0] >= [0] = c_7(FLATTEN#(z1)) FLATTEN#1#(node(z0,z1,z2)) = [0] >= [0] = c_8(FLATTEN#(z2)) INSERTIONSORT#(z0) = [0] >= [0] = c_15(INSERTIONSORT#1#(z0)) INSERTIONSORT#1#(::(z0,z1)) = [0] >= [0] = c_16(INSERTIONSORT#(z1)) ** Step 7.a:6: WeightGap. WORST_CASE(?,O(n^1)) + Considered Problem: - Strict DPs: FLATTEN#(z0) -> c_5(FLATTEN#1#(z0)) INSERTIONSORT#(z0) -> c_15(INSERTIONSORT#1#(z0)) - Weak DPs: FLATTEN#1#(node(z0,z1,z2)) -> c_7(FLATTEN#(z1)) FLATTEN#1#(node(z0,z1,z2)) -> c_8(FLATTEN#(z2)) FLATTENSORT#(z0) -> c_9(INSERTIONSORT#(flatten(z0)),FLATTEN#(z0)) INSERTIONSORT#1#(::(z0,z1)) -> c_16(INSERTIONSORT#(z1)) - Weak TRS: append(z0,z1) -> append#1(z0,z1) append#1(::(z0,z1),z2) -> ::(z0,append(z1,z2)) append#1(nil(),z0) -> z0 flatten(z0) -> flatten#1(z0) flatten#1(leaf()) -> nil() flatten#1(node(z0,z1,z2)) -> append(z0,append(flatten(z1),flatten(z2))) - Signature: {#CKLT/1,#COMPARE/2,#LESS/2,#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,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,#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,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,::/2,c/0,c1/0,c10/0,c11/0 ,c12/1,c13/0,c14/1,c15/2,c16/1,c17/1,c18/0,c19/1,c2/0,c20/0,c21/3,c22/3,c23/2,c24/1,c25/2,c26/0,c27/0,c28/1 ,c29/1,c3/0,c30/2,c31/0,c4/0,c5/0,c6/0,c7/0,c8/1,c9/0,leaf/0,nil/0,node/3,c_1/3,c_2/1,c_3/1,c_4/0,c_5/1 ,c_6/0,c_7/1,c_8/1,c_9/2,c_10/1,c_11/1,c_12/0,c_13/0,c_14/1,c_15/1,c_16/1,c_17/0,c_18/0,c_19/0,c_20/0,c_21/0 ,c_22/0,c_23/0,c_24/0,c_25/0,c_26/1,c_27/0,c_28/0,c_29/0,c_30/1,c_31/0,c_32/1,c_33/0,c_34/0,c_35/0,c_36/0 ,c_37/0,c_38/0,c_39/0,c_40/0,c_41/1,c_42/0,c_43/0,c_44/0,c_45/1,c_46/0,c_47/1,c_48/2,c_49/1,c_50/1,c_51/0 ,c_52/1,c_53/0,c_54/4,c_55/2,c_56/1,c_57/2,c_58/0,c_59/0,c_60/1,c_61/1,c_62/2,c_63/0} - Obligation: innermost runtime complexity wrt. defined symbols {#CKLT#,#COMPARE#,#LESS#,#cklt#,#compare#,#less#,APPEND# ,APPEND#1#,FLATTEN#,FLATTEN#1#,FLATTENSORT#,INSERT#,INSERT#1#,INSERT#2#,INSERTIONSORT#,INSERTIONSORT#1# ,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,::,c,c1,c10,c11,c12,c13,c14 ,c15,c16,c17,c18,c19,c2,c20,c21,c22,c23,c24,c25,c26,c27,c28,c29,c3,c30,c31,c4,c5,c6,c7,c8,c9,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(::) = {2}, uargs(append) = {1,2}, uargs(INSERTIONSORT#) = {1}, uargs(c_5) = {1}, uargs(c_7) = {1}, uargs(c_8) = {1}, uargs(c_9) = {1,2}, uargs(c_15) = {1}, uargs(c_16) = {1} Following symbols are considered usable: all TcT has computed the following interpretation: p(#0) = [0] p(#CKLT) = [0] p(#COMPARE) = [0] p(#EQ) = [0] p(#GT) = [0] p(#LESS) = [4] x2 + [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(::) = [1] x2 + [5] p(APPEND) = [0] p(APPEND#1) = [0] p(FLATTEN) = [0] p(FLATTEN#1) = [0] p(FLATTENSORT) = [0] p(INSERT) = [0] p(INSERT#1) = [0] p(INSERT#2) = [1] x1 + [1] x2 + [1] x3 + [2] x4 + [0] p(INSERTIONSORT) = [4] x1 + [1] p(INSERTIONSORT#1) = [0] p(append) = [1] x1 + [1] x2 + [0] p(append#1) = [1] x1 + [1] x2 + [0] p(c) = [4] p(c1) = [1] p(c10) = [1] p(c11) = [0] p(c12) = [0] p(c13) = [1] p(c14) = [1] x1 + [4] p(c15) = [1] x1 + [2] p(c16) = [1] x1 + [2] p(c17) = [2] p(c18) = [1] p(c19) = [1] x1 + [1] p(c2) = [1] p(c20) = [0] p(c21) = [1] x2 + [1] x3 + [0] p(c22) = [1] x2 + [1] x3 + [0] p(c23) = [1] x1 + [1] x2 + [0] p(c24) = [1] x1 + [2] p(c25) = [1] x1 + [1] x2 + [0] p(c26) = [0] p(c27) = [0] p(c28) = [1] x1 + [0] p(c29) = [1] x1 + [0] p(c3) = [0] p(c30) = [1] x1 + [1] x2 + [0] p(c31) = [0] p(c4) = [0] p(c5) = [0] p(c6) = [0] p(c7) = [0] p(c8) = [1] x1 + [0] p(c9) = [0] p(flatten) = [1] x1 + [1] 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) = [7] p(nil) = [7] p(node) = [1] x1 + [1] x2 + [1] x3 + [2] p(#CKLT#) = [0] p(#COMPARE#) = [0] p(#LESS#) = [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#) = [4] x1 + [7] p(INSERT#) = [0] p(INSERT#1#) = [0] p(INSERT#2#) = [0] p(INSERTIONSORT#) = [1] x1 + [4] p(INSERTIONSORT#1#) = [1] x1 + [0] p(append#) = [0] p(append#1#) = [0] p(flatten#) = [0] p(flatten#1#) = [0] p(flattensort#) = [0] p(insert#) = [0] p(insert#1#) = [0] p(insert#2#) = [0] p(insertionsort#) = [0] p(insertionsort#1#) = [0] p(c_1) = [0] p(c_2) = [0] p(c_3) = [0] p(c_4) = [0] p(c_5) = [1] x1 + [7] p(c_6) = [0] p(c_7) = [1] x1 + [0] p(c_8) = [1] x1 + [0] p(c_9) = [1] x1 + [1] x2 + [2] p(c_10) = [0] p(c_11) = [0] p(c_12) = [0] p(c_13) = [0] p(c_14) = [2] x1 + [0] p(c_15) = [1] x1 + [0] p(c_16) = [1] x1 + [1] p(c_17) = [0] p(c_18) = [0] p(c_19) = [0] p(c_20) = [0] p(c_21) = [0] p(c_22) = [0] p(c_23) = [0] p(c_24) = [0] p(c_25) = [0] p(c_26) = [0] p(c_27) = [0] p(c_28) = [0] p(c_29) = [0] p(c_30) = [0] p(c_31) = [0] p(c_32) = [0] p(c_33) = [0] p(c_34) = [0] p(c_35) = [0] p(c_36) = [0] p(c_37) = [0] p(c_38) = [0] p(c_39) = [0] p(c_40) = [0] p(c_41) = [0] p(c_42) = [0] p(c_43) = [1] p(c_44) = [0] p(c_45) = [1] x1 + [0] p(c_46) = [0] p(c_47) = [0] p(c_48) = [2] p(c_49) = [1] p(c_50) = [0] p(c_51) = [0] p(c_52) = [1] p(c_53) = [0] p(c_54) = [2] x2 + [1] p(c_55) = [1] x1 + [1] p(c_56) = [0] p(c_57) = [1] x1 + [0] p(c_58) = [0] p(c_59) = [1] p(c_60) = [1] x1 + [0] p(c_61) = [1] x1 + [1] p(c_62) = [4] x2 + [1] p(c_63) = [0] Following rules are strictly oriented: INSERTIONSORT#(z0) = [1] z0 + [4] > [1] z0 + [0] = c_15(INSERTIONSORT#1#(z0)) Following rules are (at-least) weakly oriented: FLATTEN#(z0) = [0] >= [7] = c_5(FLATTEN#1#(z0)) FLATTEN#1#(node(z0,z1,z2)) = [0] >= [0] = c_7(FLATTEN#(z1)) FLATTEN#1#(node(z0,z1,z2)) = [0] >= [0] = c_8(FLATTEN#(z2)) FLATTENSORT#(z0) = [4] z0 + [7] >= [1] z0 + [7] = c_9(INSERTIONSORT#(flatten(z0)),FLATTEN#(z0)) INSERTIONSORT#1#(::(z0,z1)) = [1] z1 + [5] >= [1] z1 + [5] = c_16(INSERTIONSORT#(z1)) append(z0,z1) = [1] z0 + [1] z1 + [0] >= [1] z0 + [1] z1 + [0] = append#1(z0,z1) append#1(::(z0,z1),z2) = [1] z1 + [1] z2 + [5] >= [1] z1 + [1] z2 + [5] = ::(z0,append(z1,z2)) append#1(nil(),z0) = [1] z0 + [7] >= [1] z0 + [0] = z0 flatten(z0) = [1] z0 + [1] >= [1] z0 + [0] = flatten#1(z0) flatten#1(leaf()) = [7] >= [7] = nil() flatten#1(node(z0,z1,z2)) = [1] z0 + [1] z1 + [1] z2 + [2] >= [1] z0 + [1] z1 + [1] z2 + [2] = append(z0,append(flatten(z1),flatten(z2))) Further, it can be verified that all rules not oriented are covered by the weightgap condition. ** Step 7.a:7: WeightGap. WORST_CASE(?,O(n^1)) + Considered Problem: - Strict DPs: FLATTEN#(z0) -> c_5(FLATTEN#1#(z0)) - Weak DPs: FLATTEN#1#(node(z0,z1,z2)) -> c_7(FLATTEN#(z1)) FLATTEN#1#(node(z0,z1,z2)) -> c_8(FLATTEN#(z2)) FLATTENSORT#(z0) -> c_9(INSERTIONSORT#(flatten(z0)),FLATTEN#(z0)) INSERTIONSORT#(z0) -> c_15(INSERTIONSORT#1#(z0)) INSERTIONSORT#1#(::(z0,z1)) -> c_16(INSERTIONSORT#(z1)) - Weak TRS: append(z0,z1) -> append#1(z0,z1) append#1(::(z0,z1),z2) -> ::(z0,append(z1,z2)) append#1(nil(),z0) -> z0 flatten(z0) -> flatten#1(z0) flatten#1(leaf()) -> nil() flatten#1(node(z0,z1,z2)) -> append(z0,append(flatten(z1),flatten(z2))) - Signature: {#CKLT/1,#COMPARE/2,#LESS/2,#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,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,#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,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,::/2,c/0,c1/0,c10/0,c11/0 ,c12/1,c13/0,c14/1,c15/2,c16/1,c17/1,c18/0,c19/1,c2/0,c20/0,c21/3,c22/3,c23/2,c24/1,c25/2,c26/0,c27/0,c28/1 ,c29/1,c3/0,c30/2,c31/0,c4/0,c5/0,c6/0,c7/0,c8/1,c9/0,leaf/0,nil/0,node/3,c_1/3,c_2/1,c_3/1,c_4/0,c_5/1 ,c_6/0,c_7/1,c_8/1,c_9/2,c_10/1,c_11/1,c_12/0,c_13/0,c_14/1,c_15/1,c_16/1,c_17/0,c_18/0,c_19/0,c_20/0,c_21/0 ,c_22/0,c_23/0,c_24/0,c_25/0,c_26/1,c_27/0,c_28/0,c_29/0,c_30/1,c_31/0,c_32/1,c_33/0,c_34/0,c_35/0,c_36/0 ,c_37/0,c_38/0,c_39/0,c_40/0,c_41/1,c_42/0,c_43/0,c_44/0,c_45/1,c_46/0,c_47/1,c_48/2,c_49/1,c_50/1,c_51/0 ,c_52/1,c_53/0,c_54/4,c_55/2,c_56/1,c_57/2,c_58/0,c_59/0,c_60/1,c_61/1,c_62/2,c_63/0} - Obligation: innermost runtime complexity wrt. defined symbols {#CKLT#,#COMPARE#,#LESS#,#cklt#,#compare#,#less#,APPEND# ,APPEND#1#,FLATTEN#,FLATTEN#1#,FLATTENSORT#,INSERT#,INSERT#1#,INSERT#2#,INSERTIONSORT#,INSERTIONSORT#1# ,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,::,c,c1,c10,c11,c12,c13,c14 ,c15,c16,c17,c18,c19,c2,c20,c21,c22,c23,c24,c25,c26,c27,c28,c29,c3,c30,c31,c4,c5,c6,c7,c8,c9,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(::) = {2}, uargs(append) = {1,2}, uargs(INSERTIONSORT#) = {1}, uargs(c_5) = {1}, uargs(c_7) = {1}, uargs(c_8) = {1}, uargs(c_9) = {1,2}, uargs(c_15) = {1}, uargs(c_16) = {1} Following symbols are considered usable: all TcT has computed the following interpretation: p(#0) = [0] p(#CKLT) = [4] x1 + [0] p(#COMPARE) = [1] x2 + [0] p(#EQ) = [0] p(#GT) = [0] p(#LESS) = [4] x1 + [0] p(#LT) = [0] p(#cklt) = [1] x1 + [0] p(#compare) = [0] p(#false) = [0] p(#less) = [1] x1 + [1] x2 + [1] p(#neg) = [1] x1 + [4] p(#pos) = [4] p(#s) = [1] x1 + [4] p(#true) = [1] p(::) = [1] x1 + [1] x2 + [7] p(APPEND) = [0] p(APPEND#1) = [1] x1 + [2] x2 + [1] p(FLATTEN) = [0] p(FLATTEN#1) = [4] p(FLATTENSORT) = [1] x1 + [0] p(INSERT) = [2] x1 + [2] x2 + [1] p(INSERT#1) = [4] p(INSERT#2) = [2] x2 + [0] p(INSERTIONSORT) = [2] x1 + [0] p(INSERTIONSORT#1) = [4] x1 + [0] p(append) = [1] x1 + [1] x2 + [1] p(append#1) = [1] x1 + [1] x2 + [1] p(c) = [4] p(c1) = [0] p(c10) = [0] p(c11) = [4] p(c12) = [1] x1 + [1] p(c13) = [1] p(c14) = [1] p(c15) = [1] p(c16) = [1] x1 + [2] p(c17) = [1] p(c18) = [2] p(c19) = [1] p(c2) = [1] p(c20) = [0] p(c21) = [1] x3 + [1] p(c22) = [1] x3 + [1] p(c23) = [2] p(c24) = [0] p(c25) = [4] p(c26) = [1] p(c27) = [1] p(c28) = [2] p(c29) = [0] p(c3) = [0] p(c30) = [1] x1 + [1] p(c31) = [1] p(c4) = [0] p(c5) = [0] p(c6) = [2] p(c7) = [0] p(c8) = [0] p(c9) = [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) = [2] p(nil) = [2] p(node) = [1] x1 + [1] x2 + [1] x3 + [4] p(#CKLT#) = [0] p(#COMPARE#) = [0] p(#LESS#) = [0] p(#cklt#) = [0] p(#compare#) = [0] p(#less#) = [0] p(APPEND#) = [0] p(APPEND#1#) = [0] p(FLATTEN#) = [1] x1 + [7] p(FLATTEN#1#) = [1] x1 + [6] p(FLATTENSORT#) = [2] x1 + [7] p(INSERT#) = [0] p(INSERT#1#) = [0] p(INSERT#2#) = [4] x3 + [1] x4 + [0] p(INSERTIONSORT#) = [1] x1 + [0] p(INSERTIONSORT#1#) = [1] x1 + [0] p(append#) = [0] p(append#1#) = [0] p(flatten#) = [0] p(flatten#1#) = [0] p(flattensort#) = [0] p(insert#) = [0] p(insert#1#) = [0] p(insert#2#) = [0] p(insertionsort#) = [0] p(insertionsort#1#) = [0] p(c_1) = [1] x1 + [1] x2 + [2] x3 + [0] p(c_2) = [1] x1 + [1] p(c_3) = [1] x1 + [1] p(c_4) = [1] p(c_5) = [1] x1 + [0] p(c_6) = [0] p(c_7) = [1] x1 + [3] p(c_8) = [1] x1 + [2] p(c_9) = [1] x1 + [1] x2 + [0] p(c_10) = [0] p(c_11) = [0] p(c_12) = [0] p(c_13) = [1] p(c_14) = [0] p(c_15) = [1] x1 + [0] p(c_16) = [1] x1 + [7] p(c_17) = [0] p(c_18) = [0] p(c_19) = [0] p(c_20) = [0] p(c_21) = [0] p(c_22) = [0] p(c_23) = [0] p(c_24) = [0] p(c_25) = [0] p(c_26) = [0] p(c_27) = [0] p(c_28) = [0] p(c_29) = [0] p(c_30) = [2] x1 + [0] p(c_31) = [0] p(c_32) = [2] p(c_33) = [1] p(c_34) = [0] p(c_35) = [2] p(c_36) = [0] p(c_37) = [1] p(c_38) = [1] p(c_39) = [0] p(c_40) = [0] p(c_41) = [4] x1 + [0] p(c_42) = [0] p(c_43) = [1] p(c_44) = [4] p(c_45) = [1] x1 + [0] p(c_46) = [0] p(c_47) = [2] x1 + [4] p(c_48) = [1] x2 + [4] p(c_49) = [1] x1 + [0] p(c_50) = [1] x1 + [0] p(c_51) = [1] p(c_52) = [0] p(c_53) = [0] p(c_54) = [2] x1 + [1] p(c_55) = [1] x1 + [4] x2 + [2] p(c_56) = [1] p(c_57) = [4] x2 + [0] p(c_58) = [0] p(c_59) = [0] p(c_60) = [1] x1 + [0] p(c_61) = [4] x1 + [0] p(c_62) = [1] x1 + [4] x2 + [2] p(c_63) = [0] Following rules are strictly oriented: FLATTEN#(z0) = [1] z0 + [7] > [1] z0 + [6] = c_5(FLATTEN#1#(z0)) Following rules are (at-least) weakly oriented: FLATTEN#1#(node(z0,z1,z2)) = [1] z0 + [1] z1 + [1] z2 + [10] >= [1] z1 + [10] = c_7(FLATTEN#(z1)) FLATTEN#1#(node(z0,z1,z2)) = [1] z0 + [1] z1 + [1] z2 + [10] >= [1] z2 + [9] = c_8(FLATTEN#(z2)) FLATTENSORT#(z0) = [2] z0 + [7] >= [2] z0 + [7] = c_9(INSERTIONSORT#(flatten(z0)),FLATTEN#(z0)) INSERTIONSORT#(z0) = [1] z0 + [0] >= [1] z0 + [0] = c_15(INSERTIONSORT#1#(z0)) INSERTIONSORT#1#(::(z0,z1)) = [1] z0 + [1] z1 + [7] >= [1] z1 + [7] = c_16(INSERTIONSORT#(z1)) append(z0,z1) = [1] z0 + [1] z1 + [1] >= [1] z0 + [1] z1 + [1] = append#1(z0,z1) append#1(::(z0,z1),z2) = [1] z0 + [1] z1 + [1] z2 + [8] >= [1] z0 + [1] z1 + [1] z2 + [8] = ::(z0,append(z1,z2)) append#1(nil(),z0) = [1] z0 + [3] >= [1] z0 + [0] = z0 flatten(z0) = [1] z0 + [0] >= [1] z0 + [0] = flatten#1(z0) flatten#1(leaf()) = [2] >= [2] = nil() flatten#1(node(z0,z1,z2)) = [1] z0 + [1] z1 + [1] z2 + [4] >= [1] z0 + [1] z1 + [1] z2 + [2] = append(z0,append(flatten(z1),flatten(z2))) Further, it can be verified that all rules not oriented are covered by the weightgap condition. ** Step 7.a:8: EmptyProcessor. WORST_CASE(?,O(1)) + Considered Problem: - Weak DPs: FLATTEN#(z0) -> c_5(FLATTEN#1#(z0)) FLATTEN#1#(node(z0,z1,z2)) -> c_7(FLATTEN#(z1)) FLATTEN#1#(node(z0,z1,z2)) -> c_8(FLATTEN#(z2)) FLATTENSORT#(z0) -> c_9(INSERTIONSORT#(flatten(z0)),FLATTEN#(z0)) INSERTIONSORT#(z0) -> c_15(INSERTIONSORT#1#(z0)) INSERTIONSORT#1#(::(z0,z1)) -> c_16(INSERTIONSORT#(z1)) - Weak TRS: append(z0,z1) -> append#1(z0,z1) append#1(::(z0,z1),z2) -> ::(z0,append(z1,z2)) append#1(nil(),z0) -> z0 flatten(z0) -> flatten#1(z0) flatten#1(leaf()) -> nil() flatten#1(node(z0,z1,z2)) -> append(z0,append(flatten(z1),flatten(z2))) - Signature: {#CKLT/1,#COMPARE/2,#LESS/2,#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,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,#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,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,::/2,c/0,c1/0,c10/0,c11/0 ,c12/1,c13/0,c14/1,c15/2,c16/1,c17/1,c18/0,c19/1,c2/0,c20/0,c21/3,c22/3,c23/2,c24/1,c25/2,c26/0,c27/0,c28/1 ,c29/1,c3/0,c30/2,c31/0,c4/0,c5/0,c6/0,c7/0,c8/1,c9/0,leaf/0,nil/0,node/3,c_1/3,c_2/1,c_3/1,c_4/0,c_5/1 ,c_6/0,c_7/1,c_8/1,c_9/2,c_10/1,c_11/1,c_12/0,c_13/0,c_14/1,c_15/1,c_16/1,c_17/0,c_18/0,c_19/0,c_20/0,c_21/0 ,c_22/0,c_23/0,c_24/0,c_25/0,c_26/1,c_27/0,c_28/0,c_29/0,c_30/1,c_31/0,c_32/1,c_33/0,c_34/0,c_35/0,c_36/0 ,c_37/0,c_38/0,c_39/0,c_40/0,c_41/1,c_42/0,c_43/0,c_44/0,c_45/1,c_46/0,c_47/1,c_48/2,c_49/1,c_50/1,c_51/0 ,c_52/1,c_53/0,c_54/4,c_55/2,c_56/1,c_57/2,c_58/0,c_59/0,c_60/1,c_61/1,c_62/2,c_63/0} - Obligation: innermost runtime complexity wrt. defined symbols {#CKLT#,#COMPARE#,#LESS#,#cklt#,#compare#,#less#,APPEND# ,APPEND#1#,FLATTEN#,FLATTEN#1#,FLATTENSORT#,INSERT#,INSERT#1#,INSERT#2#,INSERTIONSORT#,INSERTIONSORT#1# ,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,::,c,c1,c10,c11,c12,c13,c14 ,c15,c16,c17,c18,c19,c2,c20,c21,c22,c23,c24,c25,c26,c27,c28,c29,c3,c30,c31,c4,c5,c6,c7,c8,c9,leaf,nil,node} + Applied Processor: EmptyProcessor + Details: The problem is already closed. The intended complexity is O(1). ** Step 7.b:1: RemoveHeads. WORST_CASE(?,O(n^1)) + Considered Problem: - Strict DPs: APPEND#(z0,z1) -> c_2(APPEND#1#(z0,z1)) APPEND#1#(::(z0,z1),z2) -> c_3(APPEND#(z1,z2)) INSERT#(z0,z1) -> c_10(INSERT#1#(z1,z0)) INSERT#1#(::(z0,z1),z2) -> c_11(INSERT#2#(#less(z0,z2),z2,z0,z1)) INSERT#2#(#true(),z0,z1,z2) -> c_14(INSERT#(z0,z2)) - Weak DPs: FLATTEN#(z0) -> FLATTEN#1#(z0) FLATTEN#1#(node(z0,z1,z2)) -> APPEND#(z0,append(flatten(z1),flatten(z2))) FLATTEN#1#(node(z0,z1,z2)) -> APPEND#(flatten(z1),flatten(z2)) FLATTEN#1#(node(z0,z1,z2)) -> FLATTEN#(z1) FLATTEN#1#(node(z0,z1,z2)) -> FLATTEN#(z2) FLATTENSORT#(z0) -> FLATTEN#(z0) FLATTENSORT#(z0) -> INSERTIONSORT#(flatten(z0)) INSERTIONSORT#(z0) -> INSERTIONSORT#1#(z0) INSERTIONSORT#1#(::(z0,z1)) -> INSERT#(z0,insertionsort(z1)) INSERTIONSORT#1#(::(z0,z1)) -> INSERTIONSORT#(z1) - Weak TRS: #cklt(#EQ()) -> #false() #cklt(#GT()) -> #false() #cklt(#LT()) -> #true() #compare(#0(),#0()) -> #EQ() #compare(#0(),#neg(z0)) -> #GT() #compare(#0(),#pos(z0)) -> #LT() #compare(#0(),#s(z0)) -> #LT() #compare(#neg(z0),#0()) -> #LT() #compare(#neg(z0),#neg(z1)) -> #compare(z1,z0) #compare(#neg(z0),#pos(z1)) -> #LT() #compare(#pos(z0),#0()) -> #GT() #compare(#pos(z0),#neg(z1)) -> #GT() #compare(#pos(z0),#pos(z1)) -> #compare(z0,z1) #compare(#s(z0),#0()) -> #GT() #compare(#s(z0),#s(z1)) -> #compare(z0,z1) #less(z0,z1) -> #cklt(#compare(z0,z1)) append(z0,z1) -> append#1(z0,z1) append#1(::(z0,z1),z2) -> ::(z0,append(z1,z2)) append#1(nil(),z0) -> z0 flatten(z0) -> flatten#1(z0) flatten#1(leaf()) -> nil() flatten#1(node(z0,z1,z2)) -> append(z0,append(flatten(z1),flatten(z2))) insert(z0,z1) -> insert#1(z1,z0) insert#1(::(z0,z1),z2) -> insert#2(#less(z0,z2),z2,z0,z1) insert#1(nil(),z0) -> ::(z0,nil()) insert#2(#false(),z0,z1,z2) -> ::(z0,::(z1,z2)) insert#2(#true(),z0,z1,z2) -> ::(z1,insert(z0,z2)) insertionsort(z0) -> insertionsort#1(z0) insertionsort#1(::(z0,z1)) -> insert(z0,insertionsort(z1)) insertionsort#1(nil()) -> nil() - Signature: {#CKLT/1,#COMPARE/2,#LESS/2,#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,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,#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,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,::/2,c/0,c1/0,c10/0,c11/0 ,c12/1,c13/0,c14/1,c15/2,c16/1,c17/1,c18/0,c19/1,c2/0,c20/0,c21/3,c22/3,c23/2,c24/1,c25/2,c26/0,c27/0,c28/1 ,c29/1,c3/0,c30/2,c31/0,c4/0,c5/0,c6/0,c7/0,c8/1,c9/0,leaf/0,nil/0,node/3,c_1/3,c_2/1,c_3/1,c_4/0,c_5/1 ,c_6/0,c_7/3,c_8/3,c_9/2,c_10/1,c_11/1,c_12/0,c_13/0,c_14/1,c_15/1,c_16/2,c_17/0,c_18/0,c_19/0,c_20/0,c_21/0 ,c_22/0,c_23/0,c_24/0,c_25/0,c_26/1,c_27/0,c_28/0,c_29/0,c_30/1,c_31/0,c_32/1,c_33/0,c_34/0,c_35/0,c_36/0 ,c_37/0,c_38/0,c_39/0,c_40/0,c_41/1,c_42/0,c_43/0,c_44/0,c_45/1,c_46/0,c_47/1,c_48/2,c_49/1,c_50/1,c_51/0 ,c_52/1,c_53/0,c_54/4,c_55/2,c_56/1,c_57/2,c_58/0,c_59/0,c_60/1,c_61/1,c_62/2,c_63/0} - Obligation: innermost runtime complexity wrt. defined symbols {#CKLT#,#COMPARE#,#LESS#,#cklt#,#compare#,#less#,APPEND# ,APPEND#1#,FLATTEN#,FLATTEN#1#,FLATTENSORT#,INSERT#,INSERT#1#,INSERT#2#,INSERTIONSORT#,INSERTIONSORT#1# ,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,::,c,c1,c10,c11,c12,c13,c14 ,c15,c16,c17,c18,c19,c2,c20,c21,c22,c23,c24,c25,c26,c27,c28,c29,c3,c30,c31,c4,c5,c6,c7,c8,c9,leaf,nil,node} + Applied Processor: RemoveHeads + Details: Consider the dependency graph 1:S:APPEND#(z0,z1) -> c_2(APPEND#1#(z0,z1)) -->_1 APPEND#1#(::(z0,z1),z2) -> c_3(APPEND#(z1,z2)):2 2:S:APPEND#1#(::(z0,z1),z2) -> c_3(APPEND#(z1,z2)) -->_1 APPEND#(z0,z1) -> c_2(APPEND#1#(z0,z1)):1 3:S:INSERT#(z0,z1) -> c_10(INSERT#1#(z1,z0)) -->_1 INSERT#1#(::(z0,z1),z2) -> c_11(INSERT#2#(#less(z0,z2),z2,z0,z1)):4 4:S:INSERT#1#(::(z0,z1),z2) -> c_11(INSERT#2#(#less(z0,z2),z2,z0,z1)) -->_1 INSERT#2#(#true(),z0,z1,z2) -> c_14(INSERT#(z0,z2)):5 5:S:INSERT#2#(#true(),z0,z1,z2) -> c_14(INSERT#(z0,z2)) -->_1 INSERT#(z0,z1) -> c_10(INSERT#1#(z1,z0)):3 6:W:FLATTEN#(z0) -> FLATTEN#1#(z0) -->_1 FLATTEN#1#(node(z0,z1,z2)) -> FLATTEN#(z2):10 -->_1 FLATTEN#1#(node(z0,z1,z2)) -> FLATTEN#(z1):9 -->_1 FLATTEN#1#(node(z0,z1,z2)) -> APPEND#(flatten(z1),flatten(z2)):8 -->_1 FLATTEN#1#(node(z0,z1,z2)) -> APPEND#(z0,append(flatten(z1),flatten(z2))):7 7:W:FLATTEN#1#(node(z0,z1,z2)) -> APPEND#(z0,append(flatten(z1),flatten(z2))) -->_1 APPEND#(z0,z1) -> c_2(APPEND#1#(z0,z1)):1 8:W:FLATTEN#1#(node(z0,z1,z2)) -> APPEND#(flatten(z1),flatten(z2)) -->_1 APPEND#(z0,z1) -> c_2(APPEND#1#(z0,z1)):1 9:W:FLATTEN#1#(node(z0,z1,z2)) -> FLATTEN#(z1) -->_1 FLATTEN#(z0) -> FLATTEN#1#(z0):6 10:W:FLATTEN#1#(node(z0,z1,z2)) -> FLATTEN#(z2) -->_1 FLATTEN#(z0) -> FLATTEN#1#(z0):6 11:W:FLATTENSORT#(z0) -> FLATTEN#(z0) -->_1 FLATTEN#(z0) -> FLATTEN#1#(z0):6 12:W:FLATTENSORT#(z0) -> INSERTIONSORT#(flatten(z0)) -->_1 INSERTIONSORT#(z0) -> INSERTIONSORT#1#(z0):13 13:W:INSERTIONSORT#(z0) -> INSERTIONSORT#1#(z0) -->_1 INSERTIONSORT#1#(::(z0,z1)) -> INSERTIONSORT#(z1):15 -->_1 INSERTIONSORT#1#(::(z0,z1)) -> INSERT#(z0,insertionsort(z1)):14 14:W:INSERTIONSORT#1#(::(z0,z1)) -> INSERT#(z0,insertionsort(z1)) -->_1 INSERT#(z0,z1) -> c_10(INSERT#1#(z1,z0)):3 15:W:INSERTIONSORT#1#(::(z0,z1)) -> INSERTIONSORT#(z1) -->_1 INSERTIONSORT#(z0) -> INSERTIONSORT#1#(z0):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#(z0) -> FLATTEN#(z0))] ** Step 7.b:2: WeightGap. WORST_CASE(?,O(n^1)) + Considered Problem: - Strict DPs: APPEND#(z0,z1) -> c_2(APPEND#1#(z0,z1)) APPEND#1#(::(z0,z1),z2) -> c_3(APPEND#(z1,z2)) INSERT#(z0,z1) -> c_10(INSERT#1#(z1,z0)) INSERT#1#(::(z0,z1),z2) -> c_11(INSERT#2#(#less(z0,z2),z2,z0,z1)) INSERT#2#(#true(),z0,z1,z2) -> c_14(INSERT#(z0,z2)) - Weak DPs: FLATTEN#(z0) -> FLATTEN#1#(z0) FLATTEN#1#(node(z0,z1,z2)) -> APPEND#(z0,append(flatten(z1),flatten(z2))) FLATTEN#1#(node(z0,z1,z2)) -> APPEND#(flatten(z1),flatten(z2)) FLATTEN#1#(node(z0,z1,z2)) -> FLATTEN#(z1) FLATTEN#1#(node(z0,z1,z2)) -> FLATTEN#(z2) FLATTENSORT#(z0) -> INSERTIONSORT#(flatten(z0)) INSERTIONSORT#(z0) -> INSERTIONSORT#1#(z0) INSERTIONSORT#1#(::(z0,z1)) -> INSERT#(z0,insertionsort(z1)) INSERTIONSORT#1#(::(z0,z1)) -> INSERTIONSORT#(z1) - Weak TRS: #cklt(#EQ()) -> #false() #cklt(#GT()) -> #false() #cklt(#LT()) -> #true() #compare(#0(),#0()) -> #EQ() #compare(#0(),#neg(z0)) -> #GT() #compare(#0(),#pos(z0)) -> #LT() #compare(#0(),#s(z0)) -> #LT() #compare(#neg(z0),#0()) -> #LT() #compare(#neg(z0),#neg(z1)) -> #compare(z1,z0) #compare(#neg(z0),#pos(z1)) -> #LT() #compare(#pos(z0),#0()) -> #GT() #compare(#pos(z0),#neg(z1)) -> #GT() #compare(#pos(z0),#pos(z1)) -> #compare(z0,z1) #compare(#s(z0),#0()) -> #GT() #compare(#s(z0),#s(z1)) -> #compare(z0,z1) #less(z0,z1) -> #cklt(#compare(z0,z1)) append(z0,z1) -> append#1(z0,z1) append#1(::(z0,z1),z2) -> ::(z0,append(z1,z2)) append#1(nil(),z0) -> z0 flatten(z0) -> flatten#1(z0) flatten#1(leaf()) -> nil() flatten#1(node(z0,z1,z2)) -> append(z0,append(flatten(z1),flatten(z2))) insert(z0,z1) -> insert#1(z1,z0) insert#1(::(z0,z1),z2) -> insert#2(#less(z0,z2),z2,z0,z1) insert#1(nil(),z0) -> ::(z0,nil()) insert#2(#false(),z0,z1,z2) -> ::(z0,::(z1,z2)) insert#2(#true(),z0,z1,z2) -> ::(z1,insert(z0,z2)) insertionsort(z0) -> insertionsort#1(z0) insertionsort#1(::(z0,z1)) -> insert(z0,insertionsort(z1)) insertionsort#1(nil()) -> nil() - Signature: {#CKLT/1,#COMPARE/2,#LESS/2,#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,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,#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,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,::/2,c/0,c1/0,c10/0,c11/0 ,c12/1,c13/0,c14/1,c15/2,c16/1,c17/1,c18/0,c19/1,c2/0,c20/0,c21/3,c22/3,c23/2,c24/1,c25/2,c26/0,c27/0,c28/1 ,c29/1,c3/0,c30/2,c31/0,c4/0,c5/0,c6/0,c7/0,c8/1,c9/0,leaf/0,nil/0,node/3,c_1/3,c_2/1,c_3/1,c_4/0,c_5/1 ,c_6/0,c_7/3,c_8/3,c_9/2,c_10/1,c_11/1,c_12/0,c_13/0,c_14/1,c_15/1,c_16/2,c_17/0,c_18/0,c_19/0,c_20/0,c_21/0 ,c_22/0,c_23/0,c_24/0,c_25/0,c_26/1,c_27/0,c_28/0,c_29/0,c_30/1,c_31/0,c_32/1,c_33/0,c_34/0,c_35/0,c_36/0 ,c_37/0,c_38/0,c_39/0,c_40/0,c_41/1,c_42/0,c_43/0,c_44/0,c_45/1,c_46/0,c_47/1,c_48/2,c_49/1,c_50/1,c_51/0 ,c_52/1,c_53/0,c_54/4,c_55/2,c_56/1,c_57/2,c_58/0,c_59/0,c_60/1,c_61/1,c_62/2,c_63/0} - Obligation: innermost runtime complexity wrt. defined symbols {#CKLT#,#COMPARE#,#LESS#,#cklt#,#compare#,#less#,APPEND# ,APPEND#1#,FLATTEN#,FLATTEN#1#,FLATTENSORT#,INSERT#,INSERT#1#,INSERT#2#,INSERTIONSORT#,INSERTIONSORT#1# ,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,::,c,c1,c10,c11,c12,c13,c14 ,c15,c16,c17,c18,c19,c2,c20,c21,c22,c23,c24,c25,c26,c27,c28,c29,c3,c30,c31,c4,c5,c6,c7,c8,c9,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(::) = {2}, uargs(append) = {1,2}, uargs(insert) = {2}, uargs(insert#2) = {1}, uargs(APPEND#) = {1,2}, uargs(INSERT#) = {2}, uargs(INSERT#2#) = {1}, uargs(INSERTIONSORT#) = {1}, uargs(c_2) = {1}, uargs(c_3) = {1}, uargs(c_10) = {1}, uargs(c_11) = {1}, uargs(c_14) = {1} Following symbols are considered usable: all TcT has computed the following interpretation: p(#0) = [1] p(#CKLT) = [1] x1 + [0] p(#COMPARE) = [0] p(#EQ) = [0] p(#GT) = [0] p(#LESS) = [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(::) = [1] x2 + [0] p(APPEND) = [0] p(APPEND#1) = [0] p(FLATTEN) = [0] p(FLATTEN#1) = [0] p(FLATTENSORT) = [0] p(INSERT) = [0] p(INSERT#1) = [0] p(INSERT#2) = [0] p(INSERTIONSORT) = [0] p(INSERTIONSORT#1) = [0] p(append) = [1] x1 + [1] x2 + [0] p(append#1) = [1] x1 + [1] x2 + [0] p(c) = [0] p(c1) = [0] p(c10) = [0] p(c11) = [0] p(c12) = [1] x1 + [0] p(c13) = [0] p(c14) = [1] x1 + [0] p(c15) = [1] x1 + [1] x2 + [0] p(c16) = [1] x1 + [0] p(c17) = [1] x1 + [0] p(c18) = [0] p(c19) = [1] x1 + [0] p(c2) = [0] p(c20) = [0] p(c21) = [1] x2 + [1] x3 + [0] p(c22) = [1] x1 + [1] x2 + [1] x3 + [0] p(c23) = [1] x1 + [1] x2 + [0] p(c24) = [1] x1 + [0] p(c25) = [1] x1 + [1] x2 + [0] p(c26) = [0] p(c27) = [0] p(c28) = [1] x1 + [0] p(c29) = [1] x1 + [0] p(c3) = [0] p(c30) = [1] x1 + [1] x2 + [0] p(c31) = [0] p(c4) = [0] p(c5) = [0] p(c6) = [0] p(c7) = [0] p(c8) = [1] x1 + [0] p(c9) = [0] p(flatten) = [1] x1 + [4] p(flatten#1) = [1] x1 + [1] p(flattensort) = [0] p(insert) = [1] x2 + [0] p(insert#1) = [1] x1 + [0] p(insert#2) = [1] x1 + [1] x4 + [0] p(insertionsort) = [1] p(insertionsort#1) = [1] p(leaf) = [0] p(nil) = [1] p(node) = [1] x1 + [1] x2 + [1] x3 + [7] p(#CKLT#) = [0] p(#COMPARE#) = [0] p(#LESS#) = [2] p(#cklt#) = [1] x1 + [1] p(#compare#) = [1] x1 + [4] p(#less#) = [1] p(APPEND#) = [1] x1 + [1] x2 + [0] p(APPEND#1#) = [1] x1 + [1] x2 + [1] p(FLATTEN#) = [2] x1 + [1] p(FLATTEN#1#) = [2] x1 + [0] p(FLATTENSORT#) = [4] x1 + [5] p(INSERT#) = [1] x2 + [0] p(INSERT#1#) = [1] x1 + [1] p(INSERT#2#) = [1] x1 + [1] x4 + [0] p(INSERTIONSORT#) = [1] x1 + [1] p(INSERTIONSORT#1#) = [1] x1 + [1] p(append#) = [0] p(append#1#) = [0] p(flatten#) = [0] p(flatten#1#) = [0] p(flattensort#) = [0] p(insert#) = [0] p(insert#1#) = [0] p(insert#2#) = [0] p(insertionsort#) = [0] p(insertionsort#1#) = [0] p(c_1) = [0] p(c_2) = [1] x1 + [0] p(c_3) = [1] x1 + [0] p(c_4) = [0] p(c_5) = [0] p(c_6) = [0] p(c_7) = [0] p(c_8) = [0] p(c_9) = [0] p(c_10) = [1] x1 + [0] p(c_11) = [1] x1 + [0] p(c_12) = [0] p(c_13) = [0] p(c_14) = [1] x1 + [0] p(c_15) = [0] p(c_16) = [0] p(c_17) = [0] p(c_18) = [0] p(c_19) = [0] p(c_20) = [0] p(c_21) = [0] p(c_22) = [0] p(c_23) = [0] p(c_24) = [0] p(c_25) = [0] p(c_26) = [0] p(c_27) = [0] p(c_28) = [0] p(c_29) = [0] p(c_30) = [0] p(c_31) = [0] p(c_32) = [0] p(c_33) = [0] p(c_34) = [0] p(c_35) = [0] p(c_36) = [0] p(c_37) = [0] p(c_38) = [0] p(c_39) = [0] p(c_40) = [0] p(c_41) = [0] p(c_42) = [0] p(c_43) = [0] p(c_44) = [0] p(c_45) = [0] p(c_46) = [0] p(c_47) = [0] p(c_48) = [0] p(c_49) = [0] p(c_50) = [0] p(c_51) = [0] p(c_52) = [0] p(c_53) = [0] p(c_54) = [0] p(c_55) = [0] p(c_56) = [0] p(c_57) = [0] p(c_58) = [0] p(c_59) = [0] p(c_60) = [0] p(c_61) = [0] p(c_62) = [0] p(c_63) = [0] Following rules are strictly oriented: APPEND#1#(::(z0,z1),z2) = [1] z1 + [1] z2 + [1] > [1] z1 + [1] z2 + [0] = c_3(APPEND#(z1,z2)) INSERT#1#(::(z0,z1),z2) = [1] z1 + [1] > [1] z1 + [0] = c_11(INSERT#2#(#less(z0,z2),z2,z0,z1)) Following rules are (at-least) weakly oriented: APPEND#(z0,z1) = [1] z0 + [1] z1 + [0] >= [1] z0 + [1] z1 + [1] = c_2(APPEND#1#(z0,z1)) FLATTEN#(z0) = [2] z0 + [1] >= [2] z0 + [0] = FLATTEN#1#(z0) FLATTEN#1#(node(z0,z1,z2)) = [2] z0 + [2] z1 + [2] z2 + [14] >= [1] z0 + [1] z1 + [1] z2 + [8] = APPEND#(z0,append(flatten(z1),flatten(z2))) FLATTEN#1#(node(z0,z1,z2)) = [2] z0 + [2] z1 + [2] z2 + [14] >= [1] z1 + [1] z2 + [8] = APPEND#(flatten(z1),flatten(z2)) FLATTEN#1#(node(z0,z1,z2)) = [2] z0 + [2] z1 + [2] z2 + [14] >= [2] z1 + [1] = FLATTEN#(z1) FLATTEN#1#(node(z0,z1,z2)) = [2] z0 + [2] z1 + [2] z2 + [14] >= [2] z2 + [1] = FLATTEN#(z2) FLATTENSORT#(z0) = [4] z0 + [5] >= [1] z0 + [5] = INSERTIONSORT#(flatten(z0)) INSERT#(z0,z1) = [1] z1 + [0] >= [1] z1 + [1] = c_10(INSERT#1#(z1,z0)) INSERT#2#(#true(),z0,z1,z2) = [1] z2 + [0] >= [1] z2 + [0] = c_14(INSERT#(z0,z2)) INSERTIONSORT#(z0) = [1] z0 + [1] >= [1] z0 + [1] = INSERTIONSORT#1#(z0) INSERTIONSORT#1#(::(z0,z1)) = [1] z1 + [1] >= [1] = INSERT#(z0,insertionsort(z1)) INSERTIONSORT#1#(::(z0,z1)) = [1] z1 + [1] >= [1] z1 + [1] = INSERTIONSORT#(z1) #cklt(#EQ()) = [0] >= [0] = #false() #cklt(#GT()) = [0] >= [0] = #false() #cklt(#LT()) = [0] >= [0] = #true() #compare(#0(),#0()) = [0] >= [0] = #EQ() #compare(#0(),#neg(z0)) = [0] >= [0] = #GT() #compare(#0(),#pos(z0)) = [0] >= [0] = #LT() #compare(#0(),#s(z0)) = [0] >= [0] = #LT() #compare(#neg(z0),#0()) = [0] >= [0] = #LT() #compare(#neg(z0),#neg(z1)) = [0] >= [0] = #compare(z1,z0) #compare(#neg(z0),#pos(z1)) = [0] >= [0] = #LT() #compare(#pos(z0),#0()) = [0] >= [0] = #GT() #compare(#pos(z0),#neg(z1)) = [0] >= [0] = #GT() #compare(#pos(z0),#pos(z1)) = [0] >= [0] = #compare(z0,z1) #compare(#s(z0),#0()) = [0] >= [0] = #GT() #compare(#s(z0),#s(z1)) = [0] >= [0] = #compare(z0,z1) #less(z0,z1) = [0] >= [0] = #cklt(#compare(z0,z1)) append(z0,z1) = [1] z0 + [1] z1 + [0] >= [1] z0 + [1] z1 + [0] = append#1(z0,z1) append#1(::(z0,z1),z2) = [1] z1 + [1] z2 + [0] >= [1] z1 + [1] z2 + [0] = ::(z0,append(z1,z2)) append#1(nil(),z0) = [1] z0 + [1] >= [1] z0 + [0] = z0 flatten(z0) = [1] z0 + [4] >= [1] z0 + [1] = flatten#1(z0) flatten#1(leaf()) = [1] >= [1] = nil() flatten#1(node(z0,z1,z2)) = [1] z0 + [1] z1 + [1] z2 + [8] >= [1] z0 + [1] z1 + [1] z2 + [8] = append(z0,append(flatten(z1),flatten(z2))) insert(z0,z1) = [1] z1 + [0] >= [1] z1 + [0] = insert#1(z1,z0) insert#1(::(z0,z1),z2) = [1] z1 + [0] >= [1] z1 + [0] = insert#2(#less(z0,z2),z2,z0,z1) insert#1(nil(),z0) = [1] >= [1] = ::(z0,nil()) insert#2(#false(),z0,z1,z2) = [1] z2 + [0] >= [1] z2 + [0] = ::(z0,::(z1,z2)) insert#2(#true(),z0,z1,z2) = [1] z2 + [0] >= [1] z2 + [0] = ::(z1,insert(z0,z2)) insertionsort(z0) = [1] >= [1] = insertionsort#1(z0) insertionsort#1(::(z0,z1)) = [1] >= [1] = insert(z0,insertionsort(z1)) insertionsort#1(nil()) = [1] >= [1] = nil() Further, it can be verified that all rules not oriented are covered by the weightgap condition. ** Step 7.b:3: WeightGap. WORST_CASE(?,O(n^1)) + Considered Problem: - Strict DPs: APPEND#(z0,z1) -> c_2(APPEND#1#(z0,z1)) INSERT#(z0,z1) -> c_10(INSERT#1#(z1,z0)) INSERT#2#(#true(),z0,z1,z2) -> c_14(INSERT#(z0,z2)) - Weak DPs: APPEND#1#(::(z0,z1),z2) -> c_3(APPEND#(z1,z2)) FLATTEN#(z0) -> FLATTEN#1#(z0) FLATTEN#1#(node(z0,z1,z2)) -> APPEND#(z0,append(flatten(z1),flatten(z2))) FLATTEN#1#(node(z0,z1,z2)) -> APPEND#(flatten(z1),flatten(z2)) FLATTEN#1#(node(z0,z1,z2)) -> FLATTEN#(z1) FLATTEN#1#(node(z0,z1,z2)) -> FLATTEN#(z2) FLATTENSORT#(z0) -> INSERTIONSORT#(flatten(z0)) INSERT#1#(::(z0,z1),z2) -> c_11(INSERT#2#(#less(z0,z2),z2,z0,z1)) INSERTIONSORT#(z0) -> INSERTIONSORT#1#(z0) INSERTIONSORT#1#(::(z0,z1)) -> INSERT#(z0,insertionsort(z1)) INSERTIONSORT#1#(::(z0,z1)) -> INSERTIONSORT#(z1) - Weak TRS: #cklt(#EQ()) -> #false() #cklt(#GT()) -> #false() #cklt(#LT()) -> #true() #compare(#0(),#0()) -> #EQ() #compare(#0(),#neg(z0)) -> #GT() #compare(#0(),#pos(z0)) -> #LT() #compare(#0(),#s(z0)) -> #LT() #compare(#neg(z0),#0()) -> #LT() #compare(#neg(z0),#neg(z1)) -> #compare(z1,z0) #compare(#neg(z0),#pos(z1)) -> #LT() #compare(#pos(z0),#0()) -> #GT() #compare(#pos(z0),#neg(z1)) -> #GT() #compare(#pos(z0),#pos(z1)) -> #compare(z0,z1) #compare(#s(z0),#0()) -> #GT() #compare(#s(z0),#s(z1)) -> #compare(z0,z1) #less(z0,z1) -> #cklt(#compare(z0,z1)) append(z0,z1) -> append#1(z0,z1) append#1(::(z0,z1),z2) -> ::(z0,append(z1,z2)) append#1(nil(),z0) -> z0 flatten(z0) -> flatten#1(z0) flatten#1(leaf()) -> nil() flatten#1(node(z0,z1,z2)) -> append(z0,append(flatten(z1),flatten(z2))) insert(z0,z1) -> insert#1(z1,z0) insert#1(::(z0,z1),z2) -> insert#2(#less(z0,z2),z2,z0,z1) insert#1(nil(),z0) -> ::(z0,nil()) insert#2(#false(),z0,z1,z2) -> ::(z0,::(z1,z2)) insert#2(#true(),z0,z1,z2) -> ::(z1,insert(z0,z2)) insertionsort(z0) -> insertionsort#1(z0) insertionsort#1(::(z0,z1)) -> insert(z0,insertionsort(z1)) insertionsort#1(nil()) -> nil() - Signature: {#CKLT/1,#COMPARE/2,#LESS/2,#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,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,#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,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,::/2,c/0,c1/0,c10/0,c11/0 ,c12/1,c13/0,c14/1,c15/2,c16/1,c17/1,c18/0,c19/1,c2/0,c20/0,c21/3,c22/3,c23/2,c24/1,c25/2,c26/0,c27/0,c28/1 ,c29/1,c3/0,c30/2,c31/0,c4/0,c5/0,c6/0,c7/0,c8/1,c9/0,leaf/0,nil/0,node/3,c_1/3,c_2/1,c_3/1,c_4/0,c_5/1 ,c_6/0,c_7/3,c_8/3,c_9/2,c_10/1,c_11/1,c_12/0,c_13/0,c_14/1,c_15/1,c_16/2,c_17/0,c_18/0,c_19/0,c_20/0,c_21/0 ,c_22/0,c_23/0,c_24/0,c_25/0,c_26/1,c_27/0,c_28/0,c_29/0,c_30/1,c_31/0,c_32/1,c_33/0,c_34/0,c_35/0,c_36/0 ,c_37/0,c_38/0,c_39/0,c_40/0,c_41/1,c_42/0,c_43/0,c_44/0,c_45/1,c_46/0,c_47/1,c_48/2,c_49/1,c_50/1,c_51/0 ,c_52/1,c_53/0,c_54/4,c_55/2,c_56/1,c_57/2,c_58/0,c_59/0,c_60/1,c_61/1,c_62/2,c_63/0} - Obligation: innermost runtime complexity wrt. defined symbols {#CKLT#,#COMPARE#,#LESS#,#cklt#,#compare#,#less#,APPEND# ,APPEND#1#,FLATTEN#,FLATTEN#1#,FLATTENSORT#,INSERT#,INSERT#1#,INSERT#2#,INSERTIONSORT#,INSERTIONSORT#1# ,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,::,c,c1,c10,c11,c12,c13,c14 ,c15,c16,c17,c18,c19,c2,c20,c21,c22,c23,c24,c25,c26,c27,c28,c29,c3,c30,c31,c4,c5,c6,c7,c8,c9,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(::) = {2}, uargs(append) = {1,2}, uargs(insert) = {2}, uargs(insert#2) = {1}, uargs(APPEND#) = {1,2}, uargs(INSERT#) = {2}, uargs(INSERT#2#) = {1}, uargs(INSERTIONSORT#) = {1}, uargs(c_2) = {1}, uargs(c_3) = {1}, uargs(c_10) = {1}, uargs(c_11) = {1}, uargs(c_14) = {1} Following symbols are considered usable: all TcT has computed the following interpretation: p(#0) = [0] p(#CKLT) = [0] p(#COMPARE) = [0] p(#EQ) = [0] p(#GT) = [0] p(#LESS) = [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(::) = [1] x2 + [0] p(APPEND) = [0] p(APPEND#1) = [0] p(FLATTEN) = [0] p(FLATTEN#1) = [0] p(FLATTENSORT) = [0] p(INSERT) = [0] p(INSERT#1) = [1] x1 + [0] p(INSERT#2) = [0] p(INSERTIONSORT) = [0] p(INSERTIONSORT#1) = [0] p(append) = [1] x1 + [1] x2 + [1] p(append#1) = [1] x1 + [1] x2 + [1] p(c) = [0] p(c1) = [0] p(c10) = [0] p(c11) = [0] p(c12) = [1] x1 + [0] p(c13) = [0] p(c14) = [1] x1 + [0] p(c15) = [1] x1 + [1] x2 + [0] p(c16) = [1] x1 + [0] p(c17) = [1] x1 + [0] p(c18) = [0] p(c19) = [1] x1 + [0] p(c2) = [0] p(c20) = [0] p(c21) = [1] x1 + [1] x2 + [1] x3 + [0] p(c22) = [1] x1 + [1] x2 + [1] x3 + [0] p(c23) = [1] x1 + [1] x2 + [0] p(c24) = [1] x1 + [0] p(c25) = [1] x1 + [1] x2 + [0] p(c26) = [0] p(c27) = [0] p(c28) = [1] x1 + [0] p(c29) = [1] x1 + [0] p(c3) = [0] p(c30) = [1] x1 + [1] x2 + [0] p(c31) = [0] p(c4) = [0] p(c5) = [0] p(c6) = [0] p(c7) = [0] p(c8) = [1] x1 + [0] p(c9) = [0] p(flatten) = [1] x1 + [1] p(flatten#1) = [1] x1 + [1] p(flattensort) = [0] p(insert) = [1] x2 + [0] p(insert#1) = [1] x1 + [0] p(insert#2) = [1] x1 + [1] x4 + [0] p(insertionsort) = [1] x1 + [2] p(insertionsort#1) = [1] x1 + [2] p(leaf) = [0] p(nil) = [0] p(node) = [1] x1 + [1] x2 + [1] x3 + [7] p(#CKLT#) = [0] p(#COMPARE#) = [0] p(#LESS#) = [0] p(#cklt#) = [0] p(#compare#) = [0] p(#less#) = [0] p(APPEND#) = [1] x1 + [1] x2 + [0] p(APPEND#1#) = [1] x1 + [1] x2 + [0] p(FLATTEN#) = [1] x1 + [0] p(FLATTEN#1#) = [1] x1 + [0] p(FLATTENSORT#) = [4] x1 + [4] p(INSERT#) = [1] x2 + [0] p(INSERT#1#) = [1] x1 + [2] p(INSERT#2#) = [1] x1 + [1] x4 + [2] p(INSERTIONSORT#) = [1] x1 + [2] p(INSERTIONSORT#1#) = [1] x1 + [2] p(append#) = [0] p(append#1#) = [0] p(flatten#) = [0] p(flatten#1#) = [0] p(flattensort#) = [0] p(insert#) = [0] p(insert#1#) = [0] p(insert#2#) = [0] p(insertionsort#) = [0] p(insertionsort#1#) = [0] p(c_1) = [0] p(c_2) = [1] x1 + [0] p(c_3) = [1] x1 + [0] p(c_4) = [0] p(c_5) = [0] p(c_6) = [0] p(c_7) = [0] p(c_8) = [0] p(c_9) = [1] x2 + [0] p(c_10) = [1] x1 + [5] p(c_11) = [1] x1 + [0] p(c_12) = [1] p(c_13) = [2] p(c_14) = [1] x1 + [0] p(c_15) = [0] p(c_16) = [0] p(c_17) = [0] p(c_18) = [0] p(c_19) = [0] p(c_20) = [0] p(c_21) = [0] p(c_22) = [0] p(c_23) = [0] p(c_24) = [0] p(c_25) = [0] p(c_26) = [0] p(c_27) = [0] p(c_28) = [0] p(c_29) = [0] p(c_30) = [0] p(c_31) = [0] p(c_32) = [0] p(c_33) = [0] p(c_34) = [0] p(c_35) = [0] p(c_36) = [0] p(c_37) = [0] p(c_38) = [0] p(c_39) = [0] p(c_40) = [0] p(c_41) = [0] p(c_42) = [0] p(c_43) = [0] p(c_44) = [0] p(c_45) = [0] p(c_46) = [0] p(c_47) = [0] p(c_48) = [0] p(c_49) = [0] p(c_50) = [1] x1 + [0] p(c_51) = [1] p(c_52) = [1] x1 + [0] p(c_53) = [0] p(c_54) = [1] x1 + [2] p(c_55) = [1] x1 + [2] p(c_56) = [2] p(c_57) = [1] x1 + [1] p(c_58) = [1] p(c_59) = [1] p(c_60) = [0] p(c_61) = [0] p(c_62) = [1] p(c_63) = [1] Following rules are strictly oriented: INSERT#2#(#true(),z0,z1,z2) = [1] z2 + [2] > [1] z2 + [0] = c_14(INSERT#(z0,z2)) Following rules are (at-least) weakly oriented: APPEND#(z0,z1) = [1] z0 + [1] z1 + [0] >= [1] z0 + [1] z1 + [0] = c_2(APPEND#1#(z0,z1)) APPEND#1#(::(z0,z1),z2) = [1] z1 + [1] z2 + [0] >= [1] z1 + [1] z2 + [0] = c_3(APPEND#(z1,z2)) FLATTEN#(z0) = [1] z0 + [0] >= [1] z0 + [0] = FLATTEN#1#(z0) FLATTEN#1#(node(z0,z1,z2)) = [1] z0 + [1] z1 + [1] z2 + [7] >= [1] z0 + [1] z1 + [1] z2 + [3] = APPEND#(z0,append(flatten(z1),flatten(z2))) FLATTEN#1#(node(z0,z1,z2)) = [1] z0 + [1] z1 + [1] z2 + [7] >= [1] z1 + [1] z2 + [2] = APPEND#(flatten(z1),flatten(z2)) FLATTEN#1#(node(z0,z1,z2)) = [1] z0 + [1] z1 + [1] z2 + [7] >= [1] z1 + [0] = FLATTEN#(z1) FLATTEN#1#(node(z0,z1,z2)) = [1] z0 + [1] z1 + [1] z2 + [7] >= [1] z2 + [0] = FLATTEN#(z2) FLATTENSORT#(z0) = [4] z0 + [4] >= [1] z0 + [3] = INSERTIONSORT#(flatten(z0)) INSERT#(z0,z1) = [1] z1 + [0] >= [1] z1 + [7] = c_10(INSERT#1#(z1,z0)) INSERT#1#(::(z0,z1),z2) = [1] z1 + [2] >= [1] z1 + [2] = c_11(INSERT#2#(#less(z0,z2),z2,z0,z1)) INSERTIONSORT#(z0) = [1] z0 + [2] >= [1] z0 + [2] = INSERTIONSORT#1#(z0) INSERTIONSORT#1#(::(z0,z1)) = [1] z1 + [2] >= [1] z1 + [2] = INSERT#(z0,insertionsort(z1)) INSERTIONSORT#1#(::(z0,z1)) = [1] z1 + [2] >= [1] z1 + [2] = INSERTIONSORT#(z1) #cklt(#EQ()) = [0] >= [0] = #false() #cklt(#GT()) = [0] >= [0] = #false() #cklt(#LT()) = [0] >= [0] = #true() #compare(#0(),#0()) = [0] >= [0] = #EQ() #compare(#0(),#neg(z0)) = [0] >= [0] = #GT() #compare(#0(),#pos(z0)) = [0] >= [0] = #LT() #compare(#0(),#s(z0)) = [0] >= [0] = #LT() #compare(#neg(z0),#0()) = [0] >= [0] = #LT() #compare(#neg(z0),#neg(z1)) = [0] >= [0] = #compare(z1,z0) #compare(#neg(z0),#pos(z1)) = [0] >= [0] = #LT() #compare(#pos(z0),#0()) = [0] >= [0] = #GT() #compare(#pos(z0),#neg(z1)) = [0] >= [0] = #GT() #compare(#pos(z0),#pos(z1)) = [0] >= [0] = #compare(z0,z1) #compare(#s(z0),#0()) = [0] >= [0] = #GT() #compare(#s(z0),#s(z1)) = [0] >= [0] = #compare(z0,z1) #less(z0,z1) = [0] >= [0] = #cklt(#compare(z0,z1)) append(z0,z1) = [1] z0 + [1] z1 + [1] >= [1] z0 + [1] z1 + [1] = append#1(z0,z1) append#1(::(z0,z1),z2) = [1] z1 + [1] z2 + [1] >= [1] z1 + [1] z2 + [1] = ::(z0,append(z1,z2)) append#1(nil(),z0) = [1] z0 + [1] >= [1] z0 + [0] = z0 flatten(z0) = [1] z0 + [1] >= [1] z0 + [1] = flatten#1(z0) flatten#1(leaf()) = [1] >= [0] = nil() flatten#1(node(z0,z1,z2)) = [1] z0 + [1] z1 + [1] z2 + [8] >= [1] z0 + [1] z1 + [1] z2 + [4] = append(z0,append(flatten(z1),flatten(z2))) insert(z0,z1) = [1] z1 + [0] >= [1] z1 + [0] = insert#1(z1,z0) insert#1(::(z0,z1),z2) = [1] z1 + [0] >= [1] z1 + [0] = insert#2(#less(z0,z2),z2,z0,z1) insert#1(nil(),z0) = [0] >= [0] = ::(z0,nil()) insert#2(#false(),z0,z1,z2) = [1] z2 + [0] >= [1] z2 + [0] = ::(z0,::(z1,z2)) insert#2(#true(),z0,z1,z2) = [1] z2 + [0] >= [1] z2 + [0] = ::(z1,insert(z0,z2)) insertionsort(z0) = [1] z0 + [2] >= [1] z0 + [2] = insertionsort#1(z0) insertionsort#1(::(z0,z1)) = [1] z1 + [2] >= [1] z1 + [2] = insert(z0,insertionsort(z1)) insertionsort#1(nil()) = [2] >= [0] = nil() Further, it can be verified that all rules not oriented are covered by the weightgap condition. ** Step 7.b:4: WeightGap. WORST_CASE(?,O(n^1)) + Considered Problem: - Strict DPs: APPEND#(z0,z1) -> c_2(APPEND#1#(z0,z1)) INSERT#(z0,z1) -> c_10(INSERT#1#(z1,z0)) - Weak DPs: APPEND#1#(::(z0,z1),z2) -> c_3(APPEND#(z1,z2)) FLATTEN#(z0) -> FLATTEN#1#(z0) FLATTEN#1#(node(z0,z1,z2)) -> APPEND#(z0,append(flatten(z1),flatten(z2))) FLATTEN#1#(node(z0,z1,z2)) -> APPEND#(flatten(z1),flatten(z2)) FLATTEN#1#(node(z0,z1,z2)) -> FLATTEN#(z1) FLATTEN#1#(node(z0,z1,z2)) -> FLATTEN#(z2) FLATTENSORT#(z0) -> INSERTIONSORT#(flatten(z0)) INSERT#1#(::(z0,z1),z2) -> c_11(INSERT#2#(#less(z0,z2),z2,z0,z1)) INSERT#2#(#true(),z0,z1,z2) -> c_14(INSERT#(z0,z2)) INSERTIONSORT#(z0) -> INSERTIONSORT#1#(z0) INSERTIONSORT#1#(::(z0,z1)) -> INSERT#(z0,insertionsort(z1)) INSERTIONSORT#1#(::(z0,z1)) -> INSERTIONSORT#(z1) - Weak TRS: #cklt(#EQ()) -> #false() #cklt(#GT()) -> #false() #cklt(#LT()) -> #true() #compare(#0(),#0()) -> #EQ() #compare(#0(),#neg(z0)) -> #GT() #compare(#0(),#pos(z0)) -> #LT() #compare(#0(),#s(z0)) -> #LT() #compare(#neg(z0),#0()) -> #LT() #compare(#neg(z0),#neg(z1)) -> #compare(z1,z0) #compare(#neg(z0),#pos(z1)) -> #LT() #compare(#pos(z0),#0()) -> #GT() #compare(#pos(z0),#neg(z1)) -> #GT() #compare(#pos(z0),#pos(z1)) -> #compare(z0,z1) #compare(#s(z0),#0()) -> #GT() #compare(#s(z0),#s(z1)) -> #compare(z0,z1) #less(z0,z1) -> #cklt(#compare(z0,z1)) append(z0,z1) -> append#1(z0,z1) append#1(::(z0,z1),z2) -> ::(z0,append(z1,z2)) append#1(nil(),z0) -> z0 flatten(z0) -> flatten#1(z0) flatten#1(leaf()) -> nil() flatten#1(node(z0,z1,z2)) -> append(z0,append(flatten(z1),flatten(z2))) insert(z0,z1) -> insert#1(z1,z0) insert#1(::(z0,z1),z2) -> insert#2(#less(z0,z2),z2,z0,z1) insert#1(nil(),z0) -> ::(z0,nil()) insert#2(#false(),z0,z1,z2) -> ::(z0,::(z1,z2)) insert#2(#true(),z0,z1,z2) -> ::(z1,insert(z0,z2)) insertionsort(z0) -> insertionsort#1(z0) insertionsort#1(::(z0,z1)) -> insert(z0,insertionsort(z1)) insertionsort#1(nil()) -> nil() - Signature: {#CKLT/1,#COMPARE/2,#LESS/2,#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,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,#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,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,::/2,c/0,c1/0,c10/0,c11/0 ,c12/1,c13/0,c14/1,c15/2,c16/1,c17/1,c18/0,c19/1,c2/0,c20/0,c21/3,c22/3,c23/2,c24/1,c25/2,c26/0,c27/0,c28/1 ,c29/1,c3/0,c30/2,c31/0,c4/0,c5/0,c6/0,c7/0,c8/1,c9/0,leaf/0,nil/0,node/3,c_1/3,c_2/1,c_3/1,c_4/0,c_5/1 ,c_6/0,c_7/3,c_8/3,c_9/2,c_10/1,c_11/1,c_12/0,c_13/0,c_14/1,c_15/1,c_16/2,c_17/0,c_18/0,c_19/0,c_20/0,c_21/0 ,c_22/0,c_23/0,c_24/0,c_25/0,c_26/1,c_27/0,c_28/0,c_29/0,c_30/1,c_31/0,c_32/1,c_33/0,c_34/0,c_35/0,c_36/0 ,c_37/0,c_38/0,c_39/0,c_40/0,c_41/1,c_42/0,c_43/0,c_44/0,c_45/1,c_46/0,c_47/1,c_48/2,c_49/1,c_50/1,c_51/0 ,c_52/1,c_53/0,c_54/4,c_55/2,c_56/1,c_57/2,c_58/0,c_59/0,c_60/1,c_61/1,c_62/2,c_63/0} - Obligation: innermost runtime complexity wrt. defined symbols {#CKLT#,#COMPARE#,#LESS#,#cklt#,#compare#,#less#,APPEND# ,APPEND#1#,FLATTEN#,FLATTEN#1#,FLATTENSORT#,INSERT#,INSERT#1#,INSERT#2#,INSERTIONSORT#,INSERTIONSORT#1# ,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,::,c,c1,c10,c11,c12,c13,c14 ,c15,c16,c17,c18,c19,c2,c20,c21,c22,c23,c24,c25,c26,c27,c28,c29,c3,c30,c31,c4,c5,c6,c7,c8,c9,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(::) = {2}, uargs(append) = {1,2}, uargs(insert) = {2}, uargs(insert#2) = {1}, uargs(APPEND#) = {1,2}, uargs(INSERT#) = {2}, uargs(INSERT#2#) = {1}, uargs(INSERTIONSORT#) = {1}, uargs(c_2) = {1}, uargs(c_3) = {1}, uargs(c_10) = {1}, uargs(c_11) = {1}, uargs(c_14) = {1} Following symbols are considered usable: all TcT has computed the following interpretation: p(#0) = [0] p(#CKLT) = [0] p(#COMPARE) = [0] p(#EQ) = [0] p(#GT) = [0] p(#LESS) = [0] p(#LT) = [0] p(#cklt) = [1] x1 + [1] p(#compare) = [0] p(#false) = [1] p(#less) = [1] p(#neg) = [1] x1 + [0] p(#pos) = [1] x1 + [0] p(#s) = [1] x1 + [0] p(#true) = [1] p(::) = [1] x2 + [4] p(APPEND) = [0] p(APPEND#1) = [0] p(FLATTEN) = [0] p(FLATTEN#1) = [0] p(FLATTENSORT) = [0] p(INSERT) = [0] p(INSERT#1) = [0] p(INSERT#2) = [0] p(INSERTIONSORT) = [0] p(INSERTIONSORT#1) = [0] p(append) = [1] x1 + [1] x2 + [0] p(append#1) = [1] x1 + [1] x2 + [0] p(c) = [0] p(c1) = [0] p(c10) = [0] p(c11) = [0] p(c12) = [1] x1 + [0] p(c13) = [0] p(c14) = [1] x1 + [0] p(c15) = [1] x1 + [1] x2 + [0] p(c16) = [1] x1 + [0] p(c17) = [1] x1 + [0] p(c18) = [0] p(c19) = [1] x1 + [0] p(c2) = [0] p(c20) = [0] p(c21) = [1] x1 + [1] x2 + [1] x3 + [0] p(c22) = [1] x1 + [1] x2 + [1] x3 + [0] p(c23) = [1] x1 + [1] x2 + [0] p(c24) = [1] x1 + [0] p(c25) = [1] x1 + [1] x2 + [0] p(c26) = [0] p(c27) = [0] p(c28) = [1] x1 + [0] p(c29) = [1] x1 + [0] p(c3) = [0] p(c30) = [1] x1 + [1] x2 + [0] p(c31) = [0] p(c4) = [0] p(c5) = [0] p(c6) = [0] p(c7) = [0] p(c8) = [1] x1 + [0] p(c9) = [0] p(flatten) = [1] x1 + [0] p(flatten#1) = [1] x1 + [0] p(flattensort) = [0] p(insert) = [1] x2 + [4] p(insert#1) = [1] x1 + [4] p(insert#2) = [1] x1 + [1] x4 + [7] 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#) = [0] p(#COMPARE#) = [0] p(#LESS#) = [0] p(#cklt#) = [0] p(#compare#) = [0] p(#less#) = [0] p(APPEND#) = [1] x1 + [1] x2 + [3] p(APPEND#1#) = [1] x1 + [1] x2 + [0] p(FLATTEN#) = [1] x1 + [3] p(FLATTEN#1#) = [1] x1 + [0] p(FLATTENSORT#) = [2] x1 + [1] p(INSERT#) = [1] x2 + [0] p(INSERT#1#) = [1] x1 + [5] p(INSERT#2#) = [1] x1 + [1] x4 + [3] p(INSERTIONSORT#) = [1] x1 + [1] p(INSERTIONSORT#1#) = [1] x1 + [1] p(append#) = [0] p(append#1#) = [0] p(flatten#) = [0] p(flatten#1#) = [0] p(flattensort#) = [0] p(insert#) = [0] p(insert#1#) = [0] p(insert#2#) = [0] p(insertionsort#) = [0] p(insertionsort#1#) = [0] p(c_1) = [4] x2 + [0] p(c_2) = [1] x1 + [1] p(c_3) = [1] x1 + [1] p(c_4) = [0] p(c_5) = [0] p(c_6) = [0] p(c_7) = [0] p(c_8) = [2] x2 + [0] p(c_9) = [2] x2 + [2] p(c_10) = [1] x1 + [6] p(c_11) = [1] x1 + [5] p(c_12) = [0] p(c_13) = [2] p(c_14) = [1] x1 + [4] p(c_15) = [1] x1 + [0] p(c_16) = [1] x1 + [2] x2 + [0] p(c_17) = [1] p(c_18) = [0] p(c_19) = [0] p(c_20) = [4] p(c_21) = [0] p(c_22) = [2] p(c_23) = [0] p(c_24) = [2] p(c_25) = [1] p(c_26) = [1] x1 + [4] p(c_27) = [0] p(c_28) = [0] p(c_29) = [0] p(c_30) = [1] p(c_31) = [2] p(c_32) = [1] x1 + [0] p(c_33) = [1] p(c_34) = [0] p(c_35) = [0] p(c_36) = [4] p(c_37) = [1] p(c_38) = [0] p(c_39) = [1] p(c_40) = [0] p(c_41) = [1] p(c_42) = [0] p(c_43) = [0] p(c_44) = [1] p(c_45) = [1] x1 + [0] p(c_46) = [0] p(c_47) = [2] p(c_48) = [1] x1 + [1] x2 + [0] p(c_49) = [0] p(c_50) = [1] p(c_51) = [0] p(c_52) = [1] x1 + [1] p(c_53) = [0] p(c_54) = [1] x1 + [2] x3 + [2] x4 + [1] p(c_55) = [4] p(c_56) = [1] x1 + [4] p(c_57) = [1] x1 + [0] p(c_58) = [4] p(c_59) = [0] p(c_60) = [0] p(c_61) = [2] p(c_62) = [1] x1 + [1] x2 + [0] p(c_63) = [0] Following rules are strictly oriented: APPEND#(z0,z1) = [1] z0 + [1] z1 + [3] > [1] z0 + [1] z1 + [1] = c_2(APPEND#1#(z0,z1)) Following rules are (at-least) weakly oriented: APPEND#1#(::(z0,z1),z2) = [1] z1 + [1] z2 + [4] >= [1] z1 + [1] z2 + [4] = c_3(APPEND#(z1,z2)) FLATTEN#(z0) = [1] z0 + [3] >= [1] z0 + [0] = FLATTEN#1#(z0) FLATTEN#1#(node(z0,z1,z2)) = [1] z0 + [1] z1 + [1] z2 + [3] >= [1] z0 + [1] z1 + [1] z2 + [3] = APPEND#(z0,append(flatten(z1),flatten(z2))) FLATTEN#1#(node(z0,z1,z2)) = [1] z0 + [1] z1 + [1] z2 + [3] >= [1] z1 + [1] z2 + [3] = APPEND#(flatten(z1),flatten(z2)) FLATTEN#1#(node(z0,z1,z2)) = [1] z0 + [1] z1 + [1] z2 + [3] >= [1] z1 + [3] = FLATTEN#(z1) FLATTEN#1#(node(z0,z1,z2)) = [1] z0 + [1] z1 + [1] z2 + [3] >= [1] z2 + [3] = FLATTEN#(z2) FLATTENSORT#(z0) = [2] z0 + [1] >= [1] z0 + [1] = INSERTIONSORT#(flatten(z0)) INSERT#(z0,z1) = [1] z1 + [0] >= [1] z1 + [11] = c_10(INSERT#1#(z1,z0)) INSERT#1#(::(z0,z1),z2) = [1] z1 + [9] >= [1] z1 + [9] = c_11(INSERT#2#(#less(z0,z2),z2,z0,z1)) INSERT#2#(#true(),z0,z1,z2) = [1] z2 + [4] >= [1] z2 + [4] = c_14(INSERT#(z0,z2)) INSERTIONSORT#(z0) = [1] z0 + [1] >= [1] z0 + [1] = INSERTIONSORT#1#(z0) INSERTIONSORT#1#(::(z0,z1)) = [1] z1 + [5] >= [1] z1 + [0] = INSERT#(z0,insertionsort(z1)) INSERTIONSORT#1#(::(z0,z1)) = [1] z1 + [5] >= [1] z1 + [1] = INSERTIONSORT#(z1) #cklt(#EQ()) = [1] >= [1] = #false() #cklt(#GT()) = [1] >= [1] = #false() #cklt(#LT()) = [1] >= [1] = #true() #compare(#0(),#0()) = [0] >= [0] = #EQ() #compare(#0(),#neg(z0)) = [0] >= [0] = #GT() #compare(#0(),#pos(z0)) = [0] >= [0] = #LT() #compare(#0(),#s(z0)) = [0] >= [0] = #LT() #compare(#neg(z0),#0()) = [0] >= [0] = #LT() #compare(#neg(z0),#neg(z1)) = [0] >= [0] = #compare(z1,z0) #compare(#neg(z0),#pos(z1)) = [0] >= [0] = #LT() #compare(#pos(z0),#0()) = [0] >= [0] = #GT() #compare(#pos(z0),#neg(z1)) = [0] >= [0] = #GT() #compare(#pos(z0),#pos(z1)) = [0] >= [0] = #compare(z0,z1) #compare(#s(z0),#0()) = [0] >= [0] = #GT() #compare(#s(z0),#s(z1)) = [0] >= [0] = #compare(z0,z1) #less(z0,z1) = [1] >= [1] = #cklt(#compare(z0,z1)) append(z0,z1) = [1] z0 + [1] z1 + [0] >= [1] z0 + [1] z1 + [0] = append#1(z0,z1) append#1(::(z0,z1),z2) = [1] z1 + [1] z2 + [4] >= [1] z1 + [1] z2 + [4] = ::(z0,append(z1,z2)) append#1(nil(),z0) = [1] z0 + [0] >= [1] z0 + [0] = z0 flatten(z0) = [1] z0 + [0] >= [1] z0 + [0] = flatten#1(z0) flatten#1(leaf()) = [0] >= [0] = nil() flatten#1(node(z0,z1,z2)) = [1] z0 + [1] z1 + [1] z2 + [3] >= [1] z0 + [1] z1 + [1] z2 + [0] = append(z0,append(flatten(z1),flatten(z2))) insert(z0,z1) = [1] z1 + [4] >= [1] z1 + [4] = insert#1(z1,z0) insert#1(::(z0,z1),z2) = [1] z1 + [8] >= [1] z1 + [8] = insert#2(#less(z0,z2),z2,z0,z1) insert#1(nil(),z0) = [4] >= [4] = ::(z0,nil()) insert#2(#false(),z0,z1,z2) = [1] z2 + [8] >= [1] z2 + [8] = ::(z0,::(z1,z2)) insert#2(#true(),z0,z1,z2) = [1] z2 + [8] >= [1] z2 + [8] = ::(z1,insert(z0,z2)) insertionsort(z0) = [1] z0 + [0] >= [1] z0 + [0] = insertionsort#1(z0) insertionsort#1(::(z0,z1)) = [1] z1 + [4] >= [1] z1 + [4] = insert(z0,insertionsort(z1)) insertionsort#1(nil()) = [0] >= [0] = nil() Further, it can be verified that all rules not oriented are covered by the weightgap condition. ** Step 7.b:5: NaturalMI. WORST_CASE(?,O(n^1)) + Considered Problem: - Strict DPs: INSERT#(z0,z1) -> c_10(INSERT#1#(z1,z0)) - Weak DPs: APPEND#(z0,z1) -> c_2(APPEND#1#(z0,z1)) APPEND#1#(::(z0,z1),z2) -> c_3(APPEND#(z1,z2)) FLATTEN#(z0) -> FLATTEN#1#(z0) FLATTEN#1#(node(z0,z1,z2)) -> APPEND#(z0,append(flatten(z1),flatten(z2))) FLATTEN#1#(node(z0,z1,z2)) -> APPEND#(flatten(z1),flatten(z2)) FLATTEN#1#(node(z0,z1,z2)) -> FLATTEN#(z1) FLATTEN#1#(node(z0,z1,z2)) -> FLATTEN#(z2) FLATTENSORT#(z0) -> INSERTIONSORT#(flatten(z0)) INSERT#1#(::(z0,z1),z2) -> c_11(INSERT#2#(#less(z0,z2),z2,z0,z1)) INSERT#2#(#true(),z0,z1,z2) -> c_14(INSERT#(z0,z2)) INSERTIONSORT#(z0) -> INSERTIONSORT#1#(z0) INSERTIONSORT#1#(::(z0,z1)) -> INSERT#(z0,insertionsort(z1)) INSERTIONSORT#1#(::(z0,z1)) -> INSERTIONSORT#(z1) - Weak TRS: #cklt(#EQ()) -> #false() #cklt(#GT()) -> #false() #cklt(#LT()) -> #true() #compare(#0(),#0()) -> #EQ() #compare(#0(),#neg(z0)) -> #GT() #compare(#0(),#pos(z0)) -> #LT() #compare(#0(),#s(z0)) -> #LT() #compare(#neg(z0),#0()) -> #LT() #compare(#neg(z0),#neg(z1)) -> #compare(z1,z0) #compare(#neg(z0),#pos(z1)) -> #LT() #compare(#pos(z0),#0()) -> #GT() #compare(#pos(z0),#neg(z1)) -> #GT() #compare(#pos(z0),#pos(z1)) -> #compare(z0,z1) #compare(#s(z0),#0()) -> #GT() #compare(#s(z0),#s(z1)) -> #compare(z0,z1) #less(z0,z1) -> #cklt(#compare(z0,z1)) append(z0,z1) -> append#1(z0,z1) append#1(::(z0,z1),z2) -> ::(z0,append(z1,z2)) append#1(nil(),z0) -> z0 flatten(z0) -> flatten#1(z0) flatten#1(leaf()) -> nil() flatten#1(node(z0,z1,z2)) -> append(z0,append(flatten(z1),flatten(z2))) insert(z0,z1) -> insert#1(z1,z0) insert#1(::(z0,z1),z2) -> insert#2(#less(z0,z2),z2,z0,z1) insert#1(nil(),z0) -> ::(z0,nil()) insert#2(#false(),z0,z1,z2) -> ::(z0,::(z1,z2)) insert#2(#true(),z0,z1,z2) -> ::(z1,insert(z0,z2)) insertionsort(z0) -> insertionsort#1(z0) insertionsort#1(::(z0,z1)) -> insert(z0,insertionsort(z1)) insertionsort#1(nil()) -> nil() - Signature: {#CKLT/1,#COMPARE/2,#LESS/2,#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,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,#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,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,::/2,c/0,c1/0,c10/0,c11/0 ,c12/1,c13/0,c14/1,c15/2,c16/1,c17/1,c18/0,c19/1,c2/0,c20/0,c21/3,c22/3,c23/2,c24/1,c25/2,c26/0,c27/0,c28/1 ,c29/1,c3/0,c30/2,c31/0,c4/0,c5/0,c6/0,c7/0,c8/1,c9/0,leaf/0,nil/0,node/3,c_1/3,c_2/1,c_3/1,c_4/0,c_5/1 ,c_6/0,c_7/3,c_8/3,c_9/2,c_10/1,c_11/1,c_12/0,c_13/0,c_14/1,c_15/1,c_16/2,c_17/0,c_18/0,c_19/0,c_20/0,c_21/0 ,c_22/0,c_23/0,c_24/0,c_25/0,c_26/1,c_27/0,c_28/0,c_29/0,c_30/1,c_31/0,c_32/1,c_33/0,c_34/0,c_35/0,c_36/0 ,c_37/0,c_38/0,c_39/0,c_40/0,c_41/1,c_42/0,c_43/0,c_44/0,c_45/1,c_46/0,c_47/1,c_48/2,c_49/1,c_50/1,c_51/0 ,c_52/1,c_53/0,c_54/4,c_55/2,c_56/1,c_57/2,c_58/0,c_59/0,c_60/1,c_61/1,c_62/2,c_63/0} - Obligation: innermost runtime complexity wrt. defined symbols {#CKLT#,#COMPARE#,#LESS#,#cklt#,#compare#,#less#,APPEND# ,APPEND#1#,FLATTEN#,FLATTEN#1#,FLATTENSORT#,INSERT#,INSERT#1#,INSERT#2#,INSERTIONSORT#,INSERTIONSORT#1# ,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,::,c,c1,c10,c11,c12,c13,c14 ,c15,c16,c17,c18,c19,c2,c20,c21,c22,c23,c24,c25,c26,c27,c28,c29,c3,c30,c31,c4,c5,c6,c7,c8,c9,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_2) = {1}, uargs(c_3) = {1}, uargs(c_10) = {1}, uargs(c_11) = {1}, uargs(c_14) = {1} Following symbols are considered usable: {append,append#1,flatten,flatten#1,insert,insert#1,insert#2,insertionsort,insertionsort#1,#CKLT#,#COMPARE# ,#LESS#,#cklt#,#compare#,#less#,APPEND#,APPEND#1#,FLATTEN#,FLATTEN#1#,FLATTENSORT#,INSERT#,INSERT#1# ,INSERT#2#,INSERTIONSORT#,INSERTIONSORT#1#,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(#CKLT) = [4] x1 + [1] p(#COMPARE) = [4] p(#EQ) = [4] p(#GT) = [0] p(#LESS) = [2] x2 + [4] p(#LT) = [0] p(#cklt) = [0] p(#compare) = [0] p(#false) = [0] p(#less) = [0] p(#neg) = [0] p(#pos) = [1] x1 + [0] p(#s) = [1] x1 + [1] p(#true) = [0] p(::) = [1] x1 + [1] x2 + [1] p(APPEND) = [4] x1 + [1] p(APPEND#1) = [2] p(FLATTEN) = [1] p(FLATTEN#1) = [0] p(FLATTENSORT) = [2] x1 + [0] p(INSERT) = [1] x2 + [0] p(INSERT#1) = [2] x2 + [2] p(INSERT#2) = [2] x1 + [4] x2 + [0] p(INSERTIONSORT) = [0] p(INSERTIONSORT#1) = [1] p(append) = [1] x1 + [1] x2 + [0] p(append#1) = [1] x1 + [1] x2 + [0] p(c) = [0] p(c1) = [1] p(c10) = [0] p(c11) = [4] p(c12) = [1] p(c13) = [0] p(c14) = [0] p(c15) = [1] x2 + [4] p(c16) = [0] p(c17) = [4] p(c18) = [2] p(c19) = [0] p(c2) = [0] p(c20) = [1] p(c21) = [1] x1 + [1] x2 + [1] x3 + [1] p(c22) = [1] x2 + [1] x3 + [1] p(c23) = [1] p(c24) = [1] x1 + [2] p(c25) = [0] p(c26) = [1] p(c27) = [0] p(c28) = [1] p(c29) = [0] p(c3) = [1] p(c30) = [1] x1 + [0] p(c31) = [2] p(c4) = [1] p(c5) = [1] p(c6) = [0] p(c7) = [0] p(c8) = [1] p(c9) = [0] p(flatten) = [1] x1 + [0] p(flatten#1) = [1] x1 + [0] p(flattensort) = [0] p(insert) = [1] x1 + [1] x2 + [1] p(insert#1) = [1] x1 + [1] x2 + [1] p(insert#2) = [1] x2 + [1] x3 + [1] x4 + [2] p(insertionsort) = [1] x1 + [0] p(insertionsort#1) = [1] x1 + [0] p(leaf) = [3] p(nil) = [0] p(node) = [1] x1 + [1] x2 + [1] x3 + [0] p(#CKLT#) = [1] x1 + [4] p(#COMPARE#) = [1] p(#LESS#) = [2] x2 + [1] p(#cklt#) = [0] p(#compare#) = [4] x1 + [4] p(#less#) = [1] x1 + [1] p(APPEND#) = [0] p(APPEND#1#) = [0] p(FLATTEN#) = [5] p(FLATTEN#1#) = [5] p(FLATTENSORT#) = [7] x1 + [4] p(INSERT#) = [4] x1 + [4] x2 + [1] p(INSERT#1#) = [4] x1 + [4] x2 + [0] p(INSERT#2#) = [4] x2 + [4] x3 + [4] x4 + [4] p(INSERTIONSORT#) = [7] x1 + [1] p(INSERTIONSORT#1#) = [7] x1 + [1] p(append#) = [1] x1 + [4] x2 + [1] p(append#1#) = [2] x1 + [0] p(flatten#) = [1] x1 + [4] p(flatten#1#) = [0] p(flattensort#) = [1] p(insert#) = [1] x1 + [0] p(insert#1#) = [1] x1 + [0] p(insert#2#) = [2] x1 + [1] x3 + [0] p(insertionsort#) = [1] x1 + [1] p(insertionsort#1#) = [1] p(c_1) = [1] x2 + [2] p(c_2) = [2] x1 + [0] p(c_3) = [1] x1 + [0] p(c_4) = [0] p(c_5) = [0] p(c_6) = [1] p(c_7) = [1] x1 + [0] p(c_8) = [4] x1 + [4] x3 + [1] p(c_9) = [4] x1 + [1] x2 + [0] p(c_10) = [1] x1 + [0] p(c_11) = [1] x1 + [0] p(c_12) = [0] p(c_13) = [1] p(c_14) = [1] x1 + [3] p(c_15) = [1] x1 + [2] p(c_16) = [2] x1 + [1] x2 + [1] p(c_17) = [0] p(c_18) = [0] p(c_19) = [1] p(c_20) = [0] p(c_21) = [4] p(c_22) = [0] p(c_23) = [1] p(c_24) = [0] p(c_25) = [1] p(c_26) = [0] p(c_27) = [1] p(c_28) = [1] p(c_29) = [1] p(c_30) = [2] x1 + [0] p(c_31) = [1] p(c_32) = [0] p(c_33) = [0] p(c_34) = [4] p(c_35) = [2] p(c_36) = [1] p(c_37) = [4] p(c_38) = [4] p(c_39) = [4] p(c_40) = [1] p(c_41) = [2] x1 + [2] p(c_42) = [1] p(c_43) = [0] p(c_44) = [1] p(c_45) = [2] x1 + [0] p(c_46) = [0] p(c_47) = [0] p(c_48) = [1] x1 + [1] x2 + [0] p(c_49) = [4] p(c_50) = [0] p(c_51) = [1] p(c_52) = [1] x1 + [1] p(c_53) = [2] p(c_54) = [1] x2 + [1] p(c_55) = [1] x1 + [0] p(c_56) = [0] p(c_57) = [4] x1 + [0] p(c_58) = [0] p(c_59) = [1] p(c_60) = [1] x1 + [1] p(c_61) = [1] x1 + [1] p(c_62) = [2] x2 + [1] p(c_63) = [1] Following rules are strictly oriented: INSERT#(z0,z1) = [4] z0 + [4] z1 + [1] > [4] z0 + [4] z1 + [0] = c_10(INSERT#1#(z1,z0)) Following rules are (at-least) weakly oriented: APPEND#(z0,z1) = [0] >= [0] = c_2(APPEND#1#(z0,z1)) APPEND#1#(::(z0,z1),z2) = [0] >= [0] = c_3(APPEND#(z1,z2)) FLATTEN#(z0) = [5] >= [5] = FLATTEN#1#(z0) FLATTEN#1#(node(z0,z1,z2)) = [5] >= [0] = APPEND#(z0,append(flatten(z1),flatten(z2))) FLATTEN#1#(node(z0,z1,z2)) = [5] >= [0] = APPEND#(flatten(z1),flatten(z2)) FLATTEN#1#(node(z0,z1,z2)) = [5] >= [5] = FLATTEN#(z1) FLATTEN#1#(node(z0,z1,z2)) = [5] >= [5] = FLATTEN#(z2) FLATTENSORT#(z0) = [7] z0 + [4] >= [7] z0 + [1] = INSERTIONSORT#(flatten(z0)) INSERT#1#(::(z0,z1),z2) = [4] z0 + [4] z1 + [4] z2 + [4] >= [4] z0 + [4] z1 + [4] z2 + [4] = c_11(INSERT#2#(#less(z0,z2),z2,z0,z1)) INSERT#2#(#true(),z0,z1,z2) = [4] z0 + [4] z1 + [4] z2 + [4] >= [4] z0 + [4] z2 + [4] = c_14(INSERT#(z0,z2)) INSERTIONSORT#(z0) = [7] z0 + [1] >= [7] z0 + [1] = INSERTIONSORT#1#(z0) INSERTIONSORT#1#(::(z0,z1)) = [7] z0 + [7] z1 + [8] >= [4] z0 + [4] z1 + [1] = INSERT#(z0,insertionsort(z1)) INSERTIONSORT#1#(::(z0,z1)) = [7] z0 + [7] z1 + [8] >= [7] z1 + [1] = INSERTIONSORT#(z1) append(z0,z1) = [1] z0 + [1] z1 + [0] >= [1] z0 + [1] z1 + [0] = append#1(z0,z1) append#1(::(z0,z1),z2) = [1] z0 + [1] z1 + [1] z2 + [1] >= [1] z0 + [1] z1 + [1] z2 + [1] = ::(z0,append(z1,z2)) append#1(nil(),z0) = [1] z0 + [0] >= [1] z0 + [0] = z0 flatten(z0) = [1] z0 + [0] >= [1] z0 + [0] = flatten#1(z0) flatten#1(leaf()) = [3] >= [0] = nil() flatten#1(node(z0,z1,z2)) = [1] z0 + [1] z1 + [1] z2 + [0] >= [1] z0 + [1] z1 + [1] z2 + [0] = append(z0,append(flatten(z1),flatten(z2))) insert(z0,z1) = [1] z0 + [1] z1 + [1] >= [1] z0 + [1] z1 + [1] = insert#1(z1,z0) insert#1(::(z0,z1),z2) = [1] z0 + [1] z1 + [1] z2 + [2] >= [1] z0 + [1] z1 + [1] z2 + [2] = insert#2(#less(z0,z2),z2,z0,z1) insert#1(nil(),z0) = [1] z0 + [1] >= [1] z0 + [1] = ::(z0,nil()) insert#2(#false(),z0,z1,z2) = [1] z0 + [1] z1 + [1] z2 + [2] >= [1] z0 + [1] z1 + [1] z2 + [2] = ::(z0,::(z1,z2)) insert#2(#true(),z0,z1,z2) = [1] z0 + [1] z1 + [1] z2 + [2] >= [1] z0 + [1] z1 + [1] z2 + [2] = ::(z1,insert(z0,z2)) insertionsort(z0) = [1] z0 + [0] >= [1] z0 + [0] = insertionsort#1(z0) insertionsort#1(::(z0,z1)) = [1] z0 + [1] z1 + [1] >= [1] z0 + [1] z1 + [1] = insert(z0,insertionsort(z1)) insertionsort#1(nil()) = [0] >= [0] = nil() ** Step 7.b:6: EmptyProcessor. WORST_CASE(?,O(1)) + Considered Problem: - Weak DPs: APPEND#(z0,z1) -> c_2(APPEND#1#(z0,z1)) APPEND#1#(::(z0,z1),z2) -> c_3(APPEND#(z1,z2)) FLATTEN#(z0) -> FLATTEN#1#(z0) FLATTEN#1#(node(z0,z1,z2)) -> APPEND#(z0,append(flatten(z1),flatten(z2))) FLATTEN#1#(node(z0,z1,z2)) -> APPEND#(flatten(z1),flatten(z2)) FLATTEN#1#(node(z0,z1,z2)) -> FLATTEN#(z1) FLATTEN#1#(node(z0,z1,z2)) -> FLATTEN#(z2) FLATTENSORT#(z0) -> INSERTIONSORT#(flatten(z0)) INSERT#(z0,z1) -> c_10(INSERT#1#(z1,z0)) INSERT#1#(::(z0,z1),z2) -> c_11(INSERT#2#(#less(z0,z2),z2,z0,z1)) INSERT#2#(#true(),z0,z1,z2) -> c_14(INSERT#(z0,z2)) INSERTIONSORT#(z0) -> INSERTIONSORT#1#(z0) INSERTIONSORT#1#(::(z0,z1)) -> INSERT#(z0,insertionsort(z1)) INSERTIONSORT#1#(::(z0,z1)) -> INSERTIONSORT#(z1) - Weak TRS: #cklt(#EQ()) -> #false() #cklt(#GT()) -> #false() #cklt(#LT()) -> #true() #compare(#0(),#0()) -> #EQ() #compare(#0(),#neg(z0)) -> #GT() #compare(#0(),#pos(z0)) -> #LT() #compare(#0(),#s(z0)) -> #LT() #compare(#neg(z0),#0()) -> #LT() #compare(#neg(z0),#neg(z1)) -> #compare(z1,z0) #compare(#neg(z0),#pos(z1)) -> #LT() #compare(#pos(z0),#0()) -> #GT() #compare(#pos(z0),#neg(z1)) -> #GT() #compare(#pos(z0),#pos(z1)) -> #compare(z0,z1) #compare(#s(z0),#0()) -> #GT() #compare(#s(z0),#s(z1)) -> #compare(z0,z1) #less(z0,z1) -> #cklt(#compare(z0,z1)) append(z0,z1) -> append#1(z0,z1) append#1(::(z0,z1),z2) -> ::(z0,append(z1,z2)) append#1(nil(),z0) -> z0 flatten(z0) -> flatten#1(z0) flatten#1(leaf()) -> nil() flatten#1(node(z0,z1,z2)) -> append(z0,append(flatten(z1),flatten(z2))) insert(z0,z1) -> insert#1(z1,z0) insert#1(::(z0,z1),z2) -> insert#2(#less(z0,z2),z2,z0,z1) insert#1(nil(),z0) -> ::(z0,nil()) insert#2(#false(),z0,z1,z2) -> ::(z0,::(z1,z2)) insert#2(#true(),z0,z1,z2) -> ::(z1,insert(z0,z2)) insertionsort(z0) -> insertionsort#1(z0) insertionsort#1(::(z0,z1)) -> insert(z0,insertionsort(z1)) insertionsort#1(nil()) -> nil() - Signature: {#CKLT/1,#COMPARE/2,#LESS/2,#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,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,#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,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,::/2,c/0,c1/0,c10/0,c11/0 ,c12/1,c13/0,c14/1,c15/2,c16/1,c17/1,c18/0,c19/1,c2/0,c20/0,c21/3,c22/3,c23/2,c24/1,c25/2,c26/0,c27/0,c28/1 ,c29/1,c3/0,c30/2,c31/0,c4/0,c5/0,c6/0,c7/0,c8/1,c9/0,leaf/0,nil/0,node/3,c_1/3,c_2/1,c_3/1,c_4/0,c_5/1 ,c_6/0,c_7/3,c_8/3,c_9/2,c_10/1,c_11/1,c_12/0,c_13/0,c_14/1,c_15/1,c_16/2,c_17/0,c_18/0,c_19/0,c_20/0,c_21/0 ,c_22/0,c_23/0,c_24/0,c_25/0,c_26/1,c_27/0,c_28/0,c_29/0,c_30/1,c_31/0,c_32/1,c_33/0,c_34/0,c_35/0,c_36/0 ,c_37/0,c_38/0,c_39/0,c_40/0,c_41/1,c_42/0,c_43/0,c_44/0,c_45/1,c_46/0,c_47/1,c_48/2,c_49/1,c_50/1,c_51/0 ,c_52/1,c_53/0,c_54/4,c_55/2,c_56/1,c_57/2,c_58/0,c_59/0,c_60/1,c_61/1,c_62/2,c_63/0} - Obligation: innermost runtime complexity wrt. defined symbols {#CKLT#,#COMPARE#,#LESS#,#cklt#,#compare#,#less#,APPEND# ,APPEND#1#,FLATTEN#,FLATTEN#1#,FLATTENSORT#,INSERT#,INSERT#1#,INSERT#2#,INSERTIONSORT#,INSERTIONSORT#1# ,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,::,c,c1,c10,c11,c12,c13,c14 ,c15,c16,c17,c18,c19,c2,c20,c21,c22,c23,c24,c25,c26,c27,c28,c29,c3,c30,c31,c4,c5,c6,c7,c8,c9,leaf,nil,node} + Applied Processor: EmptyProcessor + Details: The problem is already closed. The intended complexity is O(1). WORST_CASE(?,O(n^2))